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

let

  fun output {state: Toplevel.state, source = src, context = 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.antiquotation "ML" parser output

end

(* checks and prints types and structures *)

fun output_exp ml =

let 

  fun output {state: Toplevel.state, source = src, context = ctxt} (txt,pos) = 

    (eval_fn ctxt pos (ml txt);

     output_fn src ctxt (string_explode "" txt))

in

  ThyOutput.antiquotation "ML_type" single_arg output

end

(* checks and expression agains a result pattern *)

fun output_ml_response () =

let

  fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat),pos) = 

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

     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))

in

  ThyOutput.antiquotation "ML_response" two_args output

end

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

fun output_ml_response_fake () =

let

  fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs, pat), pos) = 

    (eval_fn ctxt pos (ml_val lhs);

     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))

in

  ThyOutput.antiquotation "ML_response_fake" two_args output

end

(* just prints an expression and a result pattern *)

fun output_ml_response_fake_both () =

let 

  fun ouput {state: Toplevel.state, source = src, context = ctxt}   ((lhs,pat), _) = 

    output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))

in

  ThyOutput.antiquotation "ML_response_fake_both" two_args ouput

end

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

fun check_file_exists () =

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.antiquotation "ML_file" (Scan.lift Args.name)

      (fn _ => fn s => (check s; ThyOutput.output [Pretty.str s]))

end

(* replaces the official subgoal antiquotation with one *)

(* that is closer to the actual output                  *)

(*

fun output_goals  {state = node, source: Args.src, context: Proof.context}  _ = 

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 

  output 

end

*)

val _ = output_ml ();

val _ = check_file_exists ();

val _ = output_ml_response ();

val _ = output_ml_response_fake ();

val _ = output_ml_response_fake_both ();

val _ = output_exp ml_struct;

val _ = output_exp ml_type;

(*val _ = output_goals*)

end;