]> matita.cs.unibo.it Git - helm.git/log
helm.git
17 years agoSubstTactic: bug fix
Ferruccio Guidi [Tue, 1 May 2007 16:15:58 +0000 (16:15 +0000)]
SubstTactic: bug fix
RELATIONAL : some improvements on integers

17 years agoEven if we are at depth 0, we first check in the cache for a solution,
Andrea Asperti [Mon, 30 Apr 2007 10:51:14 +0000 (10:51 +0000)]
Even if we are at depth 0, we first check in the cache for a solution,
before failing. In the other case the assert false at line 76 of
autocache may fail.

17 years agoRemoved an assert false; everything works again, but something
Andrea Asperti [Mon, 30 Apr 2007 10:31:15 +0000 (10:31 +0000)]
Removed an assert false; everything works again, but something
is clearly wrong (to be fixed).

17 years agoGrafiteAstPp: \n's finally fixed
Ferruccio Guidi [Sun, 29 Apr 2007 15:41:14 +0000 (15:41 +0000)]
GrafiteAstPp: \n's finally fixed
acic_procedural:
 - elimination patterns are generated correctly
 - comments on elimination cases added

17 years agoAMBDA-TYPES: some improvements. subst now fully exploited
Ferruccio Guidi [Sat, 28 Apr 2007 12:17:50 +0000 (12:17 +0000)]
AMBDA-TYPES: some improvements. subst now fully exploited
developments.txt: added library_auto
RELATIONAL: some improvements. subst now fully exploited
cic_procedural: a List.rev was missing :-p
substTactic: tacticals are now exploited properly

17 years agoLAMBDA-TYPES: some improvements
Ferruccio Guidi [Fri, 27 Apr 2007 19:08:54 +0000 (19:08 +0000)]
LAMBDA-TYPES: some improvements

17 years agoSubst is passed in input to apapluy, so no need to concatenate the results
Andrea Asperti [Fri, 27 Apr 2007 14:00:24 +0000 (14:00 +0000)]
Subst is passed in input to apapluy, so no need to concatenate the results

17 years agoApply_with_subst now returns a subst with a correct type for the meta.
Andrea Asperti [Fri, 27 Apr 2007 13:46:36 +0000 (13:46 +0000)]
Apply_with_subst now returns a subst with a correct type for the meta.

17 years agoprocedural: bug fixes
Ferruccio Guidi [Thu, 26 Apr 2007 19:06:42 +0000 (19:06 +0000)]
procedural: bug fixes
matita: some \n rearranged
GrafiteAstPp: some \n rearranged
GrafiteParser: added callback

17 years agobug fix in subst tactic
Ferruccio Guidi [Thu, 26 Apr 2007 13:05:48 +0000 (13:05 +0000)]
bug fix in subst tactic

17 years agogoal ==> focus
Claudio Sacerdoti Coen [Tue, 24 Apr 2007 15:06:19 +0000 (15:06 +0000)]
goal ==> focus

17 years agoSubsumption_subst re-added to initial.
Andrea Asperti [Tue, 24 Apr 2007 13:54:10 +0000 (13:54 +0000)]
Subsumption_subst re-added to initial.

17 years ago@
Andrea Asperti [Tue, 24 Apr 2007 13:42:00 +0000 (13:42 +0000)]
@

17 years agoDeprecated "goal" removed.
Claudio Sacerdoti Coen [Mon, 23 Apr 2007 13:40:00 +0000 (13:40 +0000)]
Deprecated "goal" removed.

17 years agoA new test on some non punctuation tacticals.
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 15:39:16 +0000 (15:39 +0000)]
A new test on some non punctuation tacticals.

17 years agoThe declarative rewriting step now tries auto timeout=3 before
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 15:33:27 +0000 (15:33 +0000)]
The declarative rewriting step now tries auto timeout=3 before
auto paramodulation timeout=3. This seems to work better then just
auto paramodulation alone when the user tries to help the system.
This because paramodulation is more confused than helped.

17 years agoadded skip, removed end
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 14:47:25 +0000 (14:47 +0000)]
added skip, removed end

17 years agoMuch ado about nothing:
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 14:46:36 +0000 (14:46 +0000)]
Much ado about nothing:
 1) repeat tac end ==> repeat tac
 2) do n tac end   ==> do n tac
 3) "goal n" finally dropped (deprecated, semantics no longer clear)
 4) the AST (in grafiteAst) has been changed to better reflect the
    distinction between tactics (including h.o. tactics, i.e. tacticals),
    punctuational tinycals and non punctuation tinycals (i.e. skip, focus,
    unfocus)
 5) all tacticals are now running properly in every condition;
    but tacticals argument (i.e. tactics occurring in tacticals) are
    disambiguated eagerly and not lazily (to be changed)

WARNING: the code in proceduralTypes.ml has been commented out since I am
not able to figure out how to fix it properly

