diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-19 17:58:43 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-19 17:58:43 +0000 |
commit | 1f31ca099259fbea08a7fef56e1989283aec040a (patch) | |
tree | 90064d4985a02321746c63027a8045fff9f2cb62 /interp | |
parent | e5ca537c17ad96529b4b39c7dbff0f25cd53b3a6 (diff) |
Do another pass on the typeclasses code. Correct globalization of class
names, gives the ability to specify qualified classes in instance
declarations. Use that in the class_tactics code.
Refine the implementation of classes. For singleton classes the
implementation of the class becomes a regular definition (into Type or
Prop). The single method becomes a 'trivial' projection that allows to
launch typeclass resolution. Each instance is just a definition as
usual. Examples in theories/Classes/RelationClasses. This permits to
define [Class reflexive A (R : relation A) := refl : forall x, R x
x.]. The definition of [reflexive] that is generated is the same as the
original one. We just need a way to declare arbitrary lemmas as
instances of a particular class to retrofit existing reflexivity lemmas
as typeclass instances of the [reflexive] class.
Also debug rewriting under binders in setoid_rewrite to allow rewriting
with lemmas which capture the bound variables when applied (works only
with setoid_rewrite, as rewrite first matches the lemma with the entire,
closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal
[exists x, P (f x)].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10697 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r-- | interp/implicit_quantifiers.ml | 15 | ||||
-rw-r--r-- | interp/implicit_quantifiers.mli | 9 |
2 files changed, 13 insertions, 11 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8a0b940b1..3b2b5d3d4 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -159,12 +159,12 @@ let compute_context_vars env l = let destClassApp cl = match cl with - | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l + | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l | _ -> raise Not_found - + let destClassAppExpl cl = match cl with - | CApp (loc, (None,CRef (Ident f)), l) -> f, l + | CApp (loc, (None,CRef ref), l) -> loc, ref, l | _ -> raise Not_found let full_class_binders env l = @@ -173,12 +173,13 @@ let full_class_binders env l = List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> match bk with Explicit -> - let (id, l) = destClassAppExpl cl in + let (loc, id, l) = destClassAppExpl cl in + let gr = Nametab.global id in (try - let c = class_info (snd id) in + let c = class_info gr in let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in - (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid - with Not_found -> unbound_class (Global.env ()) id) + (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid + with Not_found -> not_a_class (Global.env ()) (constr_of_global gr)) | Implicit -> (x :: l', avoid)) ([], avoid) l in List.rev l' diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 4ea95fc43..9ecdcd6c0 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -20,12 +20,13 @@ open Mod_subst open Rawterm open Topconstr open Util +open Libnames open Typeclasses (*i*) val ids_of_list : identifier list -> Idset.t -val destClassApp : constr_expr -> identifier located * constr_expr list -val destClassAppExpl : constr_expr -> identifier located * (constr_expr * explicitation located option) list +val destClassApp : constr_expr -> loc * reference * constr_expr list +val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list val free_vars_of_constr_expr : Topconstr.constr_expr -> ?bound:Idset.t -> @@ -55,10 +56,10 @@ val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list val combine_params : Names.Idset.t -> - (Names.Idset.t -> (Names.identifier * bool) option * (Names.identifier * Term.constr option * Term.types) -> + (Names.Idset.t -> (global_reference * bool) option * (Names.identifier * Term.constr option * Term.types) -> Topconstr.constr_expr * Names.Idset.t) -> (Topconstr.constr_expr * Topconstr.explicitation located option) list -> - ((Names.identifier * bool) option * Term.named_declaration) list -> + ((global_reference * bool) option * Term.named_declaration) list -> Topconstr.constr_expr list * Names.Idset.t |