summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/core.sml16
-rw-r--r--src/core_env.sig2
-rw-r--r--src/core_env.sml14
-rw-r--r--src/core_print.sml54
-rw-r--r--src/core_util.sml16
-rw-r--r--src/corify.sml141
-rw-r--r--src/monoize.sml4
7 files changed, 228 insertions, 19 deletions
diff --git a/src/core.sml b/src/core.sml
index b16766b3..5baa0351 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -59,10 +59,24 @@ datatype con' =
withtype con = con' located
+datatype patCon =
+ PConVar of int
+ | PConFfi of string * string
+
+datatype pat' =
+ PWild
+ | PVar of string
+ | PPrim of Prim.t
+ | PCon of patCon * pat option
+ | PRecord of (string * pat) list
+
+withtype pat = pat' located
+
datatype exp' =
EPrim of Prim.t
| ERel of int
| ENamed of int
+ | ECon of int * exp option
| EFfi of string * string
| EFfiApp of string * string * exp list
| EApp of exp * exp
@@ -75,6 +89,8 @@ datatype exp' =
| ECut of exp * con * { field : con, rest : con }
| EFold of kind
+ | ECase of exp * (pat * exp) list * con
+
| EWrite of exp
| EClosure of int * exp list
diff --git a/src/core_env.sig b/src/core_env.sig
index b2005fa8..220c1da8 100644
--- a/src/core_env.sig
+++ b/src/core_env.sig
@@ -45,6 +45,8 @@ signature CORE_ENV = sig
val pushDatatype : env -> string -> int -> (string * int * Core.con option) list -> env
val lookupDatatype : env -> int -> string * (string * int * Core.con option) list
+ val lookupConstructor : env -> int -> string * Core.con option * int
+
val pushERel : env -> string -> Core.con -> env
val lookupERel : env -> int -> string * Core.con
diff --git a/src/core_env.sml b/src/core_env.sml
index cb10a354..4895de9c 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -62,6 +62,7 @@ type env = {
namedC : (string * kind * con option) IM.map,
datatypes : (string * (string * int * con option) list) IM.map,
+ constructors : (string * con option * int) IM.map,
relE : (string * con) list,
namedE : (string * con * exp option * string) IM.map
@@ -72,6 +73,7 @@ val empty = {
namedC = IM.empty,
datatypes = IM.empty,
+ constructors = IM.empty,
relE = [],
namedE = IM.empty
@@ -82,6 +84,7 @@ fun pushCRel (env : env) x k =
namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
datatypes = #datatypes env,
+ constructors = #constructors env,
relE = map (fn (x, c) => (x, lift c)) (#relE env),
namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)}
@@ -95,6 +98,7 @@ fun pushCNamed (env : env) x n k co =
namedC = IM.insert (#namedC env, n, (x, k, co)),
datatypes = #datatypes env,
+ constructors = #constructors env,
relE = #relE env,
namedE = #namedE env}
@@ -109,6 +113,9 @@ fun pushDatatype (env : env) x n xncs =
namedC = #namedC env,
datatypes = IM.insert (#datatypes env, n, (x, xncs)),
+ constructors = foldl (fn ((x, n, to), constructors) =>
+ IM.insert (constructors, n, (x, to, n)))
+ (#constructors env) xncs,
relE = #relE env,
namedE = #namedE env}
@@ -118,11 +125,17 @@ fun lookupDatatype (env : env) n =
NONE => raise UnboundNamed n
| SOME x => x
+fun lookupConstructor (env : env) n =
+ case IM.find (#constructors env, n) of
+ NONE => raise UnboundNamed n
+ | SOME x => x
+
fun pushERel (env : env) x t =
{relC = #relC env,
namedC = #namedC env,
datatypes = #datatypes env,
+ constructors = #constructors env,
relE = (x, t) :: #relE env,
namedE = #namedE env}
@@ -136,6 +149,7 @@ fun pushENamed (env : env) x n t eo s =
namedC = #namedC env,
datatypes = #datatypes env,
+ constructors = #constructors env,
relE = #relE env,
namedE = IM.insert (#namedE env, n, (x, t, eo, s))}
diff --git a/src/core_print.sml b/src/core_print.sml
index 28080bfa..7458fef0 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -152,6 +152,43 @@ fun p_enamed env n =
string (#1 (E.lookupENamed env n)))
handle E.UnboundNamed _ => string ("UNBOUNDN_" ^ Int.toString n)
+fun p_con_named env n =
+ (if !debug then
+ string (#1 (E.lookupConstructor env n) ^ "__" ^ Int.toString n)
+ else
+ string (#1 (E.lookupConstructor env n)))
+ handle E.UnboundNamed _ => string ("CONSTRUCTOR_" ^ Int.toString n)
+
+fun p_patCon env pc =
+ case pc of
+ PConVar n => p_con_named env n
+ | PConFfi (m, x) => box [string "FFI(",
+ string m,
+ string ".",
+ string x,
+ string ")"]
+
+fun p_pat' par env (p, _) =
+ case p of
+ PWild => string "_"
+ | PVar s => string s
+ | PPrim p => Prim.p_t p
+ | PCon (n, NONE) => p_patCon env n
+ | PCon (n, SOME p) => parenIf par (box [p_patCon env n,
+ space,
+ p_pat' true env p])
+ | PRecord xps =>
+ box [string "{",
+ p_list_sep (box [string ",", space]) (fn (x, p) =>
+ box [string x,
+ space,
+ string "=",
+ space,
+ p_pat env p]) xps,
+ string "}"]
+
+and p_pat x = p_pat' false x
+
fun p_exp' par env (e, _) =
case e of
EPrim p => Prim.p_t p
@@ -162,6 +199,10 @@ fun p_exp' par env (e, _) =
string (#1 (E.lookupERel env n)))
handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n))
| ENamed n => p_enamed env n
+ | ECon (n, NONE) => p_con_named env n
+ | ECon (n, SOME e) => parenIf par (box [p_con_named env n,
+ space,
+ p_exp' true env e])
| EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"]
| EFfiApp (m, x, es) => box [string "FFI(",
string m,
@@ -249,6 +290,19 @@ fun p_exp' par env (e, _) =
p_con' true env c])
| EFold _ => string "fold"
+ | ECase (e, pes, _) => parenIf par (box [string "case",
+ space,
+ p_exp env e,
+ space,
+ string "of",
+ space,
+ p_list_sep (box [space, string "|", space])
+ (fn (p, e) => box [p_pat env p,
+ space,
+ string "=>",
+ space,
+ p_exp env e]) pes])
+
| EWrite e => box [string "write(",
p_exp env e,
string ")"]
diff --git a/src/core_util.sml b/src/core_util.sml
index 95c4f10f..85cf24ac 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -227,6 +227,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
EPrim _ => S.return2 eAll
| ERel _ => S.return2 eAll
| ENamed _ => S.return2 eAll
+ | ECon (_, NONE) => S.return2 eAll
+ | ECon (n, SOME e) =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (ECon (n, SOME e'), loc))
| EFfi _ => S.return2 eAll
| EFfiApp (m, x, es) =>
S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es,
@@ -297,6 +302,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
fn k' =>
(EFold k', loc))
+ | ECase (e, pes, t) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (ListUtil.mapfold (fn (p, e) =>
+ S.map2 (mfe ctx e,
+ fn e' => (p, e'))) pes,
+ fn pes' =>
+ S.map2 (mfc ctx t,
+ fn t' =>
+ (ECase (e', pes', t'), loc))))
+
| EWrite e =>
S.map2 (mfe ctx e,
fn e' =>
diff --git a/src/corify.sml b/src/corify.sml
index cf6d5658..44da20da 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -71,11 +71,15 @@ structure St : sig
val lookupConById : t -> int -> int option
val lookupConByName : t -> string -> core_con
+ val bindConstructor : t -> string -> int -> L'.patCon -> t
+ 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 bindConstructor : t -> string -> int -> t
+ val bindConstructorVal : t -> string -> int -> t
val lookupValById : t -> int -> int option
val lookupValByName : t -> string -> core_val
@@ -90,6 +94,7 @@ 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}
@@ -98,6 +103,7 @@ datatype flattening =
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,
@@ -107,15 +113,17 @@ type t = {
val empty = {
cons = IM.empty,
+ constructors = IM.empty,
vals = IM.empty,
strs = IM.empty,
funs = IM.empty,
- current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
+ current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
nested = []
}
-fun debug ({current = FNormal {cons, vals, strs, funs}, ...} : t) =
+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")
@@ -129,20 +137,22 @@ datatype core_val =
ENormal of int
| EFfi of string * L'.con
-fun bindCon {cons, vals, strs, funs, current, nested} s n =
+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, vals, strs, funs} =>
+ | 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,
@@ -161,20 +171,22 @@ fun lookupConByName ({current, ...} : t) x =
NONE => raise Fail "Corify.St.lookupConByName"
| SOME n => CNormal n
-fun bindVal {cons, vals, strs, funs, current, nested} s 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, vals, strs, funs} =>
+ | 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,
@@ -183,18 +195,20 @@ fun bindVal {cons, vals, strs, funs, current, nested} s n =
n')
end
-fun bindConstructor {cons, vals, strs, funs, current, nested} s n =
+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, vals, strs, funs} =>
+ | 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,
@@ -202,6 +216,7 @@ fun bindConstructor {cons, vals, strs, funs, current, nested} s n =
nested = nested}
end
+
fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
fun lookupValByName ({current, ...} : t) x =
@@ -215,26 +230,64 @@ fun lookupValByName ({current, ...} : t) x =
NONE => raise Fail "Corify.St.lookupValByName"
| SOME n => ENormal n
-fun enter {cons, vals, strs, funs, current, nested} =
+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
+
+fun lookupConstructorById ({constructors, ...} : t) n =
+ case IM.find (constructors, n) of
+ NONE => raise Fail "Corify.St.lookupConstructorById"
+ | SOME x => x
+
+fun lookupConstructorByName ({current, ...} : t) x =
+ case current of
+ FFfi {mod = m, ...} => L'.PConFfi (m, x)
+ | FNormal {constructors, ...} =>
+ case SM.find (constructors, x) of
+ NONE => raise Fail "Corify.St.lookupConstructorByName"
+ | 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, vals, strs, funs, current, nested = m1 :: rest} =
+fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
{outer = {cons = cons,
+ constructors = constructors,
vals = vals,
strs = strs,
funs = funs,
@@ -245,14 +298,17 @@ fun leave {cons, vals, strs, funs, current, nested = m1 :: rest} =
fun ffi m vals = dummy (FFfi {mod = m, vals = vals})
-fun bindStr ({cons, vals, strs, funs,
- current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
+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},
@@ -270,14 +326,17 @@ fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
| SOME f => dummy f)
| lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
-fun bindFunctor ({cons, vals, strs, funs,
- current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
+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))},
@@ -338,6 +397,25 @@ fun corifyCon st (c, loc) =
| L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
| L.CUnit => (L'.CUnit, 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 => (L'.PVar x, loc)
+ | L.PPrim p => (L'.PPrim p, loc)
+ | L.PCon (pc, po) => (L'.PCon (corifyPatCon st pc, Option.map (corifyPat st) po), loc)
+ | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, corifyPat st p)) xps), loc)
+
fun corifyExp st (e, loc) =
case e of
L.EPrim p => (L'.EPrim p, loc)
@@ -394,7 +472,12 @@ fun corifyExp st (e, 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 _ => raise Fail "Corify ECase"
+
+ | L.ECase (e, pes, t) => (L'.ECase (corifyExp st e,
+ map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
+ corifyCon st t),
+ loc)
+
| L.EWrite e => (L'.EWrite (corifyExp st e), loc)
fun corifyDecl ((d, loc : EM.span), st) =
@@ -410,27 +493,47 @@ fun corifyDecl ((d, loc : EM.span), st) =
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
+ 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 t = (L'.CNamed n, loc)
+ val dcons = map (fn (x, n, to) =>
+ let
+ val (e, t) =
+ case to of
+ NONE => ((L'.ECon (n, NONE), loc), t)
+ | SOME t' => ((L'.EAbs ("x", t', t,
+ (L'.ECon (n, SOME (L'.ERel 0, loc)), loc)),
+ loc),
+ (L'.TFun (t', t), loc))
+ in
+ (L'.DVal (x, n, t, e, ""), loc)
+ end) xncs
in
- ([(L'.DDatatype (x, n, xncs), loc)], st)
+ ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
end
| L.DDatatypeImp (x, n, m1, ms, s, 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 cds = map (fn (x, n, co) =>
let
val t = case co of
diff --git a/src/monoize.sml b/src/monoize.sml
index c8060937..50e705f2 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -171,6 +171,7 @@ fun monoExp (env, st) (all as (e, loc)) =
L.EPrim p => (L'.EPrim p, loc)
| L.ERel n => (L'.ERel n, loc)
| L.ENamed n => (L'.ENamed n, loc)
+ | L.ECon _ => raise Fail "Monoize ECon"
| L.EFfi mx => (L'.EFfi mx, loc)
| L.EFfiApp (m, x, es) => (L'.EFfiApp (m, x, map (monoExp (env, st)) es), loc)
@@ -448,6 +449,9 @@ fun monoExp (env, st) (all as (e, loc)) =
| L.EField (e, x, _) => (L'.EField (monoExp (env, st) e, monoName env x), loc)
| L.ECut _ => poly ()
| L.EFold _ => poly ()
+
+ | L.ECase _ => raise Fail "Monoize ECase"
+
| L.EWrite e => (L'.EWrite (monoExp (env, st) e), loc)
| L.EClosure (n, es) => (L'.EClosure (n, map (monoExp (env, st)) es), loc)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 19:56:33 +0000