]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agopretty printing of URIs
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 14:01:21 +0000 (14:01 +0000)]
pretty printing of URIs

19 years agoaded confirmation dialog for baseuri redefinement
Enrico Tassi [Mon, 4 Jul 2005 13:43:05 +0000 (13:43 +0000)]
aded confirmation dialog for baseuri redefinement

19 years agomoo do not depend on .depend
Enrico Tassi [Mon, 4 Jul 2005 13:33:19 +0000 (13:33 +0000)]
moo do not depend on .depend

19 years agocenter on parent now works for ask_confirmation dialog
Enrico Tassi [Mon, 4 Jul 2005 12:33:50 +0000 (12:33 +0000)]
center on parent now works for ask_confirmation dialog

19 years agoAll the tactics have been ported to use the objects in LibraryObjects.
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 12:30:36 +0000 (12:30 +0000)]
All the tactics have been ported to use the objects in LibraryObjects.

19 years agoinclude
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 12:21:00 +0000 (12:21 +0000)]
include

19 years agoComestic changes.
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 12:20:38 +0000 (12:20 +0000)]
Comestic changes.

19 years agocoercions are now stored in the .moo file.
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 12:17:23 +0000 (12:17 +0000)]
coercions are now stored in the .moo file.

19 years agoCosmetic changes.
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 12:16:11 +0000 (12:16 +0000)]
Cosmetic changes.

19 years agoNew function (only partially implemented) to pretty print an Ast at the
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 12:10:00 +0000 (12:10 +0000)]
New function (only partially implemented) to pretty print an Ast at the
semantics level.

19 years agoadded some utility functions on filename suffixes
Stefano Zacchiroli [Mon, 4 Jul 2005 12:08:55 +0000 (12:08 +0000)]
added some utility functions on filename suffixes

19 years agoUse eval_from_stream in place of eval_from_stream_ref to avoid printing the
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 11:59:55 +0000 (11:59 +0000)]
Use eval_from_stream in place of eval_from_stream_ref to avoid printing the
prompt.

19 years agoinclude must not add aliases in the script!
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 11:55:48 +0000 (11:55 +0000)]
include must not add aliases in the script!

19 years ago"include" command implemented.
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 10:45:52 +0000 (10:45 +0000)]
"include" command implemented.

19 years ago"include" command implemented.
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 10:38:32 +0000 (10:38 +0000)]
"include" command implemented.

19 years agomatitaclean splitted in matitacleanLib and matitaclean.
Enrico Tassi [Mon, 4 Jul 2005 09:59:57 +0000 (09:59 +0000)]
matitaclean splitted in matitacleanLib and matitaclean.

19 years agoalias declarations are now put in the .moo file.
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 08:57:07 +0000 (08:57 +0000)]
alias declarations are now put in the .moo file.

19 years agomatitaclean now call getter.ls using a buri with a trailing /
Enrico Tassi [Mon, 4 Jul 2005 08:49:24 +0000 (08:49 +0000)]
matitaclean now call getter.ls using a buri with a trailing /

19 years agoImprovements in matitatop: instead of doing exit -1 it enters the toploop
Claudio Sacerdoti Coen [Mon, 4 Jul 2005 07:40:28 +0000 (07:40 +0000)]
Improvements in matitatop: instead of doing exit -1 it enters the toploop
after a ^C.

19 years agoEquality tactics are now used in the first half of the script.
Claudio Sacerdoti Coen [Sun, 3 Jul 2005 14:47:59 +0000 (14:47 +0000)]
Equality tactics are now used in the first half of the script.

Note: it seems that "elim H ?" is more powerful than "rewrite < H ?" since
it is able to discover the value of the implicit argument ?. To be improved.

19 years agoThe equality tactics are now exploited.
Claudio Sacerdoti Coen [Sat, 2 Jul 2005 14:50:11 +0000 (14:50 +0000)]
The equality tactics are now exploited.

19 years agoAll the equalityTactics have now been ported to use both the equality of
Claudio Sacerdoti Coen [Sat, 2 Jul 2005 14:42:46 +0000 (14:42 +0000)]
All the equalityTactics have now been ported to use both the equality of
Coq and that of Matita.

Note: the only problematic tactic is replace that must pick an equality without
any hint. Right now it always picks the one of matita.

19 years agoNew theorem: eq_ind_r.
Claudio Sacerdoti Coen [Sat, 2 Jul 2005 13:59:16 +0000 (13:59 +0000)]
New theorem: eq_ind_r.

19 years agocosmetic change: a space removed (to make tests/Makefile and library/Makefile
Claudio Sacerdoti Coen [Sat, 2 Jul 2005 13:49:22 +0000 (13:49 +0000)]
cosmetic change: a space removed (to make tests/Makefile and library/Makefile
the same)

19 years agofixed bug in proof generation, new weight function to sort equalities, which
Alberto Griggio [Fri, 1 Jul 2005 19:08:05 +0000 (19:08 +0000)]
fixed bug in proof generation, new weight function to sort equalities, which
gives a huge speedup

19 years agomay fix the nigtly build
Enrico Tassi [Fri, 1 Jul 2005 18:57:48 +0000 (18:57 +0000)]
may fix the nigtly build

19 years agomore makefile work
Enrico Tassi [Fri, 1 Jul 2005 17:59:48 +0000 (17:59 +0000)]
more makefile work

19 years agomake tests and make tests.opt now call their counterparts in library and tests
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 17:39:20 +0000 (17:39 +0000)]
make tests and make tests.opt now call their counterparts in library and tests

