# HG changeset patch # User Adam Chlipala # Date 1213912536 14400 # Node ID 44a1bc863f0fb125878669ef40cb5425d4cfc935 # Parent 3c1ce1b4eb3ddb3efe91f6e4e14954ed3fd90dce Corifying functors diff -r 3c1ce1b4eb3d -r 44a1bc863f0f src/corify.sml --- a/src/corify.sml Thu Jun 19 17:11:24 2008 -0400 +++ b/src/corify.sml Thu Jun 19 17:55:36 2008 -0400 @@ -68,16 +68,22 @@ val bindStr : t -> string -> int -> t -> t val lookupStrById : t -> int -> t val lookupStrByName : string * t -> t + + val bindFunctor : t -> string -> int -> int -> L.str -> t + val lookupFunctorById : t -> int -> int * L.str + val lookupFunctorByName : string * t -> int * L.str end = struct datatype flattening = F of { core : int SM.map, - strs : flattening SM.map + strs : flattening SM.map, + funs : (int * L.str) SM.map } type t = { core : int IM.map, strs : flattening IM.map, + funs : (int * L.str) IM.map, current : flattening, nested : flattening list } @@ -85,24 +91,27 @@ val empty = { core = IM.empty, strs = IM.empty, - current = F { core = SM.empty, strs = SM.empty }, + funs = IM.empty, + current = F { core = SM.empty, strs = SM.empty, funs = SM.empty }, nested = [] } -fun bindCore {core, strs, current, nested} s n = +fun bindCore {core, strs, funs, current, nested} s n = let val n' = alloc () val current = let - val F {core, strs} = current + val F {core, strs, funs} = current in F {core = SM.insert (core, s, n'), - strs = strs} + strs = strs, + funs = funs} end in ({core = IM.insert (core, n, n'), strs = strs, + funs = funs, current = current, nested = nested}, n') @@ -115,36 +124,43 @@ NONE => raise Fail "Corify.St.lookupCoreByName" | SOME n => n -fun enter {core, strs, current, nested} = +fun enter {core, strs, funs, current, nested} = {core = core, strs = strs, + funs = funs, current = F {core = SM.empty, - strs = SM.empty}, + strs = SM.empty, + funs = SM.empty}, nested = current :: nested} fun dummy f = {core = IM.empty, strs = IM.empty, + funs = IM.empty, current = f, nested = []} -fun leave {core, strs, current, nested = m1 :: rest} = +fun leave {core, strs, funs, current, nested = m1 :: rest} = {outer = {core = core, strs = strs, + funs = funs, current = m1, nested = rest}, inner = dummy current} | leave _ = raise Fail "Corify.St.leave" -fun bindStr ({core, strs, current = F {core = mcore, strs = mstrs}, nested} : t) x n ({current = f, ...} : t) = +fun bindStr ({core, strs, funs, current = F {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) + x n ({current = f, ...} : t) = {core = core, strs = IM.insert (strs, n, f), + funs = funs, current = F {core = mcore, - strs = SM.insert (mstrs, x, f)}, + strs = SM.insert (mstrs, x, f), + funs = mfuns}, nested = nested} fun lookupStrById ({strs, ...} : t) n = case IM.find (strs, n) of - NONE => raise Fail "Corify.St.lookupStr" + NONE => raise Fail "Corify.St.lookupStrById" | SOME f => dummy f fun lookupStrByName (m, {current = F {strs, ...}, ...} : t) = @@ -152,6 +168,26 @@ NONE => raise Fail "Corify.St.lookupStrByName" | SOME f => dummy f +fun bindFunctor ({core, strs, funs, current = F {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) + x n na str = + {core = core, + strs = strs, + funs = IM.insert (funs, n, (na, str)), + current = F {core = mcore, + strs = mstrs, + funs = SM.insert (mfuns, x, (na, str))}, + nested = nested} + +fun lookupFunctorById ({funs, ...} : t) n = + case IM.find (funs, n) of + NONE => raise Fail "Corify.St.lookupFunctorById" + | SOME v => v + +fun lookupFunctorByName (m, {current = F {funs, ...}, ...} : t) = + case SM.find (funs, m) of + NONE => raise Fail "Corify.St.lookupFunctorByName" + | SOME v => v + end @@ -233,6 +269,9 @@ | L.DSgn _ => ([], st) + | L.DStr (x, n, _, (L.StrFun (_, na, _, _, str), _)) => + ([], St.bindFunctor st x n na str) + | L.DStr (x, n, _, str) => let val (ds, {inner, outer}) = corifyStr (str, st) @@ -257,8 +296,28 @@ in (ds, {inner = St.lookupStrByName (x, inner), outer = outer}) end - | L.StrFun _ => raise Fail "Corify functor" - | L.StrApp _ => raise Fail "Corify functor app" + | L.StrFun _ => raise Fail "Corify of nested functor definition" + | L.StrApp (str1, str2) => + let + fun unwind' (str, _) = + case str of + L.StrVar n => St.lookupStrById st n + | L.StrProj (str, x) => St.lookupStrByName (x, unwind' str) + | _ => raise Fail "Corify of fancy functor application [1]" + + fun unwind (str, _) = + case str of + L.StrVar n => St.lookupFunctorById st n + | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str) + | _ => raise Fail "Corify of fancy functor application [2]" + + val (na, body) = unwind str1 + + val (ds1, {inner, outer}) = corifyStr (str2, st) + val (ds2, sts) = corifyStr (body, St.bindStr outer "ARG" na inner) + in + (ds1 @ ds2, sts) + end fun maxName ds = foldl (fn ((d, _), n) => case d of diff -r 3c1ce1b4eb3d -r 44a1bc863f0f src/elaborate.sml --- a/src/elaborate.sml Thu Jun 19 17:11:24 2008 -0400 +++ b/src/elaborate.sml Thu Jun 19 17:55:36 2008 -0400 @@ -1015,6 +1015,7 @@ datatype str_error = UnboundStr of ErrorMsg.span * string | NotFunctor of L'.sgn + | FunctorRebind of ErrorMsg.span fun strError env err = case err of @@ -1023,6 +1024,8 @@ | NotFunctor sgn => (ErrorMsg.errorAt (#2 sgn) "Application of non-functor"; eprefaces' [("Signature", p_sgn env sgn)]) + | FunctorRebind loc => + ErrorMsg.errorAt loc "Attempt to rebind functor" val hnormSgn = E.hnormSgn @@ -1391,6 +1394,13 @@ val (env', n) = E.pushStrNamed env x sgn' in + case #1 (hnormSgn env sgn') of + L'.SgnFun _ => + (case #1 str' of + L'.StrFun _ => () + | _ => strError env (FunctorRebind loc)) + | _ => (); + ((L'.DStr (x, n, sgn', str'), loc), env') end end diff -r 3c1ce1b4eb3d -r 44a1bc863f0f tests/functor.lac --- a/tests/functor.lac Thu Jun 19 17:11:24 2008 -0400 +++ b/tests/functor.lac Thu Jun 19 17:55:36 2008 -0400 @@ -14,11 +14,6 @@ val three = M.s (M.s (M.s M.z)) end -structure F2 : functor (M : S) : T where type t = M.t = F -structure F3 : functor (M : S) : T = F -(*structure F4 : functor (M : S) : sig type q end = F*) -(*structure F5 : functor (M : S) : T where type t = int = F*) - structure O = F (struct type t = int