Todo revision 8338fbf3cfb9cf981261d893286f070bd9fa17ef
general:
pToken, oBraceT, etc. do not allow to be followed by (a line-comment)
annotations. Call wrapAnnos if needed.
haddockify code
checking legality of internal and external terms is missing
subtypes are treated like type synonyms. Function and product types
are builtin. Subtypes relations of these builtin types and user
defined types are problematic. The unit type is a separat type!
class names are not considered for mapping (Morphism.hs)
exhaustive and overlapping patterns are not checked for several
program equations or case patterns. (Merge.hs?)
Sentences for attributes comm, assoc, unit are not generated yet.
datatypes:
Data types result in special data type sentences that imply the usual
equations, only selector equations are generated (so
that they may become program equations)
Operations (constructors) in DatatypeDefns are not renamed (selectors
are also not renamed in DatatypeSens, because they are not used)
types:
(Add known function subtypings '__->__ < __->?__', does not seem to be
necessary, though.)
Lazy typings are not handled yet
terms:
polymorphic (and constrained) let bindings are not supported
yet, because variables are monomorph
checking for a legal let-Pattern (a variable applied to arguments) for
executable terms (ProgEq.hs).
Overloading is forbidden for builtin functions
shorter printing of terms
terms in sentences (from formulas) are not quantified
over global variables
misc:
hiding of sub- or supertypes is a problem, with respect to dependent
operations. (SymbolMapAnalysis.hs)
CASL:
Overload.hs should generate Applications for constants rather than
Var_decls (partially implemented)
convert TERM to Mixfix_bracketed terms and use printText0 rather than
showTerm from ShowMixfix
Maybe funKind should be ignored as fun_map key for lookup. (Also the
FunKind value of the mapping seems to be redundant, as it could also
be looked up in the target signature.)
Maybe the translated type should be stored as value rather than only
the funKind.
id mappings should be represented by empty maps (as for HasCASL)
Maybe in CASL.Morphism.compose the target(m1) only needs to be a
subsignature of the source(m2) (as for HasCASL)
conversion HsSyn and AHsSyn is stupid
AxiomBinds are not renamed
PrintModuleInfo is entirely faked and unusable for showing a Haskell
theory that was directly read in (form a .het file and Haskell code in
curly braces.)
for logic Haskell static analysis is not executed because its result
is unused (also parser error messages are poor)
ToHaskell:
formulas are not translated to Hassle Axioms
free types with subtypes components get too few constructors (and
become disjoint types)
comparing symbol sets with (symbol-) equality may be a problem
legal_obj (Logic.hs) is currently unused
signatures should be always legal by construction
Design a comand line interface to trigger various outputs and
translations (without daVinci!) to allow for profiling