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

11 years agosemantics of uni_step
Andrea Asperti [Fri, 18 Jan 2013 10:32:00 +0000 (10:32 +0000)]
semantics of uni_step

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 16:01:27 +0000 (16:01 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 15:54:07 +0000 (15:54 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 15:34:55 +0000 (15:34 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 14:47:22 +0000 (14:47 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 14:05:02 +0000 (14:05 +0000)]
progress

11 years agoMoved a list comparison function in the list file
Andrea Asperti [Thu, 17 Jan 2013 14:00:11 +0000 (14:00 +0000)]
Moved a list comparison function in the list file

11 years agonormal and tuples
Andrea Asperti [Thu, 17 Jan 2013 12:59:25 +0000 (12:59 +0000)]
normal and tuples

11 years ago- paths and left residuals: first case of the equivalence proved!
Ferruccio Guidi [Wed, 16 Jan 2013 19:05:56 +0000 (19:05 +0000)]
- paths and left residuals: first case of the equivalence proved!
- some corrections and additions
- some "?" removed in customized eliminations

11 years agoadded null character to the alphabet
Wilmer Ricciotti [Wed, 16 Jan 2013 16:01:54 +0000 (16:01 +0000)]
added null character to the alphabet

11 years agoprogress
Wilmer Ricciotti [Wed, 16 Jan 2013 11:02:20 +0000 (11:02 +0000)]
progress

11 years ago- some additions and renaming ...
Ferruccio Guidi [Tue, 15 Jan 2013 20:08:08 +0000 (20:08 +0000)]
- some additions and renaming ...

11 years agoprogress in unistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 16:48:30 +0000 (16:48 +0000)]
progress in unistep_aux

11 years agounistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 15:38:57 +0000 (15:38 +0000)]
unistep_aux

11 years agomore unistep
Wilmer Ricciotti [Tue, 15 Jan 2013 15:38:11 +0000 (15:38 +0000)]
more unistep

11 years agounistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 12:29:35 +0000 (12:29 +0000)]
unistep_aux

11 years agocopy finished
Andrea Asperti [Tue, 15 Jan 2013 11:35:33 +0000 (11:35 +0000)]
copy finished

11 years ago- a few more lemmas ...
Ferruccio Guidi [Tue, 15 Jan 2013 10:34:32 +0000 (10:34 +0000)]
- a few more lemmas ...
- some renaming

11 years agocopy.ma
Andrea Asperti [Tue, 15 Jan 2013 09:45:58 +0000 (09:45 +0000)]
copy.ma

11 years agomatch.ma completed
Wilmer Ricciotti [Mon, 14 Jan 2013 16:45:27 +0000 (16:45 +0000)]
match.ma completed

11 years agomatch termination completed, still a small case ignored in wsem_match
Wilmer Ricciotti [Mon, 14 Jan 2013 16:24:17 +0000 (16:24 +0000)]
match termination completed, still a small case ignored in wsem_match

11 years agowsem_match finished
Wilmer Ricciotti [Mon, 14 Jan 2013 15:47:08 +0000 (15:47 +0000)]
wsem_match finished

11 years agoadvancement in match
Wilmer Ricciotti [Mon, 14 Jan 2013 15:14:11 +0000 (15:14 +0000)]
advancement in match

11 years agoClosed some daemons
Andrea Asperti [Mon, 14 Jan 2013 11:46:18 +0000 (11:46 +0000)]
Closed some daemons

11 years agonth_current_chars
Andrea Asperti [Mon, 14 Jan 2013 10:36:34 +0000 (10:36 +0000)]
nth_current_chars

11 years agostandardization: equivalence between paths and left residuals started
Ferruccio Guidi [Sun, 13 Jan 2013 19:10:32 +0000 (19:10 +0000)]
standardization: equivalence between paths and left residuals started

11 years agomatch almost finished
Wilmer Ricciotti [Fri, 11 Jan 2013 23:28:57 +0000 (23:28 +0000)]
match almost finished

