]> matita.cs.unibo.it Git - helm.git/log
helm.git
17 years agoremoved dust
Enrico Tassi [Mon, 12 Nov 2007 16:38:46 +0000 (16:38 +0000)]
removed dust

17 years agoHIDDEN (since glade do not read out file properly anymore) tactic bar and
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

17 years agonew file with some relations stated in Type
Enrico Tassi [Mon, 12 Nov 2007 15:22:59 +0000 (15:22 +0000)]
new file with some relations stated in Type

17 years agoordered set is over, much new stuff coming from a coreflexivee/cotransitive
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.

17 years agorefactoring
Ferruccio Guidi [Mon, 12 Nov 2007 12:35:56 +0000 (12:35 +0000)]
refactoring

17 years agoold subst tactics removed. New destruct tactic used instead
Ferruccio Guidi [Sat, 10 Nov 2007 16:54:55 +0000 (16:54 +0000)]
old subst tactics removed. New destruct tactic used instead

17 years agoa) Detection of existential types now implemented
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.

17 years agoMore correct (but still bugged) implementation of type definition.
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 13:16:57 +0000 (13:16 +0000)]
More correct (but still bugged) implementation of type definition.

17 years agoDead code removed.
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 11:05:00 +0000 (11:05 +0000)]
Dead code removed.
More ocaml keywords.

17 years agosnapshot
Enrico Tassi [Fri, 9 Nov 2007 13:37:05 +0000 (13:37 +0000)]
snapshot

17 years ago...
Enrico Tassi [Fri, 9 Nov 2007 08:39:33 +0000 (08:39 +0000)]
...

17 years ago- subst tactic keyword removed from highlight syntax tables
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

17 years agoTrivial bug fixed in type inference of LetIn source types.
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 21:46:15 +0000 (21:46 +0000)]
Trivial bug fixed in type inference of LetIn source types.

17 years agoxxx
Enrico Tassi [Thu, 8 Nov 2007 17:03:23 +0000 (17:03 +0000)]
xxx

17 years agoported to the new destruct
Enrico Tassi [Thu, 8 Nov 2007 14:54:31 +0000 (14:54 +0000)]
ported to the new destruct

17 years agoArguments of constructors in a case pattern are now ppid-ed.
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.

17 years agosvn:ignore set
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 14:02:56 +0000 (14:02 +0000)]
svn:ignore set

17 years agoplease, commit files with debug=false otherwise the distributed matita prints a ton...
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

17 years agoforced associativity in if construct
Enrico Tassi [Thu, 8 Nov 2007 12:28:12 +0000 (12:28 +0000)]
forced associativity in if construct

17 years agoZoli's note (in Italian) about a constructive version of Lebesgue's dominated
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.

17 years agoset svn:ignore to *.ml in the deve directories
Ferruccio Guidi [Wed, 7 Nov 2007 20:24:34 +0000 (20:24 +0000)]
set svn:ignore to *.ml in the deve directories

17 years ago- bug fix in destruct
Ferruccio Guidi [Wed, 7 Nov 2007 19:52:14 +0000 (19:52 +0000)]
- bug fix in destruct
- old subst tactic removed
- some tests fixed

17 years agoreorganization of the whole story, the root dir contains the algebraic structure
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

17 years agoCode extraction unbranched again.
Enrico Tassi [Wed, 7 Nov 2007 14:39:07 +0000 (14:39 +0000)]
Code extraction unbranched again.

17 years agonew implementation of the destruct tactic,
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)

17 years agocic_acic should be compiled before cic_exportation
Claudio Sacerdoti Coen [Tue, 6 Nov 2007 12:29:13 +0000 (12:29 +0000)]
cic_acic should be compiled before cic_exportation

17 years agoBug in detection of too polymorphic types partially fixed (see comment).
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).

17 years agoMutCases that occur in types should be handled with "any type".
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.

17 years agoObj.magic are now generated to extract dependently typed MutCases.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 14:29:47 +0000 (14:29 +0000)]
Obj.magic are now generated to extract dependently typed MutCases.

17 years agoHandling of left parameters of constructors/indutive type definitions improved.
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.

17 years agoSlightly nicer output.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 12:18:15 +0000 (12:18 +0000)]
Slightly nicer output.

17 years agoFilenames are now fully mangled (e.g. matita_nat_nat.ml) to avoid file name
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.

