(* 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_vars ys src = 

    ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @

    ML_Lex.read " => (" @ src @ ML_Lex.read ")"

fun ml_with_struct (NONE) src = ML_Lex.read_source false src 

  | ml_with_struct (SOME st) src = 

      ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source false src @ ML_Lex.read " end"

fun ml_val vs stru txt = 

    txt |> ml_with_struct stru

        |> ml_with_vars vs 

fun ml_pat pat lhs =

  ML_Lex.read "val " @ ML_Lex.read (translate_string (fn "\<dots>" => "_" | s => s) pat) @ 

  ML_Lex.read " = " @

  ML_Lex.read_source false lhs 

fun ml_struct src = 

  ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @

  ML_Lex.read_source false src @

  ML_Lex.read " end"

fun ml_type src = 

  ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option"

(* eval function *)

fun eval_fn ctxt prep exp =

  ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp)

(* checks and prints a possibly open expressions, no index *)

fun output_ml ctxt (src, (vs, stru)) =

  (eval_fn ctxt (ml_val vs stru) src; 

   output ctxt (split_lines (Input.source_content src)))

val parser_ml = Scan.lift (Args.text_input --

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

   Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))) 

(* checks and prints a single ML-item and produces an index entry *)

fun output_ml_ind ctxt (txt, stru) =

  (eval_fn ctxt (ml_val [] stru) (Input.string txt); 

   case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of

     (NONE, _, "")  => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt)

   | (NONE, bn, qn)  => output_indexed ctxt {main = Code bn,  minor = Struct qn} (split_lines txt)

   | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt))

val parser_ml_ind = Scan.lift (Args.name --

  Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))

(* checks and prints structures *)

fun gen_output_struct outfn ctxt txt = 

  (eval_fn ctxt ml_struct (Input.string txt); 

   outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))

fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt 

fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt 

(* prints functors; no checks *)

fun gen_output_funct outfn txt = 

  (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))

fun output_funct ctxt = gen_output_funct (K (output ctxt)) 

fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt)

(* checks and prints types *)

fun gen_output_type outfn ctxt txt = 

  (eval_fn ctxt ml_type (Input.string txt); 

   outfn {main = Code txt, minor = Plain "type"} (split_lines txt))

fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt

fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt 

(* checks and expression against a result pattern *)

fun output_response ctxt (lhs, pat) = 

    (eval_fn ctxt (ml_pat pat) lhs;

     (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*)

     output ctxt ((prefix_lines "" (Input.source_content lhs)) @ (prefix_lines "> " pat)))

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

fun output_response_fake ctxt (lhs, pat) = 

    (eval_fn ctxt (ml_val [] NONE) lhs;

     (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *)

     output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat)))

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

fun ouput_response_fake_both ctxt (lhs, pat) = 

    (output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat)))

val single_arg = Scan.lift (Args.name)

val two_args   = Scan.lift (Args.text_input -- Args.name)

val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))

val ml_setup = 

  Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml 

  #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind

  #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type

  #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind

  #> Thy_Output.antiquotation_raw @{binding "ML_struct"} single_arg output_struct

  #> Thy_Output.antiquotation_raw @{binding "ML_struct_ind"} single_arg output_struct_ind

  #> Thy_Output.antiquotation_raw @{binding "ML_funct"} single_arg output_funct

  #> Thy_Output.antiquotation_raw @{binding "ML_funct_ind"} single_arg output_funct_ind

  #> Thy_Output.antiquotation_raw @{binding "ML_response"} two_args output_response

  #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake

  #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both

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

fun href_link txt =

let 

  val raw = I (* FIXME: 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 "}{", get_word txt, raw "}"]

end 

fun check_file_exists _ txt =

  (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 

   then Latex.string (href_link txt)

   else error (implode ["Source file ", quote txt, " does not exist."]))

val ml_file_setup = Thy_Output.antiquotation_raw @{binding "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 (Proof.goal o Toplevel.proof_of) state of

    SOME {goal, ...} => goal

  | _ => error "No proof state");

fun output_goals ctxt _ = 

let

  fun subgoals 0 = ""

    | subgoals 1 = "goal (1 subgoal):"

    | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"

  val state = proof_state (Toplevel.presentation_state ctxt)

  val goals = Goal_Display.pretty_goal ctxt state

  val prop = Thm.prop_of state;

  val (As, _) = Logic.strip_horn prop;

  val out  = (case (length As) of

                      0 => goals 

                    | n => Pretty.big_list (subgoals n) [goals])  (* FIXME: improve printing? *)

in 

  output ctxt [Pretty.string_of out]

end

fun output_raw_goal_state  ctxt  _ = 

  let

    val goals = proof_state (Toplevel.presentation_state ctxt)

    val out  = Syntax.string_of_term ctxt (Thm.prop_of goals)

  in

    output ctxt [out]

  end

val subgoals_setup = 

  Thy_Output.antiquotation_raw @{binding "subgoals"} (Scan.succeed ()) output_goals

val raw_goal_state_setup = 

  Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state

val setup =

  ml_setup #>

  ml_file_setup #>

  subgoals_setup #>

  raw_goal_state_setup

end;