adamc@2: (* Copyright (c) 2008, Adam Chlipala adamc@2: * All rights reserved. adamc@2: * adamc@2: * Redistribution and use in source and binary forms, with or without adamc@2: * modification, are permitted provided that the following conditions are met: adamc@2: * adamc@2: * - Redistributions of source code must retain the above copyright notice, adamc@2: * this list of conditions and the following disclaimer. adamc@2: * - Redistributions in binary form must reproduce the above copyright notice, adamc@2: * this list of conditions and the following disclaimer in the documentation adamc@2: * and/or other materials provided with the distribution. adamc@2: * - The names of contributors may not be used to endorse or promote products adamc@2: * derived from this software without specific prior written permission. adamc@2: * adamc@2: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@2: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@2: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@2: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@2: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@2: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@2: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@2: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@2: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@2: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@2: * POSSIBILITY OF SUCH DAMAGE. adamc@2: *) adamc@2: adamc@2: structure ElabEnv :> ELAB_ENV = struct adamc@2: adamc@2: open Elab adamc@2: adamc@13: structure U = ElabUtil adamc@13: adamc@2: structure IM = IntBinaryMap adamc@2: structure SM = BinaryMapFn(struct adamc@2: type ord_key = string adamc@2: val compare = String.compare adamc@2: end) adamc@2: adamc@2: exception UnboundRel of int adamc@2: exception UnboundNamed of int adamc@2: adamc@13: adamc@13: (* AST utility functions *) adamc@13: adamc@13: exception SynUnif adamc@13: adamc@13: val liftConInCon = adamc@13: U.Con.mapB {kind = fn k => k, adamc@13: con = fn bound => fn c => adamc@13: case c of adamc@16: CRel xn => adamc@13: if xn < bound then adamc@13: c adamc@13: else adamc@16: CRel (xn + 1) adamc@17: (*| CUnif _ => raise SynUnif*) adamc@13: | _ => c, adamc@13: bind = fn (bound, U.Con.Rel _) => bound + 1 adamc@13: | (bound, _) => bound} adamc@13: adamc@13: val lift = liftConInCon 0 adamc@13: adamc@13: adamc@13: (* Back to environments *) adamc@13: adamc@9: datatype 'a var' = adamc@9: Rel' of int * 'a adamc@9: | Named' of int * 'a adamc@2: adamc@9: datatype 'a var = adamc@9: NotBound adamc@9: | Rel of int * 'a adamc@9: | Named of int * 'a adamc@2: adamc@2: type env = { adamc@9: renameC : kind var' SM.map, adamc@2: relC : (string * kind) list, adamc@11: namedC : (string * kind * con option) IM.map, adamc@9: adamc@9: renameE : con var' SM.map, adamc@9: relE : (string * con) list, adamc@31: namedE : (string * con) IM.map, adamc@31: adamc@31: renameSgn : (int * sgn) SM.map, adamc@31: sgn : (string * sgn) IM.map, adamc@31: adamc@31: renameStr : (int * sgn) SM.map, adamc@31: str : (string * sgn) IM.map adamc@2: } adamc@2: adamc@2: val namedCounter = ref 0 adamc@2: adamc@2: val empty = { adamc@2: renameC = SM.empty, adamc@2: relC = [], adamc@9: namedC = IM.empty, adamc@9: adamc@9: renameE = SM.empty, adamc@9: relE = [], adamc@31: namedE = IM.empty, adamc@31: adamc@31: renameSgn = SM.empty, adamc@31: sgn = IM.empty, adamc@31: adamc@31: renameStr = SM.empty, adamc@31: str = IM.empty adamc@2: } adamc@2: adamc@2: fun pushCRel (env : env) x k = adamc@2: let adamc@9: val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) adamc@2: | x => x) (#renameC env) adamc@2: in adamc@9: {renameC = SM.insert (renameC, x, Rel' (0, k)), adamc@2: relC = (x, k) :: #relC env, adamc@13: namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), adamc@9: adamc@9: renameE = #renameE env, adamc@13: relE = map (fn (x, c) => (x, lift c)) (#relE env), adamc@31: namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), adamc@31: adamc@31: renameSgn = #renameSgn env, adamc@31: sgn = #sgn env, adamc@31: adamc@31: renameStr = #renameStr env, adamc@31: str = #str env adamc@31: } adamc@2: end adamc@2: adamc@2: fun lookupCRel (env : env) n = adamc@2: (List.nth (#relC env, n)) adamc@2: handle Subscript => raise UnboundRel n adamc@2: adamc@11: fun pushCNamedAs (env : env) x n k co = adamc@9: {renameC = SM.insert (#renameC env, x, Named' (n, k)), adamc@5: relC = #relC env, adamc@11: namedC = IM.insert (#namedC env, n, (x, k, co)), adamc@9: adamc@9: renameE = #renameE env, adamc@9: relE = #relE env, adamc@31: namedE = #namedE env, adamc@31: adamc@31: renameSgn = #renameSgn env, adamc@31: sgn = #sgn env, adamc@31: adamc@31: renameStr = #renameStr env, adamc@31: str = #str env} adamc@5: adamc@11: fun pushCNamed env x k co = adamc@2: let adamc@2: val n = !namedCounter adamc@2: in adamc@2: namedCounter := n + 1; adamc@11: (pushCNamedAs env x n k co, n) adamc@2: end adamc@2: adamc@2: fun lookupCNamed (env : env) n = adamc@2: case IM.find (#namedC env, n) of adamc@2: NONE => raise UnboundNamed n adamc@2: | SOME x => x adamc@2: adamc@2: fun lookupC (env : env) x = adamc@2: case SM.find (#renameC env, x) of adamc@9: NONE => NotBound adamc@9: | SOME (Rel' x) => Rel x adamc@9: | SOME (Named' x) => Named x adamc@9: adamc@9: fun pushERel (env : env) x t = adamc@9: let adamc@9: val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) adamc@9: | x => x) (#renameE env) adamc@9: in adamc@9: {renameC = #renameC env, adamc@9: relC = #relC env, adamc@9: namedC = #namedC env, adamc@9: adamc@9: renameE = SM.insert (renameE, x, Rel' (0, t)), adamc@9: relE = (x, t) :: #relE env, adamc@31: namedE = #namedE env, adamc@31: adamc@31: renameSgn = #renameSgn env, adamc@31: sgn = #sgn env, adamc@31: adamc@31: renameStr = #renameStr env, adamc@31: str = #str env} adamc@9: end adamc@9: adamc@9: fun lookupERel (env : env) n = adamc@9: (List.nth (#relE env, n)) adamc@9: handle Subscript => raise UnboundRel n adamc@9: adamc@9: fun pushENamedAs (env : env) x n t = adamc@9: {renameC = #renameC env, adamc@9: relC = #relC env, adamc@9: namedC = #namedC env, adamc@9: adamc@9: renameE = SM.insert (#renameE env, x, Named' (n, t)), adamc@9: relE = #relE env, adamc@31: namedE = IM.insert (#namedE env, n, (x, t)), adamc@31: adamc@31: renameSgn = #renameSgn env, adamc@31: sgn = #sgn env, adamc@31: adamc@31: renameStr = #renameStr env, adamc@31: str = #str env} adamc@9: adamc@9: fun pushENamed env x t = adamc@9: let adamc@9: val n = !namedCounter adamc@9: in adamc@9: namedCounter := n + 1; adamc@9: (pushENamedAs env x n t, n) adamc@9: end adamc@9: adamc@9: fun lookupENamed (env : env) n = adamc@9: case IM.find (#namedE env, n) of adamc@9: NONE => raise UnboundNamed n adamc@9: | SOME x => x adamc@9: adamc@9: fun lookupE (env : env) x = adamc@9: case SM.find (#renameE env, x) of adamc@9: NONE => NotBound adamc@9: | SOME (Rel' x) => Rel x adamc@9: | SOME (Named' x) => Named x adamc@2: adamc@31: fun pushSgnNamedAs (env : env) x n sgis = adamc@31: {renameC = #renameC env, adamc@31: relC = #relC env, adamc@31: namedC = #namedC env, adamc@31: adamc@31: renameE = #renameE env, adamc@31: relE = #relE env, adamc@31: namedE = #namedE env, adamc@31: adamc@31: renameSgn = SM.insert (#renameSgn env, x, (n, sgis)), adamc@31: sgn = IM.insert (#sgn env, n, (x, sgis)), adamc@31: adamc@31: renameStr = #renameStr env, adamc@31: str = #str env} adamc@31: adamc@31: fun pushSgnNamed env x sgis = adamc@31: let adamc@31: val n = !namedCounter adamc@31: in adamc@31: namedCounter := n + 1; adamc@31: (pushSgnNamedAs env x n sgis, n) adamc@31: end adamc@31: adamc@31: fun lookupSgnNamed (env : env) n = adamc@31: case IM.find (#sgn env, n) of adamc@31: NONE => raise UnboundNamed n adamc@31: | SOME x => x adamc@31: adamc@31: fun lookupSgn (env : env) x = SM.find (#renameSgn env, x) adamc@31: adamc@31: fun pushStrNamedAs (env : env) x n sgis = adamc@31: {renameC = #renameC env, adamc@31: relC = #relC env, adamc@31: namedC = #namedC env, adamc@31: adamc@31: renameE = #renameE env, adamc@31: relE = #relE env, adamc@31: namedE = #namedE env, adamc@31: adamc@31: renameSgn = #renameSgn env, adamc@31: sgn = #sgn env, adamc@31: adamc@31: renameStr = SM.insert (#renameStr env, x, (n, sgis)), adamc@31: str = IM.insert (#str env, n, (x, sgis))} adamc@31: adamc@31: fun pushStrNamed env x sgis = adamc@31: let adamc@31: val n = !namedCounter adamc@31: in adamc@31: namedCounter := n + 1; adamc@31: (pushStrNamedAs env x n sgis, n) adamc@31: end adamc@31: adamc@31: fun lookupStrNamed (env : env) n = adamc@31: case IM.find (#str env, n) of adamc@31: NONE => raise UnboundNamed n adamc@31: | SOME x => x adamc@31: adamc@31: fun lookupStr (env : env) x = SM.find (#renameStr env, x) adamc@31: adamc@13: fun declBinds env (d, _) = adamc@13: case d of adamc@13: DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) adamc@13: | DVal (x, n, t, _) => pushENamedAs env x n t adamc@31: | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn adamc@31: | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn adamc@48: | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn adamc@88: | DConstraint _ => env adamc@100: | DPage _ => env adamc@31: adamc@31: fun sgiBinds env (sgi, _) = adamc@31: case sgi of adamc@31: SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE adamc@31: | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) adamc@31: | SgiVal (x, n, t) => pushENamedAs env x n t adamc@31: | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn adamc@59: | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn adamc@88: | SgiConstraint _ => env adamc@31: adamc@34: fun sgnSeek f sgis = adamc@34: let adamc@59: fun seek (sgis, sgns, strs, cons) = adamc@34: case sgis of adamc@34: [] => NONE adamc@34: | (sgi, _) :: sgis => adamc@34: case f sgi of adamc@59: SOME v => SOME (v, (sgns, strs, cons)) adamc@88: | NONE => adamc@88: case sgi of adamc@88: SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) adamc@88: | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) adamc@88: | SgiVal _ => seek (sgis, sgns, strs, cons) adamc@88: | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) adamc@88: | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) adamc@88: | SgiConstraint _ => seek (sgis, sgns, strs, cons) adamc@34: in adamc@59: seek (sgis, IM.empty, IM.empty, IM.empty) adamc@34: end adamc@34: adamc@34: fun id x = x adamc@34: adamc@34: fun unravelStr (str, _) = adamc@34: case str of adamc@34: StrVar x => (x, []) adamc@34: | StrProj (str, m) => adamc@34: let adamc@34: val (x, ms) = unravelStr str adamc@34: in adamc@34: (x, ms @ [m]) adamc@34: end adamc@34: | _ => raise Fail "unravelStr" adamc@34: adamc@59: fun sgnS_con (str, (sgns, strs, cons)) c = adamc@34: case c of adamc@34: CModProj (m1, ms, x) => adamc@34: (case IM.find (strs, m1) of adamc@34: NONE => c adamc@34: | SOME m1x => adamc@34: let adamc@34: val (m1, ms') = unravelStr str adamc@34: in adamc@34: CModProj (m1, ms' @ m1x :: ms, x) adamc@34: end) adamc@34: | CNamed n => adamc@34: (case IM.find (cons, n) of adamc@34: NONE => c adamc@34: | SOME nx => adamc@34: let adamc@34: val (m1, ms) = unravelStr str adamc@34: in adamc@34: CModProj (m1, ms, nx) adamc@34: end) adamc@34: | _ => c adamc@34: adamc@59: fun sgnS_sgn (str, (sgns, strs, cons)) sgn = adamc@59: case sgn of adamc@59: SgnProj (m1, ms, x) => adamc@59: (case IM.find (strs, m1) of adamc@59: NONE => sgn adamc@59: | SOME m1x => adamc@59: let adamc@59: val (m1, ms') = unravelStr str adamc@59: in adamc@59: SgnProj (m1, ms' @ m1x :: ms, x) adamc@59: end) adamc@59: | SgnVar n => adamc@59: (case IM.find (sgns, n) of adamc@59: NONE => sgn adamc@59: | SOME nx => adamc@59: let adamc@59: val (m1, ms) = unravelStr str adamc@59: in adamc@59: SgnProj (m1, ms, nx) adamc@59: end) adamc@59: | _ => sgn adamc@59: adamc@59: fun sgnSubCon x = adamc@34: ElabUtil.Con.map {kind = id, adamc@59: con = sgnS_con x} adamc@34: adamc@59: fun sgnSubSgn x = adamc@34: ElabUtil.Sgn.map {kind = id, adamc@59: con = sgnS_con x, adamc@34: sgn_item = id, adamc@59: sgn = sgnS_sgn x} adamc@34: adamc@42: fun hnormSgn env (all as (sgn, loc)) = adamc@34: case sgn of adamc@42: SgnError => all adamc@42: | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n)) adamc@42: | SgnConst _ => all adamc@42: | SgnFun _ => all adamc@59: | SgnProj (m, ms, x) => adamc@59: let adamc@59: val (_, sgn) = lookupStrNamed env m adamc@59: in adamc@59: case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms, adamc@59: sgn = sgn, adamc@59: field = x} of adamc@59: NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed" adamc@59: | SOME sgn => sgn adamc@59: end adamc@42: | SgnWhere (sgn, x, c) => adamc@42: case #1 (hnormSgn env sgn) of adamc@42: SgnError => (SgnError, loc) adamc@42: | SgnConst sgis => adamc@42: let adamc@42: fun traverse (pre, post) = adamc@42: case post of adamc@42: [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]" adamc@42: | (sgi as (SgiConAbs (x', n, k), loc)) :: rest => adamc@42: if x = x' then adamc@42: List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest) adamc@42: else adamc@42: traverse (sgi :: pre, rest) adamc@42: | sgi :: rest => traverse (sgi :: pre, rest) adamc@42: adamc@42: val sgis = traverse ([], sgis) adamc@42: in adamc@42: (SgnConst sgis, loc) adamc@42: end adamc@42: | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" adamc@42: adamc@59: and projectSgn env {sgn, str, field} = adamc@59: case #1 (hnormSgn env sgn) of adamc@59: SgnConst sgis => adamc@59: (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of adamc@59: NONE => NONE adamc@59: | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) adamc@59: | SgnError => SOME (SgnError, ErrorMsg.dummySpan) adamc@59: | _ => NONE adamc@59: adamc@59: fun projectStr env {sgn, str, field} = adamc@59: case #1 (hnormSgn env sgn) of adamc@59: SgnConst sgis => adamc@59: (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of adamc@59: NONE => NONE adamc@59: | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) adamc@59: | SgnError => SOME (SgnError, ErrorMsg.dummySpan) adamc@59: | _ => NONE adamc@59: adamc@42: fun projectCon env {sgn, str, field} = adamc@42: case #1 (hnormSgn env sgn) of adamc@34: SgnConst sgis => adamc@34: (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE adamc@34: | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE adamc@34: | _ => NONE) sgis of adamc@34: NONE => NONE adamc@34: | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) adamc@34: | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) adamc@42: | _ => NONE adamc@34: adamc@42: fun projectVal env {sgn, str, field} = adamc@42: case #1 (hnormSgn env sgn) of adamc@34: SgnConst sgis => adamc@34: (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of adamc@34: NONE => NONE adamc@34: | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)) adamc@34: | SgnError => SOME (CError, ErrorMsg.dummySpan) adamc@42: | _ => NONE adamc@34: adamc@88: fun sgnSeekConstraints (str, sgis) = adamc@88: let adamc@88: fun seek (sgis, sgns, strs, cons, acc) = adamc@88: case sgis of adamc@88: [] => acc adamc@88: | (sgi, _) :: sgis => adamc@88: case sgi of adamc@88: SgiConstraint (c1, c2) => adamc@88: let adamc@88: val sub = sgnSubCon (str, (sgns, strs, cons)) adamc@88: in adamc@88: seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc) adamc@88: end adamc@88: | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) adamc@88: | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) adamc@88: | SgiVal _ => seek (sgis, sgns, strs, cons, acc) adamc@88: | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) adamc@88: | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) adamc@88: in adamc@88: seek (sgis, IM.empty, IM.empty, IM.empty, []) adamc@88: end adamc@88: adamc@88: fun projectConstraints env {sgn, str} = adamc@88: case #1 (hnormSgn env sgn) of adamc@88: SgnConst sgis => SOME (sgnSeekConstraints (str, sgis)) adamc@88: | SgnError => SOME [] adamc@88: | _ => NONE adamc@34: adamc@2: end