Theory PrimTypes

chapter ‹Generated by Lem from ‹semantics/primTypes.lem›.›

theory "PrimTypes" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives"
  "Lib"
  "Namespace"
  "Ast"
  "SemanticPrimitives"
  "Ffi"
  "Evaluate"

begin 

― ‹‹open import Pervasives››
― ‹‹open import Ast››
― ‹‹open import SemanticPrimitives››
― ‹‹open import Ffi››
― ‹‹open import Namespace››
― ‹‹open import Lib››
― ‹‹open import Evaluate››

― ‹‹val prim_types_program : prog››
definition prim_types_program  :: "(top0)list "  where 
     " prim_types_program = (
  [Tdec  (Dexn ((| row = 0, col = 0, offset = 0 |), (| row = 0, col = 0, offset = 0 |)) (''Bind'') []),
   Tdec  (Dexn ((| row = 0, col = 0, offset = 0 |), (| row = 0, col = 0, offset = 0 |)) (''Chr'') []),
   Tdec  (Dexn ((| row = 0, col = 0, offset = 0 |), (| row = 0, col = 0, offset = 0 |)) (''Div'') []),
   Tdec  (Dexn ((| row = 0, col = 0, offset = 0 |), (| row = 0, col = 0, offset = 0 |)) (''Subscript'') []),
   Tdec  (Dtype ((| row = 0, col = 0, offset = 0 |), (| row = 0, col = 0, offset = 0 |)) [([], (''bool''), [((''false''), []), ((''true''), [])])]),
   Tdec  (Dtype ((| row = 0, col = 0, offset = 0 |), (| row = 0, col = 0, offset = 0 |)) [([([(CHR 0x27), (CHR ''a'')])], (''list''), [((''nil''), []), ((''::''), [Tvar ([(CHR 0x27), (CHR ''a'')]), Tapp [Tvar ([(CHR 0x27), (CHR ''a'')])] (TC_name (Short (''list'')))]) ])]),
   Tdec (Dtype ((| row = 0, col = 0, offset = 0 |), (| row = 0, col = 0, offset = 0 |)) [([([(CHR 0x27), (CHR ''a'')])], (''option''), [((''NONE''), []),((''SOME''), [Tvar ([(CHR 0x27), (CHR ''a'')])]) ])]) ])"


― ‹‹val add_to_sem_env :
  forall 'ffi. Eq 'ffi => (state 'ffi * sem_env v) -> prog -> maybe (state 'ffi * sem_env v)››
fun add_to_sem_env  :: " 'ffi state*(v)sem_env ⇒(top0)list ⇒('ffi state*(v)sem_env)option "  where 
     " add_to_sem_env (st, env) prog = (
  (case  fun_evaluate_prog st env prog of
    (st', Rval env') => Some (st', extend_dec_env env' env)
  | _ => None
  ))"


― ‹‹val prim_sem_env : forall 'ffi. Eq 'ffi => ffi_state 'ffi -> maybe (state 'ffi * sem_env v)››
definition prim_sem_env  :: " 'ffi ffi_state ⇒('ffi state*(v)sem_env)option "  where 
     " prim_sem_env ffi1 = (
  add_to_sem_env
    ((| clock =(( 0 :: nat)), refs = ([]), ffi = ffi1, defined_types = ({}), defined_mods = ({})  |),
     (| v = nsEmpty, c = nsEmpty |))
        prim_types_program )"

end