]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agomatitadep: we now handle the inline of an uri, we removed the -exclude option
Ferruccio Guidi [Tue, 22 Jul 2008 17:28:07 +0000 (17:28 +0000)]
matitadep: we now handle the inline of an uri, we removed the -exclude option
matitaInit: we removed the -drop option (now handled automatically)
transcript: we removed the baseuri generation
CoRN-Procedural: the mma files and the depends file are now available

16 years agotranscript: now we can generate procedural output
Ferruccio Guidi [Tue, 22 Jul 2008 12:43:10 +0000 (12:43 +0000)]
transcript: now we can generate procedural output
CoRN-Procedural: development started:
                 we aim at the procedural reconstruction of CoRN

16 years ago...
Enrico Tassi [Tue, 22 Jul 2008 11:52:25 +0000 (11:52 +0000)]
...

16 years ago...
Enrico Tassi [Tue, 22 Jul 2008 08:34:00 +0000 (08:34 +0000)]
...

16 years agoIn some universe, membership is a morphism.
Claudio Sacerdoti Coen [Tue, 22 Jul 2008 08:00:09 +0000 (08:00 +0000)]
In some universe, membership is a morphism.

16 years agoSambin's & Valentini's toolbox (???)
Claudio Sacerdoti Coen [Tue, 22 Jul 2008 07:01:46 +0000 (07:01 +0000)]
Sambin's & Valentini's toolbox (???)

16 years agoDependencies removed.
Claudio Sacerdoti Coen [Tue, 22 Jul 2008 07:01:06 +0000 (07:01 +0000)]
Dependencies removed.

16 years ago...
Enrico Tassi [Mon, 21 Jul 2008 19:26:28 +0000 (19:26 +0000)]
...

16 years agofrac is an infix operator!
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 19:05:42 +0000 (19:05 +0000)]
frac is an infix operator!

16 years agoError message improved.
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 19:05:27 +0000 (19:05 +0000)]
Error message improved.

16 years agoRendering of \infrule improved.
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 19:05:12 +0000 (19:05 +0000)]
Rendering of \infrule improved.

16 years agowe implemented the support for generating ma files from mma files
Ferruccio Guidi [Mon, 21 Jul 2008 18:10:30 +0000 (18:10 +0000)]
we implemented the support for generating ma files from mma files

16 years agoadded notes about notation
Enrico Tassi [Mon, 21 Jul 2008 13:38:38 +0000 (13:38 +0000)]
added notes about notation

16 years agoadd conf key matita.debug_menu
Enrico Tassi [Mon, 21 Jul 2008 11:47:15 +0000 (11:47 +0000)]
add conf key matita.debug_menu

16 years agoavoid empty hvbox
Enrico Tassi [Mon, 21 Jul 2008 11:34:35 +0000 (11:34 +0000)]
avoid empty hvbox

16 years ago...
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 10:55:23 +0000 (10:55 +0000)]
...

16 years agoSemantic analysis implemented (sort of).
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 10:11:49 +0000 (10:11 +0000)]
Semantic analysis implemented (sort of).

16 years ago...
Claudio Sacerdoti Coen [Fri, 18 Jul 2008 15:11:22 +0000 (15:11 +0000)]
...

16 years agoNew input notation for bottom-up tree construction finished.
Claudio Sacerdoti Coen [Fri, 18 Jul 2008 14:47:29 +0000 (14:47 +0000)]
New input notation for bottom-up tree construction finished.

16 years agoSnapshot.
Claudio Sacerdoti Coen [Fri, 18 Jul 2008 14:23:01 +0000 (14:23 +0000)]
Snapshot.

16 years agoInput notation.
Claudio Sacerdoti Coen [Fri, 18 Jul 2008 13:13:43 +0000 (13:13 +0000)]
Input notation.

16 years agobetter metavariable context
Enrico Tassi [Fri, 18 Jul 2008 12:55:24 +0000 (12:55 +0000)]
better metavariable context

16 years agometavariable context has a separator now
Enrico Tassi [Fri, 18 Jul 2008 12:51:05 +0000 (12:51 +0000)]
metavariable context has a separator now

16 years agoexception inside regex callback not re-raised if equal to sys.break
Enrico Tassi [Fri, 18 Jul 2008 08:30:09 +0000 (08:30 +0000)]
exception inside regex callback not re-raised if equal to sys.break