17 years agoType application and abstractions are now exported correctly.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 10:10:33 +0000 (10:10 +0000)]
Type application and abstractions are now exported correctly.

17 years agoNew OCaml keyword "val".
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 09:48:59 +0000 (09:48 +0000)]
New OCaml keyword "val".

17 years ago"f" => "aux" to avoid name clashes
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 09:27:14 +0000 (09:27 +0000)]
"f" => "aux" to avoid name clashes

17 years agoThe type parameters in an inductive type declaration should be the left ones,
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.

17 years agoType arguments are better uncapitalized.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 18:55:44 +0000 (18:55 +0000)]
Type arguments are better uncapitalized.

17 years agoEmpty types not in Prop and empty types elimination handled correctly.
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.

17 years agoEmpty and singleton type elimination are now handled properly.
Claudio Sacerdoti Coen [Sun, 4 Nov 2007 18:34:01 +0000 (18:34 +0000)]
Empty and singleton type elimination are now handled properly.

17 years ago1. type definitions of propositions are no longer exported even if parametric
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

17 years agoBug fixed: qualified names were not generated correctly when the dirname was not
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.

17 years ago* type definitions that define a new proposition are no longer exported
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

17 years agoCicExportation branched. Change "if false" with "if true" to activate automatic
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.

17 years agoAll exported names are now qualified. This avoids the need for "open" statements.
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.

17 years agoAll 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.

17 years ago*** Very experimental and not branched ***
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.

17 years ago- tacticals: new tactical ifs added: uses thens where if_ uses then_
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

17 years agoAdded an hook useful in many situations.
Claudio Sacerdoti Coen [Fri, 2 Nov 2007 16:02:52 +0000 (16:02 +0000)]
Added an hook useful in many situations.

17 years agofinisced configuration section
Enrico Tassi [Fri, 2 Nov 2007 14:16:23 +0000 (14:16 +0000)]
finisced configuration section

17 years agoadded doc for db and getter sections
Enrico Tassi [Fri, 2 Nov 2007 13:07:27 +0000 (13:07 +0000)]
added doc for db and getter sections

17 years agoadded notes about sqlite and removed obsolete zack repository
Enrico Tassi [Fri, 2 Nov 2007 12:19:08 +0000 (12:19 +0000)]
added notes about sqlite and removed obsolete zack repository

17 years agoNew image from Tassi's PhD thesis.
Claudio Sacerdoti Coen [Wed, 31 Oct 2007 15:46:37 +0000 (15:46 +0000)]
New image from Tassi's PhD thesis.

17 years agobetter implementation of if_
Ferruccio Guidi [Tue, 30 Oct 2007 19:40:06 +0000 (19:40 +0000)]
better implementation of if_

17 years agoremade dependencies that were wrong
Enrico Tassi [Tue, 30 Oct 2007 10:47:37 +0000 (10:47 +0000)]
remade dependencies that were wrong

17 years ago- destruct: core of subst tactic implemented,
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)

17 years ago reverted matita db configuration fixed
Ferruccio Guidi [Mon, 29 Oct 2007 16:13:47 +0000 (16:13 +0000)]
 reverted matita db configuration fixed

17 years agoBug fixed: patterns in hypotheses under binders where not computed correctly
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.

17 years agoNew syntax for match patterns in terms and in patterns.
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 22:25:56 +0000 (22:25 +0000)]
New syntax for match patterns in terms and in patterns.

17 years agoThe document was not valid. Fixed.
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 22:25:32 +0000 (22:25 +0000)]
The document was not valid. Fixed.

17 years agoPretty-printing of "match ... with" pattern syntax fixed. We need an
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 ]

17 years agoNil => nil, Cons => cons
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 16:10:53 +0000 (16:10 +0000)]
Nil => nil, Cons => cons

17 years agoNil => nil; Cons => cons
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 16:07:10 +0000 (16:07 +0000)]
Nil => nil; Cons => cons

17 years agoNew syntax for match patterns.
Claudio Sacerdoti Coen [Sun, 28 Oct 2007 16:05:41 +0000 (16:05 +0000)]
New syntax for match patterns.
New semantics for destruct.

17 years agoclean can't fail
Enrico Tassi [Sun, 28 Oct 2007 13:50:04 +0000 (13:50 +0000)]
clean can't fail

17 years agoadded patch for the configuration file
Enrico Tassi [Sun, 28 Oct 2007 13:49:42 +0000 (13:49 +0000)]
added patch for the configuration file

