Porting to new parametric TJ.

Dummies are blocked.

New version of TJ parametric in the specification of pts.

we added a property

ground: some arithmetical properties added
lift: some properties proved

interim version (added smallLexer)

Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).

Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).

Partial modifications.

we uncommented R3 and R4 tu be used in lambda-delta

- weight: bugfix + weight-based eliminator axiomatized
- notation: bugfix
- lift: first main property axiomatized

- we added notation for the zetable and thetable items
- the first inversion lemma for lift shows a bug in the destruct tactic :(

convertibility.

generatin lemmas and subject reduction (with a lot of axioms).

progress

error in the conversion rule

notation bug fix

- some bug fixes
- we defined the thinning relation

complete reformalization of lambda-delta in matita (initial commit)
first definitions and one lemma

disambiguation of explicit interprettions with arguments now works
i.e. 'eq x y z

...

we added an nmap from NCic.obj to NotationPt.obj (to be continued)

we removed an extra dot from the "include" syntax

we introduced nterm for NotationPt.term

Patch to avoid equations of the form ? -> T (oriented this way) that
can always be applied to later yield non well typed terms.

Moreover, when T is a Leaf and when the goal contains a Leaf, the equation
above is applied breaking one of the "assert (subst=[])" in the code
(since the Leaf is matched by ?).

we proved that the union of two saturated sets is saturated

Keeping track of locations of disambiguated ids and symbols.
Matitac produces disambiguated files, with hyperlinks for ids and § marks
for symbols.
Matita is able to reparse ids with hypelinks.

Fixes previous wrong commit.

1) Second half of the bug fixing for the "lexical keywords lost" bug.
   I expected the need for re-building the lexer also after the Notation command
   and indeed I have found an example for this in CerCo.
2) Printing of compilation result and times required fixed.

Bug fixed: some Uri was not refreshed. The effect of the bug was that some
file was re-compiled even if already compiled.

Debugging code commented out.

- terms.ma: we included 'is_dummy" and "neutral" (maybe "is_neutral
would be better)
- sn.ma rc_sat.ma: we introduced the axioms for dummy

More verbose in case of errors.

red star

Use jmeq from lib.

Nested calls to matitac are now pretty-printed nicely.
The times printed, however, still include the nested compilation time
(to be fixed).

Reindentation.

the weakening lemma is not needed since it is assumed in the rules of
the type judgement :)

the thinning lemma follows immediately from the substitution lemma ...

- lambda_notation.ma: more notation and bug fixes
- terms.ma: contains the data structure of terms and related functions (not involving substitution).
- ext_lambda.ma: cut off of previous ext.ma, containing the lambda-related objects
- subst.ma, types.ma: we removed notation from here
- types.ma: we added special cases of the weakening and thinning lemmas as axioms

Bug fixed and code refactoring: now both matitac and matita include files
correctly by re-generating ~include_paths in the same way and every time a
file is opened (either by matitaScript or by assert_ng itself).

Use matita/lib as the new standard library in place of matita/nlibrary.

Debugging code removed.

sn_prod

sn_lambda

extensions

Bug "fixed" (i.e avoided).

Bug description:
 - matitac (more precisely, MatitaEngine.assert_ng, hence the "include"
   command) parses files differently from Matita. In particular, it works on
   a camlp5 "Grammar.parsable" lexer, which is a lexer that remembers
   look-ahead tokens.
 - an "include" file can change the list of keywords for the lexer
   (e.g. when defining the "if-then-else" notation). Hence, after an include,
   the lexer to be used must change and thus the corresponding
   "Grammar.parsable" should change too. This was not the case since the
   "Grammar.parsable" was not regenerated to avoid loosing the look-ahead
   tokens

Bug avoidance:
 - we assume that the "include" command is properly terminated. Hence no
   look-ahead is performed. After each "include" command we regenerate
   the lexer to avoid the bug.

Note:
 - why don't we need to do this just after a "notation" command?
   Apparently, this is not required. However, I do not understand why.
   Is this to be better understood in the future?

Ported to

- camlp5 version 6.02.2 + patches
- ocaml version 3.11.2-4

If you are still using the old version of OCaml + Camlp5, do not update
these two files.

