]>
matita.cs.unibo.it Git - helm.git/log
Enrico Tassi [Mon, 12 Nov 2007 16:38:46 +0000 (16:38 +0000)]
removed dust
Enrico Tassi [Mon, 12 Nov 2007 16:38:25 +0000 (16:38 +0000)]
HIDDEN (since glade do not read out file properly anymore) tactic bar and
outline notebook tab
Enrico Tassi [Mon, 12 Nov 2007 15:22:59 +0000 (15:22 +0000)]
new file with some relations stated in Type
Enrico Tassi [Mon, 12 Nov 2007 15:22:43 +0000 (15:22 +0000)]
ordered set is over, much new stuff coming from a coreflexivee/cotransitive
execedence relation.
Ferruccio Guidi [Mon, 12 Nov 2007 12:35:56 +0000 (12:35 +0000)]
refactoring
Ferruccio Guidi [Sat, 10 Nov 2007 16:54:55 +0000 (16:54 +0000)]
old subst tactics removed. New destruct tactic used instead
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 14:07:13 +0000 (14:07 +0000)]
a) Detection of existential types now implemented
b) New heuristic for pretty printing of type definition arguments.
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 13:16:57 +0000 (13:16 +0000)]
More correct (but still bugged) implementation of type definition.
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 11:05:00 +0000 (11:05 +0000)]
Dead code removed.
More ocaml keywords.
Enrico Tassi [Fri, 9 Nov 2007 13:37:05 +0000 (13:37 +0000)]
snapshot
Enrico Tassi [Fri, 9 Nov 2007 08:39:33 +0000 (08:39 +0000)]
...
Ferruccio Guidi [Thu, 8 Nov 2007 22:01:54 +0000 (22:01 +0000)]
- subst tactic keyword removed from highlight syntax tables
- svn:ignore property fixed for Base-2 devel
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 21:46:15 +0000 (21:46 +0000)]
Trivial bug fixed in type inference of LetIn source types.
Enrico Tassi [Thu, 8 Nov 2007 17:03:23 +0000 (17:03 +0000)]
xxx
Enrico Tassi [Thu, 8 Nov 2007 14:54:31 +0000 (14:54 +0000)]
ported to the new destruct
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 14:06:13 +0000 (14:06 +0000)]
Arguments of constructors in a case pattern are now ppid-ed.
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 14:02:56 +0000 (14:02 +0000)]
svn:ignore set
Enrico Tassi [Thu, 8 Nov 2007 12:33:11 +0000 (12:33 +0000)]
please, commit files with debug=false otherwise the distributed matita prints a ton of dust
Enrico Tassi [Thu, 8 Nov 2007 12:28:12 +0000 (12:28 +0000)]
forced associativity in if construct
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 08:43:02 +0000 (08:43 +0000)]
Zoli's note (in Italian) about a constructive version of Lebesgue's dominated
convergence theorem in a point-free setting.
Ferruccio Guidi [Wed, 7 Nov 2007 20:24:34 +0000 (20:24 +0000)]
set svn:ignore to *.ml in the deve directories
Ferruccio Guidi [Wed, 7 Nov 2007 19:52:14 +0000 (19:52 +0000)]
- bug fix in destruct
- old subst tactic removed
- some tests fixed
Enrico Tassi [Wed, 7 Nov 2007 14:44:24 +0000 (14:44 +0000)]
reorganization of the whole story, the root dir contains the algebraic structure
Enrico Tassi [Wed, 7 Nov 2007 14:39:07 +0000 (14:39 +0000)]
Code extraction unbranched again.
Ferruccio Guidi [Tue, 6 Nov 2007 19:30:16 +0000 (19:30 +0000)]
new implementation of the destruct tactic,
which includes the old subst tactic (now removed)
Claudio Sacerdoti Coen [Tue, 6 Nov 2007 12:29:13 +0000 (12:29 +0000)]
cic_acic should be compiled before cic_exportation
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 15:14:23 +0000 (15:14 +0000)]
Bug in detection of too polymorphic types partially fixed (see comment).
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 14:56:16 +0000 (14:56 +0000)]
MutCases that occur in types should be handled with "any type".
Unfortunately, such type does not exists in OCaml. For now I generate
unit with a comment. Applications to arguments will fail and require another
Obj.magic.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 14:29:47 +0000 (14:29 +0000)]
Obj.magic are now generated to extract dependently typed MutCases.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 14:20:20 +0000 (14:20 +0000)]
Handling of left parameters of constructors/indutive type definitions improved.
Bug fixed: arguments of sort Prop were not dropped from MutCase branches.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 12:18:15 +0000 (12:18 +0000)]
Slightly nicer output.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 12:10:34 +0000 (12:10 +0000)]
Filenames are now fully mangled (e.g. matita_nat_nat.ml) to avoid file name
clashes.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 10:10:33 +0000 (10:10 +0000)]
Type application and abstractions are now exported correctly.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 09:48:59 +0000 (09:48 +0000)]
New OCaml keyword "val".
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 09:27:14 +0000 (09:27 +0000)]
"f" => "aux" to avoid name clashes
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 19:17:22 +0000 (19:17 +0000)]
The type parameters in an inductive type declaration should be the left ones,
that are replicated in every constructor. They used to be listed n times for
an inductive type with n constructors.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 18:55:44 +0000 (18:55 +0000)]
Type arguments are better uncapitalized.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 18:52:32 +0000 (18:52 +0000)]
Empty types not in Prop and empty types elimination handled correctly.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 18:34:01 +0000 (18:34 +0000)]
Empty and singleton type elimination are now handled properly.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 18:27:05 +0000 (18:27 +0000)]
1. type definitions of propositions are no longer exported even if parametric
2. arguments of type definitions are now printed correctly according to
OCaml awful syntax
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 18:24:57 +0000 (18:24 +0000)]
Bug fixed: qualified names were not generated correctly when the dirname was not
empty.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 17:44:37 +0000 (17:44 +0000)]
* type definitions that define a new proposition are no longer exported
* type arguments of type Prop are no longer abstracted in inductive types
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 17:26:29 +0000 (17:26 +0000)]
CicExportation branched. Change "if false" with "if true" to activate automatic
exportation of OCaml files during compilation.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 17:25:25 +0000 (17:25 +0000)]
All exported names are now qualified. This avoids the need for "open" statements.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 17:24:52 +0000 (17:24 +0000)]
All names are now qualified. This avoids the need for "open" statements.
Claudio Sacerdoti Coen [Fri, 2 Nov 2007 18:05:40 +0000 (18:05 +0000)]
*** Very experimental and not branched ***
Exportation to OCaml partially implement in cic_exportation.
It can already export several files from the freescale development (also not
committed yet).
Still to be implemented:
a) erasure of term dependencies from types
b) extraction of "open" statements
[ I do not know how to implement this! ]
c) extraction from CurrentProof
d) extraction from Let-In
e) extraction from CoFix
f) extraction from mutually recursive inductive types and Fix
Known bugs/missing features:
1) All the "classical" ones (described, for instance, in Letouzey's papers).
In particular, terms may diverge, singleton elimination and false
elimination not implemented in the correct way, Obj.magic not generated
where needed, etc.
2) Name clashes can be generated by the extraction. OCaml keywords may be
chosen. And so on.
Ferruccio Guidi [Fri, 2 Nov 2007 17:36:33 +0000 (17:36 +0000)]
- tacticals: new tactical ifs added: uses thens where if_ uses then_
- ProofEngineHelpers: namer_of exported from GrafiteEngine
Claudio Sacerdoti Coen [Fri, 2 Nov 2007 16:02:52 +0000 (16:02 +0000)]
Added an hook useful in many situations.
Enrico Tassi [Fri, 2 Nov 2007 14:16:23 +0000 (14:16 +0000)]
finisced configuration section
Enrico Tassi [Fri, 2 Nov 2007 13:07:27 +0000 (13:07 +0000)]
added doc for db and getter sections
Enrico Tassi [Fri, 2 Nov 2007 12:19:08 +0000 (12:19 +0000)]
added notes about sqlite and removed obsolete zack repository
Claudio Sacerdoti Coen [Wed, 31 Oct 2007 15:46:37 +0000 (15:46 +0000)]
New image from Tassi's PhD thesis.
Ferruccio Guidi [Tue, 30 Oct 2007 19:40:06 +0000 (19:40 +0000)]
better implementation of if_
Enrico Tassi [Tue, 30 Oct 2007 10:47:37 +0000 (10:47 +0000)]
remade dependencies that were wrong
Ferruccio Guidi [Mon, 29 Oct 2007 19:11:26 +0000 (19:11 +0000)]
- destruct: core of subst tactic implemented,
must be linked to destruct in order to work
- "if" tactical implemented (used by core subst tactic) - to be tested
- added freqently used constant hole = Cic.Implicit (Some 'Hole)
Ferruccio Guidi [Mon, 29 Oct 2007 16:13:47 +0000 (16:13 +0000)]
reverted matita db configuration fixed
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 23:26:30 +0000 (23:26 +0000)]
Bug fixed: patterns in hypotheses under binders where not computed correctly
because of a bad and wrong hack. Replaced with a correct solution. However, a
better unimplemented one exists (see new comment).
Note: copy&paste as multiple pattern not implemented yet. But it seems very
easy to do.
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 22:25:56 +0000 (22:25 +0000)]
New syntax for match patterns in terms and in patterns.
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 22:25:32 +0000 (22:25 +0000)]
The document was not valid. Fixed.
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 21:56:23 +0000 (21:56 +0000)]
Pretty-printing of "match ... with" pattern syntax fixed. We need an
~output_type flag since the semantics of patterns is slightly different from
the semantics of terms (and maybe this was a very bad choice I made):
match p return p with [ _ => p | ... | _ => p ]
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 16:10:53 +0000 (16:10 +0000)]
Nil => nil, Cons => cons
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 16:07:10 +0000 (16:07 +0000)]
Nil => nil; Cons => cons
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 16:05:41 +0000 (16:05 +0000)]
New syntax for match patterns.
New semantics for destruct.
Enrico Tassi [Sun, 28 Oct 2007 13:50:04 +0000 (13:50 +0000)]
clean can't fail
Enrico Tassi [Sun, 28 Oct 2007 13:49:42 +0000 (13:49 +0000)]
added patch for the configuration file
Enrico Tassi [Sun, 28 Oct 2007 13:10:17 +0000 (13:10 +0000)]
reverted last commit
Enrico Tassi [Fri, 26 Oct 2007 12:48:33 +0000 (12:48 +0000)]
...
Enrico Tassi [Fri, 26 Oct 2007 12:48:18 +0000 (12:48 +0000)]
rebuilt
Enrico Tassi [Fri, 26 Oct 2007 12:48:03 +0000 (12:48 +0000)]
no -rectype passed to ocamldep
Enrico Tassi [Fri, 26 Oct 2007 12:47:38 +0000 (12:47 +0000)]
rebuilt
Enrico Tassi [Fri, 26 Oct 2007 12:47:30 +0000 (12:47 +0000)]
0.4.0 almost working
Claudio Sacerdoti Coen [Fri, 26 Oct 2007 12:37:21 +0000 (12:37 +0000)]
Syntax of patterns changed (and not documented yet).
It is now:
match p with [ _ => p | ... | _ => p ]
(use lambda-abstractions for dummy arguments). Hmmm...
Claudio Sacerdoti Coen [Fri, 26 Oct 2007 12:26:59 +0000 (12:26 +0000)]
Wildcard patterns implemented in case analysis. The following term is now
accepted:
match n with
[ A => O
| B m => m
| _ => O
]
Enrico Tassi [Fri, 26 Oct 2007 10:14:01 +0000 (10:14 +0000)]
we use ulex08 not ulex
Ferruccio Guidi [Thu, 25 Oct 2007 21:36:13 +0000 (21:36 +0000)]
bug fix in injection e relocate term
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 17:10:25 +0000 (17:10 +0000)]
neg => Qneg :-)
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 17:01:32 +0000 (17:01 +0000)]
true and false were swapped!
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 16:59:55 +0000 (16:59 +0000)]
flase => false :-)
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 16:57:04 +0000 (16:57 +0000)]
Ooops. In previous commit I forgot to subtract the left arguments in case
analysis.
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 16:53:12 +0000 (16:53 +0000)]
Bug fixed: case analysis where a case had not the expected number of arguments
was not detected.
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 16:41:20 +0000 (16:41 +0000)]
Bug fixed: a MutCase considering a wrong number of cases was not detected.
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 16:35:32 +0000 (16:35 +0000)]
Bug fixed: a MutCase with missing or exceeding cases was not detected!
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 16:23:06 +0000 (16:23 +0000)]
1. More localization: interpretation errors are now loosely localized.
2. Interpretation of pattern matching highly improved:
a) missing branches are now detected
b) additional branches are now detected
c) permutated branches are handled correctly
Still to do:
d) check that every constructor is given as parameters exactly the
number of expected arguments
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 15:28:04 +0000 (15:28 +0000)]
Recently introduced bug fixed: error localization was not working properly for
the error "more arguments than expected".
Ferruccio Guidi [Wed, 24 Oct 2007 17:24:18 +0000 (17:24 +0000)]
bug fix in injection: we have to recur on the generated premises
Ferruccio Guidi [Wed, 24 Oct 2007 16:10:11 +0000 (16:10 +0000)]
we revisited the implementation of the destruct tactic in the perspective of joining the subst tactic to it
Claudio Sacerdoti Coen [Wed, 24 Oct 2007 14:40:47 +0000 (14:40 +0000)]
Debugging code improved.
Ferruccio Guidi [Wed, 24 Oct 2007 10:50:58 +0000 (10:50 +0000)]
- new function for general relocation of local references (rels) in terms
- swapped names injection and injection1
Enrico Tassi [Mon, 22 Oct 2007 09:48:12 +0000 (09:48 +0000)]
fixed copyright file... an ITP should be done
Claudio Sacerdoti Coen [Tue, 16 Oct 2007 21:39:28 +0000 (21:39 +0000)]
Interesting. Do we need many more inversion lemmas? (Or a different and
dumbier inversion tactic?).
Enrico Tassi [Tue, 16 Oct 2007 11:57:51 +0000 (11:57 +0000)]
fixed make opt
Claudio Sacerdoti Coen [Tue, 16 Oct 2007 09:55:32 +0000 (09:55 +0000)]
DOS-style CR+LF added to the blanks list.
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 14:01:47 +0000 (14:01 +0000)]
Dead code clean-up.
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:38:14 +0000 (11:38 +0000)]
The behaviour of autobatch paramodulation has changed.
But autobatch works! Is the test still correct?
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:36:49 +0000 (11:36 +0000)]
natural number => Coq natural number
The behaviour of paramodulation has changed.
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:35:32 +0000 (11:35 +0000)]
natural number => Coq natural number
The behaviour of demodulate has changed.
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:34:37 +0000 (11:34 +0000)]
natural number => Coq natural number
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:32:46 +0000 (11:32 +0000)]
Wrong test patched.
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:29:57 +0000 (11:29 +0000)]
natural number => Coq natural number
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:29:21 +0000 (11:29 +0000)]
discriminate.ma => destruct.ma