comparison src/corify.sml @ 146:80ac94b54e41

Fix opening and corifying of functors
author Adam Chlipala <adamc@hcoop.net>
date Tue, 22 Jul 2008 18:20:13 -0400
parents f0d3402184d1
children eb16f2aadbe9
comparison
equal deleted inserted replaced
145:b1b33f7cf555 146:80ac94b54e41
56 structure St : sig 56 structure St : sig
57 type t 57 type t
58 58
59 val empty : t 59 val empty : t
60 60
61 val debug : t -> unit
62
61 val enter : t -> t 63 val enter : t -> t
62 val leave : t -> {outer : t, inner : t} 64 val leave : t -> {outer : t, inner : t}
63 val ffi : string -> L'.con SM.map -> t 65 val ffi : string -> L'.con SM.map -> t
64 66
65 datatype core_con = 67 datatype core_con =
78 80
79 val bindStr : t -> string -> int -> t -> t 81 val bindStr : t -> string -> int -> t -> t
80 val lookupStrById : t -> int -> t 82 val lookupStrById : t -> int -> t
81 val lookupStrByName : string * t -> t 83 val lookupStrByName : string * t -> t
82 84
83 val bindFunctor : t -> string -> int -> int -> L.str -> t 85 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
84 val lookupFunctorById : t -> int -> int * L.str 86 val lookupFunctorById : t -> int -> string * int * L.str
85 val lookupFunctorByName : string * t -> int * L.str 87 val lookupFunctorByName : string * t -> string * int * L.str
86 end = struct 88 end = struct
87 89
88 datatype flattening = 90 datatype flattening =
89 FNormal of {cons : int SM.map, 91 FNormal of {cons : int SM.map,
90 vals : int SM.map, 92 vals : int SM.map,
91 strs : flattening SM.map, 93 strs : flattening SM.map,
92 funs : (int * L.str) SM.map} 94 funs : (string * int * L.str) SM.map}
93 | FFfi of {mod : string, 95 | FFfi of {mod : string,
94 vals : L'.con SM.map} 96 vals : L'.con SM.map}
95 97
96 type t = { 98 type t = {
97 cons : int IM.map, 99 cons : int IM.map,
98 vals : int IM.map, 100 vals : int IM.map,
99 strs : flattening IM.map, 101 strs : flattening IM.map,
100 funs : (int * L.str) IM.map, 102 funs : (string * int * L.str) IM.map,
101 current : flattening, 103 current : flattening,
102 nested : flattening list 104 nested : flattening list
103 } 105 }
104 106
105 val empty = { 107 val empty = {
108 strs = IM.empty, 110 strs = IM.empty,
109 funs = IM.empty, 111 funs = IM.empty,
110 current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, 112 current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
111 nested = [] 113 nested = []
112 } 114 }
115
116 fun debug ({current = FNormal {cons, vals, strs, funs}, ...} : t) =
117 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
118 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
119 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
120 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
121 | debug _ = print "Not normal!\n"
113 122
114 datatype core_con = 123 datatype core_con =
115 CNormal of int 124 CNormal of int
116 | CFfi of string 125 | CFfi of string
117 126
241 | SOME f => dummy f) 250 | SOME f => dummy f)
242 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" 251 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
243 252
244 fun bindFunctor ({cons, vals, strs, funs, 253 fun bindFunctor ({cons, vals, strs, funs,
245 current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 254 current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
246 x n na str = 255 x n xa na str =
247 {cons = cons, 256 {cons = cons,
248 vals = vals, 257 vals = vals,
249 strs = strs, 258 strs = strs,
250 funs = IM.insert (funs, n, (na, str)), 259 funs = IM.insert (funs, n, (xa, na, str)),
251 current = FNormal {cons = mcons, 260 current = FNormal {cons = mcons,
252 vals = mvals, 261 vals = mvals,
253 strs = mstrs, 262 strs = mstrs,
254 funs = SM.insert (mfuns, x, (na, str))}, 263 funs = SM.insert (mfuns, x, (xa, na, str))},
255 nested = nested} 264 nested = nested}
256 | bindFunctor _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" 265 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
257 266
258 fun lookupFunctorById ({funs, ...} : t) n = 267 fun lookupFunctorById ({funs, ...} : t) n =
259 case IM.find (funs, n) of 268 case IM.find (funs, n) of
260 NONE => raise Fail "Corify.St.lookupFunctorById" 269 NONE => raise Fail "Corify.St.lookupFunctorById"
261 | SOME v => v 270 | SOME v => v
410 in 419 in
411 ([(L'.DValRec vis, loc)], st) 420 ([(L'.DValRec vis, loc)], st)
412 end 421 end
413 | L.DSgn _ => ([], st) 422 | L.DSgn _ => ([], st)
414 423
415 | L.DStr (x, n, _, (L.StrFun (_, na, _, _, str), _)) => 424 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
416 ([], St.bindFunctor st x n na str) 425 ([], St.bindFunctor st x n xa na str)
417 426
418 | L.DStr (x, n, _, str) => 427 | L.DStr (x, n, _, str) =>
419 let 428 let
420 val (ds, {inner, outer}) = corifyStr (str, st) 429 val (ds, {inner, outer}) = corifyStr (str, st)
421 val st = St.bindStr outer x n inner 430 val st = St.bindStr outer x n inner
512 in 521 in
513 (ds, st) 522 (ds, st)
514 end 523 end
515 end 524 end
516 | _ => raise Fail "Non-const signature for 'export'") 525 | _ => raise Fail "Non-const signature for 'export'")
517
518 526
519 and corifyStr ((str, _), st) = 527 and corifyStr ((str, _), st) =
520 case str of 528 case str of
521 L.StrConst ds => 529 L.StrConst ds =>
522 let 530 let
545 case str of 553 case str of
546 L.StrVar n => St.lookupFunctorById st n 554 L.StrVar n => St.lookupFunctorById st n
547 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str) 555 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
548 | _ => raise Fail "Corify of fancy functor application [2]" 556 | _ => raise Fail "Corify of fancy functor application [2]"
549 557
550 val (na, body) = unwind str1 558 val (xa, na, body) = unwind str1
551 559
552 val (ds1, {inner, outer}) = corifyStr (str2, st) 560 val (ds1, {inner = inner', outer}) = corifyStr (str2, st)
553 val (ds2, sts) = corifyStr (body, St.bindStr outer "ARG" na inner) 561 val (ds2, {inner, outer}) = corifyStr (body, St.bindStr outer xa na inner')
554 in 562 in
555 (ds1 @ ds2, sts) 563 (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer})
556 end 564 end
557 565
558 fun maxName ds = foldl (fn ((d, _), n) => 566 fun maxName ds = foldl (fn ((d, _), n) =>
559 case d of 567 case d of
560 L.DCon (_, n', _, _) => Int.max (n, n') 568 L.DCon (_, n', _, _) => Int.max (n, n')
575 | L.StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2) 583 | L.StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
576 584
577 fun corify ds = 585 fun corify ds =
578 let 586 let
579 val () = reset (maxName ds + 1) 587 val () = reset (maxName ds + 1)
588
580 val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds 589 val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds
581 in 590 in
582 ds 591 ds
583 end 592 end
584 593