summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_env.sml58
-rw-r--r--src/elab_print.sml22
-rw-r--r--src/elab_util.sml6
-rw-r--r--src/elaborate.sml64
-rw-r--r--src/expl.sml2
-rw-r--r--src/expl_print.sml4
-rw-r--r--src/expl_util.sml4
-rw-r--r--src/explify.sml2
-rw-r--r--src/source.sml2
-rw-r--r--src/source_print.sml24
-rw-r--r--src/urweb.grm4
12 files changed, 120 insertions, 74 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 9147f7d3..2dab5c34 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -154,7 +154,7 @@ and sgn' =
SgnConst of sgn_item list
| SgnVar of int
| SgnFun of string * int * sgn * sgn
- | SgnWhere of sgn * string * con
+ | SgnWhere of sgn * string list * string * con
| SgnProj of int * string list * string
| SgnError
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 5d684817..465fb7e4 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1126,26 +1126,44 @@ and hnormSgn env (all as (sgn, loc)) =
NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
| SOME sgn => hnormSgn env sgn
end
- | SgnWhere (sgn, x, c) =>
- case #1 (hnormSgn env sgn) of
- SgnError => (SgnError, loc)
- | SgnConst sgis =>
- let
- fun traverse (pre, post) =
- case post of
- [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
- | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
- if x = x' then
- List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
- else
- traverse (sgi :: pre, rest)
- | sgi :: rest => traverse (sgi :: pre, rest)
-
- val sgis = traverse ([], sgis)
- in
- (SgnConst sgis, loc)
- end
- | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
+ | SgnWhere (sgn, ms, x, c) =>
+ let
+ fun rewrite (sgn, ms) =
+ case #1 (hnormSgn env sgn) of
+ SgnError => (SgnError, loc)
+ | SgnConst sgis =>
+ let
+ fun traverse (ms, pre, post) =
+ case post of
+ [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
+
+ | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
+ if List.null ms andalso x = x' then
+ List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
+ else
+ traverse (ms, sgi :: pre, rest)
+
+ | (sgi as (SgiStr (x', n, sgn'), loc)) :: rest =>
+ (case ms of
+ [] => traverse (ms, sgi :: pre, rest)
+ | x :: ms' =>
+ if x = x' then
+ List.revAppend (pre,
+ (SgiStr (x', n,
+ rewrite (sgn', ms')), loc) :: rest)
+ else
+ traverse (ms, sgi :: pre, rest))
+
+ | sgi :: rest => traverse (ms, sgi :: pre, rest)
+
+ val sgis = traverse (ms, [], sgis)
+ in
+ (SgnConst sgis, loc)
+ end
+ | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
+ in
+ rewrite (sgn, ms)
+ end
fun manifest (m, ms, loc) =
foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms
diff --git a/src/elab_print.sml b/src/elab_print.sml
index c32368a9..7ce94c97 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -680,17 +680,17 @@ and p_sgn env (sgn, _) =
string ":",
space,
p_sgn (E.pushStrNamedAs env x n sgn) sgn']
- | SgnWhere (sgn, x, c) => box [p_sgn env sgn,
- space,
- string "where",
- space,
- string "con",
- space,
- string x,
- space,
- string "=",
- space,
- p_con env c]
+ | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn,
+ space,
+ string "where",
+ space,
+ string "con",
+ space,
+ p_list_sep (string ".") string (ms @ [x]),
+ space,
+ string "=",
+ space,
+ p_con env c]
| SgnProj (m1, ms, x) =>
let
val m1x = #1 (E.lookupStrNamed env m1)
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 51bcba5a..60245585 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -759,12 +759,12 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
fn s2' =>
(SgnFun (m, n, s1', s2'), loc)))
| SgnProj _ => S.return2 sAll
- | SgnWhere (sgn, x, c) =>
+ | SgnWhere (sgn, ms, x, c) =>
S.bind2 (sg ctx sgn,
fn sgn' =>
S.map2 (con ctx c,
fn c' =>
- (SgnWhere (sgn', x, c'), loc)))
+ (SgnWhere (sgn', ms, x, c'), loc)))
| SgnError => S.return2 sAll
in
sg
@@ -1248,7 +1248,7 @@ and maxNameSgn (sgn, _) =
SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
| SgnVar n => n
| SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
- | SgnWhere (sgn, _, _) => maxNameSgn sgn
+ | SgnWhere (sgn, _, _, _) => maxNameSgn sgn
| SgnProj (n, _, _) => n
| SgnError => 0
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 426934bd..18010244 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2013, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -2640,8 +2640,9 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
let
val (sgn', gs') = elabSgn (env, denv) sgn
val (env', n) = E.pushStrNamed env x sgn'
+ val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []}
in
- ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
+ ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv', gs' @ gs))
end
| L.SgiSgn (x, sgn) =>
@@ -2798,26 +2799,33 @@ and elabSgn (env, denv) (sgn, loc) =
in
((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
end
- | L.SgnWhere (sgn, x, c) =>
+ | L.SgnWhere (sgn, ms, x, c) =>
let
val (sgn', ds1) = elabSgn (env, denv) sgn
val (c', ck, ds2) = elabCon (env, denv) c
- in
- case #1 (hnormSgn env sgn') of
- L'.SgnError => (sgnerror, [])
- | L'.SgnConst sgis =>
- if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
- x' = x andalso
- (unifyKinds env k ck
- handle KUnify x => sgnError env (WhereWrongKind x);
- true)
- | _ => false) sgis then
- ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
- else
- (sgnError env (UnWhereable (sgn', x));
- (sgnerror, []))
- | _ => (sgnError env (UnWhereable (sgn', x));
- (sgnerror, []))
+
+ fun checkPath (ms, sgn') =
+ case #1 (hnormSgn env sgn') of
+ L'.SgnConst sgis =>
+ List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
+ List.null ms andalso x' = x andalso
+ (unifyKinds env k ck
+ handle KUnify x => sgnError env (WhereWrongKind x);
+ true)
+ | (L'.SgiStr (x', _, sgn''), _) =>
+ (case ms of
+ [] => false
+ | m :: ms' =>
+ m = x' andalso
+ checkPath (ms', sgn''))
+ | _ => false) sgis
+ | _ => false
+ in
+ if checkPath (ms, sgn') then
+ ((L'.SgnWhere (sgn', ms, x, c'), loc), ds1 @ ds2)
+ else
+ (sgnError env (UnWhereable (sgn', x));
+ (sgnerror, []))
end
| L.SgnProj (m, ms, x) =>
(case E.lookupStr env m of
@@ -3594,6 +3602,24 @@ and wildifyStr env (str, sgn) =
(SOME f, SOME x) => SOME (L.CApp (f, x), loc)
| _ => NONE)
+ | L'.CTuple cs =>
+ let
+ val cs' = foldr (fn (c, cs') =>
+ case cs' of
+ NONE => NONE
+ | SOME cs' =>
+ case decompileCon env c of
+ NONE => NONE
+ | SOME c' => SOME (c' :: cs'))
+ (SOME []) cs
+ in
+ case cs' of
+ NONE => NONE
+ | SOME cs' => SOME (L.CTuple cs', loc)
+ end
+
+ | L'.CMap _ => SOME (L.CMap, loc)
+
| c => (Print.preface ("WTF?", p_con env (c, loc)); NONE)
fun buildNeeded env sgis =
diff --git a/src/expl.sml b/src/expl.sml
index 119c1d92..0d4e63cc 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -125,7 +125,7 @@ and sgn' =
SgnConst of sgn_item list
| SgnVar of int
| SgnFun of string * int * sgn * sgn
- | SgnWhere of sgn * string * con
+ | SgnWhere of sgn * string list * string * con
| SgnProj of int * string list * string
withtype sgn_item = sgn_item' located
diff --git a/src/expl_print.sml b/src/expl_print.sml
index d89b0512..a830dccb 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -569,13 +569,13 @@ and p_sgn env (sgn, loc) =
string ":",
space,
p_sgn (E.pushStrNamed env x n sgn) sgn']
- | SgnWhere (sgn, x, c) => box [p_sgn env sgn,
+ | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn,
space,
string "where",
space,
string "con",
space,
- string x,
+ p_list_sep (string ".") string (ms @ [x]),
space,
string "=",
space,
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 1932d52d..ff55823f 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -526,12 +526,12 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
fn s2' =>
(SgnFun (m, n, s1', s2'), loc)))
- | SgnWhere (sgn, x, c) =>
+ | SgnWhere (sgn, ms, x, c) =>
S.bind2 (sg ctx sgn,
fn sgn' =>
S.map2 (con ctx c,
fn c' =>
- (SgnWhere (sgn', x, c'), loc)))
+ (SgnWhere (sgn', ms, x, c'), loc)))
| SgnProj _ => S.return2 sAll
in
sg
diff --git a/src/explify.sml b/src/explify.sml
index 65e78443..4c60bd20 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -162,7 +162,7 @@ and explifySgn (sgn, loc) =
L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc)
| L.SgnVar n => (L'.SgnVar n, loc)
| L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc)
- | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc)
+ | L.SgnWhere (sgn, ms, x, c) => (L'.SgnWhere (explifySgn sgn, ms, x, explifyCon c), loc)
| L.SgnProj x => (L'.SgnProj x, loc)
| L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
diff --git a/src/source.sml b/src/source.sml
index 18f83d2b..d66160db 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -100,7 +100,7 @@ and sgn' =
SgnConst of sgn_item list
| SgnVar of string
| SgnFun of string * sgn * sgn
- | SgnWhere of sgn * string * con
+ | SgnWhere of sgn * string list * string * con
| SgnProj of string * string list * string
and pat' =
diff --git a/src/source_print.sml b/src/source_print.sml
index cd3314e1..c8a38922 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -505,17 +505,19 @@ and p_sgn (sgn, _) =
string ":",
space,
p_sgn sgn']
- | SgnWhere (sgn, x, c) => box [p_sgn sgn,
- space,
- string "where",
- space,
- string "con",
- space,
- string x,
- space,
- string "=",
- space,
- p_con c]
+ | SgnWhere (sgn, ms, x, c) => box [p_sgn sgn,
+ space,
+ string "where",
+ space,
+ string "con",
+ space,
+ p_list_sep (string ".")
+ string (ms @ [x]),
+ string x,
+ space,
+ string "=",
+ space,
+ p_con c]
| SgnProj (m, ms, x) => p_list_sep (string ".") string (m :: ms @ [x])
diff --git a/src/urweb.grm b/src/urweb.grm
index c2a48742..29019649 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -802,8 +802,8 @@ sgntm : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright))
List.take (ms, length ms - 1),
List.nth (ms, length ms - 1)),
s (mpathleft, mpathright))
- | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
- | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
+ | sgntm WHERE CON path EQ cexp (SgnWhere (sgntm, #1 path, #2 path, cexp), s (sgntmleft, cexpright))
+ | sgntm WHERE LTYPE path EQ cexp (SgnWhere (sgntm, #1 path, #2 path, cexp), s (sgntmleft, cexpright))
| LPAREN sgn RPAREN (sgn)
cexpO : (NONE)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-10 19:33:28 +0000