]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

20 years agoeat_prods reimplemented to generalize the output type of the application
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 13:04:33 +0000 (13:04 +0000)]
eat_prods reimplemented to generalize the output type of the application
a bit more (when it is a metavariable).

20 years agoAdded an optional parameter to identity_relocation_list. The parameter
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 13:03:49 +0000 (13:03 +0000)]
Added an optional parameter to identity_relocation_list. The parameter
is the "starting" rel.

20 years agoMore debug informations.
Claudio Sacerdoti Coen [Tue, 3 Feb 2004 12:34:32 +0000 (12:34 +0000)]
More debug informations.

20 years agoSubstitution no longer returned from CicRefine.type_of_aux
Claudio Sacerdoti Coen [Mon, 2 Feb 2004 18:39:42 +0000 (18:39 +0000)]
Substitution no longer returned from CicRefine.type_of_aux

20 years agoported to new type_of prototype
Stefano Zacchiroli [Mon, 2 Feb 2004 17:06:25 +0000 (17:06 +0000)]
ported to new type_of prototype

20 years agouses CicMetaSubst.ppterm where needed
Stefano Zacchiroli [Mon, 2 Feb 2004 17:03:12 +0000 (17:03 +0000)]
uses CicMetaSubst.ppterm where needed

20 years ago- refine's type_of no longer return a substitution
Stefano Zacchiroli [Mon, 2 Feb 2004 17:01:50 +0000 (17:01 +0000)]
- refine's type_of no longer return a substitution

20 years agoported to latest Ast changes (mainly capture_variable addition)
Stefano Zacchiroli [Mon, 2 Feb 2004 16:46:12 +0000 (16:46 +0000)]
ported to latest Ast changes (mainly capture_variable addition)

20 years ago- added entries for capture variables parsing
Stefano Zacchiroli [Mon, 2 Feb 2004 16:45:33 +0000 (16:45 +0000)]
- added entries for capture variables parsing
- factorized function for parsing Cic.names

20 years ago- added capture_variable entry and Cic.names here and there
Stefano Zacchiroli [Mon, 2 Feb 2004 16:44:26 +0000 (16:44 +0000)]
- added capture_variable entry and Cic.names here and there

20 years ago- changed ast for pattern matching so that type annotations are possible
Stefano Zacchiroli [Mon, 2 Feb 2004 16:43:49 +0000 (16:43 +0000)]
- changed ast for pattern matching so that type annotations are possible
- bugfix for indexes in Fix/CoFix cases

20 years ago- big hack: keep on unifying/refining when SortExpectedMetaFound
Stefano Zacchiroli [Mon, 2 Feb 2004 16:38:21 +0000 (16:38 +0000)]
- big hack: keep on unifying/refining when SortExpectedMetaFound
  exception is encountered

20 years ago- removed metasenv argument from kernel proxies invocations
Stefano Zacchiroli [Mon, 2 Feb 2004 16:37:10 +0000 (16:37 +0000)]
- removed metasenv argument from kernel proxies invocations
- lift_meta over defs with an explicit type implemented
- reimplemented eat_prods (open bug: when an application has more than
  one argument and its type is a meta then the outtype is a Meta whose
  context is not general enough. To be implemented)

20 years ago- added SortExpectedMetaFound exception (huge hack)
Stefano Zacchiroli [Mon, 2 Feb 2004 16:30:06 +0000 (16:30 +0000)]
- added SortExpectedMetaFound exception (huge hack)
- more information along with assertion failed "9"

20 years ago- bugfix for expand_implicits, return correct term on Fix and CoFix cases
Stefano Zacchiroli [Mon, 2 Feb 2004 16:15:43 +0000 (16:15 +0000)]
- bugfix for expand_implicits, return correct term on Fix and CoFix cases

20 years ago- removed unwind: every substitution is now _not_ unwinded
Stefano Zacchiroli [Mon, 2 Feb 2004 16:14:56 +0000 (16:14 +0000)]
- removed unwind: every substitution is now _not_ unwinded
- removed extra metasenv argument from all kernel proxies
- added kernel proxy: subst (for CicSubstitution.subst)
- added pretty printer ppterm

20 years agochanged prototype of CicMetaSubst.apply_subst*
Stefano Zacchiroli [Mon, 2 Feb 2004 16:11:37 +0000 (16:11 +0000)]
changed prototype of CicMetaSubst.apply_subst*

20 years agoadded comments
Stefano Zacchiroli [Mon, 2 Feb 2004 16:10:49 +0000 (16:10 +0000)]
added comments

20 years agofact regtest
Stefano Zacchiroli [Mon, 2 Feb 2004 14:53:48 +0000 (14:53 +0000)]
fact regtest

20 years agoreordered
Stefano Zacchiroli [Fri, 30 Jan 2004 08:15:01 +0000 (08:15 +0000)]
reordered

20 years agoadded string_of_html_msg
Stefano Zacchiroli [Fri, 30 Jan 2004 08:14:19 +0000 (08:14 +0000)]
added string_of_html_msg

20 years ago- typo bugfix: INT token no longer exists
Stefano Zacchiroli [Fri, 30 Jan 2004 08:13:56 +0000 (08:13 +0000)]
- typo bugfix: INT token no longer exists
- use "=" instead of \def for let definitions
- added a new "binder" level so that \forall n. n=n binds correctly

