From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Nov 2016 19:02:40 +0100 Subject: Pretyping API using EConstr. --- engine/proofview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 21227ed198..b0f6d463bc 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -71,7 +71,7 @@ let dependent_init = | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in + let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in let sigma = Sigma.to_evar_map sigma in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (gl, _) = Term.destEvar econstr in -- cgit v1.2.3 From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- engine/proofview.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index b0f6d463bc..9adf947441 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -72,6 +72,7 @@ let dependent_init = | TCons (env, sigma, typ, t) -> let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in + let econstr = EConstr.Unsafe.to_constr econstr in let sigma = Sigma.to_evar_map sigma in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (gl, _) = Term.destEvar econstr in -- cgit v1.2.3 From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 22:16:08 +0100 Subject: Proofview.Goal primitive now return EConstrs. --- engine/proofview.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 9adf947441..9e5e9c7dae 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -984,7 +984,7 @@ module Goal = struct type ('a, 'r) t = { env : Environ.env; sigma : Evd.evar_map; - concl : Term.constr ; + concl : EConstr.constr ; self : Evar.t ; (* for compatibility with old-style definitions *) } @@ -1005,7 +1005,7 @@ module Goal = struct let gmake_with info env sigma goal = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; - concl = Evd.evar_concl info ; + concl = EConstr.of_constr (Evd.evar_concl info); self = goal } let nf_gmake env sigma goal = -- cgit v1.2.3 From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- engine/proofview.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 9e5e9c7dae..ab72cc405f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -24,7 +24,7 @@ type proofview = Proofview_monad.proofview (* The first items in pairs below are proofs (under construction). The second items in the pairs below are statements that are being proved. *) -type entry = (Term.constr * Term.types) list +type entry = (EConstr.constr * EConstr.types) list (** Returns a stylised view of a proofview for use by, for instance, ide-s. *) @@ -37,15 +37,16 @@ let proofview p = p.comb , p.solution let compact el ({ solution } as pv) = - let nf = Evarutil.nf_evar solution in + let nf c = Evarutil.nf_evar solution c in + let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in let apply_subst_einfo _ ei = Evd.({ ei with - evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf ei.evar_hyps; - evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in + evar_concl = nf0 ei.evar_concl; + evar_hyps = Environ.map_named_val nf0 ei.evar_hyps; + evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); @@ -56,7 +57,7 @@ let compact el ({ solution } as pv) = type telescope = | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) + | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) let typeclass_resolvable = Evd.Store.field () @@ -71,11 +72,10 @@ let dependent_init = | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in - let econstr = EConstr.Unsafe.to_constr econstr in + let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in + let (gl, _) = EConstr.destEvar (Sigma.to_evar_map sigma) econstr in let sigma = Sigma.to_evar_map sigma in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in - let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in entry, { solution = sol; comb = gl :: comb; shelf = [] } in @@ -1222,12 +1222,12 @@ module V82 = struct { Evd.it = comb ; sigma = solution } let top_goals initial { solution=solution; } = - let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in + let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } let top_evars initial = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term c) + Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c)) in CList.flatten (CList.map evars_of_initial initial) -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- engine/proofview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index ab72cc405f..0a18cf191b 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -995,7 +995,7 @@ module Goal = struct let env { env=env } = env let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma - let hyps { env=env } = Environ.named_context env + let hyps { env=env } = EConstr.named_context env let concl { concl=concl } = concl let extra { sigma=sigma; self=self } = goal_extra sigma self -- cgit v1.2.3 From d549d9d3d169fbfc5f555e3e4f22f46301161d53 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 16:30:00 +0100 Subject: Do not ask for a normalized goal to get hypotheses and conclusions. This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization. --- engine/proofview.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 0a18cf191b..71e9acc88e 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -999,9 +999,6 @@ module Goal = struct let concl { concl=concl } = concl let extra { sigma=sigma; self=self } = goal_extra sigma self - let raw_concl { concl=concl } = concl - - let gmake_with info env sigma goal = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; -- cgit v1.2.3