]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agostupid error fixed
Claudio Sacerdoti Coen [Wed, 30 Apr 2008 21:38:26 +0000 (21:38 +0000)]
stupid error fixed

16 years agofixed_args fixed to accept passing a partially applied fix to a fix that
Claudio Sacerdoti Coen [Wed, 30 Apr 2008 20:50:58 +0000 (20:50 +0000)]
fixed_args fixed to accept passing a partially applied fix to a fix that
passes itself partially applied to anothere fix

16 years agoadded check on all bodies, only the one we actually encountered is applied to all...
Enrico Tassi [Wed, 30 Apr 2008 19:42:34 +0000 (19:42 +0000)]
added check on all bodies, only the one we actually encountered is applied to all arguments, other boedies are applied only up to j

16 years agoadded fake uri when the univ is anon
Enrico Tassi [Wed, 30 Apr 2008 19:04:28 +0000 (19:04 +0000)]
added fake uri when the univ is anon

16 years agofixed wrong Rel, still to do: Fix(i,j) applied to dangerous rel, check all bodies...
Enrico Tassi [Wed, 30 Apr 2008 17:02:00 +0000 (17:02 +0000)]
fixed wrong Rel, still to do: Fix(i,j) applied to dangerous rel, check all bodies in parallel, not just the i-th

16 years agouniverses are written with the URI inside objects, this allows
Enrico Tassi [Wed, 30 Apr 2008 15:50:06 +0000 (15:50 +0000)]
universes are written with the URI inside objects, this allows
universes to be actually shared between objects and no duplication is necessary.
in this way the typechecker is more strict and unification can be an ungly beast implicitly
adding an = constranint between two universes. speedup granted!

16 years agoxml strict!
Enrico Tassi [Wed, 30 Apr 2008 10:53:27 +0000 (10:53 +0000)]
xml strict!

16 years agomany pending modifications were there, now the website at least validates
Enrico Tassi [Wed, 30 Apr 2008 10:46:54 +0000 (10:46 +0000)]
many pending modifications were there, now the website at least validates

16 years agoguarded_by_destructors on steroids
Enrico Tassi [Wed, 30 Apr 2008 10:17:34 +0000 (10:17 +0000)]
guarded_by_destructors on steroids

  when Fix/i args and some args are not guarded
  1) fixed params in interval 0..i are checked for bewing just passed around
  2) the fix is unfolded, debruijned, fixed arguments substituted,
     not fixed arguments pushed and checked for guardednes
  3) a new function with relative fixed arguments (not to be checked again)
     is added to k
  4) the resulting term is applied to the remaining arguments

  testcase: cic:/Suresnes/MiniC/MiniC/State/sizeOfType.con

16 years agoadded list_mapi
Enrico Tassi [Wed, 30 Apr 2008 10:14:23 +0000 (10:14 +0000)]
added list_mapi

16 years agoTests status update.
Claudio Sacerdoti Coen [Tue, 29 Apr 2008 14:58:22 +0000 (14:58 +0000)]
Tests status update.

16 years agospeedup in fixing the graph closures
Enrico Tassi [Tue, 29 Apr 2008 10:18:56 +0000 (10:18 +0000)]
speedup in fixing the graph closures

16 years agoAvoid (whd ~delta:true) during guarded_by_destructors as much as possible.
Claudio Sacerdoti Coen [Mon, 28 Apr 2008 17:52:04 +0000 (17:52 +0000)]
Avoid (whd ~delta:true) during guarded_by_destructors as much as possible.
Note: it is better to check again if this commit is fully correct (i.e.
w.r.t. the catch-all case in the main "match ... with" of the aux function).

16 years agoIn guarded by destructors, avoid computing the (whd ~delta:true) unless the
Claudio Sacerdoti Coen [Mon, 28 Apr 2008 17:43:33 +0000 (17:43 +0000)]
In guarded by destructors, avoid computing the (whd ~delta:true) unless the
check fails. This is a major speed up, for instance for
cic:/Coq/ZArith/Zsqrt/sqrtrempos.con

16 years agoUpdate...
Claudio Sacerdoti Coen [Thu, 24 Apr 2008 17:08:25 +0000 (17:08 +0000)]
Update...

