Mercurial > urweb

comparison src/corify.sml @ 376:6fd102fa28f9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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