16 years agoBugs fixed:
Claudio Sacerdoti Coen [Thu, 17 Jul 2008 13:28:34 +0000 (13:28 +0000)]
Bugs fixed:
\frac is an infix operator
\infrule is a prefix operator

16 years ago1 => \\e
Claudio Sacerdoti Coen [Thu, 17 Jul 2008 13:27:14 +0000 (13:27 +0000)]
1 => \\e

16 years agoExecutables are now ignored.
Claudio Sacerdoti Coen [Thu, 17 Jul 2008 12:02:22 +0000 (12:02 +0000)]
Executables are now ignored.

16 years agoProcedural: some comments added in the generated script
Ferruccio Guidi [Wed, 16 Jul 2008 18:16:19 +0000 (18:16 +0000)]
Procedural: some comments added in the generated script
tests/fguidi.ma: we removed the dependence from legacy/coq.ma
ApplyTransformation: new function procedural_text_of_cic_term
                     for use in matitaScript (still disabled)

16 years agonotations for lists adds some breaking points
Enrico Tassi [Wed, 16 Jul 2008 16:16:30 +0000 (16:16 +0000)]
notations for lists adds some breaking points

16 years agoDuplicated doc removed.
Claudio Sacerdoti Coen [Wed, 16 Jul 2008 14:02:07 +0000 (14:02 +0000)]
Duplicated doc removed.

16 years agoSnapshot (not working).
Claudio Sacerdoti Coen [Wed, 16 Jul 2008 13:58:11 +0000 (13:58 +0000)]
Snapshot (not working).

16 years agoa) update with upstream version
Claudio Sacerdoti Coen [Wed, 16 Jul 2008 12:37:24 +0000 (12:37 +0000)]
a) update with upstream version
b) new: implemented semantic analyzer from untyped to typed AST for
   an imperative structured function-less C compiler
c) all URIs removed from .ma files

16 years agocic2acic: new function acic_term_of_cic_term
Ferruccio Guidi [Tue, 15 Jul 2008 17:54:23 +0000 (17:54 +0000)]
cic2acic: new function acic_term_of_cic_term
matita/Makefile: LAMBDA-TYPES tested only in opt mode

16 years agomore notation moved to core notation, unification of duplicated CProp connectives
Enrico Tassi [Tue, 15 Jul 2008 17:01:14 +0000 (17:01 +0000)]
more notation moved to core notation, unification of duplicated CProp connectives

16 years agoSince CProp_i = Type_i everything lowered without 2 distinct Sigma.
Enrico Tassi [Tue, 15 Jul 2008 12:01:23 +0000 (12:01 +0000)]
Since CProp_i = Type_i everything lowered without 2 distinct Sigma.

16 years agoCProp_i <= Type_i , Type_i <= CProp_i
Enrico Tassi [Tue, 15 Jul 2008 12:00:24 +0000 (12:00 +0000)]
CProp_i <= Type_i , Type_i <= CProp_i

16 years agomodels over N fixed
Enrico Tassi [Tue, 15 Jul 2008 10:16:06 +0000 (10:16 +0000)]
models over N fixed

16 years agonew q_function representation
Enrico Tassi [Tue, 15 Jul 2008 09:18:23 +0000 (09:18 +0000)]
new q_function representation

16 years agoremoved dummy comment
Enrico Tassi [Tue, 15 Jul 2008 09:09:30 +0000 (09:09 +0000)]
removed dummy comment

16 years agoUsing Prop conjuction on Props lowers the universes.
Enrico Tassi [Tue, 15 Jul 2008 09:08:15 +0000 (09:08 +0000)]
Using Prop conjuction on Props lowers the universes.
SigT instead of ExT

16 years agolambda-delta: we added the support for position indexes in global references
Ferruccio Guidi [Mon, 14 Jul 2008 20:17:22 +0000 (20:17 +0000)]
lambda-delta: we added the support for position indexes in global references
              we added a pretty printer for the intermediate language
librarian   : utime stamps now appear only in debug mode

16 years agoProcedural: we added the support for rendering definitions and axioms
Ferruccio Guidi [Mon, 14 Jul 2008 11:57:42 +0000 (11:57 +0000)]
Procedural: we added the support for rendering definitions and axioms

