]> matita.cs.unibo.it Git - helm.git/log
helm.git
14 years ago freescale porting, work in progress
Cosimo Oliboni [Thu, 21 Jan 2010 02:16:45 +0000 (02:16 +0000)]
 freescale porting, work in progress

14 years agoWe can always use the "covered by emptyset" relation...
Claudio Sacerdoti Coen [Tue, 19 Jan 2010 12:52:53 +0000 (12:52 +0000)]
We can always use the "covered by emptyset" relation...
Closer and closer to Bove-Capretta, but more and more far away from IGFT...

14 years agoMore //.
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:49:58 +0000 (12:49 +0000)]
More //.

14 years agoMore // everywhere.
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:40:38 +0000 (12:40 +0000)]
More // everywhere.

14 years ago// used everywhere!
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:00:31 +0000 (12:00 +0000)]
// used everywhere!

14 years ago// in place of nauto everywhere
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 11:46:06 +0000 (11:46 +0000)]
// in place of nauto everywhere

14 years ago// is now more powerful
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 10:39:40 +0000 (10:39 +0000)]
// is now more powerful

14 years ago// is now more powerful
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 10:34:24 +0000 (10:34 +0000)]
// is now more powerful

14 years agoNew paramod tac.
Andrea Asperti [Mon, 18 Jan 2010 10:04:51 +0000 (10:04 +0000)]
New paramod tac.

14 years agoInvocation of paramod
Andrea Asperti [Mon, 18 Jan 2010 09:59:04 +0000 (09:59 +0000)]
Invocation of paramod

14 years agoparamod_tac exported
Andrea Asperti [Mon, 18 Jan 2010 09:57:43 +0000 (09:57 +0000)]
paramod_tac exported

14 years agoNumber notation for NG
Andrea Asperti [Mon, 18 Jan 2010 09:51:57 +0000 (09:51 +0000)]
Number notation for NG

14 years agoNumber notation for NG
Andrea Asperti [Mon, 18 Jan 2010 09:51:09 +0000 (09:51 +0000)]
Number notation for NG

14 years agoNumber notation for NG.
Andrea Asperti [Mon, 18 Jan 2010 09:50:06 +0000 (09:50 +0000)]
Number notation for NG.

14 years agoKeeping Implicit for refinement (instead of transforming them to Metas:
Andrea Asperti [Mon, 18 Jan 2010 07:25:27 +0000 (07:25 +0000)]
Keeping Implicit for refinement (instead of transforming them to Metas:
context bug).

14 years agoUpdating.
Andrea Asperti [Mon, 18 Jan 2010 07:23:03 +0000 (07:23 +0000)]
Updating.

14 years agoA slightly more complicated example.
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 17:10:07 +0000 (17:10 +0000)]
A slightly more complicated example.

14 years agoFinished!
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 17:06:45 +0000 (17:06 +0000)]
Finished!

14 years agoWe are still equivalent (even if the definition of ncover is obfuscated).
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 16:15:09 +0000 (16:15 +0000)]
We are still equivalent (even if the definition of ncover is obfuscated).

14 years agoUrrah!
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 16:12:43 +0000 (16:12 +0000)]
Urrah!

14 years agoExtending to the nAx set.
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 15:55:29 +0000 (15:55 +0000)]
Extending to the nAx set.

14 years agoSkipfact function (a partial general recursive function) defined by recursion
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 10:46:34 +0000 (10:46 +0000)]
Skipfact function (a partial general recursive function) defined by recursion
over the cover relation of an IGFT.

14 years agoFixed a bug in the discrimination principle: the refiner was not able to
Wilmer Ricciotti [Tue, 12 Jan 2010 12:23:37 +0000 (12:23 +0000)]
Fixed a bug in the discrimination principle: the refiner was not able to
synthesize the return type of the inner match correctly.

14 years agoFinished
Claudio Sacerdoti Coen [Mon, 11 Jan 2010 16:59:40 +0000 (16:59 +0000)]
Finished

