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@211: val liftExpInExp = adamc@211: U.Exp.mapB {kind = fn k => k, adamc@211: con = fn _ => fn c => c, adamc@211: exp = fn bound => fn e => adamc@211: case e of adamc@211: ERel xn => adamc@211: if xn < bound then adamc@211: e adamc@211: else adamc@211: ERel (xn + 1) adamc@211: | _ => e, adamc@211: bind = fn (bound, U.Exp.RelE _) => bound + 1 adamc@211: | (bound, _) => bound} adamc@211: adamc@211: adamc@211: val liftExp = liftExpInExp 0 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@211: datatype class_name = adamc@211: ClNamed of int adamc@211: | ClProj of int * string list * string adamc@211: adamc@216: fun cn2s cn = adamc@216: case cn of adamc@216: ClNamed n => "Named(" ^ Int.toString n ^ ")" adamc@216: | ClProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" adamc@216: adamc@211: structure CK = struct adamc@211: type ord_key = class_name adamc@211: open Order adamc@211: fun compare x = adamc@211: case x of adamc@211: (ClNamed n1, ClNamed n2) => Int.compare (n1, n2) adamc@211: | (ClNamed _, _) => LESS adamc@211: | (_, ClNamed _) => GREATER adamc@211: adamc@211: | (ClProj (m1, ms1, x1), ClProj (m2, ms2, x2)) => adamc@211: join (Int.compare (m1, m2), adamc@211: fn () => join (joinL String.compare (ms1, ms2), adamc@211: fn () => String.compare (x1, x2))) adamc@211: end adamc@211: adamc@211: structure CM = BinaryMapFn(CK) adamc@211: adamc@211: datatype class_key = adamc@211: CkNamed of int adamc@211: | CkRel of int adamc@211: | CkProj of int * string list * string adamc@211: adamc@216: fun ck2s ck = adamc@216: case ck of adamc@216: CkNamed n => "Named(" ^ Int.toString n ^ ")" adamc@216: | CkRel n => "Rel(" ^ Int.toString n ^ ")" adamc@216: | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" adamc@216: adamc@216: fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")" adamc@216: adamc@211: structure KK = struct adamc@211: type ord_key = class_key adamc@211: open Order adamc@211: fun compare x = adamc@211: case x of adamc@211: (CkNamed n1, CkNamed n2) => Int.compare (n1, n2) adamc@211: | (CkNamed _, _) => LESS adamc@211: | (_, CkNamed _) => GREATER adamc@211: adamc@211: | (CkRel n1, CkRel n2) => Int.compare (n1, n2) adamc@211: | (CkRel _, _) => LESS adamc@211: | (_, CkRel _) => GREATER adamc@211: adamc@211: | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) => adamc@211: join (Int.compare (m1, m2), adamc@211: fn () => join (joinL String.compare (ms1, ms2), adamc@211: fn () => String.compare (x1, x2))) adamc@211: end adamc@211: adamc@211: structure KM = BinaryMapFn(KK) adamc@211: adamc@211: type class = { adamc@211: ground : exp KM.map adamc@211: } adamc@211: adamc@211: val empty_class = { adamc@211: ground = KM.empty adamc@211: } adamc@211: adamc@216: fun printClasses cs = CM.appi (fn (cn, {ground = km}) => adamc@216: (print (cn2s cn ^ ":"); adamc@216: KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km; adamc@216: print "\n")) cs adamc@216: 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@211: classes : class CM.map, adamc@211: 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@211: classes = CM.empty, adamc@211: 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@211: fun liftClassKey ck = adamc@211: case ck of adamc@211: CkNamed _ => ck adamc@211: | CkRel n => CkRel (n + 1) adamc@211: | CkProj _ => ck adamc@211: 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@211: classes = CM.map (fn class => { adamc@211: ground = KM.foldli (fn (ck, e, km) => adamc@211: KM.insert (km, liftClassKey ck, e)) adamc@211: KM.empty (#ground class) adamc@211: }) adamc@211: (#classes env), adamc@211: 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@211: classes = #classes env, adamc@211: 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@211: classes = #classes env, adamc@211: 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@211: fun pushClass (env : env) n = adamc@211: {renameC = #renameC env, adamc@211: relC = #relC env, adamc@211: namedC = #namedC env, adamc@211: adamc@211: datatypes = #datatypes env, adamc@211: constructors = #constructors env, adamc@211: adamc@211: classes = CM.insert (#classes env, ClNamed n, {ground = KM.empty}), adamc@211: adamc@211: renameE = #renameE env, adamc@211: relE = #relE env, adamc@211: namedE = #namedE env, adamc@211: adamc@211: renameSgn = #renameSgn env, adamc@211: sgn = #sgn env, adamc@211: adamc@211: renameStr = #renameStr env, adamc@211: str = #str env} adamc@211: adamc@211: fun class_name_in (c, _) = adamc@211: case c of adamc@211: CNamed n => SOME (ClNamed n) adamc@211: | CModProj x => SOME (ClProj x) adamc@228: | CUnif (_, _, _, ref (SOME c)) => class_name_in c adamc@211: | _ => NONE adamc@211: adamc@211: fun class_key_in (c, _) = adamc@211: case c of adamc@211: CRel n => SOME (CkRel n) adamc@211: | CNamed n => SOME (CkNamed n) adamc@211: | CModProj x => SOME (CkProj x) adamc@228: | CUnif (_, _, _, ref (SOME c)) => class_key_in c adamc@211: | _ => NONE adamc@211: adamc@211: fun class_pair_in (c, _) = adamc@211: case c of adamc@211: CApp (f, x) => adamc@211: (case (class_name_in f, class_key_in x) of adamc@211: (SOME f, SOME x) => SOME (f, x) adamc@211: | _ => NONE) adamc@211: | _ => NONE adamc@211: adamc@211: fun resolveClass (env : env) c = adamc@211: case class_pair_in c of adamc@211: SOME (f, x) => adamc@211: (case CM.find (#classes env, f) of adamc@211: NONE => NONE adamc@211: | SOME class => adamc@211: case KM.find (#ground class, x) of adamc@211: NONE => NONE adamc@211: | SOME e => SOME e) adamc@211: | _ => NONE adamc@211: 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@211: adamc@211: val classes = CM.map (fn class => { adamc@211: ground = KM.map liftExp (#ground class) adamc@211: }) (#classes env) adamc@211: val classes = case class_pair_in t of adamc@211: NONE => classes adamc@211: | SOME (f, x) => adamc@211: let adamc@211: val class = Option.getOpt (CM.find (classes, f), empty_class) adamc@211: val class = { adamc@211: ground = KM.insert (#ground class, x, (ERel 0, #2 t)) adamc@211: } adamc@211: in adamc@211: CM.insert (classes, f, class) adamc@211: end 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@211: classes = classes, adamc@211: 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@211: let adamc@211: val classes = #classes env adamc@211: val classes = case class_pair_in t of adamc@211: NONE => classes adamc@211: | SOME (f, x) => adamc@211: let adamc@211: val class = Option.getOpt (CM.find (classes, f), empty_class) adamc@211: val class = { adamc@211: ground = KM.insert (#ground class, x, (ENamed n, #2 t)) adamc@211: } adamc@211: in adamc@211: CM.insert (classes, f, class) adamc@211: end adamc@211: in adamc@211: {renameC = #renameC env, adamc@211: relC = #relC env, adamc@211: namedC = #namedC env, adamc@9: adamc@211: datatypes = #datatypes env, adamc@211: constructors = #constructors env, adamc@157: adamc@211: classes = classes, adamc@31: adamc@211: renameE = SM.insert (#renameE env, x, Named' (n, t)), adamc@211: relE = #relE env, adamc@211: namedE = IM.insert (#namedE env, n, (x, t)), adamc@211: adamc@211: renameSgn = #renameSgn env, adamc@211: sgn = #sgn env, adamc@211: adamc@211: renameStr = #renameStr env, adamc@211: str = #str env} adamc@211: end 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@211: classes = #classes env, adamc@211: 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 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@203: adamc@216: fun sgiSeek (sgi, (sgns, strs, cons)) = adamc@216: case sgi of adamc@216: SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) adamc@216: | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) adamc@216: | SgiDatatype (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) adamc@216: | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x)) adamc@216: | SgiVal _ => (sgns, strs, cons) adamc@216: | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons) adamc@216: | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons) adamc@216: | SgiConstraint _ => (sgns, strs, cons) adamc@216: | SgiTable _ => (sgns, strs, cons) adamc@216: | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x)) adamc@216: | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) adamc@216: 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@216: let adamc@216: val (sgns, strs, cons) = sgiSeek (sgi, (sgns, strs, cons)) adamc@216: in adamc@216: seek (sgis, sgns, strs, cons) adamc@216: end 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@216: fun sgnS_con' (m1, ms', (sgns, strs, cons)) c = adamc@216: case c of adamc@216: CModProj (m1, ms, x) => adamc@216: (case IM.find (strs, m1) of adamc@216: NONE => c adamc@216: | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) adamc@216: | CNamed n => adamc@216: (case IM.find (cons, n) of adamc@216: NONE => c adamc@216: | SOME nx => CModProj (m1, ms', nx)) adamc@216: | _ => c adamc@216: 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 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@211: adamc@211: adamc@211: and projectSgn env {sgn, str, field} = adamc@211: case #1 (hnormSgn env sgn) of adamc@211: SgnConst sgis => adamc@211: (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of adamc@211: NONE => NONE adamc@211: | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) adamc@211: | SgnError => SOME (SgnError, ErrorMsg.dummySpan) adamc@211: | _ => NONE adamc@211: adamc@211: and 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@211: fun enrichClasses env classes (m1, ms) sgn = adamc@59: case #1 (hnormSgn env sgn) of adamc@59: SgnConst sgis => adamc@211: let adamc@218: val (classes, _, _, _) = adamc@218: foldl (fn (sgi, (classes, newClasses, fmap, env)) => adamc@211: let adamc@211: fun found (x, n) = adamc@211: (CM.insert (classes, adamc@211: ClProj (m1, ms, x), adamc@211: empty_class), adamc@216: IM.insert (newClasses, n, x), adamc@218: sgiSeek (#1 sgi, fmap), adamc@218: env) adamc@216: adamc@218: fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env) adamc@211: in adamc@211: case #1 sgi of adamc@217: SgiStr (x, _, sgn) => adamc@217: (enrichClasses env classes (m1, ms @ [x]) sgn, adamc@217: newClasses, adamc@218: sgiSeek (#1 sgi, fmap), adamc@218: env) adamc@218: | SgiSgn (x, n, sgn) => adamc@218: (classes, adamc@218: newClasses, adamc@218: fmap, adamc@218: pushSgnNamedAs env x n sgn) adamc@218: adamc@217: | SgiClassAbs xn => found xn adamc@211: | SgiClass (x, n, _) => found (x, n) adamc@216: | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) => adamc@216: (case IM.find (newClasses, f) of adamc@216: NONE => default () adamc@216: | SOME fx => adamc@216: case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of adamc@216: NONE => default () adamc@216: | SOME ck => adamc@216: let adamc@216: val cn = ClProj (m1, ms, fx) adamc@216: val class = Option.getOpt (CM.find (classes, cn), empty_class) adamc@216: val class = { adamc@216: ground = KM.insert (#ground class, ck, adamc@216: (EModProj (m1, ms, x), #2 sgn)) adamc@216: } adamc@216: adamc@216: in adamc@216: (CM.insert (classes, cn, class), adamc@216: newClasses, adamc@218: fmap, adamc@218: env) adamc@216: end) adamc@217: | SgiVal _ => default () adamc@216: | _ => default () adamc@211: end) adamc@218: (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis adamc@211: in adamc@211: classes adamc@211: end adamc@211: | _ => classes adamc@211: adamc@211: fun pushStrNamedAs (env : env) x n sgn = adamc@211: {renameC = #renameC env, adamc@211: relC = #relC env, adamc@211: namedC = #namedC env, adamc@211: adamc@211: datatypes = #datatypes env, adamc@211: constructors = #constructors env, adamc@211: adamc@211: classes = enrichClasses env (#classes env) (n, []) sgn, adamc@211: adamc@211: renameE = #renameE env, adamc@211: relE = #relE env, adamc@211: namedE = #namedE env, adamc@211: adamc@211: renameSgn = #renameSgn env, adamc@211: sgn = #sgn env, adamc@211: adamc@211: renameStr = SM.insert (#renameStr env, x, (n, sgn)), adamc@211: str = IM.insert (#str env, n, (x, sgn))} adamc@211: adamc@211: fun pushStrNamed env x sgn = adamc@211: let adamc@211: val n = !namedCounter adamc@211: in adamc@211: namedCounter := n + 1; adamc@211: (pushStrNamedAs env x n sgn, n) adamc@211: end adamc@211: adamc@211: fun sgiBinds env (sgi, loc) = adamc@211: case sgi of adamc@211: SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE adamc@211: | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) adamc@211: | SgiDatatype (x, n, xs, xncs) => adamc@211: let adamc@211: val env = pushCNamedAs env x n (KType, loc) NONE adamc@211: in adamc@211: foldl (fn ((x', n', to), env) => adamc@211: let adamc@211: val t = adamc@211: case to of adamc@211: NONE => (CNamed n, loc) adamc@211: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@211: adamc@211: val k = (KType, loc) adamc@211: val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs adamc@211: in adamc@211: pushENamedAs env x' n' t adamc@211: end) adamc@211: env xncs adamc@211: end adamc@211: | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@211: let adamc@211: val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) adamc@211: in adamc@211: foldl (fn ((x', n', to), env) => adamc@211: let adamc@211: val t = adamc@211: case to of adamc@211: NONE => (CNamed n, loc) adamc@211: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@211: adamc@211: val k = (KType, loc) adamc@211: val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs adamc@211: in adamc@211: pushENamedAs env x' n' t adamc@211: end) adamc@211: env xncs adamc@211: end adamc@211: | SgiVal (x, n, t) => pushENamedAs env x n t adamc@211: | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn adamc@211: | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn adamc@211: | SgiConstraint _ => env adamc@211: adamc@211: | SgiTable (tn, x, n, c) => adamc@211: let adamc@211: val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc) adamc@211: in adamc@211: pushENamedAs env x n t adamc@211: end adamc@211: adamc@211: | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE adamc@211: | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c) adamc@211: adamc@211: adamc@211: fun sgnSubCon x = adamc@211: ElabUtil.Con.map {kind = id, adamc@211: con = sgnS_con x} 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@216: | SgiClassAbs (x, _) => if x = field then adamc@216: SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), NONE) adamc@216: else adamc@216: NONE adamc@216: | SgiClass (x, _, c) => if x = field then adamc@216: SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), SOME c) adamc@216: else adamc@216: 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@211: | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) adamc@211: | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), 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@297: val k = (KType, loc) adamc@297: val nxs = length xs adamc@297: val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) => adamc@297: ((CApp (tb, (CRel (nxs - i - 1), loc)), loc), adamc@297: (KArrow (k, kb), loc))) adamc@297: ((CNamed n, loc), k) xs adamc@297: adamc@297: val env = pushCNamedAs env x n kb 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@297: NONE => tb adamc@297: | SOME t => (TFun (t, tb), loc) adamc@297: val t = foldr (fn (x, t) => (TCFun (Implicit, 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@297: val k = (KType, loc) adamc@297: val nxs = length xs adamc@297: val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) => adamc@297: ((CApp (tb, (CRel (nxs - i - 1), loc)), loc), adamc@297: (KArrow (k, kb), loc))) adamc@297: ((CNamed n, loc), k) xs adamc@297: adamc@297: val t' = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs adamc@297: val env = pushCNamedAs env x n kb (SOME t') 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@297: NONE => tb adamc@297: | SOME t => (TFun (t, tb), loc) adamc@297: val t = foldr (fn (x, t) => (TCFun (Implicit, 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@205: | DTable (tn, x, n, c) => adamc@205: let adamc@205: val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc) adamc@205: in adamc@205: pushENamedAs env x n t adamc@205: end adamc@213: | DClass (x, n, c) => adamc@213: let adamc@213: val k = (KArrow ((KType, loc), (KType, loc)), loc) adamc@213: val env = pushCNamedAs env x n k (SOME c) adamc@213: in adamc@213: pushClass env n adamc@213: end adamc@271: | DDatabase _ => env adamc@157: adamc@243: fun patBinds env (p, loc) = adamc@243: case p of adamc@243: PWild => env adamc@243: | PVar (x, t) => pushERel env x t adamc@243: | PPrim _ => env adamc@243: | PCon (_, _, _, NONE) => env adamc@243: | PCon (_, _, _, SOME p) => patBinds env p adamc@243: | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps adamc@243: adamc@2: end