From f946d43f10e2f78d179db30c3c9ae8dcc10f3c10 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 3 Aug 2008 18:53:20 -0400 Subject: bool in Basis --- src/corify.sml | 131 +++++++++++++++++++++++++++++++++++---------------------- 1 file changed, 81 insertions(+), 50 deletions(-) (limited to 'src/corify.sml') diff --git a/src/corify.sml b/src/corify.sml index 81c32f40..146868e6 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -62,7 +62,7 @@ structure St : sig val enter : t -> t val leave : t -> {outer : t, inner : t} - val ffi : string -> L'.con SM.map -> string SM.map -> t + val ffi : string -> L'.con SM.map -> (string * L'.con option) SM.map -> t datatype core_con = CNormal of int @@ -72,6 +72,7 @@ structure St : sig val lookupConByName : t -> string -> core_con val bindConstructor : t -> string -> int -> L'.patCon -> t + val lookupConstructorByNameOpt : t -> string -> L'.patCon option val lookupConstructorByName : t -> string -> L'.patCon val lookupConstructorById : t -> int -> L'.patCon @@ -100,7 +101,7 @@ datatype flattening = funs : (string * int * L.str) SM.map} | FFfi of {mod : string, vals : L'.con SM.map, - constructors : string SM.map} + constructors : (string * L'.con option) SM.map} type t = { cons : int IM.map, @@ -257,12 +258,23 @@ fun lookupConstructorById ({constructors, ...} : t) n = 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, to) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to})) + | 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 => L'.PConFfi {mod = m, datatyp = n, con = x}) + | SOME (n, to) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to}) | FNormal {constructors, ...} => case SM.find (constructors, x) of NONE => raise Fail "Corify.St.lookupConstructorByName [2]" @@ -433,36 +445,43 @@ fun corifyExp st (e, loc) = val st = St.lookupStrById st m val st = foldl St.lookupStrByName st ms in - 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) + case St.lookupConstructorByNameOpt st x of + SOME (pc as L'.PConFfi {mod = m, datatyp, arg, ...}) => + (case arg of + NONE => (L'.ECon (pc, NONE), loc) + | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), + (L'.ECon (pc, SOME (L'.ERel 0, loc)), loc)), loc)) + | _ => + 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) @@ -630,36 +649,48 @@ fun corifyDecl ((d, loc : EM.span), st) = | L.SgiDatatype (x, n, xnts) => let val (st, n') = St.bindCon st x n - val (xnts, (st, cmap, conmap)) = + val (xnts, (ds', st, cmap, conmap)) = ListUtil.foldlMap - (fn ((x', n, to), (st, cmap, conmap)) => + (fn ((x', n, to), (ds', st, cmap, conmap)) => let - val st = St.bindConstructor st x' n - (L'.PConFfi {mod = m, - datatyp = x, - con = x'}) - val st = St.bindConstructorVal st x' n - val dt = (L'.CNamed n', loc) - val (to, cmap) = + val to = Option.map (corifyCon st) to + + val pc = L'.PConFfi {mod = m, + datatyp = x, + con = x', + arg = to} + + val (cmap, d) = case to of - NONE => (NONE, SM.insert (cmap, x', dt)) + NONE => (SM.insert (cmap, x', dt), + (L'.DVal (x', n, dt, + (L'.ECon (pc, NONE), loc), + ""), loc)) | SOME t => let - val t = corifyCon st t + val tf = (L'.TFun (t, dt), loc) + val d = (L'.DVal (x', n, tf, + (L'.EAbs ("x", t, tf, + (L'.ECon (pc, + SOME (L'.ERel 0, + loc)), + loc)), loc), ""), loc) in - (SOME t, SM.insert (cmap, x', - (L'.TFun (t, dt), loc))) + (SM.insert (cmap, x', tf), d) end - val conmap = SM.insert (conmap, x', x) + val st = St.bindConstructor st x' n pc + (*val st = St.bindConstructorVal st x' n*) + + val conmap = SM.insert (conmap, x', (x, to)) in ((x', n, to), - (st, cmap, conmap)) - end) (st, cmap, conmap) xnts + (d :: ds', st, cmap, conmap)) + end) ([], st, cmap, conmap) xnts in - ((L'.DDatatype (x, n', xnts), loc) :: ds, + (ds' @ (L'.DDatatype (x, n', xnts), loc) :: ds, cmap, conmap, st) -- cgit v1.2.3