diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 311 |
1 files changed, 311 insertions, 0 deletions
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 |