diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 431 |
1 files changed, 213 insertions, 218 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 216a0611..b85c6721 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: typeclasses.ml 12189 2009-06-15 05:08:44Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Names @@ -21,8 +21,20 @@ open Nametab open Mod_subst open Util open Typeclasses_errors +open Libobject (*i*) + +let add_instance_hint_ref = ref (fun id pri -> assert false) +let register_add_instance_hint = + (:=) add_instance_hint_ref +let add_instance_hint id = !add_instance_hint_ref id + +let set_typeclass_transparency_ref = ref (fun id pri -> assert false) +let register_set_typeclass_transparency = + (:=) set_typeclass_transparency_ref +let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c + 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 @@ -32,284 +44,265 @@ type rels = constr list (* This module defines type-classes *) type typeclass = { (* The class implementation *) - cl_impl : global_reference; + cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : (global_reference * bool) option list * rel_context; + cl_context : (global_reference * bool) option list * rel_context; (* Context of definitions and properties on defs, will not be shared *) cl_props : rel_context; - + (* The method implementaions as projections. *) cl_projs : (identifier * constant option) list; } +module Gmap = Fmap.Make(RefOrdered) -type typeclasses = (global_reference, typeclass) Gmap.t +type typeclasses = typeclass Gmap.t type instance = { is_class: global_reference; is_pri: int option; - (* Sections where the instance should be redeclared, - -1 for discard, 0 for none, mutable to avoid redeclarations + (* Sections where the instance should be redeclared, + -1 for discard, 0 for none, mutable to avoid redeclarations when multiple rebuild_object happen. *) - is_global: int ref; - is_impl: constant; + is_global: int; + is_impl: global_reference; } -type instances = (global_reference, instance Cmap.t) Gmap.t +type instances = (instance Gmap.t) Gmap.t let instance_impl is = is.is_impl -let new_instance cl pri glob impl = +let new_instance cl pri glob impl = let global = - if Lib.sections_are_opened () then - if glob then Lib.sections_depth () - else -1 - else 0 + if glob then Lib.sections_depth () + else -1 in { is_class = cl.cl_impl; is_pri = pri ; - is_global = ref global ; + is_global = global ; is_impl = impl } - + +(* + * states management + *) + let classes : typeclasses ref = ref Gmap.empty -let methods : (constant, global_reference) Gmap.t ref = ref Gmap.empty - let instances : instances ref = ref Gmap.empty - -let freeze () = !classes, !methods, !instances -let unfreeze (cl,m,is) = +let freeze () = !classes, !instances + +let unfreeze (cl,is) = classes:=cl; - methods:=m; instances:=is - + let init () = - classes:= Gmap.empty; - methods:= Gmap.empty; + classes:= Gmap.empty; instances:= Gmap.empty - -let _ = + +let _ = Summary.declare_summary "classes_and_instances" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = true } - -let gmap_merge old ne = - Gmap.fold (fun k v acc -> Gmap.add k v acc) old ne + Summary.init_function = init } -let cmap_union = Cmap.fold Cmap.add +(* + * classes persistent object + *) -let gmap_cmap_merge old ne = - let ne' = - Gmap.fold (fun cl insts acc -> - let oldinsts = try Gmap.find cl old with Not_found -> Cmap.empty in - Gmap.add cl (cmap_union oldinsts insts) acc) - ne Gmap.empty - in - Gmap.fold (fun cl insts acc -> - if Gmap.mem cl acc then acc - else Gmap.add cl insts acc) - old ne' +let load_class (_, cl) = + classes := Gmap.add cl.cl_impl cl !classes -let add_instance_hint_ref = ref (fun id pri -> assert false) -let register_add_instance_hint = - (:=) add_instance_hint_ref -let add_instance_hint id = !add_instance_hint_ref id +let cache_class = load_class -let cache (_, (cl, m, inst)) = - classes := cl; - methods := m; - instances := inst - -let load (_, (cl, m, inst)) = - classes := gmap_merge !classes cl; - methods := gmap_merge !methods m; - instances := gmap_cmap_merge !instances inst - -open Libobject - -let subst (_,subst,(cl,m,inst)) = +let subst_class (subst,cl) = 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_gr gr = fst (subst_global subst gr) - in - let do_subst_ctx ctx = - list_smartmap (fun (na, b, t) -> - (na, Option.smartmap do_subst b, do_subst t)) - ctx - in - let do_subst_context (grs,ctx) = + and do_subst_gr gr = fst (subst_global subst gr) in + let do_subst_ctx ctx = list_smartmap + (fun (na, b, t) -> (na, Option.smartmap do_subst b, do_subst t)) + ctx in + let do_subst_context (grs,ctx) = list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, - do_subst_ctx ctx - in + do_subst_ctx ctx in let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, Option.smartmap do_subst_con y)) projs in - let subst_class k cl classes = - let k = do_subst_gr k in - let cl' = { cl_impl = k; - cl_context = do_subst_context cl.cl_context; - cl_props = do_subst_ctx cl.cl_props; - cl_projs = do_subst_projs cl.cl_projs; } - in - let cl' = if cl' = cl then cl else cl' in - Gmap.add k cl' classes - in - let classes = Gmap.fold subst_class cl Gmap.empty in - let subst_inst k insts instances = - let k = do_subst_gr k in - let insts' = - Cmap.fold (fun cst is acc -> - let cst = do_subst_con cst in - let is' = { is with is_class = k; is_impl = cst } in - Cmap.add cst (if is' = is then is else is') acc) insts Cmap.empty - in Gmap.add k insts' instances - in - let instances = Gmap.fold subst_inst inst Gmap.empty in - (classes, m, instances) - -let rel_of_variable_context ctx = - List.fold_right (fun (n,_,b,t) (ctx', subst)-> - let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in - (decl :: ctx', n :: subst)) ctx ([], []) - -let discharge (_,(cl,m,inst)) = + { cl_impl = do_subst_gr cl.cl_impl; + cl_context = do_subst_context cl.cl_context; + cl_props = do_subst_ctx cl.cl_props; + cl_projs = do_subst_projs cl.cl_projs; } + +let discharge_class (_,cl) = + let repl = Lib.replacement_context () in + let rel_of_variable_context ctx = List.fold_right + ( fun (n,_,b,t) (ctx', subst) -> + let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in + (decl :: ctx', n :: subst) + ) ctx ([], []) in let discharge_rel_context subst n rel = + let rel = map_rel_context (Cooking.expmod_constr repl) rel in let ctx, _ = List.fold_right - (fun (id, b, t) (ctx, k) -> - (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k) + (fun (id, b, t) (ctx, k) -> + (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k) rel ([], n) in ctx in let abs_context cl = match cl.cl_impl with - | VarRef _ | ConstructRef _ -> assert false - | ConstRef cst -> Lib.section_segment_of_constant cst - | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind - in + | VarRef _ | ConstructRef _ -> assert false + | ConstRef cst -> Lib.section_segment_of_constant cst + | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in let discharge_context ctx' subst (grs, ctx) = - let grs' = List.map (fun _ -> None) subst @ + let grs' = List.map (fun _ -> None) subst @ list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs - in grs', discharge_rel_context subst 1 ctx @ ctx' - in - let subst_class k cl acc = - let cl_impl' = Lib.discharge_global cl.cl_impl in - let cl' = - if cl_impl' == cl.cl_impl then cl - else - let ctx = abs_context cl in - let ctx', subst = rel_of_variable_context ctx in - { cl_impl = cl_impl'; - cl_context = discharge_context ctx' subst cl.cl_context; - cl_props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props; - cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs } - in Gmap.add cl_impl' cl' acc - in - let classes = Gmap.fold subst_class cl Gmap.empty in - let subst_inst k insts acc = - let k' = Lib.discharge_global k in - let insts' = - Cmap.fold (fun k is acc -> - let impl = Lib.discharge_con is.is_impl in - let is = { is with is_class = k'; is_impl = impl } in - Cmap.add impl is acc) - insts Cmap.empty - in Gmap.add k' insts' acc - in - let instances = Gmap.fold subst_inst inst Gmap.empty in - Some (classes, m, instances) - -let rebuild (cl,m,inst) = - let inst = - Gmap.map (fun insts -> - Cmap.fold (fun k is insts -> - match !(is.is_global) with - | -1 -> insts - | 0 -> Cmap.add k is insts - | n -> - add_instance_hint is.is_impl is.is_pri; - is.is_global := pred n; - Cmap.add k is insts) insts Cmap.empty) - inst - in (cl, m, inst) - -let (input,output) = + in grs', discharge_rel_context subst 1 ctx @ ctx' in + let cl_impl' = Lib.discharge_global cl.cl_impl in + if cl_impl' == cl.cl_impl then cl else + let ctx = abs_context cl in + let ctx, subst = rel_of_variable_context ctx in + let context = discharge_context ctx subst cl.cl_context in + let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in + { cl_impl = cl_impl'; + cl_context = context; + cl_props = props; + cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs } + +let rebuild_class cl = cl + +let (class_input,class_output) = declare_object { (default_object "type classes state") with - cache_function = cache; - load_function = (fun _ -> load); - open_function = (fun _ -> load); - classify_function = (fun (_,x) -> Substitute x); - discharge_function = discharge; - rebuild_function = rebuild; - subst_function = subst; - export_function = (fun x -> Some x) } - -let update () = - Lib.add_anonymous_leaf (input (!classes, !methods, !instances)) - -let add_class c = - classes := Gmap.add c.cl_impl c !classes; - methods := List.fold_left (fun acc x -> - match snd x with - | Some m -> Gmap.add m c.cl_impl acc - | None -> acc) !methods c.cl_projs; - update () + cache_function = cache_class; + load_function = (fun _ -> load_class); + open_function = (fun _ -> load_class); + classify_function = (fun x -> Substitute x); + discharge_function = (fun a -> Some (discharge_class a)); + rebuild_function = rebuild_class; + subst_function = subst_class } + +let add_class cl = + Lib.add_anonymous_leaf (class_input cl) + + +(* + * instances persistent object + *) + +let load_instance (_,inst) = + let insts = + try Gmap.find inst.is_class !instances + with Not_found -> Gmap.empty in + let insts = Gmap.add inst.is_impl inst insts in + instances := Gmap.add inst.is_class insts !instances + +let cache_instance = load_instance + +let subst_instance (subst,inst) = + { inst with + is_class = fst (subst_global subst inst.is_class); + is_impl = fst (subst_global subst inst.is_impl) } + +let discharge_instance (_,inst) = + if inst.is_global <= 0 then None + else Some + { inst with + is_global = pred inst.is_global; + is_class = Lib.discharge_global inst.is_class; + is_impl = Lib.discharge_global inst.is_impl } -let class_info c = +let rebuild_instance inst = + add_instance_hint inst.is_impl inst.is_pri; + inst + +let classify_instance inst = + if inst.is_global = -1 then Dispose + else Substitute inst + +let (instance_input,instance_output) = + declare_object + { (default_object "type classes instances state") with + cache_function = cache_instance; + load_function = (fun _ -> load_instance); + open_function = (fun _ -> load_instance); + classify_function = classify_instance; + discharge_function = discharge_instance; + rebuild_function = rebuild_instance; + subst_function = subst_instance } + +let add_instance i = + Lib.add_anonymous_leaf (instance_input i); + add_instance_hint i.is_impl i.is_pri + +open Declarations + +let add_constant_class cst = + let ty = Typeops.type_of_constant (Global.env ()) cst in + let ctx, arity = decompose_prod_assum ty in + let tc = + { cl_impl = ConstRef cst; + cl_context = (List.map (const None) ctx, ctx); + cl_props = [(Anonymous, None, arity)]; + cl_projs = [] + } + in add_class tc; + set_typeclass_transparency (EvalConstRef cst) false + +let add_inductive_class ind = + let mind, oneind = Global.lookup_inductive ind in + let k = + let ctx = oneind.mind_arity_ctxt in + let ty = Inductive.type_of_inductive_knowing_parameters + (push_rel_context ctx (Global.env ())) + oneind (Termops.extended_rel_vect 0 ctx) + in + { cl_impl = IndRef ind; + cl_context = List.map (const None) ctx, ctx; + cl_props = [Anonymous, None, ty]; + cl_projs = [] } + in add_class k + +(* + * interface functions + *) + +let class_info c = try Gmap.find c !classes with _ -> not_a_class (Global.env()) (constr_of_global c) -let instance_constructor cl args = - let pars = fst (list_chop (List.length (fst cl.cl_context)) args) in +let instance_constructor cl args = + let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in + let pars = fst (list_chop lenpars args) in match cl.cl_impl with | IndRef ind -> applistc (mkConstruct (ind, 1)) args, applistc (mkInd ind) pars | ConstRef cst -> list_last args, applistc (mkConst cst) pars | _ -> assert false - + let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes [] let cmapl_add x y m = try let l = Gmap.find x m in - Gmap.add x (Cmap.add y.is_impl y l) m + Gmap.add x (Gmap.add y.is_impl y l) m with Not_found -> - Gmap.add x (Cmap.add y.is_impl y Cmap.empty) m + Gmap.add x (Gmap.add y.is_impl y Gmap.empty) m -let cmap_elements c = Cmap.fold (fun k v acc -> v :: acc) c [] +let cmap_elements c = Gmap.fold (fun k v acc -> v :: acc) c [] -let instances_of c = +let instances_of c = try cmap_elements (Gmap.find c.cl_impl !instances) with Not_found -> [] -let add_instance i = - let cl = class_info i.is_class in - instances := cmapl_add cl.cl_impl i !instances; - add_instance_hint i.is_impl i.is_pri; - update () - let all_instances () = Gmap.fold (fun k v acc -> - Cmap.fold (fun k v acc -> v :: acc) v acc) + Gmap.fold (fun k v acc -> v :: acc) v acc) !instances [] let instances r = - let cl = class_info r in instances_of cl - -let method_typeclass ref = - match ref with - | ConstRef c -> - class_info (Gmap.find c !methods) - | _ -> raise Not_found + let cl = class_info r in instances_of cl let is_class gr = Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false - -let is_method c = - Gmap.mem c !methods let is_instance = function | ConstRef c -> @@ -320,18 +313,20 @@ let is_instance = function (match Decls.variable_kind v with | IsDefinition Instance -> true | _ -> false) + | ConstructRef (ind,_) -> + is_class (IndRef ind) | _ -> false -let is_implicit_arg k = +let is_implicit_arg k = match k with - ImplicitArg (ref, (n, id)) -> true + ImplicitArg (ref, (n, id), b) -> true | InternalHole -> true | _ -> false -let global_class_of_constr env c = +let global_class_of_constr env c = try class_info (global_of_constr c) with Not_found -> not_a_class env c - + let dest_class_app env c = let cl, args = decompose_app c in global_class_of_constr env cl, args @@ -339,49 +334,49 @@ let dest_class_app env c = let class_of_constr c = try Some (fst (dest_class_app (Global.env ()) c)) with _ -> None (* To embed a boolean for resolvability status. - This is essentially a hack to mark which evars correspond to - goals and do not need to be resolved when we have nested [resolve_all_evars] + This is essentially a hack to mark which evars correspond to + goals and do not need to be resolved when we have nested [resolve_all_evars] calls (e.g. when doing apply in an External hint in typeclass_instances). Would be solved by having real evars-as-goals. *) let ((bool_in : bool -> Dyn.t), (bool_out : Dyn.t -> bool)) = Dyn.create "bool" - + let bool_false = bool_in false let is_resolvable evi = match evi.evar_extra with Some t -> if Dyn.tag t = "bool" then bool_out t else true | None -> true - -let mark_unresolvable evi = + +let mark_unresolvable evi = { evi with evar_extra = Some bool_false } - + let mark_unresolvables sigma = Evd.fold (fun ev evi evs -> Evd.add evs ev (mark_unresolvable evi)) sigma Evd.empty - -let rec is_class_type c = + +let rec is_class_type evd c = match kind_of_term c with - | Prod (_, _, t) -> is_class_type t + | Prod (_, _, t) -> is_class_type evd t + | Evar (e, _) when is_defined evd e -> is_class_type evd (Evarutil.nf_evar evd c) | _ -> class_of_constr c <> None -let is_class_evar evi = - is_class_type evi.Evd.evar_concl - +let is_class_evar evd evi = + is_class_type evd evi.Evd.evar_concl + let has_typeclasses evd = - Evd.fold (fun ev evi has -> has || - (evi.evar_body = Evar_empty && is_class_evar evi && is_resolvable evi)) + Evd.fold (fun ev evi has -> has || + (evi.evar_body = Evar_empty && is_class_evar evd evi && is_resolvable evi)) evd false let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) let solve_instanciation_problem = ref (fun _ _ _ -> assert false) let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd = - if not (has_typeclasses (Evd.evars_of evd)) then evd - else - !solve_instanciations_problem env evd onlyargs split fail + if not (has_typeclasses evd) then evd + else !solve_instanciations_problem env evd onlyargs split fail let resolve_one_typeclass env evm t = !solve_instanciation_problem env evm t |