diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /pretyping/recordops.ml | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r-- | pretyping/recordops.ml | 128 |
1 files changed, 80 insertions, 48 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 284af0cb..d070edea 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.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) *) (************************************************************************) (* Created by Amokrane Saïbi, Dec 1998 *) @@ -19,7 +21,7 @@ open Pp open Names open Globnames open Nametab -open Term +open Constr open Libobject open Mod_subst open Reductionops @@ -37,7 +39,7 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (Name.t * bool) list; - s_PROJ : constant option list } + s_PROJ : Constant.t option list } let structure_table = Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs" @@ -48,7 +50,7 @@ let projection_table = is the inductive always (fst constructor) ? It seems so... *) type struc_tuple = - inductive * constructor * (Name.t * bool) list * constant option list + 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 @@ -134,7 +136,7 @@ let find_projection = function type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) @@ -144,7 +146,7 @@ type obj_typ = { type cs_pattern = Const_cs of global_reference | Prod_cs - | Sort_cs of sorts_family + | Sort_cs of Sorts.family | Default_cs let eq_cs_pattern p1 p2 = match p1, p2 with @@ -171,16 +173,20 @@ let keep_true_projections projs kinds = let filter (p, (_, b)) = if b then Some p else None in List.map_filter filter (List.combine projs kinds) -let cs_pattern_of_constr t = - match kind_of_term t with +let cs_pattern_of_constr env t = + match kind t with App (f,vargs) -> begin try Const_cs (global_of_constr f) , None, Array.to_list vargs with e when CErrors.noncritical e -> raise Not_found end | Rel n -> Default_cs, Some n, [] - | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b] - | Sort s -> Sort_cs (family_of_sort s), None, [] + | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] + | Proj (p, c) -> + let { Environ.uj_type = ty } = Typeops.infer env c in + let _, params = Inductive.find_rectype env ty in + Const_cs (ConstRef (Projection.constant p)), None, params @ [c] + | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> begin try Const_cs (global_of_constr t) , None, [] @@ -189,27 +195,33 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (t,con_pp,proji_sp_pp) -> + (fun (sign,env,t,con,proji_sp) -> + 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 strbrk "Projection value has no head constant: " - ++ Termops.print_constr t ++ strbrk " in canonical instance " + ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) let compute_canonical_projections warn (con,ind) = let env = Global.env () in - let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in - let u = Univ.UContext.instance ctx in + let ctx = Environ.constant_context env con in + let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in - let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in - let lt,t = Reductionops.splay_lam env Evd.empty c in - let lt = List.rev_map snd lt in + let sign,t = Reductionops.splay_lam env Evd.empty (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 let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in let params, projs = List.chop p args in let lpj = keep_true_projections lpj kl in let lps = List.combine lpj projs in + let nenv = Termops.push_rels_assum sign env in let comp = List.fold_left (fun l (spopt,t) -> (* comp=components *) @@ -217,12 +229,10 @@ let compute_canonical_projections warn (con,ind) = | Some proji_sp -> begin try - let patt, n , args = cs_pattern_of_constr t in + let patt, n , args = cs_pattern_of_constr nenv t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> - let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) - and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); l end | _ -> l) @@ -255,8 +265,8 @@ 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 cs.o_DEF) - and new_can_s = (Termops.print_constr s.o_DEF) in + 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 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)) @@ -278,7 +288,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) = let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) -let inCanonStruc : constant * inductive -> obj = +let inCanonStruc : Constant.t * inductive -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; @@ -290,29 +300,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) (*s High-level declaration of a canonical structure *) -let error_not_structure ref = - errorlabstrm "object_declare" - (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.") +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))) let check_and_decompose_canonical_structure ref = - let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in + let sp = + match ref with + ConstRef sp -> sp + | _ -> error_not_structure ref "Expected an instance of a record or structure." + in let env = Global.env () in - let ctx = Environ.constant_context env sp in - let u = Univ.UContext.instance ctx 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 in - let body = snd (splay_lam (Global.env()) Evd.empty vc) in - let f,args = match kind_of_term body with + | 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 + let body = EConstr.Unsafe.to_constr body in + let f,args = match kind body with | App (f,args) -> f,args - | _ -> error_not_structure ref in - let indsp = match kind_of_term f with + | _ -> + error_not_structure ref "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 in - let s = try lookup_structure indsp with Not_found -> error_not_structure ref in + | _ -> error_not_structure ref "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 let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref; + error_not_structure ref "Got too few arguments to the record or structure constructor."; (sp,indsp) let declare_canonical_structure ref = @@ -321,15 +342,26 @@ let declare_canonical_structure ref = let lookup_canonical_conversion (proj,pat) = assoc_pat pat (Refmap.find proj !object_table) +let decompose_projection sigma c args = + match EConstr.kind sigma c with + | Const (c, u) -> + let n = find_projection_nparams (ConstRef c) in + (** Check if there is some canonical projection attached to this structure *) + let _ = Refmap.find (ConstRef c) !object_table in + let arg = Stack.nth args n in + arg + | Proj (p, c) -> + let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in + c + | _ -> raise Not_found + let is_open_canonical_projection env sigma (c,args) = + let open EConstr in try - let ref = global_of_constr c in - let n = find_projection_nparams ref in - (** Check if there is some canonical projection attached to this structure *) - let _ = Refmap.find ref !object_table in + let arg = decompose_projection sigma c args in try - let arg = whd_all env sigma (Stack.nth args n) in - let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in - not (isConstruct hd) + let arg = whd_all env sigma arg in + let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in + not (isConstruct sigma hd) with Failure _ -> false with Not_found -> false |