14 years ago1. New paramodulation function
Andrea Asperti [Mon, 11 Jan 2010 11:27:54 +0000 (11:27 +0000)]
1. New paramodulation function
2. goal narrowing works both on the current goal both before and after
demodulation

14 years agosaturate cust be called with delta=0
Andrea Asperti [Mon, 11 Jan 2010 11:23:25 +0000 (11:23 +0000)]
saturate cust be called with delta=0

14 years agoAdded is_equation
Andrea Asperti [Mon, 11 Jan 2010 11:21:58 +0000 (11:21 +0000)]
Added is_equation

14 years agoDebugging info
Andrea Asperti [Mon, 11 Jan 2010 11:21:00 +0000 (11:21 +0000)]
Debugging info

14 years agoImproved
Claudio Sacerdoti Coen [Fri, 8 Jan 2010 18:43:54 +0000 (18:43 +0000)]
Improved

14 years agoPartial porting to new syntax.
Claudio Sacerdoti Coen [Fri, 8 Jan 2010 18:36:06 +0000 (18:36 +0000)]
Partial porting to new syntax.

14 years agoSource language path must be appended, not replaced.
Claudio Sacerdoti Coen [Fri, 8 Jan 2010 17:34:30 +0000 (17:34 +0000)]
Source language path must be appended, not replaced.

14 years agoCategorical stuff postponed.
Claudio Sacerdoti Coen [Fri, 8 Jan 2010 15:18:46 +0000 (15:18 +0000)]
Categorical stuff postponed.

14 years agoThe body of constants is a reference, not the actual body!
Andrea Asperti [Fri, 8 Jan 2010 09:29:51 +0000 (09:29 +0000)]
The body of constants is a reference, not the actual body!

14 years agoremoved debugging info
Andrea Asperti [Fri, 8 Jan 2010 08:23:31 +0000 (08:23 +0000)]
removed debugging info

14 years agorebuilding the library
Andrea Asperti [Fri, 8 Jan 2010 08:19:24 +0000 (08:19 +0000)]
rebuilding the library

14 years agorebuilding the library
Andrea Asperti [Fri, 8 Jan 2010 08:18:20 +0000 (08:18 +0000)]
rebuilding the library

14 years agorebuilding the library
Andrea Asperti [Fri, 8 Jan 2010 08:17:37 +0000 (08:17 +0000)]
rebuilding the library

14 years agoapplyS
Andrea Asperti [Fri, 8 Jan 2010 08:12:06 +0000 (08:12 +0000)]
applyS

14 years agorefresh uri
Andrea Asperti [Fri, 8 Jan 2010 08:11:14 +0000 (08:11 +0000)]
refresh uri
applyS

14 years agoSupport for the new auto tactics //
Andrea Asperti [Fri, 8 Jan 2010 08:10:20 +0000 (08:10 +0000)]
Support for the new auto tactics //

14 years agoSupport for the new // tactics.
Andrea Asperti [Fri, 8 Jan 2010 08:09:39 +0000 (08:09 +0000)]
Support for the new // tactics.

14 years agonew reloc_subst (to avoid cyclic substitutions).
Andrea Asperti [Fri, 8 Jan 2010 08:08:44 +0000 (08:08 +0000)]
new reloc_subst (to avoid cyclic substitutions).
Changed default sig.

14 years ago....
Enrico Tassi [Thu, 7 Jan 2010 23:24:52 +0000 (23:24 +0000)]
....

14 years ago...
Enrico Tassi [Thu, 7 Jan 2010 23:23:09 +0000 (23:23 +0000)]
...

14 years ago...
Enrico Tassi [Thu, 7 Jan 2010 22:53:47 +0000 (22:53 +0000)]
...

14 years agoSimplified.
Claudio Sacerdoti Coen [Wed, 6 Jan 2010 23:03:47 +0000 (23:03 +0000)]
Simplified.

