Mercurial > urweb

comparison src/elab_print.sml @ 11:e97c6d335869

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simple elaboration working
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 15:20:46 -0400
parents 14b533dbe6cc
children d89477f07c1e
comparison
equal deleted inserted replaced
10:dde5c52e5e5e 11:e97c6d335869
34 34
35 open Elab 35 open Elab
36 36
37 structure E = ElabEnv 37 structure E = ElabEnv
38 38
39 val debug = ref false
40
39 fun p_kind' par (k, _) = 41 fun p_kind' par (k, _) =
40 case k of 42 case k of
41 KType => string "Type" 43 KType => string "Type"
42 | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, 44 | KArrow (k1, k2) => parenIf par (box [p_kind' true k1,
43 space, 45 space,
83 p_con env c]) xcs, 85 p_con env c]) xcs,
84 string "}"] 86 string "}"]
85 | TRecord c => box [string "$", 87 | TRecord c => box [string "$",
86 p_con' true env c] 88 p_con' true env c]
87 89
88 | CRel n => string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) 90 | CRel n =>
89 | CNamed n => string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) 91 if !debug then
92 string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
93 else
94 string (#1 (E.lookupCRel env n))
95 | CNamed n =>
96 if !debug then
97 string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
98 else
99 string (#1 (E.lookupCNamed env n))
90 100
91 | CApp (c1, c2) => parenIf par (box [p_con env c1, 101 | CApp (c1, c2) => parenIf par (box [p_con env c1,
92 space, 102 space,
93 p_con' true env c2]) 103 p_con' true env c2])
94 | CAbs (x, k, c) => parenIf par (box [string "fn", 104 | CAbs (x, k, c) => parenIf par (box [string "fn",
128 138
129 and p_con env = p_con' false env 139 and p_con env = p_con' false env
130 140
131 fun p_exp' par env (e, _) = 141 fun p_exp' par env (e, _) =
132 case e of 142 case e of
133 ERel n => string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) 143 ERel n =>
134 | ENamed n => string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) 144 if !debug then
145 string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
146 else
147 string (#1 (E.lookupERel env n))
148 | ENamed n =>
149 if !debug then
150 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
151 else
152 string (#1 (E.lookupENamed env n))
135 | EApp (e1, e2) => parenIf par (box [p_exp env e1, 153 | EApp (e1, e2) => parenIf par (box [p_exp env e1,
136 space, 154 space,
137 p_exp' true env e2]) 155 p_exp' true env e2])
138 | EAbs (x, t, e) => parenIf par (box [string "fn", 156 | EAbs (x, t, e) => parenIf par (box [string "fn",
139 space, 157 space,
167 185
168 and p_exp env = p_exp' false env 186 and p_exp env = p_exp' false env
169 187
170 fun p_decl env ((d, _) : decl) = 188 fun p_decl env ((d, _) : decl) =
171 case d of 189 case d of
172 DCon (x, n, k, c) => box [string "con", 190 DCon (x, n, k, c) =>
173 space, 191 let
174 string x, 192 val xp = if !debug then
175 string "__", 193 box [string x,
176 string (Int.toString n), 194 string "__",
177 space, 195 string (Int.toString n)]
178 string "::", 196 else
179 space, 197 string x
180 p_kind k, 198 in
181 space, 199 box [string "con",
182 string "=", 200 space,
183 space, 201 xp,
184 p_con env c] 202 space,
185 | DVal (x, n, t, e) => box [string "val", 203 string "::",
186 space, 204 space,
187 string x, 205 p_kind k,
188 string "__", 206 space,
189 string (Int.toString n), 207 string "=",
190 space, 208 space,
191 string ":", 209 p_con env c]
192 space, 210 end
193 p_con env t, 211 | DVal (x, n, t, e) =>
194 space, 212 let
195 string "=", 213 val xp = if !debug then
196 space, 214 box [string x,
197 p_exp env e] 215 string "__",
216 string (Int.toString n)]
217 else
218 string x
219 in
220 box [string "val",
221 space,
222 xp,
223 space,
224 string ":",
225 space,
226 p_con env t,
227 space,
228 string "=",
229 space,
230 p_exp env e]
231 end
198 232
199 fun p_file env file = 233 fun p_file env file =
200 let 234 let
201 val (_, pds) = ListUtil.mapfoldl (fn (d, env) => 235 val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
202 (ElabUtil.declBinds env d, 236 (ElabUtil.declBinds env d,