GitLab

the verification algorithm must always terminate and be reasonably
performant in practice, but its worst-case complexity is unknown
and probably exponential. What is quite easy when there is only
one recursive definition, becomes difficult when there is a group
of mutually recursive definitions. An educated discussion would
be highly appreciated.

BTW, I had to convert a couple of recursive "logic"s on integers
into an abstract "logic" + axiom. Pretty much all of them supposed
that the argument was non-negative, and thus were non-terminating!

= replaced by ls_equal in core/pretty (was discovered thanks to a Invalid_argument(equal: functional value)

This reverts commit 70a9e16d1d5818186692ca50931712e1fe2f19f0.

completion : complete theories and goals

- introduce a new Theory.tdecl "Meta" to be used for tags
- simplify cloning procedure, get rid of the th_clone field
- when a goal proposition is discarded during cloning, 
  it's still keeped in the theory as a "skip proposition",
  this is needed to preserve/clone every local identifier.
  Skip propositions are eliminated during task formation.
- get rid of a separate Task.tdecl type
- reorganize the Task.task_hd record:
  * use/clone history is cached in a theory-keyed map;
  * meta-properties are cached in a tagname-keyed map.
  This is done to simplify the fine-grained configuration
  of transformations.

- move exception reporting for Ty, Pattern, Term, and Decl
  to Pretty, as it occasionnaly requires some pretty-printing

printer : print_prelude inside printers instead of prover.ml. Required for smt which has its own prelude.

It's not more expressive but much nicer than epsilon.

- provide several helper functions in Task
- Pretty.print_named_task will also print Use and Clone decls

  as it is most often ignored
- check for empty map in t_subst/f_subst
- bugfix: don't forget nested match statements in Decl and Compile_match

- check pattern well-formedness in Pattern
- add arguments to exceptions in Ty and Term