general:

pToken, oBraceT, etc. do not allow to be followed by (a line-comment)

annotations. Call wrapAnnos if needed.

report other uninspected annotations

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

let the example test/CastFun.hascasl go through

(the variable v for s --> s is to early or wrongly substituted

in s ->? s < v. Maybe a variable also for the arrow must be

introduced in shapeMgu.)

remove FunType and ProductType in favour of uniform TypeAppls

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

redeclaration for builtin identifiers are ignored

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.

MixAna only recognises new variables and thus cannot check for shadowing

First try type checking without lazy types

implement empty lambda terms as functions from Unit

(test/EmptyLambda.hascasl)

CASL:

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 Hatchet static analysis is not executed because its result

is unused (also parser error messages are poor)

Haskell:

formulas are not translated to P-Logic Axioms

class and instance stuff is filtered out in Haskell/HatAna (as

conflict with the prelude)

free types with subtypes components get too few constructors (and

become disjoint types, see HasCASL/Secd.het)

Programatica's output of decorated modules is not legal haskell

wrt. inserted dictionaries

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

(started)