[determinacy] static analysis

[FissoreD]

TODO:

• func f i:... o:... (makes things more readable sometimes)
  NOTE: in the current parser, we already have a special case when a function has no output.
  In this case the arrow in the type signature is optional
• Variadic in dtype (no special case for , )
  Ok, but in infer_fold for constants other than comma, we could stop if the call is_wrong, in comma
  we should continue since the cut could make the predicate again deterministic
• review builtins -> todo: stdlib_map and stdlib_set: their main constructor carries a prediate which may impact the determinacy of calls to add, remove etc...
  A similar example below:

  kind k type.
  type k0 (func -> fprop) -> k.
  func fst-proj k -> (func -> fprop).
  fst-proj (k0 F) F.
  pred g.
  
  func give-rel -> prop.
  give-rel g.
  
  func f.
  f :- fst-proj (k0 give-rel) X, X Y, Y. % Note that Y is not a function, but it is difficult to detect

• cleanup env
• What is the type of this p in this code:

  pred p.
  func p.
  func g.
  g :- p.

  Should we consider that p is a function or a relation?
• in pp_args in data.ml, should I check that all inputs are before all outputs?
• change determinacy of Arithmetic tests
• findall signature is not precise enough: it is functional and it returns a list of functional prop if the input is functional
• Difficult case:

  func map (func A -> B), list A -> list B.
  pred divisor i:int, o:int.
  
  func give-div list int -> (list(list int)).
  give-div L L1 :- map (x\y\x y) [map divisor L] L1. % here map is wrongly called in the list, 
                                                     % i.e. x should be rel

• In the spilling (it is also true in master) the type inside Spill is wrong. E.g. if t = (Spill({ty;it},_) then ty is wrong, but it.ty is ok
• In the follwing code, we should check the output of the anonymous functions to have the determinacy expected by its signature

  func f.
  pred rel.
  
  f :-
   F = ((y\ y = rel) : (func -> fprop)),
   F R,
   R.

• For the overlapping check in Coq, be careful about the problematic-subterms as in here: the two non unifying terms {{fun x => f (H x)}} and {{fun y => g (G y)}} are both replaced with a uvar combined with a constraint relating the uvar with the original term. Wrt overlapping check, this will cause a compilation error of the DB...
• lambdas are of course, not the only issues for determinacy when loading clauses with implication operator.
  For example, X = f rel, X => f Y, Y with func f -> func
• error if 2 types only differ by the mode/functionality
• check for grafting and cut (mut excl)
• update Elpi.md

[gares]

please run make menhir-strip-...

[gares]

overall looks good