(* ========================================================================== *)
(* ML EXPORT (HOL LIGHT)                                                      *)
(* - Exporting recorded tactics into a proof script                           *)
(*                                                                            *)
(* By Mark Adams                                                              *)
(* Copyright (c) Univeristy of Edinburgh, 2012                                *)
(* ========================================================================== *)


(* Routines for exporting an ML tactic proof script from the recorded tactic  *)
(* proof tree.                                                                *)



(* Translation to hiproof *)

let rec gtree_to_hiproof gtr =
  let (_,gtrm) = gtr in
  match !gtrm with
    Gactive
       -> Hactive
  | Gexit id
       -> Hidentity
  | Gexecuted (gstp,gtrs)
       -> let h1 =
             match gstp with
               Gatom info | Gbox (info,_,true)
                  -> Hatomic (info, length gtrs)
             | Gbox (info,gtr,false)
                  -> Hlabelled (info, gtree_to_hiproof gtr) in
          let h2 = Htensor (map gtree_to_hiproof gtrs) in
          Hsequence (h1,h2);;



(* ** PRINT UTILITIES ** *)


(* Basics *)

let print_string_if b x = if b then print_string x;;

let print_fstring x = print_string ("\"" ^ String.escaped x ^ "\"");;

let print_fterm tm = print_string ("`" ^ string_of_term tm ^ "`");;

let print_ftype ty = print_string ("`" ^ string_of_type ty ^ "`");;


(* Printer for 'finfo' *)

let rec print_farg x0 br arg =
  match arg with
    Fint n       -> print_int n
  | Fstring x    -> print_fstring x
  | Fterm tm     -> print_fterm tm
  | Ftype ty     -> print_ftype ty
  | Fthm prf     -> print_finfo "<rule>" br prf
  | Fpair (arg1,arg2)
       -> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in
          (print_string_if br "(";
           print_farg x0 false arg1;
           print_string sep;
           print_farg x0 false arg2;
           print_string_if br ")")
  | Flist args 
       -> let sep = if (forall is_atomic_farg args) then ";" else "; " in
          (print_string "[";
           print_seplist (print_farg x0 false) sep args;
           print_string "]")
  | Ffn f
       -> (print_finfo x0 br f)

and print_finfo x0 br ((x_,args):finfo) =
  (print_string_if (br & not (is_empty args)) "(";
   print_option x0 x_;
   do_list (fun arg -> print_string " "; print_farg x0 true arg) args;
   print_string_if (br & not (is_empty args)) ")");;


(* Printer for tactic 'finfo' *)

let print_tactic br ((x_,args):finfo) =
  print_finfo "<tactic>" br ((x_,args):finfo);;


(* Printer for subgoal comments *)

let print_hicomment_line ns =
  (print_string "(* *** Subgoal ";
   print_int (hd ns);
   do_list (fun n -> print_string "."; print_int n) (tl ns);
   print_string " *** *)\n");;


(* print_tactic_line *)

let print_tactic_line_with pr arg =
  (print_string "e ("; pr false arg; print_string ");;\n");;

let print_tactic_line info =
  (print_tactic_line_with print_tactic info);;

let print_hitrace_line_with fl pr htr =
  match htr with
    Hicomment ns -> if fl then print_hicomment_line ns
  | Hiproof h    -> print_tactic_line_with pr h;;


(* print_hiproof0 *)