17 years agoBug fixed: off by one array access in the last patch.
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 14:31:25 +0000 (14:31 +0000)]
Bug fixed: off by one array access in the last patch.

17 years agodevelopments root are now part of default inclusion paths;
Enrico Tassi [Fri, 20 Apr 2007 13:30:16 +0000 (13:30 +0000)]
developments root are now part of default inclusion paths;
incluson path used to include something is printed (to understand what is gouing on)

17 years agoadded library_auto/ to tests.
Enrico Tassi [Fri, 20 Apr 2007 12:26:16 +0000 (12:26 +0000)]
added library_auto/ to tests.

17 years agofixed paths and prefixes of included files
Enrico Tassi [Fri, 20 Apr 2007 12:24:44 +0000 (12:24 +0000)]
fixed paths and prefixes of included files

17 years agoInterface of the argument to Continuationals.Make greately simplified. The
Claudio Sacerdoti Coen [Fri, 20 Apr 2007 11:30:44 +0000 (11:30 +0000)]
Interface of the argument to Continuationals.Make greately simplified. The
following functions have been removed:
 - id_tactic
 - get_status
 - get_proof
 - set_goals

17 years agochanged base uri
Cristian Armentano [Fri, 20 Apr 2007 10:06:10 +0000 (10:06 +0000)]
changed base uri

17 years agoinitial import
Cristian Armentano [Fri, 20 Apr 2007 10:03:20 +0000 (10:03 +0000)]
initial import

17 years agoEXPERIMENTAL and _INCOMPLETE_ COMMIT:
Claudio Sacerdoti Coen [Thu, 19 Apr 2007 17:21:09 +0000 (17:21 +0000)]
EXPERIMENTAL and _INCOMPLETE_ COMMIT:

Tacticals invoked from the top-level but the ones implemented on top
of tinycals  where not working properly because of several bugs.

The current commit changes the code in quite a few places:

1) there is no longer a function Tacticals.Make since tacticals implemented
   on top of tinycals always instantiated the functor with
   Tacticals.ProofEngineStatus, and the toplevel can avoid any instantiation
   at all since it can invoke tinycals directly on the low-level machine
   (implemented by the functor Continuationals.Make)
2) when GrafiteEngine now meets a punctuation tacticals, it directly invokes
   an instantiation of Continuationals.Make, without going througw Tacticals.
   Instead, when it meets a real tactical, it directly invokes Tacticals
   (where Continuationals.Make is applied to Tacticals.ProofEngineStatus
   and not to the module defined in GrafiteEngine and used for punctuation
   tacticals)
3) most of the tacticals not implemented on top of tinycals were bugged
   (and unused). E.g.: solve always diverged unless it was applied to the
   empty list. All these bugs have been fixed.

The commit is incomplete since:

1) all tacticals not implemented on top of tactics now accept only a single
   tactic as argument (if they require a list, the list must be a singleton).
   This limitation is going to disappear again, but we must change GrafiteAst
   so that an atomic tactical becomes a recursive tactic.
2) Seq and Then are not branched (for the same reasons as 1 and a bit of
   lazyness)
3) several auxiliary functions in the argument of Continuaniolas.Make can now
   be removed since they were introduced for wrong reasons.

17 years agoThe night test now shows the last commits and blames/praises the authors.
Claudio Sacerdoti Coen [Thu, 19 Apr 2007 17:17:36 +0000 (17:17 +0000)]
The night test now shows the last commits and blames/praises the authors.

17 years agomore discriminate
Enrico Tassi [Wed, 18 Apr 2007 10:08:40 +0000 (10:08 +0000)]
more discriminate

