From 680da1afd0b8d2f4b4a6b4ec0ef3bad48d0babde Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 31 Mar 2017 17:35:05 -0400 Subject: Fix normalization of signatures that project signatures from other modules with multi-element paths (fixes #72) --- src/elab_env.sig | 3 +- src/elab_env.sml | 93 ++++++++++++++++++++++++++++++++-------------------- src/elab_print.sml | 6 ++-- tests/sigInModule.ur | 8 +++++ 4 files changed, 69 insertions(+), 41 deletions(-) create mode 100644 tests/sigInModule.ur diff --git a/src/elab_env.sig b/src/elab_env.sig index cbc85cdd..47b31c08 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -96,6 +96,7 @@ signature ELAB_ENV = sig val pushStrNamed : env -> string -> Elab.sgn -> env * int val pushStrNamedAs : env -> string -> int -> Elab.sgn -> env + val pushStrNamedAs' : bool (* also enrich typeclass instances? *) -> env -> string -> int -> Elab.sgn -> env val lookupStrNamed : env -> int -> string * Elab.sgn val lookupStr : env -> string -> (int * Elab.sgn) option @@ -123,6 +124,4 @@ signature ELAB_ENV = sig val patBinds : env -> Elab.pat -> env val patBindsN : Elab.pat -> int - exception Bad of Elab.con * Elab.con - end diff --git a/src/elab_env.sml b/src/elab_env.sml index cb08f348..8402bcba 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1097,14 +1097,21 @@ fun sgnS_sgn (str, (sgns, strs, cons)) sgn = end) | _ => sgn -fun sgnSubSgn x = +fun projectStr env {sgn, str, field} = + case #1 (hnormSgn env sgn) of + SgnConst sgis => + (case sgnSeek (fn SgiStr (_, x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of + NONE => NONE + | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) + | SgnError => SOME (SgnError, ErrorMsg.dummySpan) + | _ => NONE + +and sgnSubSgn x = ElabUtil.Sgn.map {kind = id, con = sgnS_con x, sgn_item = id, sgn = sgnS_sgn x} - - and projectSgn env {sgn, str, field} = case #1 (hnormSgn env sgn) of SgnConst sgis => @@ -1123,12 +1130,23 @@ and hnormSgn env (all as (sgn, loc)) = | SgnProj (m, ms, x) => let val (_, sgn) = lookupStrNamed env m + + fun doProjection (m1, NONE) = NONE + | doProjection (m1, SOME (str, sgn)) = + case projectStr env {str = str, + sgn = sgn, + field = m1} of + NONE => NONE + | SOME sgn' => SOME ((StrProj (str, m1), loc), sgn') in - case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms, - sgn = sgn, - field = x} of - NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed" - | SOME sgn => hnormSgn env sgn + case foldl doProjection (SOME ((StrVar m, loc), sgn)) ms of + NONE => raise Fail "ElabEnv.hnormSgn: pre-projectSgn failed" + | SOME (str, sgn) => + case projectSgn env {str = str, + sgn = sgn, + field = x} of + NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed" + | SOME sgn => hnormSgn env sgn end | SgnWhere (sgn, ms, x, c) => let @@ -1281,28 +1299,40 @@ fun enrichClasses env classes (m1, ms) sgn = end | _ => classes -fun pushStrNamedAs (env : env) x n sgn = - {renameK = #renameK env, - relK = #relK env, +and pushStrNamedAs' enrich (env : env) x n sgn = + let + val renameStr = SM.insert (#renameStr env, x, (n, sgn)) + val str = IM.insert (#str env, n, (x, sgn)) + fun newEnv classes = + {renameK = #renameK env, + relK = #relK env, - renameC = #renameC env, - relC = #relC env, - namedC = #namedC env, + renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, - datatypes = #datatypes env, - constructors = #constructors env, + datatypes = #datatypes env, + constructors = #constructors env, - classes = enrichClasses env (#classes env) (n, []) sgn, + classes = classes, - renameE = #renameE env, - relE = #relE env, - namedE = #namedE env, + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, - renameSgn = #renameSgn env, - sgn = #sgn env, + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = renameStr, + str = str} + in + if enrich then + newEnv (enrichClasses (newEnv (#classes env)) (#classes env) (n, []) sgn) + else + newEnv (#classes env) + end - renameStr = SM.insert (#renameStr env, x, (n, sgn)), - str = IM.insert (#str env, n, (x, sgn))} +and pushStrNamedAs env = pushStrNamedAs' true env fun pushStrNamed env x sgn = let @@ -1364,7 +1394,7 @@ fun sgiBinds env (sgi, loc) = env xncs end | SgiVal (x, n, t) => pushENamedAs env x n t - | SgiStr (_, x, n, sgn) => pushStrNamedAs env x n sgn + | SgiStr (_, x, n, sgn) => pushStrNamedAs' false env x n sgn | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | SgiConstraint _ => env @@ -1375,15 +1405,6 @@ fun sgnSubCon x = ElabUtil.Con.map {kind = id, con = sgnS_con x} -fun projectStr env {sgn, str, field} = - case #1 (hnormSgn env sgn) of - SgnConst sgis => - (case sgnSeek (fn SgiStr (_, x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of - NONE => NONE - | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) - | SgnError => SOME (SgnError, ErrorMsg.dummySpan) - | _ => NONE - fun chaseMpath env (n, ms) = let val (_, sgn) = lookupStrNamed env n @@ -1642,8 +1663,8 @@ fun declBinds env (d, loc) = | DVal (x, n, t, _) => pushENamedAs env x n t | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn - | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn - | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn + | DStr (x, n, sgn, _) => pushStrNamedAs' false env x n sgn + | DFfiStr (x, n, sgn) => pushStrNamedAs' false env x n sgn | DConstraint _ => env | DExport _ => env | DTable (tn, x, n, c, _, pc, _, cc) => diff --git a/src/elab_print.sml b/src/elab_print.sml index 06ea097f..8a6a651a 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -678,7 +678,7 @@ and p_sgn env (sgn, _) = space, string ":", space, - p_sgn (E.pushStrNamedAs env x n sgn) sgn'] + p_sgn (E.pushStrNamedAs' false env x n sgn) sgn'] | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn, space, string "where", @@ -695,7 +695,7 @@ and p_sgn env (sgn, _) = val m1x = #1 (E.lookupStrNamed env m1) handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1 - val m1s = if !debug then + val m1x = if !debug then m1x ^ "__" ^ Int.toString m1 else m1x @@ -867,7 +867,7 @@ and p_str env (str, _) = string s] | StrFun (x, n, sgn, sgn', str) => let - val env' = E.pushStrNamedAs env x n sgn + val env' = E.pushStrNamedAs' false env x n sgn in box [string "functor", space, diff --git a/tests/sigInModule.ur b/tests/sigInModule.ur new file mode 100644 index 00000000..efb7b0fc --- /dev/null +++ b/tests/sigInModule.ur @@ -0,0 +1,8 @@ +structure A = struct + signature S = sig + val x : int + end +end +structure B : A.S = struct + val x = 42 +end -- cgit v1.2.3