# HG changeset patch # User Adam Chlipala # Date 1376929532 14400 # Node ID 1aa9629e3a4c534161abf603a2be8408853b8478 # Parent 32784d27b5bc3750db5af41aae495e39530dbbe9 Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items diff -r 32784d27b5bc -r 1aa9629e3a4c src/elab.sml --- a/src/elab.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/elab.sml Mon Aug 19 12:25:32 2013 -0400 @@ -154,7 +154,7 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/elab_env.sml --- a/src/elab_env.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/elab_env.sml Mon Aug 19 12:25:32 2013 -0400 @@ -1126,26 +1126,44 @@ 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) + | 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]" - val sgis = traverse ([], sgis) - in - (SgnConst sgis, loc) - end - | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" + | (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 -r 32784d27b5bc -r 1aa9629e3a4c src/elab_print.sml --- a/src/elab_print.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/elab_print.sml Mon Aug 19 12:25:32 2013 -0400 @@ -680,17 +680,17 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/elab_util.sml --- a/src/elab_util.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/elab_util.sml Mon Aug 19 12:25:32 2013 -0400 @@ -759,12 +759,12 @@ 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 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/elaborate.sml --- a/src/elaborate.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/elaborate.sml Mon Aug 19 12:25:32 2013 -0400 @@ -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 @@ 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 @@ 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 @@ (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 -r 32784d27b5bc -r 1aa9629e3a4c src/expl.sml --- a/src/expl.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/expl.sml Mon Aug 19 12:25:32 2013 -0400 @@ -125,7 +125,7 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/expl_print.sml --- a/src/expl_print.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/expl_print.sml Mon Aug 19 12:25:32 2013 -0400 @@ -569,13 +569,13 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/expl_util.sml --- a/src/expl_util.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/expl_util.sml Mon Aug 19 12:25:32 2013 -0400 @@ -526,12 +526,12 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/explify.sml --- a/src/explify.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/explify.sml Mon Aug 19 12:25:32 2013 -0400 @@ -162,7 +162,7 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/source.sml --- a/src/source.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/source.sml Mon Aug 19 12:25:32 2013 -0400 @@ -100,7 +100,7 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/source_print.sml --- a/src/source_print.sml Sat Aug 10 10:13:40 2013 -0400 +++ b/src/source_print.sml Mon Aug 19 12:25:32 2013 -0400 @@ -505,17 +505,19 @@ 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 -r 32784d27b5bc -r 1aa9629e3a4c src/urweb.grm --- a/src/urweb.grm Sat Aug 10 10:13:40 2013 -0400 +++ b/src/urweb.grm Mon Aug 19 12:25:32 2013 -0400 @@ -802,8 +802,8 @@ 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)