]> matita.cs.unibo.it Git - helm.git/log
helm.git
17 years agonew case implementation
Enrico Tassi [Tue, 3 Apr 2007 08:35:14 +0000 (08:35 +0000)]
new case implementation

17 years agoProcedural: some improvements
Ferruccio Guidi [Mon, 2 Apr 2007 17:57:03 +0000 (17:57 +0000)]
Procedural: some improvements

17 years agoProcedural: refactoring
Ferruccio Guidi [Mon, 2 Apr 2007 12:20:41 +0000 (12:20 +0000)]
Procedural: refactoring

17 years agoCic2acic : added some debugging information
Ferruccio Guidi [Mon, 2 Apr 2007 12:09:35 +0000 (12:09 +0000)]
Cic2acic  : added some debugging information
Procedural: some refactoring and improvements

17 years agoadded some tests for cases
Enrico Tassi [Mon, 2 Apr 2007 11:20:44 +0000 (11:20 +0000)]
added some tests for cases

17 years agohopefully fixed cases implementation
Enrico Tassi [Mon, 2 Apr 2007 11:20:22 +0000 (11:20 +0000)]
hopefully fixed cases implementation

17 years agoOptimizer: refactored according to its formal description
Ferruccio Guidi [Fri, 30 Mar 2007 21:54:45 +0000 (21:54 +0000)]
Optimizer: refactored according to its formal description

17 years agoSerious bug fixed: a variable was captured during unfolding of Fix, resulting
Claudio Sacerdoti Coen [Mon, 26 Mar 2007 18:05:50 +0000 (18:05 +0000)]
Serious bug fixed: a variable was captured during unfolding of Fix, resulting
in the context of the return type of mutually recursive definitions being
lifted for each function but the first one!

17 years agoadded eta expansion to avoid universe inconsistency.
Enrico Tassi [Mon, 26 Mar 2007 13:24:27 +0000 (13:24 +0000)]
added eta expansion to avoid universe inconsistency.

17 years agoSeveral instances of the same bug fixed at once: when processing a Fix,
Claudio Sacerdoti Coen [Thu, 22 Mar 2007 19:04:32 +0000 (19:04 +0000)]
Several instances of the same bug fixed at once: when processing a Fix,
before adding the types to the context (to process the bodies), the types
must be lifted. The simplify tactic is still not working propertly.

17 years agoDebugging code removed.
Claudio Sacerdoti Coen [Thu, 22 Mar 2007 16:20:36 +0000 (16:20 +0000)]
Debugging code removed.

17 years agoelim tactic: it needs two arguments, a term as well as a pattern
Ferruccio Guidi [Fri, 16 Mar 2007 18:39:27 +0000 (18:39 +0000)]
elim tactic: it needs two arguments, a term as well as a pattern
CicReduction: head_beta_reduce now can take the number of beta-redexes to reduce
Procedural: refactoring

17 years agoNew contrib moebius.ma.
Andrea Asperti [Fri, 16 Mar 2007 08:05:44 +0000 (08:05 +0000)]
New contrib moebius.ma.

17 years agoExtensions required for the moebius function (in Z).
Andrea Asperti [Fri, 16 Mar 2007 08:04:32 +0000 (08:04 +0000)]
Extensions required for the moebius function (in Z).

17 years agoRole of
Claudio Sacerdoti Coen [Tue, 13 Mar 2007 16:17:42 +0000 (16:17 +0000)]
Role of
 - replace
 - replace_lifting
 - replace_lifting_csc
clarified with comments. None of this function is the inverse of subst :-)

17 years agoelim tactic: now takes a pattern instead of just a term
Ferruccio Guidi [Tue, 13 Mar 2007 13:21:56 +0000 (13:21 +0000)]
elim tactic: now takes a pattern instead of just a term
             works as before for now. the pattern wil be activated soon
Procedural:  cleaning up
ProofEngineReduction: new subst_inv function exactly inverts subst

17 years agoFew theorems added.`
Andrea Asperti [Tue, 13 Mar 2007 10:58:06 +0000 (10:58 +0000)]
Few theorems added.`

