]> matita.cs.unibo.it Git - helm.git/log
helm.git
13 years agosubst.ma: some additions
Ferruccio Guidi [Wed, 1 Jun 2011 11:55:11 +0000 (11:55 +0000)]
subst.ma: some additions
convertibility.ma: non "conv" refers to the correct predicate
CC2FO_K.ma: CC to Fomega: first interpretation: substitution lemma

13 years agoPrint backtrace of exceptions when OCAMLRUNPARAM=b is setted.
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 11:34:24 +0000 (11:34 +0000)]
Print backtrace of exceptions when OCAMLRUNPARAM=b is setted.

13 years agoassert false removed
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 11:27:34 +0000 (11:27 +0000)]
assert false removed

13 years agoPartial implementation of "go to cursor" action.
Wilmer Ricciotti [Tue, 31 May 2011 13:59:37 +0000 (13:59 +0000)]
Partial implementation of "go to cursor" action.

13 years agoauto does not work here :(
Ferruccio Guidi [Mon, 30 May 2011 19:18:51 +0000 (19:18 +0000)]
auto does not work here :(

13 years agobasics: some additions
Ferruccio Guidi [Mon, 30 May 2011 18:34:47 +0000 (18:34 +0000)]
basics: some additions
lambda: some additions + split of lift and subst

13 years agoBetter indentation.
Claudio Sacerdoti Coen [Mon, 30 May 2011 16:28:27 +0000 (16:28 +0000)]
Better indentation.

13 years agoPartially working table layout of matita web (only on some browsers).
Wilmer Ricciotti [Mon, 30 May 2011 12:25:24 +0000 (12:25 +0000)]
Partially working table layout of matita web (only on some browsers).

13 years agoDebugging code to understand cases where the output notation is not
Claudio Sacerdoti Coen [Mon, 30 May 2011 11:02:26 +0000 (11:02 +0000)]
Debugging code to understand cases where the output notation is not
applied, is applied badly or it raises an assert failure.

Usually the problem is given by optional parts of the term. For instance,
in output all typing information is present and it _must_ be matched.

13 years agoName generator for Russell greatly improved.
Claudio Sacerdoti Coen [Fri, 27 May 2011 14:58:10 +0000 (14:58 +0000)]
Name generator for Russell greatly improved.
But maybe we need a longer term solution.

13 years agoImproved rendering of sequents in matitaweb, including handling of multiple
Wilmer Ricciotti [Thu, 26 May 2011 14:14:13 +0000 (14:14 +0000)]
Improved rendering of sequents in matitaweb, including handling of multiple
goals.

13 years agoSerious bug fixed:
Claudio Sacerdoti Coen [Thu, 26 May 2011 12:06:11 +0000 (12:06 +0000)]
Serious bug fixed:
 - in order to look for coercions to sort and funclass, we passed
   types containing implicits and a flag to avoid unification
 - totally avoiding unification, it happened
    1) that we diverged:
       t : A :> B ==> inject t : Sigma x.A :> B ==> eject (inject t): A :> B
    2) that we called unification on types that contained implicits
       (in some cases)

13 years agoProd indexed as Dead, that is equal only to itself, instead of Variable that
Enrico Tassi [Thu, 26 May 2011 11:57:17 +0000 (11:57 +0000)]
Prod indexed as Dead, that is equal only to itself, instead of Variable that
is equal to anything

13 years agoPreliminary version of matitaweb handling multiple goals in the sequent view.
Wilmer Ricciotti [Thu, 26 May 2011 11:48:48 +0000 (11:48 +0000)]
Preliminary version of matitaweb handling multiple goals in the sequent view.

13 years agoSyntax for coercion nocomposites fixed.
Claudio Sacerdoti Coen [Thu, 26 May 2011 09:33:31 +0000 (09:33 +0000)]
Syntax for coercion nocomposites fixed.

13 years agoAdded "nocomposites" to coercions.
Claudio Sacerdoti Coen [Thu, 26 May 2011 09:27:38 +0000 (09:27 +0000)]
Added "nocomposites" to coercions.