16 years agoNo more bugs on guarded_by_constructors in the old kernel.
Claudio Sacerdoti Coen [Thu, 24 Apr 2008 16:23:53 +0000 (16:23 +0000)]
No more bugs on guarded_by_constructors in the old kernel.

16 years agoWhen going under a binder, a term must be converted twice, as explained in the
Claudio Sacerdoti Coen [Thu, 24 Apr 2008 16:22:17 +0000 (16:22 +0000)]
When going under a binder, a term must be converted twice, as explained in the
previous commit. The problem is that in this way the complexity of the
translation becomes O(2^n) when n is the maximum depth of binders. However,
this computation is completely unuseful if no (co)fix is found in the term.
This commits adds as much lazyness as possible to fix the issue.

16 years agoProof of adequacy.
Wilmer Ricciotti [Thu, 24 Apr 2008 15:55:21 +0000 (15:55 +0000)]
Proof of adequacy.

16 years agoguarded_by_constructor completely rewritten, fixed missing lift when generating the...
Enrico Tassi [Thu, 24 Apr 2008 13:01:26 +0000 (13:01 +0000)]
guarded_by_constructor completely rewritten, fixed missing lift when generating the context of an inductive type in guarded_by_destructors.

16 years agoadded coinductive example
Enrico Tassi [Thu, 24 Apr 2008 13:00:21 +0000 (13:00 +0000)]
added coinductive example

16 years agoWorking and broken URIs.
Claudio Sacerdoti Coen [Thu, 24 Apr 2008 12:56:14 +0000 (12:56 +0000)]
Working and broken URIs.

16 years agoported the instantiate-left-params-to-calculate-rec-args patch from the old to the...
Enrico Tassi [Wed, 23 Apr 2008 16:41:37 +0000 (16:41 +0000)]
ported the instantiate-left-params-to-calculate-rec-args patch from the old to the new kernel,
to test the patch properly some steps of substitution inside a possibly blocked fix are performed,
this should be in general avoided without good checks (still to understand)

16 years agoAvoid other comparisons on universes using =.
Claudio Sacerdoti Coen [Wed, 23 Apr 2008 08:17:26 +0000 (08:17 +0000)]
Avoid other comparisons on universes using =.

16 years agoAvoid code duplication.
Claudio Sacerdoti Coen [Wed, 23 Apr 2008 08:09:39 +0000 (08:09 +0000)]
Avoid code duplication.

16 years agoDo NOT dare using Pervasives.compare on data structures containing URIs!
Claudio Sacerdoti Coen [Wed, 23 Apr 2008 08:04:53 +0000 (08:04 +0000)]
Do NOT dare using Pervasives.compare on data structures containing URIs!
Use UriManager.compare to get a 2x speed-up in type-checking setoids.

16 years agooblivion ugraph everywhere outside the kernel
Enrico Tassi [Tue, 22 Apr 2008 19:18:53 +0000 (19:18 +0000)]
oblivion ugraph everywhere outside the kernel

16 years agoslow_implementation and some dead code removed
Enrico Tassi [Tue, 22 Apr 2008 13:44:27 +0000 (13:44 +0000)]
slow_implementation and some dead code removed

16 years agomore strict check by CSC, I miss it
Enrico Tassi [Tue, 22 Apr 2008 13:28:10 +0000 (13:28 +0000)]
more strict check by CSC, I miss it

16 years agofix cache comparison relaxed to URI and not REFERENCE
Enrico Tassi [Tue, 22 Apr 2008 12:50:33 +0000 (12:50 +0000)]
fix cache comparison relaxed to URI and not REFERENCE

16 years agoadded a call to ppcontext in the case of appl, to ease the localization of the error
Enrico Tassi [Tue, 22 Apr 2008 12:48:10 +0000 (12:48 +0000)]
added a call to ppcontext in the case of appl, to ease the localization of the error

16 years agoadded ppcontext
Enrico Tassi [Tue, 22 Apr 2008 12:47:31 +0000 (12:47 +0000)]
added ppcontext