16 years agoProcedural: we added the support for theorem flavours and we fixed the handling ...
Ferruccio Guidi [Sun, 13 Jul 2008 15:02:49 +0000 (15:02 +0000)]
Procedural: we added the support for theorem flavours and we fixed the handling             of unexpected proof constructions

16 years agocicUtil : we added a context to is_sober to check for consistancy
Ferruccio Guidi [Sun, 13 Jul 2008 11:06:20 +0000 (11:06 +0000)]
cicUtil            : we added a context to is_sober to check for consistancy
                     of RELS (not implemented yet)
doubleTypeInference: the inferred name of an anonymous lambda must be the name
                     of the expected prod :)
acic2Procedural    : we added a consistancy check that was missing

16 years agoProcedural: bug fix in the procedural rendering of the abstraction
Ferruccio Guidi [Sat, 12 Jul 2008 22:17:46 +0000 (22:17 +0000)]
Procedural: bug fix in the procedural rendering of the abstraction

16 years agolibrarian: retrieval of buildable files speeded up a lot
Ferruccio Guidi [Sat, 12 Jul 2008 20:40:30 +0000 (20:40 +0000)]
librarian: retrieval of buildable files speeded up a lot
Procedural: some bug fixes
termContentPres.ml: syntax of let-in construction fixed
LAMBDA-TYPES: some improvements in the Makefile

16 years agoNew feature/bug fixed (hopefully): it is now possible to use fixed (term)
Claudio Sacerdoti Coen [Sat, 12 Jul 2008 11:43:21 +0000 (11:43 +0000)]
New feature/bug fixed (hopefully): it is now possible to use fixed (term)
variables in fold bodies.
The notation for exists is now fully working as expected.

16 years agoNotation for existential partially fixed: it is now possible to write
Claudio Sacerdoti Coen [Sat, 12 Jul 2008 11:17:17 +0000 (11:17 +0000)]
Notation for existential partially fixed: it is now possible to write
\exists a,b,c:T.P
(possibly omitting the type).
In any case, however, the type is got rid of during parsing.

16 years agoA very nice experiment using notation: we define the notation for natural
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 17:22:19 +0000 (17:22 +0000)]
A very nice experiment using notation: we define the notation for natural
language derivations so that, when looking at the proof, we see it as a
natural deduction tree! Useful to teach logic to first year students, but
much work still need to be done (expecially to give derivation trees to
the system in some way).

16 years agoExists is no longer an ad-hoc notation hard-coded in the parser.
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 16:49:18 +0000 (16:49 +0000)]
Exists is no longer an ad-hoc notation hard-coded in the parser.
It was so becauses it was previously impossible to declare a notation that
changed the level of its subterms.

16 years agoAdded new ternary layout \infrule premises conclusion name.
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 14:29:09 +0000 (14:29 +0000)]
Added new ternary layout \infrule premises conclusion name.
Very useful to render proof terms as trees.

16 years agovalue has a specification
Enrico Tassi [Thu, 10 Jul 2008 10:16:48 +0000 (10:16 +0000)]
value has a specification

16 years agoupdated changelog
Enrico Tassi [Thu, 10 Jul 2008 08:13:16 +0000 (08:13 +0000)]
updated changelog

16 years agomore work on dama
Enrico Tassi [Thu, 10 Jul 2008 08:00:45 +0000 (08:00 +0000)]
more work on dama

16 years agofixed regression in casting an argument to funclass, this incidentally leaded to...
Enrico Tassi [Thu, 10 Jul 2008 08:00:30 +0000 (08:00 +0000)]
fixed regression in casting an argument to funclass, this incidentally leaded to a single look_for_coercion_function

16 years agosome bug fixes
Ferruccio Guidi [Wed, 9 Jul 2008 18:24:46 +0000 (18:24 +0000)]
some bug fixes

16 years agobetter notation
Enrico Tassi [Wed, 9 Jul 2008 14:16:17 +0000 (14:16 +0000)]
better notation

16 years agominor fixes
Enrico Tassi [Wed, 9 Jul 2008 13:40:43 +0000 (13:40 +0000)]
minor fixes

16 years agoCProp hierarchy fixed:
Enrico Tassi [Wed, 9 Jul 2008 11:19:02 +0000 (11:19 +0000)]
CProp hierarchy fixed:
- CProp universes are not swept away
- CProp i : Type j (where i < j, used to be a fresh j)
- new kernel universe inconsistency error message improved
- pp function for universes constraints for new kernel

