]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agogetter's revolution (now uses backend in ocaml/getter)
Stefano Zacchiroli [Wed, 11 Feb 2004 17:17:26 +0000 (17:17 +0000)]
getter's revolution (now uses backend in ocaml/getter)

20 years agoPorted to Helm_registry.
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 17:05:27 +0000 (17:05 +0000)]
Ported to Helm_registry.

20 years agobugfix: auto_disambiguation is not considered for searchPatternApply
Stefano Zacchiroli [Wed, 11 Feb 2004 16:02:18 +0000 (16:02 +0000)]
bugfix: auto_disambiguation is not considered for searchPatternApply

20 years ago- script.sh removed from CVS. script.sh.sample added isntead
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 12:17:35 +0000 (12:17 +0000)]
- script.sh removed from CVS. script.sh.sample added isntead
- triciclo.conf.xml.sample added

20 years agofixed typo
Stefano Zacchiroli [Wed, 11 Feb 2004 12:09:30 +0000 (12:09 +0000)]
fixed typo

20 years agonew logger
Stefano Zacchiroli [Wed, 11 Feb 2004 12:04:16 +0000 (12:04 +0000)]
new logger

20 years agonew getter, logger, and the hell
Stefano Zacchiroli [Wed, 11 Feb 2004 12:03:40 +0000 (12:03 +0000)]
new getter, logger, and the hell

20 years agonew logger, getter, and the hell
Stefano Zacchiroli [Wed, 11 Feb 2004 12:03:07 +0000 (12:03 +0000)]
new logger, getter, and the hell

20 years agosupport for subst
Stefano Zacchiroli [Wed, 11 Feb 2004 12:02:46 +0000 (12:02 +0000)]
support for subst

20 years agonew metas (getter's backend, registry, logger, and the hell)
Stefano Zacchiroli [Wed, 11 Feb 2004 12:02:23 +0000 (12:02 +0000)]
new metas (getter's backend, registry, logger, and the hell)

20 years agoported to new getter (backend)
Stefano Zacchiroli [Wed, 11 Feb 2004 12:01:56 +0000 (12:01 +0000)]
ported to new getter (backend)

20 years agoported to helm registry
Stefano Zacchiroli [Wed, 11 Feb 2004 12:01:08 +0000 (12:01 +0000)]
ported to helm registry

20 years agoported to new logger
Stefano Zacchiroli [Wed, 11 Feb 2004 12:00:51 +0000 (12:00 +0000)]
ported to new logger

20 years agouse debug_print in a debugging message
Stefano Zacchiroli [Wed, 11 Feb 2004 11:57:37 +0000 (11:57 +0000)]
use debug_print in a debugging message

20 years ago- getter revolution: split backend and frontend (this is the backend)
Stefano Zacchiroli [Wed, 11 Feb 2004 11:57:00 +0000 (11:57 +0000)]
- getter revolution: split backend and frontend (this is the backend)
- working remote part but not yet the local one (extra unneeded headers)

20 years ago- split away gtk logger
Stefano Zacchiroli [Wed, 11 Feb 2004 11:56:15 +0000 (11:56 +0000)]
- split away gtk logger
- renamed module to HelmLogger

20 years agoadded some debugging messages
Stefano Zacchiroli [Wed, 11 Feb 2004 11:55:42 +0000 (11:55 +0000)]
added some debugging messages

20 years agoA type checking error report now prints also the metasenv.
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 11:23:05 +0000 (11:23 +0000)]
A type checking error report now prints also the metasenv.

20 years agoadded target *.opt (e.g. test.opt, librarytest.opt, etc.)
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 11:14:18 +0000 (11:14 +0000)]
added target *.opt (e.g. test.opt, librarytest.opt, etc.)

20 years ago- make *opt fixed
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 11:11:49 +0000 (11:11 +0000)]
- make *opt fixed
- added -vars -varsprefix cic:/Coq to testlibrary

20 years agoBig changes:
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 10:35:52 +0000 (10:35 +0000)]
Big changes:
  1. every level now catches the *Failure excecptions of the lower level
     and converts it to its own *Failure. The same for *Uncertain.
  2. CicMetaSubst.delift now raises also Uncertain (that is converted
     to CicUnification.Uncertain and then to CicRefine.Uncertain).