17 years agohandles failures (sometimes you can't inject)
Enrico Tassi [Wed, 18 Apr 2007 09:20:57 +0000 (09:20 +0000)]
handles failures (sometimes you can't inject)

17 years agoNew query result diff.
Claudio Sacerdoti Coen [Wed, 18 Apr 2007 09:15:18 +0000 (09:15 +0000)]
New query result diff.

17 years agoOnly benches with the same result are compared for timing.
Claudio Sacerdoti Coen [Wed, 18 Apr 2007 09:10:30 +0000 (09:10 +0000)]
Only benches with the same result are compared for timing.

17 years agoAdded new query to time-diff the last mark with the previous one.
Claudio Sacerdoti Coen [Wed, 18 Apr 2007 08:56:53 +0000 (08:56 +0000)]
Added new query to time-diff the last mark with the previous one.
The query is also the example query below in case you want to change the two
marks.

17 years agotassi/sacerdot
Claudio Sacerdoti Coen [Wed, 18 Apr 2007 08:12:52 +0000 (08:12 +0000)]
tassi/sacerdot

17 years ago"end" keyword added
Ferruccio Guidi [Tue, 17 Apr 2007 18:51:26 +0000 (18:51 +0000)]
"end" keyword added

17 years agoone more step toward a decent destruct
Enrico Tassi [Tue, 17 Apr 2007 14:53:04 +0000 (14:53 +0000)]
one more step toward a decent destruct
lifting should now be ok, but handling of wight params is still
shaky

17 years agoRT_BASEDIR changed to a sensible path
Enrico Tassi [Tue, 17 Apr 2007 09:44:43 +0000 (09:44 +0000)]
RT_BASEDIR changed to a sensible path

17 years agobroken list fix
Enrico Tassi [Tue, 17 Apr 2007 09:22:56 +0000 (09:22 +0000)]
broken list fix

17 years agofixed a list.nth called on a too short list
Enrico Tassi [Tue, 17 Apr 2007 08:41:09 +0000 (08:41 +0000)]
fixed a list.nth called on a too short list

17 years ago...
Enrico Tassi [Tue, 17 Apr 2007 08:22:49 +0000 (08:22 +0000)]
...

17 years agoadded generation of hne and heq problems
Enrico Tassi [Tue, 17 Apr 2007 08:21:57 +0000 (08:21 +0000)]
added generation of hne and heq problems

17 years agobetter simplify
Enrico Tassi [Mon, 16 Apr 2007 21:16:11 +0000 (21:16 +0000)]
better simplify

17 years agosimplify has a brand new semantics!
Enrico Tassi [Mon, 16 Apr 2007 21:15:44 +0000 (21:15 +0000)]
simplify has a brand new semantics!
replace_lifting passes a context to the comparison function
(but in the case Fix/CoFix is incomplete)

17 years agosubst tactic put in a file on its own
Ferruccio Guidi [Mon, 16 Apr 2007 15:28:27 +0000 (15:28 +0000)]
subst tactic put in a file on its own

17 years agoclosed all axioms
Enrico Tassi [Mon, 16 Apr 2007 08:33:28 +0000 (08:33 +0000)]
closed all axioms

17 years agoHACK for indtype checking
Enrico Tassi [Thu, 12 Apr 2007 12:11:11 +0000 (12:11 +0000)]
HACK for indtype checking

17 years agofixed case
Enrico Tassi [Tue, 10 Apr 2007 15:08:33 +0000 (15:08 +0000)]
fixed case

17 years agoset -> type
Enrico Tassi [Tue, 10 Apr 2007 14:32:28 +0000 (14:32 +0000)]
set -> type

17 years ago...
Enrico Tassi [Tue, 10 Apr 2007 14:32:01 +0000 (14:32 +0000)]
...

17 years ago...
Enrico Tassi [Tue, 10 Apr 2007 14:29:38 +0000 (14:29 +0000)]
...

17 years ago...
Enrico Tassi [Tue, 10 Apr 2007 14:29:04 +0000 (14:29 +0000)]
...

17 years agomatch x in IDENT and not TERM
Enrico Tassi [Tue, 10 Apr 2007 14:28:33 +0000 (14:28 +0000)]
match x in IDENT and not TERM

17 years agostill not completely working but at least non dumb destruct
Enrico Tassi [Tue, 10 Apr 2007 14:27:15 +0000 (14:27 +0000)]
still not completely working but at least non dumb destruct

17 years agoyou can case even if only a right appears... so, substituting them for metas is wrong...
Enrico Tassi [Tue, 10 Apr 2007 14:24:30 +0000 (14:24 +0000)]
you can case even if only a right appears... so, substituting them for metas is wrong, rels are better

17 years ago...
Enrico Tassi [Tue, 10 Apr 2007 14:23:02 +0000 (14:23 +0000)]
...

17 years agoeval_from_stream is now tail recursive!
Enrico Tassi [Fri, 6 Apr 2007 11:25:34 +0000 (11:25 +0000)]
eval_from_stream is now tail recursive!

17 years agopattern with match fixed
Enrico Tassi [Thu, 5 Apr 2007 13:18:15 +0000 (13:18 +0000)]
pattern with match fixed

17 years agomany printings added
Enrico Tassi [Thu, 5 Apr 2007 13:17:08 +0000 (13:17 +0000)]
many printings added

17 years agofixed the pretty (notation aware) printer
Enrico Tassi [Thu, 5 Apr 2007 13:15:51 +0000 (13:15 +0000)]
fixed the pretty (notation aware) printer

17 years agoalpha equivalence fixed: in the case "meta against meta" we did not recur on theexpli...
Ferruccio Guidi [Wed, 4 Apr 2007 15:01:50 +0000 (15:01 +0000)]
alpha equivalence fixed: in the case "meta against meta" we did not recur on theexplicit substitutions. The case "Type against Type" and "Implicit against Implicit" need to be checked. Are we really sure that structural equality is enough?
(when we compare universes and implict annotations)

17 years agoalpha equivalence test factorized and moved to CicUtil
Ferruccio Guidi [Wed, 4 Apr 2007 12:36:33 +0000 (12:36 +0000)]
alpha equivalence test factorized and moved to CicUtil

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