Note: it breaks the file later (maybe a coercion conflict, I suppose).

14 years agoCoercions via unification hints?
Claudio Sacerdoti Coen [Wed, 6 Jan 2010 22:37:10 +0000 (22:37 +0000)]
Coercions via unification hints?

14 years ago- we now add the kernel options in the preamble of the URI hierarchy
Ferruccio Guidi [Tue, 5 Jan 2010 19:13:40 +0000 (19:13 +0000)]
- we now add the kernel options in the preamble of the URI hierarchy
- we now quote the identifiers by default to make them NMTOKENS but we added a command line option to disable this quoting (it can be time consuming)

14 years ago1) stuff moved from categories.ma to setoids*.ma
Claudio Sacerdoti Coen [Sat, 2 Jan 2010 19:40:58 +0000 (19:40 +0000)]
1) stuff moved from categories.ma to setoids*.ma
2) we are now ready to define the category of o-algebras

14 years ago...
Enrico Tassi [Wed, 30 Dec 2009 18:17:43 +0000 (18:17 +0000)]
...

14 years agoAlmost done (up to definition of category).
Claudio Sacerdoti Coen [Wed, 30 Dec 2009 17:41:59 +0000 (17:41 +0000)]
Almost done (up to definition of category).

14 years agoPorting of Sambin's stuff started.
Claudio Sacerdoti Coen [Wed, 30 Dec 2009 17:33:30 +0000 (17:33 +0000)]
Porting of Sambin's stuff started.
Everything is now automatically enriched using hints.
It seems to work quite smoothly.

14 years agoPorting of Sambin's stuff started.
Claudio Sacerdoti Coen [Wed, 30 Dec 2009 17:31:56 +0000 (17:31 +0000)]
Porting of Sambin's stuff started.

14 years agoRemoved line is back again.
Claudio Sacerdoti Coen [Wed, 30 Dec 2009 17:31:18 +0000 (17:31 +0000)]
Removed line is back again.

14 years ago...
Claudio Sacerdoti Coen [Wed, 30 Dec 2009 17:30:48 +0000 (17:30 +0000)]
...

14 years agoRefining with no expected type + unification seems to be faster.
Andrea Asperti [Mon, 21 Dec 2009 10:52:10 +0000 (10:52 +0000)]
Refining with no expected type + unification seems to be faster.

14 years agoTrying to be faster
Andrea Asperti [Mon, 21 Dec 2009 08:56:01 +0000 (08:56 +0000)]
Trying to be faster

14 years agoTrying to be faster.
Andrea Asperti [Mon, 21 Dec 2009 08:41:29 +0000 (08:41 +0000)]
Trying to be faster.

14 years agoFinal subst returned by superposition and passed around.
Andrea Asperti [Fri, 18 Dec 2009 08:53:10 +0000 (08:53 +0000)]
Final subst returned by superposition and passed around.

14 years agousing = instead of alpha conversions. context metasenv and subst are not
Andrea Asperti [Fri, 18 Dec 2009 08:52:16 +0000 (08:52 +0000)]
using = instead of alpha conversions. context metasenv and subst are not
needed any more

14 years agoeq_coerc for smart application.
Andrea Asperti [Tue, 15 Dec 2009 08:04:26 +0000 (08:04 +0000)]
eq_coerc for smart application.

14 years agothe sort hierarchy parameter enter the kernel status
Ferruccio Guidi [Mon, 14 Dec 2009 14:36:44 +0000 (14:36 +0000)]
the sort hierarchy parameter enter the kernel status

14 years agoMinor bag fixed, relative to failures.
Andrea Asperti [Thu, 10 Dec 2009 12:22:41 +0000 (12:22 +0000)]
Minor bag fixed, relative to failures.

14 years agoA compiling version?
Andrea Asperti [Thu, 10 Dec 2009 11:51:22 +0000 (11:51 +0000)]
A compiling version?

