summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/cjr_print.sml6
-rw-r--r--src/compiler.sig2
-rw-r--r--src/compiler.sml4
-rw-r--r--src/core_print.sml6
-rw-r--r--src/corify.sml3
-rw-r--r--src/elab.sml24
-rw-r--r--src/elab_env.sig15
-rw-r--r--src/elab_env.sml119
-rw-r--r--src/elab_print.sig1
-rw-r--r--src/elab_print.sml154
-rw-r--r--src/elaborate.sig2
-rw-r--r--src/elaborate.sml267
-rw-r--r--src/flat_print.sml6
-rw-r--r--src/lacweb.lex2
-rw-r--r--src/list_util.sig3
-rw-r--r--src/list_util.sml15
-rw-r--r--src/mono_print.sml6
17 files changed, 537 insertions, 98 deletions
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index c7263e3b..c49d934e 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -186,9 +186,9 @@ fun p_decl env ((d, _) : decl) =
fun p_file env file =
let
- val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
- (E.declBinds env d,
- p_decl env d))
+ val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+ (p_decl env d,
+ E.declBinds env d))
env file
in
p_list_sep newline (fn x => x) pds
diff --git a/src/compiler.sig b/src/compiler.sig
index 3c9eea8b..65254873 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -32,7 +32,7 @@ signature COMPILER = sig
val compile : string -> unit
val parse : string -> Source.file option
- val elaborate : ElabEnv.env -> string -> (ElabEnv.env * Elab.file) option
+ val elaborate : ElabEnv.env -> string -> (Elab.file * ElabEnv.env) option
val corify : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
val reduce : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
val shake : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
diff --git a/src/compiler.sml b/src/compiler.sml
index 4276ed46..9a213ab6 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -70,7 +70,7 @@ fun elaborate env filename =
fun corify eenv cenv filename =
case elaborate eenv filename of
NONE => NONE
- | SOME (_, file) =>
+ | SOME (file, _) =>
if ErrorMsg.anyErrors () then
NONE
else
@@ -131,7 +131,7 @@ fun testParse filename =
fun testElaborate filename =
(case elaborate ElabEnv.basis filename of
NONE => print "Failed\n"
- | SOME (_, file) =>
+ | SOME (file, _) =>
(Print.print (ElabPrint.p_file ElabEnv.basis file);
print "\n"))
handle ElabEnv.UnboundNamed n =>
diff --git a/src/core_print.sml b/src/core_print.sml
index a219ac4d..42cbbc7a 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -258,9 +258,9 @@ fun p_decl env ((d, _) : decl) =
fun p_file env file =
let
- val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
- (E.declBinds env d,
- p_decl env d))
+ val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+ (p_decl env d,
+ E.declBinds env d))
env file
in
p_list_sep newline (fn x => x) pds
diff --git a/src/corify.sml b/src/corify.sml
index f9433cff..a5309dec 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -83,6 +83,9 @@ fun corifyDecl (d, loc : EM.span) =
L.DCon (x, n, k, c) => (L'.DCon (x, n, corifyKind k, corifyCon c), loc)
| L.DVal (x, n, t, e) => (L'.DVal (x, n, corifyCon t, corifyExp e), loc)
+ | L.DSgn _ => raise Fail "Not ready to corify signature"
+ | L.DStr _ => raise Fail "Not ready to corify structure"
+
val corify = map corifyDecl
end
diff --git a/src/elab.sml b/src/elab.sml
index ac1b4224..14664c0f 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -80,12 +80,34 @@ datatype exp' =
withtype exp = exp' located
+datatype sgn_item' =
+ SgiConAbs of string * int * kind
+ | SgiCon of string * int * kind * con
+ | SgiVal of string * int * con
+ | SgiStr of string * int * sgn
+
+and sgn' =
+ SgnConst of sgn_item list
+ | SgnVar of int
+ | SgnError
+
+withtype sgn_item = sgn_item' located
+and sgn = sgn' located
+
datatype decl' =
DCon of string * int * kind * con
| DVal of string * int * con * exp
+ | DSgn of string * int * sgn
+ | DStr of string * int * sgn * str
-withtype decl = decl' located
+ and str' =
+ StrConst of decl list
+ | StrVar of int
+ | StrError
+withtype decl = decl' located
+ and str = str' located
+
type file = decl list
end
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 8fe1da71..05badecf 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -58,9 +58,22 @@ signature ELAB_ENV = sig
val pushENamed : env -> string -> Elab.con -> env * int
val pushENamedAs : env -> string -> int -> Elab.con -> env
val lookupENamed : env -> int -> string * Elab.con
-
+
val lookupE : env -> string -> Elab.con var
+ val pushSgnNamed : env -> string -> Elab.sgn -> env * int
+ val pushSgnNamedAs : env -> string -> int -> Elab.sgn -> env
+ val lookupSgnNamed : env -> int -> string * Elab.sgn
+
+ val lookupSgn : env -> string -> (int * Elab.sgn) option
+
+ val pushStrNamed : env -> string -> Elab.sgn -> env * int
+ val pushStrNamedAs : env -> string -> int -> Elab.sgn -> env
+ val lookupStrNamed : env -> int -> string * Elab.sgn
+
+ val lookupStr : env -> string -> (int * Elab.sgn) option
+
val declBinds : env -> Elab.decl -> env
+ val sgiBinds : env -> Elab.sgn_item -> env
end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 78fa3daa..fd078e05 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -80,7 +80,13 @@ type env = {
renameE : con var' SM.map,
relE : (string * con) list,
- namedE : (string * con) IM.map
+ namedE : (string * con) IM.map,
+
+ renameSgn : (int * sgn) SM.map,
+ sgn : (string * sgn) IM.map,
+
+ renameStr : (int * sgn) SM.map,
+ str : (string * sgn) IM.map
}
val namedCounter = ref 0
@@ -92,7 +98,13 @@ val empty = {
renameE = SM.empty,
relE = [],
- namedE = IM.empty
+ namedE = IM.empty,
+
+ renameSgn = SM.empty,
+ sgn = IM.empty,
+
+ renameStr = SM.empty,
+ str = IM.empty
}
fun pushCRel (env : env) x k =
@@ -106,7 +118,14 @@ fun pushCRel (env : env) x k =
renameE = #renameE env,
relE = map (fn (x, c) => (x, lift c)) (#relE env),
- namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)}
+ namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
+
+ renameSgn = #renameSgn env,
+ sgn = #sgn env,
+
+ renameStr = #renameStr env,
+ str = #str env
+ }
end
fun lookupCRel (env : env) n =
@@ -120,7 +139,13 @@ fun pushCNamedAs (env : env) x n k co =
renameE = #renameE env,
relE = #relE env,
- namedE = #namedE env}
+ namedE = #namedE env,
+
+ renameSgn = #renameSgn env,
+ sgn = #sgn env,
+
+ renameStr = #renameStr env,
+ str = #str env}
fun pushCNamed env x k co =
let
@@ -152,7 +177,13 @@ fun pushERel (env : env) x t =
renameE = SM.insert (renameE, x, Rel' (0, t)),
relE = (x, t) :: #relE env,
- namedE = #namedE env}
+ namedE = #namedE env,
+
+ renameSgn = #renameSgn env,
+ sgn = #sgn env,
+
+ renameStr = #renameStr env,
+ str = #str env}
end
fun lookupERel (env : env) n =
@@ -166,7 +197,13 @@ fun pushENamedAs (env : env) x n t =
renameE = SM.insert (#renameE env, x, Named' (n, t)),
relE = #relE env,
- namedE = IM.insert (#namedE env, n, (x, t))}
+ namedE = IM.insert (#namedE env, n, (x, t)),
+
+ renameSgn = #renameSgn env,
+ sgn = #sgn env,
+
+ renameStr = #renameStr env,
+ str = #str env}
fun pushENamed env x t =
let
@@ -187,10 +224,80 @@ fun lookupE (env : env) x =
| SOME (Rel' x) => Rel x
| SOME (Named' x) => Named x
+fun pushSgnNamedAs (env : env) x n sgis =
+ {renameC = #renameC env,
+ relC = #relC env,
+ namedC = #namedC env,
+
+ renameE = #renameE env,
+ relE = #relE env,
+ namedE = #namedE env,
+
+ renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
+ sgn = IM.insert (#sgn env, n, (x, sgis)),
+
+ renameStr = #renameStr env,
+ str = #str env}
+
+fun pushSgnNamed env x sgis =
+ let
+ val n = !namedCounter
+ in
+ namedCounter := n + 1;
+ (pushSgnNamedAs env x n sgis, n)
+ end
+
+fun lookupSgnNamed (env : env) n =
+ case IM.find (#sgn env, n) of
+ NONE => raise UnboundNamed n
+ | SOME x => x
+
+fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
+
+fun pushStrNamedAs (env : env) x n sgis =
+ {renameC = #renameC env,
+ relC = #relC env,
+ namedC = #namedC env,
+
+ renameE = #renameE env,
+ relE = #relE env,
+ namedE = #namedE env,
+
+ renameSgn = #renameSgn env,
+ sgn = #sgn env,
+
+ renameStr = SM.insert (#renameStr env, x, (n, sgis)),
+ str = IM.insert (#str env, n, (x, sgis))}
+
+fun pushStrNamed env x sgis =
+ let
+ val n = !namedCounter
+ in
+ namedCounter := n + 1;
+ (pushStrNamedAs env x n sgis, n)
+ end
+
+fun lookupStrNamed (env : env) n =
+ case IM.find (#str env, n) of
+ NONE => raise UnboundNamed n
+ | SOME x => x
+
+fun lookupStr (env : env) x = SM.find (#renameStr env, x)
+
fun declBinds env (d, _) =
case d of
DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
| DVal (x, n, t, _) => pushENamedAs env x n t
+ | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
+ | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
+
+fun sgiBinds env (sgi, _) =
+ case sgi of
+ SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
+ | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
+ | SgiVal (x, n, t) => pushENamedAs env x n t
+ | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
+
val ktype = (KType, ErrorMsg.dummySpan)
diff --git a/src/elab_print.sig b/src/elab_print.sig
index 66ae8d43..49af2ded 100644
--- a/src/elab_print.sig
+++ b/src/elab_print.sig
@@ -33,6 +33,7 @@ signature ELAB_PRINT = sig
val p_con : ElabEnv.env -> Elab.con Print.printer
val p_exp : ElabEnv.env -> Elab.exp Print.printer
val p_decl : ElabEnv.env -> Elab.decl Print.printer
+ val p_sgn_item : ElabEnv.env -> Elab.sgn_item Print.printer
val p_file : ElabEnv.env -> Elab.file Print.printer
val debug : bool ref
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 37648068..c07631a0 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -228,57 +228,119 @@ fun p_exp' par env (e, _) =
and p_exp env = p_exp' false env
+fun p_named x n =
+ if !debug then
+ box [string x,
+ string "__",
+ string (Int.toString n)]
+ else
+ string x
+
+fun p_sgn_item env (sgi, _) =
+ case sgi of
+ SgiConAbs (x, n, k) => box [string "con",
+ space,
+ p_named x n,
+ space,
+ string "::",
+ space,
+ p_kind k]
+ | SgiCon (x, n, k, c) => box [string "con",
+ space,
+ p_named x n,
+ space,
+ string "::",
+ space,
+ p_kind k,
+ space,
+ string "=",
+ space,
+ p_con env c]
+ | SgiVal (x, n, c) => box [string "val",
+ space,
+ p_named x n,
+ space,
+ string ":",
+ space,
+ p_con env c]
+ | SgiStr (x, n, sgn) => box [string "structure",
+ space,
+ p_named x n,
+ space,
+ string ":",
+ space,
+ p_sgn env sgn]
+
+and p_sgn env (sgn, _) =
+ case sgn of
+ SgnConst sgis => box [string "sig",
+ newline,
+ p_list_sep newline (p_sgn_item env) sgis,
+ newline,
+ string "end"]
+ | SgnVar n => string (#1 (E.lookupSgnNamed env n))
+ | SgnError => string "<ERROR>"
+
fun p_decl env ((d, _) : decl) =
case d of
- DCon (x, n, k, c) =>
- let
- val xp = if !debug then
- box [string x,
- string "__",
- string (Int.toString n)]
- else
- string x
- in
- box [string "con",
- space,
- xp,
- space,
- string "::",
- space,
- p_kind k,
- space,
- string "=",
- space,
- p_con env c]
- end
- | DVal (x, n, t, e) =>
- let
- val xp = if !debug then
- box [string x,
- string "__",
- string (Int.toString n)]
- else
- string x
- in
- box [string "val",
- space,
- xp,
- space,
- string ":",
- space,
- p_con env t,
- space,
- string "=",
- space,
- p_exp env e]
- end
+ DCon (x, n, k, c) => box [string "con",
+ space,
+ p_named x n,
+ space,
+ string "::",
+ space,
+ p_kind k,
+ space,
+ string "=",
+ space,
+ p_con env c]
+ | DVal (x, n, t, e) => box [string "val",
+ space,
+ p_named x n,
+ space,
+ string ":",
+ space,
+ p_con env t,
+ space,
+ string "=",
+ space,
+ p_exp env e]
+
+ | DSgn (x, n, sgn) => box [string "signature",
+ space,
+ p_named x n,
+ space,
+ string "=",
+ space,
+ p_sgn env sgn]
+ | DStr (x, n, sgn, str) => box [string "structure",
+ space,
+ p_named x n,
+ space,
+ string ":",
+ space,
+ p_sgn env sgn,
+ space,
+ string "=",
+ space,
+ p_str env str]
+
+and p_str env (str, _) =
+ case str of
+ StrConst ds => box [string "struct",
+ newline,
+ p_list_sep newline (p_decl env) ds,
+ newline,
+ string "end"]
+ | StrVar n => string (#1 (E.lookupStrNamed env n))
+ | StrError => string "<ERROR>"
fun p_file env file =
let
- val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
- (E.declBinds env d,
- p_decl env d))
- env file
+ val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+ (p_decl env d,
+ E.declBinds env d))
+ env file
in
p_list_sep newline (fn x => x) pds
end
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 655df86c..1d388122 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -27,6 +27,6 @@
signature ELABORATE = sig
- val elabFile : ElabEnv.env -> Source.file -> ElabEnv.env * Elab.file
+ val elabFile : ElabEnv.env -> Source.file -> Elab.file * ElabEnv.env
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9b25f5ca..3cdb2d9f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -135,6 +135,8 @@ val ktype_record = (L'.KRecord ktype, dummy)
val cerror = (L'.CError, dummy)
val kerror = (L'.KError, dummy)
val eerror = (L'.EError, dummy)
+val sgnerror = (L'.SgnError, dummy)
+val strerror = (L'.StrError, dummy)
local
val count = ref 0
@@ -864,7 +866,220 @@ fun declError env err =
(ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
eprefaces' [("Expression", p_exp env e)])
-fun elabDecl env (d, loc) =
+datatype sgn_error =
+ UnboundSgn of ErrorMsg.span * string
+ | UnmatchedSgi of L'.sgn_item
+ | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
+ | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
+
+fun sgnError env err =
+ case err of
+ UnboundSgn (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
+ | UnmatchedSgi (sgi as (_, loc)) =>
+ (ErrorMsg.errorAt loc "Unmatched signature item";
+ eprefaces' [("Item", p_sgn_item env sgi)])
+ | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
+ (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
+ eprefaces' [("Item 1", p_sgn_item env sgi1),
+ ("Item 2", p_sgn_item env sgi2),
+ ("Kind 1", p_kind k1),
+ ("Kind 2", p_kind k2)];
+ kunifyError kerr)
+ | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
+ (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
+ eprefaces' [("Item 1", p_sgn_item env sgi1),
+ ("Item 2", p_sgn_item env sgi2),
+ ("Con 1", p_con env c1),
+ ("Con 2", p_con env c2)];
+ cunifyError env cerr)
+
+datatype str_error =
+ UnboundStr of ErrorMsg.span * string
+
+fun strError env err =
+ case err of
+ UnboundStr (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
+
+
+fun elabSgn_item ((sgi, loc), env) =
+ let
+
+ in
+ resetKunif ();
+ resetCunif ();
+ case sgi of
+ L.SgiConAbs (x, k) =>
+ let
+ val k' = elabKind k
+
+ val (env', n) = E.pushCNamed env x k' NONE
+ in
+ if ErrorMsg.anyErrors () then
+ ()
+ else (
+ if kunifsInKind k' then
+ declError env (KunifsRemainKind (loc, k'))
+ else
+ ()
+ );
+
+ ((L'.SgiConAbs (x, n, k'), loc), env')
+ end
+
+ | L.SgiCon (x, ko, c) =>
+ let
+ val k' = case ko of
+ NONE => kunif ()
+ | SOME k => elabKind k
+
+ val (c', ck) = elabCon env c
+ val (env', n) = E.pushCNamed env x k' (SOME c')
+ in
+ checkKind env c' ck k';
+
+ if ErrorMsg.anyErrors () then
+ ()
+ else (
+ if kunifsInKind k' then
+ declError env (KunifsRemainKind (loc, k'))
+ else
+ ();
+
+ if kunifsInCon c' then
+ declError env (KunifsRemainCon (loc, c'))
+ else
+ ()
+ );
+
+ ((L'.SgiCon (x, n, k', c'), loc), env')
+ end
+
+ | L.SgiVal (x, c) =>
+ let
+ val (c', ck) = elabCon env c
+
+ val (env', n) = E.pushENamed env x c'
+ in
+ unifyKinds ck ktype;
+
+ if ErrorMsg.anyErrors () then
+ ()
+ else (
+ if kunifsInCon c' then
+ declError env (KunifsRemainCon (loc, c'))
+ else
+ ()
+ );
+
+ ((L'.SgiVal (x, n, c'), loc), env')
+ end
+
+ | L.SgiStr (x, sgn) =>
+ let
+ val sgn' = elabSgn env sgn
+ val (env', n) = E.pushStrNamed env x sgn'
+ in
+ ((L'.SgiStr (x, n, sgn'), loc), env')
+ end
+
+ end
+
+and elabSgn env (sgn, loc) =
+ case sgn of
+ L.SgnConst sgis =>
+ let
+ val (sgis', _) = ListUtil.foldlMap elabSgn_item env sgis
+ in
+ (L'.SgnConst sgis', loc)
+ end
+ | L.SgnVar x =>
+ (case E.lookupSgn env x of
+ NONE =>
+ (sgnError env (UnboundSgn (loc, x));
+ (L'.SgnError, loc))
+ | SOME (n, sgis) => (L'.SgnVar n, loc))
+
+fun sgiOfDecl (d, loc) =
+ case d of
+ L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
+ | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
+ | L'.DSgn _ => NONE
+ | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
+
+fun subSgn env (all1 as (sgn1, _)) (all2 as (sgn2, loc2)) =
+ case (sgn1, sgn2) of
+ (L'.SgnError, _) => ()
+ | (_, L'.SgnError) => ()
+
+ | (L'.SgnVar n, _) =>
+ subSgn env (#2 (E.lookupSgnNamed env n)) all2
+ | (_, L'.SgnVar n) =>
+ subSgn env all1 (#2 (E.lookupSgnNamed env n))
+
+ | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
+ let
+ fun folder (sgi2All as (sgi, _), env) =
+ let
+ fun seek p =
+ let
+ fun seek env ls =
+ case ls of
+ [] => (sgnError env (UnmatchedSgi sgi2All);
+ env)
+ | h :: t =>
+ case p h of
+ NONE => seek (E.sgiBinds env h) t
+ | SOME env => env
+ in
+ seek env sgis1
+ end
+ in
+ case sgi of
+ L'.SgiConAbs (x, n2, k2) =>
+ seek (fn sgi1All as (sgi1, _) =>
+ let
+ fun found (x, n1, k1, co1) =
+ let
+ val () = unifyKinds k1 k2
+ handle KUnify (k1, k2, err) =>
+ sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+ val env = E.pushCNamedAs env x n1 k1 co1
+ in
+ SOME (if n1 = n2 then
+ env
+ else
+ E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))
+ end
+ in
+ case sgi1 of
+ L'.SgiConAbs (x, n1, k1) => found (x, n1, k1, NONE)
+ | L'.SgiCon (x, n1, k1, c1) => found (x, n1, k1, SOME c1)
+ | _ => NONE
+ end)
+
+ | L'.SgiCon (x, n2, k2, c2) =>
+ seek (fn sgi1All as (sgi1, _) =>
+ case sgi1 of
+ L'.SgiCon (x, n1, k1, c1) =>
+ let
+ val () = unifyCons env c1 c2
+ handle CUnify (c1, c2, err) =>
+ sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err))
+ in
+ SOME (E.pushCNamedAs env x n2 k2 (SOME c2))
+ end
+ | _ => NONE)
+
+ | _ => raise Fail "Not ready for more sig matching"
+ end
+ in
+ ignore (foldl folder env sgis2)
+ end
+
+
+fun elabDecl ((d, loc), env) =
let
in
@@ -896,8 +1111,7 @@ fun elabDecl env (d, loc) =
()
);
- (env',
- (L'.DCon (x, n, k', c'), loc))
+ ((L'.DCon (x, n, k', c'), loc), env')
end
| L.DVal (x, co, e) =>
let
@@ -933,15 +1147,50 @@ fun elabDecl env (d, loc) =
else
());
- (env',
- (L'.DVal (x, n, c', e'), loc))
+ ((L'.DVal (x, n, c', e'), loc), env')
end
- | L.DSgn _ => raise Fail "Not ready to elaborate signature"
- | L.DStr _ => raise Fail "Not ready to elaborate structure"
+ | L.DSgn (x, sgn) =>
+ let
+ val sgn' = elabSgn env sgn
+ val (env', n) = E.pushSgnNamed env x sgn'
+ in
+ ((L'.DSgn (x, n, sgn'), loc), env')
+ end
+
+ | L.DStr (x, sgno, str) =>
+ let
+ val formal = Option.map (elabSgn env) sgno
+ val (str', actual) = elabStr env str
+
+ val sgn' = case formal of
+ NONE => actual
+ | SOME formal =>
+ (subSgn env actual formal;
+ formal)
+
+ val (env', n) = E.pushStrNamed env x sgn'
+ in
+ ((L'.DStr (x, n, sgn', str'), loc), env')
+ end
end
-fun elabFile env ds =
- ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds
+and elabStr env (str, loc) =
+ case str of
+ L.StrConst ds =>
+ let
+ val (ds', env') = ListUtil.foldlMap elabDecl env ds
+ val sgis = List.mapPartial sgiOfDecl ds'
+ in
+ ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
+ end
+ | L.StrVar x =>
+ (case E.lookupStr env x of
+ NONE =>
+ (strError env (UnboundStr (loc, x));
+ (strerror, sgnerror))
+ | SOME (n, sgn) => ((L'.StrVar n, loc), sgn))
+
+val elabFile = ListUtil.foldlMap elabDecl
end
diff --git a/src/flat_print.sml b/src/flat_print.sml
index 612291c0..08008e9a 100644
--- a/src/flat_print.sml
+++ b/src/flat_print.sml
@@ -187,9 +187,9 @@ fun p_decl env ((d, _) : decl) =
fun p_file env file =
let
- val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
- (E.declBinds env d,
- p_decl env d))
+ val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+ (p_decl env d,
+ E.declBinds env d))
env file
in
p_list_sep newline (fn x => x) pds
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 2170c1d5..c5ce7ae8 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -129,7 +129,7 @@ realconst = [0-9]+\.[0-9]*;
<INITIAL> "fn" => (Tokens.FN (yypos, yypos + size yytext));
<INITIAL> "structure" => (Tokens.STRUCTURE (yypos, yypos + size yytext));
-<INITIAL> "signature" => (Tokens.STRUCTURE (yypos, yypos + size yytext));
+<INITIAL> "signature" => (Tokens.SIGNATURE (yypos, yypos + size yytext));
<INITIAL> "struct" => (Tokens.STRUCT (yypos, yypos + size yytext));
<INITIAL> "sig" => (Tokens.SIG (yypos, yypos + size yytext));
<INITIAL> "end" => (Tokens.END (yypos, yypos + size yytext));
diff --git a/src/list_util.sig b/src/list_util.sig
index 8185a28b..62013d25 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -27,9 +27,6 @@
signature LIST_UTIL = sig
- val mapfoldl : ('data1 * 'state -> 'state * 'data2) -> 'state -> 'data1 list
- -> 'state * 'data2 list
-
val mapfold : ('data, 'state, 'abort) Search.mapfolder
-> ('data list, 'state, 'abort) Search.mapfolder
diff --git a/src/list_util.sml b/src/list_util.sml
index aed2cdf0..7d3f8333 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -27,21 +27,6 @@
structure ListUtil :> LIST_UTIL = struct
-fun mapfoldl f i =
- let
- fun mf s ls' ls =
- case ls of
- nil => (s, rev ls')
- | h :: t =>
- let
- val (s, h') = f (h, s)
- in
- mf s (h' :: ls') t
- end
- in
- mf i []
- end
-
structure S = Search
fun mapfold f =
diff --git a/src/mono_print.sml b/src/mono_print.sml
index 6b259b7c..885b2d34 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -130,9 +130,9 @@ fun p_decl env ((d, _) : decl) =
fun p_file env file =
let
- val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
- (E.declBinds env d,
- p_decl env d))
+ val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
+ (p_decl env d,
+ E.declBinds env d))
env file
in
p_list_sep newline (fn x => x) pds
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-10 20:13:29 +0000