(* Auxiliary antiquotations for the tutorial. *)

structure AntiquoteSetup =
struct

open OutputTutorial

(* functions for generating appropriate expressions *)
fun translate_string f str =
  implode (map f (Symbol.explode str))

fun prefix_lines prfx txt = 
  map (fn s => prfx ^ s) (split_lines txt)

fun ml_with_vars ys txt = 
    implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]

fun ml_with_struct (NONE) txt = txt 
  | ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"]

fun ml_val vs stru txt = 
    txt |> ml_with_struct stru
        |> ml_with_vars  vs 

fun ml_pat (lhs, pat) =
  implode ["val ", translate_string (fn "\<dots>" => "_" | s => s) pat, " = ", lhs] 

fun ml_struct txt = 
  implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"]

fun ml_type txt = 
  implode ["val _ = NONE : (", txt, ") option"];

(* 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 *)
fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
  (eval_fn ctxt (ml_val vs stru txt); 
   output (split_lines txt))

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 a single ML-item and produces an index entry *)
fun output_ml_ind {context = ctxt, ...} (txt, stru) =
  (eval_fn ctxt (ml_val [] stru txt); 
   case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
     (NONE, bn, "")  => output_indexed {main = Code txt, minor = NoString} (split_lines txt)
   | (NONE, bn, qn)  => output_indexed {main = Code bn,  minor = Struct qn} (split_lines txt)
   | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt))

val parser_ml_ind = Scan.lift (Args.name --
  Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))

(* checks and prints structures *)
fun gen_output_struct outfn {context = ctxt, ...} txt = 
  (eval_fn ctxt (ml_struct txt); 
   outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))

val output_struct = gen_output_struct (K output)
val output_struct_ind = gen_output_struct output_indexed

(* prints functors; no checks *)
fun gen_output_funct outfn {context = ctxt, ...} txt = 
  (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))

val output_funct = gen_output_funct (K output)
val output_funct_ind = gen_output_funct output_indexed

(* checks and prints types *)
fun gen_output_type outfn {context = ctxt, ...} txt = 
  (eval_fn ctxt (ml_type txt); 
   outfn {main = Code txt, minor = Plain "type"} (split_lines txt))

val output_type = gen_output_type (K output)
val output_type_ind = gen_output_type output_indexed

(* checks and expression agains a result pattern *)
fun output_response {context = ctxt, ...} (lhs, pat) = 
    (eval_fn ctxt (ml_pat (lhs, pat));
     write_file_ml_blk lhs (ProofContext.theory_of ctxt);
     output ((prefix_lines "" lhs) @ (prefix_lines "> " 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 [] NONE lhs);
     write_file_ml_blk lhs (ProofContext.theory_of ctxt);
     output ((split_lines lhs) @ (prefix_lines "> " pat)))

(* checks the expressions, but does not check it against a result pattern *)
fun ouput_response_fake_both _ (lhs, pat) = 
    output ((split_lines lhs) @ (prefix_lines "> " pat))

val single_arg = Scan.lift (Args.name)
val two_args   = Scan.lift (Args.name -- Args.name)
val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- 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_type_ind" single_arg output_type_ind
val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind
val _ = ThyOutput.antiquotation "ML_funct" single_arg output_funct
val _ = ThyOutput.antiquotation "ML_funct_ind" single_arg output_funct_ind
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

(* FIXME: experimental *)
fun ml_eq (lhs, pat, eq) =
  implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] 

fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) = 
    (case eq of 
       NONE => eval_fn ctxt (ml_pat (lhs, pat))
     | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
     output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))

val _ = ThyOutput.antiquotation "ML_response_eq" test output_response_eq

(* checks whether a file exists in the Isabelle distribution *)
fun href_link txt =
let 
  val raw = Symbol.encode_raw
  val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    
in
 implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
end 

fun check_file_exists _ txt =
  (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
   then output [href_link txt]
   else error (implode ["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 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 o #goal o Proof.goal) state;
  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 = (#goal o Proof.goal) state;

  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;