]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agocount_pattern implemented
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 13:53:46 +0000 (13:53 +0000)]
count_pattern implemented

19 years agoMore cases implemented in tactic_count.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 13:49:56 +0000 (13:49 +0000)]
More cases implemented in tactic_count.

19 years agoAn interesting test for replace.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 13:10:27 +0000 (13:10 +0000)]
An interesting test for replace.

19 years agoreplace tactic reimplemented.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 13:06:43 +0000 (13:06 +0000)]
replace tactic reimplemented.
It is now able to replace several terms at once.
NOTE: it is still unable to replace terms in the hypotheses.

19 years agopattern_of function reimplemented. Now it takes a term and a list of subterms
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 13:05:51 +0000 (13:05 +0000)]
pattern_of function reimplemented. Now it takes a term and a list of subterms
and it returns the _minimal_ pattern for the subterms in the term.

19 years agoprerr_endline -> debug_print
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 11:18:50 +0000 (11:18 +0000)]
prerr_endline -> debug_print

19 years agoSignature of fwdSimpl changed to get rid of a warning.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 11:18:42 +0000 (11:18 +0000)]
Signature of fwdSimpl changed to get rid of a warning.

19 years agoThe replace tactic is now working again. It can now replace simultaneously
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 11:13:34 +0000 (11:13 +0000)]
The replace tactic is now working again. It can now replace simultaneously
n terms.

19 years agoSignature of fwdSimpl changed to get rid of a warning.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 11:13:10 +0000 (11:13 +0000)]
Signature of fwdSimpl changed to get rid of a warning.

19 years agouri_of_string now checks the uri is well formed
Enrico Tassi [Fri, 1 Jul 2005 10:03:11 +0000 (10:03 +0000)]
uri_of_string now checks the uri is well formed

19 years agomatitaclean
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 09:39:24 +0000 (09:39 +0000)]
matitaclean

19 years agoNew syntax for patterns.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 09:38:55 +0000 (09:38 +0000)]
New syntax for patterns.

19 years ago1. change_tac moved from PrimitiveTactics to ReductionTactics
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 09:34:07 +0000 (09:34 +0000)]
1. change_tac moved from PrimitiveTactics to ReductionTactics
2. fold_tac reimplemented using change_tac

19 years agoNew test.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 09:33:55 +0000 (09:33 +0000)]
New test.

19 years ago\vdash added
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 09:33:16 +0000 (09:33 +0000)]
\vdash added

19 years agoSyntax of patterns changed again to make it non-ambiguous:
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 09:25:51 +0000 (09:25 +0000)]
Syntax of patterns changed again to make it non-ambiguous:
 [in match t] [in sequent_pattern]

19 years agoin case of performace improvement there is no performace loss message
Enrico Tassi [Fri, 1 Jul 2005 08:06:46 +0000 (08:06 +0000)]
in case of performace improvement there is no performace loss message

19 years agomatitaclean anapshot
Enrico Tassi [Thu, 30 Jun 2005 16:19:00 +0000 (16:19 +0000)]
matitaclean anapshot

19 years agoproofs are now built lazily at the end of the computation
Alberto Griggio [Thu, 30 Jun 2005 16:05:34 +0000 (16:05 +0000)]
proofs are now built lazily at the end of the computation

19 years ago...
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 14:56:12 +0000 (14:56 +0000)]
...

19 years agoSignature and concrete syntax of fold fixed.
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 14:52:17 +0000 (14:52 +0000)]
Signature and concrete syntax of fold fixed.

19 years agoThe pattern of a fold cannot have the "wanted" part (for the same reasons as
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 14:48:12 +0000 (14:48 +0000)]
The pattern of a fold cannot have the "wanted" part (for the same reasons as
rewrite)

19 years agoSignature and concrete syntax of fold fixed.
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 14:46:31 +0000 (14:46 +0000)]
Signature and concrete syntax of fold fixed.

19 years agolapply and fwd improved
Ferruccio Guidi [Thu, 30 Jun 2005 14:27:19 +0000 (14:27 +0000)]
lapply and fwd improved

19 years agoText fixed (due to stricter semantics for naming the binders in the patterns).
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 14:25:17 +0000 (14:25 +0000)]
Text fixed (due to stricter semantics for naming the binders in the patterns).