14 years agoAdded a "sort_metasenv" function.
Andrea Asperti [Wed, 9 Dec 2009 16:14:23 +0000 (16:14 +0000)]
Added a "sort_metasenv" function.

14 years agoCommented a couple of calls to "set_reference_of_oxuri".
Andrea Asperti [Wed, 9 Dec 2009 16:11:54 +0000 (16:11 +0000)]
Commented a couple of calls to "set_reference_of_oxuri".

14 years agoAdded the paramodulation stuff to the status
Andrea Asperti [Wed, 9 Dec 2009 16:10:09 +0000 (16:10 +0000)]
Added the paramodulation stuff to the status

14 years agoparam "slir" to call the new auto
Andrea Asperti [Wed, 9 Dec 2009 16:07:57 +0000 (16:07 +0000)]
param "slir" to call the new auto
and "fast paramod" for the constrained narrowing of the goal

14 years agoAdded the paramodulation active/passive tables to the state
Andrea Asperti [Wed, 9 Dec 2009 16:05:05 +0000 (16:05 +0000)]
Added the paramodulation active/passive tables to the state

14 years agoAttached fast_eq_check to auto
Andrea Asperti [Wed, 9 Dec 2009 16:02:48 +0000 (16:02 +0000)]
Attached fast_eq_check to auto

14 years agoAdded nnAuto.mli
Andrea Asperti [Wed, 9 Dec 2009 16:01:22 +0000 (16:01 +0000)]
Added nnAuto.mli

14 years agoDebug set to ()
Andrea Asperti [Wed, 9 Dec 2009 15:57:09 +0000 (15:57 +0000)]
Debug set to ()

14 years agoClean up of debgging info
Andrea Asperti [Wed, 9 Dec 2009 15:56:01 +0000 (15:56 +0000)]
Clean up of debgging info

14 years agoSyntax error
Andrea Asperti [Wed, 9 Dec 2009 15:53:26 +0000 (15:53 +0000)]
Syntax error

14 years agoWrong reference corrected
Andrea Asperti [Wed, 9 Dec 2009 15:48:41 +0000 (15:48 +0000)]
Wrong reference corrected

14 years agoMinor fixing for last chance
Andrea Asperti [Wed, 9 Dec 2009 15:47:38 +0000 (15:47 +0000)]
Minor fixing for last chance

14 years agoAdded a fol operation
Andrea Asperti [Wed, 9 Dec 2009 15:35:07 +0000 (15:35 +0000)]
Added a fol operation

14 years agoBugfix in inversion (was using refl_eq instead of refl).
Wilmer Ricciotti [Fri, 4 Dec 2009 11:30:34 +0000 (11:30 +0000)]
Bugfix in inversion (was using refl_eq instead of refl).

14 years agoIndexing local context for paramod.
Andrea Asperti [Fri, 4 Dec 2009 08:45:24 +0000 (08:45 +0000)]
Indexing local context for paramod.

14 years agoPropositional equality
Andrea Asperti [Wed, 2 Dec 2009 16:41:32 +0000 (16:41 +0000)]
Propositional equality

14 years agoThe new paramodulation functions instantiated over nCic.
Andrea Asperti [Wed, 2 Dec 2009 10:06:47 +0000 (10:06 +0000)]
The new paramodulation functions instantiated over nCic.

14 years agoNew ways for initialising the signature required for paramodultion
Andrea Asperti [Wed, 2 Dec 2009 10:05:30 +0000 (10:05 +0000)]
New ways for initialising the signature required for paramodultion

14 years agoPassive equations have their own index (not passive goals).
Andrea Asperti [Wed, 2 Dec 2009 10:01:06 +0000 (10:01 +0000)]
Passive equations have their own index (not passive goals).
New, simple version of "last chance" (yet to be improved).
Added a narrowing function the merely works on goals, in parallel.

14 years agodebug takes lazy strings. Moved here the are_alpha_eq test.
Andrea Asperti [Wed, 2 Dec 2009 09:54:05 +0000 (09:54 +0000)]
debug takes lazy strings. Moved here the are_alpha_eq test.

