diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 457 |
1 files changed, 457 insertions, 0 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml new file mode 100644 index 00000000..a2392033 --- /dev/null +++ b/pretyping/typeclasses.ml @@ -0,0 +1,457 @@ +(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *) +(************************************************************************) +(* 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: typeclasses.ml 11143 2008-06-18 15:52:42Z msozeau $ i*) + +(*i*) +open Names +open Libnames +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 = { + (* The class implementation *) + cl_impl : global_reference; + + (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) + cl_context : ((global_reference * bool) option * named_declaration) list; + + cl_params: int; + + (* Context of definitions and properties on defs, will not be shared *) + cl_props : named_context; + + (* The method implementaions as projections. *) + cl_projs : (identifier * constant) list; +} + +type typeclasses = (global_reference, typeclass) Gmap.t + +type globality = int option + +type instance = { + is_class: global_reference; + is_pri: int option; + is_global: globality; + (* Sections where the instance should be redeclared, + Some n for n sections, None for discard at end of section. *) + is_impl: constant; +} + +type instances = (global_reference, instance Cmap.t) Gmap.t + +let instance_impl is = is.is_impl + +let new_instance cl pri glob impl = + let global = + if Lib.sections_are_opened () then + if glob then Some (Lib.sections_depth ()) + else None + else Some 0 + in + { is_class = cl.cl_impl; + is_pri = pri ; + is_global = global ; + is_impl = impl } + +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) = + 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 = false; + Summary.survive_section = true } + +let gmap_merge old ne = + Gmap.fold (fun k v acc -> Gmap.add k v acc) old ne + +let cmap_union = Cmap.fold Cmap.add + +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) + Gmap.empty ne + in + Gmap.fold (fun cl insts acc -> + if Gmap.mem cl ne' then acc + else Gmap.add cl insts acc) + ne' old + +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 (_, (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 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_named ctx = + list_smartmap (fun (na, b, t) -> + (na, Option.smartmap do_subst b, do_subst t)) + ctx + in + let do_subst_ctx ctx = + list_smartmap (fun (cl, (na, b, t)) -> + (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b) cl, + (na, Option.smartmap do_subst b, do_subst t))) + ctx + in + let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs in + let subst_class k cl classes = + let k = do_subst_gr k in + let cl' = { cl with cl_impl = k; + cl_context = do_subst_ctx cl.cl_context; + cl_props = do_subst_named 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 discharge (_,(cl,m,inst)) = + let discharge_named (cl, r) = + Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b) cl, r + 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 + 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 + { cl with cl_impl = cl_impl'; + cl_context = + List.map (fun x -> None, x) (abs_context cl) @ + (list_smartmap discharge_named cl.cl_context); + cl_projs = list_smartmap (fun (x, y) -> x, 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 + | None -> insts + | Some 0 -> Cmap.add k is insts + | Some n -> + add_instance_hint is.is_impl is.is_pri; + let is' = { is with is_global = Some (pred n) } + in Cmap.add k is' insts) insts Cmap.empty) + inst + in (cl, m, inst) + +let (input,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 -> Gmap.add (snd x) c.cl_impl acc) !methods c.cl_projs; + update () + +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 cl.cl_context) 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 + with Not_found -> + Gmap.add x (Cmap.add y.is_impl y Cmap.empty) m + +let cmap_elements c = Cmap.fold (fun k v acc -> v :: acc) 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 instances r = + let cl = class_info r in instances_of cl + +let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false) +let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) + +let resolve_typeclass env ev evi (evd, defined as acc) = + try + assert(evi.evar_body = Evar_empty); + !solve_instanciation_problem env evd ev evi + with Exit -> 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 -> Evarutil.nf_evar evm' c + else raise Not_found + with Exit -> raise Not_found + +let method_typeclass ref = + match ref with + | ConstRef c -> + class_info (Gmap.find c !methods) + | _ -> raise Not_found + +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 -> + (match Decls.constant_kind c with + | IsDefinition Instance -> true + | _ -> false) + | VarRef v -> + (match Decls.variable_kind v with + | IsDefinition Instance -> true + | _ -> false) + | _ -> false + +let is_implicit_arg k = + match k with + ImplicitArg (ref, (n, id)) -> true + | InternalHole -> true + | _ -> false + +let destClassApp c = + match kind_of_term c with + | App (ki, args) when isInd ki -> + Some (destInd ki, args) + | _ when isInd c -> Some (destInd c, [||]) + | _ -> None + +let is_independent evm ev = + Evd.fold (fun ev' evi indep -> indep && + (ev = ev' || + evi.evar_body <> Evar_empty || + not (Termops.occur_evar ev evi.evar_concl))) + evm true + + +(* try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *) +(* with _ -> *) +(* 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 destClassApp evi.evar_concl with *) +(* | Some (i, args) when is_class i -> *) +(* Evd.add acc ev evi *) +(* | _ -> acc *) +(* else acc *) +(* in Evd.fold f evm Evd.empty *) +(* in *) +(* let rec sat evars = *) +(* let evm = Evd.evars_of evars in *) +(* let (evars', progress) = *) +(* Evd.fold *) +(* (fun ev evi acc -> *) +(* if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) *) +(* && evi.evar_body = Evar_empty then *) +(* resolve_typeclass env ev evi acc *) +(* else acc) *) +(* evm (evars, false) *) +(* in *) +(* if not progress then evars' *) +(* else *) +(* sat (Evarutil.nf_evar_defs evars') *) +(* in sat (Evarutil.nf_evar_defs evd) *) + +let class_of_constr c = + let extract_cl c = + try Some (class_info (global_of_constr c)) with _ -> None + in + match kind_of_term c with + App (c, _) -> extract_cl c + | _ -> extract_cl c + +let dest_class_app c = + let cl c = class_info (global_of_constr c) in + match kind_of_term c with + App (c, args) -> cl c, args + | _ -> cl c, [||] + +(* 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] + 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 = + { 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 has_typeclasses evd = + Evd.fold (fun ev evi has -> has || + (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None + && is_resolvable evi)) + evd 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 (Evarutil.nf_evar_defs evd) onlyargs split fail + +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 |