]> matita.cs.unibo.it Git - helm.git/log
helm.git
11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 8 Mar 2013 13:47:28 +0000 (13:47 +0000)]
update in basic_2

11 years agoimproved "big treee" computation allows to close a case in the
Ferruccio Guidi [Fri, 8 Mar 2013 13:33:29 +0000 (13:33 +0000)]
improved "big treee" computation allows to close a case in the
preservation proof

11 years agoBug fixed: let-rec defined propositions are no longer extracted.
Claudio Sacerdoti Coen [Mon, 4 Mar 2013 01:31:00 +0000 (01:31 +0000)]
Bug fixed: let-rec defined propositions are no longer extracted.
They used to be extracted, but in the interface the type abstraction was
wrong.

11 years agoupdate in basic_2
Ferruccio Guidi [Sun, 3 Mar 2013 18:54:10 +0000 (18:54 +0000)]
update in basic_2

11 years ago- lambdadelta: we removed focalized reduction from snv preservation
Ferruccio Guidi [Sun, 3 Mar 2013 18:52:14 +0000 (18:52 +0000)]
- lambdadelta: we removed focalized reduction from snv preservation
- matitadep: bug fix in loop detection

11 years agoupdate in basic_2
Ferruccio Guidi [Thu, 28 Feb 2013 18:15:19 +0000 (18:15 +0000)]
update in basic_2

11 years ago- lambdadelta: first recursive part of preservation finally proved!
Ferruccio Guidi [Thu, 28 Feb 2013 18:14:27 +0000 (18:14 +0000)]
- lambdadelta: first recursive part of preservation finally proved!
- lambda: bugfix in include paths, now they are relative to the root
- matita.lang: keyword "fact" added (used in lambdadelta)

11 years agochapter2 revisited
Andrea Asperti [Thu, 28 Feb 2013 16:22:28 +0000 (16:22 +0000)]
chapter2 revisited

11 years agoQuick patch: the maxmeta is now pushed/popped when compiling an external file.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:19:28 +0000 (20:19 +0000)]
Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.

11 years agoQuick patch: the maxmeta is now pushed/popped when compiling an external file.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:19:04 +0000 (20:19 +0000)]
Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.

11 years agoBug fixed: composite coercions were not extracted.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:18:18 +0000 (20:18 +0000)]
Bug fixed: composite coercions were not extracted.

11 years agoBug fixed that reveals a new one: in case of inductive types defined via
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:17:41 +0000 (20:17 +0000)]
Bug fixed that reveals a new one: in case of inductive types defined via
let rec, it used to happen that a "type 'a foo" in the .mli was implemented
by a "type 'a foo" in the .ml. Now the opposite happens in other situations.

11 years agoFerruccio's removal of objects commented out because it breaks compilation of
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 18:30:24 +0000 (18:30 +0000)]
Ferruccio's removal of objects commented out because it breaks compilation of
the standard library!

11 years agoChapter 1 revisited
Andrea Asperti [Wed, 27 Feb 2013 16:48:15 +0000 (16:48 +0000)]
Chapter 1 revisited

11 years agowhen we serialize the contents of a .ma, we remove the old objects
Ferruccio Guidi [Mon, 25 Feb 2013 21:22:24 +0000 (21:22 +0000)]
when we serialize the contents of a .ma, we remove the old objects
before adding the new ones

11 years ago- xhtbl: now double quotes can appear in string literals
Ferruccio Guidi [Sun, 24 Feb 2013 18:25:57 +0000 (18:25 +0000)]
- xhtbl: now double quotes can appear in string literals
         built-in help completed

11 years ago- nUri : added Sets of uris for use in "probe"
Ferruccio Guidi [Sun, 24 Feb 2013 16:20:34 +0000 (16:20 +0000)]
- nUri : added Sets of uris for use in "probe"
- probe: now we can exclude the objects of dismissed sources
  (those in .matita/ but not in the development as .ma)
