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@191: type datatyp = string list * (string * con option) IM.map adamc@157: 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@157: datatypes : datatyp IM.map, adamc@191: constructors : (datatype_kind * int * string list * con option * int) SM.map, adamc@157: 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@109: fun newNamed () = adamc@109: let adamc@109: val r = !namedCounter adamc@109: in adamc@109: namedCounter := r + 1; adamc@109: r adamc@109: end adamc@109: adamc@2: val empty = { adamc@2: renameC = SM.empty, adamc@2: relC = [], adamc@9: namedC = IM.empty, adamc@9: adamc@157: datatypes = IM.empty, adamc@171: constructors = SM.empty, adamc@157: 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@157: datatypes = #datatypes env, adamc@171: constructors = #constructors env, adamc@157: 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@157: datatypes = #datatypes env, adamc@171: constructors = #constructors env, adamc@157: 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@191: fun pushDatatype (env : env) n xs xncs = adamc@188: let adamc@188: val dk = U.classifyDatatype xncs adamc@188: in adamc@188: {renameC = #renameC env, adamc@188: relC = #relC env, adamc@188: namedC = #namedC env, adamc@157: adamc@188: datatypes = IM.insert (#datatypes env, n, adamc@191: (xs, foldl (fn ((x, n, to), cons) => adamc@191: IM.insert (cons, n, (x, to))) IM.empty xncs)), adamc@188: constructors = foldl (fn ((x, n', to), cmap) => adamc@191: SM.insert (cmap, x, (dk, n', xs, to, n))) adamc@188: (#constructors env) xncs, adamc@157: adamc@188: renameE = #renameE env, adamc@188: relE = #relE env, adamc@188: namedE = #namedE env, adamc@157: adamc@188: renameSgn = #renameSgn env, adamc@188: sgn = #sgn env, adamc@157: adamc@188: renameStr = #renameStr env, adamc@188: str = #str env} adamc@188: end adamc@157: adamc@157: fun lookupDatatype (env : env) n = adamc@157: case IM.find (#datatypes env, n) of adamc@157: NONE => raise UnboundNamed n adamc@157: | SOME x => x adamc@157: adamc@191: fun lookupDatatypeConstructor (_, dt) n = adamc@157: case IM.find (dt, n) of adamc@157: NONE => raise UnboundNamed n adamc@157: | SOME x => x adamc@157: adamc@171: fun lookupConstructor (env : env) s = SM.find (#constructors env, s) adamc@171: adamc@191: fun datatypeArgs (xs, _) = xs adamc@191: fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt adamc@157: 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@157: datatypes = #datatypes env, adamc@171: constructors = #constructors env, adamc@157: 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@157: datatypes = #datatypes env, adamc@171: constructors = #constructors env, adamc@157: 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@157: datatypes = #datatypes env, adamc@171: constructors = #constructors env, adamc@157: 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@157: datatypes = #datatypes env, adamc@171: constructors = #constructors env, adamc@157: 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@156: fun sgiBinds env (sgi, loc) = 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@191: | SgiDatatype (x, n, xs, xncs) => adamc@156: let adamc@156: val env = pushCNamedAs env x n (KType, loc) NONE adamc@156: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamedAs env x' n' t adamc@191: end) adamc@156: env xncs adamc@156: end adamc@191: | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@162: let adamc@162: val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) adamc@162: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamedAs env x' n' t adamc@191: end) adamc@162: env xncs adamc@162: end 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@203: | SgiTable (x, n, c) => adamc@203: (case lookupStr env "Basis" of adamc@203: NONE => raise Fail "ElabEnv.sgiBinds: Can't find Basis" adamc@203: | SOME (n, _) => adamc@203: let adamc@203: val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) adamc@203: in adamc@203: pushENamedAs env x n t adamc@203: end) adamc@203: 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@158: SOME v => adamc@158: let adamc@158: val cons = adamc@158: case sgi of adamc@191: SgiDatatype (x, n, _, _) => IM.insert (cons, n, x) adamc@191: | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x) adamc@158: | _ => cons adamc@158: in adamc@158: SOME (v, (sgns, strs, cons)) adamc@158: end 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@191: | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) adamc@191: | SgiDatatypeImp (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@203: | SgiTable _ => 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@158: fun chaseMpath env (n, ms) = adamc@158: let adamc@158: val (_, sgn) = lookupStrNamed env n adamc@158: in adamc@158: foldl (fn (m, (str, sgn)) => adamc@158: case projectStr env {sgn = sgn, str = str, field = m} of adamc@158: NONE => raise Fail "kindof: Unknown substructure" adamc@158: | SOME sgn => ((StrProj (str, m), #2 sgn), sgn)) adamc@158: ((StrVar n, #2 sgn), sgn) ms adamc@158: end adamc@158: 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@191: | SgiDatatype (x, _, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE adamc@191: | SgiDatatypeImp (x, _, m1, ms, x', _, _) => adamc@158: if x = field then adamc@158: SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn)) adamc@158: else adamc@158: 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@157: fun projectDatatype env {sgn, str, field} = adamc@157: case #1 (hnormSgn env sgn) of adamc@157: SgnConst sgis => adamc@191: (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE adamc@191: | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE adamc@157: | _ => NONE) sgis of adamc@157: NONE => NONE adamc@191: | SOME ((xs, xncs), subs) => SOME (xs, adamc@191: map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) adamc@157: | _ => NONE adamc@157: adamc@174: fun projectConstructor env {sgn, str, field} = adamc@174: case #1 (hnormSgn env sgn) of adamc@174: SgnConst sgis => adamc@174: let adamc@191: fun consider (n, xs, xncs) = adamc@174: ListUtil.search (fn (x, n', to) => adamc@174: if x <> field then adamc@174: NONE adamc@174: else adamc@191: SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs adamc@174: in adamc@191: case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs) adamc@191: | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs) adamc@174: | _ => NONE) sgis of adamc@174: NONE => NONE adamc@191: | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to, adamc@191: sgnSubCon (str, subs) t) adamc@174: end adamc@174: | _ => NONE adamc@174: adamc@42: fun projectVal env {sgn, str, field} = adamc@42: case #1 (hnormSgn env sgn) of adamc@34: SgnConst sgis => adamc@162: let adamc@191: fun seek (n, xs, xncs) = adamc@162: ListUtil.search (fn (x, _, to) => adamc@162: if x = field then adamc@191: SOME (let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, #2 sgn) adamc@191: | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn) adamc@191: val k = (KType, #2 sgn) adamc@191: in adamc@191: foldr (fn (x, t) => (TCFun (Explicit, x, k, t), #2 sgn)) adamc@191: t xs adamc@191: end) adamc@162: else adamc@162: NONE) xncs adamc@162: in adamc@162: case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE adamc@191: | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs) adamc@191: | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs) adamc@162: | _ => NONE) sgis of adamc@162: NONE => NONE adamc@162: | SOME (c, subs) => SOME (sgnSubCon (str, subs) c) adamc@162: end 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@191: | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) adamc@191: | SgiDatatypeImp (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@203: | SgiTable _ => seek (sgis, sgns, strs, 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@157: fun declBinds env (d, loc) = adamc@157: case d of adamc@157: DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) adamc@191: | DDatatype (x, n, xs, xncs) => adamc@157: let adamc@157: val env = pushCNamedAs env x n (KType, loc) NONE adamc@191: val env = pushDatatype env n xs xncs adamc@157: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamedAs env x' n' t adamc@191: end) adamc@191: env xncs adamc@157: end adamc@191: | DDatatypeImp (x, n, m, ms, x', xs, xncs) => adamc@157: let adamc@157: val t = (CModProj (m, ms, x'), loc) adamc@157: val env = pushCNamedAs env x n (KType, loc) (SOME t) adamc@191: val env = pushDatatype env n xs xncs adamc@157: adamc@157: val t = (CNamed n, loc) adamc@157: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamedAs env x' n' t adamc@191: end) adamc@191: env xncs adamc@157: end adamc@157: | DVal (x, n, t, _) => pushENamedAs env x n t adamc@157: | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis adamc@157: | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn adamc@157: | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn adamc@157: | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn adamc@157: | DConstraint _ => env adamc@157: | DExport _ => env adamc@203: | DTable (x, n, c) => adamc@203: (case lookupStr env "Basis" of adamc@203: NONE => raise Fail "ElabEnv.declBinds: Can't find Basis" adamc@203: | SOME (n, _) => adamc@203: let adamc@203: val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) adamc@203: in adamc@203: pushENamedAs env x n t adamc@203: end) adamc@157: adamc@2: end