16 years agoTypes for LetIns computed during parsing for Coq objects may contain universes
Claudio Sacerdoti Coen [Tue, 22 Apr 2008 09:41:34 +0000 (09:41 +0000)]
Types for LetIns computed during parsing for Coq objects may contain universes
that must be made fresh.

16 years agodefn2.ma is to be used with part1a_inversion3
Claudio Sacerdoti Coen [Mon, 21 Apr 2008 17:20:43 +0000 (17:20 +0000)]
defn2.ma is to be used with part1a_inversion3
the induction/inversion lemma in part1a_inversion3 is more regular w.r.t.
 the meta-theory
automation pushed to its limits in part1a_inversion3.ma

16 years agofix universe handling, newly encountered objects are typed in an empty ugraph
Enrico Tassi [Mon, 21 Apr 2008 09:19:23 +0000 (09:19 +0000)]
fix universe handling, newly encountered objects are typed in an empty ugraph
that after the cleanup phase is committed into the cic_environement and merged
with the current one.

minor reformatting of sources and some more for_all

16 years agoAlternative prove using just one induction/inversion principle.
Claudio Sacerdoti Coen [Sun, 20 Apr 2008 21:32:11 +0000 (21:32 +0000)]
Alternative prove using just one induction/inversion principle.

16 years agobetter error message
Enrico Tassi [Sat, 19 Apr 2008 16:33:26 +0000 (16:33 +0000)]
better error message

16 years ago...
Enrico Tassi [Sat, 19 Apr 2008 16:32:53 +0000 (16:32 +0000)]
...

16 years agoimpredicative set work around
Enrico Tassi [Sat, 19 Apr 2008 16:32:36 +0000 (16:32 +0000)]
impredicative set work around

16 years agoimpredicative set work around
Enrico Tassi [Sat, 19 Apr 2008 16:32:22 +0000 (16:32 +0000)]
impredicative set work around

16 years agoassociativity of -> fixed
Enrico Tassi [Sat, 19 Apr 2008 16:30:53 +0000 (16:30 +0000)]
associativity of -> fixed

16 years agoancient graph regarding universes and trust=false, universes calculated for internal...
Enrico Tassi [Sat, 19 Apr 2008 16:30:21 +0000 (16:30 +0000)]
ancient graph regarding universes and trust=false, universes calculated for internal objects
were used for the toplevel object (that should be sound) but cleaned using the univ list of
the internal object

16 years agoextlib list_uniq instead of local copy
Enrico Tassi [Sat, 19 Apr 2008 16:27:57 +0000 (16:27 +0000)]
extlib list_uniq instead of local copy

16 years agoranking function fixed: when graphs are collapsed one step links are not updated...
Enrico Tassi [Sat, 19 Apr 2008 16:27:28 +0000 (16:27 +0000)]
ranking function fixed: when graphs are collapsed one step links are not updated (nor serialized to disk)
thus you can not rely on them, just use the closures!

16 years agoadded flag to change Set into Type on the fly, that helps on some coq objects using...
Enrico Tassi [Sat, 19 Apr 2008 16:26:21 +0000 (16:26 +0000)]
added flag to change Set into Type on the fly, that helps on some coq objects using impredicative set

16 years agooblivion_ugraph => empty_ugraph
Claudio Sacerdoti Coen [Sat, 19 Apr 2008 11:13:05 +0000 (11:13 +0000)]
oblivion_ugraph => empty_ugraph

16 years agoAdded to flags to activate/disactivate pretty-printing and exception catching.
Claudio Sacerdoti Coen [Sat, 19 Apr 2008 10:52:50 +0000 (10:52 +0000)]
Added to flags to activate/disactivate pretty-printing and exception catching.

16 years agoUris must be stripped of their xpointers.
Claudio Sacerdoti Coen [Sat, 19 Apr 2008 09:20:24 +0000 (09:20 +0000)]
Uris must be stripped of their xpointers.

16 years agoDead code removed.
Claudio Sacerdoti Coen [Fri, 18 Apr 2008 18:31:58 +0000 (18:31 +0000)]
Dead code removed.

16 years agoInversion lemma for Forall.
Claudio Sacerdoti Coen [Fri, 18 Apr 2008 18:27:43 +0000 (18:27 +0000)]
Inversion lemma for Forall.