- lambdadelta: Makefile now uses the new feature of "probe"

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 22 Feb 2013 21:54:29 +0000 (21:54 +0000)]
update in basic_2

11 years ago- "big tree" order implemented
Ferruccio Guidi [Fri, 22 Feb 2013 21:47:07 +0000 (21:47 +0000)]
- "big tree" order implemented
- some annotations

11 years agotrace added in a failing invocation of auto :-(
Ferruccio Guidi [Mon, 18 Feb 2013 21:50:27 +0000 (21:50 +0000)]
trace added in a failing invocation of auto :-(

11 years agoupdate in basic_2
Ferruccio Guidi [Mon, 18 Feb 2013 19:41:43 +0000 (19:41 +0000)]
update in basic_2

11 years agosubstitution lemma for stratified native validity!
Ferruccio Guidi [Mon, 18 Feb 2013 19:40:13 +0000 (19:40 +0000)]
substitution lemma for stratified native validity!

11 years agoupdate in basic_2 summary
Ferruccio Guidi [Fri, 15 Feb 2013 18:54:16 +0000 (18:54 +0000)]
update in basic_2 summary

11 years agowe rephrased sstas in terms of star
Ferruccio Guidi [Fri, 15 Feb 2013 18:52:30 +0000 (18:52 +0000)]
we rephrased sstas in terms of star

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 15 Feb 2013 14:21:51 +0000 (14:21 +0000)]
update in basic_2

11 years agowe reformulate the extended computation to simplify the proof of its
Ferruccio Guidi [Fri, 15 Feb 2013 14:17:58 +0000 (14:17 +0000)]
we reformulate the extended computation to simplify the proof of its
normalization property

11 years agostatistics update in basic_2
Ferruccio Guidi [Wed, 13 Feb 2013 15:48:46 +0000 (15:48 +0000)]
statistics update in basic_2

11 years ago- first piece of the mutual induction for preservation finally closed!
Ferruccio Guidi [Wed, 13 Feb 2013 15:41:00 +0000 (15:41 +0000)]
- first piece of the mutual induction for preservation finally closed!
- a conjecture closed

11 years agoan update in basic_2
Ferruccio Guidi [Mon, 11 Feb 2013 22:58:04 +0000 (22:58 +0000)]
an update in basic_2

11 years agomore service lemmas in nat and lambdadelta
Ferruccio Guidi [Mon, 11 Feb 2013 22:56:54 +0000 (22:56 +0000)]
more service lemmas in nat and lambdadelta

11 years agoone table was nissing ...
Ferruccio Guidi [Thu, 7 Feb 2013 19:54:16 +0000 (19:54 +0000)]
one table was nissing ...

11 years agoupdate in basic_2
Ferruccio Guidi [Thu, 7 Feb 2013 19:50:22 +0000 (19:50 +0000)]
update in basic_2

11 years agoeven more service lemmas ...
Ferruccio Guidi [Thu, 7 Feb 2013 18:58:52 +0000 (18:58 +0000)]
even more service lemmas ...

11 years agoA few integrations
Andrea Asperti [Thu, 7 Feb 2013 09:15:07 +0000 (09:15 +0000)]
A few integrations

11 years agorestructuring
Andrea Asperti [Thu, 7 Feb 2013 09:14:39 +0000 (09:14 +0000)]
restructuring

11 years ago(no commit message)
Andrea Asperti [Thu, 7 Feb 2013 09:13:27 +0000 (09:13 +0000)]

11 years agorestructuring
Andrea Asperti [Thu, 7 Feb 2013 09:10:31 +0000 (09:10 +0000)]
restructuring

11 years agoupdate in basic_2
Ferruccio Guidi [Wed, 6 Feb 2013 20:58:01 +0000 (20:58 +0000)]
update in basic_2

11 years ago- lambdadelta: more service lemmas ...
Ferruccio Guidi [Wed, 6 Feb 2013 20:51:46 +0000 (20:51 +0000)]
- lambdadelta: more service lemmas ...
- matitadep: bug fix due to new invocation from Makefile

11 years agosome missing files ...
Ferruccio Guidi [Tue, 5 Feb 2013 17:50:19 +0000 (17:50 +0000)]
some missing files ...

11 years agoBug fixed: .ml/.mli files were opened/closed even when ocaml extraction was
Claudio Sacerdoti Coen [Tue, 5 Feb 2013 13:16:22 +0000 (13:16 +0000)]
Bug fixed: .ml/.mli files were opened/closed even when ocaml extraction was
not active.

11 years agoBug fixed: "open X" were not printed in .mli because streams are destructive.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 22:38:43 +0000 (22:38 +0000)]
Bug fixed: "open X" were not printed in .mli because streams are destructive.