19 years agoThe rewrite_* set of tactics is now working again. However, as before,
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 14:20:20 +0000 (14:20 +0000)]
The rewrite_* set of tactics is now working again. However, as before,
they do not work yet when the user asks to rewrite somethign also in the
hypotheses.

19 years agoBug fixed: a wrong lift made select unuseful when wanted was an open term.
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 13:17:30 +0000 (13:17 +0000)]
Bug fixed: a wrong lift made select unuseful when wanted was an open term.

19 years agoPretty printing of Cic.Implict (Some `Hole) is now "%"
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 13:05:27 +0000 (13:05 +0000)]
Pretty printing of Cic.Implict (Some `Hole) is now "%"

19 years ago1. rewrite_* and rewrite_back_* merged into one function
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 12:31:24 +0000 (12:31 +0000)]
1. rewrite_* and rewrite_back_* merged into one function
2. signature of rewrite_* improved
3. concrete syntax for the rewrite direction fixed to ">" and "<"

NOTE: rewrite_* is still no longer working.

19 years ago1. rewrite_* and rewrite_back_* merged into one function
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 12:25:19 +0000 (12:25 +0000)]
1. rewrite_* and rewrite_back_* merged into one function
2. signature of rewrite_* improved
3. concrete syntax for the rewrite direction fixed to ">" and "<"

NOTE: rewrite_* is still no longer working.

19 years agoOooops. I forgot the convertibility test that makes the change tactic correct!
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 11:44:24 +0000 (11:44 +0000)]
Oooops. I forgot the convertibility test that makes the change tactic correct!

19 years agobaseuri put back
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 11:44:06 +0000 (11:44 +0000)]
baseuri put back

19 years agoThe tactic change is now working again. Moreover, it now receives a pattern
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 11:36:49 +0000 (11:36 +0000)]
The tactic change is now working again. Moreover, it now receives a pattern
in input; moreover it handles correctly the with_what argument when it must
be put in a context different from the one it was parsed in.

19 years agoA bit of renaming in the code to make it more clear.
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 11:35:30 +0000 (11:35 +0000)]
A bit of renaming in the code to make it more clear.

19 years ago...
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 10:34:59 +0000 (10:34 +0000)]
...

19 years agoA simpler implementation of inversion that does not generate the dummy
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 10:24:36 +0000 (10:24 +0000)]
A simpler implementation of inversion that does not generate the dummy
hypothesis Hcut: 0=0.

19 years agoburi_of_uri is now #xpointer aware.
Enrico Tassi [Thu, 30 Jun 2005 09:39:28 +0000 (09:39 +0000)]
buri_of_uri is now #xpointer aware.

19 years agoadded license stuff
Stefano Zacchiroli [Thu, 30 Jun 2005 09:36:02 +0000 (09:36 +0000)]
added license stuff

19 years agobetter handling of script names
Stefano Zacchiroli [Thu, 30 Jun 2005 09:32:45 +0000 (09:32 +0000)]
better handling of script names

19 years agoadded a debugging helper
Stefano Zacchiroli [Thu, 30 Jun 2005 09:32:28 +0000 (09:32 +0000)]
added a debugging helper

19 years agoObsolete comment removed.
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 09:07:35 +0000 (09:07 +0000)]
Obsolete comment removed.

19 years agoStupid bug fixed (a completely erroneous assert false removed).
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 08:48:22 +0000 (08:48 +0000)]
Stupid bug fixed (a completely erroneous assert false removed).

19 years agoThis commit makes ProofEngineHelpers.select reach its full potentials.
Claudio Sacerdoti Coen [Thu, 30 Jun 2005 08:44:39 +0000 (08:44 +0000)]
This commit makes ProofEngineHelpers.select reach its full potentials.
Its arguments are now a conjecture and a pattern and its output is
a conjecture-like structure made of physical pointers to matching subterms
(together with their contexts).

19 years agofirst matitadep snapshot
Enrico Tassi [Thu, 30 Jun 2005 07:54:34 +0000 (07:54 +0000)]
first matitadep snapshot

19 years ago1. new syntax for patterns:
Claudio Sacerdoti Coen [Wed, 29 Jun 2005 16:24:08 +0000 (16:24 +0000)]
1. new syntax for patterns:
    [t] [in p]
   where t is the term to be matched and p is the pattern on the hypotheses
   and on the conclusion (whose syntax is not changed).
   All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
   (that also have the optional term in them)
