general:

haddockify code

checking legality of internal and external terms is missing

subtypes are treated like type synonyms. Function and product types

are builtin. The unit type is the empty product type. Subtypes

relations of these builtin types and user defined types are

problematic.

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)

terms:

polymorphic (and constrained) let bindings are not supported

yet, because variables are monomorph

a wild card pattern can be given by a single underscore

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)

TypeSchemes must be uniquely represented (numbered type vars and

expanded aliases)

Try to get rid of expandAlias in Unify.hs (only needed for SymbolMapAnalysis)

CASL:

Overload.hs should generated Applications for constants rather than

Var_decls

convert TERM to Mixfix_bracketed terms and use printText0 rather than

showTerm from ShowMixfix

assoc ops are partial and may not be found via the fun_map of

morphisms, but the morphism should also map this partial functions

correctly, since morphisms should be applicable to subsignatures.

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)

Hatchet/Haskell:

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)

HetAna/Logic:

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