20 years agoAdded copyright notice.
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 10:33:22 +0000 (10:33 +0000)]
Added copyright notice.

20 years agoExplicit Named Substitutions now supported.
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 15:25:49 +0000 (15:25 +0000)]
Explicit Named Substitutions now supported.

20 years agoCicCache ==> CicEnvironment (in testlibrary.ml)
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 14:07:21 +0000 (14:07 +0000)]
CicCache ==> CicEnvironment (in testlibrary.ml)

20 years ago- fixed final log reporting (that was broken by one of the previous commits)
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 14:06:51 +0000 (14:06 +0000)]
- fixed final log reporting (that was broken by one of the previous commits)
- CicCache ==> CicEnvironment

20 years agoBug fixed: when an axiom was asked, an exception was raised (since the
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 14:03:33 +0000 (14:03 +0000)]
Bug fixed: when an axiom was asked, an exception was raised (since the
check for an existent body was skipped).

20 years agopatched
Ferruccio Guidi [Tue, 10 Feb 2004 13:03:23 +0000 (13:03 +0000)]
patched

20 years agoOnly applications whose head was a constant were eta-fixed.
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 12:11:36 +0000 (12:11 +0000)]
Only applications whose head was a constant were eta-fixed.
Result: sometimes the generated term was no longer well-typed.
The fix consists in calling the type-checker on the head of the
applications. Slower, but more reliable.

20 years agoBug fixed: checking inductive type declarations with left parameters (e.g.
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 12:07:08 +0000 (12:07 +0000)]
Bug fixed: checking inductive type declarations with left parameters (e.g.
le) lead to mistakes due to debrujin/undebrujin: terms to be debrujined must
be closed and then left parameters can not be removed _before_ calling
debrujin_constructor.

20 years agoadded "'" as a valid (continuation) identifier character
Stefano Zacchiroli [Tue, 10 Feb 2004 09:04:35 +0000 (09:04 +0000)]
added "'" as a valid (continuation) identifier character

20 years agoAdded flag ?eta_fix:bool to acic_object_of_cic_object.
Claudio Sacerdoti Coen [Mon, 9 Feb 2004 18:43:38 +0000 (18:43 +0000)]
Added flag ?eta_fix:bool to acic_object_of_cic_object.

20 years agoadded thread entry
Stefano Zacchiroli [Mon, 9 Feb 2004 17:05:59 +0000 (17:05 +0000)]
added thread entry

20 years agoadded netstring and pxp deps
Stefano Zacchiroli [Mon, 9 Feb 2004 17:05:44 +0000 (17:05 +0000)]
added netstring and pxp deps

20 years agohelm-thread's META
Stefano Zacchiroli [Mon, 9 Feb 2004 17:05:16 +0000 (17:05 +0000)]
helm-thread's META

20 years agothread library (actually contains just ThreadSafe module)
Stefano Zacchiroli [Mon, 9 Feb 2004 17:04:36 +0000 (17:04 +0000)]
thread library (actually contains just ThreadSafe module)

20 years ago- added environment variable overriding
Stefano Zacchiroli [Mon, 9 Feb 2004 17:03:56 +0000 (17:03 +0000)]
- added environment variable overriding
- XML syntax for configuration file

20 years agosort_of_prod now thinks that a "sort metavariable" is a metavariable where
Claudio Sacerdoti Coen [Mon, 9 Feb 2004 16:40:29 +0000 (16:40 +0000)]
sort_of_prod now thinks that a "sort metavariable" is a metavariable where
no free variable occurs in the local context. Reason: there used to be a bug
induced by the fact that a metavariable ?1 with an empty canonical context
could be istantiated with a metavariable ?2[l] where l has no free variables
but still it is not of length 0.

20 years agoAdded is_closed.
Claudio Sacerdoti Coen [Mon, 9 Feb 2004 16:37:16 +0000 (16:37 +0000)]
Added is_closed.

20 years agosplit into two major parts:
Stefano Zacchiroli [Mon, 9 Feb 2004 13:22:00 +0000 (13:22 +0000)]
split into two major parts:
- backend (ocaml API)
- frontend (web service)

20 years agobumped version (tag soon)
Stefano Zacchiroli [Mon, 9 Feb 2004 13:18:48 +0000 (13:18 +0000)]
bumped version (tag soon)

