Commit cfbb7849 authored by POTTIER Francois's avatar POTTIER Francois


parent da8f46c8
Relax ba so as to not require well-formedness?
Define wf separately, relying on ba_wf internally.
Global uniqueness, or uniqueness along a branch?
Which wf criterion do we want?
Implement avoid, which renames the bound names of a term so as to
avoid a certain set of names.
......@@ -11,33 +20,16 @@ Or, suppose I want to annotate every abstraction with the
Can I easily do it?
Need a map_reduce visitor?
If TVar is a constructor of some type other than term
(e.g. value: one substitutes values for variables in terms)
then Toolbox must be adapted.
Check that every module has an .mli file, except where that would be too heavy.
The type (_, _) abstraction could be transparent, private, or opaque.
Benchmark fa versus fa' and decide which one to keep.
Possibly cut Toolbox.Make down into several smaller functors.
At least [subst] should be a separate functor.
Operations on terms:
simultaneous opening? (nominal)
conversion from debruijn back to nominal
a printer for debruijn terms?
-- test for global uniqueness everywhere an environment is extended?
Operations on each kind of environment:
Entering a binder (and testing for global uniqueness).
Add printers for Atom.Map
and possibly the various kinds of environments that we use.
Document the precondition and postcondition of every function
in terms of ownership of atoms.
Document the precondition and postcondition of every function.
Deal with more complex forms of binding.
......@@ -51,9 +43,3 @@ Look at the visitors in Why3.
Can we treat 'bn specially so that we do not need to implement visit_'bn?
Or should we just mark 'bn as [@opaque] so as to get visit_'bn for free? Ugly.
Operations in nominal style, without the GUH.
Capture-avoiding substitution with freshening of bound names.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment