Mercurial > urweb

comparison src/corify.sml @ 1989:210fb3dfc483

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some more nested functor bug-fixing, including generating fresh internal names at applications; still need to debug issues with datatype constructors
author Adam Chlipala <adam@chlipala.net>
date Thu, 20 Feb 2014 10:27:15 -0500
parents 6745eafff617
children 7bd2ecf96bb0
comparison
equal deleted inserted replaced
1988:abb6981a2c4c 1989:210fb3dfc483
62 let 62 let
63 val r = !count 63 val r = !count
64 in 64 in
65 count := r + 1; 65 count := r + 1;
66 r 66 r
67 end 67 end
68
69 fun getCounter () = !count
70 fun setCounter n = count := n
68 71
69 end 72 end
70 73
71 structure St : sig 74 structure St : sig
72 type t 75 type t
105 val lookupValById : t -> int -> int option 108 val lookupValById : t -> int -> int option
106 val lookupValByName : t -> string -> core_val 109 val lookupValByName : t -> string -> core_val
107 110
108 val bindStr : t -> string -> int -> t -> t 111 val bindStr : t -> string -> int -> t -> t
109 val lookupStrById : t -> int -> t 112 val lookupStrById : t -> int -> t
113 val lookupStrByIdOpt : t -> int -> t option
110 val lookupStrByName : string * t -> t 114 val lookupStrByName : string * t -> t
111 val lookupStrByNameOpt : string * t -> t option 115 val lookupStrByNameOpt : string * t -> t option
112 116
113 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t 117 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
114 val lookupFunctorById : t -> int -> string * int * L.str 118 val lookupFunctorById : t -> int -> string * int * L.str
119 val lookupFunctorByIdOpt : t -> int -> (string * int * L.str) option
115 val lookupFunctorByName : string * t -> string * int * L.str 120 val lookupFunctorByName : string * t -> string * int * L.str
116 end = struct 121 end = struct
117 122
118 datatype flattening = 123 datatype flattening =
119 FNormal of {name : string list, 124 FNormal of {name : string list,
397 fun lookupStrById ({basis, strs, ...} : t) n = 402 fun lookupStrById ({basis, strs, ...} : t) n =
398 case IM.find (strs, n) of 403 case IM.find (strs, n) of
399 NONE => raise Fail ("Corify.St.lookupStrById(" ^ Int.toString n ^ ")") 404 NONE => raise Fail ("Corify.St.lookupStrById(" ^ Int.toString n ^ ")")
400 | SOME f => dummy (basis, f) 405 | SOME f => dummy (basis, f)
401 406
407 fun lookupStrByIdOpt ({basis, strs, ...} : t) n =
408 case IM.find (strs, n) of
409 NONE => NONE
410 | SOME f => SOME (dummy (basis, f))
411
402 fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) = 412 fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) =
403 (case SM.find (strs, m) of 413 (case SM.find (strs, m) of
404 NONE => raise Fail "Corify.St.lookupStrByName [1]" 414 NONE => raise Fail "Corify.St.lookupStrByName [1]"
405 | SOME f => dummy (basis, f)) 415 | SOME f => dummy (basis, f))
406 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName [2]" 416 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName [2]"
432 442
433 fun lookupFunctorById ({funs, ...} : t) n = 443 fun lookupFunctorById ({funs, ...} : t) n =
434 case IM.find (funs, n) of 444 case IM.find (funs, n) of
435 NONE => raise Fail "Corify.St.lookupFunctorById" 445 NONE => raise Fail "Corify.St.lookupFunctorById"
436 | SOME v => v 446 | SOME v => v
447
448 fun lookupFunctorByIdOpt ({funs, ...} : t) n =
449 IM.find (funs, n)
437 450
438 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = 451 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
439 (case SM.find (funs, m) of 452 (case SM.find (funs, m) of
440 NONE => raise Fail ("Corify.St.lookupFunctorByName " ^ m ^ "[1]") 453 NONE => raise Fail ("Corify.St.lookupFunctorByName " ^ m ^ "[1]")
441 | SOME v => v) 454 | SOME v => v)
779 end 792 end
780 in 793 in
781 ([], st) 794 ([], st)
782 end 795 end
783 796
797 | L.DStr (x, n, _, (L.StrVar n', _)) =>
798 (case St.lookupFunctorByIdOpt st n' of
799 SOME (arg, dom, body) => ([], St.bindFunctor st x n arg dom body)
800 | NONE => ([], St.bindStr st x n (St.lookupStrById st n')))
801
784 | L.DStr (x, n, _, str) => 802 | L.DStr (x, n, _, str) =>
785 let 803 let
786 val mods' = 804 val mods' =
787 if x = "anon" then 805 if x = "anon" then
788 mods 806 mods
1128 St.ENormal n => ([(L'.DOnError n, loc)], st) 1146 St.ENormal n => ([(L'.DOnError n, loc)], st)
1129 | _ => (ErrorMsg.errorAt loc "Wrong type of identifier for 'onError'"; 1147 | _ => (ErrorMsg.errorAt loc "Wrong type of identifier for 'onError'";
1130 ([], st)) 1148 ([], st))
1131 end 1149 end
1132 1150
1133 and corifyStr mods ((str, _), st) = 1151 and corifyStr mods ((str, loc), st) =
1134 case str of 1152 case str of
1135 L.StrConst ds => 1153 L.StrConst ds =>
1136 let 1154 let
1137 val st = St.enter (st, mods) 1155 val st = St.enter (st, mods)
1138 val (ds, st) = ListUtil.foldlMapConcat (corifyDecl mods) st ds 1156 val (ds, st) = ListUtil.foldlMapConcat (corifyDecl mods) st ds
1160 L.StrVar n => St.lookupFunctorById st n 1178 L.StrVar n => St.lookupFunctorById st n
1161 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str) 1179 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
1162 | _ => raise Fail "Corify of fancy functor application [2]" 1180 | _ => raise Fail "Corify of fancy functor application [2]"
1163 1181
1164 val (xa, na, body) = unwind str1 1182 val (xa, na, body) = unwind str1
1183
1184 (* An important step to make sure that nested functors
1185 * "close under their environments": *)
1186 val (next, body') = ExplRename.rename {NextId = getCounter (),
1187 FormalName = xa,
1188 FormalId = na,
1189 Body = body}
1190
1191 (*val () = Print.prefaces ("RENAME " ^ ErrorMsg.spanToString loc)
1192 [("FROM", ExplPrint.p_str ExplEnv.empty body),
1193 ("TO", ExplPrint.p_str ExplEnv.empty body')]*)
1194 val body = body'
1195
1196 val () = setCounter next
1165 1197
1166 val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st) 1198 val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st)
1167 1199
1168 val (ds2, {inner, outer}) = corifyStr mods (body, St.bindStr outer xa na inner') 1200 val (ds2, {inner, outer}) = corifyStr mods (body, St.bindStr outer xa na inner')
1169 in 1201 in