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/recordops.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'pretyping/recordops.ml') 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/recordops.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'pretyping/recordops.ml') 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); -- 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 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'pretyping/recordops.ml') 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 -- cgit v1.2.3