- more notation and service lemmas
- arity.ma: arities and arity types
- arity_eval.ma: arities and arity types assigned to terms

- some ignores
- new service lemmas

dependences fix

added star.ma (star closure of a relation)

Improvements.

diamond property

more notation and all-purpose lemmas

the interpretation for Sigma was missing

First commit with new (incomplete) disambiguation engine.

sottotermini e confluenza (manca pr_substs).

we started the implementation of higher order saturated sets

- rc_sat.ma: we changed the notation for extensional equality. we now
use \cong like in geometry
- rc_eval.ma (second part of former rc_ma): we completed the evaluation
by adding a stack, and we proved weakening and thinning for it

- notation is now in a separate file
- sn.ma: we updated the axiomatization of SN while correcting the saturation
conditions
- rc_sat.ma: we proved that depRC is a candidate

- new file ext.ma with the objects needed for the normalization so
far, that should be removed or should go into other files
- sn.ma: we parametrized the saturation conditions
- rc_sat.ma (first part of former rc.ma): we introduced extensional
equality on candidates

we started to set up the strong normalization proof.
we plan to use saturated subsets of strongly normalizing terms
(see for instance D. Cescutti 2001, but a better citation is required)
rather than reducibility candidates.
The benefit is that reduction is not needed to define such subsets.
Also, this approach was never tried on a system with dependent types.

fork for Matita version B

we added some comments

Added typing rule for dummies

Added lambda

enabling destruct defs

Hyperlinks are back.

Hyperlinks are now computed correctly. I least I hope...

Removed inclusion of logic/equality.ma in datatypes/list.ma (not needed and
source of conflicts in other scripts).

Bugfix for elimination principles.

Bug fix for generation of elimination principles.

Added some typing info to elimination principles, allowing the refiner
to succeed in more cases, also speeding up the generation process (no
more slow record definitions).

Added some typing info to elimination principles, allowing the refiner
to succeed in more cases, also speeding up the generation process (no
more slow record definitions).

The sequent window now always scroll to the bottom when its content changes.

Bug fixed: the script windows did not scroll correctly because I used the
wrong method.

ctrl+pgUp/Down to navigate tabs

ctrl+pgUp/Down to navigate tabs

...

Bug fixed: the newScript method must be called only after registering the
gui. I have moved the invocation of self#newScript from the initializer to the
instance() function to solve the issue (an ugly gtk error when Matita starts).

Bug fixed: the accelerators for Close and Quit were both Ctrl+q (???)

Last commit reverted (it was an error).

Part of last HUGE COMMIT about NCic.status

Stupid bug fixed (introduced a couple of commits ago): the close button for
tabs always closed the first tab instead of the right one.

HUGE COMMIT:

1) sequent2pres merged into content2pres
2) more functions to render sequents/context/substs to content and then to
   presentation
3) new virtual class NCic.status with methods implementing pretty-printing
   functions (same interface that used to be given in NCicPp); objects of this
   class are now used REALLY ALL OVER the matita code (well, almost...)
4) NCicPp implements a concrete version of NCic.status
   (low level pretty-printer)
5) ApplyTransformation implements a concrete version of NCic.status
   (high level pretty-printer that uses notation). It also exports the boolean
   reference to deactivate the high level pretty printer in favour of the
   low level one
6) some code simplifications here and there (in particular for tactics)
7) return type of BoxPp changed to yield informations about hyperlinks;
   the information is not used yet by the interface and it is not computed
   yet (not that easy to do...)
8) other minor stuff here and there

coercion lookup now returns coercions ranked using the number of symbols matched, the more precise match first

code simplification

...

added retrieval function with weight

non uniform coercion names in sync with the TYPES talk, stil commented out...

...

...

...

Brainstorming

ops, we forgot to update the version indicator :)

- ld-html-root: ported to permanent lambda-delta url
- ld.dtd: we can specify a language encoding for the metalinguistic
annotation, moreover we export the metalinguistic classification
- the other files are modified in order to support this feature

Bugs and other stuff to do to complete the Matita 1/2 => Matita 1.0 transition.

Interface reduction; code clean up.

code simplification