From a27fb3c67238cc41dc24308a233a02422e0f83f3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 15 Nov 2020 10:28:04 +0100 Subject: Fixes #9971: expand_projections failing on primitive projections of unknown type. This was a case where expand_projections was calling find_mrectype which was expecting the argument of the projection to be an inductive. We could have ensured that this type is at least the appropriate inductive applied to fresh evars, but this expand_projections was in practice used for checking the applicability of canonical structures and the unifiability of the parameters of the projections is anyway a consequence of the unifiability of the principal argument of the projections. So, the latter is enough. --- pretyping/evarconv.ml | 6 ++---- pretyping/recordops.ml | 5 +---- 2 files changed, 3 insertions(+), 8 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 00d4c7b3d8..16be4812fe 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -253,10 +253,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> let c2 = GlobRef.ConstRef (Projection.constant p) in - let c = Retyping.expand_projection env sigma p c [] in - let _, args = destApp sigma c in - let sk2 = Stack.append_app args sk2 in - lookup_canonical_conversion (proji, Const_cs c2), sk2 + lookup_canonical_conversion (proji, Const_cs c2), Stack.append_app [|c|] sk2 | _ -> let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in lookup_canonical_conversion (proji, Const_cs c2),sk2 @@ -273,6 +270,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Some c -> (* A primitive projection applied to c *) let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = + (* Are we sure that ty is not an evar? *) try Inductiveops.find_mrectype env sigma ty with _ -> raise Not_found in Stack.append_app_list ind_args Stack.empty, c, sk1 diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e6e5ad8dd4..f26f59d6c5 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -179,10 +179,7 @@ let rec cs_pattern_of_constr env t = patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] - | Proj (p, c) -> - let ty = Retyping.get_type_of_constr env c in - let _, params = Inductive.find_rectype env ty in - Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] + | Proj (p, c) -> Const_cs (GlobRef.ConstRef (Projection.constant p)), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (fst @@ destRef t) , None, [] -- cgit v1.2.3 From 115fe6ba6f77cabe8729cc39ec9c373c3b0173d3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 15 Nov 2020 11:10:40 +0100 Subject: Use a proper canonical structure entry for projections. This is to make more explicit that arguments of the projection are not kept. We seize this opportunity to use QGlobRef equality on GlobRef. --- pretyping/evarconv.ml | 11 +++++------ pretyping/recordops.ml | 19 +++++++++++-------- pretyping/recordops.mli | 3 ++- 3 files changed, 18 insertions(+), 15 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 16be4812fe..cdf2922516 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -244,21 +244,20 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then - lookup_canonical_conversion (proji, Prod_cs), + lookup_canonical_conversion env (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> let s = ESorts.kind sigma s in - lookup_canonical_conversion + lookup_canonical_conversion env (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> - let c2 = GlobRef.ConstRef (Projection.constant p) in - lookup_canonical_conversion (proji, Const_cs c2), Stack.append_app [|c|] sk2 + lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2 | _ -> let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in - lookup_canonical_conversion (proji, Const_cs c2),sk2 + lookup_canonical_conversion env (proji, Const_cs c2),sk2 with Not_found -> - let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in + let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in (c,cs),[] in let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f26f59d6c5..b6e44265ae 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -144,19 +144,21 @@ type obj_typ = { type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.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 -> GlobRef.equal gr1 gr2 +let eq_cs_pattern env p1 p2 = match p1, p2 with +| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2 +| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2 | Prod_cs, Prod_cs -> true | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 | Default_cs, Default_cs -> true | _ -> false -let rec assoc_pat a = function - | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs +let rec assoc_pat env a = function + | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs | [] -> raise Not_found @@ -179,7 +181,7 @@ let rec cs_pattern_of_constr env t = patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] - | Proj (p, c) -> Const_cs (GlobRef.ConstRef (Projection.constant p)), None, [c] + | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (fst @@ destRef t) , None, [] @@ -235,6 +237,7 @@ let compute_canonical_projections env ~warn (gref,ind) = let pr_cs_pattern = function Const_cs c -> Nametab.pr_global_env Id.Set.empty c + | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p)) | Prod_cs -> str "_ -> _" | Default_cs -> str "_" | Sort_cs s -> Sorts.pr_sort_family s @@ -250,7 +253,7 @@ let register_canonical_structure ~warn env sigma o = compute_canonical_projections env ~warn o |> List.iter (fun ((proj, (cs_pat, _ as pat)), s) -> let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in - match assoc_pat cs_pat l with + match assoc_pat env cs_pat l with | exception Not_found -> object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table | _, cs -> @@ -317,8 +320,8 @@ let check_and_decompose_canonical_structure env sigma ref = error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (ref,indsp) -let lookup_canonical_conversion (proj,pat) = - assoc_pat pat (GlobRef.Map.find proj !object_table) +let lookup_canonical_conversion env (proj,pat) = + assoc_pat env pat (GlobRef.Map.find proj !object_table) let decompose_projection sigma c args = match EConstr.kind sigma c with diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 3be60d5e62..5b8dc8184a 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -67,6 +67,7 @@ val find_primitive_projection : Constant.t -> Projection.Repr.t option (** A cs_pattern characterizes the form of a component of canonical structure *) type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs @@ -88,7 +89,7 @@ val pr_cs_pattern : cs_pattern -> Pp.t type cs = GlobRef.t * inductive -val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ +val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> cs -> unit val subst_canonical_structure : Mod_subst.substitution -> cs -> cs -- cgit v1.2.3