Todo revision 5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederhaddockify code
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederadapt language summary (C.1.1, A-2, C-3 - C-8)
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederchecking legality of internal and external terms is missing
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedersubtypes are treated like type synonyms
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederclass constraints are not checked in function applications
ac98d93dea3218a8ed35e870fa8ff61d2a1c095cChristian Maederclass names are not considered for mapping (Morphism.hs)
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederexhaustive and overlapping patterns are not checked for several
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederprogram equations or case patterns. (Merge.hs?)
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederSentences for attributes comm, assoc, unit are not generated yet.
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederData types result in special data type sentences that imply the usual
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederequations, but at least selector equations should be 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)
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedermutual recursive let-equations (and what not?) are not supported yet
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederMaybe TypeCheck should generate new type variables for unknown
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedervariables (with type "MixfixType []") rather than MixAna
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maeder(extractBindings).
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedera wild card pattern (just "__" with lowest precedence?) is missing
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederas-patterns are only partially implemented
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederif-then-else is currently build in, but schould be user-definable.
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederAllow for "op if__then__else : ..." .
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederDisallow "=" and "<=>" after "op" to avoid overloading with builtin
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedernames (Builtin.hs) or check for the type when changing terms to
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederprogram equations (ProgEq.hs).
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederAdd a "bottom" or a missing case term to convert conditional equations
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder(implications) to when-else terms.
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederConvert executable formulas "f" or "not f" to program equations "f =
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederTrue" or "f = False"
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederchecking for a legal let-Pattern (a variable applied to arguments) for
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederexecutable terms (ProgEq.hs).
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maeder"__ __" has highest precedence and ":" has (strong) postfix precedence
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maeder(adapt language summary C.2.1)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maedershorter printing of terms
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederterms in sentences (from formulas and definitions) are not quantified
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederover global variables
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederhiding of sub- or supertypes is a problem, with respect to dependent
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederOverload.hs should generated Applications for constants rather than
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederconvert TERM to Mixfix_bracketed terms and use printText0 rather than
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaedershowTerm from ShowMixfix
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederassoc ops are partial and may not be found via the fun_map of
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedermorphisms, but the morphism should also map this partial functions
ac98d93dea3218a8ed35e870fa8ff61d2a1c095cChristian Maedercorrectly, since morphisms should be applicable to subsignatures.
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederMaybe funKind should be ignored as fun_map key for lookup. (Also the
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian MaederFunKind value of the mapping seems to be redundant, as it could also
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederbe looked up in the target signature.)
ac98d93dea3218a8ed35e870fa8ff61d2a1c095cChristian MaederMaybe the translated type should be stored as value rather than only
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederid mappings should be represented by empty maps (as for HasCASL)
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
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedertheory that was directly read in (form a .het file and Haskell code in
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maedercurly braces.)
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederformulas are not translated to Hassle Axioms
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederoverloaded names are not properly distinguished (Secd.het __+__)
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederfree types with subtypes components get too few constructors (and
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederbecome disjoint types)
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