20 years agono longer use marshalled table for unicode macros
Stefano Zacchiroli [Mon, 9 Feb 2004 09:42:15 +0000 (09:42 +0000)]
no longer use marshalled table for unicode macros

20 years agouse CicAstPp
Stefano Zacchiroli [Mon, 9 Feb 2004 09:42:02 +0000 (09:42 +0000)]
use CicAstPp

20 years agoeat_prods now uses mk_implicit_type.
Claudio Sacerdoti Coen [Mon, 9 Feb 2004 09:27:25 +0000 (09:27 +0000)]
eat_prods now uses mk_implicit_type.

20 years ago- Added mk_implicit_sort.
Claudio Sacerdoti Coen [Sat, 7 Feb 2004 18:03:36 +0000 (18:03 +0000)]
- Added mk_implicit_sort.
- Used in CicRefine.sort_of_prod.

20 years agoAdded mk_implicit_sort.
Claudio Sacerdoti Coen [Sat, 7 Feb 2004 18:01:53 +0000 (18:01 +0000)]
Added mk_implicit_sort.

20 years agoA better (but yet not empty) metasenv is now returned.
Claudio Sacerdoti Coen [Sat, 7 Feb 2004 17:58:39 +0000 (17:58 +0000)]
A better (but yet not empty) metasenv is now returned.

20 years agosort_of_prod: the second term, when it is a meta, was unified with a fresh
Claudio Sacerdoti Coen [Sat, 7 Feb 2004 17:52:01 +0000 (17:52 +0000)]
sort_of_prod: the second term, when it is a meta, was unified with a fresh
meta in a wrong context. Fixed.

20 years ago- added options "-vars" and "-varsprefix"
Stefano Zacchiroli [Sat, 7 Feb 2004 10:33:09 +0000 (10:33 +0000)]
- added options "-vars" and "-varsprefix"
- ported testlibrary to Arg module

20 years agochanged deps since testlibrary now uses (minimally) BatchParser
Stefano Zacchiroli [Sat, 7 Feb 2004 10:32:38 +0000 (10:32 +0000)]
changed deps since testlibrary now uses (minimally) BatchParser

20 years agorebuilt
Stefano Zacchiroli [Sat, 7 Feb 2004 10:32:16 +0000 (10:32 +0000)]
rebuilt

20 years agosort metavariables are now generated in an empty canonical context.
Claudio Sacerdoti Coen [Fri, 6 Feb 2004 18:06:28 +0000 (18:06 +0000)]
sort metavariables are now generated in an empty canonical context.

20 years agoadded annotations to Cic.Implicit
Stefano Zacchiroli [Fri, 6 Feb 2004 17:16:20 +0000 (17:16 +0000)]
added annotations to Cic.Implicit

20 years agouse ledit for debugging
Stefano Zacchiroli [Fri, 6 Feb 2004 17:11:59 +0000 (17:11 +0000)]
use ledit for debugging

20 years agoComments (notes) removed.
Claudio Sacerdoti Coen [Fri, 6 Feb 2004 14:34:20 +0000 (14:34 +0000)]
Comments (notes) removed.

20 years agoCode riorganization.
Claudio Sacerdoti Coen [Fri, 6 Feb 2004 14:27:47 +0000 (14:27 +0000)]
Code riorganization.

20 years agoadded Format-library-friendly pretty printers defined on top of the
Stefano Zacchiroli [Fri, 6 Feb 2004 12:31:27 +0000 (12:31 +0000)]
added Format-library-friendly pretty printers defined on top of the
previous ones (still exported)

20 years agoadded -g flag to ocamlc per default
Stefano Zacchiroli [Fri, 6 Feb 2004 12:29:30 +0000 (12:29 +0000)]
added -g flag to ocamlc per default

20 years agotextual term editor is now the default one
Stefano Zacchiroli [Fri, 6 Feb 2004 12:28:58 +0000 (12:28 +0000)]
textual term editor is now the default one

