(* 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 is_sep "\<dots>" = true
  | is_sep s = Symbol.is_ascii_blank s; 

fun scan_word sep =
  Scan.many1 sep >> K NONE ||
  Scan.many1 (fn s => not (sep s) andalso Symbol.not_eof s) >> (SOME o implode);

fun split_words sep = Symbol.scanner "Bad text" (Scan.repeat (scan_word sep) >> map_filter I);

fun explode_words sep = split_words sep o Symbol.explode;

fun match_string sep pat str =
  let
    fun match [] _ = true
      | match (p :: ps) s =
          size p <= size s andalso
            (case try (unprefix p) s of
              SOME s' => match ps s'
            | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
  in match (explode_words sep pat) str end;

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 src 
  | ml_with_struct (SOME st) src = 
      ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source 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_source pat @ 
  ML_Lex.read " = " @
  ML_Lex.read_source lhs 


fun ml_struct src = 
  ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @
  ML_Lex.read_source src @
  ML_Lex.read " end"

fun ml_type src = 
  ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source 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)

(* Evalate expression and convert result to a string *)
fun eval_response ctxt exp =
let 
  fun compute exp = 
     let 
       val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source exp @ 
                   ML_Lex.read " in (raise ERROR (@{make_string} r); ()) end )"
       val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) input 
     in ""
     end 
in
  (compute exp 
   handle ERROR s => s)
end

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

fun output_ml_response ignore_pat ctxt (src, opat) =
let 
  val res = eval_response ctxt src
  val _ = writeln res
  val cnt = YXML.content_of res
  val pat = case opat of NONE => cnt 
            | SOME p => p |>  fst o Input.source_content 
  val _ = if ignore_pat orelse Print_Mode.print_mode_active Latex.latexN orelse match_string is_sep pat cnt then () 
          else error (cat_lines ["Substring:", pat, "not contained in:", cnt])
  val out = if ignore_pat then cnt else pat
in 
  OutputTutorial.output ctxt ([fst (Input.source_content src)] @ [Library.prefix_lines "> " out])
end

(* checks and prints a single ML-item and produces an index entry *)
fun output_ml_ind ctxt (src, stru) =
let 
  val (txt,_) = Input.source_content src
in
  (eval_fn ctxt (ml_val [] stru) src; 
   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))
end

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

(* checks and prints structures *)
fun gen_output_struct outfn ctxt src = 
let 
  val (txt, _) = Input.source_content src
in
  (eval_fn ctxt ml_struct src; 
   outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
end

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 src = 
let
  val (txt, _) = Input.source_content src
in
  (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
end

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 src = 
let 
  val (txt, _) = Input.source_content src
in
  (eval_fn ctxt ml_type src; 
   outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
end

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

val dots_pat = translate_string (fn "_" => "\<dots>"  | s => s) 

(* checks and expression against a result pattern *)
fun output_response ctxt (lhs, pat) = 
    (eval_fn ctxt (ml_pat pat) lhs;
     output ctxt ((prefix_lines "" (fst (Input.source_content lhs))) @ 
       (prefix_lines "> " (dots_pat (fst (Input.source_content 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;
     output ctxt ( (split_lines (fst (Input.source_content lhs))) @ 
        (prefix_lines "> " (dots_pat (fst (Input.source_content 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 (fst (Input.source_content lhs))) @ 
     (prefix_lines "> " (dots_pat (fst ((Input.source_content pat)))))))

val single_arg = Scan.lift (Args.text_input)
val two_args   = Scan.lift (Args.text_input -- Args.text_input)
val maybe_two_args = Scan.lift (Args.text_input -- Scan.option Args.text_input)
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_response"} maybe_two_args (output_ml_response false)
  #> Thy_Output.antiquotation_raw @{binding "ML_response_ignore"} maybe_two_args (output_ml_response true)
  #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind
  #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind
  #> Thy_Output.antiquotation_raw @{binding "ML_structure_ind"} single_arg output_struct_ind
  #> Thy_Output.antiquotation_raw @{binding "ML_functor_ind"} single_arg output_funct_ind
  #> Thy_Output.antiquotation_raw @{binding "ML_matchresult"} two_args output_response
  #> Thy_Output.antiquotation_raw @{binding "ML_matchresult_fake"} two_args output_response_fake
  #> Thy_Output.antiquotation_raw @{binding "ML_matchresult_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 _ src =
let
  val (txt, _) = Input.source_content src
in
  (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."]))
end

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_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 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 #>
  raw_goal_state_setup
end;