-
Notifications
You must be signed in to change notification settings - Fork 0
/
utils.ml
177 lines (159 loc) · 6.27 KB
/
utils.ml
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
type identifier = string
open Format
exception SyntaxError of string
type judgement =
| JValue
| JComp
let pp_judgement fmt = function
| JValue -> pp_print_string fmt "val"
| JComp -> pp_print_string fmt "comput"
type ttype =
| TUnit
| TArrow of ttype * ttype
| TComp of ttype
| TSum of ttype * ttype
| TProduct of ttype * ttype
| TRecursive of identifier * ttype
| TVar of identifier
| TMacro of identifier * ttype list
let rec pp_ttype fmt = function
| TUnit -> pp_print_string fmt "1"
| TArrow (t1, t2) -> fprintf fmt "(%a -> %a)" pp_ttype t1 pp_ttype t2
| TComp t -> fprintf fmt "lazy(%a)" pp_ttype t
| TSum (t1, t2) -> fprintf fmt "(%a + %a)" pp_ttype t1 pp_ttype t2
| TProduct (t1, t2) -> fprintf fmt "(%a x %a)" pp_ttype t1 pp_ttype t2
| TRecursive (id, t) -> fprintf fmt "rec(%s, %a)" id pp_ttype t
| TVar s -> pp_print_string fmt s
| TMacro (m, tl) ->
let pp_sep fmt () = Format.fprintf fmt ",@ " in
fprintf fmt "%s(%a)" m (pp_print_list ~pp_sep pp_ttype) tl
type metatype = ttype * judgement
let pp_metatype fmt (a, b) = fprintf fmt "%a %a" pp_judgement b pp_ttype a
type term =
| Unit
| Variable of identifier
| Computation of term
| Abstraction of ttype * identifier * term
| Return of term
| Bind of term * identifier * term
| Application of term * term
| Force of term
| Left of ttype * term
| Right of ttype * term
| Case of term * identifier * term * identifier * term
| Tuple of term * term
| Split of term * identifier * identifier * term
| Fold of ttype * term
| Unfold of term
| Macro of identifier * ttype list * term list
| Print_char of term
| Read_char
let rec pp_term fmt = function
| Unit -> pp_print_string fmt "()"
| Variable v -> pp_print_string fmt v
| Computation t -> fprintf fmt "@[<hv 2>lazy(@,%a)@]" pp_term t
| Abstraction (ttype, id, e) ->
fprintf fmt "@[<hv 2>λ(%s : %a,@ %a)@]" id pp_ttype ttype pp_term e
| Return t -> fprintf fmt "@[<hv 2>ret (@,%a)@]" pp_term t
| Bind (t, id, e) -> fprintf fmt "@[<hv 2>let %s =@ %a@]@ in@ %a" id pp_term t pp_term e
| Application (t1, t2) -> fprintf fmt "@[<hv 2>(@,%a@ .@ %a)@]" pp_term t1 pp_term t2
| Force t -> fprintf fmt "@[<hv 2>force (@,%a)@]" pp_term t
| Left (_, t) -> fprintf fmt "@[<hv 2>left(@,%a)@]"
pp_term t
| Right (_, t) -> fprintf fmt "@[<hv 2>right(@,%a)@]"
pp_term t
| Case (e, x1, e1, x2, e2) ->
fprintf fmt "@[<hv 2>(match@ %a with@ left(%s) ->@ %a@ right(%s) ->@ %a)@]"
pp_term e x1 pp_term e1 x2 pp_term e2
| Tuple (t1, t2) -> fprintf fmt "@[<hv 2><%a,@ %a>@]" pp_term t1 pp_term t2
| Split (e, x1, x2, e') ->
fprintf fmt "@[<hv 2>(let <%s,%s> =@ %a@ in %a)@]"
x1 x2 pp_term e pp_term e'
| Fold (_, e) -> fprintf fmt "@[<hv 2>fold(@,%a)@]" pp_term e
| Unfold e -> fprintf fmt "@[<hv 2>unfold(@,%a)@]" pp_term e
| Macro (m, tyl, tl) ->
let pp_sep fmt () = Format.fprintf fmt ",@ " in
fprintf fmt "%s[%a](%a)" m (pp_print_list ~pp_sep pp_ttype) tyl
(pp_print_list ~pp_sep pp_term) tl
| Print_char e -> fprintf fmt "@[<hv 2>print (@,%a)@]" pp_term e
| Read_char -> fprintf fmt "@[<hv 2>read ()@]"
type command =
| Declare of string * term
| Type of string * ttype
| DeclareMacro of string * string list * string list * term
| Typemacro of string * string list * ttype
| Check of term
| Eval of term
| Include of string
let rec tsubstitute subs t = match t with
| TUnit -> TUnit
| TVar id ->
begin match List.assoc_opt id subs with
| None -> t
| Some replacement -> replacement
end
| TArrow (tau1, tau2) ->
TArrow (tsubstitute subs tau1, tsubstitute subs tau2)
| TComp tau -> TComp (tsubstitute subs tau)
| TSum (tau1, tau2) -> TSum (tsubstitute subs tau1, tsubstitute subs tau2)
| TProduct (tau1, tau2) -> TProduct (tsubstitute subs tau1, tsubstitute subs tau2)
| TRecursive (id, tau) ->
TRecursive (id, tsubstitute (List.remove_assoc id subs) tau)
| TMacro (id, tl) -> TMacro (id, List.map (tsubstitute subs) tl)
(* [substitute f t e] replaces variables named f in e by term t] *)
let rec substitute subs t = match t with
| Unit -> Unit
| Variable id ->
begin match List.assoc_opt id subs with
| None -> t
| Some replacement -> replacement
end
| Computation c -> Computation (substitute subs c)
| Abstraction (tt, id, a) ->
Abstraction (tt, id, substitute (List.remove_assoc id subs) a)
| Return r -> Return (substitute subs r)
| Force r -> Force (substitute subs r)
| Bind (t1, id, t2) ->
Bind (substitute subs t1, id, substitute (List.remove_assoc id subs) t2)
| Application (t1, t2) -> Application (substitute subs t1, substitute subs t2)
| Right (ty, e) -> Right (ty, substitute subs e)
| Left (ty, e) -> Left (ty, substitute subs e)
| Case (e, x1, e1, x2, e2) ->
let e' = substitute subs e in
let e1' = substitute (List.remove_assoc x1 subs) e1 in
let e2' = substitute (List.remove_assoc x2 subs) e2 in
Case (e', x1, e1', x2, e2')
| Tuple (t1, t2) -> Tuple (substitute subs t1, substitute subs t2)
| Split (e1, x1, x2, e2) ->
let e1' = substitute subs e1 in
let e2' = substitute (List.remove_assoc x1 (List.remove_assoc x2 subs)) e2 in
Split (e1', x1, x2, e2')
| Fold (a, e) -> Fold (a, substitute subs e)
| Unfold e -> Unfold (substitute subs e)
| Macro (id, ttl, tl) -> Macro (id, ttl, List.map (substitute subs) tl)
| Print_char e -> Print_char (substitute subs e)
| Read_char -> Read_char
let nat_type = TRecursive ("char", TSum(TUnit, TVar "char"))
let maybe_type tau = TSum(tau, TUnit)
let rec int_of_term = function
| Fold (_, Right(_, next)) -> 1 + int_of_term next
| Fold (_, Left(_, Unit)) -> 0
| _ -> failwith "int_of_term got wrong structure"
let rec term_of_int i =
if i = 0 then Fold(nat_type, Left(nat_type, Unit))
else Fold(nat_type, Right(nat_type, term_of_int (i - 1)))
let print_char_term e =
let i = (int_of_term e) mod 256 in
if i < 32 && i <> 10 then
Printf.printf "<%d>%!" i
else Printf.printf "%c%!" (Char.chr i)
let term_of_option tau convert =
let ot = maybe_type tau in
function
| Some x -> Left(ot, convert x)
| None -> Right(ot, Unit)
let read_char_term () =
let c =
try Some(input_char stdin |> Char.code)
with End_of_file -> None
in term_of_option nat_type term_of_int c