Todo revision 4d5f32c7e4e49e726f5d10943be3718afdff73cd
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederhaddockify code
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederadapt language summary (C.1.1, A-2, C-3 - C-8)
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederchecking legality of internal and external terms is missing
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowskisubtypes are treated like type synonyms
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederclass constraints are not checked in function applications
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiclass names are not considered for mapping (Morphism.hs)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederexhaustive and overlapping patterns are not checked for several
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiprogram equations or case patterns. (Merge.hs?)
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiSentences for attributes comm, assoc, unit are not generated yet.
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian MaederData types result in special data type sentences that imply the usual
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederequations, only selector equations are generated (so
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederthat they may become program equations)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederOperations (constructors) in DatatypeDefns are not renamed (selectors
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederare also not renamed in DatatypeSens, because they are not used)
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowskimutual recursive let-equations (and what not?) are not supported yet
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaybe TypeCheck should generate new type variables for unknown
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedervariables (with type "MixfixType []") rather than MixAna
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski(extractBindings).
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maedera wild card pattern (just "__" with lowest precedence?) is missing
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederas-patterns are only partially implemented
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiif-then-else is currently build in, but schould be user-definable.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiAllow for "op if__then__else : ..." .
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiDisallow "=" and "<=>" after "op" to avoid overloading with builtin
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskinames (Builtin.hs) or check for the type when changing terms to
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiprogram equations (ProgEq.hs).
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiAdd a "bottom" or a missing case term to convert conditional equations
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski(implications) to when-else terms.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskichecking for a legal let-Pattern (a variable applied to arguments) for
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiexecutable terms (ProgEq.hs).
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder"__ __" has highest precedence and ":" has (strong) postfix precedence
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder(adapt language summary C.2.1)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedershorter printing of terms
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederterms in sentences (from formulas) are not quantified
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiover global variables
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederhiding of sub- or supertypes is a problem, with respect to dependent
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederOverload.hs should generated Applications for constants rather than
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederconvert TERM to Mixfix_bracketed terms and use printText0 rather than
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian MaedershowTerm from ShowMixfix
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maederassoc ops are partial and may not be found via the fun_map of
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maedermorphisms, but the morphism should also map this partial functions
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maedercorrectly, since morphisms should be applicable to subsignatures.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaybe funKind should be ignored as fun_map key for lookup. (Also the
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederFunKind value of the mapping seems to be redundant, as it could also
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederbe looked up in the target signature.)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederMaybe the translated type should be stored as value rather than only
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maederid mappings should be represented by empty maps (as for HasCASL)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederMaybe in CASL.Morphism.compose the target(m1) only needs to be a
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskisubsignature of the source(m2) (as for HasCASL)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederconversion HsSyn and AHsSyn is stupid
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederAxiomBinds are not renamed
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederPrintModuleInfo is entirely faked and unusable for showing a Haskell
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maedertheory that was directly read in (form a .het file and Haskell code in
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedercurly braces.)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiformulas are not translated to Hassle Axioms
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederoverloaded names are not properly distinguished (Secd.het __+__)
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maederfree types with subtypes components get too few constructors (and
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederbecome disjoint types)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maedercomparing symbol sets with (symbol-) equality may be a problem
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maederlegal_obj (Logic.hs) is currently unused
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maedersignatures should be always legal by construction
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDesign a comand line interface to trigger various outputs and
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertranslations (without daVinci!) to allow for profiling