11 years agoFlushing needed before closing the channel.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 22:36:52 +0000 (22:36 +0000)]
Flushing needed before closing the channel.

11 years agoImproved exception handling.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 22:35:57 +0000 (22:35 +0000)]
Improved exception handling.

11 years agoBug fixed in pretty printing of mutual inductive types.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 20:27:04 +0000 (20:27 +0000)]
Bug fixed in pretty printing of mutual inductive types.

11 years agoBug fixed: the indty can be typed with a Prod, not only with a Sort.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 18:09:37 +0000 (18:09 +0000)]
Bug fixed: the indty can be typed with a Prod, not only with a Sort.

11 years agoNew option -extract_ocaml to extract to ocaml files.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 17:38:31 +0000 (17:38 +0000)]
New option -extract_ocaml to extract to ocaml files.

11 years agoPretty printing of ocaml files slightly improved.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 17:35:10 +0000 (17:35 +0000)]
Pretty printing of ocaml files slightly improved.

11 years agoLast known bug unrelated to names fixed: a fixpoint that creates a type used
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 17:27:38 +0000 (17:27 +0000)]
Last known bug unrelated to names fixed: a fixpoint that creates a type used
to be extracted in the wrong way.

11 years agostate mte2 renamed to mte_acc
Wilmer Ricciotti [Mon, 4 Feb 2013 16:18:55 +0000 (16:18 +0000)]
state mte2 renamed to mte_acc

11 years ago...
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 15:55:41 +0000 (15:55 +0000)]
...

11 years agoconverting certain basic machines to composed machines
Wilmer Ricciotti [Mon, 4 Feb 2013 15:46:19 +0000 (15:46 +0000)]
converting certain basic machines to composed machines

11 years agodefs.ma was never really used
Wilmer Ricciotti [Mon, 4 Feb 2013 11:14:36 +0000 (11:14 +0000)]
defs.ma was never really used

11 years agoMakefile to extract to ocaml code.
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:44:07 +0000 (00:44 +0000)]
Makefile to extract to ocaml code.

11 years agoOops, part of last commit (ocaml extraction implementation)
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:41:54 +0000 (00:41 +0000)]
Oops, part of last commit (ocaml extraction implementation)

11 years agoOoops, this completes the previous commit (ocaml extraction implementation).
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:38:55 +0000 (00:38 +0000)]
Ooops, this completes the previous commit (ocaml extraction implementation).

11 years agoImplementation of Ocaml extraction (largely ported from Coq).
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:38:05 +0000 (00:38 +0000)]
Implementation of Ocaml extraction (largely ported from Coq).
Note: yet to be thoroughly debugged.

In order to use, recompile everything with "OCAML_EXTRACTION=1 ocamlc".

11 years agoIdentity change, improves readability.
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:30:45 +0000 (00:30 +0000)]
Identity change, improves readability.

11 years ago- Now the nodes count does not include the generated objects
Ferruccio Guidi [Fri, 1 Feb 2013 19:33:42 +0000 (19:33 +0000)]
- Now the nodes count does not include the generated objects

11 years agolambda finaly moved in lib
Ferruccio Guidi [Fri, 1 Feb 2013 16:37:41 +0000 (16:37 +0000)]
lambda finaly moved in lib