19 years agoThe tests are now in alphabetical order.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 17:38:35 +0000 (17:38 +0000)]
The tests are now in alphabetical order.

19 years agomatch.ma removed
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 17:31:33 +0000 (17:31 +0000)]
match.ma removed

19 years ago* match.ma removed (it is now splitted in several files in library/*.ma)
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 17:21:13 +0000 (17:21 +0000)]
* match.ma removed (it is now splitted in several files in library/*.ma)
* Makefile.tests removed (redundant with tests/Makefile)
* make tests and make tests.opt now call the same targets in library and tests

19 years ago...
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 17:16:00 +0000 (17:16 +0000)]
...

19 years agoconflicting baseuri
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 17:14:39 +0000 (17:14 +0000)]
conflicting baseuri

19 years agomatitaclean is necessary!
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 17:05:23 +0000 (17:05 +0000)]
matitaclean is necessary!
However, we need a fast ls method for this. Waiting for Zack's new getter...

19 years ago...
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 17:00:00 +0000 (17:00 +0000)]
...

19 years ago* makefile improved
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:47:33 +0000 (16:47 +0000)]
* makefile improved
* new target-schema: *.opt

19 years agonew targets:
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:40:54 +0000 (16:40 +0000)]
new targets:
  opt
  verbose.opt

19 years ago...
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:29:19 +0000 (16:29 +0000)]
...

19 years agoNew argument: the cleaner.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:27:37 +0000 (16:27 +0000)]
New argument: the cleaner.

19 years agomake all is now nicer
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:24:15 +0000 (16:24 +0000)]
make all is now nicer

19 years agoTwo targets now:
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:22:42 +0000 (16:22 +0000)]
Two targets now:
 make all
 make verbose

19 years agomake MATITAC="../scripts/do_tests.sh ../matitac /dev/null"
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:16:15 +0000 (16:16 +0000)]
make MATITAC="../scripts/do_tests.sh ../matitac /dev/null"
can now be used to benchmark the output

19 years ago...
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:01:12 +0000 (16:01 +0000)]
...

19 years agoMakefile improved
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 16:00:53 +0000 (16:00 +0000)]
Makefile improved

19 years agoThe library of matita is borned! Long life to the library of matita.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 15:43:43 +0000 (15:43 +0000)]
The library of matita is borned! Long life to the library of matita.

19 years agoma -> moo in dependencies
Enrico Tassi [Fri, 1 Jul 2005 15:01:38 +0000 (15:01 +0000)]
ma -> moo in dependencies

19 years agomore logging information on received request
Stefano Zacchiroli [Fri, 1 Jul 2005 14:57:18 +0000 (14:57 +0000)]
more logging information on received request

19 years agouses relative OCAMLPATH
Stefano Zacchiroli [Fri, 1 Jul 2005 14:56:59 +0000 (14:56 +0000)]
uses relative OCAMLPATH

19 years agonow maketests uses matitaclean (but not in the right way)
Enrico Tassi [Fri, 1 Jul 2005 14:55:19 +0000 (14:55 +0000)]
now maketests uses matitaclean (but not in the right way)
tests are made in the stupid order, not in the needed one

19 years agofirst snapshot of separate compilation
Enrico Tassi [Fri, 1 Jul 2005 14:40:19 +0000 (14:40 +0000)]
first snapshot of separate compilation

19 years agoon is now a keyword (needed in let rec)
Enrico Tassi [Fri, 1 Jul 2005 14:38:10 +0000 (14:38 +0000)]
on is now a keyword (needed in let rec)

19 years agoadded uri_is_ind
Enrico Tassi [Fri, 1 Jul 2005 14:37:39 +0000 (14:37 +0000)]
added uri_is_ind

19 years agomatitaclean.opt, matitadep.opt
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 14:33:39 +0000 (14:33 +0000)]
matitaclean.opt, matitadep.opt

19 years agoremoved first Cic.term from type equality, added an int (weight of the equality)
Alberto Griggio [Fri, 1 Jul 2005 14:28:02 +0000 (14:28 +0000)]
removed first Cic.term from type equality, added an int (weight of the equality)

19 years ago...
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 14:27:50 +0000 (14:27 +0000)]
...

19 years agoTacticAst2Box no longer used.
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 14:20:45 +0000 (14:20 +0000)]
TacticAst2Box no longer used.

19 years agoModule TacticAst2Box unused!
Claudio Sacerdoti Coen [Fri, 1 Jul 2005 14:18:51 +0000 (14:18 +0000)]
Module TacticAst2Box unused!

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).