(* Auxiliary antiquotations for the tutorial. *)

structure AntiquoteSetup =

struct

open OutputTutorial

(* functions for generating appropriate expressions *)

fun ml_pat (lhs, pat) =

(* eval function *)

fun eval_fn ctxt exp =

  ML_Context.eval_in (SOME ctxt) false Position.none exp

(* checks and prints a possibly open expressions, no index *)

val parser_ml = Scan.lift (Args.name --

  (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --

   Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))) 

val parser_ml_ind = Scan.lift (Args.name --

  Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))

(* checks and expression agains a result pattern *)

fun output_response {context = ctxt, ...} (lhs, pat) = 

    (eval_fn ctxt (ml_pat (lhs, pat));

(* checks the expressions, but does not check it against a result pattern *)

fun output_response_fake {context = ctxt, ...} (lhs, pat) = 

(* checks the expressions, but does not check it against a result pattern *)

fun ouput_response_fake_both _ (lhs, pat) = 

val single_arg = Scan.lift (Args.name)

val two_args   = Scan.lift (Args.name -- Args.name)

val _ = ThyOutput.antiquotation "ML" parser_ml output_ml

val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind

val _ = ThyOutput.antiquotation "ML_type" single_arg output_type

val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct

val _ = ThyOutput.antiquotation "ML_response" two_args output_response

val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake

val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both

fun href_link txt =

let 

  val raw = Symbol.encode_raw

  val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    

in

end 

(* checks whether a file exists in the Isabelle distribution *)

fun check_file_exists _ txt =

  (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 

   then output [href_link txt]

val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists

(* replaces the official subgoal antiquotation with one *)

(* that is closer to the actual output                  *)

fun proof_state state =

    (case try Toplevel.proof_of state of

      SOME prf => prf

    | _ => error "No proof state")

fun output_goals  {state = node, ...}  _ = 

let

  fun subgoals 0 = ""

    | subgoals 1 = "goal (1 subgoal):"

    | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"

  val state = proof_state node;

  val goals = Pretty.chunks (Proof.pretty_goals false state);

  val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);

  val (As, _) = Logic.strip_horn prop;

  val output  = (case (length As) of

                      0 => [goals] 

                    | n => [Pretty.str (subgoals n), goals])  

in 

  ThyOutput.output output

end

fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 

let

  val state = proof_state node;

  val goals = (Proof.get_goal state |> snd |> snd)

  val output  = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]  

  val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))

  val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))

in 

  ThyOutput.output output

end

val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals

val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state

end;