diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r-- | pretyping/typeclasses.ml | 215 |
1 files changed, 113 insertions, 102 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index b8da6b68..08051fd3 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) @@ -11,12 +13,16 @@ open Names open Globnames open Decl_kinds open Term +open Constr open Vars open Evd open Util open Typeclasses_errors open Libobject open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (*i*) let typeclasses_unique_solutions = ref false @@ -27,8 +33,7 @@ open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "check that typeclasses proof search returns unique solutions"; optkey = ["Typeclasses";"Unique";"Solutions"]; optread = get_typeclasses_unique_solutions; @@ -55,18 +60,21 @@ type direction = Forward | Backward (* This module defines type-classes *) type typeclass = { + (* Universe quantification *) + cl_univs : Univ.AUContext.t; + (* 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 list * Context.Rel.t; + cl_context : global_reference option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; (* The method implementaions as projections. *) cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option - * constant option) list; + * Constant.t option) list; cl_strict : bool; @@ -79,9 +87,8 @@ type instance = { is_class: global_reference; is_info: Vernacexpr.hint_info_expr; (* Sections where the instance should be redeclared, - -1 for discard, 0 for none. *) - is_global: int; - is_poly: bool; + None for discard, Some 0 for none. *) + is_global: int option; is_impl: global_reference; } @@ -91,15 +98,16 @@ let instance_impl is = is.is_impl let hint_priority is = is.is_info.Vernacexpr.hint_priority -let new_instance cl info glob poly impl = +let new_instance cl info glob impl = let global = - if glob then Lib.sections_depth () - else -1 + if glob then Some (Lib.sections_depth ()) + else None in + if match global with Some n -> n>0 && isVarRef impl | _ -> false then + CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable."); { is_class = cl.cl_impl; is_info = info ; is_global = global ; - is_poly = poly; is_impl = impl } (* @@ -109,64 +117,48 @@ let new_instance cl info glob poly impl = let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes" let instances : instances ref = Summary.ref Refmap.empty ~name:"instances" -open Declarations - -let typeclass_univ_instance (cl,u') = - let subst = - let u = - match cl.cl_impl with - | ConstRef c -> - let cb = Global.lookup_constant c in - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty - | IndRef c -> - let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty - | _ -> Univ.Instance.empty - in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) - Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') - in - let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in - { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context); - cl_props = subst_ctx cl.cl_props}, u' +let typeclass_univ_instance (cl, u) = + assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u); + let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in + { cl with cl_context = on_snd subst_ctx cl.cl_context; + cl_props = subst_ctx cl.cl_props} let class_info c = try Refmap.find c !classes - with Not_found -> not_a_class (Global.env()) (printable_constr_of_global c) + with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c)) -let global_class_of_constr env c = - try let gr, u = Universes.global_of_constr c in +let global_class_of_constr env sigma c = + try let gr, u = Termops.global_of_constr sigma c in class_info gr, u 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 +let dest_class_app env sigma c = + let cl, args = EConstr.decompose_app sigma c in + global_class_of_constr env sigma cl, (List.map EConstr.Unsafe.to_constr args) -let dest_class_arity env c = - let rels, c = decompose_prod_assum c in - rels, dest_class_app env c +let dest_class_arity env sigma c = + let open EConstr in + let rels, c = decompose_prod_assum sigma c in + rels, dest_class_app env sigma c -let class_of_constr c = - try Some (dest_class_arity (Global.env ()) c) +let class_of_constr sigma c = + try Some (dest_class_arity (Global.env ()) sigma c) with e when CErrors.noncritical e -> None -let is_class_constr c = - try let gr, u = Universes.global_of_constr c in +let is_class_constr sigma c = + try let gr, u = Termops.global_of_constr sigma c in Refmap.mem gr !classes with Not_found -> false let rec is_class_type evd c = - let c, args = decompose_app c in - match kind_of_term c with + let c, _ = Termops.decompose_app_vect evd c in + match EConstr.kind evd c with | Prod (_, _, t) -> is_class_type evd t - | Evar (e, _) when Evd.is_defined evd e -> - is_class_type evd (Evarutil.whd_head_evar evd c) - | _ -> is_class_constr c + | Cast (t, _, _) -> is_class_type evd t + | _ -> is_class_constr evd c let is_class_evar evd evi = - is_class_type evd evi.Evd.evar_concl + is_class_type evd (EConstr.of_constr evi.Evd.evar_concl) (* * classes persistent object @@ -181,13 +173,14 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant 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 = List.smartmap (map_constr do_subst) in + let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, + List.smartmap (Option.smartmap do_subst_gr) grs, do_subst_ctx ctx in let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in - { cl_impl = do_subst_gr cl.cl_impl; + { cl_univs = cl.cl_univs; + 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; @@ -197,22 +190,18 @@ let subst_class (subst,cl) = 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 = match b with - | None -> LocalAssum (Name n, substn_vars 1 subst t) - | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t) - in - (decl :: ctx', n :: subst) + ( fun (decl,_) (ctx', subst) -> + let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in + (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in - let discharge_rel_context subst n rel = + let discharge_rel_context (subst, usubst) n rel = let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in - let ctx, _ = - List.fold_right - (fun decl (ctx, k) -> - map_constr (substn_vars k subst) decl :: ctx, succ k - ) - rel ([], n) - in ctx + let fold decl (ctx, k) = + let map c = subst_univs_level_constr usubst (substn_vars k subst c) in + RelDecl.map_constr map decl :: ctx, succ k + in + let ctx, _ = List.fold_right fold rel ([], n) in + ctx in let abs_context cl = match cl.cl_impl with @@ -222,22 +211,25 @@ let discharge_class (_,cl) = let discharge_context ctx' subst (grs, ctx) = let grs' = let newgrs = List.map (fun decl -> - match decl |> get_type |> class_of_constr with + match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with | None -> None - | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) + | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs + List.smartmap (Option.smartmap Lib.discharge_global) grs @ newgrs 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, usubst, uctx = abs_context cl in + let info = abs_context cl in + let ctx = info.Lib.abstr_ctx 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 + let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in + let context = discharge_context ctx (subst, usubst) cl.cl_context in + let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in - { cl_impl = cl_impl'; + { cl_univs = cl_univs'; + cl_impl = cl_impl'; cl_context = context; cl_props = props; cl_projs = List.smartmap discharge_proj cl.cl_projs; @@ -284,15 +276,18 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in + let inst, ctx = Universes.fresh_instance_from ctx None in + let ty = Vars.subst_instance_constr inst ty in + let ty = EConstr.of_constr ty in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let rec aux pri c ty path = - let ty = Evarutil.nf_evar sigma ty in - match class_of_constr ty with + match class_of_constr sigma ty with | None -> [] | Some (rels, ((tc,u), args)) -> let instapp = - Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels)) + Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels))) in + let instapp = EConstr.Unsafe.to_constr instapp in let projargs = Array.of_list (args @ [instapp]) in let projs = List.map_filter (fun (n, b, proj) -> @@ -301,8 +296,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = | Some (Backward, _) -> None | Some (Forward, info) -> let proj = Option.get proj in + let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in + let u = EConstr.EInstance.kind sigma u in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in - if check && check_instance env sigma body then None + if check && check_instance env sigma (EConstr.of_constr body) then None else let newpri = match pri, info.hint_priority with @@ -314,12 +311,12 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = in let declare_proj hints (cref, info, body) = let path' = cref :: path in - let ty = Retyping.get_type_of env sigma body in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in let rest = aux pri body ty path' in hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in + let term = Universes.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] @@ -357,22 +354,34 @@ let subst_instance (subst, (action, inst)) = action, is_impl = fst (subst_global subst inst.is_impl) } let discharge_instance (_, (action, inst)) = - if inst.is_global <= 0 then None - else Some (action, + match inst.is_global with + | None -> None + | Some n -> + assert (not (isVarRef inst.is_impl)); + Some (action, { inst with - is_global = pred inst.is_global; + is_global = Some (pred n); is_class = Lib.discharge_global inst.is_class; is_impl = Lib.discharge_global inst.is_impl }) -let is_local i = Int.equal i.is_global (-1) +let is_local i = (i.is_global == None) + +let is_local_for_hint i = + match i.is_global with + | None -> true (* i.e. either no Global keyword not in section, or in section *) + | Some n -> n <> 0 (* i.e. in a section, declare the hint as local + since discharge is managed by rebuild_instance which calls again + add_instance_hint; don't ask hints to take discharge into account + itself *) let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) + let local = is_local_for_hint inst in + add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local inst.is_info poly; List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path - (is_local inst) pri poly) + local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) @@ -407,11 +416,12 @@ let remove_instance i = remove_instance_hint i.is_impl let declare_instance info local glob = - let ty = Global.type_of_global_unsafe glob in + let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in - match class_of_constr ty with + match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> - add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) + assert (not (isVarRef glob) || local); + add_instance (new_instance tc info (not local) glob) | None -> () let add_class cl = @@ -420,7 +430,7 @@ let add_class cl = match inst with | Some (Backward, info) -> (match body with - | None -> CErrors.error "Non-definable projection can not be declared as a subinstance" + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") | Some b -> declare_instance (Some info) false (ConstRef b)) | _ -> ()) cl.cl_projs @@ -433,19 +443,20 @@ let add_class cl = let instance_constructor (cl,u) args = let lenpars = List.count is_local_assum (snd cl.cl_context) in + let open EConstr in let pars = fst (List.chop lenpars args) in match cl.cl_impl with | IndRef ind -> let ind = ind, u in - (Some (applistc (mkConstructUi (ind, 1)) args), - applistc (mkIndU ind) pars) + (Some (applist (mkConstructUi (ind, 1), args)), + applist (mkIndU ind, pars)) | ConstRef cst -> let cst = cst, u in let term = match args with | [] -> None | _ -> Some (List.last args) in - (term, applistc (mkConstU cst) pars) + (term, applist (mkConstU cst, pars)) | _ -> assert false let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes [] @@ -512,7 +523,7 @@ let mark_unresolvable evi = mark_resolvability false evi let mark_resolvable evi = mark_resolvability true evi open Evar_kinds -type evar_filter = existential_key -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t -> bool let all_evars _ _ = true let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false @@ -543,8 +554,8 @@ let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) -(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) -(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) +(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) +(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = |