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

proper type terms as supertypes 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)

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:

Make sure that no supertypes are

declared for type synonyms. Cyclic atomic supertypes are not supported

yet. In MinType the equality of terms and the overload relation of

their types is not properly computed!

The supertype relation is not checked in isSubEnv and diffEnv

(AsToLe).

terms:

polymorphic (and constrained) let bindings are not supported

yet.

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

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.

the LHS type of a program equation is not propagated to the RHS

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)

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)

SimpleDatatypes.casl cannot be translated, because of wrong names

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