17 years agonew version of div_and_mod
Andrea Asperti [Tue, 13 Mar 2007 10:53:33 +0000 (10:53 +0000)]
new version of div_and_mod

17 years agoCapturing Invalid_argument inside pp (otherwise we cannot even
Andrea Asperti [Tue, 13 Mar 2007 10:50:01 +0000 (10:50 +0000)]
Capturing Invalid_argument inside pp (otherwise we cannot even
see what's wrong *) wrong.

17 years agocase to elim conversion works fine
Ferruccio Guidi [Sun, 11 Mar 2007 21:17:44 +0000 (21:17 +0000)]
case to elim conversion works fine

17 years agoadded a test for rewrite under Pi
Ferruccio Guidi [Sat, 10 Mar 2007 22:58:31 +0000 (22:58 +0000)]
added a test for rewrite under Pi

17 years agorewrite tactic: bug fix in rewriting under Pi's:
Ferruccio Guidi [Sat, 10 Mar 2007 22:23:38 +0000 (22:23 +0000)]
rewrite tactic: bug fix in rewriting under Pi's:
                the application context of the subterm to rewrite can not be
forgotten

17 years agoProcedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation
Ferruccio Guidi [Fri, 9 Mar 2007 22:53:49 +0000 (22:53 +0000)]
Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

17 years agosome improvements
Ferruccio Guidi [Thu, 8 Mar 2007 15:31:02 +0000 (15:31 +0000)]
some improvements

17 years agoProcedural: bug fix
Ferruccio Guidi [Wed, 7 Mar 2007 15:49:41 +0000 (15:49 +0000)]
Procedural: bug fix

17 years agoRelational: one file was missing :-)
Ferruccio Guidi [Wed, 7 Mar 2007 11:29:03 +0000 (11:29 +0000)]
Relational: one file was missing :-)
Procedural: the cic object preprocessor was not added to svn :-)

17 years agoProcedural : cic object preprocessor added
Ferruccio Guidi [Wed, 7 Mar 2007 11:11:22 +0000 (11:11 +0000)]
Procedural  : cic object preprocessor added
depend[.opt]: some fixes

17 years agoProcedural: now patterns for rewrite are generated correctly
Ferruccio Guidi [Fri, 2 Mar 2007 22:24:16 +0000 (22:24 +0000)]
Procedural: now patterns for rewrite are generated correctly

17 years agoProcedural: some improvements
Ferruccio Guidi [Thu, 1 Mar 2007 19:00:14 +0000 (19:00 +0000)]
Procedural: some improvements
rewrite tactic: bug fix in hyps searching
TermContentPres: one space added in let-in rendering
prova.ma: new procedural proof of ty3_gen_cast

17 years agoprocedural proof of ty3_gen_cast
Ferruccio Guidi [Thu, 1 Mar 2007 15:45:33 +0000 (15:45 +0000)]
procedural proof of ty3_gen_cast

17 years ago"by j let x : T such that P(x)" generalized to allow arbitrary justifications.
Enrico Zoli [Thu, 1 Mar 2007 12:15:24 +0000 (12:15 +0000)]
"by j let x : T such that P(x)" generalized to allow arbitrary justifications.
The code and behaviour should be cleaned up a little bit.

17 years agosome improvements
Ferruccio Guidi [Tue, 27 Feb 2007 19:20:48 +0000 (19:20 +0000)]
some improvements

17 years ago- Procedural: some improvements
Ferruccio Guidi [Tue, 27 Feb 2007 16:36:45 +0000 (16:36 +0000)]
- Procedural: some improvements
- intros n tactic: now tries whd when Pi or let-ins are not enough

17 years agodecompose: delta-expansion of the type to eliminate now works fine
Ferruccio Guidi [Mon, 26 Feb 2007 13:36:43 +0000 (13:36 +0000)]
decompose: delta-expansion of the type to eliminate now works fine

17 years agoRELATIONAL: new undecomposable definition of NLE
Ferruccio Guidi [Sun, 25 Feb 2007 16:28:38 +0000 (16:28 +0000)]
RELATIONAL: new undecomposable definition of NLE
Procedural: some refactoring
decompose tactic: only types of sort Prop are decomposed now

