restructuration des printers: proofs passe avant parsing

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

7 files changed, 411 insertions, 7 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index ded6e823f..3a02e5f25 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -108,10 +108,6 @@ let pr_opt_type pr = function
 
 let pr_tight_coma () = str "," ++ cut ()
 
-let pr_name = function
-  | Anonymous -> str "_"
-  | Name id -> pr_id id
-
 let pr_located pr (loc,x) = pr x
 
 let pr_let_binder pr x a =
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 5f01e7173..c961baa01 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -26,7 +26,6 @@ val split_fix : int -> constr_expr -> constr_expr ->
 val pr_global : Idset.t -> global_reference -> std_ppcmds
 
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
-val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
 val pr_red_expr :
   ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index bddf601d4..e093954f8 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -28,7 +28,6 @@ let pr_global x =
     Ppconstrnew.pr_global Idset.empty x
   else
     Ppconstr.pr_global Idset.empty x
-let pr_name = Ppconstr.pr_name
 let pr_opt = Ppconstr.pr_opt
 let pr_occurrences = Ppconstr.pr_occurrences
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index c331eea6f..06a1cc812 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -25,6 +25,10 @@ open Libnames
 open Extend
 open Nametab
 open Ppconstr
+open Evd
+open Proof_type
+open Refiner
+open Pfedit
 
 let emacs_str s = if !Options.print_emacs then s else "" 
 
@@ -124,7 +128,8 @@ let prterm t = prterm_env (Global.env()) t
 let prtype t = prtype_env (Global.env()) t
 let prjudge j = prjudge_env (Global.env()) j
 
-let _ = Termops.set_print_constr prterm
+let _ = Termops.set_print_constr prterm_env
+(*let _ = Tactic_debug.set_pattern_printer pr_pattern_env*)
 
 let pr_constant env cst = prterm_env env (mkConst cst)
 let pr_existential env ev = prterm_env env (mkEvar ev)
@@ -250,3 +255,226 @@ let pr_context_of env = match Options.print_hyps_limit () with
   | None -> hv 0 (pr_context_unlimited env)
   | Some n -> hv 0 (pr_context_limit n env)
 
