(************************************************************************)
(*  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