Mercurial > urweb

comparison src/elab_env.sml @ 188:8e9f97508f0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Datatype representation optimization
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 19:49:21 -0400
parents 88d46972de53
children aa54250f58ac
comparison
equal deleted inserted replaced
187:fb6ed259f5bd 188:8e9f97508f0d
79 renameC : kind var' SM.map, 79 renameC : kind var' SM.map,
80 relC : (string * kind) list, 80 relC : (string * kind) list,
81 namedC : (string * kind * con option) IM.map, 81 namedC : (string * kind * con option) IM.map,
82 82
83 datatypes : datatyp IM.map, 83 datatypes : datatyp IM.map,
84 constructors : (int * con option * int) SM.map, 84 constructors : (datatype_kind * int * con option * int) SM.map,
85 85
86 renameE : con var' SM.map, 86 renameE : con var' SM.map,
87 relE : (string * con) list, 87 relE : (string * con) list,
88 namedE : (string * con) IM.map, 88 namedE : (string * con) IM.map,
89 89
187 NONE => NotBound 187 NONE => NotBound
188 | SOME (Rel' x) => Rel x 188 | SOME (Rel' x) => Rel x
189 | SOME (Named' x) => Named x 189 | SOME (Named' x) => Named x
190 190
191 fun pushDatatype (env : env) n xncs = 191 fun pushDatatype (env : env) n xncs =
192 {renameC = #renameC env, 192 let
193 relC = #relC env, 193 val dk = U.classifyDatatype xncs
194 namedC = #namedC env, 194 in
195 195 {renameC = #renameC env,
196 datatypes = IM.insert (#datatypes env, n, 196 relC = #relC env,
197 foldl (fn ((x, n, to), cons) => 197 namedC = #namedC env,
198 IM.insert (cons, n, (x, to))) IM.empty xncs), 198
199 constructors = foldl (fn ((x, n', to), cmap) => 199 datatypes = IM.insert (#datatypes env, n,
200 SM.insert (cmap, x, (n', to, n))) 200 foldl (fn ((x, n, to), cons) =>
201 (#constructors env) xncs, 201 IM.insert (cons, n, (x, to))) IM.empty xncs),
202 202 constructors = foldl (fn ((x, n', to), cmap) =>
203 renameE = #renameE env, 203 SM.insert (cmap, x, (dk, n', to, n)))
204 relE = #relE env, 204 (#constructors env) xncs,
205 namedE = #namedE env, 205
206 206 renameE = #renameE env,
207 renameSgn = #renameSgn env, 207 relE = #relE env,
208 sgn = #sgn env, 208 namedE = #namedE env,
209 209
210 renameStr = #renameStr env, 210 renameSgn = #renameSgn env,
211 str = #str env} 211 sgn = #sgn env,
212
213 renameStr = #renameStr env,
214 str = #str env}
215 end
212 216
213 fun lookupDatatype (env : env) n = 217 fun lookupDatatype (env : env) n =
214 case IM.find (#datatypes env, n) of 218 case IM.find (#datatypes env, n) of
215 NONE => raise UnboundNamed n 219 NONE => raise UnboundNamed n
216 | SOME x => x 220 | SOME x => x
577 fun consider (n, xncs) = 581 fun consider (n, xncs) =
578 ListUtil.search (fn (x, n', to) => 582 ListUtil.search (fn (x, n', to) =>
579 if x <> field then 583 if x <> field then
580 NONE 584 NONE
581 else 585 else
582 SOME (n', to, (CNamed n, #2 str))) xncs 586 SOME (U.classifyDatatype xncs, n', to, (CNamed n, #2 str))) xncs
583 in 587 in
584 case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs) 588 case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs)
585 | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs) 589 | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs)
586 | _ => NONE) sgis of 590 | _ => NONE) sgis of
587 NONE => NONE 591 NONE => NONE
588 | SOME ((n, to, t), subs) => SOME (n, Option.map (sgnSubCon (str, subs)) to, sgnSubCon (str, subs) t) 592 | SOME ((dk, n, to, t), subs) => SOME (dk, n, Option.map (sgnSubCon (str, subs)) to,
593 sgnSubCon (str, subs) t)
589 end 594 end
590 | _ => NONE 595 | _ => NONE
591 596
592 fun projectVal env {sgn, str, field} = 597 fun projectVal env {sgn, str, field} =
593 case #1 (hnormSgn env sgn) of 598 case #1 (hnormSgn env sgn) of