16 years agoworkaround for Pi associativity
Enrico Tassi [Fri, 18 Apr 2008 16:58:38 +0000 (16:58 +0000)]
workaround for Pi associativity

16 years agoworkaround for some Set/Type problems
Enrico Tassi [Fri, 18 Apr 2008 16:50:10 +0000 (16:50 +0000)]
workaround for some Set/Type problems

16 years agocicEnvironment refactoring with sound view of Coq`s univ-less terms
Enrico Tassi [Fri, 18 Apr 2008 15:30:40 +0000 (15:30 +0000)]
cicEnvironment refactoring with sound view of Coq`s univ-less terms

16 years agoassertion was wrong, an object can contain a named univers if its uri is the one...
Enrico Tassi [Fri, 18 Apr 2008 15:27:39 +0000 (15:27 +0000)]
assertion was wrong, an object can contain a named univers if its uri is the one of the object itself

16 years agograph generation phase fixed
Enrico Tassi [Fri, 18 Apr 2008 15:26:11 +0000 (15:26 +0000)]
graph generation phase fixed

16 years agoAppl case in is_really_smaller fixed as in the old kernel
Enrico Tassi [Fri, 18 Apr 2008 13:59:17 +0000 (13:59 +0000)]
Appl case in is_really_smaller fixed as in the old kernel

16 years agoexample:
Enrico Tassi [Thu, 17 Apr 2008 16:55:36 +0000 (16:55 +0000)]
example:
  inductive I : Type :=
  | k : \forall A. (A -> I)-> I

  match t with
  | k _ f => f w (* is smaller than t even if applied! *)

16 years agoadded a missing whd
Enrico Tassi [Thu, 17 Apr 2008 16:34:44 +0000 (16:34 +0000)]
added a missing whd

16 years agonew calculation of recursive parameters in guarded by destructors:
Enrico Tassi [Thu, 17 Apr 2008 16:12:12 +0000 (16:12 +0000)]
new calculation of recursive parameters in guarded by destructors:

  inductive I : Type :=
  | K : list (pair Type I) -> I

  let rec f t on t : I -> bool :=
  match t with
  | k ((nat, x)::_) -> f x
  | k _ -> true

is now accepted. the arg of k used to be recursive but not the head of the list
(only its tail) since constructors types were not specialized on actual left
arguments (and the information that the type of the head contains I was lost).

16 years agoTwo similar cases packed together
Enrico Tassi [Thu, 17 Apr 2008 14:39:30 +0000 (14:39 +0000)]
Two similar cases packed together

16 years agosome fixes for guardness conditions
Enrico Tassi [Thu, 17 Apr 2008 14:30:56 +0000 (14:30 +0000)]
some fixes for guardness conditions

16 years agois_really_smaller in sync with old kernel, impossible cases removed
Enrico Tassi [Thu, 17 Apr 2008 14:26:23 +0000 (14:26 +0000)]
is_really_smaller in sync with old kernel, impossible cases removed

16 years agocheck_is_really_smaller simplified to consider that it is called only on terms
Claudio Sacerdoti Coen [Tue, 15 Apr 2008 20:52:43 +0000 (20:52 +0000)]
check_is_really_smaller simplified to consider that it is called only on terms
(immediately put in normal form) that inhabit an inductive type. Moreover,
some duplicated code has been removed.

16 years ago1. bug fixed: the context must be type-checked before using it in type_of_aux'.
Claudio Sacerdoti Coen [Tue, 15 Apr 2008 20:10:44 +0000 (20:10 +0000)]
1. bug fixed: the context must be type-checked before using it in type_of_aux'.
   Otherwise get_cooked_obj raises Not_found in Deannotate
2. big improvement in guarded_by_destructors: when a fix applied to a safe
   argument is found in the body of another fix, the body of the inner fix
   is check adding the recusrive formal parameter as an additional safe
   argument.

16 years agoget_checked_fix -> get_checked_fixes
Enrico Tassi [Tue, 15 Apr 2008 13:44:16 +0000 (13:44 +0000)]
get_checked_fix -> get_checked_fixes

