| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
comportement est similaire à la 8.1). Les records récursifs peuvent-être
déclarés avec Inductive et CoInductive, avec les effets idoines sur leur
nature.
J'ai fait quelques changements dans VernacInductive pour que tout ceci
fonctionne bien ensemble. Il reste du nettoyage à faire et probablement
des ajustement dans le Printing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11808 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
==========
This big patch is commited here with a HUGE experimental tag on it. It
is probably not a finished job. The aim of committing it now, as
agreed with Hugo, is to get some feedback from potential users to
identify more clearly the directions the implementation could take. So
please feel free to mail me any remarks, bug reports or advices at
<puech@cs.unibo.it>.
Here are the changes induced by it :
For the user
============
* Search tools have been reimplemented to be faster and more
general. Affected are [SearchPattern], [SearchRewrite] and [Search]
(not [SearchAbout] yet). Changes are:
- All of them accept general constructions, and previous syntactical
limitations are abolished. In particular, one can for example
[SearchPattern (nat -> Prop)], which will find [isSucc], but also
[le], [gt] etc.
- Patterns are typed. This means that you cannot search mistyped
expressions anymore. I'm not sure if it's a good or a bad thing
though (especially regarding coercions)...
* New tool to automatically infer (some) Record/Typeclasses instances.
Usage : [Record/Class *Infer* X := ...] flags a record/class as
subject to instance search. There is also an option to
activate/deactivate the search [Set/Unset Autoinstance]. It works
by finding combinations of definitions (actually all kinds of
objects) which forms a record instance, possibly parameterized. It
is activated at two moments:
- A complete search is done when defining a new record, to find all
possible instances that could have been formed with past
definitions. Example:
Require Import List.
Record Infer Monoid A (op:A->A->A) e :=
{ assoc : forall x y z, op x (op y z) = op (op x y) z;
idl : forall x, x = op x e ;
idr : forall x, x = op e x }.
new instance Monoid_autoinstance_1 : (Monoid nat plus 0)
[...]
- At each new declaration (Definition, Axiom, Inductive), a search
is made to find instances involving the new object. Example:
Parameter app_nil_beg : forall A (l:list A), l = nil ++ l.
new instance Build_Monoid_autoinstance_12 :
(forall H : Type, Monoid (list H) app nil) :=
(fun H : Type =>
Build_Monoid (list H) app nil ass_app (app_nil_beg H)
(app_nil_end H))
For the developper
==================
* New yet-to-be-named datastructure in [lib/dnet.ml]. Should do
efficient one-to-many or many-to-one non-linear first-order
filtering, faster than traditional methods like discrimination nets
(so yes, the name of the file should probably be changed).
* Comes with its application to Coq's terms
[pretyping/term_dnet.ml]. Terms are represented so that you can
search for patterns under products as fast as you would do not under
products, and facilities are provided to express other kind of
searches (head of application, under equality, whatever you need
that can be expressed as a pattern)
* A global repository of all objects defined and imported is
maintained [toplevel/libtypes.ml], with all search facilities
described before.
* A certain kind of proof search in [toplevel/autoinstance.ml]. For
the moment it is specialized on finding instances, but it should be
generalizable and reusable (more on this in a few months :-).
The bad news
============
* Compile time should increase by 0 to 15% (depending on the size of
the Requires done). This could be optimized greatly by not
performing substitutions on modules which are not functors I
think. There may also be some inefficiency sources left in my code
though...
* Vo's also gain a little bit of weight (20%). That's inevitable if I
wanted to store the big datastructure of objects, but could also be
optimized some more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
guessing the binding name by default and making all generalized
variables implicit. At the same time, continue refactoring of
Record/Class/Inductive etc.., getting rid of [VernacRecord]
definitively. The AST is not completely satisfying, but leaning towards
Record/Class as restrictions of inductive (Arnaud, anyone ?).
Now, [Class] declaration bodies are either of the form [meth : type] or
[{ meth : type ; ... }], distinguishing singleton "definitional" classes
and inductive classes based on records. The constructor syntax is
accepted ([meth1 : type1 | meth1 : type2]) but raises an error
immediately, as support for defining a class by a general inductive type
is not there yet (this is a bugfix!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11625 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11624 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
declaration code to toplevel/record, including support for singleton
classes as definitions. Parsing code also factorized. Arnaud: one more
thing to think about when refactoring the definitions in vernacentries.
Add support for specifying what to do with anonymous variables in
contexts during internalisation (fixes bug #1982), current choice is to
generate a name for typeclass bindings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
for record fields (using "someproj : sometype where not := constr" syntax). Only one
notation allowed currently and no redeclaration after the record
declaration either (will be done for typeclasses).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
CoInductive stream (A:Type) := { hd : A ; tl : stream A }.
Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }.
L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de
la syntaxe qui était apparue dans la 8.2beta pour les records
coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive"
comme maintenant).
VernacRecord et VernacInductive semblent maintenant faire doublon, il
doit y avoir moyen de les fusionner.
Les records mutuellement inductifs restent aussi à faire.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
It solves feature request 1852, makes me and Arnaud happy and
will permit to factor some more code in typeclasses.
- Records are introduced using the syntax "{| x := t; y := foo |}" and
"with" clauses are currently parsed but not yet supported in the
elaboration. You are invited to suggest other syntaxes :)
- Missing fields are turned into holes, extra fields cause an error
message. The current implementation finds the type of the record
at pretyping time, from the typing constraint alone (and just expects
an inductive with one constructor). It is then impossible to use
scope information to parse the bodies: that may be wrong. The other
solution I see is using the fields to detect the type earlier, before
internalisation of the bodies, but then we get in name clash hell.
- In funind/contrib/interface I mostly put [assert false] everywhere to
avoid warnings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
[in I] := t [return pred] in b", just as SSReflect does with let:.
Change implementation: no longer a separate AST node, just add a case_style
annotation on Cases to indicate it (if ML was dependently typed we
could ensure that LetPatternStyle Cases have only one term to be
matched and one branch, alas...). This factors out most code and we lose
no functionality (win ! win !). Add LetPat.v test suite.
- Slight improvement of inference of return clauses for dependent
pattern matching. If matching a variable of non-dependent type
under a tycon that mentions it while giving no return clause, the
dependency will be automatically infered. Examples at the end of
DepPat. Should get rid of most explicit returns under tycons.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10676 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
backwards compatible. Update CHANGES with things i've done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from
svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses
........
r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
Comment grammar error
........
r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
The initial Type Classes patch.
This patch introduces type classes and instance definitions a la Haskell.
Technically, it uses the implicit arguments mechanism which was extended a bit.
The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac).
........
r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
Fix interface
........
r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
Fix more xlate code
........
r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
Bug fixes in Instance decls.
........
r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
Streamline typeclass context implementation, prepare for class binders in proof statements.
........
r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
Stupid bug
........
r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
Other bugs related to naming in typeclasses fixed.
........
r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
Progress on setoids using type classes, recognize setoid equalities in hyps better.
Streamline implementation to return more information when resolving setoids (return the results setoid).
........
r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
Syntax change, more like Coq
........
r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
Work on type classes based rewrite tactic.
........
r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
Forgot to add a file
........
r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and
implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations.
Add useful tactics to Program.Subsets.
........
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
obligations (even an opaque one).
Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9182 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
(+ uniformisation position notation dans les blocs inductifs et récursifs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9081 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
generation des graphes de Function
+ Correction d'un petit bug dans les lemmes d'inversions de Function
+ Nettoyage d'hypotheses inutile dans les obligations de preuve de Function (wf et measure).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9053 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
+ Code cleaning un Function code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9036 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9014 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9003 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
inductive
- bug correction in "Functional scheme" and "functional inversion": the
function are now parsed as references and not indent
- adding a zeta normalization function in rawtermops to zeta normalize
graph constructions (not used for now)
- Bug correction in generation of functional principle types (if an
arguments of the function has a type which is a sort)
- adding a new persistent table for functional induction informations
(graph,...)
- new save mechanism for functional induction principles (reuse of
proofs when possible)
- Minor bug correction in proof of principle.
- Distinguishing building_principles (that is save them) and making then
(just construct their proof term)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9000 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8841 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Fixing .depend (forgot to remove new_arg_principles dependencies in last commit
)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8786 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
to files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8781 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
des inductifs de la clause "in" du filtrage.
- Débogage et extension du parseur xml (g_xml.ml4)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8755 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
+ Correcting a bug in recursives funcitons detection in GenFixpoint
+ Parially handling applied binders in funcitonal principles generation tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
+ New tactic to prove functions schemes
+ Add a command "Generate graph for <functionname>" to generate automatiquelly
the graph associated to a function (usefull only when the function
has not been defined by GenFixpoint).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8694 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8620 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
is_empty in those versions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
+ Compatibility with new induction
+ Induction principle for general recursion preparation still continuing
+ Cleaning dead code ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8055 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
+ Recursive definition (repository contrib/recdef) can now be used with GenFixpoint syntax by just replacing the usual {struct x} annotation by {wf R x} where x is one of the function declared arguments and R is a expression well-typed in the x typing environment.
+ Bug correction in new functional induction
+ For now no induction principle for general recursive definition is generated.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
Benjamin Gregoire, Gilles Barthe.
For the moment, it is as followed:
If one uses GenFixpoint instead of Fixpoint, then induction principles
are generated on the fly (respecting the match structure written by
the user, with wildcards etc). These principles can be used directly
or by tactics "new functional induction" and "functional inversion".
We will soon make "new functional induction" become "functional
induction", before release of V8.1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
aspiwack
puech
msozeau
jforest
lmamane
herbelin
bertot
coq