20 years agoignore .debug_script (used by Makefile's debug target)
Stefano Zacchiroli [Fri, 6 Feb 2004 12:25:11 +0000 (12:25 +0000)]
ignore .debug_script (used by Makefile's debug target)

20 years ago- split regtest/testlibrary/gTopLevel objects so that the first two
Stefano Zacchiroli [Fri, 6 Feb 2004 12:24:38 +0000 (12:24 +0000)]
- split regtest/testlibrary/gTopLevel objects so that the first two
  aren't linked in thread mode
- added debug target to debug with wowcamldebug executables
- link with -g per default in bytecode mode

20 years agoBug MutCase fixed: now the type of the constructor only eats the
Andrea Asperti [Fri, 6 Feb 2004 10:25:04 +0000 (10:25 +0000)]
Bug MutCase fixed: now the type of the constructor only eats the
left params.

20 years agoadded testlibrary.opt and some cm****
Stefano Zacchiroli [Fri, 6 Feb 2004 09:19:49 +0000 (09:19 +0000)]
added testlibrary.opt and some cm****

20 years agoNameExpected exception removed. The "identifier" __n is now returned
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 18:30:57 +0000 (18:30 +0000)]
NameExpected exception removed. The "identifier" __n is now returned
(as CicPp does).

20 years agoImproved error messages.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 18:21:36 +0000 (18:21 +0000)]
Improved error messages.

20 years agoNo more garbage in the metasenv.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 18:18:52 +0000 (18:18 +0000)]
No more garbage in the metasenv.

20 years agoNew target librarytest (to apply testlibrary.opt to index.txt). The output
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 18:15:45 +0000 (18:15 +0000)]
New target librarytest (to apply testlibrary.opt to index.txt). The output
is in LOG.

20 years ago- added support for multiple choices
Stefano Zacchiroli [Thu, 5 Feb 2004 17:59:39 +0000 (17:59 +0000)]
- added support for multiple choices
- added pping of toplevel exceptions

20 years agobetter output format
Stefano Zacchiroli [Thu, 5 Feb 2004 17:47:07 +0000 (17:47 +0000)]
better output format

20 years agoflush stdout after print_string
Stefano Zacchiroli [Thu, 5 Feb 2004 17:46:21 +0000 (17:46 +0000)]
flush stdout after print_string

20 years agodebug prints on stderr
Stefano Zacchiroli [Thu, 5 Feb 2004 17:45:48 +0000 (17:45 +0000)]
debug prints on stderr

20 years agoremoved duplicated entry about freshNamesGenerator
Stefano Zacchiroli [Thu, 5 Feb 2004 17:28:52 +0000 (17:28 +0000)]
removed duplicated entry about freshNamesGenerator

20 years ago- added testlibrary .opts
Stefano Zacchiroli [Thu, 5 Feb 2004 17:22:54 +0000 (17:22 +0000)]
- added testlibrary .opts
- build just gTopLevel per default

20 years agoadded \to notation for anonymous binders Pi and Lambda
Stefano Zacchiroli [Thu, 5 Feb 2004 17:18:25 +0000 (17:18 +0000)]
added \to notation for anonymous binders Pi and Lambda

20 years agobugfix: use rev_uniq also on non-located term
Stefano Zacchiroli [Thu, 5 Feb 2004 17:17:57 +0000 (17:17 +0000)]
bugfix: use rev_uniq also on non-located term

20 years agosort_of_prod relaxed to accept also Metas (when the second Meta has an
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 16:43:15 +0000 (16:43 +0000)]
sort_of_prod relaxed to accept also Metas (when the second Meta has an
empty context). In this case the second Meta is returned.

20 years ago- sort_of_prod now returns the second Meta (if it is a Meta) after
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 16:41:42 +0000 (16:41 +0000)]
- sort_of_prod now returns the second Meta (if it is a Meta) after
  unifying it with a fresh Meta whose context is empty
- the name generated by eat_prods where not always fresh. Fixed.

20 years agoadded html_of_html_msg
Stefano Zacchiroli [Thu, 5 Feb 2004 15:20:47 +0000 (15:20 +0000)]
added html_of_html_msg

20 years ago__n no longer generated.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 14:40:03 +0000 (14:40 +0000)]
__n no longer generated.

20 years ago"assert false" relaxed to a warning.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 14:38:56 +0000 (14:38 +0000)]
"assert false" relaxed to a warning.
The problem raises when a non-dependent type is found and there IS a Rel
to it. It used to be an assert false (that failed). It is now relaxed
to a Cic.Anonymous (plus a warning on stderr).