Formal topology example fixed to eploit left parameters to reduce the universe
height and solve universe inconsistency

16 years agotab -> ' '
Enrico Tassi [Wed, 9 Jul 2008 11:07:16 +0000 (11:07 +0000)]
tab -> '        '

16 years ago...
Enrico Tassi [Wed, 9 Jul 2008 10:55:55 +0000 (10:55 +0000)]
...

16 years agosimplified coercDb implementation with additional info about the position of
Enrico Tassi [Mon, 7 Jul 2008 21:01:17 +0000 (21:01 +0000)]
simplified coercDb implementation with additional info about the position of
the coerced argument. Now (C ??? x ??? y z) is printed as (x y z) when C is a
coercion and ? are implicits or saturations generated to apply the coercion to
x.

New case in unification, when there is a triangular pullback and the
coerced is not flexible an unfolding of the composed coercion is attempted.
this helps in the case:

  C ??? X ??? y ? +?+ C1 ??? (C2 ??? X ???) ??? y z

where C = C1 composed C2 but X is rigid abd conversion fails cause
x != ? and the heads are different... unfolding C helps

16 years ago- we replaced a normalize with a whd in the classification algorithm
Ferruccio Guidi [Fri, 4 Jul 2008 18:46:29 +0000 (18:46 +0000)]
- we replaced a normalize with a whd in the classification algorithm
- we turned on the display of the inner types to debug drop/props.ma

16 years agoMore definitions, following Ciraulo's Phd Thesis "Constructive Satisfiability".
Claudio Sacerdoti Coen [Fri, 4 Jul 2008 15:31:22 +0000 (15:31 +0000)]
More definitions, following Ciraulo's Phd Thesis "Constructive Satisfiability".

16 years ago- Procedural: bug fix in rendering the application: we must handle the
Ferruccio Guidi [Fri, 4 Jul 2008 12:03:19 +0000 (12:03 +0000)]
- Procedural: bug fix in rendering the application: we must handle the
              arguments that are inferrable but do not occur in the goal
- LAMBDA-TYPES: bug fix in Makefile: MAS was not computed correctly

16 years agoCompatibility finished.
Claudio Sacerdoti Coen [Fri, 4 Jul 2008 11:57:33 +0000 (11:57 +0000)]
Compatibility finished.

16 years agoNice: cotransitivity proved.
Claudio Sacerdoti Coen [Fri, 4 Jul 2008 10:21:26 +0000 (10:21 +0000)]
Nice: cotransitivity proved.

16 years agoMore work.
Claudio Sacerdoti Coen [Thu, 3 Jul 2008 21:54:34 +0000 (21:54 +0000)]
More work.

16 years agoFirst few lemmas. But I have some problems in making Matita accept
Claudio Sacerdoti Coen [Thu, 3 Jul 2008 21:31:55 +0000 (21:31 +0000)]
First few lemmas. But I have some problems in making Matita accept
my constructor.

16 years agoFirst experiment in Padua about formal topologies.
Claudio Sacerdoti Coen [Thu, 3 Jul 2008 15:22:12 +0000 (15:22 +0000)]
First experiment in Padua about formal topologies.

16 years ago...snapshot
Enrico Tassi [Thu, 3 Jul 2008 14:20:35 +0000 (14:20 +0000)]
...snapshot

16 years ago...
Enrico Tassi [Thu, 3 Jul 2008 08:00:54 +0000 (08:00 +0000)]
...

16 years agosome work
Enrico Tassi [Wed, 2 Jul 2008 21:43:55 +0000 (21:43 +0000)]
some work

16 years agosvn:ignore set on LambdaDelta-2
Ferruccio Guidi [Wed, 2 Jul 2008 17:54:41 +0000 (17:54 +0000)]
svn:ignore set on LambdaDelta-2

16 years ago- new tactic applyP for use in the *P*rocedural script reconstruction
Ferruccio Guidi [Wed, 2 Jul 2008 17:33:03 +0000 (17:33 +0000)]
- new tactic applyP for use in the *P*rocedural script reconstruction
- LAMBDA-TYPES: the mma files from the LambdaDelta section

16 years agoFixed a bug which prevented mutually recursive definitions of 3 or more
Wilmer Ricciotti [Wed, 2 Jul 2008 15:12:24 +0000 (15:12 +0000)]
Fixed a bug which prevented mutually recursive definitions of 3 or more
functions from being added to the library

