cakeml/semantics/primTypesScript.sml at master · ncough/cakeml · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
(*Generated by Lem from primTypes.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory libTheory astTheory namespaceTheory ffiTheory semanticPrimitivesTheory evaluateTheory;

val _ = numLib.prefer_num();


val _ = new_theory "primTypes"

(*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*)
val _ = Define `
 (prim_types_program=
 ([Tdec  (Dexn unknown_loc "Bind" []);
   Tdec  (Dexn unknown_loc "Chr" []);
   Tdec  (Dexn unknown_loc "Div" []);
   Tdec  (Dexn unknown_loc "Subscript" []);
   Tdec  (Dtype unknown_loc [([], "bool", [("false", []); ("true", [])])]);
   Tdec  (Dtype unknown_loc [(["'a"], "list", [("nil", []); ("::", [Tvar "'a"; Tapp [Tvar "'a"] (TC_name (Short "list"))]) ])]);
   Tdec (Dtype unknown_loc [(["'a"], "option", [("NONE", []);("SOME", [Tvar "'a"]) ])]) ]))`;


(*val add_to_sem_env :
  forall 'ffi. Eq 'ffi => (state 'ffi * sem_env v) -> prog -> maybe (state 'ffi * sem_env v)*)
val _ = Define `
 (add_to_sem_env (st, env) prog=
 ((case 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)*)
val _ = Define `
 (prim_sem_env ffi=
 (add_to_sem_env
    (<| clock :=(( 0 : num)); ffi := ffi; refs := ([]); defined_mods := ({}); defined_types := ({}) |>,
     <| v := nsEmpty; c := nsEmpty |>)
        prim_types_program))`;

val _ = export_theory()