Theory Printer_init

(******************************************************************************
 * Citadelle
 *
 * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2017 IRT SystemX, France
 *               2011-2015 Achim D. Brucker, Germany
 *               2016-2018 The University of Sheffield, UK
 *               2016-2017 Nanyang Technological University, Singapore
 *               2017-2018 Virginia Tech, USA
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

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›

  (* We put in 'CodeConst' functions using characters
     not allowed in a Isabelle 'code_const' expr
     (e.g. '_', '"', ...) *)

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)
    file .isFile match {
      case true => None
      case false =>
        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
      try (fn () => File.write_list pfile (rev (Unsynchronized.! oc))) ()
    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" ― ‹syntax!›
            | type_constructor ml_int  (OCaml) "CodeType.mlInt"
            | type_constructor ml_int  (Scala) "CodeType.mlInt"
            | type_constructor ml_int  (SML) "CodeType.mlInt"

datatype 'a ml_monad = ML_monad 'a
code_printing type_constructor ml_monad  (Haskell) "CodeType.MlMonad _" ― ‹syntax!›
            | type_constructor ml_monad  (OCaml) "_ CodeType.mlMonad"
            | type_constructor ml_monad  (Scala) "CodeType.mlMonad [_]"
            | type_constructor ml_monad  (SML) "_ CodeType.mlMonad"

type_synonym ml_string = String.literal

subsection‹Interface with Constants›

text‹module CodeConst›

consts out_file1 :: "((ml_string  'α1  unit ml_monad) ― ‹fprintf›  unit ml_monad)  ml_string  unit ml_monad"
code_printing constant out_file1  (Haskell) "CodeConst.outFile1"
            | constant out_file1  (OCaml) "CodeConst.outFile1"
            | constant out_file1  (Scala) "CodeConst.outFile1"
            | constant out_file1  (SML) "CodeConst.outFile1"

consts out_stand1 :: "((ml_string  'α1  unit ml_monad) ― ‹fprintf›  unit ml_monad)  unit ml_monad"
code_printing constant out_stand1  (Haskell) "CodeConst.outStand1"
            | constant out_stand1  (OCaml) "CodeConst.outStand1"
            | constant out_stand1  (Scala) "CodeConst.outStand1"
            | constant out_stand1  (SML) "CodeConst.outStand1"

text‹module Monad›

consts bind :: "'a ml_monad  ('a  'b ml_monad)  'b ml_monad"
code_printing constant bind  (Haskell) "CodeConst.Monad.bind"
            | constant bind  (OCaml) "CodeConst.Monad.bind"
            | constant bind  (Scala) "CodeConst.Monad.bind"
            | constant bind  (SML) "CodeConst.Monad.bind"

consts return :: "'a  'a ml_monad"
code_printing constant return  (Haskell) "CodeConst.Monad.return"
            | constant return  (OCaml) "CodeConst.Monad.return"
            | constant return  (Scala) "CodeConst.Monad.Return" ― ‹syntax!›
            | constant return  (SML) "CodeConst.Monad.return"

text‹module Printf›

consts sprintf0 :: "ml_string  ml_string"
code_printing constant sprintf0  (Haskell) "CodeConst.Printf.sprintf0"
            | constant sprintf0  (OCaml) "CodeConst.Printf.sprintf0"
            | constant sprintf0  (Scala) "CodeConst.Printf.sprintf0"
            | constant sprintf0  (SML) "CodeConst.Printf.sprintf0"

consts sprintf1 :: "ml_string  'α1  ml_string"
code_printing constant sprintf1  (Haskell) "CodeConst.Printf.sprintf1"
            | constant sprintf1  (OCaml) "CodeConst.Printf.sprintf1"
            | constant sprintf1  (Scala) "CodeConst.Printf.sprintf1"
            | constant sprintf1  (SML) "CodeConst.Printf.sprintf1"

consts sprintf2 :: "ml_string  'α1  'α2  ml_string"
code_printing constant sprintf2  (Haskell) "CodeConst.Printf.sprintf2"
            | constant sprintf2  (OCaml) "CodeConst.Printf.sprintf2"
            | constant sprintf2  (Scala) "CodeConst.Printf.sprintf2"
            | constant sprintf2  (SML) "CodeConst.Printf.sprintf2"

consts sprintf3 :: "ml_string  'α1  'α2  'α3  ml_string"
code_printing constant sprintf3  (Haskell) "CodeConst.Printf.sprintf3"
            | constant sprintf3  (OCaml) "CodeConst.Printf.sprintf3"
            | constant sprintf3  (Scala) "CodeConst.Printf.sprintf3"
            | constant sprintf3  (SML) "CodeConst.Printf.sprintf3"

consts sprintf4 :: "ml_string  'α1  'α2  'α3  'α4  ml_string"
code_printing constant sprintf4  (Haskell) "CodeConst.Printf.sprintf4"
            | constant sprintf4  (OCaml) "CodeConst.Printf.sprintf4"
            | constant sprintf4  (Scala) "CodeConst.Printf.sprintf4"
            | constant sprintf4  (SML) "CodeConst.Printf.sprintf4"

consts sprintf5 :: "ml_string  'α1  'α2  'α3  'α4  'α5  ml_string"
code_printing constant sprintf5  (Haskell) "CodeConst.Printf.sprintf5"
            | constant sprintf5  (OCaml) "CodeConst.Printf.sprintf5"
            | constant sprintf5  (Scala) "CodeConst.Printf.sprintf5"
            | constant sprintf5  (SML) "CodeConst.Printf.sprintf5"

text‹module String›

consts String_concat :: "ml_string  ml_string list  ml_string"
code_printing constant String_concat  (Haskell) "CodeConst.String.concat"
            | constant String_concat  (OCaml) "CodeConst.String.concat"
            | constant String_concat  (Scala) "CodeConst.String.concat"
            | constant String_concat  (SML) "CodeConst.String.concat"

text‹module Sys›

consts Sys_is_directory2 :: "ml_string  bool ml_monad"
code_printing constant Sys_is_directory2  (Haskell) "CodeConst.Sys.isDirectory2"
            | constant Sys_is_directory2  (OCaml) "CodeConst.Sys.isDirectory2"
            | constant Sys_is_directory2  (Scala) "CodeConst.Sys.isDirectory2"
            | constant Sys_is_directory2  (SML) "CodeConst.Sys.isDirectory2"

text‹module To›

consts ToNat :: "(nat  integer)  nat  ml_int"
code_printing constant ToNat  (Haskell) "CodeConst.To.nat"
            | constant ToNat  (OCaml) "CodeConst.To.nat"
            | constant ToNat  (Scala) "CodeConst.To.nat"
            | constant ToNat  (SML) "CodeConst.To.nat"

subsection‹Some Notations (I): Raw Translations›

syntax "_sprint0" :: "_  ml_string" ("sprint0 (_)´")
translations "sprint0 x´"  "CONST sprintf0 x"

syntax "_sprint1" :: "_  _  ml_string" ("sprint1 (_)´")
translations "sprint1 x´"  "CONST sprintf1 x"

syntax "_sprint2" :: "_  _  ml_string" ("sprint2 (_)´")
translations "sprint2 x´"  "CONST sprintf2 x"

syntax "_sprint3" :: "_  _  ml_string" ("sprint3 (_)´")
translations "sprint3 x´"  "CONST sprintf3 x"

syntax "_sprint4" :: "_  _  ml_string" ("sprint4 (_)´")
translations "sprint4 x´"  "CONST sprintf4 x"

syntax "_sprint5" :: "_  _  ml_string" ("sprint5 (_)´")
translations "sprint5 x´"  "CONST sprintf5 x"

subsection‹Some Notations (II): Polymorphic Cartouches›

syntax "_cartouche_string'" :: String.literal
translations "_cartouche_string"  "_cartouche_string'"

parse_translation [( @{syntax_const "_cartouche_string'"}
   , parse_translation_cartouche
       @{binding cartouche_type'}
       (( "funprintf"
        , ( Cartouche_Grammar.nil1
          , Cartouche_Grammar.cons1
          , let fun f c x = Syntax.const c $ x in
            fn (0, x) => x
             | (1, x) => f @{const_syntax sprintf1} x
             | (2, x) => f @{const_syntax sprintf2} x
             | (3, x) => f @{const_syntax sprintf3} x
             | (4, x) => f @{const_syntax sprintf4} x
             | (5, x) => f @{const_syntax sprintf5} x
            end))
        :: Cartouche_Grammar.default)
       (fn 37 ― ‹‹#"%"› => (fn x => x + 1)
         | _ => I)
       0)]

subsection‹Generic Locale for Printing›

locale Print =
  fixes To_string :: "string  ml_string"
  fixes To_nat :: "nat  ml_int"
begin
  declare[[cartouche_type' = "funprintf"]]
end

text‹As remark, printing functions (like @{term sprintf5}...) are currently 
weakly typed in Isabelle, we will continue the typing using the type system of target languages.›

end