+
+(* display complete goal *)
+let pr_goal g =
+  let env = evar_env g in
+  let penv = pr_context_of env in
+  let pc = prterm_env_at_top env g.evar_concl in
+  str"  " ++ hv 0 (penv ++ fnl () ++
+		   str (emacs_str (String.make 1 (Char.chr 253)))  ++
+                   str "============================" ++ fnl ()  ++
+                   str" "  ++ pc) ++ fnl ()
+
+(* display the conclusion of a goal *)
+let pr_concl n g =
+  let env = evar_env g in
+  let pc = prterm_env_at_top env g.evar_concl in
+  str (emacs_str (String.make 1 (Char.chr 253)))  ++
+  str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
+
+(* display evar type: a context and a type *)
+let pr_evgl_sign gl = 
+  let ps = pr_named_context_of (evar_env gl) in
+  let pc = prterm gl.evar_concl in
+  hov 0 (str"["  ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]")
+
+(* Print an enumerated list of existential variables *)
+let rec pr_evars_int i = function
+  | [] -> (mt ())
+  | (ev,evd)::rest ->
+      let pegl = pr_evgl_sign evd in 
+      let pei = pr_evars_int (i+1) rest in
+      (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
+              str (string_of_existential ev)  ++ str " : " ++ pegl)) ++ 
+      fnl () ++ pei
+
+let pr_subgoal n =
+  let rec prrec p = function
+    | [] -> error "No such goal"
+    | g::rest ->
+       	if p = 1 then
+          let pg = pr_goal g in
+          v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
+       	else 
+	  prrec (p-1) rest
+  in 
+  prrec n
+
+(* Print open subgoals. Checks for uninstantiated existential variables *)
+let pr_subgoals sigma = function 
+  | [] -> 
+      let exl = Evarutil.non_instantiated sigma in 
+      if exl = [] then 
+	(str"Proof completed."  ++ fnl ())
+      else
+        let pei = pr_evars_int 1 exl in
+        (str "No more subgoals but non-instantiated existential " ++
+           str "variables :"  ++fnl () ++ (hov 0 pei))
+  | [g] ->
+      let pg = pr_goal g in
+      v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
+  | g1::rest ->
+      let rec pr_rec n = function
+        | [] -> (mt ())
+        | g::rest ->
+            let pc = pr_concl n g in
+            let prest = pr_rec (n+1) rest in
+            (cut () ++ pc ++ prest) 
+      in
+      let pg1 = pr_goal g1 in
+      let prest = pr_rec 2 rest in
+      v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
+	   ++ pg1 ++ prest ++ fnl ())
+
+
+let pr_subgoals_of_pfts pfts = 
+  let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in 
+  let sigma = (top_goal_of_pftreestate pfts).sigma in
+  pr_subgoals sigma gls
+
+let pr_open_subgoals () =
+  let pfts = get_pftreestate () in
+  match focus() with
+    | 0 -> 
+	pr_subgoals_of_pfts pfts
+    | n -> 
+	let pf = proof_of_pftreestate pfts in
+	let gls = fst (frontier pf) in 
+	assert (n > List.length gls);
+	if List.length gls < 2 then 
+	  pr_subgoal n gls
+	else 
+	  v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
+	  pr_subgoal n gls)
+
+let pr_nth_open_subgoal n =
+  let pf = proof_of_pftreestate (get_pftreestate ()) in
+  pr_subgoal n (fst (frontier pf))
+
+(* Elementary tactics *)
+
+let pr_prim_rule_v7 = function
+  | Intro id -> 
+      str"Intro " ++ pr_id id
+	
+  | Intro_replacing id -> 
+      (str"intro replacing "  ++ pr_id id)
+	
+  | Cut (b,id,t) ->
+      if b then
+        (str"Assert " ++ print_constr t)
+      else
+        (str"Cut " ++ print_constr t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]")
+	
+  | FixRule (f,n,[]) ->
+      (str"Fix " ++ pr_id f ++ str"/" ++ int n)
+      
+  | FixRule (f,n,others) -> 
+      let rec print_mut = function
+	| (f,n,ar)::oth -> 
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ print_constr ar ++ print_mut oth
+        | [] -> mt () in
+      (str"Fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut others)
+
+  | Cofix (f,[]) ->
+      (str"Cofix " ++ pr_id f)
+
+  | Cofix (f,others) ->
+      let rec print_mut = function
+	| (f,ar)::oth ->
+	  (pr_id f ++ str" : " ++ print_constr ar ++ print_mut oth)
+        | [] -> mt () in
+      (str"Cofix " ++ pr_id f ++  str" with " ++ print_mut others)
+
+  | Refine c -> 
+      str(if occur_meta c then "Refine " else "Exact ") ++
+      Constrextern.with_meta_as_hole print_constr c
+      
+  | Convert_concl c ->
+      (str"Change "  ++ print_constr c)
+      
+  | Convert_hyp (id,None,t) ->
+      (str"Change "  ++ print_constr t  ++ spc ()  ++ str"in "  ++ pr_id id)
+
+  | Convert_hyp (id,Some c,t) ->
+      (str"Change "  ++ print_constr c  ++ spc ()  ++ str"in "
+       ++ pr_id id ++ str" (Type of "  ++ pr_id id ++ str ")")
+      
+  | Thin ids ->
+      (str"Clear "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | ThinBody ids ->
+      (str"ClearBody "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | Move (withdep,id1,id2) ->
+      (str (if withdep then "Dependent " else "") ++
+	 str"Move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+  | Rename (id1,id2) ->
+      (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+
+let pr_prim_rule_v8 = function
+  | Intro id -> 
+      str"intro " ++ pr_id id
+	
+  | Intro_replacing id -> 
+      (str"intro replacing "  ++ pr_id id)
+	
+  | Cut (b,id,t) ->
+      if b then
+        (str"assert " ++ print_constr t)
+      else
+        (str"cut " ++ print_constr t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
+	
+  | FixRule (f,n,[]) ->
+      (str"fix " ++ pr_id f ++ str"/" ++ int n)
+      
+  | FixRule (f,n,others) -> 
+      let rec print_mut = function
+	| (f,n,ar)::oth -> 
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ print_constr ar ++ print_mut oth
+        | [] -> mt () in
+      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut others)
+
+  | Cofix (f,[]) ->
+      (str"cofix " ++ pr_id f)
+
+  | Cofix (f,others) ->
+      let rec print_mut = function
+	| (f,ar)::oth ->
+	  (pr_id f ++ str" : " ++ print_constr ar ++ print_mut oth)
+        | [] -> mt () in
+      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
+
+  | Refine c -> 
+      str(if occur_meta c then "refine " else "exact ") ++
+      Constrextern.with_meta_as_hole print_constr c
+      
+  | Convert_concl c ->
+      (str"change "  ++ print_constr c)
+      
+  | Convert_hyp (id,None,t) ->
+      (str"change "  ++ print_constr t  ++ spc ()  ++ str"in "  ++ pr_id id)
+
+  | Convert_hyp (id,Some c,t) ->
+      (str"change "  ++ print_constr c  ++ spc ()  ++ str"in "
+       ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
+      
+  | Thin ids ->
+      (str"clear "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | ThinBody ids ->
+      (str"clearbody "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | Move (withdep,id1,id2) ->
+      (str (if withdep then "dependent " else "") ++
+	 str"move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+  | Rename (id1,id2) ->
+      (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+
+let pr_prim_rule t =
+  if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t
diff --git a/parsing/printer.mli b/parsing/printer.mli
index cd0f3d39e..04c61ed05 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -19,6 +19,8 @@ open Rawterm
 open Pattern
 open Nametab
 open Termops
+open Evd
+open Proof_type
 (*i*)
 
 (* These are the entry points for printing terms, context, tac, ... *)
@@ -58,3 +60,13 @@ val pr_context_of   : env -> std_ppcmds
 
 val emacs_str       : string -> string
 
+(* Proofs *)
+val pr_goal : goal -> std_ppcmds
+val pr_subgoals : evar_map -> goal list -> std_ppcmds
+val pr_subgoal   : int -> goal list -> std_ppcmds
+
+val pr_open_subgoals    : unit -> std_ppcmds
+val pr_nth_open_subgoal : int -> std_ppcmds
+val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds
+
+val pr_prim_rule : prim_rule -> std_ppcmds
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
new file mode 100644
index 000000000..6063e9448
--- /dev/null
+++ b/parsing/tactic_printer.ml
@@ -0,0 +1,143 @@
+(************************************************************************)
+(*  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$ *)
+
+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) ->
+      if !Options.v7 then
+	Pptactic.pr_glob_tactic t (*top tactic from tacinterp*)
+      else
+	Pptacticnew.pr_glob_tactic (Global.env()) t
+  | t -> 
+      if !Options.v7 then
+	Pptactic.pr_tactic t
+      else
+	Pptacticnew.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 -> add_named_decl d sign)
+    sign ~init:empty_named_context
+
+let rec print_proof sigma osign pf =
+  let {evar_hyps=hyps; evar_concl=cl; 
+       evar_body=body} = pf.goal 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 " ++
+  prterm_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
+  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 =
+    let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+    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 sign pf1)
+             | _ -> (str"." ++ fnl () ++
+                       prlist_with_sep pr_fnl
+                         (print_info_script sigma 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
+
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
new file mode 100644
index 000000000..b4ad0143e
--- /dev/null
+++ b/parsing/tactic_printer.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Pp
+open Sign
+open Evd
+open Tacexpr
+open Proof_type
+(*i*)
+
+(* These are the entry points for tactics, proof trees, ... *)
+
+val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
+val pr_rule     : rule -> std_ppcmds
+val pr_tactic   : tactic_expr -> std_ppcmds
+val print_script :
+  bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
+val print_treescript :
+  bool -> evar_map -> named_context -> proof_tree -> std_ppcmds