From 8764f77d807ff9d3f6260b657865ad0f40248cab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Aug 2017 12:57:38 +0200 Subject: Handling primitive projections in canonical structures. --- pretyping/evarconv.ml | 4 ++++ pretyping/recordops.ml | 2 ++ 2 files changed, 6 insertions(+) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cb76df4e8a..9b002a5bcc 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -176,6 +176,10 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let s = ESorts.kind sigma s in lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] + | Proj (p, c) -> + let c2 = Globnames.ConstRef (Projection.constant p) in + let sk2 = Stack.append_app [|c|] sk2 in + lookup_canonical_conversion (proji, Const_cs c2), sk2 | _ -> let (c2, _) = Termops.global_of_constr sigma t2 in lookup_canonical_conversion (proji, Const_cs c2),sk2 diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index a23579609a..469b32ebad 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -180,6 +180,8 @@ let cs_pattern_of_constr t = end | 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 (ConstRef (Projection.constant p)), None, [c] | Sort s -> Sort_cs (family_of_sort s), None, [] | _ -> begin -- cgit v1.2.3 From 1a58e205e79ca2fd0a40b014e929c180e5ff57eb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 22 Aug 2017 21:05:59 +0200 Subject: Properly handling projection parameters in canonical structures. --- pretyping/evarconv.ml | 4 +++- pretyping/recordops.ml | 13 ++++++++----- pretyping/recordops.mli | 2 +- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9b002a5bcc..0f1a508c8d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -178,7 +178,9 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = (proji, Sort_cs (family_of_sort s)),[] | Proj (p, c) -> let c2 = Globnames.ConstRef (Projection.constant p) in - let sk2 = Stack.append_app [|c|] sk2 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 | _ -> let (c2, _) = Termops.global_of_constr sigma t2 in diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 469b32ebad..26b16c039b 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -171,7 +171,7 @@ 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 = +let cs_pattern_of_constr env t = match kind_of_term t with App (f,vargs) -> begin @@ -181,7 +181,9 @@ let cs_pattern_of_constr t = | 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 (ConstRef (Projection.constant p)), None, [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 (family_of_sort s), None, [] | _ -> begin @@ -192,7 +194,6 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (sign,env,t,con,proji_sp) -> - let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in 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 @@ -209,14 +210,16 @@ let compute_canonical_projections warn (con,ind) = 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 = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in - let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign 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 *) @@ -224,7 +227,7 @@ 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 -> if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 5480b14af0..8e2333b349 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -65,7 +65,7 @@ type obj_typ = { o_TCOMPS : constr list } (** ordered *) (** Return the form of the component of a canonical structure *) -val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list +val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list val pr_cs_pattern : cs_pattern -> Pp.t -- cgit v1.2.3 From d21586b1355cbc178ffeb066392a9ef86d5184d2 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 24 Aug 2017 15:50:47 +0200 Subject: unification: fix BZ#5692, recognize prim projs as CS projections --- pretyping/recordops.ml | 20 +++++++++++++++----- pretyping/unification.ml | 8 ++++++-- 2 files changed, 21 insertions(+), 7 deletions(-) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 26b16c039b..e970a1db90 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -329,15 +329,25 @@ 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, _) = Termops.global_of_constr sigma 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 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 diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d52c3932df..e8f7e2bbaf 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -501,6 +501,10 @@ let expand_key ts env sigma = function in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red | None -> None +let isApp_or_Proj sigma c = + match kind sigma c with + | App _ | Proj _ -> true + | _ -> false type unirec_flags = { at_top: bool; @@ -1020,7 +1024,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = - if isApp sigma cM then + if isApp_or_Proj sigma cM then let f1l1 = whd_nored_state sigma (cM,Stack.empty) in if is_open_canonical_projection curenv sigma f1l1 then let f2l2 = whd_nored_state sigma (cN,Stack.empty) in @@ -1036,7 +1040,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e error_cannot_unify (fst curenvnb) sigma (cM,cN) else try f1 () with e when precatchable_exception e -> - if isApp sigma cN then + if isApp_or_Proj sigma cN then let f2l2 = whd_nored_state sigma (cN, Stack.empty) in if is_open_canonical_projection curenv sigma f2l2 then let f1l1 = whd_nored_state sigma (cM, Stack.empty) in -- cgit v1.2.3 From 157d3fdce504e59eada13068b630c6b9d3d44360 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Aug 2017 17:50:02 +0200 Subject: Adding a test for bug BZ#5692. --- test-suite/bugs/closed/5692.v | 54 +++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 52 insertions(+), 2 deletions(-) diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v index 55ef7abe40..4c8d464f19 100644 --- a/test-suite/bugs/closed/5692.v +++ b/test-suite/bugs/closed/5692.v @@ -1,9 +1,59 @@ Set Primitive Projections. Require Import ZArith ssreflect. -Module Test3. +Module Test1. -Set Primitive Projections. +Structure semigroup := SemiGroup { + sg_car :> Type; + sg_op : sg_car -> sg_car -> sg_car; +}. + +Structure monoid := Monoid { + monoid_car :> Type; + monoid_op : monoid_car -> monoid_car -> monoid_car; + monoid_unit : monoid_car; +}. + +Coercion monoid_sg (X : monoid) : semigroup := + SemiGroup (monoid_car X) (monoid_op X). +Canonical Structure monoid_sg. + +Parameter X : monoid. +Parameter x y : X. + +Check (sg_op _ x y). + +End Test1. + +Module Test2. + +Structure semigroup := SemiGroup { + sg_car :> Type; + sg_op : sg_car -> sg_car -> sg_car; +}. + +Structure monoid := Monoid { + monoid_car :> Type; + monoid_op : monoid_car -> monoid_car -> monoid_car; + monoid_unit : monoid_car; + monoid_left_id x : monoid_op monoid_unit x = x; +}. + +Coercion monoid_sg (X : monoid) : semigroup := + SemiGroup (monoid_car X) (monoid_op X). +Canonical Structure monoid_sg. + +Canonical Structure nat_sg := SemiGroup nat plus. +Canonical Structure nat_monoid := Monoid nat plus 0 plus_O_n. + +Lemma foo (x : nat) : 0 + x = x. +Proof. +apply monoid_left_id. +Qed. + +End Test2. + +Module Test3. Structure semigroup := SemiGroup { sg_car :> Type; -- cgit v1.2.3