(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* prove_by_refinement                                                    *)
(* Chapter: General                                                        *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================== *)

(*

This is an alternative to "prove"
Instead of chaining tactics together with THEN and THENL,
a list is given of all the tactics used, in the exact same order as the sequence of steps used with "e"

The advantage of this over "prove" is that the list exactly matches the sequence of steps with "e".
There is no need to reorganize the interactive proof by working out what branches were followed
when multiple goals are in play.

The navigation commands are for a proof set up with prove_by_step.  It allows one to step
through the tactics in the tactic list one-by-one for purposes of debugging.

*)



module type Prove_by_refinement_type = sig

  val prove_by_refinement : term*(tactic list) -> thm
  val prove_by_refinement_2 : string*term*(tactic list) -> thm

(*
  val prove_by_step : term*(tactic list) -> goalstack
*)

(* navigation of prove_by_step: *)

(*
  val e' : unit -> goalstack (* one step forward *)
  val f' : int -> goalstack (* n steps forward *)
  val b' : unit -> goalstack (* one step backwards *)
  val p' : unit -> goalstack  (* print goalstack *)
  val r' : unit -> goalstack (* revert to original goal *)
  val n' : unit -> int (* number of next step *)
  val l' : unit -> int (* total number of steps *)
  val x' : unit -> int (* step position of next error *)
*)

end;;


module Prove_by_refinement : Prove_by_refinement_type = struct



(* adapted from 
hol_til_2005/HOL_TIL_2005/FLYSPECK_PUB_9_2004/hol_light_o/hol-ext/tactics_2.ml
:prove_by_refinement *)



  let prove_by_refinement(t,(tacl:tactic list)) = 
    let gstate = mk_goalstate ([],t) in
    let _,sgs,just = rev_itlist 
      (fun tac gs -> by 
	 (tac) gs)
      tacl gstate in
    let th = if sgs = [] then just null_inst []
    else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
    let t' = concl th in
      if t' = t then th else
	try EQ_MP (ALPHA t' t) th
	with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;

  let prove_by_refinement_2(thm_name,t,(tacl:tactic list)) = 
    let gstate = mk_goalstate ([],t) in
    let ctacl = zip (0--(List.length tacl -1)) tacl in
    let _,sgs,just = rev_itlist 
      (fun (i,tac) gs -> 
	 try by 
	   (tac) gs
         with Failure s -> 
	   let _ = print_goalstack ([gs]) in
	   let _ = report ("Proof of "^thm_name^" fails at step: "^(string_of_int i)) in
	     failwith s
      )
      ctacl gstate in
    let th = if sgs = [] then just null_inst []
    else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
    let t' = concl th in
      if t' = t then th else
	try EQ_MP (ALPHA t' t) th
	with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;


(* replaying proof by refinement *)

(*
  let tl = ref ([]:tactic list);;
  let step = ref 0;;
  let gtm = ref `T`;;

  let g_step t = (step:=0; gtm := t; g t);;
  let e_step() = let gs = e(List.nth (!tl) (!step)) in (step:= (!step + 1);gs);; 
  let rec f_step n = if (n<=0) then p() else if (n=1) then e_step() else f_step (n-1);;
  let p_step() =p();;
  let get_step() = (!step);;
  let get_steplength() = List.length (!tl);;

  let b_step() =
    if (!step <= 0) then failwith "Can't back up any more"
    else let gs = b() in (step:= (!step -1);gs);;

  let rec next_error () = if (!step >= List.length (!tl)) then (!step) else
    try ((let _ = e(List.nth (!tl) (!step)) in () ) ; step:= (!step + 1);next_error())
    with Failure _ -> (!step);;

  let prove_by_step (gl,t) =
    (tl := t;g_step gl);;
  let r_step () = (prove_by_step (!gtm,!tl));;  (* revert *)

  let (e',f',b',p',r',n',l',x') = (e_step,f_step,b_step,p_step,r_step,get_step,get_steplength,next_error);;
*)

end;;