Theory SimpleIO

chapter ‹Generated by Lem from ‹semantics/ffi/simpleIO.lem›.›

theory "SimpleIO" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives"
  "LEM.Lem_pervasives_extra"
  "Lib"
  "Ffi"

begin 

― ‹‹open import Pervasives››
― ‹‹open import Pervasives_extra››
― ‹‹open import Lib››
― ‹‹open import Ffi››

datatype_record simpleIO = 
 input ::"  8 word llist " 
 output0 ::"  8 word llist " 


― ‹‹val isEof : oracle_function simpleIO››
fun isEof  :: " simpleIO ⇒(8 word)list ⇒(8 word)list ⇒(simpleIO)oracle_result "  where 
     " isEof st conf ([]) = ( Oracle_fail )"
|" isEof st conf (x # xs) = ( Oracle_return st ((if(input   st) = LNil then of_nat (( 1 :: nat)) else of_nat (( 0 :: nat)))# xs))"


― ‹‹val getChar : oracle_function simpleIO››
fun getChar  :: " simpleIO ⇒(8 word)list ⇒(8 word)list ⇒(simpleIO)oracle_result "  where 
     " getChar st conf ([]) = ( Oracle_fail )"
|" getChar st conf (x # xs) = (
      (case  lhd'(input   st) of
        Some y => Oracle_return (( st (| input := (Option.the (ltl'(input   st))) |))) (y # xs)
      | _ => Oracle_fail
      ))"


― ‹‹val putChar : oracle_function simpleIO››
definition putChar  :: " simpleIO ⇒(8 word)list ⇒(8 word)list ⇒(simpleIO)oracle_result "  where 
     " putChar st conf input1 = (
  (case  input1 of
    [] => Oracle_fail
  | x # _ => Oracle_return (( st (| output0 := (LCons x(output0   st)) |))) input1
  ))"


― ‹‹val exit : oracle_function simpleIO››
definition exit0  :: " simpleIO ⇒(8 word)list ⇒(8 word)list ⇒(simpleIO)oracle_result "  where 
     " exit0 st conf input1 = ( Oracle_diverge )"


― ‹‹val simpleIO_oracle : oracle simpleIO››
definition simpleIO_oracle  :: " string ⇒ simpleIO ⇒(8 word)list ⇒(8 word)list ⇒(simpleIO)oracle_result "  where 
     " simpleIO_oracle s st conf input1 = (
  if s = (''isEof'') then
    isEof st conf input1
  else if s = (''getChar'') then
    getChar st conf input1
  else if s = (''putChar'') then
    putChar st conf input1
  else if s = (''exit'') then
    exit0 st conf input1
  else
    Oracle_fail )"

end