From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 parsing/tactic_printer.ml | 141 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 141 insertions(+)
 create mode 100644 parsing/tactic_printer.ml

(limited to 'parsing/tactic_printer.ml')

diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
new file mode 100644
index 00000000..3584e375
--- /dev/null
+++ b/parsing/tactic_printer.ml
@@ -0,0 +1,141 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: tactic_printer.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
+
+open Pp
+open Util
+open Sign
+open Evd
+open Tacexpr
+open Proof_type
+open Proof_trees
+open Logic
+open Printer
+
+let pr_tactic = function
+  | TacArg (Tacexp t) ->
+      (*top tactic from tacinterp*)
+      Pptactic.pr_glob_tactic (Global.env()) t
+  | t -> 
+      Pptactic.pr_tactic (Global.env()) t
+
+let pr_rule = function
+  | Prim r -> hov 0 (pr_prim_rule r)
+  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
+  | Change_evars ->
+      (* This is internal tactic and cannot be replayed at user-level.
+         Function pr_rule_dot below is used when we want to hide
+         Change_evars *)
+      str "Evar change"
+
+(* Does not print change of evars *)
+let pr_rule_dot = function 
+  | Change_evars -> mt ()
+  | r -> pr_rule r ++ str"."
+
+exception Different
+
+(* We remove from the var context of env what is already in osign *)
+let thin_sign osign sign =
+  Sign.fold_named_context
+    (fun (id,c,ty as d) sign ->
+       try 
+	 if Sign.lookup_named id osign = (id,c,ty) then sign
+	 else raise Different
+       with Not_found | Different -> Environ.push_named_context_val d sign)
+    sign ~init:Environ.empty_named_context_val
+
+let rec print_proof sigma osign pf =
+  let {evar_hyps=hyps; evar_concl=cl; 
+       evar_body=body} = pf.goal in
+  let hyps = Environ.named_context_of_val hyps in
+  let hyps' = thin_sign osign hyps in
+  match pf.ref with
+    | None -> 
+	hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body})
+    | Some(r,spfl) ->
+    	hov 0 
+	  (hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++
+	   spc () ++ str" BY " ++
+	   hov 0 (pr_rule r) ++ fnl () ++
+	   str"  " ++
+	   hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
+)
+	  
+let pr_change gl = 
+  str"Change " ++
+  pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
+
+let rec print_script nochange sigma osign pf =
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+  let sign = Environ.named_context_of_val sign in
+  match pf.ref with
+    | None ->
+        (if nochange then 
+	  (str"<Your Tactic Text here>") 
+	else 
+	  pr_change pf.goal)
+	++ fnl ()
+    | Some(r,spfl) ->
+        ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+           pr_rule_dot r ++ fnl () ++
+           prlist_with_sep pr_fnl
+             (print_script nochange sigma sign) spfl)
+
+(* printed by Show Script command *)
+let print_treescript nochange sigma _osign pf =
+  let rec aux top pf =
+    match pf.ref with
+    | None ->
+        if nochange then 
+	  (str"<Your Tactic Text here>") 
+	else 
+	  (pr_change pf.goal)
+    | Some(r,spfl) ->
+        (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
+	pr_rule_dot r ++
+	match spfl with
+	| [] -> mt ()
+	| [spf] -> fnl () ++ (if top then mt () else str "  ") ++ aux top spf
+	| _ -> fnl () ++ str " " ++
+	    hov 0 (prlist_with_sep fnl (aux false) spfl)
+  in hov 0 (aux true pf)
+
+let rec print_info_script sigma osign pf =
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+  match pf.ref with
+    | None -> (mt ())
+    | Some(Change_evars,[spf]) ->
+        print_info_script sigma osign spf
+    | Some(r,spfl) ->
+        (pr_rule r ++ 
+           match spfl with
+             | [pf1] ->
+                 if pf1.ref = None then 
+		   (str "." ++ fnl ())
+                 else 
+		   (str";" ++ brk(1,3) ++
+		      print_info_script sigma 
+		      (Environ.named_context_of_val sign) pf1)
+             | _ -> (str"." ++ fnl () ++
+                       prlist_with_sep pr_fnl
+                         (print_info_script sigma 
+			    (Environ.named_context_of_val sign)) spfl))
+
+let format_print_info_script sigma osign pf = 
+  hov 0 (print_info_script sigma osign pf)
+    
+let print_subscript sigma sign pf = 
+  if is_tactic_proof pf then 
+    format_print_info_script sigma sign (subproof_of_proof pf)
+  else 
+    format_print_info_script sigma sign pf
+
+let _ = Refiner.set_info_printer print_subscript
+
-- 
cgit v1.2.3