(* This is a utility used in exporters, for basic cases not explicitly dealt  *)
(* with in the exporter's special cases.  Does not print tacticals, other     *)
(* than 'THEN' (for single arity) and 'THENL' (for multi-arity).  Argument    *)
(* 'pr' is the printer to be used on subcases.                                *)

let print_hiproof0 pr br h =
  match h with
    Hactive
       -> print_string "..."
  | Hatomic (info,_)
       -> print_tactic br info
  | Hidentity
       -> print_string "ALL_TAC"
  | Hlabelled (info,h0)
       -> pr br h0
  | Hsequence (h1, Htensor h2s)
       -> (print_string_if br "(";
           pr false h1;
           print_string " THENL [";
           print_seplist (pr false) "; " h2s;
           print_string "]";
           print_string_if br ")")
  | Hsequence (h1,Hempty)
       -> (pr br h1)
  | Hsequence (h1,h2)
       -> (print_string_if br "(";
           pr false h1;
           print_string " THEN ";
           pr true h2;
           print_string_if br ")")
  | Htensor _
       -> failwith "print_hiproof: Unexpected tensor"
  | Hempty
       -> failwith "print_hiproof: Unexpected empty";;


(* A basic hiproof printer that just uses 'print_hiproof0'.                   *)

let rec print_hiproof1 br h = print_hiproof0 print_hiproof1 br h;;


(* print_hiproof2 *)

let rec print_hiproof2 br h =
  match h with
    Hlabelled ((Some "REPEAT", _), Hsequence (h1,h2))  (* only if repeats *)
       -> (print_string_if br "(";
           print_string "REPEAT ";
           print_hiproof2 true h1;
           print_string_if br ")")
  | Hlabelled ((Some "THEN", _),
               Hsequence (h1, Htensor (h2::h2s)))      (* only if tac2 used *)
       -> (print_string_if br "(";
           print_hiproof2 false h1;
           print_string " THEN ";
           print_hiproof2 true h2;
           print_string_if br ")")
  | Hlabelled (((Some "SUBGOAL_THEN", (Fterm tm)::[farg]) as info), _)
       -> (print_tactic br info)
  | _  -> (print_hiproof0 print_hiproof2 br h);;



(* ** PRINTERS ** *)


(* Executed proof *)

(* Prints proof according to how it was executed, i.e. using the original e-  *)
(* steps and according to any user-supplied 'REPEAT' and 'THEN' tacticals,    *)
(* but only those parts that actually execute and not according to any other  *)
(* tacticals.                                                                 *)

let print_hiproof_executed_proof fl h =
  let h' = trivsimp_hiproof h in
  let htrs' = hiproof_block_trace h' in
  do_list (print_hitrace_line_with fl print_hiproof2) htrs';;

let print_gtree_executed_proof fl gtr =
  (print_hiproof_executed_proof fl o gtree_to_hiproof) gtr;;

let print_executed_proof fl = print_gtree_executed_proof fl !the_goal_tree;;


(* Packaged proof *)

(* Prints proof as a monolithic step, spotting opportunities for 'REPEAT' and *)
(* multi-arity 'THEN' tacticals in addition to those already in proof.        *)
(* ! 'REPEAT' not currently catered for.                                      *)

let print_hiproof_packaged_proof h =
  let h' = (thenise_hiproof o trivsimp_hiproof o leftgroup_hiproof) h in
  print_tactic_line_with print_hiproof2 h';;

let print_gtree_packaged_proof gtr =
  (print_hiproof_packaged_proof o gtree_to_hiproof) gtr;;

let print_packaged_proof () = print_gtree_packaged_proof !the_goal_tree;;


(* THENL proof *)

(* Prints proof as a naive monolithic step, using 'THEN' for single arity,    *)
(* and 'THENL' for multi-arity (even if each subgoal has the same proof).     *)
(* This gives the full structure of each tactic execution.                    *)

let print_hiproof_thenl_proof h =
  let h' = (trivsimp_hiproof o delabel_hiproof) h in
  print_tactic_line_with print_hiproof1 h';;

let print_gtree_thenl_proof gtr =
  (print_hiproof_thenl_proof o gtree_to_hiproof) gtr;;

let print_thenl_proof () = print_gtree_thenl_proof !the_goal_tree;;


(* Flat proof *)

(* This exports a proof as a flat series of e-steps, with no tacticals.       *)

let print_hiproof_flat_proof fl h =
  let h' = (trivsimp_hiproof o rightgroup_hiproof o trivsimp_hiproof o
            delabel_hiproof) h in
  let htrs' = hiproof_block_trace h' in
  do_list (print_hitrace_line_with fl print_hiproof2) htrs';;

let print_gtree_flat_proof fl gtr =
  (print_hiproof_flat_proof fl o gtree_to_hiproof) gtr;;

let print_flat_proof fl = print_gtree_flat_proof fl !the_goal_tree;;