(* Auxiliary antiquotations for the tutorial. *)

structure AntiquoteSetup: sig end =
struct

(* functions for generating appropriate expressions *)

fun ml_val_open (ys, xs) txt = 
  let fun ml_val_open_aux ys txt = 
          "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
  in
    (case xs of
       [] => ml_val_open_aux ys txt
     | _  => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
  end;

fun ml_val txt = ml_val_open ([],[]) txt;

fun ml_pat (lhs, pat) =
  let 
     val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
  in "val " ^ pat' ^ " = " ^ lhs end;

fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";

(* eval function *)
fun eval_fn ctxt pos exp =
  ML_Context.eval_in (SOME ctxt) false pos exp

(* string functions *)
fun string_explode str txt =
  map (fn s => str ^ s) (space_explode "\n" txt)

val transform_cmts_str =
     Source.of_string 
  #> ML_Lex.source 
  #> Source.exhaust 
  #> Chunks.transform_cmts 
  #> implode 
  #> string_explode "";

(* parser for single and two arguments *)
val single_arg = Scan.lift (OuterParse.position Args.name)
val two_args = Scan.lift (OuterParse.position (Args.name -- Args.name))

(* output function *)
val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s)

(* checks and prints open expressions *)
fun output_ml src node =
let
  fun output src ctxt ((txt,ovars),pos) =
    (eval_fn ctxt pos (ml_val_open ovars txt);
     output_fn src ctxt (transform_cmts_str txt))

  val parser = Scan.lift (OuterParse.position (Args.name --
      (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
       Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))) 
in
  ThyOutput.args parser output src node
end

(* checks and prints types and structures *)
fun output_exp ml src node =
let 
  fun output src ctxt (txt,pos) = 
    (eval_fn ctxt pos (ml txt);
     output_fn src ctxt (string_explode "" txt))
in
  ThyOutput.args single_arg output src node
end

(* checks and expression agains a result pattern *)
fun output_ml_response src node =
let
  fun output src ctxt ((lhs,pat),pos) = 
    (eval_fn ctxt pos (ml_pat (lhs,pat));
     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))
in
  ThyOutput.args two_args output src node
end

(* checks the expressions, but does not check it against a result pattern *)
fun output_ml_response_fake src node =
let
  fun output src ctxt ((lhs,pat),pos) = 
    (eval_fn ctxt pos (ml_val lhs);
     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))
in
  ThyOutput.args two_args output src node
end

(* just prints an expression and a result pattern *)
fun output_ml_response_fake_both src node =
let 
  fun ouput src ctxt ((lhs,pat), _) = 
    output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))
in
  ThyOutput.args two_args ouput src node
end

(* checks whether a file exists in the Isabelle distribution *)
fun check_file_exists src node =
let 
  fun check txt =
   if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
   else error ("Source file " ^ (quote txt) ^ " does not exist.")
in
  ThyOutput.args (Scan.lift Args.name)
      (ThyOutput.output (fn _ => fn s => (check s; Pretty.str s))) src node
end

(* replaces the official subgoal antiquotation with one *)
(* that is closer to the actual output                  *)
fun output_goals src node = 
let 
  fun subgoals 0 = ""
    | subgoals 1 = "goal (1 subgoal):"
    | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):";
 
  fun proof_state node =
     (case Option.map Toplevel.proof_node node of
          SOME (SOME prf) => ProofNode.current prf
        | _ => error "No proof state");

  val state = proof_state node;
  val goals = Proof.pretty_goals false state;

  val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
  val (As, B) = Logic.strip_horn prop;
  val output  = (case (length As) of
                      0 => goals 
                    | n => (Pretty.str (subgoals n))::goals)  
in 
  ThyOutput.args (Scan.succeed ()) 
   (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node
end

val _ = ThyOutput.add_commands
  [("ML", output_ml),
   ("ML_file", check_file_exists),
   ("ML_response", output_ml_response),
   ("ML_response_fake", output_ml_response_fake),
   ("ML_response_fake_both", output_ml_response_fake_both),
   ("ML_struct", output_exp ml_struct),
   ("ML_type", output_exp ml_type),
   ("subgoals", output_goals)];
   
end;