theory Base

imports Main 

        "~~/src/HOL/Library/LaTeXsugar"

keywords "ML" "setup" "local_setup" :: thy_decl and

         "ML_prf" :: prf_decl and

         "ML_val" :: diag

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) (Proof_Context.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 {*

*}

ML {*

val _ =

*}

ML {*

val _ =

  Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" 

    (Parse.ML_source >> Isar_Cmd.ml_diag true)

*}

ML {*

val _ =

  Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup" 

      (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", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup" 

      (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