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

20 years agooptionalizide some class parameters
Stefano Zacchiroli [Sat, 24 Jan 2004 16:58:48 +0000 (16:58 +0000)]
optionalizide some class parameters

20 years ago.in version of "configuration" modules
Stefano Zacchiroli [Sat, 24 Jan 2004 12:35:09 +0000 (12:35 +0000)]
.in version of "configuration" modules

20 years agodebug_print
Stefano Zacchiroli [Sat, 24 Jan 2004 12:34:41 +0000 (12:34 +0000)]
debug_print

20 years agonew configure.ac with support for compile time configuration of termeditor/parser/...
Stefano Zacchiroli [Sat, 24 Jan 2004 12:33:42 +0000 (12:33 +0000)]
new configure.ac with support for compile time configuration of termeditor/parser/...

20 years agosplit a term0 rule for dinamycally change top-level (i.e. non-recursive) term rul
Stefano Zacchiroli [Sat, 24 Jan 2004 12:32:04 +0000 (12:32 +0000)]
split a term0 rule for dinamycally change top-level (i.e. non-recursive) term rul

20 years agocollapsed parens in a singol token
Stefano Zacchiroli [Sat, 24 Jan 2004 12:31:30 +0000 (12:31 +0000)]
collapsed parens in a singol token

20 years agoadded tex notation
Stefano Zacchiroli [Sat, 24 Jan 2004 12:31:05 +0000 (12:31 +0000)]
added tex notation

20 years agotex notation for compatibility with texTermEditor
Stefano Zacchiroli [Sat, 24 Jan 2004 12:29:57 +0000 (12:29 +0000)]
tex notation for compatibility with texTermEditor

20 years ago- quiet debugging for mathql
Stefano Zacchiroli [Sat, 24 Jan 2004 12:29:26 +0000 (12:29 +0000)]
- quiet debugging for mathql
- defined a debug_print function with a verbosity level

20 years agoEureka!
Claudio Sacerdoti Coen [Fri, 23 Jan 2004 17:45:29 +0000 (17:45 +0000)]
Eureka!
It is now possible to choose independently:

 - the widget for the term editor
 - the disambiguating parser, i.e.
   * the parsing component
   * the disambiguating component

20 years agoported to new module names
Stefano Zacchiroli [Fri, 23 Jan 2004 17:41:28 +0000 (17:41 +0000)]
ported to new module names

20 years agohandle Cic.Anonymous
Stefano Zacchiroli [Fri, 23 Jan 2004 17:41:17 +0000 (17:41 +0000)]
handle Cic.Anonymous

20 years agorenamed modules so that they are more consistent with other cic modules
Stefano Zacchiroli [Fri, 23 Jan 2004 17:05:20 +0000 (17:05 +0000)]
renamed modules so that they are more consistent with other cic modules

20 years agomoved environmentP3 in cic_textual_parser2 and reshaped interface
Stefano Zacchiroli [Fri, 23 Jan 2004 16:39:35 +0000 (16:39 +0000)]
moved environmentP3 in cic_textual_parser2 and reshaped interface

20 years agoimplemented interface for gTopLevel
Stefano Zacchiroli [Fri, 23 Jan 2004 16:38:17 +0000 (16:38 +0000)]
implemented interface for gTopLevel

20 years agomoved term_of_uri in cic/
Stefano Zacchiroli [Fri, 23 Jan 2004 16:37:57 +0000 (16:37 +0000)]
moved term_of_uri in cic/

20 years agomoved here term_of_uri
Stefano Zacchiroli [Fri, 23 Jan 2004 16:37:30 +0000 (16:37 +0000)]
moved here term_of_uri

20 years agobetter comment for kernel wrappers
Stefano Zacchiroli [Fri, 23 Jan 2004 16:37:14 +0000 (16:37 +0000)]
better comment for kernel wrappers

20 years agoa better error message
Stefano Zacchiroli [Fri, 23 Jan 2004 16:37:00 +0000 (16:37 +0000)]
a better error message

20 years ago- Added DisambiguatingParser (that abstracts both the parser and the
Claudio Sacerdoti Coen [Fri, 23 Jan 2004 15:30:33 +0000 (15:30 +0000)]
- Added DisambiguatingParser (that abstracts both the parser and the
  disambiguator used)
- Added ChosenTermEditor (used to swap quickly the editor used).
- moved disambiguate.ml* to oldDisambiguate.ml*