From ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 6 Oct 2016 17:34:12 +0200 Subject: Moving the Ltac plugin to a pack-based one. This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements. --- plugins/rtauto/g_rtauto.ml4 | 2 ++ plugins/rtauto/refl_tauto.ml | 1 + 2 files changed, 3 insertions(+) (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index d27b04834..7e58ef9a3 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin + DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 367a13333..35d6768c1 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -8,6 +8,7 @@ module Search = Explore.Make(Proof_search) +open Ltac_plugin open CErrors open Util open Term -- cgit v1.2.3 From fd6271089a0f0fcaa6d89e347d76247c7c831d23 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Sep 2016 19:44:13 +0200 Subject: [pp] Force well-formed boxes by construction. We replace open/close box commands in favor of the create box ones. --- lib/pp.ml | 14 ++------------ lib/pp.mli | 15 +++------------ plugins/rtauto/proof_search.ml | 6 +++--- 3 files changed, 8 insertions(+), 27 deletions(-) (limited to 'plugins/rtauto') diff --git a/lib/pp.ml b/lib/pp.ml index 4ff10b4d7..388eed9e4 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -32,13 +32,12 @@ type std_ppcmds = | Ppcmd_string of string | Ppcmd_glue of std_ppcmds list | Ppcmd_box of block_type * std_ppcmds + | Ppcmd_tag of pp_tag * std_ppcmds + (* Are those redundant? *) | Ppcmd_print_break of int * int | Ppcmd_white_space of int | Ppcmd_force_newline - | Ppcmd_open_box of block_type - | Ppcmd_close_box | Ppcmd_comment of string list - | Ppcmd_tag of pp_tag * std_ppcmds (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) @@ -137,13 +136,6 @@ let v n s = Ppcmd_box(Pp_vbox n,s) let hv n s = Ppcmd_box(Pp_hvbox n,s) let hov n s = Ppcmd_box(Pp_hovbox n,s) -(* Opening and closing of boxes *) -let hb n = Ppcmd_open_box(Pp_hbox n) -let vb n = Ppcmd_open_box(Pp_vbox n) -let hvb n = Ppcmd_open_box(Pp_hvbox n) -let hovb n = Ppcmd_open_box(Pp_hovbox n) -let close () = Ppcmd_close_box - (* Opening and closed of tags *) let tag t s = Ppcmd_tag(t,s) @@ -191,8 +183,6 @@ let pp_with ?pp_tag ft = cpp_open_box bty ; if not (Format.over_max_boxes ()) then pp_cmd ss; Format.pp_close_box ft () - | Ppcmd_open_box bty -> cpp_open_box bty - | Ppcmd_close_box -> pp_close_box ft () | Ppcmd_white_space n -> pp_print_break ft n 0 | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () diff --git a/lib/pp.mli b/lib/pp.mli index ed97226ae..cee7fa052 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -22,13 +22,12 @@ type std_ppcmds = | Ppcmd_string of string | Ppcmd_glue of std_ppcmds list | Ppcmd_box of block_type * std_ppcmds + | Ppcmd_tag of pp_tag * std_ppcmds + (* Are those redundant? *) | Ppcmd_print_break of int * int | Ppcmd_white_space of int | Ppcmd_force_newline - | Ppcmd_open_box of block_type - | Ppcmd_close_box | Ppcmd_comment of string list - | Ppcmd_tag of pp_tag * std_ppcmds (** {6 Formatting commands} *) @@ -69,15 +68,7 @@ val v : int -> std_ppcmds -> std_ppcmds val hv : int -> std_ppcmds -> std_ppcmds val hov : int -> std_ppcmds -> std_ppcmds -(** {6 Opening and closing of boxes} *) - -val hb : int -> std_ppcmds -val vb : int -> std_ppcmds -val hvb : int -> std_ppcmds -val hovb : int -> std_ppcmds -val close : unit -> std_ppcmds - -(** {6 Opening and closing of tags} *) +(** {6 Tagging} *) val tag : pp_tag -> std_ppcmds -> std_ppcmds diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 8b9261113..1ad4d622b 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -505,12 +505,12 @@ let pp_mapint map = pp_form obj ++ str " => " ++ pp_list (fun (i,f) -> pp_form f) l ++ cut ()) ) map; - str "{ " ++ vb 0 ++ (!pp) ++ str " }" ++ close () + str "{ " ++ hv 0 (!pp ++ str " }") let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2 let pp_gl gl= cut () ++ - str "{ " ++ vb 0 ++ + str "{ " ++ hv 0 ( begin match gl.abs with None -> str "" @@ -520,7 +520,7 @@ let pp_gl gl= cut () ++ str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++ str "arrows=" ++ pp_mapint gl.right ++ cut () ++ str "cnx =" ++ pp_list pp_connect gl.cnx ++ cut () ++ - str "goal =" ++ pp_form gl.gl ++ str " }" ++ close () + str "goal =" ++ pp_form gl.gl ++ str " }") let pp = function -- cgit v1.2.3