17 years agodecompose now works without premises
Ferruccio Guidi [Wed, 21 Feb 2007 15:59:26 +0000 (15:59 +0000)]
decompose now works without premises

17 years agoprocedural : some improvements.
Ferruccio Guidi [Wed, 21 Feb 2007 14:15:55 +0000 (14:15 +0000)]
procedural      : some improvements.
decompose tactic: user provided premise and types removed.
                  The decomposable types are now the non-recursive inductive
  types without right parameters and are auto-detected

17 years agoacic_procedural: changed module compilation order
Ferruccio Guidi [Tue, 20 Feb 2007 16:27:33 +0000 (16:27 +0000)]
acic_procedural: changed module compilation order
TermAcicContent: bug fix in AMutCase
                 the presence of left parametes was not taken into account

17 years agosmall fix to make it compile again
notin [Tue, 20 Feb 2007 14:45:11 +0000 (14:45 +0000)]
small fix to make it compile again

17 years agoadded some code to print the praamodulation proofs with a graph
Enrico Tassi [Mon, 19 Feb 2007 22:03:09 +0000 (22:03 +0000)]
added some code to print the praamodulation proofs with a graph

17 years agoUnified-Sub: lift_comm completed
Ferruccio Guidi [Mon, 19 Feb 2007 14:11:14 +0000 (14:11 +0000)]
Unified-Sub: lift_comm completed

17 years agocontribs: some improvements
Ferruccio Guidi [Sat, 17 Feb 2007 22:37:23 +0000 (22:37 +0000)]
contribs: some improvements

17 years agocontribs: some improvements
Ferruccio Guidi [Thu, 15 Feb 2007 23:02:13 +0000 (23:02 +0000)]
contribs: some improvements
Sequent2pres: added some spaces

17 years agorefactoring
Ferruccio Guidi [Thu, 15 Feb 2007 15:19:33 +0000 (15:19 +0000)]
refactoring

17 years agosome improvements
Ferruccio Guidi [Wed, 14 Feb 2007 19:54:52 +0000 (19:54 +0000)]
some improvements

17 years agoProcedural : some improvements
Ferruccio Guidi [Wed, 14 Feb 2007 17:10:16 +0000 (17:10 +0000)]
Procedural       : some improvements
PrimitiveTactics : tentative implementation of using clause in elim
CicNotationParser: noe declarations of the form (_:t) are parsable

17 years agoLexiconAstPp: fixed syntax for include
Ferruccio Guidi [Mon, 12 Feb 2007 22:53:46 +0000 (22:53 +0000)]
LexiconAstPp: fixed syntax for include
TermContentPres: fixed syntax for letin
lexiconEngine: moved callback from grafiteParser
matitac: -dump patched

17 years agounified: some theorems on Lift started
Ferruccio Guidi [Mon, 12 Feb 2007 08:03:58 +0000 (08:03 +0000)]
unified: some theorems on Lift started

17 years agoUnified: INC and BEq removed
Ferruccio Guidi [Sun, 11 Feb 2007 12:46:45 +0000 (12:46 +0000)]
Unified: INC and BEq removed
contribs: added dependence to ../legacy in the Makefile

17 years agoadded option -dump to matitac for persistent macro expansion
Ferruccio Guidi [Fri, 9 Feb 2007 17:27:31 +0000 (17:27 +0000)]
added option -dump to matitac for persistent macro expansion

17 years agoAvoid generating invalid names with "'" in the middle of them.
Claudio Sacerdoti Coen [Fri, 9 Feb 2007 16:18:37 +0000 (16:18 +0000)]
Avoid generating invalid names with "'" in the middle of them.

17 years agoAdded toggle for enabling/disabling the conversion from multibyte unicode
Stefano Zacchiroli [Fri, 9 Feb 2007 16:18:01 +0000 (16:18 +0000)]
Added toggle for enabling/disabling the conversion from multibyte unicode
characters to TeX when converting CIC terms to textual formulae. The toggle is
under the Edit menu (rational: it's near the paste commands, maybe it should be
added to the GtkSourceView contextual menu too). The toggle governs the
matita.paste_unicode_as_tex boolean registry value. The txt_of_* rendering
functions have been changed to accept a new optional boolean parameter.

