Todo revision 15c12a3ac049a4528da05b1017b78145f308aeb0
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadespToken, oBraceT, etc. do not allow to be followed by (a line-comment)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesannotations. Call wrapAnnos if needed.
9211e875148588ca96988bb781a27b96ac33adfaDaniel Mustieleshaddockify code
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadeschecking legality of internal and external terms is missing
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadessubtypes are treated like type synonyms. Function and product types
264c0eb76d6dbbf69369c8c2a44417d0655c57caDaniele Medriare builtin. The unit type is the empty product type. Subtypes
00ff00260ad0bdf35d0b2142e42b411cd2a5917bDaniele Medrirelations of these builtin types and user defined types are
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesclass names are not considered for mapping (Morphism.hs)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesexhaustive and overlapping patterns are not checked for several
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesprogram equations or case patterns. (Merge.hs?)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesSentences for attributes comm, assoc, unit are not generated yet.
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesData types result in special data type sentences that imply the usual
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesequations, only selector equations are generated (so
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesthat they may become program equations)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesOperations (constructors) in DatatypeDefns are not renamed (selectors
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesare also not renamed in DatatypeSens, because they are not used)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadescurrently certain subtype relations are checked, but unification still
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadeschecks relatedTypeIds (and fails in Secd.hascasl and Numbers.casl without this)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadespolymorphic (and constrained) let bindings are not supported
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesyet, because variables are monomorph
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadeschecking for a legal let-Pattern (a variable applied to arguments) for
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesexecutable terms (ProgEq.hs).
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesOverloading is forbidden for builtin functions
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesshorter printing of terms
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesterms in sentences (from formulas) are not quantified
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesover global variables
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadeshiding of sub- or supertypes is a problem, with respect to dependent
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesOverload.hs should generate Applications for constants rather than
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesVar_decls (partially implemented)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesconvert TERM to Mixfix_bracketed terms and use printText0 rather than
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesshowTerm from ShowMixfix
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesMaybe funKind should be ignored as fun_map key for lookup. (Also the
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesFunKind value of the mapping seems to be redundant, as it could also
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesbe looked up in the target signature.)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesMaybe the translated type should be stored as value rather than only
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesid mappings should be represented by empty maps (as for HasCASL)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesMaybe in CASL.Morphism.compose the target(m1) only needs to be a
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadessubsignature of the source(m2) (as for HasCASL)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesconversion HsSyn and AHsSyn is stupid
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesAxiomBinds are not renamed
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesPrintModuleInfo is entirely faked and unusable for showing a Haskell
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadestheory that was directly read in (form a .het file and Haskell code in
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadescurly braces.)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesfor logic Haskell static analysis is not executed because its result
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesis unused (also parser error messages are poor)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesformulas are not translated to Hassle Axioms
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesfree types with subtypes components get too few constructors (and
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadesbecome disjoint types)
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadescomparing symbol sets with (symbol-) equality may be a problem
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadeslegal_obj (Logic.hs) is currently unused
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadessignatures should be always legal by construction
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex PuchadesDesign a comand line interface to trigger various outputs and
946c950fec6d1f74b5f4f443ddeda64cca7b58ccAlex Puchadestranslations (without daVinci!) to allow for profiling