summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/corify.sml1366
-rw-r--r--src/elaborate.sml51
-rw-r--r--tests/query.ur12
3 files changed, 746 insertions, 683 deletions
diff --git a/src/corify.sml b/src/corify.sml
index b20a1136..c03fcf3a 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -64,6 +64,9 @@ structure St : sig
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 @@ structure St : sig
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
-
- 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
-
- 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 = {
- 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 = {
- 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"
-
- datatype core_con =
- CNormal of int
- | CFfi of string
-
- datatype core_val =
- ENormal of int
- | EFfi of string * L'.con
-
- fun bindCon {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 = 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 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,
+
+ 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 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}
+
+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
+}
+
+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 = []
+}
+
+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}
+
+fun lookupBasis ({basis, ...} : t) = basis
+
+datatype core_con =
+ CNormal of int
+ | CFfi of string
+
+datatype core_val =
+ ENormal of int
+ | EFfi of string * L'.con
+
+fun bindCon {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 = 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),
+ vals = vals,
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,
+ nested = nested},
+ n')
+ end
+
+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 {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}
- 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, 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
+ 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
-
- 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 dummy f = {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 ffi m vals constructors = dummy (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 lookupStrById ({strs, ...} : t) n =
- case IM.find (strs, n) of
- NONE => raise Fail "Corify.St.lookupStrById"
- | SOME f => dummy 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 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 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"
-
- 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 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.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.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)
-
- 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 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 (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)
-
- | 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.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
-
- 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 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 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 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)
-
- | 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.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, _) =>
+ | 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 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 (b, f) = {basis = b,
+ cons = IM.empty,
+ constructors = IM.empty,
+ vals = IM.empty,
+ strs = IM.empty,
+ funs = IM.empty,
+ current = f,
+ nested = []}
+
+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 (NONE, FFfi {mod = m, vals = vals, constructors = constructors})
+
+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 ({basis, strs, ...} : t) n =
+ case IM.find (strs, n) of
+ NONE => raise Fail "Corify.St.lookupStrById"
+ | SOME f => dummy (basis, f)
+
+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 ({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 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
+
+
+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)
+
+ | 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.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.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 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)
+
+ 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 (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.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)
+
+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 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 (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 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.bindCon st x n
+ val (st, n) = St.bindVal st x n
in
- ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
- cmap,
- conmap,
- st)
- end
+ ((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)
- | 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 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
-
- 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)
+ | 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.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
+
+ val to = Option.map (corifyCon st) to
+
+ 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
+
+ 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 @@ structure St : sig
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 @@ structure St : sig
([], 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 @@ structure St : sig
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 @@ structure St : sig
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 @@ fun maxName ds = foldl (fn ((d, _), n) =>
| 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
diff --git a/src/elaborate.sml b/src/elaborate.sml
index b86514e7..206c58cd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3036,27 +3036,36 @@ fun elabDecl ((d, loc), (env, denv, gs : constraint list)) =
((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)
diff --git a/tests/query.ur b/tests/query.ur
index 2caf0412..1039e40a 100644
--- a/tests/query.ur
+++ b/tests/query.ur
@@ -9,8 +9,14 @@ val r1 : transaction (list {A : int, B : string, C : float}) =
(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>
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 03:27:19 +0000