Todo revision c81507d35d11b2eedf7425a3bb52bceec3224532
9869e75929acd9377aa460074334d8523cf8e822Lennart PoetteringpToken, oBraceT, etc. do not allow to be followed by (a line-comment)
12b42c76672a66c2d4ea7212c14f8f1b5a62b78dTom Gundersenannotations. Call wrapAnnos if needed.
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringreport other uninspected annotations
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringhaddockify code
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringchecking legality of internal and external terms is missing
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringproper type terms as supertypes are treated like type
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringsynonyms. Function and product types are builtin. Subtype relations
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringof these builtin types and user defined types are problematic. The
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringunit type is a separat type!
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringclass names are not considered for mapping (Morphism.hs)
9869e75929acd9377aa460074334d8523cf8e822Lennart PoetteringData types result in special data type sentences that imply the usual
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringequations, only selector equations are generated (so
9869e75929acd9377aa460074334d8523cf8e822Lennart Poetteringthat they may become program equations)
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekOperations (constructors) in DatatypeDefns are not renamed (selectors
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekare also not renamed in DatatypeSens, because they are not used)
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekMake sure that no supertypes are
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekdeclared for type synonyms. Cyclic atomic supertypes are not supported
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekyet. In MinType the equality of terms and the overload relation of
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmektheir types is not properly computed!
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekThe supertype relation is not checked in isSubEnv and diffEnv
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmektest/Double.hascasl (for the function twice) fails
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmeklet the example test/CastFun.hascasl go through
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmek(the variable v for s --> s is to early or wrongly substituted
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekin s ->? s < v. Maybe a variable also for the arrow must be
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekintroduced in shapeMgu.)
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekremove FunType and ProductType in favour of uniform TypeAppls
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekpolymorphic (and constrained) let bindings are not supported
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekchecking for a legal let-Pattern (a variable applied to arguments) for
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekexecutable terms (ProgEq.hs).
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekredeclaration for builtin identifiers are ignored
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekshorter printing of terms
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekterms in sentences (from formulas) are not quantified
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekover global variables
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekexhaustive and overlapping patterns are not checked for several
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekprogram equations or case patterns. (Merge.hs?)
cd72d2044ad28b475bf84a38ba6db45292467dd8Jan EngelhardtSentences for attributes comm, assoc, unit are not generated yet.
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekMixAna only recognises new variables and thus cannot check for shadowing
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekFirst try type checking without lazy types
a8eaaee72a2f06e0fb64fb71de3b71ecba31dafbJan Engelhardtimplement empty lambda terms as functions from Unit
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekMaybe in CASL.Morphism.compose the target(m1) only needs to be a
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmeksubsignature of the source(m2) (as for HasCASL)
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekconversion HsSyn and AHsSyn is stupid
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekAxiomBinds are not renamed
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekPrintModuleInfo is entirely faked and unusable for showing a Haskell
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmektheory that was directly read in (form a .het file and Haskell code in
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekfor logic Hatchet static analysis is not executed because its result
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekis unused (also parser error messages are poor)
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekformulas are not translated to P-Logic Axioms
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekclass and instance stuff is filtered out in Haskell/HatAna (as
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekconflict with the prelude)
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekfree types with subtypes components get too few constructors (and
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekbecome disjoint types, see HasCASL/Secd.het)
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekProgramatica's output of decorated modules is not legal haskell
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekwrt. inserted dictionaries
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmekcomparing symbol sets with (symbol-) equality may be a problem
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmeklegal_obj (Logic.hs) is currently unused
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmeksignatures should be always legal by construction
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-SzmekDesign a comand line interface to trigger various outputs and
798d3a524ea57aaf40cb53858aaa45ec702f012dZbigniew Jędrzejewski-Szmektranslations (without daVinci!) to allow for profiling