diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 30 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 8 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 34 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 28 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 8 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 311 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 70 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 42 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.mli | 40 |
12 files changed, 534 insertions, 49 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 058f3d210d..e71083c509 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1408,9 +1408,9 @@ let set_arity_signature dep n arsign tomatchl pred x = let rec decomp_lam_force n avoid l p = if n = 0 then (List.rev l,p,avoid) else match p with - | RLambda (_,(Name id as na),_,c) -> + | RLambda (_,(Name id as na),_,_,c) -> decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c + | RLambda (_,(Anonymous as na),_,_,c) -> decomp_lam_force (n-1) avoid (na::l) c | _ -> let x = next_ident_away (id_of_string "x") avoid in decomp_lam_force (n-1) (x::avoid) (Name x :: l) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2cfa7076ae..a9e550bf7c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -268,7 +268,7 @@ let is_nondep_branch c n = let extract_nondep_branches test c b n = let rec strip n r = if n=0 then r else match r with - | RLambda (_,_,_,t) -> strip (n-1) t + | RLambda (_,_,_,_,t) -> strip (n-1) t | RLetIn (_,_,_,t) -> strip (n-1) t | _ -> assert false in if test c n then Some (strip n b) else None @@ -276,7 +276,7 @@ let extract_nondep_branches test c b n = let it_destRLambda_or_LetIn_names n c = let rec aux n nal c = if n=0 then (List.rev nal,c) else match c with - | RLambda (_,na,_,c) -> aux (n-1) (na::nal) c + | RLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c | RLetIn (_,na,_,c) -> aux (n-1) (na::nal) c | _ -> (* eta-expansion *) @@ -308,7 +308,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | Some p -> let nl,typ = it_destRLambda_or_LetIn_names k p in let n,typ = match typ with - | RLambda (_,x,t,c) -> x, c + | RLambda (_,x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = if List.for_all ((=) Anonymous) nl then None @@ -444,14 +444,14 @@ and share_names isgoal n l avoid env c t = let t = detype isgoal avoid env t in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) env in - share_names isgoal (n-1) ((Name id,None,t)::l) avoid env c c' + share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env c c' (* May occur for fix built interactively *) | LetIn (na,b,t',c), _ when n > 0 -> let t' = detype isgoal avoid env t' in let b = detype isgoal avoid env b in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) env in - share_names isgoal n ((Name id,Some b,t')::l) avoid env c t + share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c t (* Only if built with the f/n notation or w/o let-expansion in types *) | _, LetIn (_,b,_,t) when n > 0 -> share_names isgoal n l avoid env c (subst1 b t) @@ -461,7 +461,7 @@ and share_names isgoal n l avoid env c t = let id = next_name_away na' avoid in let avoid = id::avoid and env = add_name (Name id) env in let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names isgoal (n-1) ((Name id,None,t')::l) avoid env appc c' + share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> if n>0 then warning "Detyping.detype: cannot factorize fix enough"; @@ -524,8 +524,8 @@ and detype_binder isgoal bk avoid env na ty c = concrete_name (avoid_flag isgoal) avoid env na c in let r = detype isgoal avoid' (add_name na' env) c in match bk with - | BProd -> RProd (dl, na',detype isgoal avoid env ty, r) - | BLambda -> RLambda (dl, na',detype isgoal avoid env ty, r) + | BProd -> RProd (dl, na',Explicit,detype isgoal avoid env ty, r) + | BLambda -> RLambda (dl, na',Explicit,detype isgoal avoid env ty, r) | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r) let rec detype_rel_context where avoid env sign = @@ -541,7 +541,7 @@ let rec detype_rel_context where avoid env sign = else concrete_name None avoid env na c in let b = Option.map (detype false avoid env) b in let t = detype false avoid env t in - (na',b,t) :: aux avoid' (add_name na' env) rest + (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest in aux avoid env (List.rev sign) (**********************************************************************) @@ -573,15 +573,15 @@ let rec subst_rawconstr subst raw = if r' == r && rl' == rl then raw else RApp(loc,r',rl') - | RLambda (loc,n,r1,r2) -> + | RLambda (loc,n,bk,r1,r2) -> let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in if r1' == r1 && r2' == r2 then raw else - RLambda (loc,n,r1',r2') + RLambda (loc,n,bk,r1',r2') - | RProd (loc,n,r1,r2) -> + | RProd (loc,n,bk,r1,r2) -> let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in if r1' == r1 && r2' == r2 then raw else - RProd (loc,n,r1',r2') + RProd (loc,n,bk,r1',r2') | RLetIn (loc,n,r1,r2) -> let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in @@ -629,10 +629,10 @@ let rec subst_rawconstr subst raw = let ra1' = array_smartmap (subst_rawconstr subst) ra1 and ra2' = array_smartmap (subst_rawconstr subst) ra2 in let bl' = array_smartmap - (list_smartmap (fun (na,obd,ty as dcl) -> + (list_smartmap (fun (na,k,obd,ty as dcl) -> let ty' = subst_rawconstr subst ty in let obd' = Option.smartmap (subst_rawconstr subst) obd in - if ty'==ty & obd'==obd then dcl else (na,obd',ty'))) + if ty'==ty & obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else RRec (loc,fix,ida,bl',ra1',ra2') diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 588bc8c849..72379dfcfa 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -41,7 +41,7 @@ val detype_case : val detype_sort : sorts -> rawsort val detype_rel_context : constr option -> identifier list -> names_context -> - rel_context -> (name * rawconstr option * rawconstr) list + rel_context -> rawdecl list (* look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_renamed : env -> constr -> identifier -> int option diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index b894a9aae9..37d60e470c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -520,11 +520,11 @@ let build_mutual_indrec env sigma = function (List.map (function (mind',mibi',mipi',dep',s') -> let (sp',_) = mind' in - if sp=sp' then + if sp=sp' then let (mibi',mipi') = lookup_mind_specif env mind' in - (mind',mibi',mipi',dep',s') - else - raise (RecursionSchemeError (NotMutualInScheme (mind,mind')))) + (mind',mibi',mipi',dep',s') + else + raise (RecursionSchemeError (NotMutualInScheme (mind,mind')))) lrecspec) in let _ = check_arities listdepkind in diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 63dfbb2d9f..845f9fae1f 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -220,10 +220,10 @@ let rec pat_of_raw metas vars = function | RApp (_,c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) - | RLambda (_,na,c1,c2) -> + | RLambda (_,na,bk,c1,c2) -> PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | RProd (_,na,c1,c2) -> + | RProd (_,na,bk,c1,c2) -> PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | RLetIn (_,na,c1,c2) -> @@ -241,7 +241,7 @@ let rec pat_of_raw metas vars = function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | RLetTuple (loc,nal,(_,None),b,c) -> - let mkRLambda c na = RLambda (loc,na,RHole (loc,Evd.InternalHole),c) in + let mkRLambda c na = RLambda (loc,na,Explicit,RHole (loc,Evd.InternalHole),c) in let c = List.fold_left mkRLambda c nal in PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b, [|pat_of_raw metas vars c|]) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9ecd7e2514..3689ae174a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -321,11 +321,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct | RRec (loc,fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt - | (na,None,ty)::bl -> + | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = (na,None,ty'.utj_val) in type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl - | (na,Some bd,ty)::bl -> + | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar ty in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in @@ -420,7 +420,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | _ -> resj in inh_conv_coerce_to_tycon loc env evdref resj tycon - | RLambda(loc,name,c1,c2) -> + | RLambda(loc,name,bk,c1,c2) -> let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in @@ -428,7 +428,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let j' = pretype rng (push_rel var env) evdref lvar c2 in judge_of_abstraction env (orelse_name name name') j j' - | RProd(loc,name,c1,c2) -> + | RProd(loc,name,bk,c1,c2) -> let j = pretype_type empty_valcon env evdref lvar c1 in let var = (name,j.utj_val) in let env' = push_rel_assum var env in @@ -652,7 +652,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct (pretype tycon env evdref lvar c).uj_val | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in - nf_evar (evars_of !evdref) c' + let evd,_ = consider_remaining_unif_problems env !evdref in + let evd = nf_evar_defs evd in + let c' = nf_evar (evars_of evd) c' in + let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in + let c' = nf_evar (evars_of evd) c' in + evdref := evd; + c' (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage @@ -680,10 +686,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in let c = pretype_gen evdref env lvar kind c in +(* let evd,_ = consider_remaining_unif_problems env !evdref in *) +(* let evd = nf_evar_defs evd in *) +(* let c = nf_evar (evars_of evd) c in *) +(* let evd = undefined_evars evd in *) +(* let evd = Typeclasses.resolve_typeclasses env sigma evd in *) +(* let c = nf_evar (evars_of evd) c in *) let evd,_ = consider_remaining_unif_problems env !evdref in - let c = nf_evar (evars_of evd) c in - if fail_evar then check_evars env sigma evd c; - evd, c + if fail_evar then check_evars env (Evd.evars_of evd) evd c; + evd, c (** Entry points of the high-level type synthesis algorithm *) @@ -701,6 +712,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_tcc_evars evdref env kind c = pretype_gen evdref env ([],[]) kind c +(* let c = pretype_gen evdref env ([],[]) kind c in *) +(* evdref := nf_evar_defs !evdref; *) +(* let c = nf_evar (evars_of !evdref) c in *) +(* let evd = undefined_evars !evdref in *) +(* let evd = Typeclasses.resolve_typeclasses env (evars_of evd) !evdref in *) +(* evdref := evd; *) +(* nf_evar (evars_of evd) c *) let understand_tcc sigma env ?expected_type:exptyp c = let evd, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index d2a3473632..bf5cc22723 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -36,6 +36,8 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option type binder_kind = BProd | BLambda | BLetIn +type binding_kind = Explicit | Implicit + type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list @@ -57,8 +59,8 @@ type rawconstr = | REvar of loc * existential_key * rawconstr list option | RPatVar of loc * (bool * patvar) (* Used for patterns only *) | RApp of loc * rawconstr * rawconstr list - | RLambda of loc * name * rawconstr * rawconstr - | RProd of loc * name * rawconstr * rawconstr + | RLambda of loc * name * binding_kind * rawconstr * rawconstr + | RProd of loc * name * binding_kind * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * @@ -71,7 +73,7 @@ type rawconstr = | RCast of loc * rawconstr * rawconstr cast_type | RDynamic of loc * Dyn.t -and rawdecl = name * rawconstr option * rawconstr +and rawdecl = name * binding_kind * rawconstr option * rawconstr and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr @@ -101,13 +103,13 @@ let cases_predicate_names tml = - boolean in POldCase means it is recursive i*) -let map_rawdecl f (na,obd,ty) = (na,Option.map f obd,f ty) +let map_rawdecl f (na,k,obd,ty) = (na,k,Option.map f obd,f ty) let map_rawconstr f = function | RVar (loc,id) -> RVar (loc,id) | RApp (loc,g,args) -> RApp (loc,f g, List.map f args) - | RLambda (loc,na,ty,c) -> RLambda (loc,na,f ty,f c) - | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c) + | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c) + | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c) | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c) | RCases (loc,rtntypopt,tml,pl) -> RCases (loc,Option.map f rtntypopt, @@ -166,8 +168,8 @@ let occur_rawconstr id = let rec occur = function | RVar (loc,id') -> id = id' | RApp (loc,f,args) -> (occur f) or (List.exists occur args) - | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) - | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) + | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) + | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c)) | RCases (loc,rtntypopt,tml,pl) -> (occur_option rtntypopt) @@ -182,7 +184,7 @@ let occur_rawconstr id = not (array_for_all4 (fun fid bl ty bd -> let rec occur_fix = function [] -> not (occur ty) && (fid=id or not(occur bd)) - | (na,bbd,bty)::bl -> + | (na,k,bbd,bty)::bl -> not (occur bty) && (match bbd with Some bd -> not (occur bd) @@ -211,7 +213,7 @@ let free_rawvars = let rec vars bounded vs = function | RVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs | RApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | RLambda (loc,na,ty,c) | RProd (loc,na,ty,c) | RLetIn (loc,na,ty,c) -> + | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in vars bounded' vs' c @@ -234,7 +236,7 @@ let free_rawvars = let vars_fix i vs fid = let vs1,bounded1 = List.fold_left - (fun (vs,bounded) (na,bbd,bty) -> + (fun (vs,bounded) (na,k,bbd,bty) -> let vs' = vars_option bounded vs bbd in let vs'' = vars bounded vs' bty in let bounded' = add_name_to_ids bounded na in @@ -272,8 +274,8 @@ let loc_of_rawconstr = function | REvar (loc,_,_) -> loc | RPatVar (loc,_) -> loc | RApp (loc,_,_) -> loc - | RLambda (loc,_,_,_) -> loc - | RProd (loc,_,_,_) -> loc + | RLambda (loc,_,_,_,_) -> loc + | RProd (loc,_,_,_,_) -> loc | RLetIn (loc,_,_,_) -> loc | RCases (loc,_,_,_) -> loc | RLetTuple (loc,_,_,_,_) -> loc diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index c43c290e86..2a5dab6e40 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -40,6 +40,8 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option type binder_kind = BProd | BLambda | BLetIn +type binding_kind = Explicit | Implicit + type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list @@ -61,8 +63,8 @@ type rawconstr = | REvar of loc * existential_key * rawconstr list option | RPatVar of loc * (bool * patvar) (* Used for patterns only *) | RApp of loc * rawconstr * rawconstr list - | RLambda of loc * name * rawconstr * rawconstr - | RProd of loc * name * rawconstr * rawconstr + | RLambda of loc * name * binding_kind * rawconstr * rawconstr + | RProd of loc * name * binding_kind * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * @@ -75,7 +77,7 @@ type rawconstr = | RCast of loc * rawconstr * rawconstr cast_type | RDynamic of loc * Dyn.t -and rawdecl = name * rawconstr option * rawconstr +and rawdecl = name * binding_kind * rawconstr option * rawconstr and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml new file mode 100644 index 0000000000..b0e7cb1470 --- /dev/null +++ b/pretyping/typeclasses.ml @@ -0,0 +1,311 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Util +open Typeclasses_errors +(*i*) + +let mismatched_params env n m = mismatched_ctx_inst env Parameters n m +(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *) +let mismatched_props env n m = mismatched_ctx_inst env Properties n m + +type rels = constr list + +(* This module defines type-classes *) +type typeclass = { + cl_name : identifier; (* Name of the class *) + cl_context : named_context; (* Context in which superclasses and params are typed (usually types) *) + cl_super : named_context; (* Superclasses applied to some of the params *) + cl_params : named_context; (* Context of the parameters (usually types) *) +(* cl_defs : named_context; (\* Context of the definitions (usually functions), which may be shared *\) *) + cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *) + cl_impl : inductive; (* The class implementation: a record parameterized by params and defs *) +} + +type typeclasses = (identifier, typeclass) Gmap.t + +type instance = { + is_class: typeclass; + is_name: identifier; (* Name of the instance *) +(* is_params: named_context; (\* Context of the parameters, instanciated *\) *) +(* is_super: named_context; (\* The corresponding superclasses *\) *) +(* is_defs: named_context; (\* Context of the definitions, instanciated *\) *) + is_impl: constant; +(* is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *) +} + +type instances = (identifier, instance list) Gmap.t + +let classes : typeclasses ref = ref Gmap.empty + +let methods : (identifier, identifier) Gmap.t ref = ref Gmap.empty + +let instances : instances ref = ref Gmap.empty + +let freeze () = !classes, !methods, !instances + +let unfreeze (cl,m,is) = + classes:=cl; + methods:=m; + instances:=is + +let init () = + classes:= Gmap.empty; + methods:= Gmap.empty; + instances:= Gmap.empty + +let _ = + Summary.declare_summary "classes_and_instances" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = true; + Summary.survive_section = true } + +let gmap_merge old ne = + Gmap.fold (fun k v acc -> Gmap.add k v acc) ne old + +let gmap_list_merge old ne = + let ne = + Gmap.fold (fun k v acc -> + let oldv = try Gmap.find k old with Not_found -> [] in + let v' = + List.fold_left (fun acc x -> + if not (List.exists (fun y -> y.is_name = x.is_name) v) then x :: acc else acc) + v oldv + in Gmap.add k v' acc) + ne Gmap.empty + in + Gmap.fold (fun k v acc -> + let newv = try Gmap.find k ne with Not_found -> [] in + let v' = + List.fold_left (fun acc x -> + if not (List.exists (fun y -> y.is_name = x.is_name) acc) then x :: acc else acc) + newv v + in Gmap.add k v' acc) + old ne + +let cache (_, (cl, m, inst)) = + classes := gmap_merge !classes cl; + methods := gmap_merge !methods m; + instances := gmap_list_merge !instances inst + +open Libobject + +let subst (_,subst,(cl,m,inst)) = + let do_subst_con c = fst (Mod_subst.subst_con subst c) + and do_subst c = Mod_subst.subst_mps subst c + and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i) + in + let do_subst_named ctx = + List.map (fun (na, b, t) -> + (na, Option.smartmap do_subst b, do_subst t)) + ctx + in + let subst_class cl = + let cl' = { cl with cl_impl = do_subst_ind cl.cl_impl; + cl_context = do_subst_named cl.cl_context; + cl_super = do_subst_named cl.cl_super; + cl_params = do_subst_named cl.cl_params; + cl_props = do_subst_named cl.cl_props; } + in if cl' = cl then cl else cl' + in + let subst_inst classes insts = + List.map (fun is -> + { is with is_class = Gmap.find is.is_class.cl_name classes; + is_impl = do_subst_con is.is_impl }) insts + in + let classes = Gmap.map subst_class cl in + let instances = Gmap.map (subst_inst classes) inst in + (classes, m, instances) + +let discharge (_,(cl,m,inst)) = + let subst_class cl = + { cl with cl_impl = Lib.discharge_inductive cl.cl_impl } + in + let subst_inst classes insts = + List.map (fun is -> { is with is_impl = Lib.discharge_con is.is_impl; + is_class = Gmap.find is.is_class.cl_name classes; }) insts + in + let classes = Gmap.map subst_class cl in + let instances = Gmap.map (subst_inst classes) inst in + Some (classes, m, instances) + +let (input,output) = + declare_object + { (default_object "type classes state") with + cache_function = cache; + load_function = (fun _ -> cache); + open_function = (fun _ -> cache); + classify_function = (fun (_,x) -> Substitute x); + discharge_function = discharge; + subst_function = subst; + export_function = (fun x -> Some x) } + +let update () = + Lib.add_anonymous_leaf (input (!classes, !methods, !instances)) + +let class_methods cl = + List.map (function (x, _, _) -> x) cl.cl_props + +let add_class c = + classes := Gmap.add c.cl_name c !classes; + methods := List.fold_left (fun acc x -> Gmap.add x c.cl_name acc) !methods (class_methods c); + update () + +let class_info c = + Gmap.find c !classes + +let class_of_inductive ind = + let res = Gmap.fold + (fun k v acc -> match acc with None -> if v.cl_impl = ind then Some v else acc | _ -> acc) + !classes None + in match res with + None -> raise Not_found + | Some cl -> cl + +let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes [] + +let gmapl_add x y m = + try + let l = Gmap.find x m in + Gmap.add x (y::Util.list_except y l) m + with Not_found -> + Gmap.add x [y] m + +let instances_of c = + try Gmap.find c.cl_name !instances with Not_found -> [] + +let add_instance i = + instances := gmapl_add i.is_class.cl_name i !instances; + update () + +open Libnames + +let id_of_reference r = + let (_, id) = repr_qualid (snd (qualid_of_reference r)) in id + +let instances r = + let id = id_of_reference r in + try let cl = class_info id in instances_of cl + with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id) + +let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false) + +let resolve_typeclass env ev evi (evd, defined as acc) = + if evi.evar_body = Evar_empty then + try + !solve_instanciation_problem env evd ev evi + with Exit -> acc + else acc + +let resolve_one_typeclass env types = + try + let evi = Evd.make_evar (Environ.named_context_val env) types in + let ev = 1 in + let evm = Evd.add Evd.empty ev evi in + let evd = Evd.create_evar_defs evm in + let evd', b = !solve_instanciation_problem env evd ev evi in + if b then + let evm' = Evd.evars_of evd' in + match Evd.evar_body (Evd.find evm' ev) with + Evar_empty -> raise Not_found + | Evar_defined c -> c + else raise Not_found + with Exit -> raise Not_found + +let resolve_one_typeclass_evd env evd types = + try + let ev = Evarutil.e_new_evar evd env types in + let (ev,_) = destEvar ev in + let evd', b = + !solve_instanciation_problem env !evd ev (Evd.find (Evd.evars_of !evd) ev) + in + evd := evd'; + if b then + let evm' = Evd.evars_of evd' in + match Evd.evar_body (Evd.find evm' ev) with + Evar_empty -> raise Not_found + | Evar_defined c -> c + else raise Not_found + with Exit -> raise Not_found + +let method_typeclass ref = + match ref with + | ConstRef c -> + let (_, _, l) = Names.repr_con c in + class_info (Gmap.find (Names.id_of_label l) !methods) + | _ -> raise Not_found + +let is_class ind = + Gmap.fold (fun k v acc -> acc || v.cl_impl = ind) !classes false + +let is_implicit_arg k = + match k with + ImplicitArg (ref, (n, id)) -> true + | InternalHole -> true + | _ -> false + +let resolve_typeclasses ?(check=true) env sigma evd = + let evm = Evd.evars_of evd in + let tc_evars = + let f ev evi acc = + let (l, k) = Evd.evar_source ev evd in + if not check || is_implicit_arg k then + match kind_of_term evi.evar_concl with + | App(ki, args) when isInd ki -> + if is_class (destInd ki) then Evd.add acc ev evi + else acc + | _ -> acc + else acc + in Evd.fold f evm Evd.empty + in + let rec sat evars = + let (evars', progress) = + Evd.fold + (fun ev evi acc -> + if Evd.mem tc_evars ev then resolve_typeclass env ev evi acc else acc) + (Evd.evars_of evars) (evars, false) + in + if not progress then evars' + else + sat (Evarutil.nf_evar_defs evars') + in sat evd + +let class_of_constr c = + match kind_of_term c with + App (c, _) -> + (match kind_of_term c with + Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None) + | _ -> None) + | _ -> None + + +type substitution = (identifier * constr) list + +let substitution_of_named_context isevars env id n subst l = + List.fold_right + (fun (na, _, t) subst -> + let t' = replace_vars subst t in + let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' in + (na, b) :: subst) + l subst + +let nf_substitution sigma subst = + List.map (function (na, c) -> na, Reductionops.nf_evar sigma c) subst diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli new file mode 100644 index 0000000000..fbe48e06a2 --- /dev/null +++ b/pretyping/typeclasses.mli @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Topconstr +open Util +(*i*) + +(* This module defines type-classes *) +type typeclass = { + cl_name : identifier; (* Name of the class *) + cl_context : named_context; (* Context in which superclasses and params are typed (usually types) *) + cl_super : named_context; (* Superclasses applied to some of the params *) + cl_params : named_context; (* Context of the real parameters (types and operations) *) +(* cl_defs : rel_context; (\* Context of the definitions (usually functions), which may be shared *\) *) + cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *) + cl_impl : inductive; (* The class implementation: a record parameterized by params and defs *) +} + +type instance = { + is_class: typeclass; + is_name: identifier; (* Name of the instance *) +(* is_params: named_context; (\* Context of the parameters, instanciated *\) *) +(* is_super: named_context; (\* The corresponding superclasses *\) *) + is_impl: constant; +(* is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *) +} + +val instances : Libnames.reference -> instance list +val typeclasses : unit -> typeclass list +val add_class : typeclass -> unit +val add_instance : instance -> unit + +val class_info : identifier -> typeclass (* raises Not_found *) +val class_of_inductive : inductive -> typeclass (* raises Not_found *) + +val resolve_one_typeclass : env -> types -> types (* Raises Not_found *) +val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *) + +val is_class : inductive -> bool + +val class_of_constr : constr -> typeclass option + +val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool +val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs + +val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref + +type substitution = (identifier * constr) list + +val substitution_of_named_context : + evar_defs ref -> env -> identifier -> int -> + substitution -> named_context -> substitution + +val nf_substitution : evar_map -> substitution -> substitution diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml new file mode 100644 index 0000000000..980f327cb5 --- /dev/null +++ b/pretyping/typeclasses_errors.ml @@ -0,0 +1,42 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Topconstr +open Util +(*i*) + +type contexts = Parameters | Properties + +type typeclass_error = + | UnboundClass of identifier located + | UnboundMethod of identifier * identifier located (* Class name, method *) + | NoInstance of identifier located * constr list + | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *) + +exception TypeClassError of env * typeclass_error + +let typeclass_error env err = raise (TypeClassError (env, err)) + +let unbound_class env id = typeclass_error env (UnboundClass id) + +let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) + +let no_instance env id args = typeclass_error env (NoInstance (id, args)) + +let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli new file mode 100644 index 0000000000..fbc2f25449 --- /dev/null +++ b/pretyping/typeclasses_errors.mli @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Topconstr +open Util +(*i*) + +type contexts = Parameters | Properties + +type typeclass_error = + | UnboundClass of identifier located + | UnboundMethod of identifier * identifier located (* Class name, method *) + | NoInstance of identifier located * constr list + | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *) + +exception TypeClassError of env * typeclass_error + +val unbound_class : env -> identifier located -> 'a + +val unbound_method : env -> identifier -> identifier located -> 'a + +val no_instance : env -> identifier located -> constr list -> 'a + +val mismatched_ctx_inst : env -> contexts -> constr_expr list -> named_context -> 'a |