|
1601
|
1 |
theory ExCoreHaskell
|
|
|
2 |
imports "Parser"
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
(* core haskell *)
|
|
|
6 |
|
|
|
7 |
ML {* val _ = recursive := false *}
|
|
|
8 |
|
|
|
9 |
atom_decl var
|
|
|
10 |
atom_decl tvar
|
|
|
11 |
|
|
|
12 |
(* there are types, coercion types and regular types *)
|
|
|
13 |
(* list-data-structure
|
|
|
14 |
nominal_datatype tkind =
|
|
|
15 |
KStar
|
|
|
16 |
| KFun "tkind" "tkind"
|
|
|
17 |
and ckind =
|
|
|
18 |
CKEq "ty" "ty"
|
|
|
19 |
and ty =
|
|
|
20 |
TVar "tvar"
|
|
|
21 |
| TC "string"
|
|
|
22 |
| TApp "ty" "ty"
|
|
|
23 |
| TFun "string" "ty list"
|
|
|
24 |
| TAll tv::"tvar" "tkind" T::"ty" bind tv in T
|
|
|
25 |
| TEq "ty" "ty" "ty"
|
|
|
26 |
and co =
|
|
|
27 |
CC "string"
|
|
|
28 |
| CApp "co" "co"
|
|
|
29 |
| CFun "string" "co list"
|
|
|
30 |
| CAll tv::"tvar" "ckind" C::"co" bind tv in C
|
|
|
31 |
| CEq "co" "co" "co"
|
|
|
32 |
| CSym "co"
|
|
|
33 |
| CCir "co" "co"
|
|
|
34 |
| CLeft "co"
|
|
|
35 |
| CRight "co"
|
|
|
36 |
| CSim "co"
|
|
|
37 |
| CRightc "co"
|
|
|
38 |
| CLeftc "co"
|
|
|
39 |
| CCoe "co" "co"
|
|
|
40 |
|
|
|
41 |
abbreviation
|
|
|
42 |
"atoms A \<equiv> atom ` A"
|
|
|
43 |
|
|
|
44 |
nominal_datatype trm =
|
|
|
45 |
Var "var"
|
|
|
46 |
| C "string"
|
|
|
47 |
| LAM tv::"tvar" "kind" t::"trm" bind tv in t
|
|
|
48 |
| APP "trm" "ty"
|
|
|
49 |
| Lam v::"var" "ty" t::"trm" bind v in t
|
|
|
50 |
| App "trm" "trm"
|
|
|
51 |
| Let x::"var" "ty" "trm" t::"trm" bind x in t
|
|
|
52 |
| Case "trm" "assoc list"
|
|
|
53 |
| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
|
|
|
54 |
and assoc =
|
|
|
55 |
A p::"pat" t::"trm" bind "bv p" in t
|
|
|
56 |
and pat =
|
|
|
57 |
K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
|
|
|
58 |
binder
|
|
|
59 |
bv :: "pat \<Rightarrow> atom set"
|
|
|
60 |
where
|
|
|
61 |
"bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
|
|
|
62 |
*)
|
|
|
63 |
|
|
|
64 |
end
|
|
|
65 |
|
|
|
66 |
|
|
|
67 |
|