Andrea Asperti [Wed, 21 Sep 2011 15:51:06 +0000 (15:51 +0000)]
Map in NCicUtils now takes an optional boolea to disable head beta reduction.
We normalize cic terms in the paramodulation blob by stripping out names in
binders.
1) removed many debug prints
2) solved a bug in automation (we had forgotten to saturate clauses in
forward_infer_step, a mistake that prevented equations from being
indexed, resulting in almost certain failure of automation).
3) disabled alpha_eq in NCicBlob.compare, because it now requires a
status containing the correct environment, which can't be guessed
inside compare (enabling alpha_eq results in the automation
sporadically failing).
Andrea Asperti [Tue, 20 Sep 2011 14:00:34 +0000 (14:00 +0000)]
The Blob is not abstracted on the context any more.
The saturate function (that requires the environment now
contained in the status) is now external to the module.
It is defined in NCicBlob.
The functions mk_passive and mk_goals are now expecting
input terms already saturated.
This commit patches the environment and the library so that their status is
contained in the global status of Matita. This allows several users to execute
concurrently in the same instance of Matita, since they are now using
independent statuses.
First attempt at svn commit of developments.
Fixes a problem with hyperlinks (the </A> tag was not consumed correctly
if it appeared at the end of a command/tactic).
- the theory of parallel substitution of local environments (ltps) is ready
- the theory of context-free parallel reduction of local environments (ltpr) is ready
- the proof of the substitution lemma for context-free parallel reduction is started ...
- some renaming and annotating
Ferruccio Guidi [Mon, 29 Aug 2011 15:21:40 +0000 (15:21 +0000)]
- we shared the atomic term constructions
- we fixed the notation of the binary term construction
- we inverted the dependences of cl_shift and cl_weight
Ferruccio Guidi [Sat, 27 Aug 2011 13:59:35 +0000 (13:59 +0000)]
- the shift function is now defined and cpr_shift_fwd is proved
- tentative definition of the structures for the wh normal forms
- definition of lists without the [...] notation
- some refactoring and annotating (we separate lemmas from facts)
Ferruccio Guidi [Mon, 22 Aug 2011 12:34:34 +0000 (12:34 +0000)]
we now use non-telescopic substitution in parallel reduction, rather
than the telescopic one. This choice weakens the step of
context-sensitive reduction a bit while maintaining the expected
properties
Ferruccio Guidi [Sun, 7 Aug 2011 20:44:42 +0000 (20:44 +0000)]
- cpr is now defined and the cpr_flat propery is proved! (it did not
hold in the first version of the calculus because cpr (aka pr2) was
badly designed).
- relocation properties of tpr closed!
- fixed bug in drop (base case was too restrictive)
- some refactoring
- nnAuto.ml: width overflows are warnings, not errors
- matitaScript.ml: backup source file with ~ reactivated
- lambda-delta: main properies of lift closed!
Bug fixed: when we try to add an object and it is not _directly_ well typed
(i.e. it is not well typed, and not because it depends on a non-well-typed
object in the library), we should not remember it, since the user can change
the definition and try again.
New function replace to be used in place of time_travel every time the user
switches to a new tab. In this way, every tab is independent and it only sees
the objects defined in that tab. This fixes the following bug: in tab A go
down; go down in tab B; go up in tab A (at this point also the objects declared
in B where removed); do something in B or go up in B (BOOM))
projects / helm.git / log