17 years agoThe ApplyTransformation.txt_of_term function has been made more robust to
Claudio Sacerdoti Coen [Fri, 9 Feb 2007 16:05:29 +0000 (16:05 +0000)]
The ApplyTransformation.txt_of_term function has been made more robust to
exceptions.

17 years ago- moved to the view menu toggles for coercion hiding and notation pp
Stefano Zacchiroli [Fri, 9 Feb 2007 15:18:08 +0000 (15:18 +0000)]
- moved to the view menu toggles for coercion hiding and notation pp
- moved back the high level pp toggle to the debug menu

17 years agoExceptions should never escape the final exception handler for the worker
Claudio Sacerdoti Coen [Fri, 9 Feb 2007 15:12:07 +0000 (15:12 +0000)]
Exceptions should never escape the final exception handler for the worker
threads. This patch just reduces the probability.

17 years agoDebugging code fixed. To enable debugging just set debug to true at the
Claudio Sacerdoti Coen [Fri, 9 Feb 2007 15:07:13 +0000 (15:07 +0000)]
Debugging code fixed. To enable debugging just set debug to true at the
top of the file.

17 years agoDebugging code removed.
Claudio Sacerdoti Coen [Fri, 9 Feb 2007 14:53:30 +0000 (14:53 +0000)]
Debugging code removed.

17 years agomoved the high level pretty printing setting to a toggle menu item of the View menu...
Stefano Zacchiroli [Fri, 9 Feb 2007 13:29:08 +0000 (13:29 +0000)]
moved the high level pretty printing setting to a toggle menu item of the View menu (with CTRL-P shortcut)

17 years agoMore progress in technicalities/setoids.ma.
Claudio Sacerdoti Coen [Thu, 8 Feb 2007 18:46:57 +0000 (18:46 +0000)]
More progress in technicalities/setoids.ma.
I have now reached the final theorem!

17 years agoManual for the "default" command updated.
Claudio Sacerdoti Coen [Thu, 8 Feb 2007 18:27:48 +0000 (18:27 +0000)]
Manual for the "default" command updated.

17 years ago* 'default "equality"' command changed to consider also
Claudio Sacerdoti Coen [Thu, 8 Feb 2007 18:11:08 +0000 (18:11 +0000)]
* 'default "equality"' command changed to consider also
  eq_rec, eq_rec_r, eq_rect, eq_rect_r
* rewrite tactic changed to rewrite also in goals of type Set and Type
* more progress in technicalities/setoids.ma

17 years agoIf a pretty printed term spans on multiple lines, then it is printed after
Claudio Sacerdoti Coen [Thu, 8 Feb 2007 16:55:37 +0000 (16:55 +0000)]
If a pretty printed term spans on multiple lines, then it is printed after
a new line and followed by a new line too.

17 years agoImportant commit:
Claudio Sacerdoti Coen [Thu, 8 Feb 2007 16:44:53 +0000 (16:44 +0000)]
Important commit:
from now on the pretty printer CicMetaSubst.ppterm_in_context is substituted
with a reference to an high level pretty-printer (now defined in
matita/applyTransformation.ml). In the debug menu there is a switch to turn
it off and get back the old pretty-printer.

17 years agodevelopments fixup
Ferruccio Guidi [Thu, 8 Feb 2007 15:39:43 +0000 (15:39 +0000)]
developments fixup

17 years agoUnified refactored
Ferruccio Guidi [Thu, 8 Feb 2007 15:33:29 +0000 (15:33 +0000)]
Unified refactored

17 years agodefinitions fixup
Ferruccio Guidi [Thu, 8 Feb 2007 15:24:44 +0000 (15:24 +0000)]
definitions fixup

17 years agofix dependences for matita
Ferruccio Guidi [Thu, 8 Feb 2007 13:52:04 +0000 (13:52 +0000)]
fix dependences for matita

17 years agoLAMBDA-TYPES: refactored
Ferruccio Guidi [Wed, 7 Feb 2007 19:13:19 +0000 (19:13 +0000)]
LAMBDA-TYPES: refactored

17 years agorefactoring
Ferruccio Guidi [Wed, 7 Feb 2007 19:11:00 +0000 (19:11 +0000)]
refactoring

