Todo revision ad97909f160c13effd3bc73155aaa2c29902a5a1
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederhaddockify code
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederchecking legality of internal and external terms is missing
780f981d3c8567cfaebdc8c2d6edb0e2c57aae04Christian Maedersubtypes are treated like type synonyms. Function and product types
780f981d3c8567cfaebdc8c2d6edb0e2c57aae04Christian Maederare builtin. The unit type is the empty product type. Subtypes
780f981d3c8567cfaebdc8c2d6edb0e2c57aae04Christian Maederrelations of these builtin types and user defined types are
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
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)
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederavoid returning unresolved types (via recurse t) and terms
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederthat will cause runtime errors later on (MixAna.hs)
67d010c0b09f8bf06c8fabbe2543f3c4742ff53cChristian Maederpolymorphic (and constrained) let bindings are not supported
67d010c0b09f8bf06c8fabbe2543f3c4742ff53cChristian Maederyet, because variables are monomorph
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maedera wild card pattern can be given by a single underscore
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederchecking for a legal let-Pattern (a variable applied to arguments) for
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederexecutable terms (ProgEq.hs).
dc2ce67f56f9d4507503cc2a24f2646c7f2adf6dChristian MaederOverloading is forbidden for builtin functions
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maedershorter printing of terms
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederterms in sentences (from formulas) are not quantified
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederover global variables
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederhiding of sub- or supertypes is a problem, with respect to dependent
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaederTypeSchemes must be uniquely represented (numbered type vars and
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maederexpanded aliases)
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaederTry to get rid of expandAlias in Unify.hs (only needed for SymbolMapAnalysis)
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.)
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederfor logic Haskell static analysis is not executed because its result
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederis unused (also parser error messages are poor)
d34c258c4ee9eb153afab9b22728e9efc27279f7Christian Maederformulas are not translated to Hassle Axioms
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