20 years agoNo longer puts anonymous declarations in the canonical contexts during
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 14:37:14 +0000 (14:37 +0000)]
No longer puts anonymous declarations in the canonical contexts during
eat_prods.

20 years ago- the result of a refinement is now cleared from dummy dependent types
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 14:11:01 +0000 (14:11 +0000)]
- the result of a refinement is now cleared from dummy dependent types
  and letins
- freshNameGenerator: bug fixed

20 years agofreshNameGenerator.ml* added
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 14:09:28 +0000 (14:09 +0000)]
freshNameGenerator.ml* added

20 years agorebuilt
Stefano Zacchiroli [Thu, 5 Feb 2004 13:32:25 +0000 (13:32 +0000)]
rebuilt

20 years agoadded freshNameGenerator
Stefano Zacchiroli [Thu, 5 Feb 2004 13:31:31 +0000 (13:31 +0000)]
added freshNameGenerator

20 years agoadded testlibrary script
Stefano Zacchiroli [Thu, 5 Feb 2004 13:30:40 +0000 (13:30 +0000)]
added testlibrary script

20 years agouse a dummy location when no location is provided
Stefano Zacchiroli [Thu, 5 Feb 2004 13:29:56 +0000 (13:29 +0000)]
use a dummy location when no location is provided

20 years agoadded ( ) notation for binders
Stefano Zacchiroli [Thu, 5 Feb 2004 13:29:41 +0000 (13:29 +0000)]
added ( ) notation for binders

20 years agodummy dependent types and dummy letins are now removed from the refined
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 12:29:49 +0000 (12:29 +0000)]
dummy dependent types and dummy letins are now removed from the refined
term.

20 years agofresh_name_generator has now also the metasenv parameter.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 11:54:14 +0000 (11:54 +0000)]
fresh_name_generator has now also the metasenv parameter.
Before this patch it used the empty metasenv (and it worked, somehow!)

20 years agomk_fresh_name moved to FreshNamesGenerator.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 11:33:09 +0000 (11:33 +0000)]
mk_fresh_name moved to FreshNamesGenerator.

20 years agoNew test.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 11:07:02 +0000 (11:07 +0000)]
New test.

20 years agoFinal answer: the local context MUST be normalized w.r.t. the canonical
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 11:04:43 +0000 (11:04 +0000)]
Final answer: the local context MUST be normalized w.r.t. the canonical
context before delifting w.r.t. it. Reason: we normalize it only lazily and
this is a right place to ``force'' the normalization.

20 years agoRestrict reimplemented to avoid generating lists of indexes to be restricted
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 10:59:11 +0000 (10:59 +0000)]
Restrict reimplemented to avoid generating lists of indexes to be restricted
that fall outside the context. It doesn't change much, really.

20 years agoAdded a TODO (to catch only the right exceptions instead of everything).
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 10:58:17 +0000 (10:58 +0000)]
Added a TODO (to catch only the right exceptions instead of everything).

20 years agoBug fixed: the canonical contexts were traversed in the wrong direction
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 10:33:59 +0000 (10:33 +0000)]
Bug fixed: the canonical contexts were traversed in the wrong direction
during restriction. As a consequence, some hypothesis were not correctly
restricted.

20 years agoRel to hidden hypotheses are now printed as _hidden_n.
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 23:41:14 +0000 (23:41 +0000)]
Rel to hidden hypotheses are now printed as _hidden_n.

20 years agoppterm_in_context exported
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 23:27:11 +0000 (23:27 +0000)]
ppterm_in_context exported

20 years agoppcontext (and thus also ppmetasenv) were buggy: the occurrences of a variable
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 23:20:19 +0000 (23:20 +0000)]
ppcontext (and thus also ppmetasenv) were buggy: the occurrences of a variable
bound to a previous entry were of the form -n (instead of showing the binder)

20 years agoFunctors must be applied using parentheses around the argument in OCaml.
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 22:55:12 +0000 (22:55 +0000)]
Functors must be applied using parentheses around the argument in OCaml.
CamlP4 accepts a looser syntax ;-(

20 years agoAdded newline.
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 22:28:02 +0000 (22:28 +0000)]
Added newline.