theory Base
imports Main 
        "~~/src/HOL/Library/LaTeXsugar"
uses
  ("output_tutorial.ML")
  ("antiquote_setup.ML")
begin

notation (latex output)
  Cons ("_ # _" [66,65] 65)


(* re-definition of various ML antiquotations     *)
(* to have a special tag for text enclosed in ML; *)
(* they also write the code into a separate file  *)

ML {*
val filename = Attrib.setup_config_string @{binding "filename"} (K "File_Code.ML")
*}


ML {*
fun write_file txt thy =
let 
  val stream = Config.get_global thy filename
               |> TextIO.openAppend 
in
  TextIO.output (stream, txt); 
  TextIO.flushOut stream;       (* needed ?*)
  TextIO.closeOut stream
end
*}

ML {*
fun write_file_ml_blk txt thy =
let
  val pre  = implode ["\n", "ML ", "{", "*", "\n"]
  val post = implode ["\n", "*", "}", "\n"]
  val _ = write_file (enclose pre post txt) thy
in
  thy
end

fun write_file_setup_blk txt thy =
let
  val pre  = implode ["\n", "setup ", "{", "*", "\n"]
  val post = implode ["\n", "*", "}", "\n"]
  val _ = write_file (enclose pre post txt) thy
in
  thy
end

fun write_file_lsetup_blk txt lthy =
let
  val pre  = implode ["\n", "local_setup ", "{", "*", "\n"]
  val post = implode ["\n", "*", "}", "\n"]
  val _ = write_file (enclose pre post txt) (ProofContext.theory_of lthy)
in
  lthy
end

*}

ML {*
fun open_file name thy =
let  
  val _ = tracing ("Open File: " ^ name)
  val _ = TextIO.openOut name
in 
  Config.put_global filename name thy
end
*}

ML {*
fun open_file_with_prelude name txts thy =
let 
  val thy' = open_file name thy 
  val _ = write_file (cat_lines txts) thy'
in
  thy'
end
*}

ML {*
fun propagate_env (context as Context.Proof lthy) =
      Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
  | propagate_env context = context

fun propagate_env_prf prf = Proof.map_contexts
  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
*}

ML {*
val _ =
  Outer_Syntax.command "ML" "eval ML text within theory"
    (Keyword.tag "TutorialML" Keyword.thy_decl)
    (Parse.position Parse.text >> 
      (fn (txt, pos) =>
        Toplevel.generic_theory
         (ML_Context.exec 
           (fn () => ML_Context.eval_text true pos txt) 
              #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))
*}
ML {*
val _ =
  Outer_Syntax.command "ML_prf" "ML text within proof" 
    (Keyword.tag "TutorialML" Keyword.prf_decl)
    (Parse.ML_source >> (fn (txt, pos) =>
      Toplevel.proof (Proof.map_context (Context.proof_map
        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)))
*}

ML {*
val _ =
  Outer_Syntax.command "ML_val" "diagnostic ML text" 
  (Keyword.tag "TutorialML" Keyword.diag)
    (Parse.ML_source >> Isar_Cmd.ml_diag true)
*}

ML {*
val _ =
  Outer_Syntax.command "setup" "ML theory setup" 
    (Keyword.tag_ml Keyword.thy_decl)
      (Parse.ML_source >> (fn (txt, pos) => 
        (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
*}

ML {*
val _ =
  Outer_Syntax.local_theory "local_setup" "ML local theory setup" 
    (Keyword.tag_ml Keyword.thy_decl)
      (Parse.ML_source >> (fn (txt, pos) => 
         Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
*}

ML {*
fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 

fun rhs 1 = P 1
  | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))

fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
  | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp 
                 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)

fun de_bruijn n =
  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
*}

use "output_tutorial.ML"
use "antiquote_setup.ML"

setup {* OutputTutorial.setup *}
setup {* AntiquoteSetup.setup *}

end