16 years ago...
Enrico Tassi [Wed, 2 Jul 2008 15:05:26 +0000 (15:05 +0000)]
...

16 years agoreturn 1 in case of failure
Enrico Tassi [Wed, 2 Jul 2008 12:50:18 +0000 (12:50 +0000)]
return 1 in case of failure

16 years ago0.5.2
Enrico Tassi [Wed, 2 Jul 2008 12:14:48 +0000 (12:14 +0000)]
0.5.2

16 years ago0.5.2
Enrico Tassi [Wed, 2 Jul 2008 12:14:29 +0000 (12:14 +0000)]
0.5.2

16 years ago...
Enrico Tassi [Wed, 2 Jul 2008 09:32:37 +0000 (09:32 +0000)]
...

16 years ago...
Enrico Tassi [Wed, 2 Jul 2008 09:18:27 +0000 (09:18 +0000)]
...

16 years ago...
Enrico Tassi [Wed, 2 Jul 2008 09:18:21 +0000 (09:18 +0000)]
...

16 years agocalculation of the sort user to choose the rewriting principle fixed
Enrico Tassi [Wed, 2 Jul 2008 09:13:12 +0000 (09:13 +0000)]
calculation of the sort user to choose the rewriting principle fixed
(the one of the goal was used also to rewrite in an hypothesis)

16 years ago- lambda-delta: some speed up (not very much :) actually)
Ferruccio Guidi [Tue, 1 Jul 2008 18:21:22 +0000 (18:21 +0000)]
- lambda-delta: some speed up (not very much :) actually)
- LAMBDA-TYPES: bug fix in Makefile

16 years agoshifting done, merge attacked
Enrico Tassi [Tue, 1 Jul 2008 14:25:20 +0000 (14:25 +0000)]
shifting done, merge attacked

16 years agoshift almost done
Enrico Tassi [Tue, 1 Jul 2008 12:00:22 +0000 (12:00 +0000)]
shift almost done

16 years agonew specification
Enrico Tassi [Mon, 30 Jun 2008 22:50:55 +0000 (22:50 +0000)]
new specification

16 years agowe improved the data structures used in the translation to the intermediate
Ferruccio Guidi [Mon, 30 Jun 2008 19:34:06 +0000 (19:34 +0000)]
we improved the data structures used in the translation to the intermediate
language

16 years agosome more work on q
Enrico Tassi [Mon, 30 Jun 2008 18:54:26 +0000 (18:54 +0000)]
some more work on q

16 years agowe tranlate an Automath book in an itermediate format where:
Ferruccio Guidi [Mon, 30 Jun 2008 14:07:46 +0000 (14:07 +0000)]
we tranlate an Automath book in an itermediate format where:
- the local references are resolved as position indexes
- the global references are disambiguated
- the parameter applications are completed
For now the trnslation is slow because the involved data structures are
inefficient

16 years agosome more work to factorize out uninteresting parts of the proof...
Enrico Tassi [Sat, 28 Jun 2008 11:28:34 +0000 (11:28 +0000)]
some more work to factorize out uninteresting parts of the proof...
still to close the key lemma...

16 years agomore work to try to understand where the issue is
Enrico Tassi [Fri, 27 Jun 2008 19:11:42 +0000 (19:11 +0000)]
more work to try to understand where the issue is

16 years agolost in the wood
Enrico Tassi [Fri, 27 Jun 2008 16:32:24 +0000 (16:32 +0000)]
lost in the wood

16 years agomore work
Enrico Tassi [Thu, 26 Jun 2008 21:35:10 +0000 (21:35 +0000)]
more work

16 years agofew more steps
Enrico Tassi [Thu, 26 Jun 2008 20:48:25 +0000 (20:48 +0000)]
few more steps

16 years agomore work
Enrico Tassi [Thu, 26 Jun 2008 20:22:19 +0000 (20:22 +0000)]
more work

16 years agosome more work
Enrico Tassi [Thu, 26 Jun 2008 13:52:36 +0000 (13:52 +0000)]
some more work

16 years agomore work on q
Enrico Tassi [Thu, 26 Jun 2008 11:43:08 +0000 (11:43 +0000)]
more work on q

16 years agosome more work
Enrico Tassi [Wed, 25 Jun 2008 14:54:47 +0000 (14:54 +0000)]
some more work