13 years ago- degree: some improvements and the Deg_append lemma
Ferruccio Guidi [Wed, 25 May 2011 12:22:16 +0000 (12:22 +0000)]
- degree: some improvements and the Deg_append lemma
- lambda_notation: the K interpretation (CC to Fomega mapping)

13 years agoQuick patch to avoid name collisions when passing coercions under let...ins.
Claudio Sacerdoti Coen [Tue, 24 May 2011 22:01:19 +0000 (22:01 +0000)]
Quick patch to avoid name collisions when passing coercions under let...ins.

13 years agoCoercions are now propagated under let...ins.
Claudio Sacerdoti Coen [Tue, 24 May 2011 21:39:32 +0000 (21:39 +0000)]
Coercions are now propagated under let...ins.

13 years agoFixed box pretty printing.
Wilmer Ricciotti [Tue, 24 May 2011 16:40:35 +0000 (16:40 +0000)]
Fixed box pretty printing.

13 years agomatitaweb: added retract (undo)
Wilmer Ricciotti [Tue, 24 May 2011 13:24:53 +0000 (13:24 +0000)]
matitaweb: added retract (undo)

13 years agodegree.ma: we defined the "degree" of a term, which is meaningful in
Ferruccio Guidi [Tue, 24 May 2011 12:19:11 +0000 (12:19 +0000)]
degree.ma: we defined the "degree" of a term, which is meaningful in
the lambda-cube

13 years ago1) interpretation of matches in patterns implemented
Claudio Sacerdoti Coen [Mon, 23 May 2011 23:08:04 +0000 (23:08 +0000)]
1) interpretation of matches in patterns implemented
2) missing exception added to matitaExcPp

13 years agoAdded support for hyperlinks in the goal view of the web interface.
Wilmer Ricciotti [Mon, 23 May 2011 15:13:38 +0000 (15:13 +0000)]
Added support for hyperlinks in the goal view of the web interface.

13 years ago...
Wilmer Ricciotti [Mon, 23 May 2011 10:49:02 +0000 (10:49 +0000)]
...

13 years agoRemoved dead code
Andrea Asperti [Mon, 23 May 2011 10:24:12 +0000 (10:24 +0000)]
Removed dead code

13 years ago- we weakened SAT3
Ferruccio Guidi [Fri, 20 May 2011 14:35:59 +0000 (14:35 +0000)]
- we weakened SAT3
- we simplified the specifications of the Cube

13 years agowant_indent bug fixed
Andrea Asperti [Fri, 20 May 2011 10:34:09 +0000 (10:34 +0000)]
want_indent bug fixed

13 years agoreadded function box_of
Andrea Asperti [Fri, 20 May 2011 10:06:00 +0000 (10:06 +0000)]
readded function box_of

13 years agoCompilation fix
Wilmer Ricciotti [Fri, 20 May 2011 09:59:53 +0000 (09:59 +0000)]
Compilation fix

13 years agoCompilation fix
Wilmer Ricciotti [Fri, 20 May 2011 09:59:31 +0000 (09:59 +0000)]
Compilation fix

13 years agoSimplified rendering.
Andrea Asperti [Fri, 20 May 2011 08:50:16 +0000 (08:50 +0000)]
Simplified rendering.

13 years agoSimplified rendering
Andrea Asperti [Fri, 20 May 2011 08:49:10 +0000 (08:49 +0000)]
Simplified rendering

13 years agoSimplified rendering
Andrea Asperti [Fri, 20 May 2011 08:48:27 +0000 (08:48 +0000)]
Simplified rendering

13 years agorm rendering attrs
Andrea Asperti [Fri, 20 May 2011 08:45:36 +0000 (08:45 +0000)]
rm rendering attrs

13 years agoRemoved mathml and proof rendering.
Andrea Asperti [Fri, 20 May 2011 08:44:09 +0000 (08:44 +0000)]
Removed mathml and proof rendering.

13 years agoSimplified rendering
Andrea Asperti [Fri, 20 May 2011 08:42:04 +0000 (08:42 +0000)]
Simplified rendering

13 years agoPorting to new reduction.
Andrea Asperti [Fri, 20 May 2011 08:34:57 +0000 (08:34 +0000)]
Porting to new reduction.

