Types are separated from terms

[FissoreD]

• Change the parser: modes and type are parsed and stored in a unique data structure
  • The new syntax pred map i:list A, i:(pred i:A, o:B), o:list B. allows to know modes for the anonymous predicate passed to the map relation symbol
  • A type signature should not allow the discard operator, e.g. pred p i:_ is forbidden
  • A type signature should work only with known types, e.g. pred p i:a where a is not defined is an invalid type declaration for the predicate p
  • It should be invalid to use the syntax type p a1 -> ... -> an if an is prop or o. In this case we should use the pred syntax NOPE
  • Proposition of @gares : use the syntax ttype r1 pred i:(pred i:A, i:B, i:C), i:A, i:B, o:C. for type definition

COMING:

• Typechecking in ocaml instead of elpi (use Coppo-Denzani algo)
• Mode checking by looking at the flow of input/output arguments of predicates
  • if an atom is in negative position input are ground and outputs are set to ground,
  • if an atom is in positive position then inputs are set ground and outputs are checked for groundness after the check of the premises.
  • check for HO predicates passed to HO symbols like map
• Functionality that guarantee that a functional predicate remains functional after the insertion of new clauses with same relation symbols
  • Non overlapping rules
  • If two rules overlap then the first should have a bang
  • Every negative literal which is not in a functional context (a literal not followed by a bang) should be functional so that the rules keep its relation symbol functional
  • Pay attention of locally charged rules (with =>) this could influence the functionality of the predicate

[FissoreD]

A list of todo