7 Values = Language + Map + |
7 Values = Language + Map + |
8 |
8 |
9 (* Values, values environments and associated operators *) |
9 (* Values, values environments and associated operators *) |
10 |
10 |
11 consts |
11 consts |
12 Val, ValEnv, Val_ValEnv :: "i" |
12 Val, ValEnv, Val_ValEnv :: i |
13 codatatype <= "quniv(Const Un ExVar Un Exp)" |
13 codatatype <= "quniv(Const Un ExVar Un Exp)" |
14 "Val" = v_const("c:Const") |
14 "Val" = v_const("c:Const") |
15 | v_clos("x:ExVar","e:Exp","ve:ValEnv") |
15 | v_clos("x:ExVar","e:Exp","ve:ValEnv") |
16 and |
16 and |
17 "ValEnv" = ve_mk("m:PMap(ExVar,Val)") |
17 "ValEnv" = ve_mk("m:PMap(ExVar,Val)") |
18 monos "[map_mono]" |
18 monos "[map_mono]" |
19 type_intrs "[A_into_univ, mapQU]" |
19 type_intrs "[A_into_univ, mapQU]" |
20 |
20 |
21 consts |
21 consts |
22 ve_emp :: "i" |
22 ve_emp :: i |
23 ve_owr :: "[i,i,i] => i" |
23 ve_owr :: [i,i,i] => i |
24 ve_dom :: "i=>i" |
24 ve_dom :: i=>i |
25 ve_app :: "[i,i] => i" |
25 ve_app :: [i,i] => i |
26 defs |
26 defs |
27 ve_emp_def "ve_emp == ve_mk(map_emp)" |
27 ve_emp_def "ve_emp == ve_mk(map_emp)" |
28 ve_owr_def |
28 ve_owr_def |
29 "ve_owr(ve,x,v) == |
29 "ve_owr(ve,x,v) == |
30 ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))" |
30 ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))" |