From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- pretyping/recordops.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index cda052b796..e897d5f5c5 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 sigma t = match kind_of_term t with App (f,vargs) -> begin @@ -179,7 +179,7 @@ let cs_pattern_of_constr t = 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] + | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Prod_cs, None, [a; Termops.pop (EConstr.of_constr b)] | Sort s -> Sort_cs (family_of_sort s), None, [] | _ -> begin @@ -217,7 +217,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 Evd.empty t (** FIXME *) in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) -- cgit v1.2.3 From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- pretyping/recordops.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e897d5f5c5..062e4a0683 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -202,7 +202,7 @@ let compute_canonical_projections warn (con,ind) = 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,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in let lt = List.rev_map snd lt in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = @@ -302,7 +302,7 @@ let check_and_decompose_canonical_structure ref = 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 body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in let f,args = match kind_of_term body with | App (f,args) -> f,args | _ -> error_not_structure ref in @@ -323,6 +323,7 @@ let lookup_canonical_conversion (proj,pat) = let is_open_canonical_projection env sigma (c,args) = try + let c = EConstr.Unsafe.to_constr c in 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 *) -- cgit v1.2.3 From b113f9e1ca88514cd9d94dfe90669a27689b7434 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 03:11:44 +0100 Subject: Recordops API using EConstr. --- pretyping/recordops.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 062e4a0683..f09f3221d9 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 sigma t = +let cs_pattern_of_constr t = match kind_of_term t with App (f,vargs) -> begin @@ -179,7 +179,7 @@ let cs_pattern_of_constr sigma t = with e when CErrors.noncritical e -> raise Not_found end | Rel n -> Default_cs, Some n, [] - | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Prod_cs, None, [a; Termops.pop (EConstr.of_constr b)] + | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] | Sort s -> Sort_cs (family_of_sort s), None, [] | _ -> begin @@ -217,7 +217,7 @@ let compute_canonical_projections warn (con,ind) = | Some proji_sp -> begin try - let patt, n , args = cs_pattern_of_constr Evd.empty t (** FIXME *) in + let patt, n , args = cs_pattern_of_constr 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) -- cgit v1.2.3 From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Nov 2016 01:07:35 +0100 Subject: Inv API using EConstr. --- pretyping/recordops.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f09f3221d9..3230f92da8 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -203,7 +203,8 @@ let compute_canonical_projections warn (con,ind) = 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 (EConstr.of_constr c) in - let lt = List.rev_map snd lt in + let t = EConstr.Unsafe.to_constr t in + let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in @@ -303,6 +304,7 @@ let check_and_decompose_canonical_structure ref = | Some vc -> vc | None -> error_not_structure ref 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_of_term body with | App (f,args) -> f,args | _ -> error_not_structure ref in -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- pretyping/recordops.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 3230f92da8..8362a2a26a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -324,15 +324,15 @@ let lookup_canonical_conversion (proj,pat) = assoc_pat pat (Refmap.find proj !object_table) let is_open_canonical_projection env sigma (c,args) = + let open EConstr in try - let c = EConstr.Unsafe.to_constr c in - let ref = global_of_constr c in + 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 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 hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in + not (isConstruct sigma hd) with Failure _ -> false with Not_found -> false -- cgit v1.2.3 From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 18:18:17 +0100 Subject: Ltac now uses evar-based constrs. --- pretyping/recordops.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 8362a2a26a..bc9e3a1f46 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -191,7 +191,7 @@ let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (t,con_pp,proji_sp_pp) -> strbrk "Projection value has no head constant: " - ++ Termops.print_constr t ++ strbrk " in canonical instance " + ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) @@ -256,8 +256,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)) -- cgit v1.2.3