]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agoThis commit was manufactured by cvs2svn to create tag 'V_0_2_999'. V_0_2_999
no author [Mon, 9 Feb 2004 13:22:00 +0000 (13:22 +0000)]
This commit was manufactured by cvs2svn to create tag 'V_0_2_999'.

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.

20 years agoBug fixed: restriction of already restricted contexts was bugged (due to
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 22:22:44 +0000 (22:22 +0000)]
Bug fixed: restriction of already restricted contexts was bugged (due to
a missing "incr i").

20 years agoEffects of fixing bugs for other regression tests ;-)
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 21:31:23 +0000 (21:31 +0000)]
Effects of fixing bugs for other regression tests ;-)

20 years agoWe no longer apply the subst to a Meta in force_does_not_occur. In this
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 21:26:44 +0000 (21:26 +0000)]
We no longer apply the subst to a Meta in force_does_not_occur. In this
way we can restrict if something goes wrong.

20 years agodelift no longer apply the substitution when a Meta is found.
Andrea Asperti [Wed, 4 Feb 2004 17:32:54 +0000 (17:32 +0000)]
delift no longer apply the substitution when a Meta is found.
Reason: in this way I can restrict if something goes wrong.

20 years agoAdded a new example.
Andrea Asperti [Wed, 4 Feb 2004 16:56:46 +0000 (16:56 +0000)]
Added a new example.

20 years ago...
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 15:57:21 +0000 (15:57 +0000)]
...

20 years agoreport files are now produced (and removed) during regression testing
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 15:47:55 +0000 (15:47 +0000)]
report files are now produced (and removed) during regression testing

20 years agoPatch to delift withdrawn.
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 14:33:04 +0000 (14:33 +0000)]
Patch to delift withdrawn.
The patch was used to nullify items in the local context when they where

20 years ago...
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 14:27:38 +0000 (14:27 +0000)]
...

20 years agoTypo fixed. Used to break target gentest.
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 14:26:46 +0000 (14:26 +0000)]
Typo fixed. Used to break target gentest.

20 years agoBug fixed: when a variable not instantiated yet was restricted, some
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 14:22:11 +0000 (14:22 +0000)]
Bug fixed: when a variable not instantiated yet was restricted, some
nececssary restrictions were not performed due to a typo.

20 years agoImproved regression testing reporting.
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 13:45:03 +0000 (13:45 +0000)]
Improved regression testing reporting.

20 years ago- regtest: better argument handling (using Arg)
Claudio Sacerdoti Coen [Wed, 4 Feb 2004 11:52:51 +0000 (11:52 +0000)]
- regtest: better argument handling (using Arg)
- regtest: -dump and -nodump to dump the environment (that is authomatically
  restored if found)
- Makefile: new target envtest that generates the environments without
  changing the .test files

20 years agoremoved a debugging message
Stefano Zacchiroli [Wed, 4 Feb 2004 09:46:32 +0000 (09:46 +0000)]
removed a debugging message

20 years ago- improved some error messages
Stefano Zacchiroli [Wed, 4 Feb 2004 09:46:18 +0000 (09:46 +0000)]
- improved some error messages
- sort_of_prod: returned argument wasn't lifted correctly, as a temporary
  patch return Type

20 years agomoved here CicAst and pretty printer
Stefano Zacchiroli [Wed, 4 Feb 2004 09:44:38 +0000 (09:44 +0000)]
moved here CicAst and pretty printer

20 years agoported to CicAst
Stefano Zacchiroli [Wed, 4 Feb 2004 09:43:15 +0000 (09:43 +0000)]
ported to CicAst

20 years ago- sorted domain which hopefully avoids exponential explosion
Stefano Zacchiroli [Wed, 4 Feb 2004 09:42:58 +0000 (09:42 +0000)]
- sorted domain which hopefully avoids exponential explosion
- ported to CicAst

20 years agomoved Ast in cic_transformations/
Stefano Zacchiroli [Wed, 4 Feb 2004 09:42:12 +0000 (09:42 +0000)]
moved Ast in cic_transformations/

20 years ago- added support for implicit in concrete syntax
Stefano Zacchiroli [Wed, 4 Feb 2004 09:41:35 +0000 (09:41 +0000)]
- added support for implicit in concrete syntax
- ported to new Ast

20 years agoregression tests
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 15:43:46 +0000 (15:43 +0000)]
regression tests

20 years agocic_mkimplicit' removed (its implementation was wrong and the function is
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 15:43:24 +0000 (15:43 +0000)]
cic_mkimplicit' removed (its implementation was wrong and the function is
not really used)

20 years agoDebugging code removed.
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 15:24:12 +0000 (15:24 +0000)]
Debugging code removed.

20 years agosort_of_prod changed to not generate a new metavariable in the case Meta vs
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 15:11:07 +0000 (15:11 +0000)]
sort_of_prod changed to not generate a new metavariable in the case Meta vs
Sort. Reason: the new metavariable is not constrained in any way and, at the
end, we find it in the final metasenv.

20 years ago- comment inside .test file that explain what follows
Stefano Zacchiroli [Tue, 3 Feb 2004 15:02:52 +0000 (15:02 +0000)]
- comment inside .test file that explain what follows
- use a list to clear buffers
- better comment for .test file format

20 years agoadded cleantest target (removes tests/*.test)
Stefano Zacchiroli [Tue, 3 Feb 2004 15:01:56 +0000 (15:01 +0000)]
added cleantest target (removes tests/*.test)

20 years agoCheck missed: the two metasenv were not compared.
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 14:49:16 +0000 (14:49 +0000)]
Check missed: the two metasenv were not compared.

20 years agoDebuggin infos removed.
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 14:40:14 +0000 (14:40 +0000)]
Debuggin infos removed.

20 years ago- do not crash any longer if type-checking or reduction fails
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 14:29:34 +0000 (14:29 +0000)]
- do not crash any longer if type-checking or reduction fails
- prints also the metasenv

20 years agotime added to regtest
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 14:29:06 +0000 (14:29 +0000)]
time added to regtest

20 years agocatch just AssertFailure instead of _ (AssertFailure is the only
Stefano Zacchiroli [Tue, 3 Feb 2004 14:10:53 +0000 (14:10 +0000)]
catch just AssertFailure instead of _ (AssertFailure is the only
exception that could be raised there since the invoked function wraps
every exception inside it)

20 years agoremoved SortExpectedMetaFound special exception
Stefano Zacchiroli [Tue, 3 Feb 2004 14:09:32 +0000 (14:09 +0000)]
removed SortExpectedMetaFound special exception

20 years agoadded urimanager dependency
Stefano Zacchiroli [Tue, 3 Feb 2004 14:07:44 +0000 (14:07 +0000)]
added urimanager dependency

20 years agoMeta vs same Meta now tries unification when convertibility of the two
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 14:07:43 +0000 (14:07 +0000)]
Meta vs same Meta now tries unification when convertibility of the two
substitutions fails.

20 years agos/LocatedTerm/AnnotatedTerm + various annotations/
Stefano Zacchiroli [Tue, 3 Feb 2004 14:06:01 +0000 (14:06 +0000)]
s/LocatedTerm/AnnotatedTerm + various annotations/

20 years agoNew tests for lambdas (that show bugs in applications ;-)
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 14:04:05 +0000 (14:04 +0000)]
New tests for lambdas (that show bugs in applications ;-)

20 years agocatch exceptions and mark corresponding tests as failed
Stefano Zacchiroli [Tue, 3 Feb 2004 13:45:52 +0000 (13:45 +0000)]
catch exceptions and mark corresponding tests as failed