Mercurial > urweb
comparison src/corify.sml @ 376:6fd102fa28f9
Simple generation of persistent paths
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 19 Oct 2008 11:11:49 -0400 |
parents | 075b36dbb1a4 |
children | 78358e5df273 |
comparison
equal
deleted
inserted
replaced
375:d3de57ce4bca | 376:6fd102fa28f9 |
---|---|
35 structure SM = BinaryMapFn(struct | 35 structure SM = BinaryMapFn(struct |
36 type ord_key = string | 36 type ord_key = string |
37 val compare = String.compare | 37 val compare = String.compare |
38 end) | 38 end) |
39 | 39 |
40 val restify = ref (fn s : string => s) | |
41 | |
42 fun doRestify (mods, s) = | |
43 let | |
44 val s = if String.isPrefix "wrap_" s then | |
45 String.extract (s, 5, NONE) | |
46 else | |
47 s | |
48 in | |
49 !restify (String.concatWith "/" (rev (s :: mods))) | |
50 end | |
51 | |
40 local | 52 local |
41 val count = ref 0 | 53 val count = ref 0 |
42 in | 54 in |
43 | 55 |
44 fun reset v = count := v | 56 fun reset v = count := v |
58 | 70 |
59 val empty : t | 71 val empty : t |
60 | 72 |
61 val debug : t -> unit | 73 val debug : t -> unit |
62 | 74 |
63 val enter : t -> t | 75 val name : t -> string list |
76 | |
77 val enter : t * string list -> t | |
64 val leave : t -> {outer : t, inner : t} | 78 val leave : t -> {outer : t, inner : t} |
65 val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t | 79 val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t |
66 | 80 |
67 val basisIs : t * int -> t | 81 val basisIs : t * int -> t |
68 val lookupBasis : t -> int option | 82 val lookupBasis : t -> int option |
96 val lookupFunctorById : t -> int -> string * int * L.str | 110 val lookupFunctorById : t -> int -> string * int * L.str |
97 val lookupFunctorByName : string * t -> string * int * L.str | 111 val lookupFunctorByName : string * t -> string * int * L.str |
98 end = struct | 112 end = struct |
99 | 113 |
100 datatype flattening = | 114 datatype flattening = |
101 FNormal of {cons : int SM.map, | 115 FNormal of {name : string list, |
116 cons : int SM.map, | |
102 constructors : L'.patCon SM.map, | 117 constructors : L'.patCon SM.map, |
103 vals : int SM.map, | 118 vals : int SM.map, |
104 strs : flattening SM.map, | 119 strs : flattening SM.map, |
105 funs : (string * int * L.str) SM.map} | 120 funs : (string * int * L.str) SM.map} |
106 | FFfi of {mod : string, | 121 | FFfi of {mod : string, |
123 cons = IM.empty, | 138 cons = IM.empty, |
124 constructors = IM.empty, | 139 constructors = IM.empty, |
125 vals = IM.empty, | 140 vals = IM.empty, |
126 strs = IM.empty, | 141 strs = IM.empty, |
127 funs = IM.empty, | 142 funs = IM.empty, |
128 current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, | 143 current = FNormal { name = [], cons = SM.empty, constructors = SM.empty, |
144 vals = SM.empty, strs = SM.empty, funs = SM.empty }, | |
129 nested = [] | 145 nested = [] |
130 } | 146 } |
131 | 147 |
132 fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) = | 148 fun debug ({current = FNormal {cons, constructors, vals, strs, funs, ...}, ...} : t) = |
133 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " | 149 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " |
134 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " | 150 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " |
135 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " | 151 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " |
136 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " | 152 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " |
137 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") | 153 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") |
138 | debug _ = print "Not normal!\n" | 154 | debug _ = print "Not normal!\n" |
155 | |
156 fun name ({current = FNormal {name, ...}, ...} : t) = name | |
157 | name {current = FFfi {mod = name, ...}, ...} = [name] | |
139 | 158 |
140 fun basisIs ({cons, constructors, vals, strs, funs, current, nested, ...} : t, basis) = | 159 fun basisIs ({cons, constructors, vals, strs, funs, current, nested, ...} : t, basis) = |
141 {basis = SOME basis, | 160 {basis = SOME basis, |
142 cons = cons, | 161 cons = cons, |
143 constructors = constructors, | 162 constructors = constructors, |
162 val n' = alloc () | 181 val n' = alloc () |
163 | 182 |
164 val current = | 183 val current = |
165 case current of | 184 case current of |
166 FFfi _ => raise Fail "Binding inside FFfi" | 185 FFfi _ => raise Fail "Binding inside FFfi" |
167 | FNormal {cons, constructors, vals, strs, funs} => | 186 | FNormal {name, cons, constructors, vals, strs, funs} => |
168 FNormal {cons = SM.insert (cons, s, n'), | 187 FNormal {name = name, |
188 cons = SM.insert (cons, s, n'), | |
169 constructors = constructors, | 189 constructors = constructors, |
170 vals = vals, | 190 vals = vals, |
171 strs = strs, | 191 strs = strs, |
172 funs = funs} | 192 funs = funs} |
173 in | 193 in |
197 val n' = alloc () | 217 val n' = alloc () |
198 | 218 |
199 val current = | 219 val current = |
200 case current of | 220 case current of |
201 FFfi _ => raise Fail "Binding inside FFfi" | 221 FFfi _ => raise Fail "Binding inside FFfi" |
202 | FNormal {cons, constructors, vals, strs, funs} => | 222 | FNormal {name, cons, constructors, vals, strs, funs} => |
203 FNormal {cons = cons, | 223 FNormal {name = name, |
224 cons = cons, | |
204 constructors = constructors, | 225 constructors = constructors, |
205 vals = SM.insert (vals, s, n'), | 226 vals = SM.insert (vals, s, n'), |
206 strs = strs, | 227 strs = strs, |
207 funs = funs} | 228 funs = funs} |
208 in | 229 in |
220 fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n = | 241 fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n = |
221 let | 242 let |
222 val current = | 243 val current = |
223 case current of | 244 case current of |
224 FFfi _ => raise Fail "Binding inside FFfi" | 245 FFfi _ => raise Fail "Binding inside FFfi" |
225 | FNormal {cons, constructors, vals, strs, funs} => | 246 | FNormal {name, cons, constructors, vals, strs, funs} => |
226 FNormal {cons = cons, | 247 FNormal {name = name, |
248 cons = cons, | |
227 constructors = constructors, | 249 constructors = constructors, |
228 vals = SM.insert (vals, s, n), | 250 vals = SM.insert (vals, s, n), |
229 strs = strs, | 251 strs = strs, |
230 funs = funs} | 252 funs = funs} |
231 in | 253 in |
256 fun bindConstructor {basis, cons, constructors, vals, strs, funs, current, nested} s n n' = | 278 fun bindConstructor {basis, cons, constructors, vals, strs, funs, current, nested} s n n' = |
257 let | 279 let |
258 val current = | 280 val current = |
259 case current of | 281 case current of |
260 FFfi _ => raise Fail "Binding inside FFfi" | 282 FFfi _ => raise Fail "Binding inside FFfi" |
261 | FNormal {cons, constructors, vals, strs, funs} => | 283 | FNormal {name, cons, constructors, vals, strs, funs} => |
262 FNormal {cons = cons, | 284 FNormal {name = name, |
285 cons = cons, | |
263 constructors = SM.insert (constructors, s, n'), | 286 constructors = SM.insert (constructors, s, n'), |
264 vals = vals, | 287 vals = vals, |
265 strs = strs, | 288 strs = strs, |
266 funs = funs} | 289 funs = funs} |
267 in | 290 in |
300 | FNormal {constructors, ...} => | 323 | FNormal {constructors, ...} => |
301 case SM.find (constructors, x) of | 324 case SM.find (constructors, x) of |
302 NONE => raise Fail "Corify.St.lookupConstructorByName [2]" | 325 NONE => raise Fail "Corify.St.lookupConstructorByName [2]" |
303 | SOME n => n | 326 | SOME n => n |
304 | 327 |
305 fun enter {basis, cons, constructors, vals, strs, funs, current, nested} = | 328 fun enter ({basis, cons, constructors, vals, strs, funs, current, nested}, name) = |
306 {basis = basis, | 329 {basis = basis, |
307 cons = cons, | 330 cons = cons, |
308 constructors = constructors, | 331 constructors = constructors, |
309 vals = vals, | 332 vals = vals, |
310 strs = strs, | 333 strs = strs, |
311 funs = funs, | 334 funs = funs, |
312 current = FNormal {cons = SM.empty, | 335 current = FNormal {name = name, |
336 cons = SM.empty, | |
313 constructors = SM.empty, | 337 constructors = SM.empty, |
314 vals = SM.empty, | 338 vals = SM.empty, |
315 strs = SM.empty, | 339 strs = SM.empty, |
316 funs = SM.empty}, | 340 funs = SM.empty}, |
317 nested = current :: nested} | 341 nested = current :: nested} |
338 | leave _ = raise Fail "Corify.St.leave" | 362 | leave _ = raise Fail "Corify.St.leave" |
339 | 363 |
340 fun ffi m vals constructors = dummy (NONE, FFfi {mod = m, vals = vals, constructors = constructors}) | 364 fun ffi m vals constructors = dummy (NONE, FFfi {mod = m, vals = vals, constructors = constructors}) |
341 | 365 |
342 fun bindStr ({basis, cons, constructors, vals, strs, funs, | 366 fun bindStr ({basis, cons, constructors, vals, strs, funs, |
343 current = FNormal {cons = mcons, constructors = mconstructors, | 367 current = FNormal {name, cons = mcons, constructors = mconstructors, |
344 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) | 368 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) |
345 x n ({current = f, ...} : t) = | 369 x n ({current = f, ...} : t) = |
346 {basis = basis, | 370 {basis = basis, |
347 cons = cons, | 371 cons = cons, |
348 constructors = constructors, | 372 constructors = constructors, |
349 vals = vals, | 373 vals = vals, |
350 strs = IM.insert (strs, n, f), | 374 strs = IM.insert (strs, n, f), |
351 funs = funs, | 375 funs = funs, |
352 current = FNormal {cons = mcons, | 376 current = FNormal {name = name, |
377 cons = mcons, | |
353 constructors = mconstructors, | 378 constructors = mconstructors, |
354 vals = mvals, | 379 vals = mvals, |
355 strs = SM.insert (mstrs, x, f), | 380 strs = SM.insert (mstrs, x, f), |
356 funs = mfuns}, | 381 funs = mfuns}, |
357 nested = nested} | 382 nested = nested} |
373 NONE => NONE | 398 NONE => NONE |
374 | SOME f => SOME (dummy (basis, f))) | 399 | SOME f => SOME (dummy (basis, f))) |
375 | lookupStrByNameOpt _ = NONE | 400 | lookupStrByNameOpt _ = NONE |
376 | 401 |
377 fun bindFunctor ({basis, cons, constructors, vals, strs, funs, | 402 fun bindFunctor ({basis, cons, constructors, vals, strs, funs, |
378 current = FNormal {cons = mcons, constructors = mconstructors, | 403 current = FNormal {name, cons = mcons, constructors = mconstructors, |
379 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) | 404 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) |
380 x n xa na str = | 405 x n xa na str = |
381 {basis = basis, | 406 {basis = basis, |
382 cons = cons, | 407 cons = cons, |
383 constructors = constructors, | 408 constructors = constructors, |
384 vals = vals, | 409 vals = vals, |
385 strs = strs, | 410 strs = strs, |
386 funs = IM.insert (funs, n, (xa, na, str)), | 411 funs = IM.insert (funs, n, (xa, na, str)), |
387 current = FNormal {cons = mcons, | 412 current = FNormal {name = name, |
413 cons = mcons, | |
388 constructors = mconstructors, | 414 constructors = mconstructors, |
389 vals = mvals, | 415 vals = mvals, |
390 strs = mstrs, | 416 strs = mstrs, |
391 funs = SM.insert (mfuns, x, (xa, na, str))}, | 417 funs = SM.insert (mfuns, x, (xa, na, str))}, |
392 nested = nested} | 418 nested = nested} |
549 {disc = corifyCon st disc, result = corifyCon st result}), | 575 {disc = corifyCon st disc, result = corifyCon st result}), |
550 loc) | 576 loc) |
551 | 577 |
552 | L.EWrite e => (L'.EWrite (corifyExp st e), loc) | 578 | L.EWrite e => (L'.EWrite (corifyExp st e), loc) |
553 | 579 |
554 fun corifyDecl ((d, loc : EM.span), st) = | 580 fun corifyDecl mods ((d, loc : EM.span), st) = |
555 case d of | 581 case d of |
556 L.DCon (x, n, k, c) => | 582 L.DCon (x, n, k, c) => |
557 let | 583 let |
558 val (st, n) = St.bindCon st x n | 584 val (st, n) = St.bindCon st x n |
559 in | 585 in |
601 let | 627 let |
602 val (st, n) = St.bindCon st x n | 628 val (st, n) = St.bindCon st x n |
603 val c = corifyCon st (L.CModProj (m1, ms, s), loc) | 629 val c = corifyCon st (L.CModProj (m1, ms, s), loc) |
604 | 630 |
605 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms | 631 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms |
606 val (_, {inner, ...}) = corifyStr (m, st) | 632 val (_, {inner, ...}) = corifyStr mods (m, st) |
607 | 633 |
608 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => | 634 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => |
609 let | 635 let |
610 val n' = St.lookupConstructorByName inner x | 636 val n' = St.lookupConstructorByName inner x |
611 val st = St.bindConstructor st x n n' | 637 val st = St.bindConstructor st x n n' |
636 ((L'.DCon (x, n, k', cBase), loc) :: cds, st) | 662 ((L'.DCon (x, n, k', cBase), loc) :: cds, st) |
637 end | 663 end |
638 | L.DVal (x, n, t, e) => | 664 | L.DVal (x, n, t, e) => |
639 let | 665 let |
640 val (st, n) = St.bindVal st x n | 666 val (st, n) = St.bindVal st x n |
641 val s = | 667 val s = doRestify (mods, x) |
642 if String.isPrefix "wrap_" x then | |
643 String.extract (x, 5, NONE) | |
644 else | |
645 x | |
646 in | 668 in |
647 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) | 669 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) |
648 end | 670 end |
649 | L.DValRec vis => | 671 | L.DValRec vis => |
650 let | 672 let |
658 st vis | 680 st vis |
659 | 681 |
660 val vis = map | 682 val vis = map |
661 (fn (x, n, t, e) => | 683 (fn (x, n, t, e) => |
662 let | 684 let |
663 val s = | 685 val s = doRestify (mods, x) |
664 if String.isPrefix "wrap_" x then | |
665 String.extract (x, 5, NONE) | |
666 else | |
667 x | |
668 in | 686 in |
669 (x, n, corifyCon st t, corifyExp st e, s) | 687 (x, n, corifyCon st t, corifyExp st e, s) |
670 end) | 688 end) |
671 vis | 689 vis |
672 in | 690 in |
677 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => | 695 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => |
678 ([], St.bindFunctor st x n xa na str) | 696 ([], St.bindFunctor st x n xa na str) |
679 | 697 |
680 | L.DStr (x, n, _, (L.StrProj (str, x'), _)) => | 698 | L.DStr (x, n, _, (L.StrProj (str, x'), _)) => |
681 let | 699 let |
682 val (ds, {inner, outer}) = corifyStr (str, st) | 700 val (ds, {inner, outer}) = corifyStr mods (str, st) |
683 | 701 |
684 val st = case St.lookupStrByNameOpt (x', inner) of | 702 val st = case St.lookupStrByNameOpt (x', inner) of |
685 SOME st' => St.bindStr st x n st' | 703 SOME st' => St.bindStr st x n st' |
686 | NONE => | 704 | NONE => |
687 let | 705 let |
693 ([], st) | 711 ([], st) |
694 end | 712 end |
695 | 713 |
696 | L.DStr (x, n, _, str) => | 714 | L.DStr (x, n, _, str) => |
697 let | 715 let |
698 val (ds, {inner, outer}) = corifyStr (str, st) | 716 val (ds, {inner, outer}) = corifyStr (x :: mods) (str, st) |
699 val st = St.bindStr outer x n inner | 717 val st = St.bindStr outer x n inner |
700 in | 718 in |
701 (ds, st) | 719 (ds, st) |
702 end | 720 end |
703 | 721 |
869 | _ => (wds, eds)) | 887 | _ => (wds, eds)) |
870 | _ => (wds, eds) | 888 | _ => (wds, eds) |
871 | 889 |
872 val (wds, eds) = foldl wrapSgi ([], []) sgis | 890 val (wds, eds) = foldl wrapSgi ([], []) sgis |
873 val wrapper = (L.StrConst wds, loc) | 891 val wrapper = (L.StrConst wds, loc) |
874 val (ds, {inner, outer}) = corifyStr (wrapper, st) | 892 val mst = St.lookupStrById st m |
893 val (ds, {inner, outer}) = corifyStr (St.name mst) (wrapper, st) | |
875 val st = St.bindStr outer "wrapper" en inner | 894 val st = St.bindStr outer "wrapper" en inner |
876 | 895 |
877 val ds = ds @ map (fn f => f st) eds | 896 val ds = ds @ map (fn f => f st) eds |
878 in | 897 in |
879 (ds, st) | 898 (ds, st) |
882 | _ => raise Fail "Non-const signature for 'export'") | 901 | _ => raise Fail "Non-const signature for 'export'") |
883 | 902 |
884 | L.DTable (_, x, n, c) => | 903 | L.DTable (_, x, n, c) => |
885 let | 904 let |
886 val (st, n) = St.bindVal st x n | 905 val (st, n) = St.bindVal st x n |
887 val s = x | 906 val s = doRestify (mods, x) |
888 in | 907 in |
889 ([(L'.DTable (x, n, corifyCon st c, s), loc)], st) | 908 ([(L'.DTable (x, n, corifyCon st c, s), loc)], st) |
890 end | 909 end |
891 | L.DSequence (_, x, n) => | 910 | L.DSequence (_, x, n) => |
892 let | 911 let |
893 val (st, n) = St.bindVal st x n | 912 val (st, n) = St.bindVal st x n |
894 val s = x | 913 val s = doRestify (mods, x) |
895 in | 914 in |
896 ([(L'.DSequence (x, n, s), loc)], st) | 915 ([(L'.DSequence (x, n, s), loc)], st) |
897 end | 916 end |
898 | 917 |
899 | L.DDatabase s => ([(L'.DDatabase s, loc)], st) | 918 | L.DDatabase s => ([(L'.DDatabase s, loc)], st) |
900 | 919 |
901 and corifyStr ((str, _), st) = | 920 and corifyStr mods ((str, _), st) = |
902 case str of | 921 case str of |
903 L.StrConst ds => | 922 L.StrConst ds => |
904 let | 923 let |
905 val st = St.enter st | 924 val st = St.enter (st, mods) |
906 val (ds, st) = ListUtil.foldlMapConcat corifyDecl st ds | 925 val (ds, st) = ListUtil.foldlMapConcat (corifyDecl mods) st ds |
907 in | 926 in |
908 (ds, St.leave st) | 927 (ds, St.leave st) |
909 end | 928 end |
910 | L.StrVar n => ([], {inner = St.lookupStrById st n, outer = st}) | 929 | L.StrVar n => ([], {inner = St.lookupStrById st n, outer = st}) |
911 | L.StrProj (str, x) => | 930 | L.StrProj (str, x) => |
912 let | 931 let |
913 val (ds, {inner, outer}) = corifyStr (str, st) | 932 val (ds, {inner, outer}) = corifyStr mods (str, st) |
914 in | 933 in |
915 (ds, {inner = St.lookupStrByName (x, inner), outer = outer}) | 934 (ds, {inner = St.lookupStrByName (x, inner), outer = outer}) |
916 end | 935 end |
917 | L.StrFun _ => raise Fail "Corify of nested functor definition" | 936 | L.StrFun _ => raise Fail "Corify of nested functor definition" |
918 | L.StrApp (str1, str2) => | 937 | L.StrApp (str1, str2) => |
929 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str) | 948 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str) |
930 | _ => raise Fail "Corify of fancy functor application [2]" | 949 | _ => raise Fail "Corify of fancy functor application [2]" |
931 | 950 |
932 val (xa, na, body) = unwind str1 | 951 val (xa, na, body) = unwind str1 |
933 | 952 |
934 val (ds1, {inner = inner', outer}) = corifyStr (str2, st) | 953 val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st) |
935 val (ds2, {inner, outer}) = corifyStr (body, St.bindStr outer xa na inner') | 954 |
955 val mods' = mods | |
956 | |
957 val (ds2, {inner, outer}) = corifyStr mods' (body, St.bindStr outer xa na inner') | |
936 in | 958 in |
937 (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer}) | 959 (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer}) |
938 end | 960 end |
939 | 961 |
940 fun maxName ds = foldl (fn ((d, _), n) => | 962 fun maxName ds = foldl (fn ((d, _), n) => |
963 | 985 |
964 fun corify ds = | 986 fun corify ds = |
965 let | 987 let |
966 val () = reset (maxName ds + 1) | 988 val () = reset (maxName ds + 1) |
967 | 989 |
968 val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds | 990 val (ds, _) = ListUtil.foldlMapConcat (corifyDecl []) St.empty ds |
969 in | 991 in |
970 ds | 992 ds |
971 end | 993 end |
972 | 994 |
973 end | 995 end |