diff options
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r-- | pretyping/recordops.ml | 72 |
1 files changed, 54 insertions, 18 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index d070edea..aedef40e 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -44,7 +44,7 @@ type struc_typ = { let structure_table = Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs" let projection_table = - Summary.ref Cmap.empty ~name:"record-projs" + Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs" (* TODO: could be unify struc_typ and struc_tuple ? in particular, is the inductive always (fst constructor) ? It seems so... *) @@ -53,7 +53,9 @@ type struc_tuple = inductive * constructor * (Name.t * bool) list * Constant.t option list let load_structure i (_,(ind,id,kl,projs)) = - let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in + let open Declarations in + let mib, mip = Global.lookup_inductive ind in + let n = mib.mind_nparams in let struc = { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in structure_table := Indmap.add ind struc !structure_table; @@ -69,8 +71,8 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - List.smartmap - (Option.smartmap (fun kn -> fst (subst_con_kn subst kn))) + List.Smart.map + (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn))) projs in let id' = fst (subst_constructor subst id) in @@ -107,6 +109,34 @@ let find_projection = function | ConstRef cst -> Cmap.find cst !projection_table | _ -> raise Not_found +let prim_table = + Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs" + +let load_prim i (_,p) = + prim_table := Cmap_env.add (Projection.Repr.constant p) p !prim_table + +let cache_prim p = load_prim 1 p + +let subst_prim (subst,p) = subst_proj_repr subst p + +let discharge_prim (_,p) = Some (Lib.discharge_proj_repr p) + +let inPrim : Projection.Repr.t -> obj = + declare_object { + (default_object "PRIMPROJS") with + cache_function = cache_prim ; + load_function = load_prim; + subst_function = subst_prim; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_prim } + +let declare_primitive_projection p = Lib.add_anonymous_leaf (inPrim p) + +let is_primitive_projection c = Cmap_env.mem c !prim_table + +let find_primitive_projection c = + try Some (Cmap_env.find c !prim_table) with Not_found -> None + (************************************************************************) (*s A canonical structure declares "canonical" conversion hints between *) (* the effective components of a structure and the projections of the *) @@ -144,13 +174,13 @@ type obj_typ = { o_TCOMPS : constr list } (* ordered *) type cs_pattern = - Const_cs of global_reference + Const_cs of GlobRef.t | Prod_cs | Sort_cs of Sorts.family | Default_cs let eq_cs_pattern p1 p2 = match p1, p2 with -| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2 +| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2 | Prod_cs, Prod_cs -> true | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 | Default_cs, Default_cs -> true @@ -199,7 +229,7 @@ let warn_projection_no_head_constant = let env = Termops.push_rels_assum sign env in let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in + let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") @@ -211,7 +241,7 @@ let compute_canonical_projections warn (con,ind) = let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in let c = Environ.constant_value_in env (con,u) in - let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in let lt = List.rev_map snd sign in @@ -265,8 +295,12 @@ let add_canonical_structure warn o = in match ocs with | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table; | Some (c, cs) -> - let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF)) - and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in + (* XXX: Undesired global access to env *) + let env = Global.env () in + let sigma = Evd.from_env env in + let old_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF)) + and new_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF)) + in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) @@ -304,36 +338,38 @@ let error_not_structure ref description = user_err ~hdr:"object_declare" (str"Could not declare a canonical structure " ++ (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ - str(description))) + description)) let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp - | _ -> error_not_structure ref "Expected an instance of a record or structure." + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let env = Global.env () in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc - | None -> error_not_structure ref "Could not find its value in the global environment." in - let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in + | None -> error_not_structure ref (str "Could not find its value in the global environment.") in + let env = Global.env () in + let evd = Evd.from_env env in + let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with | App (f,args) -> f,args | _ -> - error_not_structure ref "Expected a record or structure constructor applied to arguments." in + error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in let indsp = match kind f with | Construct ((indsp,1),u) -> indsp - | _ -> error_not_structure ref "Expected an instance of a record or structure." in + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let s = try lookup_structure indsp with Not_found -> error_not_structure ref - ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in + (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref "Got too few arguments to the record or structure constructor."; + error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (sp,indsp) let declare_canonical_structure ref = |