13 years agoAdded matitadaemon.
Wilmer Ricciotti [Thu, 19 May 2011 14:14:06 +0000 (14:14 +0000)]
Added matitadaemon.

13 years agocube.ma: some pts specifications of the lambda-cube
Ferruccio Guidi [Thu, 19 May 2011 14:12:22 +0000 (14:12 +0000)]
cube.ma: some pts specifications of the lambda-cube

13 years agoPorting to the new pts.
Andrea Asperti [Thu, 19 May 2011 10:36:25 +0000 (10:36 +0000)]
Porting to the new pts.

13 years agoPorting to new parametric TJ.
Andrea Asperti [Thu, 19 May 2011 10:16:44 +0000 (10:16 +0000)]
Porting to new parametric TJ.

13 years agoDummies are blocked.
Andrea Asperti [Thu, 19 May 2011 09:58:04 +0000 (09:58 +0000)]
Dummies are blocked.

13 years agoNew version of TJ parametric in the specification of pts.
Andrea Asperti [Wed, 18 May 2011 09:46:17 +0000 (09:46 +0000)]
New version of TJ parametric in the specification of pts.

13 years agowe added a property
Ferruccio Guidi [Sat, 14 May 2011 18:59:20 +0000 (18:59 +0000)]
we added a property

13 years agoground: some arithmetical properties added
Ferruccio Guidi [Fri, 13 May 2011 21:19:34 +0000 (21:19 +0000)]
ground: some arithmetical properties added
lift: some properties proved

13 years agointerim version (added smallLexer)
Wilmer Ricciotti [Fri, 13 May 2011 08:55:12 +0000 (08:55 +0000)]
interim version (added smallLexer)

13 years agoRecord projections:
Wilmer Ricciotti [Thu, 12 May 2011 16:03:08 +0000 (16:03 +0000)]
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).

13 years agoRecord projections:
Wilmer Ricciotti [Thu, 12 May 2011 15:59:10 +0000 (15:59 +0000)]
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).

13 years agoPartial modifications.
Andrea Asperti [Wed, 11 May 2011 13:26:18 +0000 (13:26 +0000)]
Partial modifications.

13 years agowe uncommented R3 and R4 tu be used in lambda-delta
Ferruccio Guidi [Thu, 28 Apr 2011 15:24:48 +0000 (15:24 +0000)]
we uncommented R3 and R4 tu be used in lambda-delta

13 years ago- weight: bugfix + weight-based eliminator axiomatized
Ferruccio Guidi [Thu, 28 Apr 2011 15:23:38 +0000 (15:23 +0000)]
- weight: bugfix + weight-based eliminator axiomatized
- notation: bugfix
- lift: first main property axiomatized

13 years ago- we added notation for the zetable and thetable items
Ferruccio Guidi [Thu, 21 Apr 2011 14:16:26 +0000 (14:16 +0000)]
- we added notation for the zetable and thetable items
- the first inversion lemma for lift shows a bug in the destruct tactic :(

13 years agoconvertibility.
Andrea Asperti [Wed, 20 Apr 2011 08:50:32 +0000 (08:50 +0000)]
convertibility.

13 years agogeneratin lemmas and subject reduction (with a lot of axioms).
Andrea Asperti [Wed, 20 Apr 2011 08:49:15 +0000 (08:49 +0000)]
generatin lemmas and subject reduction (with a lot of axioms).

13 years agoprogress
Andrea Asperti [Wed, 20 Apr 2011 08:48:02 +0000 (08:48 +0000)]
progress

13 years agoerror in the conversion rule
Andrea Asperti [Wed, 20 Apr 2011 08:38:18 +0000 (08:38 +0000)]
error in the conversion rule

13 years agonotation bug fix
Ferruccio Guidi [Tue, 19 Apr 2011 21:28:46 +0000 (21:28 +0000)]
notation bug fix

13 years ago- some bug fixes
Ferruccio Guidi [Tue, 19 Apr 2011 20:59:15 +0000 (20:59 +0000)]
- some bug fixes
- we defined the thinning relation

13 years agocomplete reformalization of lambda-delta in matita (initial commit)
Ferruccio Guidi [Tue, 19 Apr 2011 15:15:23 +0000 (15:15 +0000)]
complete reformalization of lambda-delta in matita (initial commit)
first definitions and one lemma

13 years agodisambiguation of explicit interprettions with arguments now works
Ferruccio Guidi [Tue, 19 Apr 2011 08:06:07 +0000 (08:06 +0000)]
disambiguation of explicit interprettions with arguments now works
i.e. 'eq x y z

13 years ago...
Claudio Sacerdoti Coen [Wed, 13 Apr 2011 11:15:01 +0000 (11:15 +0000)]
...

13 years agowe added an nmap from NCic.obj to NotationPt.obj (to be continued)
Ferruccio Guidi [Tue, 5 Apr 2011 20:30:48 +0000 (20:30 +0000)]
we added an nmap from NCic.obj to NotationPt.obj (to be continued)

13 years agowe removed an extra dot from the "include" syntax
Ferruccio Guidi [Tue, 5 Apr 2011 15:59:50 +0000 (15:59 +0000)]
we removed an extra dot from the "include" syntax

13 years agowe introduced nterm for NotationPt.term
Ferruccio Guidi [Mon, 4 Apr 2011 16:55:04 +0000 (16:55 +0000)]
we introduced nterm for NotationPt.term

13 years agoPatch to avoid equations of the form ? -> T (oriented this way) that
Claudio Sacerdoti Coen [Fri, 1 Apr 2011 12:43:29 +0000 (12:43 +0000)]
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 ?).

13 years agowe proved that the union of two saturated sets is saturated
Ferruccio Guidi [Wed, 30 Mar 2011 17:33:14 +0000 (17:33 +0000)]
we proved that the union of two saturated sets is saturated

13 years agoKeeping track of locations of disambiguated ids and symbols.
Wilmer Ricciotti [Wed, 30 Mar 2011 11:52:27 +0000 (11:52 +0000)]
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.

13 years agoFixes previous wrong commit.
Claudio Sacerdoti Coen [Sun, 27 Mar 2011 13:18:36 +0000 (13:18 +0000)]
Fixes previous wrong commit.

13 years ago1) Second half of the bug fixing for the "lexical keywords lost" bug.
Claudio Sacerdoti Coen [Sun, 27 Mar 2011 13:09:20 +0000 (13:09 +0000)]
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.

13 years agoBug fixed: some Uri was not refreshed. The effect of the bug was that some
Claudio Sacerdoti Coen [Sun, 27 Mar 2011 13:08:22 +0000 (13:08 +0000)]
Bug fixed: some Uri was not refreshed. The effect of the bug was that some
file was re-compiled even if already compiled.

13 years agoDebugging code commented out.
Claudio Sacerdoti Coen [Sun, 27 Mar 2011 13:07:45 +0000 (13:07 +0000)]
Debugging code commented out.

13 years ago- terms.ma: we included 'is_dummy" and "neutral" (maybe "is_neutral
Ferruccio Guidi [Wed, 23 Mar 2011 21:31:24 +0000 (21:31 +0000)]
- 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

13 years agoMore verbose in case of errors.
Claudio Sacerdoti Coen [Wed, 23 Mar 2011 15:54:49 +0000 (15:54 +0000)]
More verbose in case of errors.

13 years agored star
Andrea Asperti [Wed, 23 Mar 2011 07:36:29 +0000 (07:36 +0000)]
red star

13 years agoUse jmeq from lib.
Claudio Sacerdoti Coen [Wed, 23 Mar 2011 01:28:29 +0000 (01:28 +0000)]
Use jmeq from lib.

13 years agoNested calls to matitac are now pretty-printed nicely.
Claudio Sacerdoti Coen [Wed, 23 Mar 2011 01:08:02 +0000 (01:08 +0000)]
Nested calls to matitac are now pretty-printed nicely.
The times printed, however, still include the nested compilation time
(to be fixed).

13 years agoReindentation.
Claudio Sacerdoti Coen [Tue, 22 Mar 2011 21:58:08 +0000 (21:58 +0000)]
Reindentation.

13 years agothe weakening lemma is not needed since it is assumed in the rules of
Ferruccio Guidi [Tue, 22 Mar 2011 21:00:04 +0000 (21:00 +0000)]
the weakening lemma is not needed since it is assumed in the rules of
the type judgement :)

