summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/corify.sml41
-rw-r--r--src/elaborate.sml69
-rw-r--r--src/expl_print.sml26
3 files changed, 80 insertions, 56 deletions
diff --git a/src/corify.sml b/src/corify.sml
index d1b44384..0b0e9787 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -58,6 +58,8 @@ structure St : sig
val empty : t
+ val debug : t -> unit
+
val enter : t -> t
val leave : t -> {outer : t, inner : t}
val ffi : string -> L'.con SM.map -> t
@@ -80,16 +82,16 @@ structure St : sig
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
+ 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,
vals : int SM.map,
strs : flattening SM.map,
- funs : (int * L.str) SM.map}
+ funs : (string * int * L.str) SM.map}
| FFfi of {mod : string,
vals : L'.con SM.map}
@@ -97,7 +99,7 @@ type t = {
cons : int IM.map,
vals : int IM.map,
strs : flattening IM.map,
- funs : (int * L.str) IM.map,
+ funs : (string * int * L.str) IM.map,
current : flattening,
nested : flattening list
}
@@ -111,6 +113,13 @@ val empty = {
nested = []
}
+fun debug ({current = FNormal {cons, vals, strs, funs}, ...} : t) =
+ print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
+ ^ "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
@@ -243,17 +252,17 @@ fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
fun bindFunctor ({cons, vals, strs, funs,
current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
- x n na str =
+ x n xa na str =
{cons = cons,
vals = vals,
strs = strs,
- funs = IM.insert (funs, n, (na, str)),
+ funs = IM.insert (funs, n, (xa, na, str)),
current = FNormal {cons = mcons,
vals = mvals,
strs = mstrs,
- funs = SM.insert (mfuns, x, (na, str))},
+ funs = SM.insert (mfuns, x, (xa, na, str))},
nested = nested}
- | bindFunctor _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
+ | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
fun lookupFunctorById ({funs, ...} : t) n =
case IM.find (funs, n) of
@@ -412,8 +421,8 @@ fun corifyDecl ((d, loc : EM.span), st) =
end
| L.DSgn _ => ([], st)
- | L.DStr (x, n, _, (L.StrFun (_, na, _, _, str), _)) =>
- ([], St.bindFunctor st x n na str)
+ | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
+ ([], St.bindFunctor st x n xa na str)
| L.DStr (x, n, _, str) =>
let
@@ -514,7 +523,6 @@ fun corifyDecl ((d, loc : EM.span), st) =
end
end
| _ => raise Fail "Non-const signature for 'export'")
-
and corifyStr ((str, _), st) =
case str of
@@ -547,12 +555,12 @@ and corifyStr ((str, _), st) =
| L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
| _ => raise Fail "Corify of fancy functor application [2]"
- val (na, body) = unwind str1
+ val (xa, na, body) = unwind str1
- val (ds1, {inner, outer}) = corifyStr (str2, st)
- val (ds2, sts) = corifyStr (body, St.bindStr outer "ARG" na inner)
+ val (ds1, {inner = inner', outer}) = corifyStr (str2, st)
+ val (ds2, {inner, outer}) = corifyStr (body, St.bindStr outer xa na inner')
in
- (ds1 @ ds2, sts)
+ (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer})
end
fun maxName ds = foldl (fn ((d, _), n) =>
@@ -577,6 +585,7 @@ and maxNameStr (str, _) =
fun corify ds =
let
val () = reset (maxName ds + 1)
+
val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds
in
ds
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a36a0224..b5794ecd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1988,41 +1988,42 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
case #1 (hnormSgn env sgn) of
L'.SgnConst sgis =>
let
- fun doOne (all as (sgi, _)) =
- case sgi of
- L'.SgiVal (x, n, t) =>
- (case hnormCon (env, denv) t of
- ((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) arg2) of
- ((tf, []), (domR, []),
- ((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
- | _ => all)
- | _ => all)
- | _ => all)
- | _ => all)
- | _ => all)
- | _ => all
+ fun doOne (all as (sgi, _), env) =
+ (case sgi of
+ L'.SgiVal (x, n, t) =>
+ (case hnormCon (env, denv) t of
+ ((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) arg2) of
+ ((tf, []), (domR, []),
+ ((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
+ | _ => all)
+ | _ => all)
+ | _ => all)
+ | _ => all)
+ | _ => all)
+ | _ => all,
+ E.sgiBinds env all)
in
- (L'.SgnConst (map doOne sgis), loc)
+ (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
end
| _ => sgn
in
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 095a6e24..2c4e7c89 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -100,7 +100,7 @@ fun p_con' par env (c, _) =
else
m1x
in
- p_list_sep (string ".") string (m1x :: ms @ [x])
+ p_list_sep (string ".") string (m1s :: ms @ [x])
end
| CApp (c1, c2) => parenIf par (box [p_con env c1,
@@ -155,7 +155,7 @@ and p_name env (all as (c, _)) =
CName s => string s
| _ => p_con env all
-fun p_exp' par env (e, _) =
+fun p_exp' par env (e, loc) =
case e of
EPrim p => Prim.p_t p
| ERel n =>
@@ -171,13 +171,14 @@ fun p_exp' par env (e, _) =
| EModProj (m1, ms, x) =>
let
val (m1x, sgn) = E.lookupStrNamed env m1
+ handle E.UnboundNamed _ => ("UNBOUND", (SgnConst [], loc))
val m1s = if !debug then
m1x ^ "__" ^ Int.toString m1
else
m1x
in
- p_list_sep (string ".") string (m1x :: ms @ [x])
+ p_list_sep (string ".") string (m1s :: ms @ [x])
end
| EApp (e1, e2) => parenIf par (box [p_exp env e1,
@@ -294,7 +295,7 @@ fun p_sgn_item env (sgi, _) =
space,
p_sgn env sgn]
-and p_sgn env (sgn, _) =
+and p_sgn env (sgn, loc) =
case sgn of
SgnConst sgis => box [string "sig",
newline,
@@ -308,7 +309,8 @@ and p_sgn env (sgn, _) =
end,
newline,
string "end"]
- | SgnVar n => string (#1 (E.lookupSgnNamed env n))
+ | SgnVar n => string ((#1 (E.lookupSgnNamed env n))
+ handle E.UnboundNamed _ => "UNBOUND")
| SgnFun (x, n, sgn, sgn') => box [string "functor",
space,
string "(",
@@ -336,6 +338,7 @@ and p_sgn env (sgn, _) =
| SgnProj (m1, ms, x) =>
let
val (m1x, sgn) = E.lookupStrNamed env m1
+ handle E.UnboundNamed _ => ("UNBOUND", (SgnConst [], loc))
val m1s = if !debug then
m1x ^ "__" ^ Int.toString m1
@@ -424,7 +427,18 @@ and p_str env (str, _) =
p_file env ds,
newline,
string "end"]
- | StrVar n => string (#1 (E.lookupStrNamed env n))
+ | StrVar n =>
+ let
+ val x = #1 (E.lookupStrNamed env n)
+ handle E.UnboundNamed _ => "UNBOUND"
+
+ val s = if !debug then
+ x ^ "__" ^ Int.toString n
+ else
+ x
+ in
+ string s
+ end
| StrProj (str, s) => box [p_str env str,
string ".",
string s]
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-06 01:02:39 +0000