primTypes.lem

(*
  Definition of the primitive types that are in scope before any CakeML program
  starts. Some of them are generated by running an initial program.
*)
open import Pervasives
open import Ast
open import SemanticPrimitives
open import Ffi
open import Namespace
open import Lib
open import Evaluate

(* The ordering in the following is important. The stamps generated from the
   exceptions and types must match those in semanticPrimitives *)
val prim_types_program : list dec
let prim_types_program =
  [Dexn unknown_loc "Bind" [];
   Dexn unknown_loc "Chr" [];
   Dexn unknown_loc "Div" [];
   Dexn unknown_loc "Subscript" [];
   Dtype unknown_loc [([], "bool", [("false", []); ("true", [])])];
   Dtype unknown_loc [(["'a"], "list", [("nil", []); ("::", [Atvar "'a"; Atapp [Atvar "'a"] (Short "list")]);])];]

val add_to_sem_env :
  forall 'ffi. Eq 'ffi => (state 'ffi * sem_env v) -> list dec -> maybe (state 'ffi * sem_env v)
let add_to_sem_env (st, env) prog =
  match evaluate_decs st env prog with
  | (st', Rval env') -> Just (st', extend_dec_env env' env)
  | _ -> Nothing
  end

val prim_sem_env : forall 'ffi. Eq 'ffi => ffi_state 'ffi -> maybe (state 'ffi * sem_env v)
let prim_sem_env ffi =
  add_to_sem_env
    (<| clock = 0; ffi = ffi; refs = []; next_type_stamp = 0; next_exn_stamp = 0 |>,
     <| v = nsEmpty; c = nsEmpty |>)
        prim_types_program

open import TypeSystem

let prim_tenv =
    <| c = alist_to_ns (List.reverse
          [("Bind", ([],[],Texn_num));
           ("Chr", ([],[],Texn_num));
           ("Div", ([],[],Texn_num));
           ("Subscript", ([],[],Texn_num));
           ("false", ([],[], Tbool_num));
           ("true", ([],[], Tbool_num));
           ("nil", (["'a"],[],Tlist_num));
           ("::", (["'a"],[Tvar "'a"; Tlist (Tvar "'a")], Tlist_num))]);
       v = nsEmpty;
       t = alist_to_ns (List.reverse
          [
          ("array",(["'a"],Tapp [Tvar "'a"] Tarray_num));
          ("bool",([],Tapp [] Tbool_num));
          ("char",([],Tapp [] Tchar_num));
          ("exn",([],Tapp [] Texn_num));
          (* Tfn is ->, specially handled *)
          ("int",([],Tapp [] Tint_num));
          ("list",(["'a"],Tapp [Tvar "'a"] Tlist_num));
          ("ref",(["'a"],Tapp [Tvar "'a"] Tref_num));
          ("string",([],Tapp [] Tstring_num));
          ("unit",([],Tapp [] Ttup_num));
          (* pairs are specially handled *)
          ("vector",(["'a"],Tapp [Tvar "'a"] Tvector_num));
          ("word64",([],Tapp [] Tword64_num));
          ("word8",([],Tapp [] Tword8_num));
          ("word8array",([],Tapp [] Tword8array_num))]
          )|>

let prim_type_ids = Set.fromList (Tlist_num :: Tbool_num :: prim_type_nums)