11 years agomatch now only uses the new move operation
Wilmer Ricciotti [Fri, 1 Feb 2013 15:38:39 +0000 (15:38 +0000)]
match now only uses the new move operation

11 years ago- ng_refiner:
Ferruccio Guidi [Fri, 1 Feb 2013 13:47:25 +0000 (13:47 +0000)]
- ng_refiner:
  now the expected type is `XTNone (was None), `XTSome (was Some, also
  was `Term), `XTSort (any sort, was `Sort), `XTInd (any (co)inductive type).
  `XTProd (was `Prod) is used in "try_coercions"
- we replaced some instances of None with `XTSort or `XTInd through the code.
  lib, lambda, and lambdadelta compile,
  in case of errors like "the term ... is not a sort" or
  "the term ... is not a (co)inductive type", revert to `XTNone in the
  corresponding check.
- Now generated objects have the `Generated attribute properly set
- lambda: many "?" removed because of the improvement in the refiner
          other instances of "?" removed for other reasons

11 years agoSpeed-up in match.ma.
Wilmer Ricciotti [Tue, 29 Jan 2013 11:47:42 +0000 (11:47 +0000)]
Speed-up in match.ma.

11 years agoProved old axiom.
Wilmer Ricciotti [Tue, 29 Jan 2013 10:46:18 +0000 (10:46 +0000)]
Proved old axiom.

11 years agoYippeee! Completes proof of soundness of the universal machine
Wilmer Ricciotti [Tue, 29 Jan 2013 10:36:18 +0000 (10:36 +0000)]
Yippeee! Completes proof of soundness of the universal machine
(multi-tape formalization).

11 years agounistep!!!
Andrea Asperti [Mon, 28 Jan 2013 21:18:58 +0000 (21:18 +0000)]
unistep!!!

11 years agoupdate in basic_2
Ferruccio Guidi [Mon, 28 Jan 2013 18:35:43 +0000 (18:35 +0000)]
update in basic_2

11 years ago- notation change for weight functions (following lambda)
Ferruccio Guidi [Mon, 28 Jan 2013 18:25:59 +0000 (18:25 +0000)]
- notation change for weight functions (following lambda)
  that used to clash with the lref construction
- some parentheses added arround application arguments

11 years agofunzioni ausiliarie
Andrea Asperti [Mon, 28 Jan 2013 17:14:23 +0000 (17:14 +0000)]
funzioni ausiliarie

11 years agocfg_in_table_to_tuple
Wilmer Ricciotti [Mon, 28 Jan 2013 15:02:23 +0000 (15:02 +0000)]
cfg_in_table_to_tuple

11 years agosem_copy_strict
Wilmer Ricciotti [Mon, 28 Jan 2013 12:11:22 +0000 (12:11 +0000)]
sem_copy_strict

11 years agomany axioms and daemons removed
Wilmer Ricciotti [Sun, 27 Jan 2013 21:30:24 +0000 (21:30 +0000)]
many axioms and daemons removed

11 years agoquasi finito
Andrea Asperti [Sun, 27 Jan 2013 17:44:49 +0000 (17:44 +0000)]
quasi finito

11 years agowell-foundedness done
Wilmer Ricciotti [Sun, 27 Jan 2013 16:31:44 +0000 (16:31 +0000)]
well-foundedness done

11 years agosem_exec_move completed
Andrea Asperti [Sun, 27 Jan 2013 14:38:20 +0000 (14:38 +0000)]
sem_exec_move completed

11 years agoalmost there
Andrea Asperti [Sun, 27 Jan 2013 12:58:58 +0000 (12:58 +0000)]
almost there

11 years agoA lot of changes
Andrea Asperti [Sat, 26 Jan 2013 21:24:19 +0000 (21:24 +0000)]
A lot of changes

11 years agoSplitted unistep_aux
Andrea Asperti [Fri, 25 Jan 2013 23:18:36 +0000 (23:18 +0000)]
Splitted unistep_aux
Added another semantics for cfg_to_obj

11 years agostarted unistep
Wilmer Ricciotti [Fri, 25 Jan 2013 18:31:33 +0000 (18:31 +0000)]
started unistep

11 years agoprogress in termination
Wilmer Ricciotti [Fri, 25 Jan 2013 14:15:04 +0000 (14:15 +0000)]
progress in termination

11 years ago- paths and left residuals: forth case of the equivalence proved!
Ferruccio Guidi [Fri, 25 Jan 2013 12:12:29 +0000 (12:12 +0000)]
- paths and left residuals: forth case of the equivalence proved!
  The proof is now complete!!

11 years agofinished semantics for termination of match machine
Wilmer Ricciotti [Thu, 24 Jan 2013 15:47:47 +0000 (15:47 +0000)]
finished semantics for termination of match machine

11 years agoprogress
Wilmer Ricciotti [Thu, 24 Jan 2013 12:31:43 +0000 (12:31 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 24 Jan 2013 09:38:30 +0000 (09:38 +0000)]
progress

11 years ago- paths and left residuals: third case of the equivalence proved!
Ferruccio Guidi [Wed, 23 Jan 2013 19:32:59 +0000 (19:32 +0000)]
- paths and left residuals: third case of the equivalence proved!

11 years agoprogress
Wilmer Ricciotti [Wed, 23 Jan 2013 07:41:41 +0000 (07:41 +0000)]
progress

11 years agotermination!
Andrea Asperti [Tue, 22 Jan 2013 14:37:41 +0000 (14:37 +0000)]
termination!

11 years agoUniversal machine
Andrea Asperti [Tue, 22 Jan 2013 12:21:58 +0000 (12:21 +0000)]
Universal machine

11 years agoRemoved all axioms in unistep_aux
Wilmer Ricciotti [Tue, 22 Jan 2013 09:57:18 +0000 (09:57 +0000)]
Removed all axioms in unistep_aux

11 years agoremoved daemons
Wilmer Ricciotti [Mon, 21 Jan 2013 15:53:26 +0000 (15:53 +0000)]
removed daemons

11 years agouniversal
Andrea Asperti [Mon, 21 Jan 2013 12:50:06 +0000 (12:50 +0000)]
universal

11 years agotape_move_obj completed (modulo daemons)
Wilmer Ricciotti [Mon, 21 Jan 2013 12:38:56 +0000 (12:38 +0000)]
tape_move_obj completed (modulo daemons)

11 years agocfg_to_obj completed (modulo daemons)
Wilmer Ricciotti [Mon, 21 Jan 2013 11:06:23 +0000 (11:06 +0000)]
cfg_to_obj completed (modulo daemons)

11 years agoprogress
Wilmer Ricciotti [Mon, 21 Jan 2013 10:01:46 +0000 (10:01 +0000)]
progress

11 years agosemantics of unistep
Andrea Asperti [Sun, 20 Jan 2013 12:31:17 +0000 (12:31 +0000)]
semantics of unistep

11 years ago- paths and left residuals: second case of the equivalence proved!
Ferruccio Guidi [Fri, 18 Jan 2013 23:27:46 +0000 (23:27 +0000)]
- paths and left residuals: second case of the equivalence proved!
- some additions to lstar and Allr

11 years agoprogress in cfg_to_obj
Wilmer Ricciotti [Fri, 18 Jan 2013 15:55:16 +0000 (15:55 +0000)]
progress in cfg_to_obj

11 years agocopy char form obj to cfg at the end
Andrea Asperti [Fri, 18 Jan 2013 12:03:48 +0000 (12:03 +0000)]
copy char form obj to cfg at the end

11 years agohigh level semantics
Andrea Asperti [Fri, 18 Jan 2013 11:41:17 +0000 (11:41 +0000)]
high level semantics

11 years agohigh level semantics
Andrea Asperti [Fri, 18 Jan 2013 11:08:33 +0000 (11:08 +0000)]
high level semantics