theory Base
imports Main LaTeXsugar
uses
  ("output_tutorial.ML")
  ("antiquote_setup.ML")
begin

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

(* rebinding of writeln and tracing so that it can *)
(* be compared in intiquotations                   *)
ML {* 
fun writeln s = (Output.writeln s; s)
fun tracing s = (Output.tracing s; s)
*}

(* 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, setup_filename) = Attrib.config_string "filename" (K "File_Code.ML")
*}

setup {* setup_filename *}

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 _ =
  OuterSyntax.command "ML" "eval ML text within theory"
    (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
    (OuterParse.position OuterParse.text >> 
      (fn (txt, pos) =>
        Toplevel.generic_theory
         (ML_Context.exec 
           (fn () => ML_Context.eval true pos txt) 
              #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))

val _ =
  OuterSyntax.command "ML_prf" "ML text within proof" 
    (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
    (OuterParse.ML_source >> (fn (txt, pos) =>
      Toplevel.proof (Proof.map_context (Context.proof_map
        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))

val _ =
  OuterSyntax.command "ML_val" "diagnostic ML text" 
  (OuterKeyword.tag "TutorialML" OuterKeyword.diag)
    (OuterParse.ML_source >> IsarCmd.ml_diag true)
*}

ML {*
val _ =
  OuterSyntax.command "setup" "ML theory setup" 
    (OuterKeyword.tag_ml OuterKeyword.thy_decl)
      (OuterParse.ML_source >> (fn (txt, pos) => 
        (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
*}

ML {* Context.proof_map *}
ML {* IsarCmd.local_setup ; Context.map_proof (write_file_lsetup_blk "") *}


ML {*
val _ =
  OuterSyntax.local_theory "local_setup" "ML local theory setup" 
    (OuterKeyword.tag_ml OuterKeyword.thy_decl)
      (OuterParse.ML_source >> (fn (txt, pos) => 
         IsarCmd.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"


end