Mercurial > urweb
changeset 192:9bbf4d383381
Parametrized datatypes through corify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 08 Aug 2008 10:59:06 -0400 |
| parents | aa54250f58ac |
| children | 8a70e2919e86 |
| files | src/core.sml src/core_env.sig src/core_env.sml src/core_print.sml src/core_util.sml src/corify.sml src/monoize.sml src/shake.sml |
| diffstat | 8 files changed, 131 insertions(+), 83 deletions(-) [+] |
line wrap: on
line diff
--- a/src/core.sml Fri Aug 08 10:28:32 2008 -0400 +++ b/src/core.sml Fri Aug 08 10:59:06 2008 -0400 @@ -63,13 +63,14 @@ datatype patCon = PConVar of int - | PConFfi of {mod : string, datatyp : string, con : string, arg : con option, kind : datatype_kind} + | PConFfi of {mod : string, datatyp : string, params : string list, + con : string, arg : con option, kind : datatype_kind} datatype pat' = PWild | PVar of string * con | PPrim of Prim.t - | PCon of datatype_kind * patCon * pat option + | PCon of datatype_kind * patCon * con list * pat option | PRecord of (string * pat * con) list withtype pat = pat' located @@ -78,7 +79,7 @@ EPrim of Prim.t | ERel of int | ENamed of int - | ECon of datatype_kind * patCon * exp option + | ECon of datatype_kind * patCon * con list * exp option | EFfi of string * string | EFfiApp of string * string * exp list | EApp of exp * exp @@ -105,7 +106,7 @@ datatype decl' = DCon of string * int * kind * con - | DDatatype of string * int * (string * int * con option) list + | DDatatype of string * int * string list * (string * int * con option) list | DVal of string * int * con * exp * string | DValRec of (string * int * con * exp * string) list | DExport of export_kind * int
--- a/src/core_env.sig Fri Aug 08 10:28:32 2008 -0400 +++ b/src/core_env.sig Fri Aug 08 10:59:06 2008 -0400 @@ -42,10 +42,10 @@ val pushCNamed : env -> string -> int -> Core.kind -> Core.con option -> env val lookupCNamed : env -> int -> string * Core.kind * Core.con option - val pushDatatype : env -> string -> int -> (string * int * Core.con option) list -> env - val lookupDatatype : env -> int -> string * (string * int * Core.con option) list + val pushDatatype : env -> string -> int -> string list -> (string * int * Core.con option) list -> env + val lookupDatatype : env -> int -> string * string list * (string * int * Core.con option) list - val lookupConstructor : env -> int -> string * Core.con option * int + val lookupConstructor : env -> int -> string * string list * Core.con option * int val pushERel : env -> string -> Core.con -> env val lookupERel : env -> int -> string * Core.con
--- a/src/core_env.sml Fri Aug 08 10:28:32 2008 -0400 +++ b/src/core_env.sml Fri Aug 08 10:59:06 2008 -0400 @@ -61,8 +61,8 @@ relC : (string * kind) list, namedC : (string * kind * con option) IM.map, - datatypes : (string * (string * int * con option) list) IM.map, - constructors : (string * con option * int) IM.map, + datatypes : (string * string list * (string * int * con option) list) IM.map, + constructors : (string * string list * con option * int) IM.map, relE : (string * con) list, namedE : (string * con * exp option * string) IM.map @@ -108,13 +108,13 @@ NONE => raise UnboundNamed n | SOME x => x -fun pushDatatype (env : env) x n xncs = +fun pushDatatype (env : env) x n xs xncs = {relC = #relC env, namedC = #namedC env, - datatypes = IM.insert (#datatypes env, n, (x, xncs)), + datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)), constructors = foldl (fn ((x, n', to), constructors) => - IM.insert (constructors, n', (x, to, n))) + IM.insert (constructors, n', (x, xs, to, n))) (#constructors env) xncs, relE = #relE env, @@ -162,9 +162,9 @@ fun declBinds env (d, loc) = case d of DCon (x, n, k, c) => pushCNamed env x n k (SOME c) - | DDatatype (x, n, xncs) => + | DDatatype (x, n, xs, xncs) => let - val env = pushDatatype env x n xncs + val env = pushDatatype env x n xs xncs val env = pushCNamed env x n (KType, loc) NONE in foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""
--- a/src/core_print.sml Fri Aug 08 10:28:32 2008 -0400 +++ b/src/core_print.sml Fri Aug 08 10:59:06 2008 -0400 @@ -173,10 +173,10 @@ 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]) + | 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, _) => @@ -199,10 +199,10 @@ string (#1 (E.lookupERel env n))) handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n)) | ENamed n => p_enamed env n - | ECon (_, pc, NONE) => p_patCon env pc - | ECon (_, pc, SOME e) => parenIf par (box [p_patCon env pc, - space, - p_exp' true env e]) + | ECon (_, pc, _, NONE) => p_patCon env pc + | ECon (_, pc, _, SOME e) => parenIf par (box [p_patCon env pc, + 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, @@ -344,13 +344,16 @@ Link => string "link" | Action => string "action" -fun p_datatype env (x, n, cons) = +fun p_datatype env (x, n, xs, cons) = let + val k = (KType, ErrorMsg.dummySpan) val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE + val env = foldl (fn (x, env) => E.pushCRel env x k) env xs in box [string "datatype", space, string x, + p_list_sep (box []) (fn x => box [space, string x]) xs, space, string "=", space,
--- a/src/core_util.sml Fri Aug 08 10:28:32 2008 -0400 +++ b/src/core_util.sml Fri Aug 08 10:59:06 2008 -0400 @@ -233,14 +233,19 @@ EPrim _ => S.return2 eAll | ERel _ => S.return2 eAll | ENamed _ => S.return2 eAll - | ECon (_, _, NONE) => S.return2 eAll - | ECon (dk, n, SOME e) => - S.map2 (mfe ctx e, - fn e' => - (ECon (dk, n, SOME e'), loc)) + | ECon (dk, pc, cs, NONE) => + S.map2 (ListUtil.mapfold (mfc ctx) cs, + fn cs' => + (ECon (dk, pc, cs', NONE), loc)) + | ECon (dk, n, cs, SOME e) => + S.bind2 (mfe ctx e, + fn e' => + S.map2 (ListUtil.mapfold (mfc ctx) cs, + fn cs' => + (ECon (dk, n, cs', SOME e'), loc))) | EFfi _ => S.return2 eAll | EFfiApp (m, x, es) => - S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es, + S.map2 (ListUtil.mapfold (mfe ctx) es, fn es' => (EFfiApp (m, x, es'), loc)) | EApp (e1, e2) => @@ -414,7 +419,7 @@ S.map2 (mfc ctx c, fn c' => (DCon (x, n, k', c'), loc))) - | DDatatype (x, n, xncs) => + | DDatatype (x, n, xs, xncs) => S.map2 (ListUtil.mapfold (fn (x, n, c) => case c of NONE => S.return2 (x, n, c) @@ -422,7 +427,7 @@ S.map2 (mfc ctx c, fn c' => (x, n, SOME c'))) xncs, fn xncs' => - (DDatatype (x, n, xncs'), loc)) + (DDatatype (x, n, xs, xncs'), loc)) | DVal vi => S.map2 (mfvi ctx vi, fn vi' => @@ -491,16 +496,24 @@ val ctx' = case #1 d' of DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c)) - | DDatatype (x, n, xncs) => + | DDatatype (x, n, xs, xncs) => let - val ctx = bind (ctx, NamedC (x, n, (KType, #2 d'), NONE)) + val loc = #2 d' + val k = (KType, loc) + val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs + + val ctx = bind (ctx, NamedC (x, n, k', NONE)) val t = (CNamed n, #2 d') + val t = ListUtil.foldli (fn (i, _, t) => (CApp (t, (CRel i, loc)), loc)) + t xs in foldl (fn ((x, n, to), ctx) => let val t = case to of NONE => t | SOME t' => (TFun (t', t), #2 d') + val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) + t xs in bind (ctx, NamedE (x, n, t, NONE, "")) end) @@ -555,7 +568,7 @@ val maxName = foldl (fn ((d, _) : decl, count) => case d of DCon (_, n, _, _) => Int.max (n, count) - | DDatatype (_, n, _) => Int.max (n, count) + | DDatatype (_, n, _, _) => Int.max (n, count) | DVal (_, n, _, _, _) => Int.max (n, count) | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis | DExport _ => count) 0
--- a/src/corify.sml Fri Aug 08 10:28:32 2008 -0400 +++ b/src/corify.sml Fri Aug 08 10:59:06 2008 -0400 @@ -62,7 +62,7 @@ val enter : t -> t val leave : t -> {outer : t, inner : t} - val ffi : string -> L'.con SM.map -> (string * L'.con option * L'.datatype_kind) SM.map -> t + val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t datatype core_con = CNormal of int @@ -101,7 +101,7 @@ funs : (string * int * L.str) SM.map} | FFfi of {mod : string, vals : L'.con SM.map, - constructors : (string * L'.con option * L'.datatype_kind) SM.map} + constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map} type t = { cons : int IM.map, @@ -263,7 +263,7 @@ FFfi {mod = m, constructors, ...} => (case SM.find (constructors, x) of NONE => NONE - | SOME (n, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk})) + | 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 @@ -274,7 +274,7 @@ FFfi {mod = m, constructors, ...} => (case SM.find (constructors, x) of NONE => raise Fail "Corify.St.lookupConstructorByName [1]" - | SOME (n, to, dk) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk}) + | 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]" @@ -429,7 +429,8 @@ 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) => raise Fail "Corify PCon" (*(L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), 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) = @@ -446,11 +447,18 @@ val st = foldl St.lookupStrByName st ms in case St.lookupConstructorByNameOpt st x of - SOME (pc as L'.PConFfi {mod = m, datatyp, arg, kind, ...}) => - (case arg of - NONE => (L'.ECon (kind, pc, NONE), loc) - | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), - (L'.ECon (kind, pc, SOME (L'.ERel 0, loc)), loc)), loc)) + 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) @@ -512,8 +520,8 @@ in ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) end - | L.DDatatype (x, n, xs, xncs) => raise Fail "Corify DDatatype" - (*let + | 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 @@ -526,24 +534,31 @@ val dk = CoreUtil.classifyDatatype xncs val t = (L'.CNamed n, loc) + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel 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 n, loc)) xs val (e, t) = case to of - NONE => ((L'.ECon (dk, L'.PConVar n, NONE), loc), t) + NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) | SOME t' => ((L'.EAbs ("x", t', t, - (L'.ECon (dk, L'.PConVar n, SOME (L'.ERel 0, loc)), + (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, xncs), loc) :: dcons, st) - end*) - | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => raise Fail "Corify DDatatypeImp" - (*let + ((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) @@ -560,18 +575,24 @@ ((x, n, co), st) end) st xncs + val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel 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, (L'.KType, loc), c), loc) :: cds, st) - end*) + ((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 @@ -648,8 +669,9 @@ st) end - | L.SgiDatatype (x, n, xs, xnts) => raise Fail "Corify FFI SgiDatatype" - (*let + | L.SgiDatatype (x, n, xs, xnts) => + let + val k = (L'.KType, loc) val dk = ExplUtil.classifyDatatype xnts val (st, n') = St.bindCon st x n val (xnts, (ds', st, cmap, conmap)) = @@ -657,48 +679,57 @@ (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', dt), - (L'.DVal (x', n, dt, - (L'.ECon (dk, pc, NONE), loc), + 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 d = (L'.DVal (x', n, tf, - (L'.EAbs ("x", t, tf, - (L'.ECon (dk, pc, - SOME (L'.ERel 0, - loc)), - loc)), loc), ""), 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', tf), d) + (SM.insert (cmap, x', wrapT tf), d) end val st = St.bindConstructor st x' n pc - (*val st = St.bindConstructorVal st x' n*) - val conmap = SM.insert (conmap, x', (x, to, dk)) + val conmap = SM.insert (conmap, x', (x, xs, to, dk)) in ((x', n, to), (d :: ds', st, cmap, conmap)) end) ([], st, cmap, conmap) xnts in - (ds' @ (L'.DDatatype (x, n', xnts), loc) :: ds, + (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds, cmap, conmap, st) - end*) + end | L.SgiVal (x, _, c) => (ds,
--- a/src/monoize.sml Fri Aug 08 10:28:32 2008 -0400 +++ b/src/monoize.sml Fri Aug 08 10:59:06 2008 -0400 @@ -67,14 +67,14 @@ (L'.TFfi ("Basis", "string"), loc) | L.CRel _ => poly () - | L.CNamed n => - let + | L.CNamed n => raise Fail "Monoize CNamed" + (*let val (_, xncs) = Env.lookupDatatype env n val xncs = map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs in (L'.TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc) - end + end*) | L.CFfi mx => (L'.TFfi mx, loc) | L.CApp _ => poly () | L.CAbs _ => poly () @@ -206,7 +206,7 @@ let fun makeDecl n fm = let - val (x, xncs) = Env.lookupDatatype env i + val (x, xncs) = raise Fail "Monoize TDataype" (*Env.lookupDatatype env i*) val (branches, fm) = ListUtil.foldlMap @@ -297,7 +297,7 @@ L.PWild => (L'.PWild, loc) | L.PVar (x, t) => (L'.PVar (x, monoType env t), loc) | L.PPrim p => (L'.PPrim p, loc) - | L.PCon (dk, pc, po) => (L'.PCon (dk, monoPatCon env pc, Option.map (monoPat env) po), loc) + | L.PCon (dk, pc, _, po) => raise Fail "Monoize PCon" (*(L'.PCon (dk, monoPatCon env pc, Option.map (monoPat env) po), loc)*) | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, monoPat env p, monoType env t)) xps), loc) fun monoExp (env, st, fm) (all as (e, loc)) = @@ -311,8 +311,8 @@ L.EPrim p => ((L'.EPrim p, loc), fm) | L.ERel n => ((L'.ERel n, loc), fm) | L.ENamed n => ((L'.ENamed n, loc), fm) - | L.ECon (dk, pc, eo) => - let + | L.ECon (dk, pc, _, eo) => raise Fail "Monoize ECon" + (*let val (eo, fm) = case eo of NONE => (NONE, fm) @@ -324,7 +324,7 @@ end in ((L'.ECon (dk, monoPatCon env pc, eo), loc), fm) - end + end*) | L.EFfi mx => ((L'.EFfi mx, loc), fm) | L.EFfiApp (m, x, es) => let @@ -718,12 +718,12 @@ in case d of L.DCon _ => NONE - | L.DDatatype (x, n, xncs) => - let + | L.DDatatype (x, n, _, xncs) => raise Fail "Monoize DDatatype" + (*let val d = (L'.DDatatype (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs), loc) in SOME (Env.declBinds env all, fm, d) - end + end*) | L.DVal (x, n, t, e, s) => let val (e, fm) = monoExp (env, St.empty, fm) e
--- a/src/shake.sml Fri Aug 08 10:28:32 2008 -0400 +++ b/src/shake.sml Fri Aug 08 10:59:06 2008 -0400 @@ -48,7 +48,7 @@ | (_, page_es) => page_es) [] file val (cdef, edef) = foldl (fn ((DCon (_, n, _, c), _), (cdef, edef)) => (IM.insert (cdef, n, [c]), edef) - | ((DDatatype (_, n, xncs), _), (cdef, edef)) => + | ((DDatatype (_, n, _, xncs), _), (cdef, edef)) => (IM.insert (cdef, n, List.mapPartial #3 xncs), edef) | ((DVal (_, n, t, e, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, (t, e))) | ((DValRec vis, _), (cdef, edef)) => @@ -102,7 +102,7 @@ | SOME (t, e) => shakeExp (shakeCon s t) e) s page_es in List.filter (fn (DCon (_, n, _, _), _) => IS.member (#con s, n) - | (DDatatype (_, n, _), _) => IS.member (#con s, n) + | (DDatatype (_, n, _, _), _) => IS.member (#con s, n) | (DVal (_, n, _, _, _), _) => IS.member (#exp s, n) | (DValRec vis, _) => List.exists (fn (_, n, _, _, _) => IS.member (#exp s, n)) vis | (DExport _, _) => true) file