17 years agoreverted last commit
Enrico Tassi [Sun, 28 Oct 2007 13:10:17 +0000 (13:10 +0000)]
reverted last commit

17 years ago...
Enrico Tassi [Fri, 26 Oct 2007 12:48:33 +0000 (12:48 +0000)]
...

17 years agorebuilt
Enrico Tassi [Fri, 26 Oct 2007 12:48:18 +0000 (12:48 +0000)]
rebuilt

17 years agono -rectype passed to ocamldep
Enrico Tassi [Fri, 26 Oct 2007 12:48:03 +0000 (12:48 +0000)]
no -rectype passed to ocamldep

17 years agorebuilt
Enrico Tassi [Fri, 26 Oct 2007 12:47:38 +0000 (12:47 +0000)]
rebuilt

17 years ago0.4.0 almost working
Enrico Tassi [Fri, 26 Oct 2007 12:47:30 +0000 (12:47 +0000)]
0.4.0 almost working

17 years agoSyntax of patterns changed (and not documented yet).
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...

17 years agoWildcard patterns implemented in case analysis. The following term is now
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
  ]

17 years agowe use ulex08 not ulex
Enrico Tassi [Fri, 26 Oct 2007 10:14:01 +0000 (10:14 +0000)]
we use ulex08 not ulex

17 years agobug fix in injection e relocate term
Ferruccio Guidi [Thu, 25 Oct 2007 21:36:13 +0000 (21:36 +0000)]
bug fix in injection e relocate term

17 years agoneg => Qneg :-)
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 17:10:25 +0000 (17:10 +0000)]
neg => Qneg :-)

17 years agotrue and false were swapped!
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 17:01:32 +0000 (17:01 +0000)]
true and false were swapped!

17 years agoflase => false :-)
Claudio Sacerdoti Coen [Thu, 25 Oct 2007 16:59:55 +0000 (16:59 +0000)]
flase => false :-)

17 years agoOoops. In previous commit I forgot to subtract the left arguments in case
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.

17 years agoBug fixed: case analysis where a case had not the expected number of arguments
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.

17 years agoBug fixed: a MutCase considering a wrong number of cases 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.

17 years agoBug fixed: a MutCase with missing or exceeding 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!

17 years ago1. More localization: interpretation errors are now loosely localized.
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

17 years agoRecently introduced bug fixed: error localization was not working properly for
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".

17 years agobug fix in injection: we have to recur on the generated premises
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

17 years agowe revisited the implementation of the destruct tactic in the perspective of joining...
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

17 years agoDebugging code improved.
Claudio Sacerdoti Coen [Wed, 24 Oct 2007 14:40:47 +0000 (14:40 +0000)]
Debugging code improved.

17 years ago- new function for general relocation of local references (rels) in terms
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

17 years agofixed copyright file... an ITP should be done
Enrico Tassi [Mon, 22 Oct 2007 09:48:12 +0000 (09:48 +0000)]
fixed copyright file... an ITP should be done

17 years agoInteresting. Do we need many more inversion lemmas? (Or a different and
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?).

17 years agofixed make opt
Enrico Tassi [Tue, 16 Oct 2007 11:57:51 +0000 (11:57 +0000)]
fixed make opt

17 years agoDOS-style CR+LF added to the blanks list.
Claudio Sacerdoti Coen [Tue, 16 Oct 2007 09:55:32 +0000 (09:55 +0000)]
DOS-style CR+LF added to the blanks list.

17 years agoDead code clean-up.
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 14:01:47 +0000 (14:01 +0000)]
Dead code clean-up.

17 years agoThe behaviour of autobatch paramodulation has changed.
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?

17 years agonatural number => Coq natural number
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.

17 years agonatural number => Coq natural number
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.

17 years agonatural number => Coq natural number
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:34:37 +0000 (11:34 +0000)]
natural number => Coq natural number

17 years agoWrong test patched.
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:32:46 +0000 (11:32 +0000)]
Wrong test patched.

17 years agonatural number => Coq natural number
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:29:57 +0000 (11:29 +0000)]
natural number => Coq natural number

17 years agodiscriminate.ma => destruct.ma
Claudio Sacerdoti Coen [Mon, 15 Oct 2007 11:29:21 +0000 (11:29 +0000)]
discriminate.ma => destruct.ma