8 |
8 |
9 atom_decl var |
9 atom_decl var |
10 atom_decl tvar |
10 atom_decl tvar |
11 |
11 |
12 (* there are types, coercion types and regular types list-data-structure *) |
12 (* there are types, coercion types and regular types list-data-structure *) |
|
13 |
13 nominal_datatype tkind = |
14 nominal_datatype tkind = |
14 KStar |
15 KStar |
15 | KFun "tkind" "tkind" |
16 | KFun "tkind" "tkind" |
16 and ckind = |
17 and ckind = |
17 CKEq "ty" "ty" |
18 CKEq "ty" "ty" |
18 and ty = |
19 and ty = |
19 TVar "tvar" |
20 TVar "tvar" |
20 | TC "string" |
21 | TC "char" |
21 | TApp "ty" "ty" |
22 | TApp "ty" "ty" |
22 | TFun "string" "ty_lst" |
23 | TFun "char" "ty_lst" |
23 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
24 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
24 | TEq "ty" "ty" "ty" |
25 | TEq "ty" "ty" "ty" |
25 and ty_lst = |
26 and ty_lst = |
26 TsNil |
27 TsNil |
27 | TsCons "ty" "ty_lst" |
28 | TsCons "ty" "ty_lst" |
28 and co = |
29 and co = |
29 CC "string" |
30 CC "char" |
30 | CApp "co" "co" |
31 | CApp "co" "co" |
31 | CFun "string" "co_lst" |
32 | CFun "char" "co_lst" |
32 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
33 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
33 | CEq "co" "co" "co" |
34 | CEq "co" "co" "co" |
34 | CSym "co" |
35 | CSym "co" |
35 | CCir "co" "co" |
36 | CCir "co" "co" |
36 | CLeft "co" |
37 | CLeft "co" |
40 | CLeftc "co" |
41 | CLeftc "co" |
41 | CCoe "co" "co" |
42 | CCoe "co" "co" |
42 and co_lst = |
43 and co_lst = |
43 CsNil |
44 CsNil |
44 | CsCons "co" "co_lst" |
45 | CsCons "co" "co_lst" |
45 |
46 and trm = |
46 (* |
|
47 abbreviation |
|
48 "atoms A \<equiv> atom ` A" |
|
49 |
|
50 nominal_datatype trm = |
|
51 Var "var" |
47 Var "var" |
52 | C "string" |
48 | C "char" |
53 | LAM tv::"tvar" "kind" t::"trm" bind tv in t |
49 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t |
|
50 | LAMC tv::"tvar" "ckind" t::"trm" bind tv in t |
54 | APP "trm" "ty" |
51 | APP "trm" "ty" |
55 | Lam v::"var" "ty" t::"trm" bind v in t |
52 | Lam v::"var" "ty" t::"trm" bind v in t |
56 | App "trm" "trm" |
53 | App "trm" "trm" |
57 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
54 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
58 | Case "trm" "assoc list" |
55 | Case "trm" "assoc_lst" |
59 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
56 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
60 and assoc = |
57 and assoc_lst = |
61 A p::"pat" t::"trm" bind "bv p" in t |
58 ANil |
|
59 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t |
62 and pat = |
60 and pat = |
63 K "string" "(tvar \<times> kind) list" "(var \<times> ty) list" |
61 K "char" "tvtk_lst" "tvck_lst" "vt_lst" |
|
62 and tvtk_lst = |
|
63 TVTKNil |
|
64 | TVTKCons "tvar" "tkind" "tvtk_lst" |
|
65 and tvck_lst = |
|
66 TVCKNil |
|
67 | TVCKCons "tvar" "ckind" "tvck_lst" |
|
68 and vt_lst = |
|
69 VTNil |
|
70 | VTCons "var" "ty" "vt_lst" |
64 binder |
71 binder |
65 bv :: "pat \<Rightarrow> atom set" |
72 bv :: "pat \<Rightarrow> atom set" |
|
73 (*and bv_vt :: "vt_lst \<Rightarrow> atom set" |
|
74 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set" |
|
75 and bv_tvck :: "tvck_lst \<Rightarrow> atom set"*) |
66 where |
76 where |
67 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
77 "bv (K s tvts tvcs vs) = {}" (*(bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs) *) |
68 *) |
78 (*| "bv_vt VTNil = {}" |
|
79 | "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t" |
|
80 | "bv_tvtk TVTKNil = {}" |
|
81 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t" |
|
82 | "bv_tvck TVCKNil = {}" |
|
83 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*) |
69 |
84 |
70 end |
85 end |
71 |
86 |
72 |
87 |
73 |
88 |