general:

haddockify code

adapt language summary (C.1.1, A-2, C-3 - C-8)

checking legality of internal and external terms is missing

subtypes are treated like type synonyms

class constraints are not checked in function applications

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.

datatyoes:

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:

mutual recursive let-equations (and what not?) are not supported yet

(TypeCheck.hs)

Maybe TypeCheck should generate new type variables for unknown

variables (with type "MixfixType []") rather than MixAna

(extractBindings).

a wild card pattern (just "__" with lowest precedence?) is missing

as-patterns are only partially implemented

Allow for "op if__then__else : ..." .

checking for a legal let-Pattern (a variable applied to arguments) for

executable terms (ProgEq.hs).

Overloading is forbidden for builtin functions

"__ __" has highest precedence and ":" has (strong) postfix precedence

(adapt language summary C.2.1)

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 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.)

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