Theory Printer_init
section‹Initializing the Printer›
theory Printer_init
imports "../Init"
"../isabelle_home/src/HOL/Isabelle_Main1"
begin
text‹At the time of writing, the following target languages supported
by Isabelle are also supported by the meta-compiler:
Haskell, OCaml, Scala, SML.›
subsection‹Kernel Code for Target Languages›
lazy_code_printing code_module "CodeType" ⇀ (Haskell) ‹
module CodeType where {
type MlInt = Integer
; type MlMonad a = IO a
}› | code_module "CodeConst" ⇀ (Haskell) ‹
module CodeConst where {
import System.Directory
; import System.IO
; import qualified CodeConst.Printf
; outFile1 f file = (do
fileExists <- doesFileExist file
if fileExists then error ("File exists " ++ file ++ "\n") else do
h <- openFile file WriteMode
f (\pat -> hPutStr h . CodeConst.Printf.sprintf1 pat)
hClose h)
; outStand1 :: ((String -> String -> IO ()) -> IO ()) -> IO ()
; outStand1 f = f (\pat -> putStr . CodeConst.Printf.sprintf1 pat)
}› | code_module "CodeConst.Monad" ⇀ (Haskell) ‹
module CodeConst.Monad where {
bind a = (>>=) a
; return :: a -> IO a
; return = Prelude.return
}› | code_module "CodeConst.Printf" ⇀ (Haskell) ‹
module CodeConst.Printf where {
import Text.Printf
; sprintf0 = id
; sprintf1 :: PrintfArg a => String -> a -> String
; sprintf1 = printf
; sprintf2 :: PrintfArg a => PrintfArg b => String -> a -> b -> String
; sprintf2 = printf
; sprintf3 :: PrintfArg a => PrintfArg b => PrintfArg c => String -> a -> b -> c -> String
; sprintf3 = printf
; sprintf4 :: PrintfArg a => PrintfArg b => PrintfArg c => PrintfArg d => String -> a -> b -> c -> d -> String
; sprintf4 = printf
; sprintf5 :: PrintfArg a => PrintfArg b => PrintfArg c => PrintfArg d => PrintfArg e => String -> a -> b -> c -> d -> e -> String
; sprintf5 = printf
}› | code_module "CodeConst.String" ⇀ (Haskell) ‹
module CodeConst.String where {
concat s [] = []
; concat s (x : xs) = x ++ concatMap ((++) s) xs
}› | code_module "CodeConst.Sys" ⇀ (Haskell) ‹
module CodeConst.Sys where {
import System.Directory
; isDirectory2 = doesDirectoryExist
}› | code_module "CodeConst.To" ⇀ (Haskell) ‹
module CodeConst.To where {
nat = id
}› | code_module "" ⇀ (OCaml) ‹
module CodeType = struct
type mlInt = int
type 'a mlMonad = 'a option
end
module CodeConst = struct
let outFile1 f file =
try
let () = if Sys.file_exists file then Printf.eprintf "File exists \"%S\"\n" file else () in
let oc = open_out file in
let b = f (fun s a -> try Some (Printf.fprintf oc s a) with _ -> None) in
let () = close_out oc in
b
with _ -> None
let outStand1 f =
f (fun s a -> try Some (Printf.fprintf stdout s a) with _ -> None)
module Monad = struct
let bind = function
None -> fun _ -> None
| Some a -> fun f -> f a
let return a = Some a
end
module Printf = struct
include Printf
let sprintf0 = sprintf
let sprintf1 = sprintf
let sprintf2 = sprintf
let sprintf3 = sprintf
let sprintf4 = sprintf
let sprintf5 = sprintf
end
module String = String
module Sys = struct open Sys
let isDirectory2 s = try Some (is_directory s) with _ -> None
end
module To = struct
let nat big_int x = Big_int.int_of_big_int (big_int x)
end
end
› | code_module "" ⇀ (Scala) ‹
object CodeType {
type mlMonad [A] = Option [A]
type mlInt = Int
}
object CodeConst {
def outFile1 [A] (f : (String => A => Option [Unit]) => Option [Unit], file0 : String) : Option [Unit] = {
val file = new java.io.File (file0)
if (file .isFile) {
None
} else {
val writer = new java.io.PrintWriter (file)
f ((fmt : String) => (s : A) => Some (writer .write (fmt .format (s))))
Some (writer .close ())
}
}
def outStand1 [A] (f : (String => A => Option [Unit]) => Option [Unit]) : Option[Unit] = {
f ((fmt : String) => (s : A) => Some (print (fmt .format (s))))
}
object Monad {
def bind [A, B] (x : Option [A], f : A => Option [B]) : Option [B] = x match {
case None => None
case Some (a) => f (a)
}
def Return [A] (a : A) = Some (a)
}
object Printf {
def sprintf0 (x0 : String) = x0
def sprintf1 [A1] (fmt : String, x1 : A1) = fmt .format (x1)
def sprintf2 [A1, A2] (fmt : String, x1 : A1, x2 : A2) = fmt .format (x1, x2)
def sprintf3 [A1, A2, A3] (fmt : String, x1 : A1, x2 : A2, x3 : A3) = fmt .format (x1, x2, x3)
def sprintf4 [A1, A2, A3, A4] (fmt : String, x1 : A1, x2 : A2, x3 : A3, x4 : A4) = fmt .format (x1, x2, x3, x4)
def sprintf5 [A1, A2, A3, A4, A5] (fmt : String, x1 : A1, x2 : A2, x3 : A3, x4 : A4, x5 : A5) = fmt .format (x1, x2, x3, x4, x5)
}
object String {
def concat (s : String, l : List [String]) = l filter (_ .nonEmpty) mkString s
}
object Sys {
def isDirectory2 (s : String) = Some (new java.io.File (s) .isDirectory)
}
object To {
def nat [A] (f : A => BigInt, x : A) = f (x) .intValue ()
}
}
› | code_module "" ⇀ (SML) ‹
structure CodeType = struct
type mlInt = string
type 'a mlMonad = 'a option
end
structure CodeConst = struct
structure Monad = struct
val bind = fn
NONE => (fn _ => NONE)
| SOME a => fn f => f a
val return = SOME
end
structure Printf = struct
local
fun sprintf s l =
case String.fields (fn #"%" => true | _ => false) s of
[] => ""
| [x] => x
| x :: xs =>
let fun aux acc l_pat l_s =
case l_pat of
[] => rev acc
| x :: xs => aux (String.extract (x, 1, NONE) :: hd l_s :: acc) xs (tl l_s) in
String.concat (x :: aux [] xs l)
end
in
fun sprintf0 s_pat = s_pat
fun sprintf1 s_pat s1 = sprintf s_pat [s1]
fun sprintf2 s_pat s1 s2 = sprintf s_pat [s1, s2]
fun sprintf3 s_pat s1 s2 s3 = sprintf s_pat [s1, s2, s3]
fun sprintf4 s_pat s1 s2 s3 s4 = sprintf s_pat [s1, s2, s3, s4]
fun sprintf5 s_pat s1 s2 s3 s4 s5 = sprintf s_pat [s1, s2, s3, s4, s5]
end
end
structure String = struct
val concat = String.concatWith
end
structure Sys = struct
val isDirectory2 = SOME o File.is_dir o Path.explode handle ERROR _ => K NONE
end
structure To = struct
fun nat f = Int.toString o f
end
fun outFile1 f file =
let
val pfile = Path.explode file
val () = if File.exists pfile then error ("File exists \"" ^ file ^ "\"\n") else ()
val oc = Unsynchronized.ref []
val _ = f (fn a => fn b => SOME (oc := Printf.sprintf1 a b :: (Unsynchronized.! oc))) in
SOME (File.write_list pfile (rev (Unsynchronized.! oc))) handle _ => NONE
end
fun outStand1 f = outFile1 f (Unsynchronized.! stdout_file)
end
›
subsection‹Interface with Types›
datatype ml_int = ML_int
code_printing type_constructor ml_int ⇀ (Haskell) "CodeType.MlInt"
| type_constructor ml_int ⇀ (OCaml) "CodeType.mlInt"
| type_constructor ml_int ⇀ (Scala) "CodeType.mlInt"
| type_constructor ml_int ⇀ (SML) "CodeType.mlInt"