16 years agoadded comment
Enrico Tassi [Tue, 15 Apr 2008 13:42:39 +0000 (13:42 +0000)]
added comment

16 years agoadded sample of guarded by in which coq is stronger
Claudio Sacerdoti Coen [Tue, 15 Apr 2008 10:47:29 +0000 (10:47 +0000)]
added sample of guarded by in which coq is stronger

16 years agopositivity check fixed, a MutInd not applied (but with an exp-named-subst)
Enrico Tassi [Tue, 15 Apr 2008 08:53:01 +0000 (08:53 +0000)]
positivity check fixed, a MutInd not applied (but with an exp-named-subst)
was considere non strictly positive always

16 years agodo not use an implicit but a sort as a neutral term for positivity check
Enrico Tassi [Tue, 15 Apr 2008 08:20:24 +0000 (08:20 +0000)]
do not use an implicit but a sort as a neutral term for positivity check

16 years agoobjects are typechecked to ensure there is a graph before doing all the stuff......
Enrico Tassi [Mon, 14 Apr 2008 14:59:12 +0000 (14:59 +0000)]
objects are typechecked to ensure there is a graph before doing all the stuff... read: much more memory is required

16 years agoleftno should be increased of the expnamedsubst, but counting only the uris of vars...
Enrico Tassi [Mon, 14 Apr 2008 14:48:14 +0000 (14:48 +0000)]
leftno should be increased of the expnamedsubst, but counting only the uris of vars without a body

16 years agobetter error message
Enrico Tassi [Mon, 14 Apr 2008 14:47:15 +0000 (14:47 +0000)]
better error message

16 years agosame_obj made more precise, fixed the order of the context for fixpoints body,
Enrico Tassi [Mon, 14 Apr 2008 13:21:15 +0000 (13:21 +0000)]
same_obj made more precise, fixed the order of the context for fixpoints body,
cache of fix extended to the mutual case (properly)

16 years agoficed fixpoint cache usage for mutual fix
Enrico Tassi [Mon, 14 Apr 2008 10:22:14 +0000 (10:22 +0000)]
ficed fixpoint cache usage for mutual fix

16 years agofixed positivity conditions
Enrico Tassi [Mon, 14 Apr 2008 10:21:33 +0000 (10:21 +0000)]
fixed positivity conditions

16 years agoadded mk_fix i j r that given an r of a fix generated another fix on i and j
Enrico Tassi [Mon, 14 Apr 2008 10:20:39 +0000 (10:20 +0000)]
added mk_fix i j r that given an r of a fix generated another fix on i and j

16 years agopositivity condition was relying on the name declared in abstractions, and
Enrico Tassi [Mon, 14 Apr 2008 09:58:24 +0000 (09:58 +0000)]
positivity condition was relying on the name declared in abstractions, and
was checking for a dependent product calling does not occurr with a wrong
index

16 years agoadded little optimization to not add twice the same arc
Enrico Tassi [Mon, 14 Apr 2008 09:00:52 +0000 (09:00 +0000)]
added little optimization to not add twice the same arc

16 years agoquinck and untested implementation of positivity conditions check
Enrico Tassi [Fri, 11 Apr 2008 16:45:29 +0000 (16:45 +0000)]
quinck and untested implementation of positivity conditions check

16 years ago...
Enrico Tassi [Fri, 11 Apr 2008 15:25:15 +0000 (15:25 +0000)]
...

16 years agoadded depndency of new kernel to metadata to allow to use the DB to calculate the...
Enrico Tassi [Fri, 11 Apr 2008 15:20:27 +0000 (15:20 +0000)]
added depndency of new kernel to metadata to allow to use the DB to calculate the minimum set of graphs to load

16 years agoFIXED bug, added assertion in case a universe inside a term T living at URI u
Enrico Tassi [Fri, 11 Apr 2008 15:19:31 +0000 (15:19 +0000)]
FIXED bug, added assertion in case a universe inside a term T living at URI u
was marked with URI v <> u. Unshare.fresh_types should be called!

added a function to linearize a given graph, imperative interface since
is is used only in the new kernel.

