Mercurial > urweb

comparison src/corify.sml @ 46:44a1bc863f0f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Corifying functors
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 17:55:36 -0400
parents 3c1ce1b4eb3d
children 0a5c312de09a
comparison
equal deleted inserted replaced
45:3c1ce1b4eb3d 46:44a1bc863f0f
66 val lookupCoreByName : t -> string -> int 66 val lookupCoreByName : t -> string -> int
67 67
68 val bindStr : t -> string -> int -> t -> t 68 val bindStr : t -> string -> int -> t -> t
69 val lookupStrById : t -> int -> t 69 val lookupStrById : t -> int -> t
70 val lookupStrByName : string * t -> t 70 val lookupStrByName : string * t -> t
71
72 val bindFunctor : t -> string -> int -> int -> L.str -> t
73 val lookupFunctorById : t -> int -> int * L.str
74 val lookupFunctorByName : string * t -> int * L.str
71 end = struct 75 end = struct
72 76
73 datatype flattening = F of { 77 datatype flattening = F of {
74 core : int SM.map, 78 core : int SM.map,
75 strs : flattening SM.map 79 strs : flattening SM.map,
80 funs : (int * L.str) SM.map
76 } 81 }
77 82
78 type t = { 83 type t = {
79 core : int IM.map, 84 core : int IM.map,
80 strs : flattening IM.map, 85 strs : flattening IM.map,
86 funs : (int * L.str) IM.map,
81 current : flattening, 87 current : flattening,
82 nested : flattening list 88 nested : flattening list
83 } 89 }
84 90
85 val empty = { 91 val empty = {
86 core = IM.empty, 92 core = IM.empty,
87 strs = IM.empty, 93 strs = IM.empty,
88 current = F { core = SM.empty, strs = SM.empty }, 94 funs = IM.empty,
95 current = F { core = SM.empty, strs = SM.empty, funs = SM.empty },
89 nested = [] 96 nested = []
90 } 97 }
91 98
92 fun bindCore {core, strs, current, nested} s n = 99 fun bindCore {core, strs, funs, current, nested} s n =
93 let 100 let
94 val n' = alloc () 101 val n' = alloc ()
95 102
96 val current = 103 val current =
97 let 104 let
98 val F {core, strs} = current 105 val F {core, strs, funs} = current
99 in 106 in
100 F {core = SM.insert (core, s, n'), 107 F {core = SM.insert (core, s, n'),
101 strs = strs} 108 strs = strs,
109 funs = funs}
102 end 110 end
103 in 111 in
104 ({core = IM.insert (core, n, n'), 112 ({core = IM.insert (core, n, n'),
105 strs = strs, 113 strs = strs,
114 funs = funs,
106 current = current, 115 current = current,
107 nested = nested}, 116 nested = nested},
108 n') 117 n')
109 end 118 end
110 119
113 fun lookupCoreByName ({current = F {core, ...}, ...} : t) x = 122 fun lookupCoreByName ({current = F {core, ...}, ...} : t) x =
114 case SM.find (core, x) of 123 case SM.find (core, x) of
115 NONE => raise Fail "Corify.St.lookupCoreByName" 124 NONE => raise Fail "Corify.St.lookupCoreByName"
116 | SOME n => n 125 | SOME n => n
117 126
118 fun enter {core, strs, current, nested} = 127 fun enter {core, strs, funs, current, nested} =
119 {core = core, 128 {core = core,
120 strs = strs, 129 strs = strs,
130 funs = funs,
121 current = F {core = SM.empty, 131 current = F {core = SM.empty,
122 strs = SM.empty}, 132 strs = SM.empty,
133 funs = SM.empty},
123 nested = current :: nested} 134 nested = current :: nested}
124 135
125 fun dummy f = {core = IM.empty, 136 fun dummy f = {core = IM.empty,
126 strs = IM.empty, 137 strs = IM.empty,
138 funs = IM.empty,
127 current = f, 139 current = f,
128 nested = []} 140 nested = []}
129 141
130 fun leave {core, strs, current, nested = m1 :: rest} = 142 fun leave {core, strs, funs, current, nested = m1 :: rest} =
131 {outer = {core = core, 143 {outer = {core = core,
132 strs = strs, 144 strs = strs,
145 funs = funs,
133 current = m1, 146 current = m1,
134 nested = rest}, 147 nested = rest},
135 inner = dummy current} 148 inner = dummy current}
136 | leave _ = raise Fail "Corify.St.leave" 149 | leave _ = raise Fail "Corify.St.leave"
137 150
138 fun bindStr ({core, strs, current = F {core = mcore, strs = mstrs}, nested} : t) x n ({current = f, ...} : t) = 151 fun bindStr ({core, strs, funs, current = F {core = mcore, strs = mstrs, funs = mfuns}, nested} : t)
152 x n ({current = f, ...} : t) =
139 {core = core, 153 {core = core,
140 strs = IM.insert (strs, n, f), 154 strs = IM.insert (strs, n, f),
155 funs = funs,
141 current = F {core = mcore, 156 current = F {core = mcore,
142 strs = SM.insert (mstrs, x, f)}, 157 strs = SM.insert (mstrs, x, f),
158 funs = mfuns},
143 nested = nested} 159 nested = nested}
144 160
145 fun lookupStrById ({strs, ...} : t) n = 161 fun lookupStrById ({strs, ...} : t) n =
146 case IM.find (strs, n) of 162 case IM.find (strs, n) of
147 NONE => raise Fail "Corify.St.lookupStr" 163 NONE => raise Fail "Corify.St.lookupStrById"
148 | SOME f => dummy f 164 | SOME f => dummy f
149 165
150 fun lookupStrByName (m, {current = F {strs, ...}, ...} : t) = 166 fun lookupStrByName (m, {current = F {strs, ...}, ...} : t) =
151 case SM.find (strs, m) of 167 case SM.find (strs, m) of
152 NONE => raise Fail "Corify.St.lookupStrByName" 168 NONE => raise Fail "Corify.St.lookupStrByName"
153 | SOME f => dummy f 169 | SOME f => dummy f
170
171 fun bindFunctor ({core, strs, funs, current = F {core = mcore, strs = mstrs, funs = mfuns}, nested} : t)
172 x n na str =
173 {core = core,
174 strs = strs,
175 funs = IM.insert (funs, n, (na, str)),
176 current = F {core = mcore,
177 strs = mstrs,
178 funs = SM.insert (mfuns, x, (na, str))},
179 nested = nested}
180
181 fun lookupFunctorById ({funs, ...} : t) n =
182 case IM.find (funs, n) of
183 NONE => raise Fail "Corify.St.lookupFunctorById"
184 | SOME v => v
185
186 fun lookupFunctorByName (m, {current = F {funs, ...}, ...} : t) =
187 case SM.find (funs, m) of
188 NONE => raise Fail "Corify.St.lookupFunctorByName"
189 | SOME v => v
154 190
155 end 191 end
156 192
157 193
158 fun corifyKind (k, loc) = 194 fun corifyKind (k, loc) =
231 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e), loc)], st) 267 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e), loc)], st)
232 end 268 end
233 269
234 | L.DSgn _ => ([], st) 270 | L.DSgn _ => ([], st)
235 271
272 | L.DStr (x, n, _, (L.StrFun (_, na, _, _, str), _)) =>
273 ([], St.bindFunctor st x n na str)
274
236 | L.DStr (x, n, _, str) => 275 | L.DStr (x, n, _, str) =>
237 let 276 let
238 val (ds, {inner, outer}) = corifyStr (str, st) 277 val (ds, {inner, outer}) = corifyStr (str, st)
239 val st = St.bindStr outer x n inner 278 val st = St.bindStr outer x n inner
240 in 279 in
255 let 294 let
256 val (ds, {inner, outer}) = corifyStr (str, st) 295 val (ds, {inner, outer}) = corifyStr (str, st)
257 in 296 in
258 (ds, {inner = St.lookupStrByName (x, inner), outer = outer}) 297 (ds, {inner = St.lookupStrByName (x, inner), outer = outer})
259 end 298 end
260 | L.StrFun _ => raise Fail "Corify functor" 299 | L.StrFun _ => raise Fail "Corify of nested functor definition"
261 | L.StrApp _ => raise Fail "Corify functor app" 300 | L.StrApp (str1, str2) =>
301 let
302 fun unwind' (str, _) =
303 case str of
304 L.StrVar n => St.lookupStrById st n
305 | L.StrProj (str, x) => St.lookupStrByName (x, unwind' str)
306 | _ => raise Fail "Corify of fancy functor application [1]"
307
308 fun unwind (str, _) =
309 case str of
310 L.StrVar n => St.lookupFunctorById st n
311 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
312 | _ => raise Fail "Corify of fancy functor application [2]"
313
314 val (na, body) = unwind str1
315
316 val (ds1, {inner, outer}) = corifyStr (str2, st)
317 val (ds2, sts) = corifyStr (body, St.bindStr outer "ARG" na inner)
318 in
319 (ds1 @ ds2, sts)
320 end
262 321
263 fun maxName ds = foldl (fn ((d, _), n) => 322 fun maxName ds = foldl (fn ((d, _), n) =>
264 case d of 323 case d of
265 L.DCon (_, n', _, _) => Int.max (n, n') 324 L.DCon (_, n', _, _) => Int.max (n, n')
266 | L.DVal (_, n', _ , _) => Int.max (n, n') 325 | L.DVal (_, n', _ , _) => Int.max (n, n')