17 years agoLevel-1 refactored
Ferruccio Guidi [Wed, 7 Feb 2007 18:35:46 +0000 (18:35 +0000)]
Level-1 refactored

17 years agorefactoring
Ferruccio Guidi [Wed, 7 Feb 2007 18:34:04 +0000 (18:34 +0000)]
refactoring

17 years agorefactoring
Ferruccio Guidi [Wed, 7 Feb 2007 18:29:01 +0000 (18:29 +0000)]
refactoring

17 years agoNew dependency over acic_procedural.
Claudio Sacerdoti Coen [Wed, 7 Feb 2007 10:47:05 +0000 (10:47 +0000)]
New dependency over acic_procedural.

17 years ago- Procedural: moved in a directory on its own
Ferruccio Guidi [Tue, 6 Feb 2007 19:36:05 +0000 (19:36 +0000)]
- Procedural: moved in a directory on its own
- ApplyTransofrmation: now handles inline macro expansion
- GrafiteParser MatitaEngine MatitacLib: added a callback in each
- tests/letrecand.ma: changed baseuri

17 years agoMore stuff in technicalities/setoids.ma
Claudio Sacerdoti Coen [Tue, 6 Feb 2007 18:50:23 +0000 (18:50 +0000)]
More stuff in technicalities/setoids.ma

17 years agoDebugging deactivated.
Claudio Sacerdoti Coen [Tue, 6 Feb 2007 18:49:52 +0000 (18:49 +0000)]
Debugging deactivated.

17 years agoBug fixed in the computation of the disambiguation domain of a let...rec.
Claudio Sacerdoti Coen [Tue, 6 Feb 2007 18:47:05 +0000 (18:47 +0000)]
Bug fixed in the computation of the disambiguation domain of a let...rec.

17 years agoIncredible bug fixed in Fix and CoFix. The types of the mutual inductive
Claudio Sacerdoti Coen [Tue, 6 Feb 2007 18:46:35 +0000 (18:46 +0000)]
Incredible bug fixed in Fix and CoFix. The types of the mutual inductive
functions were not lifted when added to the context.

17 years agoSecond formulation of a constructive (positive) proof of Lebesgue's
Claudio Sacerdoti Coen [Mon, 5 Feb 2007 18:10:17 +0000 (18:10 +0000)]
Second formulation of a constructive (positive) proof of Lebesgue's
integration theorem, based on a proof by Weber.

17 years agoSerious bug fixed: the types of a real mutual fix definition were not lifted
Claudio Sacerdoti Coen [Fri, 2 Feb 2007 18:15:59 +0000 (18:15 +0000)]
Serious bug fixed: the types of a real mutual fix definition were not lifted
as required. Moreover, an unification exception used to escape the refiner.
Now it does no more, but the error is not localized (being about the branch
of a MutCase that has no precise localization).

17 years agoadded preamble file in LambdaDelta and improved theory files
Ferruccio Guidi [Fri, 2 Feb 2007 13:35:52 +0000 (13:35 +0000)]
added preamble file in LambdaDelta and improved theory files

17 years agoThe baseuris changed
Ferruccio Guidi [Fri, 2 Feb 2007 10:58:31 +0000 (10:58 +0000)]
The baseuris changed

17 years agoLevel-1: regenerated with differnt baseuris
Ferruccio Guidi [Thu, 1 Feb 2007 19:35:29 +0000 (19:35 +0000)]
Level-1: regenerated with differnt baseuris

17 years agorestored coercions between eq and eq
Enrico Tassi [Thu, 1 Feb 2007 14:48:46 +0000 (14:48 +0000)]
restored coercions between eq and eq

17 years agoreverted a commented substitution in build_newgoal, added an euristic to
Enrico Tassi [Thu, 1 Feb 2007 14:48:05 +0000 (14:48 +0000)]
reverted a commented substitution in build_newgoal, added an euristic to
order the lambdas of a proof abstracted in a letin such that dependency betwwen the types of the lambdas is inferrable by the refiner