16 years agoadded function to fresh types
Enrico Tassi [Fri, 11 Apr 2008 15:16:33 +0000 (15:16 +0000)]
added function to fresh types

16 years agocall Unshare.fresh_types
Enrico Tassi [Fri, 11 Apr 2008 15:15:46 +0000 (15:15 +0000)]
call Unshare.fresh_types

16 years agoload the graph of objects that depend on the ones requested,
Enrico Tassi [Fri, 11 Apr 2008 15:15:21 +0000 (15:15 +0000)]
load the graph of objects that depend on the ones requested,
rank universes and use them in the transformation to obtain terms
with TypeK and not always Type0

16 years agouse universe rank instead of Type0
Enrico Tassi [Fri, 11 Apr 2008 15:13:47 +0000 (15:13 +0000)]
use universe rank instead of Type0

16 years agoType related failures fixed
Enrico Tassi [Fri, 11 Apr 2008 15:13:09 +0000 (15:13 +0000)]
Type related failures fixed

16 years agobetter pp of objects
Enrico Tassi [Fri, 11 Apr 2008 15:12:30 +0000 (15:12 +0000)]
better pp of objects

16 years agoExtracted code. The main executable is medium_tests that runs the emulator on
Claudio Sacerdoti Coen [Fri, 11 Apr 2008 13:09:02 +0000 (13:09 +0000)]
Extracted code. The main executable is medium_tests that runs the emulator on
a few assembly programs with inputs of different sizes:
  * string reverse
  * counting sort
  * perfect numbers

16 years agoremoved useless file
Enrico Tassi [Fri, 11 Apr 2008 13:07:54 +0000 (13:07 +0000)]
removed useless file

16 years agofixed modules order
Enrico Tassi [Fri, 11 Apr 2008 11:40:49 +0000 (11:40 +0000)]
fixed modules order

16 years agomore fix removed from types
Enrico Tassi [Fri, 11 Apr 2008 11:10:12 +0000 (11:10 +0000)]
more fix removed from types

16 years agomore fix removed from types in proofs
Enrico Tassi [Fri, 11 Apr 2008 11:01:53 +0000 (11:01 +0000)]
more fix removed from types in proofs

16 years agowhen we build the elimination principle we fresh universes to not
Enrico Tassi [Fri, 11 Apr 2008 10:33:49 +0000 (10:33 +0000)]
when we build the elimination principle we fresh universes to not
generate tems with different

16 years agoadded a parameter to unshare universes
Enrico Tassi [Fri, 11 Apr 2008 10:21:45 +0000 (10:21 +0000)]
added a parameter to unshare universes

16 years agoConversion of 2 lambdas was not requiring equality on universes of the source type...
Enrico Tassi [Fri, 11 Apr 2008 10:20:34 +0000 (10:20 +0000)]
Conversion of 2 lambdas was not requiring equality on universes of the source type, while the conversion of products was requiring so.
Moreover Coq seems to force that constraint too.

16 years agocontext of types built in the reverse order
Enrico Tassi [Fri, 11 Apr 2008 10:16:56 +0000 (10:16 +0000)]
context of types built in the reverse order

16 years agoadded a simplify to prevent the generation of an ugly fix
Enrico Tassi [Fri, 11 Apr 2008 10:16:00 +0000 (10:16 +0000)]
added a simplify to prevent the generation of an ugly fix

16 years agoimplemented inductive and less parentheses
Enrico Tassi [Fri, 11 Apr 2008 08:16:23 +0000 (08:16 +0000)]
implemented inductive and less parentheses

16 years agoThe cache of objects is now used also for cofixpoints.
Claudio Sacerdoti Coen [Thu, 10 Apr 2008 18:19:16 +0000 (18:19 +0000)]
The cache of objects is now used also for cofixpoints.

16 years agoNew: cache of translated fixpoints (to avoid the generative fix restriction and
Claudio Sacerdoti Coen [Thu, 10 Apr 2008 18:14:47 +0000 (18:14 +0000)]
New: cache of translated fixpoints (to avoid the generative fix restriction and
to avoid pollution of the environment). Many more Matita objects now pass.

TODO: the caching machinery should be debugged and better understood (what about
metasenv and subst?)