3. the signature of the select function has changed to require the context
   (and return a context and not a "context patch"); moreover it performs
   now both the search for roots and the search for subterms of the roots
   that are alpha-convertible with the optional given term (if any)

WARNING!!!
The following tactics have been commented out for a while:
 replace
 rewrite
 change
 fold

19 years ago1. new syntax for patterns:
Claudio Sacerdoti Coen [Wed, 29 Jun 2005 16:18:05 +0000 (16:18 +0000)]
1. new syntax for patterns:
    [t] [in p]
   where t is the term to be matched and p is the pattern on the hypotheses
   and on the conclusion (whose syntax is not changed).
   All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
   (that also have the optional term in them)
3. the signature of the select function has changed to require the context
   (and return a context and not a "context patch"); moreover it performs
   now both the search for roots and the search for subterms of the roots
   that are alpha-convertible with the optional given term (if any)

WARNING!!!
The following tactics have been commented out for a while:
 replace
 rewrite
 change
 fold

19 years agoremoved profiling function (now a stub is used instead)
Enrico Tassi [Wed, 29 Jun 2005 15:41:37 +0000 (15:41 +0000)]
removed profiling function (now a stub is used instead)
added a comment in urimanager

19 years agoIncredible bug of simpl fixed: the stack (in the terminology used for the
Claudio Sacerdoti Coen [Wed, 29 Jun 2005 15:17:19 +0000 (15:17 +0000)]
Incredible bug of simpl fixed: the stack (in the terminology used for the
Krivine's machine) was processed in the wrong context. As a result List.nth
(to get a Rel in the context) used to raise Failure in several cases. The
Failure, however, was catched somewhere in the code of matita and the
failure of simpl was hidden in most of the cases.

19 years agovarious updates, removed proofs for now because they are the real bottleneck!!
Alberto Griggio [Wed, 29 Jun 2005 15:08:20 +0000 (15:08 +0000)]
various updates, removed proofs for now because they are the real bottleneck!!

19 years agolapply reimplemented using letin_tac
Ferruccio Guidi [Wed, 29 Jun 2005 15:00:26 +0000 (15:00 +0000)]
lapply reimplemented using letin_tac

19 years agoA few bug fixes. In particular parsing errors in matitatop when a file is
Claudio Sacerdoti Coen [Wed, 29 Jun 2005 14:34:20 +0000 (14:34 +0000)]
A few bug fixes. In particular parsing errors in matitatop when a file is
given to process used to result in entering the ocaml mode. Now the user is
left in the matita mode.

19 years agofix
Enrico Tassi [Wed, 29 Jun 2005 14:26:38 +0000 (14:26 +0000)]
fix

19 years agonow baseuri is needed in each file (and its redefinition is forbidden)
Enrico Tassi [Wed, 29 Jun 2005 13:52:42 +0000 (13:52 +0000)]
now baseuri is needed in each file (and its redefinition is forbidden)
added exception prettyprinter

19 years agofixed some errers in the save/cancel ...
Enrico Tassi [Wed, 29 Jun 2005 13:08:02 +0000 (13:08 +0000)]
fixed some errers in the save/cancel ...

19 years agocatches more errors
Enrico Tassi [Wed, 29 Jun 2005 12:39:21 +0000 (12:39 +0000)]
catches more errors

19 years agodoes_not_occur unexported since it did not have the expected semantics
Claudio Sacerdoti Coen [Wed, 29 Jun 2005 11:55:15 +0000 (11:55 +0000)]
does_not_occur unexported since it did not have the expected semantics

19 years agofixed save/exit stuff
Enrico Tassi [Wed, 29 Jun 2005 11:50:10 +0000 (11:50 +0000)]
fixed save/exit stuff

19 years agofix
Enrico Tassi [Wed, 29 Jun 2005 09:01:54 +0000 (09:01 +0000)]
fix

19 years agothe error_report window is now properly closed
Enrico Tassi [Wed, 29 Jun 2005 09:01:30 +0000 (09:01 +0000)]
the error_report window is now properly closed

19 years agoRemoved a dummy "let ... in" that was there only to show a bug (now fixed).
Claudio Sacerdoti Coen [Wed, 29 Jun 2005 08:51:48 +0000 (08:51 +0000)]
Removed a dummy "let ... in" that was there only to show a bug (now fixed).

19 years agoStupid bug fixed in the refinement of let ... in
Claudio Sacerdoti Coen [Wed, 29 Jun 2005 08:46:40 +0000 (08:46 +0000)]
Stupid bug fixed in the refinement of let ... in

19 years agoInformative message corrected: MatitacLib.go () is now redefined as the more
Claudio Sacerdoti Coen [Wed, 29 Jun 2005 08:33:57 +0000 (08:33 +0000)]
Informative message corrected: MatitacLib.go () is now redefined as the more
concise go ().

19 years agofix
Enrico Tassi [Tue, 28 Jun 2005 17:41:17 +0000 (17:41 +0000)]
fix

19 years agobetter message
Enrico Tassi [Tue, 28 Jun 2005 17:41:04 +0000 (17:41 +0000)]
better message

19 years agolapply improved
Ferruccio Guidi [Tue, 28 Jun 2005 17:38:42 +0000 (17:38 +0000)]
lapply improved

19 years agomatitatop.ml is now a simple invocation of Toploop.loop and .ocamlinit is
Claudio Sacerdoti Coen [Tue, 28 Jun 2005 17:30:58 +0000 (17:30 +0000)]
matitatop.ml is now a simple invocation of Toploop.loop and .ocamlinit is
responsible to call MatitacLib.go or MatitacLib.main.

 Cons: .ocamlinit is more dirty
 Pros: it is possible to trace something even before doing a drop!

19 years agolapply improved
Ferruccio Guidi [Tue, 28 Jun 2005 17:23:03 +0000 (17:23 +0000)]
lapply improved

19 years agoNew solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
Claudio Sacerdoti Coen [Tue, 28 Jun 2005 17:15:02 +0000 (17:15 +0000)]
New solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
 Pro:  no need of doing the weird "#use matitatop.bootstrap" by playing with
       ocaml internals.
 Pro:  local definitions and #opens in matitatop.bootstrap were lost. They are
       preserved in .ocamlinit.
 Cons: .ocamlinit must be in "." or in $HOME
 Cons: it can interfere with other .ocamlinit

19 years agoIn case of EOI the "go ()" loop must exit!
Claudio Sacerdoti Coen [Tue, 28 Jun 2005 17:11:17 +0000 (17:11 +0000)]
In case of EOI the "go ()" loop must exit!

19 years agomatitatop
Claudio Sacerdoti Coen [Tue, 28 Jun 2005 16:12:29 +0000 (16:12 +0000)]
matitatop

19 years agoMore complete bootstrapper.
Claudio Sacerdoti Coen [Tue, 28 Jun 2005 16:12:15 +0000 (16:12 +0000)]
More complete bootstrapper.

19 years ago* new binary matitatop
Enrico Tassi [Tue, 28 Jun 2005 15:50:22 +0000 (15:50 +0000)]
* new binary matitatop
* command drop enabled for matitatop.
  Once dropped use MatitacLib.go () to enter again the matita toplevel.
  Use #trace and similar stuff for debugging.
  Add printers for abstract data types in matitatop.bootstrap

  Enjoy!

19 years agoadded Drop
Enrico Tassi [Tue, 28 Jun 2005 15:48:19 +0000 (15:48 +0000)]
added Drop

19 years agomisc -> domMisc
Enrico Tassi [Tue, 28 Jun 2005 15:48:01 +0000 (15:48 +0000)]
misc -> domMisc

19 years agofixed bug in response first line parsing (arbitrary reason phrases are
Stefano Zacchiroli [Tue, 28 Jun 2005 12:57:57 +0000 (12:57 +0000)]
fixed bug in response first line parsing (arbitrary reason phrases are
now supported)

19 years agoadded "are you sure you want to quit with usaved script?"
Enrico Tassi [Tue, 28 Jun 2005 10:58:10 +0000 (10:58 +0000)]
added "are you sure you want to quit with usaved script?"

19 years agoNew argument for LApply: the ident for the generated hypothesis.
Claudio Sacerdoti Coen [Tue, 28 Jun 2005 09:16:54 +0000 (09:16 +0000)]
New argument for LApply: the ident for the generated hypothesis.

19 years agoNew argument for LApply: the ident for the generated hypothesis.
Claudio Sacerdoti Coen [Tue, 28 Jun 2005 09:11:19 +0000 (09:11 +0000)]
New argument for LApply: the ident for the generated hypothesis.

19 years agochanged get_pair interface, now supports different unmarshallers
Stefano Zacchiroli [Tue, 28 Jun 2005 08:22:38 +0000 (08:22 +0000)]
changed get_pair interface, now supports different unmarshallers

19 years agoadded get_pair method
Stefano Zacchiroli [Tue, 28 Jun 2005 08:19:36 +0000 (08:19 +0000)]
added get_pair method

19 years agomoved discovery of METAS dir to configure.ac: script.sh no longer needed
Stefano Zacchiroli [Tue, 28 Jun 2005 08:13:26 +0000 (08:13 +0000)]
moved discovery of METAS dir to configure.ac: script.sh no longer needed
when invoking make in subdirectories of ocaml/

19 years agobugfix: uses awk instead of cut for splitting query output (no more empty string)
Stefano Zacchiroli [Tue, 28 Jun 2005 07:56:57 +0000 (07:56 +0000)]
bugfix: uses awk instead of cut for splitting query output (no more empty string)

19 years agoNew tactics.
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 17:12:36 +0000 (17:12 +0000)]
New tactics.

19 years agoreplace generalized to patterns
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 17:09:16 +0000 (17:09 +0000)]
replace generalized to patterns

19 years ago1. interface of replace generalized to patterns
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 17:03:38 +0000 (17:03 +0000)]
1. interface of replace generalized to patterns
2. implementation commented out (for a little while)