17 years agomethods eos, goto, advance and retract now catch Invalid_argument "Array.make"
Ferruccio Guidi [Wed, 31 Jan 2007 19:54:01 +0000 (19:54 +0000)]
methods eos, goto, advance and retract now catch Invalid_argument "Array.make"
that is raised when the script is too big to be handled (this makes quit work!)

17 years agoSeveral bugs fixed:
Claudio Sacerdoti Coen [Wed, 31 Jan 2007 18:36:04 +0000 (18:36 +0000)]
Several bugs fixed:
 1. mutual definitions were not generated correctly
    (e.g. let rec even ... and odd in even actually resulted in a
     definition of odd!)
 2. a top-level mutual definition now generates two constants (as it
    should have always been)

17 years agoNew test for mutual recursive definitions.
Claudio Sacerdoti Coen [Wed, 31 Jan 2007 18:29:53 +0000 (18:29 +0000)]
New test for mutual recursive definitions.

17 years agoProof size nicely reduced using distributive branching with goal selector.
Claudio Sacerdoti Coen [Tue, 30 Jan 2007 15:26:27 +0000 (15:26 +0000)]
Proof size nicely reduced using distributive branching with goal selector.
Look for
 ] ;
 [1,3,5,7,9,11:
   ...
 |2,4,6,8,10,12:
   ...
 ]

17 years agoEven more (painful) work on setoids.
Claudio Sacerdoti Coen [Tue, 30 Jan 2007 15:18:29 +0000 (15:18 +0000)]
Even more (painful) work on setoids.

17 years agoBehaviour of CicRefine.type_of_aux' on MutCases changed: branches are now
Claudio Sacerdoti Coen [Tue, 30 Jan 2007 13:42:09 +0000 (13:42 +0000)]
Behaviour of CicRefine.type_of_aux' on MutCases changed: branches are now
processed from right to left to make the cases tactic open goals in the
expected order.

17 years agoMore work on setoids.
Claudio Sacerdoti Coen [Mon, 29 Jan 2007 11:13:06 +0000 (11:13 +0000)]
More work on setoids.

17 years agoSome more datatypes lifted to Type.
Claudio Sacerdoti Coen [Mon, 29 Jan 2007 11:12:43 +0000 (11:12 +0000)]
Some more datatypes lifted to Type.

17 years agowell-formed ocamldoc comment
Stefano Zacchiroli [Mon, 29 Jan 2007 10:47:02 +0000 (10:47 +0000)]
well-formed ocamldoc comment

17 years agopreliminary cookie support
Stefano Zacchiroli [Mon, 29 Jan 2007 10:43:50 +0000 (10:43 +0000)]
preliminary cookie support

17 years agoAdded option datatype. Required (for technicalities/Setoids.ma).
Claudio Sacerdoti Coen [Sat, 27 Jan 2007 16:32:56 +0000 (16:32 +0000)]
Added option datatype. Required (for technicalities/Setoids.ma).

17 years ago"Warning/error/debug/infos" messages now sent on stderr.
Claudio Sacerdoti Coen [Fri, 26 Jan 2007 13:15:56 +0000 (13:15 +0000)]
"Warning/error/debug/infos" messages now sent on stderr.

17 years agoSome changes:
Claudio Sacerdoti Coen [Fri, 26 Jan 2007 13:04:44 +0000 (13:04 +0000)]
Some changes:
1. error messages are now in HTML (they used to be in plain text + vt100 colour
   scheme)
2. commands are now expected to be in a fragment of the pgip protocol.
   Supported commands are:
    <pgip><doitem>...</doitem></pgip>
    <pgip><undoitem>...</undoitem></pgip>
3. the terminator sent back is now preceded by either -1 (command not
   successful) or n (an integer to be sent for undoing)
4. undoing is now supported

17 years agotactics.mli: regenerated
Ferruccio Guidi [Wed, 24 Jan 2007 19:44:22 +0000 (19:44 +0000)]
tactics.mli: regenerated
LambdaDelta: regenerated with some new theorems

17 years agomatitaGui: some missing cases during disambiguation now treated
Ferruccio Guidi [Wed, 24 Jan 2007 19:28:15 +0000 (19:28 +0000)]
matitaGui: some missing cases during disambiguation now treated
grafiteAst: rename tactic removed
procedural: some improvements