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"

end