(* Auxiliary antiquotations for the tutorial. *)

structure AntiquoteSetup =
struct

open OutputTutorial

(* functions for generating appropriate expressions *)
fun ml_val_open ys istruc txt = 
let 
  fun ml_val_open_aux ys txt = 
          "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
in
 (case istruc of
    NONE    => ml_val_open_aux ys txt
  | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end"))
end

fun ml_val txt = ml_val_open [] NONE 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 exp =
  ML_Context.eval_in (SOME ctxt) false Position.none exp

(* string functions *)
fun string_explode prefix_str txt =
  map (fn s => prefix_str ^ s) (split_lines txt)

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

(* checks and prints open expressions, calculates index entry *)
fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) =
  (eval_fn ctxt (ml_val_open ovars istruc txt);
   case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt)  of
     (NONE, bn, "")  => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString}
   | (NONE, bn, qn)  => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruc qn}
   | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruc st})

val parser_ml = Scan.lift (Args.name --
  (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
   Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))) 

(* checks and prints types and structures *)
fun output_struct {context = ctxt, ...} txt = 
  (eval_fn ctxt (ml_struct txt);
   output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "structure"})

fun output_type {context = ctxt, ...} txt = 
  (eval_fn ctxt (ml_type txt);
   output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "type"})

(* checks and expression agains a result pattern *)
fun output_response {context = ctxt, ...} (lhs, pat) = 
    (eval_fn ctxt (ml_pat (lhs, pat));
     output ((string_explode "" lhs) @ (string_explode "> " pat)))

(* checks the expressions, but does not check it against a result pattern *)
fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
    (eval_fn ctxt (ml_val lhs);
     output ((string_explode "" lhs) @ (string_explode "> " pat)))

(* checks the expressions, but does not check it against a result pattern *)
fun ouput_response_fake_both _ (lhs, pat) = 
    output ((string_explode "" lhs) @ (string_explode "> " 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_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
 (raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}")
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]
   else error ("Source file " ^ (quote txt) ^ " does not exist."))

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 output_goals  {state = node, ...}  _ = 
let
  fun subgoals 0 = ""
    | subgoals 1 = "goal (1 subgoal):"
    | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"

  fun proof_state state =
    (case try Toplevel.proof_of state of
      SOME prf => prf
    | _ => error "No proof state")

  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, B) = Logic.strip_horn prop;
  val output  = (case (length As) of
                      0 => [goals] 
                    | n => [Pretty.str (subgoals n), goals])  
in 
  ThyOutput.output output
end

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