19 years agoA few other tactics made available to matita.
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 17:00:44 +0000 (17:00 +0000)]
A few other tactics made available to matita.
A few tactics (change, fold, replace) generalized to patterns.
The argument of clear and clearbody is now an identifier.

19 years agoA few other tactics made available to matita.
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 16:57:10 +0000 (16:57 +0000)]
A few other tactics made available to matita.
A few tactics (change, fold, replace) generalized to patterns.
The argument of clear and clearbody is now an identifier.

WARNING: the implementation of change, fold and replace has been commented
out to generalize them to patterns. To be committed soon.

19 years agoclear already exists
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 16:42:14 +0000 (16:42 +0000)]
clear already exists

19 years agoadded autosave and * (modified feature)
Enrico Tassi [Mon, 27 Jun 2005 15:32:48 +0000 (15:32 +0000)]
added autosave and * (modified feature)

19 years ago...
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 13:58:29 +0000 (13:58 +0000)]
...

19 years agoNew argument (the identifier) to generalize.
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 13:51:05 +0000 (13:51 +0000)]
New argument (the identifier) to generalize.

19 years agoNew argument (the identifier) to generalize.
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 13:45:59 +0000 (13:45 +0000)]
New argument (the identifier) to generalize.

19 years agoNew argument (the hypothesis name) for cut.
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 13:45:36 +0000 (13:45 +0000)]
New argument (the hypothesis name) for cut.