11 years agomore porting to machines that can move without writing
Andrea Asperti [Tue, 8 Jan 2013 12:03:01 +0000 (12:03 +0000)]
more porting to machines that can move without writing

11 years agoparmove based on end of the tape
Wilmer Ricciotti [Tue, 8 Jan 2013 10:26:00 +0000 (10:26 +0000)]
parmove based on end of the tape

11 years agoporting to machine that can move without writing
Wilmer Ricciotti [Tue, 8 Jan 2013 09:16:34 +0000 (09:16 +0000)]
porting to machine that can move without writing

11 years agodependences update
Ferruccio Guidi [Sun, 6 Jan 2013 20:09:18 +0000 (20:09 +0000)]
dependences update

11 years agorefactoring ...
Ferruccio Guidi [Sun, 6 Jan 2013 16:17:47 +0000 (16:17 +0000)]
refactoring ...

11 years agoPorted permutation.ma and fermat_little_theorem.ma
Andrea Asperti [Sat, 5 Jan 2013 16:22:16 +0000 (16:22 +0000)]
Ported permutation.ma and fermat_little_theorem.ma

11 years agorefactoring
Andrea Asperti [Thu, 3 Jan 2013 16:49:01 +0000 (16:49 +0000)]
refactoring

11 years agoRefactoring
Andrea Asperti [Thu, 3 Jan 2013 16:33:59 +0000 (16:33 +0000)]
Refactoring

11 years agoChebishev ported
Andrea Asperti [Thu, 3 Jan 2013 16:15:54 +0000 (16:15 +0000)]
Chebishev ported

11 years agolambda: some refactoring + support for subsets of subterms started
Ferruccio Guidi [Wed, 2 Jan 2013 22:12:53 +0000 (22:12 +0000)]
lambda: some refactoring + support for subsets of subterms started
core_notation: some "term 19" added
predefined_virtuals: an addition

11 years ago- probe: new application to compute some data on the proof objects of
Ferruccio Guidi [Tue, 1 Jan 2013 23:01:20 +0000 (23:01 +0000)]
- probe: new application to compute some data on the proof objects of
a development, such as their net size (aka intrinsinc complexity)
- lambdadelta: Makefile now asks "probe" fore some data

11 years agoupdate in basic_2
Ferruccio Guidi [Sun, 30 Dec 2012 13:11:10 +0000 (13:11 +0000)]
update in basic_2

11 years agocommit completed! some bugs fixed and some instances of auto resized
Ferruccio Guidi [Sun, 30 Dec 2012 13:00:21 +0000 (13:00 +0000)]
commit completed! some bugs fixed and some instances of auto resized

11 years agoxoa: change in naming convenctions for existential quantifies
Ferruccio Guidi [Fri, 28 Dec 2012 16:32:01 +0000 (16:32 +0000)]
xoa: change in naming convenctions for existential quantifies
     to cope with ex2 in lib
lib: some additions
lambdadelta: partial commit in basic_2: just grammar, substitution,
unfold, static

11 years ago- lambda_delta: programmed renaming to lambdadelta
Ferruccio Guidi [Tue, 25 Dec 2012 21:48:14 +0000 (21:48 +0000)]
- lambda_delta: programmed renaming to lambdadelta
- nat: general weight-based eliminator added for lambdadelta

11 years ago- we introduced the pointer_step rc in the perspective of proving
Ferruccio Guidi [Sun, 23 Dec 2012 15:02:32 +0000 (15:02 +0000)]
- we introduced the pointer_step rc in the perspective of proving
results on head normal forms
- some renaming

11 years agosome renaming ...
Ferruccio Guidi [Fri, 21 Dec 2012 18:12:41 +0000 (18:12 +0000)]
some renaming ...

11 years agoone file was missing .... :(
Ferruccio Guidi [Fri, 21 Dec 2012 18:06:10 +0000 (18:06 +0000)]
one file was missing .... :(

11 years agoMany changes
Andrea Asperti [Fri, 21 Dec 2012 12:39:18 +0000 (12:39 +0000)]
Many changes