13 years agothe thinning lemma follows immediately from the substitution lemma ...
Ferruccio Guidi [Tue, 22 Mar 2011 20:34:05 +0000 (20:34 +0000)]
the thinning lemma follows immediately from the substitution lemma ...

13 years ago- lambda_notation.ma: more notation and bug fixes
Ferruccio Guidi [Tue, 22 Mar 2011 18:53:26 +0000 (18:53 +0000)]
- 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

13 years agoBug fixed and code refactoring: now both matitac and matita include files
Claudio Sacerdoti Coen [Tue, 22 Mar 2011 17:22:53 +0000 (17:22 +0000)]
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).

13 years agoUse matita/lib as the new standard library in place of matita/nlibrary.
Claudio Sacerdoti Coen [Tue, 22 Mar 2011 16:41:24 +0000 (16:41 +0000)]
Use matita/lib as the new standard library in place of matita/nlibrary.

13 years agoDebugging code removed.
Claudio Sacerdoti Coen [Tue, 22 Mar 2011 16:39:35 +0000 (16:39 +0000)]
Debugging code removed.

13 years agosn_prod
Andrea Asperti [Mon, 21 Mar 2011 08:18:22 +0000 (08:18 +0000)]
sn_prod

13 years agosn_lambda
Andrea Asperti [Mon, 21 Mar 2011 07:41:43 +0000 (07:41 +0000)]
sn_lambda

13 years agoextensions
Andrea Asperti [Mon, 21 Mar 2011 07:40:56 +0000 (07:40 +0000)]
extensions

13 years agoBug "fixed" (i.e avoided).
Claudio Sacerdoti Coen [Sat, 19 Mar 2011 00:00:31 +0000 (00:00 +0000)]
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?

13 years agoPorted to
Claudio Sacerdoti Coen [Fri, 18 Mar 2011 16:03:55 +0000 (16:03 +0000)]
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.

13 years ago- more notation and service lemmas
Ferruccio Guidi [Tue, 15 Mar 2011 19:18:39 +0000 (19:18 +0000)]
- more notation and service lemmas
- arity.ma: arities and arity types
- arity_eval.ma: arities and arity types assigned to terms

13 years ago- some ignores
Ferruccio Guidi [Tue, 15 Mar 2011 12:03:55 +0000 (12:03 +0000)]
- some ignores
- new service lemmas

13 years agodependences fix
Ferruccio Guidi [Mon, 14 Mar 2011 21:19:49 +0000 (21:19 +0000)]
dependences fix

13 years agoadded star.ma (star closure of a relation)
Andrea Asperti [Fri, 11 Mar 2011 07:17:06 +0000 (07:17 +0000)]
added star.ma (star closure of a relation)

13 years agoImprovements.
Andrea Asperti [Fri, 11 Mar 2011 07:15:20 +0000 (07:15 +0000)]
Improvements.

13 years agodiamond property
Andrea Asperti [Thu, 10 Mar 2011 07:41:22 +0000 (07:41 +0000)]
diamond property

13 years agomore notation and all-purpose lemmas
Ferruccio Guidi [Wed, 9 Mar 2011 21:06:55 +0000 (21:06 +0000)]
more notation and all-purpose lemmas

13 years agothe interpretation for Sigma was missing
Ferruccio Guidi [Wed, 9 Mar 2011 11:59:38 +0000 (11:59 +0000)]
the interpretation for Sigma was missing

13 years agoFirst commit with new (incomplete) disambiguation engine.
Wilmer Ricciotti [Tue, 8 Mar 2011 13:26:37 +0000 (13:26 +0000)]
First commit with new (incomplete) disambiguation engine.

13 years agosottotermini e confluenza (manca pr_substs).
Andrea Asperti [Mon, 7 Mar 2011 07:29:04 +0000 (07:29 +0000)]
sottotermini e confluenza (manca pr_substs).

13 years agowe started the implementation of higher order saturated sets
Ferruccio Guidi [Wed, 2 Mar 2011 21:02:38 +0000 (21:02 +0000)]
we started the implementation of higher order saturated sets