place all pretty-printing files in new dir printing/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 170 insertions, 0 deletions

diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml
new file mode 100644
index 0000000000..2c51abcd01
--- /dev/null
+++ b/printing/tactic_printer.ml
@@ -0,0 +1,170 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Sign
+open Evd
+open Tacexpr
+open Proof_type
+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)
+  | Nested(cmpd,_) ->
+      begin
+	match cmpd with
+	  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
+      end
+  | Daimon -> str "<Daimon>"
+  | Decl_proof _ -> str "proof"
+
+let uses_default_tac = function
+  | Nested(Tactic(_,dflt),_) -> dflt
+  | _ -> false
+
+(* Does not print change of evars *)
+let pr_rule_dot = function
+  | Prim Change_evars ->str "PC: ch_evars" ++  mt ()
+      (* PC: this might be redundant *)
+  | r ->
+      pr_rule r ++ if uses_default_tac r then str "..." else str"."
+
+let pr_rule_dot_fnl = function
+  | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_)
+                              | TacMutualCofix (true,_,_))),_),_) ->
+      (* Very big hack to not display hidden tactics in "Theorem with" *)
+      (* (would not scale!) *)
+      mt ()
+   | Prim Change_evars -> mt ()
+   | r -> pr_rule_dot r ++ fnl ()
+
+exception Different
+
+let rec print_proof sigma osign pf =
+  (* spiwack: [osign] is currently ignored, not sure if this function is even used. *)
+  let hyps = Environ.named_context_of_val (Goal.V82.hyps sigma pf.goal) in
+  match pf.ref with
+    | None ->
+	hov 0 (pr_goal {sigma = sigma; it=pf.goal })
+    | Some(r,spfl) ->
+	hov 0
+	  (hov 0 (pr_goal {sigma = sigma; it=pf.goal }) ++
+	   spc () ++ str" BY " ++
+	   hov 0 (pr_rule r) ++ fnl () ++
+	   str"  " ++
+	   hov 0 (prlist_with_sep fnl (print_proof sigma hyps) spfl))
+
+let pr_change sigma gl =
+  str"change " ++
+  pr_lconstr_env (Goal.V82.env sigma gl) (Goal.V82.concl sigma gl) ++ str"."
+
+let print_decl_script tac_printer ?(nochange=true) sigma pf =
+  let rec print_prf pf =
+  match pf.ref with
+    | None ->
+	(if nochange then
+	   (str"<Your Proof Text here>")
+	 else
+	   pr_change sigma pf.goal)
+	++ fnl ()
+    | Some (Daimon,[]) -> str "(* Some proof has been skipped here *)"
+    | Some (Prim Change_evars,[subpf]) -> print_prf subpf
+    | _ -> anomaly "Not Applicable" in
+  print_prf pf
+
+let print_script ?(nochange=true) sigma pf =
+  let rec print_prf pf =
+  match pf.ref with
+    | None ->
+        (if nochange then
+	   (str"<Your Tactic Text here>")
+	 else
+	   pr_change sigma pf.goal)
+	++ fnl ()
+    | Some(Decl_proof opened,script) ->
+	assert (List.length script = 1);
+	begin
+	  if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())
+	end ++
+	  begin
+	    hov 0 (str "proof." ++ fnl () ++
+		     print_decl_script print_prf
+		     ~nochange sigma (List.hd script))
+	  end ++ fnl () ++
+	  begin
+	    if opened then mt () else (str "end proof." ++ fnl ())
+	  end
+    | Some(Daimon,spfl) ->
+	((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
+	   prlist_with_sep fnl print_prf spfl )
+    | Some(rule,spfl) ->
+	((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
+	   pr_rule_dot_fnl rule ++
+	   prlist_with_sep fnl print_prf spfl ) in
+  print_prf pf
+
+(* printed by Show Script command *)
+
+let print_treescript ?(nochange=true) sigma pf =
+  let rec print_prf pf =
+    match pf.ref with
+    | None ->
+        if nochange then
+	  str"<Your Proof Text here>"
+	else pr_change sigma pf.goal
+    | Some(Decl_proof opened,script) ->
+	assert (List.length script = 1);
+	begin
+	  if nochange then mt () else pr_change sigma pf.goal ++ fnl ()
+	end ++
+	hov 0
+	  begin str "proof." ++ fnl () ++
+	    print_decl_script print_prf ~nochange sigma (List.hd script)
+	  end ++ fnl () ++
+	begin
+	  if opened then mt () else (str "end proof." ++ fnl ())
+	end
+    | Some(Daimon,spfl) ->
+	(if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
+	prlist_with_sep fnl (print_script ~nochange sigma) spfl
+    | Some(r,spfl) ->
+        let indent = if List.length spfl >= 2 then 1 else 0 in
+        (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
+        hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl)
+  in hov 0 (print_prf pf)
+
+let rec print_info_script sigma osign pf =
+  let sign = Goal.V82.hyps sigma pf.goal in
+  match pf.ref with
+    | None -> (mt ())
+    | 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 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)