This commit makes ProofEngineHelpers.select reach its full potentials.
Its arguments are now a conjecture and a pattern and its output is
a conjecture-like structure made of physical pointers to matching subterms
(together with their contexts).
1. new syntax for patterns:
[t] [in p]
where t is the term to be matched and p is the pattern on the hypotheses
and on the conclusion (whose syntax is not changed).
All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
(that also have the optional term in them)
3. the signature of the select function has changed to require the context
(and return a context and not a "context patch"); moreover it performs
now both the search for roots and the search for subterms of the roots
that are alpha-convertible with the optional given term (if any)
WARNING!!!
The following tactics have been commented out for a while:
replace
rewrite
change
fold
1. new syntax for patterns:
[t] [in p]
where t is the term to be matched and p is the pattern on the hypotheses
and on the conclusion (whose syntax is not changed).
All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
(that also have the optional term in them)
3. the signature of the select function has changed to require the context
(and return a context and not a "context patch"); moreover it performs
now both the search for roots and the search for subterms of the roots
that are alpha-convertible with the optional given term (if any)
WARNING!!!
The following tactics have been commented out for a while:
replace
rewrite
change
fold
Incredible bug of simpl fixed: the stack (in the terminology used for the
Krivine's machine) was processed in the wrong context. As a result List.nth
(to get a Rel in the context) used to raise Failure in several cases. The
Failure, however, was catched somewhere in the code of matita and the
failure of simpl was hidden in most of the cases.
A few bug fixes. In particular parsing errors in matitatop when a file is
given to process used to result in entering the ocaml mode. Now the user is
left in the matita mode.
New solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
Pro: no need of doing the weird "#use matitatop.bootstrap" by playing with
ocaml internals.
Pro: local definitions and #opens in matitatop.bootstrap were lost. They are
preserved in .ocamlinit.
Cons: .ocamlinit must be in "." or in $HOME
Cons: it can interfere with other .ocamlinit
Enrico Tassi [Tue, 28 Jun 2005 15:50:22 +0000 (15:50 +0000)]
* new binary matitatop
* command drop enabled for matitatop.
Once dropped use MatitacLib.go () to enter again the matita toplevel.
Use #trace and similar stuff for debugging.
Add printers for abstract data types in matitatop.bootstrap
A few other tactics made available to matita.
A few tactics (change, fold, replace) generalized to patterns.
The argument of clear and clearbody is now an identifier.
A few other tactics made available to matita.
A few tactics (change, fold, replace) generalized to patterns.
The argument of clear and clearbody is now an identifier.
WARNING: the implementation of change, fold and replace has been commented
out to generalize them to patterns. To be committed soon.
Enrico Tassi [Mon, 27 Jun 2005 12:24:32 +0000 (12:24 +0000)]
support for _ in binders, and a more coplex pattern that should help if
patterns will be used on subterms.
match pattern, term with
| Binder Anonymous, Binder name -> recursion
| Binder name1, Binder name2 when name1 = name2 -> recursion
| Binder name1, Binder name2 -> []
* auto_tac removed (it can be found in CVS)
* auto_tac_new renamed to auto_tac
* TacticAst.Auto ported to auto_tac[_new] (i.e. width added)
* MetadataQuery.hint removed (only {new_,}experimental_hint were used)
Enrico Tassi [Mon, 27 Jun 2005 10:42:27 +0000 (10:42 +0000)]
1) moved select and pattern_of from cicUtil to proofEngineHelpers
2) select now returns a couple (context, term) so that we can build the right context from each returned term
New implementation of experimental_hint/auto (called new_experimental_hint) that
dramatically cuts down the total time in certain cases. The idea of
new_experimental_hint is to take in input the universe (the list of uris that
occur in the signature) and to prune the results using the universe in place
of the signature. Thus in place of doing a lot of sigmatches a sigmatch is
done just once at the very beginning.
NOTE: to reduce the size of the universe the empty set of constraints is
not considered.
projects / helm.git / log