19 years agoNew syntax of auto: auto [depth = n] [width = m].
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 13:43:55 +0000 (13:43 +0000)]
New syntax of auto: auto [depth = n] [width = m].

19 years ago...
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 13:29:45 +0000 (13:29 +0000)]
...

19 years agofized disambiguation of LApply
Enrico Tassi [Mon, 27 Jun 2005 13:12:28 +0000 (13:12 +0000)]
fized disambiguation of LApply

19 years ago* the auto AST now has the width
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 12:30:45 +0000 (12:30 +0000)]
* the auto AST now has the width
* a bit of code clean-up
* more tactics made available to matita

19 years agosupport for _ in binders, and a more coplex pattern that should help if
Enrico Tassi [Mon, 27 Jun 2005 12:24:32 +0000 (12:24 +0000)]
support for _ in binders, and a more coplex pattern that should help if
patterns will be used on subterms.
match pattern, term with
| Binder Anonymous, Binder name -> recursion
| Binder name1, Binder name2 when name1 = name2 -> recursion
| Binder name1, Binder name2 -> []

19 years agoMore tactics or tactic arguments made available to matita and a bit of code
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 12:24:31 +0000 (12:24 +0000)]
More tactics or tactic arguments made available to matita and a bit of code
cleanup.

19 years ago* auto_tac removed (it can be found in CVS)
Claudio Sacerdoti Coen [Mon, 27 Jun 2005 12:24:13 +0000 (12:24 +0000)]
* auto_tac removed (it can be found in CVS)
* auto_tac_new renamed to auto_tac
* TacticAst.Auto ported to auto_tac[_new] (i.e. width added)
* MetadataQuery.hint removed (only {new_,}experimental_hint were used)