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. --- printing/printer.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 3c8ad4255c..b36df27ed3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -760,7 +760,8 @@ let pr_prim_rule = function str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") | Refine c -> - str(if Termops.occur_meta c then "refine " else "exact ") ++ + (** FIXME *) + str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c (* Backwards compatibility *) -- cgit v1.2.3 From 7267dfafe9215c35275a39814c8af451961e997c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 17:48:47 +0100 Subject: Goal API using EConstr. --- printing/printer.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index b36df27ed3..ed6ebdc9b6 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -384,7 +384,7 @@ let pr_transparent_state (ids, csts) = let default_pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in let env = Goal.V82.env sigma g in - let concl = Goal.V82.concl sigma g in + let concl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma g) in let goal = pr_context_of env sigma ++ cut () ++ str "============================" ++ cut () ++ @@ -407,7 +407,7 @@ let pr_goal_name sigma g = let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in - let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in + let pc = pr_goal_concl_style_env env sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in str (emacs_str "") ++ str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++ str " is:" ++ cut () ++ str" " ++ pc -- cgit v1.2.3 From e6a8ab0f428c26fff2bd7e636126974f167101bf Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 01:35:54 +0100 Subject: Tactic_matching API using EConstr. --- printing/printer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index ed6ebdc9b6..2a30681bfa 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -76,7 +76,7 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* we also need to preserve the actual names of the patterns *) (* So what to do? *) let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in - pr (Termops.push_rels_assum assums env) sigma c + pr (Termops.push_rels_assum assums env) sigma (EConstr.Unsafe.to_constr c) let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env -- 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. --- printing/printer.ml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 2a30681bfa..4a6c83bd77 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -60,7 +60,10 @@ let pr_constr_goal_style_env env = pr_constr_core true env let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c - (* NB do not remove the eta-redexes! Global.env() has side-effects... *) +let pr_leconstr_env env sigma c = pr_lconstr_env env sigma (EConstr.to_constr sigma c) +let pr_econstr_env env sigma c = pr_constr_env env sigma (EConstr.to_constr sigma c) + +(* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = let (sigma, env) = get_current_context () in pr_lconstr_env env sigma t @@ -71,15 +74,18 @@ let pr_constr t = let pr_open_lconstr (_,c) = pr_lconstr c let pr_open_constr (_,c) = pr_constr c +let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c) +let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c) + let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* Warning: clashes can occur with variables of same name in env but *) (* we also need to preserve the actual names of the patterns *) (* So what to do? *) let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in - pr (Termops.push_rels_assum assums env) sigma (EConstr.Unsafe.to_constr c) + pr (Termops.push_rels_assum assums env) sigma c -let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env -let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env +let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env +let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env let pr_constr_under_binders c = let (sigma, env) = get_current_context () in @@ -147,7 +153,7 @@ let pr_constr_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.set_print_constr - (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t)) + (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma (EConstr.Unsafe.to_constr t))) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" -- cgit v1.2.3 From 778e863b77bcafc8ed339dd02226e85e5fee2532 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 11:36:09 +0100 Subject: Removing compatibility layers related to printing. --- printing/printer.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 4a6c83bd77..ba4b682960 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -99,7 +99,6 @@ let pr_type_core goal_concl_style env sigma t = let pr_ltype_core goal_concl_style env sigma t = pr_lconstr_expr (extern_type goal_concl_style env sigma t) -let pr_goal_concl_style_env env = pr_ltype_core true env let pr_ltype_env env = pr_ltype_core false env let pr_type_env env = pr_type_core false env @@ -110,8 +109,13 @@ let pr_type t = let (sigma, env) = get_current_context () in pr_type_env env sigma t +let pr_etype_env env sigma c = pr_type_env env sigma (EConstr.to_constr sigma c) +let pr_letype_env env sigma c = pr_ltype_env env sigma (EConstr.to_constr sigma c) +let pr_goal_concl_style_env env sigma c = + pr_ltype_core true env sigma (EConstr.to_constr sigma c) + let pr_ljudge_env env sigma j = - (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type) + (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) let pr_ljudge j = let (sigma, env) = get_current_context () in @@ -390,7 +394,7 @@ let pr_transparent_state (ids, csts) = let default_pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in let env = Goal.V82.env sigma g in - let concl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma g) in + let concl = Goal.V82.concl sigma g in let goal = pr_context_of env sigma ++ cut () ++ str "============================" ++ cut () ++ @@ -413,7 +417,7 @@ let pr_goal_name sigma g = let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in - let pc = pr_goal_concl_style_env env sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in + let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in str (emacs_str "") ++ str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++ str " is:" ++ cut () ++ str" " ++ pc -- 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. --- printing/printer.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index ba4b682960..63aeec82c0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -506,8 +506,8 @@ let print_evar_constraints gl sigma = end in let pr_evconstr (pbty,env,t1,t2) = - let t1 = Evarutil.nf_evar sigma t1 - and t2 = Evarutil.nf_evar sigma t2 in + let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1) + and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in let env = (** We currently allow evar instances to refer to anonymous de Bruijn indices, so we protect the error printing code in this case by giving @@ -517,11 +517,11 @@ let print_evar_constraints gl sigma = naming/renaming *) Namegen.make_all_name_different env in str" " ++ - hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++ + hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ pr_lconstr_env env sigma t2) + spc () ++ pr_leconstr_env env sigma t2) in let pr_candidate ev evi (candidates,acc) = if Option.has_some evi.evar_candidates then -- cgit v1.2.3 From 78a8d59b39dfcb07b94721fdcfd9241d404905d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 15:30:02 +0100 Subject: Introducing contexts parameterized by the inner term type. This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms. --- printing/printer.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 63aeec82c0..d9060c172d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -499,8 +499,8 @@ let print_evar_constraints gl sigma = | Some g -> let env = Goal.V82.env sigma g in fun e' -> begin - if Context.Named.equal (named_context env) (named_context e') then - if Context.Rel.equal (rel_context env) (rel_context e') then mt () + if Context.Named.equal Constr.equal (named_context env) (named_context e') then + if Context.Rel.equal Constr.equal (rel_context env) (rel_context e') then mt () else pr_rel_context_of e' sigma ++ str " |-" ++ spc () else pr_context_of e' sigma ++ str " |-" ++ spc () end -- cgit v1.2.3 From 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 23:48:28 +0100 Subject: Moving printing code from Evd to Termops. --- printing/printer.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index d9060c172d..c7d3a1ba32 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -223,7 +223,7 @@ let safe_pr_constr t = let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c + (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c else mt() @@ -240,7 +240,7 @@ let pr_puniverses f env (c,u) = else mt ()) let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) -let pr_existential_key = Evd.pr_existential_key +let pr_existential_key = Termops.pr_existential_key let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind) let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr) @@ -922,4 +922,4 @@ let pr_polymorphic b = let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}" + str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" -- cgit v1.2.3 From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: Namegen primitives now apply on evar constrs. Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. --- printing/printer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index c7d3a1ba32..447337b9a2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -515,7 +515,7 @@ let print_evar_constraints gl sigma = problem. MS: we should rather stop depending on anonymous variables, they can be used to indicate independency. Also, this depends on a strategy for naming/renaming *) - Namegen.make_all_name_different env in + Namegen.make_all_name_different env sigma in str" " ++ hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++ str (match pbty with -- cgit v1.2.3