(* Auxiliary antiquotations for the Cookbook. *)

structure AntiquoteSetup: sig end =

struct

(* main body *)

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 (rhs, pat) =

  let 

     val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))

  in "val " ^ pat' ^ " = " ^ rhs end;

fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";

fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";

val transform_cmts_str =

  Source.of_string #> ML_Lex.source #> Source.exhaust #>

  Chunks.transform_cmts #> implode;

fun output_ml ml src ctxt ((txt,ovars),pos) =

  (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);

   txt |> transform_cmts_str |> space_explode "\n" |>

   Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt)

fun output_ml_aux ml src ctxt (txt,pos) =

  output_ml (K ml) src ctxt ((txt,()),pos) 

fun output_ml_response ml src ctxt ((lhs,pat),pos) = 

  (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));

  let 

  in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)

fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = 

  (ML_Context.eval_in (SOME ctxt) false pos (ml lhs);

  in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)

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", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --

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

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

                                                                 (output_ml ml_val_open)),

   ("ML_file", check_file_exists),

   ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 

      (output_ml_response ml_pat)),

   ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 

      (output_ml_response_fake ml_val)),

   ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),

   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)),

   ("subgoals", output_goals)];

end;