Mercurial > urweb
changeset 249:b6b75e6e0898
Corify transaction wrappers
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 31 Aug 2008 09:45:23 -0400 |
| parents | d5b12daa9b47 |
| children | 98f551ddd54b |
| files | src/corify.sml src/elaborate.sml tests/query.ur |
| diffstat | 3 files changed, 691 insertions(+), 628 deletions(-) [+] |
line wrap: on
line diff
--- a/src/corify.sml Sun Aug 31 09:05:33 2008 -0400 +++ b/src/corify.sml Sun Aug 31 09:45:23 2008 -0400 @@ -64,6 +64,9 @@ val leave : t -> {outer : t, inner : t} val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t + val basisIs : t * int -> t + val lookupBasis : t -> int option + datatype core_con = CNormal of int | CFfi of string @@ -75,650 +78,673 @@ val lookupConstructorByNameOpt : t -> string -> L'.patCon option val lookupConstructorByName : t -> string -> L'.patCon val lookupConstructorById : t -> int -> L'.patCon + + datatype core_val = + ENormal of int + | EFfi of string * L'.con + val bindVal : t -> string -> int -> t * int + val bindConstructorVal : t -> string -> int -> t + val lookupValById : t -> int -> int option + val lookupValByName : t -> string -> core_val - datatype core_val = - ENormal of int - | EFfi of string * L'.con - val bindVal : t -> string -> int -> t * int - val bindConstructorVal : t -> string -> int -> t - val lookupValById : t -> int -> int option - val lookupValByName : t -> string -> core_val + val bindStr : t -> string -> int -> t -> t + val lookupStrById : t -> int -> t + val lookupStrByName : string * t -> t - val bindStr : t -> string -> int -> t -> t - val lookupStrById : t -> int -> t - val lookupStrByName : string * t -> t + val bindFunctor : t -> string -> int -> string -> int -> L.str -> t + val lookupFunctorById : t -> int -> string * int * L.str + val lookupFunctorByName : string * t -> string * int * L.str +end = struct - val bindFunctor : t -> string -> int -> string -> int -> L.str -> t - val lookupFunctorById : t -> int -> string * int * L.str - val lookupFunctorByName : string * t -> string * int * L.str - end = struct +datatype flattening = + FNormal of {cons : int SM.map, + constructors : L'.patCon SM.map, + vals : int SM.map, + strs : flattening SM.map, + funs : (string * int * L.str) SM.map} + | FFfi of {mod : string, + vals : L'.con SM.map, + constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map} - datatype flattening = - FNormal of {cons : int SM.map, - constructors : L'.patCon SM.map, - vals : int SM.map, - strs : flattening SM.map, - funs : (string * int * L.str) SM.map} - | FFfi of {mod : string, - vals : L'.con SM.map, - constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map} +type t = { + basis : int option, + cons : int IM.map, + constructors : L'.patCon IM.map, + vals : int IM.map, + strs : flattening IM.map, + funs : (string * int * L.str) IM.map, + current : flattening, + nested : flattening list +} - type t = { - cons : int IM.map, - constructors : L'.patCon IM.map, - vals : int IM.map, - strs : flattening IM.map, - funs : (string * int * L.str) IM.map, - current : flattening, - nested : flattening list - } +val empty = { + basis = NONE, + cons = IM.empty, + constructors = IM.empty, + vals = IM.empty, + strs = IM.empty, + funs = IM.empty, + current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, + nested = [] +} - val empty = { - cons = IM.empty, - constructors = IM.empty, - vals = IM.empty, - strs = IM.empty, - funs = IM.empty, - current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, - nested = [] - } +fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) = + print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " + ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " + ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " + ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " + ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") + | debug _ = print "Not normal!\n" - fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) = - print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " - ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " - ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " - ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " - ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") - | debug _ = print "Not normal!\n" +fun basisIs ({cons, constructors, vals, strs, funs, current, nested, ...} : t, basis) = + {basis = SOME basis, + cons = cons, + constructors = constructors, + vals = vals, + strs = strs, + funs = funs, + current = current, + nested = nested} - datatype core_con = - CNormal of int - | CFfi of string +fun lookupBasis ({basis, ...} : t) = basis - datatype core_val = - ENormal of int - | EFfi of string * L'.con +datatype core_con = + CNormal of int + | CFfi of string - fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n = - let - val n' = alloc () +datatype core_val = + ENormal of int + | EFfi of string * L'.con - val current = - case current of - FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {cons, constructors, vals, strs, funs} => - FNormal {cons = SM.insert (cons, s, n'), - constructors = constructors, - vals = vals, - strs = strs, - funs = funs} - in - ({cons = IM.insert (cons, n, n'), - constructors = constructors, - vals = vals, - strs = strs, - funs = funs, - current = current, - nested = nested}, - n') - end +fun bindCon {basis, cons, constructors, vals, strs, funs, current, nested} s n = + let + val n' = alloc () - fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) - - fun lookupConByName ({current, ...} : t) x = - case current of - FFfi {mod = m, ...} => CFfi m - | FNormal {cons, ...} => - case SM.find (cons, x) of - NONE => raise Fail "Corify.St.lookupConByName" - | SOME n => CNormal n - - fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n = - let - val n' = alloc () - - val current = - case current of - FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {cons, constructors, vals, strs, funs} => - FNormal {cons = cons, - constructors = constructors, - vals = SM.insert (vals, s, n'), - strs = strs, - funs = funs} - in - ({cons = cons, - constructors = constructors, - vals = IM.insert (vals, n, n'), - strs = strs, - funs = funs, - current = current, - nested = nested}, - n') - end - - fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n = - let - val current = - case current of - FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {cons, constructors, vals, strs, funs} => - FNormal {cons = cons, - constructors = constructors, - vals = SM.insert (vals, s, n), - strs = strs, - funs = funs} - in - {cons = cons, + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, constructors, vals, strs, funs} => + FNormal {cons = SM.insert (cons, s, n'), + constructors = constructors, + vals = vals, + strs = strs, + funs = funs} + in + ({basis = basis, + cons = IM.insert (cons, n, n'), constructors = constructors, - vals = IM.insert (vals, n, n), - strs = strs, - funs = funs, - current = current, - nested = nested} - end - - - fun lookupValById ({vals, ...} : t) n = IM.find (vals, n) - - fun lookupValByName ({current, ...} : t) x = - case current of - FFfi {mod = m, vals, ...} => - (case SM.find (vals, x) of - NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val" - | SOME t => EFfi (m, t)) - | FNormal {vals, ...} => - case SM.find (vals, x) of - NONE => raise Fail "Corify.St.lookupValByName" - | SOME n => ENormal n - - fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' = - let - val current = - case current of - FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {cons, constructors, vals, strs, funs} => - FNormal {cons = cons, - constructors = SM.insert (constructors, s, n'), - vals = vals, - strs = strs, - funs = funs} - in - {cons = cons, - constructors = IM.insert (constructors, n, n'), vals = vals, strs = strs, funs = funs, current = current, - nested = nested} - end + nested = nested}, + n') + end - fun lookupConstructorById ({constructors, ...} : t) n = - case IM.find (constructors, n) of - NONE => raise Fail "Corify.St.lookupConstructorById" - | SOME x => x +fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) - fun lookupConstructorByNameOpt ({current, ...} : t) x = - case current of - FFfi {mod = m, constructors, ...} => - (case SM.find (constructors, x) of - NONE => NONE - | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})) - | FNormal {constructors, ...} => - case SM.find (constructors, x) of +fun lookupConByName ({current, ...} : t) x = + case current of + FFfi {mod = m, ...} => CFfi m + | FNormal {cons, ...} => + case SM.find (cons, x) of + NONE => raise Fail "Corify.St.lookupConByName" + | SOME n => CNormal n + +fun bindVal {basis, cons, constructors, vals, strs, funs, current, nested} s n = + let + val n' = alloc () + + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, constructors, vals, strs, funs} => + FNormal {cons = cons, + constructors = constructors, + vals = SM.insert (vals, s, n'), + strs = strs, + funs = funs} + in + ({basis = basis, + cons = cons, + constructors = constructors, + vals = IM.insert (vals, n, n'), + strs = strs, + funs = funs, + current = current, + nested = nested}, + n') + end + +fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n = + let + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, constructors, vals, strs, funs} => + FNormal {cons = cons, + constructors = constructors, + vals = SM.insert (vals, s, n), + strs = strs, + funs = funs} + in + {basis = basis, + cons = cons, + constructors = constructors, + vals = IM.insert (vals, n, n), + strs = strs, + funs = funs, + current = current, + nested = nested} + end + + +fun lookupValById ({vals, ...} : t) n = IM.find (vals, n) + +fun lookupValByName ({current, ...} : t) x = + case current of + FFfi {mod = m, vals, ...} => + (case SM.find (vals, x) of + NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val" + | SOME t => EFfi (m, t)) + | FNormal {vals, ...} => + case SM.find (vals, x) of + NONE => raise Fail "Corify.St.lookupValByName" + | SOME n => ENormal n + +fun bindConstructor {basis, cons, constructors, vals, strs, funs, current, nested} s n n' = + let + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, constructors, vals, strs, funs} => + FNormal {cons = cons, + constructors = SM.insert (constructors, s, n'), + vals = vals, + strs = strs, + funs = funs} + in + {basis = basis, + cons = cons, + constructors = IM.insert (constructors, n, n'), + vals = vals, + strs = strs, + funs = funs, + current = current, + nested = nested} + end + +fun lookupConstructorById ({constructors, ...} : t) n = + case IM.find (constructors, n) of + NONE => raise Fail "Corify.St.lookupConstructorById" + | SOME x => x + +fun lookupConstructorByNameOpt ({current, ...} : t) x = + case current of + FFfi {mod = m, constructors, ...} => + (case SM.find (constructors, x) of NONE => NONE - | SOME n => SOME n + | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})) + | FNormal {constructors, ...} => + case SM.find (constructors, x) of + NONE => NONE + | SOME n => SOME n - fun lookupConstructorByName ({current, ...} : t) x = - case current of - FFfi {mod = m, constructors, ...} => - (case SM.find (constructors, x) of - NONE => raise Fail "Corify.St.lookupConstructorByName [1]" - | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}) - | FNormal {constructors, ...} => - case SM.find (constructors, x) of - NONE => raise Fail "Corify.St.lookupConstructorByName [2]" - | SOME n => n +fun lookupConstructorByName ({current, ...} : t) x = + case current of + FFfi {mod = m, constructors, ...} => + (case SM.find (constructors, x) of + NONE => raise Fail "Corify.St.lookupConstructorByName [1]" + | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}) + | FNormal {constructors, ...} => + case SM.find (constructors, x) of + NONE => raise Fail "Corify.St.lookupConstructorByName [2]" + | SOME n => n - fun enter {cons, constructors, vals, strs, funs, current, nested} = - {cons = cons, - constructors = constructors, - vals = vals, - strs = strs, - funs = funs, - current = FNormal {cons = SM.empty, - constructors = SM.empty, - vals = SM.empty, - strs = SM.empty, - funs = SM.empty}, - nested = current :: nested} +fun enter {basis, cons, constructors, vals, strs, funs, current, nested} = + {basis = basis, + cons = cons, + constructors = constructors, + vals = vals, + strs = strs, + funs = funs, + current = FNormal {cons = SM.empty, + constructors = SM.empty, + vals = SM.empty, + strs = SM.empty, + funs = SM.empty}, + nested = current :: nested} - fun dummy f = {cons = IM.empty, - constructors = IM.empty, - vals = IM.empty, - strs = IM.empty, - funs = IM.empty, - current = f, - nested = []} +fun dummy (b, f) = {basis = b, + cons = IM.empty, + constructors = IM.empty, + vals = IM.empty, + strs = IM.empty, + funs = IM.empty, + current = f, + nested = []} - fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} = - {outer = {cons = cons, - constructors = constructors, - vals = vals, - strs = strs, - funs = funs, - current = m1, - nested = rest}, - inner = dummy current} - | leave _ = raise Fail "Corify.St.leave" +fun leave {basis, cons, constructors, vals, strs, funs, current, nested = m1 :: rest} = + {outer = {basis = basis, + cons = cons, + constructors = constructors, + vals = vals, + strs = strs, + funs = funs, + current = m1, + nested = rest}, + inner = dummy (basis, current)} + | leave _ = raise Fail "Corify.St.leave" - fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors}) +fun ffi m vals constructors = dummy (NONE, FFfi {mod = m, vals = vals, constructors = constructors}) - fun bindStr ({cons, constructors, vals, strs, funs, - current = FNormal {cons = mcons, constructors = mconstructors, - vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) - x n ({current = f, ...} : t) = - {cons = cons, - constructors = constructors, - vals = vals, - strs = IM.insert (strs, n, f), - funs = funs, - current = FNormal {cons = mcons, - constructors = mconstructors, - vals = mvals, - strs = SM.insert (mstrs, x, f), - funs = mfuns}, - nested = nested} - | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" +fun bindStr ({basis, cons, constructors, vals, strs, funs, + current = FNormal {cons = mcons, constructors = mconstructors, + vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) + x n ({current = f, ...} : t) = + {basis = basis, + cons = cons, + constructors = constructors, + vals = vals, + strs = IM.insert (strs, n, f), + funs = funs, + current = FNormal {cons = mcons, + constructors = mconstructors, + vals = mvals, + strs = SM.insert (mstrs, x, f), + funs = mfuns}, + nested = nested} + | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" - fun lookupStrById ({strs, ...} : t) n = - case IM.find (strs, n) of - NONE => raise Fail "Corify.St.lookupStrById" - | SOME f => dummy f +fun lookupStrById ({basis, strs, ...} : t) n = + case IM.find (strs, n) of + NONE => raise Fail "Corify.St.lookupStrById" + | SOME f => dummy (basis, f) - fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) = - (case SM.find (strs, m) of - NONE => raise Fail "Corify.St.lookupStrByName" - | SOME f => dummy f) - | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" +fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) = + (case SM.find (strs, m) of + NONE => raise Fail "Corify.St.lookupStrByName" + | SOME f => dummy (basis, f)) + | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" - fun bindFunctor ({cons, constructors, vals, strs, funs, - current = FNormal {cons = mcons, constructors = mconstructors, - vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) - x n xa na str = - {cons = cons, - constructors = constructors, - vals = vals, - strs = strs, - funs = IM.insert (funs, n, (xa, na, str)), - current = FNormal {cons = mcons, - constructors = mconstructors, - vals = mvals, - strs = mstrs, - funs = SM.insert (mfuns, x, (xa, na, str))}, - nested = nested} - | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" +fun bindFunctor ({basis, cons, constructors, vals, strs, funs, + current = FNormal {cons = mcons, constructors = mconstructors, + vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) + x n xa na str = + {basis = basis, + cons = cons, + constructors = constructors, + vals = vals, + strs = strs, + funs = IM.insert (funs, n, (xa, na, str)), + current = FNormal {cons = mcons, + constructors = mconstructors, + vals = mvals, + strs = mstrs, + funs = SM.insert (mfuns, x, (xa, na, str))}, + nested = nested} + | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" - fun lookupFunctorById ({funs, ...} : t) n = - case IM.find (funs, n) of - NONE => raise Fail "Corify.St.lookupFunctorById" - | SOME v => v +fun lookupFunctorById ({funs, ...} : t) n = + case IM.find (funs, n) of + NONE => raise Fail "Corify.St.lookupFunctorById" + | SOME v => v - fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = - (case SM.find (funs, m) of - NONE => raise Fail "Corify.St.lookupFunctorByName" - | SOME v => v) - | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" +fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = + (case SM.find (funs, m) of + NONE => raise Fail "Corify.St.lookupFunctorByName" + | SOME v => v) + | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" - end +end - fun corifyKind (k, loc) = - case k of - L.KType => (L'.KType, loc) - | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) - | L.KName => (L'.KName, loc) - | L.KRecord k => (L'.KRecord (corifyKind k), loc) - | L.KUnit => (L'.KUnit, loc) - | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc) +fun corifyKind (k, loc) = + case k of + L.KType => (L'.KType, loc) + | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) + | L.KName => (L'.KName, loc) + | L.KRecord k => (L'.KRecord (corifyKind k), loc) + | L.KUnit => (L'.KUnit, loc) + | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc) - fun corifyCon st (c, loc) = - case c of - L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) - | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) - | L.TRecord c => (L'.TRecord (corifyCon st c), loc) +fun corifyCon st (c, loc) = + case c of + L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) + | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) + | L.TRecord c => (L'.TRecord (corifyCon st c), loc) - | L.CRel n => (L'.CRel n, loc) - | L.CNamed n => - (case St.lookupConById st n of - NONE => (L'.CNamed n, loc) - | SOME n => (L'.CNamed n, loc)) - | L.CModProj (m, ms, x) => - let - val st = St.lookupStrById st m - val st = foldl St.lookupStrByName st ms - in - case St.lookupConByName st x of - St.CNormal n => (L'.CNamed n, loc) - | St.CFfi m => (L'.CFfi (m, x), loc) - end + | L.CRel n => (L'.CRel n, loc) + | L.CNamed n => + (case St.lookupConById st n of + NONE => (L'.CNamed n, loc) + | SOME n => (L'.CNamed n, loc)) + | L.CModProj (m, ms, x) => + let + val st = St.lookupStrById st m + val st = foldl St.lookupStrByName st ms + in + case St.lookupConByName st x of + St.CNormal n => (L'.CNamed n, loc) + | St.CFfi m => (L'.CFfi (m, x), loc) + end - | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) - | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) + | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) + | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) - | L.CName s => (L'.CName s, loc) + | L.CName s => (L'.CName s, loc) - | L.CRecord (k, xcs) => - (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) - | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) - | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) - | L.CUnit => (L'.CUnit, loc) + | L.CRecord (k, xcs) => + (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) + | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) + | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) + | L.CUnit => (L'.CUnit, loc) - | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc) - | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc) + | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc) + | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc) - fun corifyPatCon st pc = - case pc of - L.PConVar n => St.lookupConstructorById st n - | L.PConProj (m1, ms, x) => - let - val st = St.lookupStrById st m1 - val st = foldl St.lookupStrByName st ms - in - St.lookupConstructorByName st x - end +fun corifyPatCon st pc = + case pc of + L.PConVar n => St.lookupConstructorById st n + | L.PConProj (m1, ms, x) => + let + val st = St.lookupStrById st m1 + val st = foldl St.lookupStrByName st ms + in + St.lookupConstructorByName st x + end - fun corifyPat st (p, loc) = - case p of - L.PWild => (L'.PWild, loc) - | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) - | L.PPrim p => (L'.PPrim p, loc) - | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts, - Option.map (corifyPat st) po), loc) - | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) +fun corifyPat st (p, loc) = + case p of + L.PWild => (L'.PWild, loc) + | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) + | L.PPrim p => (L'.PPrim p, loc) + | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts, + Option.map (corifyPat st) po), loc) + | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) - fun corifyExp st (e, loc) = - case e of - L.EPrim p => (L'.EPrim p, loc) - | L.ERel n => (L'.ERel n, loc) - | L.ENamed n => - (case St.lookupValById st n of - NONE => (L'.ENamed n, loc) - | SOME n => (L'.ENamed n, loc)) - | L.EModProj (m, ms, x) => - let - val st = St.lookupStrById st m - val st = foldl St.lookupStrByName st ms - in - case St.lookupConstructorByNameOpt st x of - SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) => - let - val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params - val e = case arg of - NONE => (L'.ECon (kind, pc, args, NONE), loc) - | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), - (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc) +fun corifyExp st (e, loc) = + case e of + L.EPrim p => (L'.EPrim p, loc) + | L.ERel n => (L'.ERel n, loc) + | L.ENamed n => + (case St.lookupValById st n of + NONE => (L'.ENamed n, loc) + | SOME n => (L'.ENamed n, loc)) + | L.EModProj (m, ms, x) => + let + val st = St.lookupStrById st m + val st = foldl St.lookupStrByName st ms + in + case St.lookupConstructorByNameOpt st x of + SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) => + let + val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params + val e = case arg of + NONE => (L'.ECon (kind, pc, args, NONE), loc) + | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), + (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc) - val k = (L'.KType, loc) - in - foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params - end - | _ => - case St.lookupValByName st x of - St.ENormal n => (L'.ENamed n, loc) - | St.EFfi (m, t) => - case t of - (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => - (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) - | t as (L'.TFun _, _) => - let - fun getArgs (all as (t, _), args) = - case t of - L'.TFun (dom, ran) => getArgs (ran, dom :: args) - | _ => (all, rev args) + val k = (L'.KType, loc) + in + foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params + end + | _ => + case St.lookupValByName st x of + St.ENormal n => (L'.ENamed n, loc) + | St.EFfi (m, t) => + case t of + (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => + (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) + | t as (L'.TFun _, _) => + let + fun getArgs (all as (t, _), args) = + case t of + L'.TFun (dom, ran) => getArgs (ran, dom :: args) + | _ => (all, rev args) - val (result, args) = getArgs (t, []) + val (result, args) = getArgs (t, []) - val (actuals, _) = foldr (fn (_, (actuals, n)) => - ((L'.ERel n, loc) :: actuals, - n + 1)) ([], 0) args - val app = (L'.EFfiApp (m, x, actuals), loc) - val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => - ((L'.EAbs ("arg" ^ Int.toString n, - t, - ran, - abs), loc), - (L'.TFun (t, ran), loc), - n - 1)) (app, result, length args - 1) args - in - abs - end - | _ => (L'.EFfi (m, x), loc) - end - | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) - | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) - | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) - | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) + val (actuals, _) = foldr (fn (_, (actuals, n)) => + ((L'.ERel n, loc) :: actuals, + n + 1)) ([], 0) args + val app = (L'.EFfiApp (m, x, actuals), loc) + val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => + ((L'.EAbs ("arg" ^ Int.toString n, + t, + ran, + abs), loc), + (L'.TFun (t, ran), loc), + n - 1)) (app, result, length args - 1) args + in + abs + end + | _ => (L'.EFfi (m, x), loc) + end + | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) + | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) + | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) + | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) - | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => - (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) - | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, - {field = corifyCon st field, rest = corifyCon st rest}), loc) - | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, - {field = corifyCon st field, rest = corifyCon st rest}), loc) - | L.EFold k => (L'.EFold (corifyKind k), loc) + | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => + (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) + | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, + {field = corifyCon st field, rest = corifyCon st rest}), loc) + | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, + {field = corifyCon st field, rest = corifyCon st rest}), loc) + | L.EFold k => (L'.EFold (corifyKind k), loc) - | L.ECase (e, pes, {disc, result}) => - (L'.ECase (corifyExp st e, - map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, - {disc = corifyCon st disc, result = corifyCon st result}), - loc) + | L.ECase (e, pes, {disc, result}) => + (L'.ECase (corifyExp st e, + map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, + {disc = corifyCon st disc, result = corifyCon st result}), + loc) - | L.EWrite e => (L'.EWrite (corifyExp st e), loc) + | L.EWrite e => (L'.EWrite (corifyExp st e), loc) - fun corifyDecl ((d, loc : EM.span), st) = - case d of - L.DCon (x, n, k, c) => - let - val (st, n) = St.bindCon st x n - in - ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) - end - | L.DDatatype (x, n, xs, xncs) => - let - val (st, n) = St.bindCon st x n - val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => - let - val st = St.bindConstructor st x n (L'.PConVar n) - val st = St.bindConstructorVal st x n - val co = Option.map (corifyCon st) co - in - ((x, n, co), st) - end) st xncs +fun corifyDecl ((d, loc : EM.span), st) = + case d of + L.DCon (x, n, k, c) => + let + val (st, n) = St.bindCon st x n + in + ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) + end + | L.DDatatype (x, n, xs, xncs) => + let + val (st, n) = St.bindCon st x n + val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => + let + val st = St.bindConstructor st x n (L'.PConVar n) + val st = St.bindConstructorVal st x n + val co = Option.map (corifyCon st) co + in + ((x, n, co), st) + end) st xncs - val dk = ElabUtil.classifyDatatype xncs - val t = (L'.CNamed n, loc) - val nxs = length xs - 1 - val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs - val k = (L'.KType, loc) - val dcons = map (fn (x, n, to) => - let - val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs - val (e, t) = - case to of - NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) - | SOME t' => ((L'.EAbs ("x", t', t, - (L'.ECon (dk, L'.PConVar n, args, - SOME (L'.ERel 0, loc)), - loc)), - loc), - (L'.TFun (t', t), loc)) + val dk = ElabUtil.classifyDatatype xncs + val t = (L'.CNamed n, loc) + val nxs = length xs - 1 + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs + val k = (L'.KType, loc) + val dcons = map (fn (x, n, to) => + let + val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs + val (e, t) = + case to of + NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) + | SOME t' => ((L'.EAbs ("x", t', t, + (L'.ECon (dk, L'.PConVar n, args, + SOME (L'.ERel 0, loc)), + loc)), + loc), + (L'.TFun (t', t), loc)) - val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs - val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs - in - (L'.DVal (x, n, t, e, ""), loc) - end) xncs - in - ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st) - end - | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => - let - val (st, n) = St.bindCon st x n - val c = corifyCon st (L.CModProj (m1, ms, s), loc) + val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs + val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs + in + (L'.DVal (x, n, t, e, ""), loc) + end) xncs + in + ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st) + end + | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => + let + val (st, n) = St.bindCon st x n + val c = corifyCon st (L.CModProj (m1, ms, s), loc) - val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms - val (_, {inner, ...}) = corifyStr (m, st) + val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms + val (_, {inner, ...}) = corifyStr (m, st) - val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => - let - val n' = St.lookupConstructorByName inner x - val st = St.bindConstructor st x n n' - val (st, n) = St.bindVal st x n - val co = Option.map (corifyCon st) co - in - ((x, n, co), st) - end) st xncs + val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => + let + val n' = St.lookupConstructorByName inner x + val st = St.bindConstructor st x n n' + val (st, n) = St.bindVal st x n + val co = Option.map (corifyCon st) co + in + ((x, n, co), st) + end) st xncs - val nxs = length xs - 1 - val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs - val k = (L'.KType, loc) - val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs + val nxs = length xs - 1 + val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs + val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs - val cds = map (fn (x, n, co) => - let - val t = case co of - NONE => c - | SOME t' => (L'.TFun (t', c), loc) - val e = corifyExp st (L.EModProj (m1, ms, x), loc) + val cds = map (fn (x, n, co) => + let + val t = case co of + NONE => c + | SOME t' => (L'.TFun (t', c), loc) + val e = corifyExp st (L.EModProj (m1, ms, x), loc) - val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs - in - (L'.DVal (x, n, t, e, x), loc) - end) xncs - in - ((L'.DCon (x, n, k', c), loc) :: cds, st) - end - | L.DVal (x, n, t, e) => - let - val (st, n) = St.bindVal st x n - val s = - if String.isPrefix "wrap_" x then - String.extract (x, 5, NONE) - else - x - in - ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) - end - | L.DValRec vis => - let - val (vis, st) = ListUtil.foldlMap - (fn ((x, n, t, e), st) => - let - val (st, n) = St.bindVal st x n - in - ((x, n, t, e), st) - end) - st vis + val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs + in + (L'.DVal (x, n, t, e, x), loc) + end) xncs + in + ((L'.DCon (x, n, k', c), loc) :: cds, st) + end + | L.DVal (x, n, t, e) => + let + val (st, n) = St.bindVal st x n + val s = + if String.isPrefix "wrap_" x then + String.extract (x, 5, NONE) + else + x + in + ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) + end + | L.DValRec vis => + let + val (vis, st) = ListUtil.foldlMap + (fn ((x, n, t, e), st) => + let + val (st, n) = St.bindVal st x n + in + ((x, n, t, e), st) + end) + st vis - val vis = map - (fn (x, n, t, e) => - let - val s = - if String.isPrefix "wrap_" x then - String.extract (x, 5, NONE) - else - x - in - (x, n, corifyCon st t, corifyExp st e, s) - end) - vis - in - ([(L'.DValRec vis, loc)], st) - end - | L.DSgn _ => ([], st) + val vis = map + (fn (x, n, t, e) => + let + val s = + if String.isPrefix "wrap_" x then + String.extract (x, 5, NONE) + else + x + in + (x, n, corifyCon st t, corifyExp st e, s) + end) + vis + in + ([(L'.DValRec vis, loc)], st) + end + | L.DSgn _ => ([], st) - | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => - ([], St.bindFunctor st x n xa na str) + | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => + ([], St.bindFunctor st x n xa na str) - | L.DStr (x, n, _, str) => - let - val (ds, {inner, outer}) = corifyStr (str, st) - val st = St.bindStr outer x n inner - in - (ds, st) - end + | L.DStr (x, n, _, str) => + let + val (ds, {inner, outer}) = corifyStr (str, st) + val st = St.bindStr outer x n inner + in + (ds, st) + end - | L.DFfiStr (m, n, (sgn, _)) => - (case sgn of - L.SgnConst sgis => - let - val (ds, cmap, conmap, st) = - foldl (fn ((sgi, _), (ds, cmap, conmap, st)) => - case sgi of - L.SgiConAbs (x, n, k) => - let - val (st, n') = St.bindCon st x n - in - ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, - cmap, - conmap, - st) - end - | L.SgiCon (x, n, k, _) => - let - val (st, n') = St.bindCon st x n - in - ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, - cmap, - conmap, - st) - end + | L.DFfiStr (m, n, (sgn, _)) => + (case sgn of + L.SgnConst sgis => + let + val (ds, cmap, conmap, st) = + foldl (fn ((sgi, _), (ds, cmap, conmap, st)) => + case sgi of + L.SgiConAbs (x, n, k) => + let + val (st, n') = St.bindCon st x n + in + ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, + cmap, + conmap, + st) + end + | L.SgiCon (x, n, k, _) => + let + val (st, n') = St.bindCon st x n + in + ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, + cmap, + conmap, + st) + end - | L.SgiDatatype (x, n, xs, xnts) => - let - val k = (L'.KType, loc) - val dk = ElabUtil.classifyDatatype xnts - val (st, n') = St.bindCon st x n - val (xnts, (ds', st, cmap, conmap)) = - ListUtil.foldlMap - (fn ((x', n, to), (ds', st, cmap, conmap)) => - let - val dt = (L'.CNamed n', loc) - val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs + | L.SgiDatatype (x, n, xs, xnts) => + let + val k = (L'.KType, loc) + val dk = ElabUtil.classifyDatatype xnts + val (st, n') = St.bindCon st x n + val (xnts, (ds', st, cmap, conmap)) = + ListUtil.foldlMap + (fn ((x', n, to), (ds', st, cmap, conmap)) => + let + val dt = (L'.CNamed n', loc) + val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs - val to = Option.map (corifyCon st) to + val to = Option.map (corifyCon st) to - val pc = L'.PConFfi {mod = m, - datatyp = x, - params = xs, - con = x', - arg = to, - kind = dk} + val pc = L'.PConFfi {mod = m, + datatyp = x, + params = xs, + con = x', + arg = to, + kind = dk} - fun wrapT t = - foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs - fun wrapE e = - foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs + fun wrapT t = + foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs + fun wrapE e = + foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs - val (cmap, d) = - case to of - NONE => (SM.insert (cmap, x', wrapT dt), - (L'.DVal (x', n, wrapT dt, - wrapE - (L'.ECon (dk, pc, args, NONE), - loc), - ""), loc)) - | SOME t => - let - val tf = (L'.TFun (t, dt), loc) - val e = wrapE (L'.EAbs ("x", t, tf, - (L'.ECon (dk, pc, args, - SOME (L'.ERel 0, - loc)), - loc)), loc) - val d = (L'.DVal (x', n, wrapT tf, - e, ""), loc) + val (cmap, d) = + case to of + NONE => (SM.insert (cmap, x', wrapT dt), + (L'.DVal (x', n, wrapT dt, + wrapE + (L'.ECon (dk, pc, args, NONE), + loc), + ""), loc)) + | SOME t => + let + val tf = (L'.TFun (t, dt), loc) + val e = wrapE (L'.EAbs ("x", t, tf, + (L'.ECon (dk, pc, args, + SOME (L'.ERel 0, + loc)), + loc)), loc) + val d = (L'.DVal (x', n, wrapT tf, + e, ""), loc) in (SM.insert (cmap, x', wrapT tf), d) end @@ -746,7 +772,7 @@ val st = St.bindStr st m n (St.ffi m cmap conmap) in - (rev ds, st) + (rev ds, St.basisIs (st, n)) end | _ => raise Fail "Non-const signature for FFI structure") @@ -766,30 +792,52 @@ ([], st)) | SOME (m, ms) => let + val basis_n = case St.lookupBasis st of + NONE => raise Fail "Corify: Don't know number of Basis" + | SOME n => n + fun wrapSgi ((sgi, _), (wds, eds)) = case sgi of L.SgiVal (s, _, t as (L.TFun (dom, ran), _)) => (case (#1 dom, #1 ran) of - (L.TRecord (L.CRecord (_, []), _), - L.CApp - ((L.CApp - ((L.CApp ((L.CModProj (_, [], "xml"), _), - (L.CRecord (_, [((L.CName "Html", _), - _)]), _)), _), _), _), _)) => + (L.TRecord _, + L.CApp ((L.CModProj (basis, [], "transaction"), _), + ran' as + (L.CApp + ((L.CApp + ((L.CApp ((L.CModProj (basis', [], "xml"), _), + (L.CRecord (_, [((L.CName "Html", _), + _)]), _)), _), _), + _), _), _))) => let val ran = (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc) + val ranT = (L.CApp ((L.CModProj (basis, [], "transaction"), loc), + ran), loc) val e = (L.EModProj (m, ms, s), loc) - val e = (L.EAbs ("vs", dom, ran, - (L.EWrite (L.EApp (e, (L.ERel 0, loc)), loc), loc)), loc) + + val ef = (L.EModProj (basis, [], "bind"), loc) + val ef = (L.ECApp (ef, ran'), loc) + val ef = (L.EApp (ef, (L.EApp (e, (L.ERel 0, loc)), loc)), loc) + + val eat = (L.CApp ((L.CModProj (basis, [], "transaction"), loc), + ran), loc) + val ea = (L.EAbs ("p", ran', eat, + (L.EWrite (L.ERel 0, loc), loc)), loc) + + val e = (L.EApp (ef, ea), loc) + val e = (L.EAbs ("vs", dom, ran, e), loc) in - ((L.DVal ("wrap_" ^ s, 0, - (L.TFun (dom, ran), loc), - e), loc) :: wds, - (fn st => - case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of - L'.ENamed n => (L'.DExport (L'.Link, n), loc) - | _ => raise Fail "Corify: Value to export didn't corify properly") - :: eds) + if basis = basis_n andalso basis' = basis_n then + ((L.DVal ("wrap_" ^ s, 0, + (L.TFun (dom, ranT), loc), + e), loc) :: wds, + (fn st => + case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of + L'.ENamed n => (L'.DExport (L'.Link, n), loc) + | _ => raise Fail "Corify: Value to export didn't corify properly") + :: eds) + else + (wds, eds) end | _ => (wds, eds)) | _ => (wds, eds) @@ -798,7 +846,7 @@ val wrapper = (L.StrConst wds, loc) val (ds, {inner, outer}) = corifyStr (wrapper, st) val st = St.bindStr outer "wrapper" en inner - + val ds = ds @ map (fn f => f st) eds in (ds, st) @@ -806,13 +854,13 @@ end | _ => raise Fail "Non-const signature for 'export'") - | L.DTable (_, x, n, c) => - let - val (st, n) = St.bindVal st x n - val s = x - in - ([(L'.DTable (x, n, corifyCon st c, s), loc)], st) - end + | L.DTable (_, x, n, c) => + let + val (st, n) = St.bindVal st x n + val s = x + in + ([(L'.DTable (x, n, corifyCon st c, s), loc)], st) + end and corifyStr ((str, _), st) = case str of @@ -865,7 +913,7 @@ | L.DFfiStr (_, n', _) => Int.max (n, n') | L.DExport _ => n | L.DTable (_, _, n', _) => Int.max (n, n')) - 0 ds + 0 ds and maxNameStr (str, _) = case str of
--- a/src/elaborate.sml Sun Aug 31 09:05:33 2008 -0400 +++ b/src/elaborate.sml Sun Aug 31 09:45:23 2008 -0400 @@ -3036,27 +3036,36 @@ ((L'.TFun (dom, ran), _), []) => (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of (((L'.TRecord domR, _), []), - ((L'.CApp (tf, arg3), _), [])) => - (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of - (((L'.CApp (tf, arg2), _), []), - (((L'.CRecord (_, []), _), []))) => - (case (hnormCon (env, denv) tf) of - ((L'.CApp (tf, arg1), _), []) => - (case (hnormCon (env, denv) tf, - hnormCon (env, denv) domR, - hnormCon (env, denv) arg1, - hnormCon (env, denv) arg2) of - ((tf, []), (domR, []), (arg1, []), - ((L'.CRecord (_, []), _), [])) => - let - val t = (L'.CApp (tf, arg1), loc) - val t = (L'.CApp (t, arg2), loc) - val t = (L'.CApp (t, arg3), loc) - in - (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), - t), - loc)), loc) - end + ((L'.CApp (tf, arg), _), [])) => + (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of + (((L'.CModProj (basis, [], "transaction"), _), []), + ((L'.CApp (tf, arg3), _), [])) => + (case (basis = !basis_r, + hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of + (true, + ((L'.CApp (tf, arg2), _), []), + (((L'.CRecord (_, []), _), []))) => + (case (hnormCon (env, denv) tf) of + ((L'.CApp (tf, arg1), _), []) => + (case (hnormCon (env, denv) tf, + hnormCon (env, denv) domR, + hnormCon (env, denv) arg1, + hnormCon (env, denv) arg2) of + ((tf, []), (domR, []), (arg1, []), + ((L'.CRecord (_, []), _), [])) => + let + val t = (L'.CApp (tf, arg1), loc) + val t = (L'.CApp (t, arg2), loc) + val t = (L'.CApp (t, arg3), loc) + val t = (L'.CApp ( + (L'.CModProj (basis, [], "transaction"), loc), + t), loc) + in + (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), + t), + loc)), loc) + end + | _ => all) | _ => all) | _ => all) | _ => all)
--- a/tests/query.ur Sun Aug 31 09:05:33 2008 -0400 +++ b/tests/query.ur Sun Aug 31 09:45:23 2008 -0400 @@ -9,8 +9,14 @@ (fn fs _ acc => return (Cons (fs.T1, acc))) Nil -val r2 : transaction int = +val r2 : transaction string = ls <- r1; return (case ls of - Nil => 0 - | Cons ({A = a, ...}, _) => a) + Nil => "Problem" + | Cons ({B = b, ...}, _) => b) + +val main : unit -> transaction page = fn () => + s <- r2; + return <html><body> + {cdata s} + </body></html>