equal
deleted
inserted
replaced
5 (* core haskell *) |
5 (* core haskell *) |
6 |
6 |
7 ML {* val _ = recursive := false *} |
7 ML {* val _ = recursive := false *} |
8 |
8 |
9 atom_decl var |
9 atom_decl var |
|
10 atom_decl cvar |
10 atom_decl tvar |
11 atom_decl tvar |
11 |
12 |
12 (* there are types, coercion types and regular types list-data-structure *) |
13 (* there are types, coercion types and regular types list-data-structure *) |
13 |
14 |
14 ML {* val _ = alpha_type := AlphaLst *} |
15 ML {* val _ = alpha_type := AlphaLst *} |
21 TVar "tvar" |
22 TVar "tvar" |
22 | TC "string" |
23 | TC "string" |
23 | TApp "ty" "ty" |
24 | TApp "ty" "ty" |
24 | TFun "string" "ty_lst" |
25 | TFun "string" "ty_lst" |
25 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
26 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
26 | TEq "ty" "ty" "ty" |
27 | TEq "ckind" "ty" |
27 and ty_lst = |
28 and ty_lst = |
28 TsNil |
29 TsNil |
29 | TsCons "ty" "ty_lst" |
30 | TsCons "ty" "ty_lst" |
30 and co = |
31 and co = |
31 CC "string" |
32 CC cvar |
|
33 | CConst "string" |
32 | CApp "co" "co" |
34 | CApp "co" "co" |
33 | CFun "string" "co_lst" |
35 | CFun "string" "co_lst" |
34 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
36 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
35 | CEq "co" "co" "co" |
37 | CEq "ckind" "co" |
|
38 | CRefl "ty" |
36 | CSym "co" |
39 | CSym "co" |
37 | CCir "co" "co" |
40 | CCir "co" "co" |
38 (* At ??? *) |
41 | CAt "co" "ty" |
39 | CLeft "co" |
42 | CLeft "co" |
40 | CRight "co" |
43 | CRight "co" |
41 | CSim "co" |
44 | CSim "co" "co" |
42 | CRightc "co" |
45 | CRightc "co" |
43 | CLeftc "co" |
46 | CLeftc "co" |
44 | CCoe "co" "co" |
47 | CCoe "co" "co" |
45 and co_lst = |
48 and co_lst = |
46 CsNil |
49 CsNil |
47 | CsCons "co" "co_lst" |
50 | CsCons "co" "co_lst" |
48 and trm = |
51 and trm = |
49 Var "var" |
52 Var "var" |
50 | C "string" |
53 | C "string" |
51 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t |
54 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t |
52 | LAMC tv::"tvar" "ckind" t::"trm" bind tv in t |
55 | LAMC cv::"cvar" "ckind" t::"trm" bind cv in t |
53 | APP "trm" "ty" |
56 | AppT "trm" "ty" |
|
57 | AppC "trm" "co" |
54 | Lam v::"var" "ty" t::"trm" bind v in t |
58 | Lam v::"var" "ty" t::"trm" bind v in t |
55 | App "trm" "trm" |
59 | App "trm" "trm" |
56 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
60 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
57 | Case "trm" "assoc_lst" |
61 | Case "trm" "assoc_lst" |
58 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
62 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
67 and tvtk_lst = |
71 and tvtk_lst = |
68 TVTKNil |
72 TVTKNil |
69 | TVTKCons "tvar" "tkind" "tvtk_lst" |
73 | TVTKCons "tvar" "tkind" "tvtk_lst" |
70 and tvck_lst = |
74 and tvck_lst = |
71 TVCKNil |
75 TVCKNil |
72 | TVCKCons "tvar" "ckind" "tvck_lst" |
76 | TVCKCons "cvar" "ckind" "tvck_lst" |
73 binder |
77 binder |
74 bv :: "pat \<Rightarrow> atom list" |
78 bv :: "pat \<Rightarrow> atom list" |
75 and bv_vt :: "vt_lst \<Rightarrow> atom list" |
79 and bv_vt :: "vt_lst \<Rightarrow> atom list" |
76 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom list" |
80 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom list" |
77 and bv_tvck :: "tvck_lst \<Rightarrow> atom list" |
81 and bv_tvck :: "tvck_lst \<Rightarrow> atom list" |