Todo revision 1987182fcaa48837e7b6a323e22cfb0cb57c667c
15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaederpToken, oBraceT, etc. do not allow to be followed by (a line-comment)
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederannotations. Call wrapAnnos if needed.
adf0cd9e940150b6e835cc0ad1266cfbf9e011b3Christian Maederreport other uninspected annotations
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederhaddockify code
975642b989852fc24119c59cf40bc1af653608ffChristian Maederproper type terms as supertypes are reduced to subtypes of higher kind
975642b989852fc24119c59cf40bc1af653608ffChristian Maederand a type synonym for the subtype that (now) must not occur
e12060f6b377b0783138431a3716126e12a6671eChristian MaederFour function- and (many) product type names are builtin in order to
975642b989852fc24119c59cf40bc1af653608ffChristian Maederconstruct type applications. The unit type is a separate type (and
975642b989852fc24119c59cf40bc1af653608ffChristian Maedernot the empty product).
111c54f59f3ecc9c19dbe84565dff8839a4c7b43Christian Maederclass names are not considered for mapping (Morphism.hs)
e12060f6b377b0783138431a3716126e12a6671eChristian Maederclass- and type names are kept disjoint
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederData types result in special data type sentences that imply the usual
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederequations, only selector equations are generated (so
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederthat they may become program equations)
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederOperations (constructors) in DatatypeDefns are not renamed (selectors
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederare also not renamed in DatatypeSens, because they are not used)
e12060f6b377b0783138431a3716126e12a6671eChristian MaederMake sure that no supertypes are declared for type synonyms.
e12060f6b377b0783138431a3716126e12a6671eChristian MaederCyclic atomic supertypes are rejected.
e12060f6b377b0783138431a3716126e12a6671eChristian MaederImprove error messages for further (or repeated) non-atomic subtype
e12060f6b377b0783138431a3716126e12a6671eChristian Maederdeclarations for the same sybtype.
87147fc0ce51105c46094830194fe3191d29ddfaChristian MaederIn MinType the equality of terms and the overload relation of their
87147fc0ce51105c46094830194fe3191d29ddfaChristian Maedertypes is not properly computed!
17448f712ed5116e6e6d2df84205cfdaae210620Christian MaederThe supertype relation is not checked in isSubEnv and diffEnv
975642b989852fc24119c59cf40bc1af653608ffChristian Maedersentences need to be generated for subtype definitions!
f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maederthe order of types in instance lists is given by the order of the
f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maedervariables that needed to be declared before!
67d010c0b09f8bf06c8fabbe2543f3c4742ff53cChristian Maederpolymorphic (and constrained) let bindings are not supported
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederchecking for a legal let-Pattern (a variable applied to arguments) for
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederexecutable terms (ProgEq.hs).
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maederredeclarations of builtin identifiers are forbidden and ignored. Do
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maedernot allow to redeclare "__ __"!
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederterms in sentences (from formulas) are not quantified
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maederover global variables. (AsToLe.hs)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederexhaustive and overlapping patterns are not checked for several
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederprogram equations or case patterns. (Merge.hs?)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederSentences for attributes comm, assoc, unit are not generated yet.
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian MaederGenerate a sentence for OpDefns (the currently generated lambda terms
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maedercannot be read back in by CASL).
acc8b88d801c026a46da4e5ba34110c5384ac745Christian MaederMixAna only recognizes unknown variables and thus cannot check for shadowing
d48085f765fca838c1d972d2123601997174583dChristian MaederUnify alone handles lazy types
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian MaederThe removal of types for printing can be refined (propagated to the
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian MaederCurrently the output is ie. "even (0)" but "even 0" would be better if it
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maedermust not be CASL.
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederMaybe in CASL.Morphism.compose the target(m1) only needs to be a
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maedersubsignature of the source(m2) (as for HasCASL)
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederconversion HsSyn and AHsSyn is stupid
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederAxiomBinds are not renamed
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederPrintModuleInfo is entirely faked and unusable for showing a Haskell
e12060f6b377b0783138431a3716126e12a6671eChristian Maedertheory that was directly read in (from a .het file with Haskell code in
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedercurly braces.)
f504d268c5b5bd491c6c9d15cf74cf16ee3feb1fChristian Maederfor logic Hatchet static analysis is not executed because its result
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederis unused (also parser error messages are poor)
f504d268c5b5bd491c6c9d15cf74cf16ee3feb1fChristian Maederformulas are not translated to P-Logic Axioms
0ed1d09c7b7cd6e26b869757509b78f03e140c6aChristian Maederclass and instance stuff is filtered out in Haskell/HatAna (as
0ed1d09c7b7cd6e26b869757509b78f03e140c6aChristian Maederconflict with the prelude)
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederfree types with subtypes components get too few constructors (and
0ed1d09c7b7cd6e26b869757509b78f03e140c6aChristian Maederbecome disjoint types, see HasCASL/Secd.het)
0ed1d09c7b7cd6e26b869757509b78f03e140c6aChristian MaederProgramatica's output of decorated modules is not legal haskell
0ed1d09c7b7cd6e26b869757509b78f03e140c6aChristian Maederwrt. inserted dictionaries
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maederduplicate code at "outputStdout" and "hasErrors"
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maederugly "showDiags{,1}" at "IO (Maybe"
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maederonly use VName.new for the key in constTab by giving instance Eq/Ord
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maedercorrect showAlt, don't do it for HasCASL
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian MaederdelLEdge, removeContraryChanges uses expensive DGraph Eq
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedercomparing symbol sets with (symbol-) equality may be a problem
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederlegal_obj (Logic.hs) is currently unused
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedersignatures should be always legal by construction
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederDesign a comand line interface to trigger various outputs and
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maedertranslations (without daVinci!) to allow for profiling
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maederadd Updateable and Readonly IntMaps for creating and using ATT
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maedertry to detect sharing earlier via addresses and an address map,
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maederadd a function to the class to avoid rewriting of all instances.
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maedertry show/read of ATT directly,
1987182fcaa48837e7b6a323e22cfb0cb57c667cChristian Maedermaybe write Binary instances for Grothendieck and DevGraph, too