14 years agoAdded a function remove_unit_clause
Andrea Asperti [Wed, 2 Dec 2009 09:48:37 +0000 (09:48 +0000)]
Added a function remove_unit_clause

14 years agoAdded a boolean test function to discriminate equations from predicates
Andrea Asperti [Wed, 2 Dec 2009 09:45:42 +0000 (09:45 +0000)]
Added a boolean test function to discriminate equations from predicates

14 years agoGeneralized intitialization for EqP
Andrea Asperti [Wed, 2 Dec 2009 09:43:54 +0000 (09:43 +0000)]
Generalized intitialization for EqP

14 years agoGeneralized initialization of eqP.
Andrea Asperti [Wed, 2 Dec 2009 09:43:20 +0000 (09:43 +0000)]
Generalized initialization of eqP.

14 years agoporting to lablgtk2 >= 2.14 and releasing
Enrico Tassi [Tue, 1 Dec 2009 23:19:11 +0000 (23:19 +0000)]
porting to lablgtk2 >= 2.14 and releasing

14 years ago...
Enrico Tassi [Tue, 1 Dec 2009 23:09:26 +0000 (23:09 +0000)]
...

14 years agondestruct now clears off identity equations whenever it's possible.
Wilmer Ricciotti [Fri, 27 Nov 2009 15:04:40 +0000 (15:04 +0000)]
ndestruct now clears off identity equations whenever it's possible.

14 years agoFixed inversion, which was broken by the last changes in the refiner.
Wilmer Ricciotti [Wed, 25 Nov 2009 13:34:55 +0000 (13:34 +0000)]
Fixed inversion, which was broken by the last changes in the refiner.

14 years agoExported forward_inference_step
Andrea Asperti [Wed, 25 Nov 2009 13:01:10 +0000 (13:01 +0000)]
Exported forward_inference_step

14 years agoBugfix in tipify: a metavariable was set to type without sortifying its type.
Wilmer Ricciotti [Tue, 24 Nov 2009 16:56:59 +0000 (16:56 +0000)]
Bugfix in tipify: a metavariable was set to type without sortifying its type.

14 years agoIn order to prevent useless meta extensions, we optimize the unification of one
Wilmer Ricciotti [Tue, 24 Nov 2009 16:42:01 +0000 (16:42 +0000)]
In order to prevent useless meta extensions, we optimize the unification of one
type and one unrefined term (currently happening only in the Lambda case).

14 years agoWhen unifying
Wilmer Ricciotti [Tue, 24 Nov 2009 15:46:34 +0000 (15:46 +0000)]
When unifying

  ?1[a,b] == ?2[a,b,c]

it is not the same to instantiate ?1 or ?2: instantiating ?2 may drop the
dependency over c, while instatianting ?1 does no harm. This patch always
instantiates the meta whose canonical context is a prefix, or the newest one if
the two canonical contexts are the same.

14 years agoRemoved dead code
Andrea Asperti [Mon, 23 Nov 2009 11:21:27 +0000 (11:21 +0000)]
Removed dead code

14 years agoSubsumption and reduction
Andrea Asperti [Mon, 23 Nov 2009 10:42:34 +0000 (10:42 +0000)]
Subsumption and reduction

14 years ago- Added a swap parameter to the unification procedure
Wilmer Ricciotti [Thu, 19 Nov 2009 10:26:27 +0000 (10:26 +0000)]
- Added a swap parameter to the unification procedure
- Fixed a bug in the metavariable restriction algorithm, which resulted in bad
  metavariable local contexts.

14 years agoNCicRefiner.force_to_sort implemented on top of NCicUnification.sortfy.
Wilmer Ricciotti [Wed, 18 Nov 2009 14:36:17 +0000 (14:36 +0000)]
NCicRefiner.force_to_sort implemented on top of NCicUnification.sortfy.