20 years agoRefinement of Fix and CoFix now implemented.
Claudio Sacerdoti Coen [Fri, 30 Jan 2004 08:13:29 +0000 (08:13 +0000)]
Refinement of Fix and CoFix now implemented.

20 years ago- removed ancient refine exception
Stefano Zacchiroli [Fri, 30 Jan 2004 08:11:56 +0000 (08:11 +0000)]
- removed ancient refine exception
- s/Try every selection/Try selected/ on a button

20 years agoadded regression tests
Stefano Zacchiroli [Fri, 30 Jan 2004 08:10:16 +0000 (08:10 +0000)]
added regression tests

20 years agos/Callbacks/DisambiguateCallbacks/
Stefano Zacchiroli [Fri, 30 Jan 2004 08:08:51 +0000 (08:08 +0000)]
s/Callbacks/DisambiguateCallbacks/

20 years ago- lift added to CicMetaSubst
Claudio Sacerdoti Coen [Thu, 29 Jan 2004 18:35:14 +0000 (18:35 +0000)]
- lift added to CicMetaSubst
- refine of Fix and CoFix implemented
- bug fixed in refine of Cast

20 years ago- s/TexTermEditor/TermEditor/ (* former no longer appropriate)
Stefano Zacchiroli [Thu, 29 Jan 2004 14:53:16 +0000 (14:53 +0000)]
- s/TexTermEditor/TermEditor/ (* former no longer appropriate)
- added "auto disambiguation" setting support

20 years ago- added "clear alias" menu item
Stefano Zacchiroli [Thu, 29 Jan 2004 13:25:52 +0000 (13:25 +0000)]
- added "clear alias" menu item
- added "clear" button to the "edit aliases" window

20 years ago- occur check test anticipated to the delift phase
Stefano Zacchiroli [Tue, 27 Jan 2004 17:30:09 +0000 (17:30 +0000)]
- occur check test anticipated to the delift phase
- uses CicUtil.lookup_meta

20 years agouse CicUtil.lookup_meta
Stefano Zacchiroli [Tue, 27 Jan 2004 17:29:18 +0000 (17:29 +0000)]
use CicUtil.lookup_meta

20 years agobad link patched
Ferruccio Guidi [Tue, 27 Jan 2004 17:25:43 +0000 (17:25 +0000)]
bad link patched

20 years agos/List.find.../CicUtil.lookup_meta/
Stefano Zacchiroli [Tue, 27 Jan 2004 17:08:31 +0000 (17:08 +0000)]
s/List.find.../CicUtil.lookup_meta/

20 years agoadded CicUtil module with just lookup_meta function
Stefano Zacchiroli [Tue, 27 Jan 2004 17:07:44 +0000 (17:07 +0000)]
added CicUtil module with just lookup_meta function

20 years agoempty goal patched
Ferruccio Guidi [Tue, 27 Jan 2004 13:47:37 +0000 (13:47 +0000)]
empty goal patched

20 years agoopt goal fixed
Ferruccio Guidi [Tue, 27 Jan 2004 13:36:06 +0000 (13:36 +0000)]
opt goal fixed

20 years agotest for empty string given, if so return Environment.empty without invoking the...
Andrea Asperti [Tue, 27 Jan 2004 12:32:25 +0000 (12:32 +0000)]
test for empty string given, if so return Environment.empty without invoking the parser

20 years agohelm registry's META
Stefano Zacchiroli [Tue, 27 Jan 2004 11:51:39 +0000 (11:51 +0000)]
helm registry's META

20 years agohelm registry --- first release
Stefano Zacchiroli [Tue, 27 Jan 2004 11:48:55 +0000 (11:48 +0000)]
helm registry --- first release

20 years agosample aliases language
Stefano Zacchiroli [Tue, 27 Jan 2004 08:47:53 +0000 (08:47 +0000)]
sample aliases language

20 years agoNotation for Case revisited and completed.
Andrea Asperti [Mon, 26 Jan 2004 13:40:46 +0000 (13:40 +0000)]
Notation for Case revisited and completed.

20 years agoGenerated ml files added.
Claudio Sacerdoti Coen [Mon, 26 Jan 2004 10:14:53 +0000 (10:14 +0000)]
Generated ml files added.

20 years agoraise proper exception when a regexp fails on term_of_uri
Stefano Zacchiroli [Mon, 26 Jan 2004 00:03:37 +0000 (00:03 +0000)]
raise proper exception when a regexp fails on term_of_uri

20 years agodon't remove METAs on clean, but on distclean
Stefano Zacchiroli [Sat, 24 Jan 2004 17:01:36 +0000 (17:01 +0000)]
don't remove METAs on clean, but on distclean

20 years ago- s/id_to_uris/environment/
Stefano Zacchiroli [Sat, 24 Jan 2004 17:00:58 +0000 (17:00 +0000)]
- s/id_to_uris/environment/
- bugfix: aliases work again

20 years agoreference moved EnvironmentP3 for new parser
Stefano Zacchiroli [Sat, 24 Jan 2004 17:00:18 +0000 (17:00 +0000)]
reference moved EnvironmentP3 for new parser

20 years ago- factorized DisambiguateChoices module
Stefano Zacchiroli [Sat, 24 Jan 2004 16:59:45 +0000 (16:59 +0000)]
- factorized DisambiguateChoices module
- implemented alias language for gTopLevel