]> matita.cs.unibo.it Git - helm.git/log
helm.git
11 years agochapters 2 e 3
Andrea Asperti [Sun, 10 Mar 2013 14:08:14 +0000 (14:08 +0000)]
chapters 2 e 3

11 years agowe removed a useless assertion that was forcing matita to edit just matita files
Ferruccio Guidi [Sun, 10 Mar 2013 12:01:43 +0000 (12:01 +0000)]
we removed a useless assertion that was forcing matita to edit just matita files
matita's editor is good on its own and has interesting facilities including predefined virtuals
in lambdadelta we use matita to edit the .tbl files containing notation from the .ma's
and we use matita as well to edit predefined_virtuals.ml
we still wonder how we could do this up to now despite the assertion!

11 years ago- update in basic_2
Ferruccio Guidi [Sat, 9 Mar 2013 22:32:07 +0000 (22:32 +0000)]
- update in basic_2
- contrib specific web pages moved out
- improved Makefiles

11 years agobasic_2_src.tbl was not updated :(
Ferruccio Guidi [Sat, 9 Mar 2013 22:26:54 +0000 (22:26 +0000)]
basic_2_src.tbl was not updated :(

11 years ago- lenv refinement for stratified native validity redefined
Ferruccio Guidi [Sat, 9 Mar 2013 17:14:31 +0000 (17:14 +0000)]
- lenv refinement for stratified native validity redefined
- contrib specufic web pages moved here

11 years agosecond recursive part of preservation finally proved!
Ferruccio Guidi [Fri, 8 Mar 2013 19:48:14 +0000 (19:48 +0000)]
second recursive part of preservation finally proved!

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