adamc@674: (* Copyright (c) 2008-2009, 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@623: val liftKindInKind = adamc@623: U.Kind.mapB {kind = fn bound => fn k => adamc@623: case k of adamc@623: KRel xn => adamc@623: if xn < bound then adamc@623: k adamc@623: else adamc@623: KRel (xn + 1) adamc@623: | _ => k, adamc@623: bind = fn (bound, _) => bound + 1} adamc@623: adamc@623: val liftKindInCon = adamc@623: U.Con.mapB {kind = fn bound => fn k => adamc@623: case k of adamc@623: KRel xn => adamc@623: if xn < bound then adamc@623: k adamc@623: else adamc@623: KRel (xn + 1) adamc@623: | _ => k, adamc@623: con = fn _ => fn c => c, adamc@623: bind = fn (bound, U.Con.RelK _) => bound + 1 adamc@623: | (bound, _) => bound} adamc@623: adamc@13: val liftConInCon = adamc@623: U.Con.mapB {kind = fn _ => 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@623: bind = fn (bound, U.Con.RelC _) => bound + 1 adamc@13: | (bound, _) => bound} adamc@13: adamc@13: val lift = liftConInCon 0 adamc@13: adamc@623: val liftKindInExp = adamc@623: U.Exp.mapB {kind = fn bound => fn k => adamc@623: case k of adamc@623: KRel xn => adamc@623: if xn < bound then adamc@623: k adamc@623: else adamc@623: KRel (xn + 1) adamc@623: | _ => k, adamc@623: con = fn _ => fn c => c, adamc@623: exp = fn _ => fn e => e, adamc@623: bind = fn (bound, U.Exp.RelK _) => bound + 1 adamc@623: | (bound, _) => bound} adamc@623: adamc@448: val liftConInExp = adamc@623: U.Exp.mapB {kind = fn _ => fn k => k, adamc@448: con = fn bound => fn c => adamc@448: case c of adamc@448: CRel xn => adamc@448: if xn < bound then adamc@448: c adamc@448: else adamc@448: CRel (xn + 1) adamc@448: | _ => c, adamc@448: exp = fn _ => fn e => e, adamc@448: bind = fn (bound, U.Exp.RelC _) => bound + 1 adamc@448: | (bound, _) => bound} adamc@448: adamc@211: val liftExpInExp = adamc@623: U.Exp.mapB {kind = fn _ => 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@448: val subExpInExp = adamc@623: U.Exp.mapB {kind = fn _ => fn k => k, adamc@448: con = fn _ => fn c => c, adamc@448: exp = fn (xn, rep) => fn e => adamc@448: case e of adamc@448: ERel xn' => adamc@448: (case Int.compare (xn', xn) of adamc@448: EQUAL => #1 rep adamc@448: | GREATER=> ERel (xn' - 1) adamc@448: | LESS => e) adamc@448: | _ => e, adamc@448: bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) adamc@448: | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) adamc@448: | (ctx, _) => ctx} adamc@448: 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@677: structure CS = BinarySetFn(CK) 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@467: | CkApp of class_key * class_key adamc@684: | CkOther of con 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@467: | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")" adamc@684: | CkOther _ => "Other" adamc@216: adamc@674: type class_key_n = class_key * int adamc@674: adamc@674: fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]" adamc@674: adamc@216: fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")" adamc@216: adamc@211: structure KK = struct adamc@674: type ord_key = class_key_n adamc@211: open Order adamc@674: 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@467: | (CkProj _, _) => LESS adamc@467: | (_, CkProj _) => GREATER adamc@467: adamc@467: | (CkApp (f1, x1), CkApp (f2, x2)) => adamc@674: join (compare' (f1, f2), adamc@674: fn () => compare' (x1, x2)) adamc@684: | (CkApp _, _) => LESS adamc@684: | (_, CkApp _) => GREATER adamc@684: adamc@684: | (CkOther _, CkOther _) => EQUAL adamc@674: fun compare ((k1, n1), (k2, n2)) = adamc@674: join (Int.compare (n1, n2), adamc@674: fn () => compare' (k1, k2)) adamc@211: end adamc@211: adamc@211: structure KM = BinaryMapFn(KK) adamc@211: adamc@675: type class = {ground : ((class_name * class_key) list * exp) KM.map, adamc@675: inclusions : exp CM.map} adamc@675: val empty_class = {ground = KM.empty, adamc@675: inclusions = CM.empty} adamc@211: adamc@419: fun printClasses cs = (print "Classes:\n"; adamc@675: CM.appi (fn (cn, {ground = km, ...} : class) => adamc@419: (print (cn2s cn ^ ":"); adamc@674: KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km; adamc@419: print "\n")) cs) adamc@216: adamc@2: type env = { adamc@623: renameK : int SM.map, adamc@623: relK : string list, adamc@623: 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@623: renameK = SM.empty, adamc@623: relK = [], adamc@623: 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@674: fun liftClassKey' ck = adamc@211: case ck of adamc@211: CkNamed _ => ck adamc@211: | CkRel n => CkRel (n + 1) adamc@211: | CkProj _ => ck adamc@674: | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2) adamc@684: | CkOther c => CkOther (lift c) adamc@674: adamc@674: fun liftClassKey (ck, n) = (liftClassKey' ck, n) adamc@211: adamc@623: fun pushKRel (env : env) x = adamc@623: let adamc@623: val renameK = SM.map (fn n => n+1) (#renameK env) adamc@623: in adamc@623: {renameK = SM.insert (renameK, x, 0), adamc@623: relK = x :: #relK env, adamc@623: adamc@623: renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k) adamc@623: | x => x) (#renameC env), adamc@623: relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env), adamc@623: namedC = #namedC env, adamc@623: adamc@623: datatypes = #datatypes env, adamc@623: constructors = #constructors env, adamc@623: adamc@623: classes = #classes env, adamc@623: adamc@623: renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c) adamc@623: | Named' (n, c) => Named' (n, c)) (#renameE env), adamc@623: relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), adamc@623: namedE = #namedE env, adamc@623: adamc@623: renameSgn = #renameSgn env, adamc@623: sgn = #sgn env, adamc@623: adamc@623: renameStr = #renameStr env, adamc@623: str = #str env adamc@623: } adamc@623: end adamc@623: adamc@623: fun lookupKRel (env : env) n = adamc@623: (List.nth (#relK env, n)) adamc@623: handle Subscript => raise UnboundRel n adamc@623: adamc@623: fun lookupK (env : env) x = SM.find (#renameK env, x) adamc@623: 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@623: {renameK = #renameK env, adamc@623: relK = #relK env, adamc@623: adamc@623: renameC = SM.insert (renameC, x, Rel' (0, k)), adamc@2: relC = (x, k) :: #relC env, adamc@514: namedC = #namedC env, adamc@9: adamc@157: datatypes = #datatypes env, adamc@171: constructors = #constructors env, adamc@157: adamc@674: classes = CM.map (fn class => adamc@675: {ground = KM.foldli (fn (ck, e, km) => adamc@675: KM.insert (km, liftClassKey ck, e)) adamc@675: KM.empty (#ground class), adamc@675: inclusions = #inclusions class}) adamc@211: (#classes env), adamc@211: adamc@328: renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) adamc@517: | Named' (n, c) => Named' (n, c)) (#renameE env), adamc@13: relE = map (fn (x, c) => (x, lift c)) (#relE env), adamc@514: 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@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@623: {renameK = #renameK env, adamc@623: relK = #relK env, adamc@623: adamc@623: 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@623: {renameK = #renameK env, adamc@623: relK = #relK env, adamc@623: adamc@623: 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@623: {renameK = #renameK env, adamc@623: relK = #relK env, adamc@623: adamc@623: 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@675: classes = CM.insert (#classes env, ClNamed n, empty_class), 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@403: 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@403: fun isClass (env : env) c = adamc@403: let adamc@403: fun find NONE = false adamc@403: | find (SOME c) = Option.isSome (CM.find (#classes env, c)) adamc@403: in adamc@403: find (class_name_in c) adamc@403: end adamc@403: adamc@684: fun class_key_in (all as (c, _)) = adamc@211: case c of adamc@684: CRel n => CkRel n adamc@684: | CNamed n => CkNamed n adamc@684: | CModProj x => CkProj x adamc@228: | CUnif (_, _, _, ref (SOME c)) => class_key_in c adamc@684: | CApp (c1, c2) => CkApp (class_key_in c1, class_key_in c2) adamc@684: | _ => CkOther all adamc@211: adamc@674: fun class_key_out loc = adamc@674: let adamc@674: fun cko k = adamc@674: case k of adamc@674: CkRel n => (CRel n, loc) adamc@674: | CkNamed n => (CNamed n, loc) adamc@674: | CkProj x => (CModProj x, loc) adamc@674: | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc) adamc@684: | CkOther c => c adamc@674: in adamc@674: cko adamc@674: end adamc@674: adamc@211: fun class_pair_in (c, _) = adamc@211: case c of adamc@211: CApp (f, x) => adamc@684: (case class_name_in f of adamc@684: SOME f => SOME (f, class_key_in x) adamc@211: | _ => NONE) adamc@452: | CUnif (_, _, _, ref (SOME c)) => class_pair_in c adamc@211: | _ => NONE adamc@211: adamc@674: fun sub_class_key (n, c) = adamc@674: let adamc@674: fun csk k = adamc@674: case k of adamc@684: CkRel n' => SOME (if n' = n then adamc@684: c adamc@684: else adamc@684: k) adamc@684: | CkNamed _ => SOME k adamc@684: | CkProj _ => SOME k adamc@684: | CkApp (k1, k2) => adamc@684: (case (csk k1, csk k2) of adamc@684: (SOME k1, SOME k2) => SOME (CkApp (k1, k2)) adamc@684: | _ => NONE) adamc@684: | CkOther _ => NONE adamc@674: in adamc@674: csk adamc@674: end adamc@674: adamc@211: fun resolveClass (env : env) c = adamc@674: let adamc@674: fun doPair (f, x) = adamc@674: case CM.find (#classes env, f) of adamc@674: NONE => NONE adamc@674: | SOME class => adamc@674: let adamc@674: val loc = #2 c adamc@675: adamc@675: fun tryIncs () = adamc@675: let adamc@675: fun tryIncs fs = adamc@675: case fs of adamc@675: [] => NONE adamc@675: | (f', e') :: fs => adamc@675: case doPair (f', x) of adamc@675: NONE => tryIncs fs adamc@675: | SOME e => adamc@675: let adamc@675: val e' = (ECApp (e', class_key_out loc x), loc) adamc@675: val e' = (EApp (e', e), loc) adamc@675: in adamc@675: SOME e' adamc@675: end adamc@675: in adamc@675: tryIncs (CM.listItemsi (#inclusions class)) adamc@675: end adamc@675: adamc@674: fun tryRules (k, args) = adamc@674: let adamc@674: val len = length args adamc@675: adamc@675: fun tryNext () = adamc@675: case k of adamc@675: CkApp (k1, k2) => tryRules (k1, k2 :: args) adamc@675: | _ => tryIncs () adamc@674: in adamc@675: case KM.find (#ground class, (k, length args)) of adamc@674: SOME (cs, e) => adamc@674: let adamc@674: val es = map (fn (cn, ck) => adamc@674: let adamc@674: val ck = ListUtil.foldli (fn (i, arg, ck) => adamc@684: case ck of adamc@684: NONE => NONE adamc@684: | SOME ck => adamc@684: sub_class_key (len - i - 1, adamc@684: arg) adamc@684: ck) adamc@684: (SOME ck) args adamc@674: in adamc@684: case ck of adamc@684: NONE => NONE adamc@684: | SOME ck => doPair (cn, ck) adamc@674: end) cs adamc@674: in adamc@674: if List.exists (not o Option.isSome) es then adamc@675: tryNext () adamc@674: else adamc@674: let adamc@674: val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc)) adamc@674: e args adamc@674: val e = foldr (fn (pf, e) => (EApp (e, pf), loc)) adamc@674: e (List.mapPartial (fn x => x) es) adamc@674: in adamc@674: SOME e adamc@674: end adamc@674: end adamc@675: | NONE => tryNext () adamc@674: end adamc@674: in adamc@674: tryRules (x, []) adamc@674: end adamc@674: in adamc@674: case class_pair_in c of adamc@674: SOME p => doPair p adamc@674: | _ => NONE adamc@674: end 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@675: val classes = CM.map (fn class => adamc@675: {ground = KM.map (fn (ps, e) => (ps, liftExp e)) (#ground class), adamc@675: inclusions = #inclusions class}) (#classes env) adamc@211: val classes = case class_pair_in t of adamc@211: NONE => classes adamc@211: | SOME (f, x) => adamc@403: case CM.find (classes, f) of adamc@403: NONE => classes adamc@403: | SOME class => adamc@403: let adamc@675: val class = {ground = KM.insert (#ground class, (x, 0), ([], (ERel 0, #2 t))), adamc@675: inclusions = #inclusions class} adamc@403: in adamc@403: CM.insert (classes, f, class) adamc@403: end adamc@9: in adamc@623: {renameK = #renameK env, adamc@623: relK = #relK env, adamc@623: adamc@623: 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@675: datatype rule = adamc@675: Normal of int * (class_name * class_key) list * class_key adamc@675: | Inclusion of class_name adamc@675: adamc@684: fun containsOther k = adamc@684: case k of adamc@684: CkOther _ => true adamc@684: | CkApp (k1, k2) => containsOther k1 orelse containsOther k2 adamc@684: | _ => false adamc@684: adamc@674: fun rule_in c = adamc@674: let adamc@674: fun quantifiers (c, nvars) = adamc@674: case #1 c of adamc@674: TCFun (_, _, _, c) => quantifiers (c, nvars + 1) adamc@674: | _ => adamc@674: let adamc@674: fun clauses (c, hyps) = adamc@674: case #1 c of adamc@674: TFun (hyp, c) => adamc@674: (case class_pair_in hyp of adamc@677: SOME (p as (_, CkRel _)) => clauses (c, p :: hyps) adamc@677: | _ => NONE) adamc@674: | _ => adamc@674: case class_pair_in c of adamc@674: NONE => NONE adamc@674: | SOME (cn, ck) => adamc@674: let adamc@674: fun dearg (ck, i) = adamc@674: if i >= nvars then adamc@684: if containsOther ck adamc@684: orelse List.exists (fn (_, k) => containsOther k) hyps then adamc@684: NONE adamc@684: else adamc@684: SOME (cn, Normal (nvars, hyps, ck)) adamc@674: else case ck of adamc@674: CkApp (ck, CkRel i') => adamc@674: if i' = i then adamc@674: dearg (ck, i + 1) adamc@674: else adamc@674: NONE adamc@674: | _ => NONE adamc@674: in adamc@674: dearg (ck, 0) adamc@674: end adamc@674: in adamc@674: clauses (c, []) adamc@674: end adamc@674: in adamc@675: case #1 c of adamc@675: TCFun (_, _, _, (TFun ((CApp (f1, (CRel 0, _)), _), adamc@675: (CApp (f2, (CRel 0, _)), _)), _)) => adamc@675: (case (class_name_in f1, class_name_in f2) of adamc@675: (SOME f1, SOME f2) => SOME (f2, Inclusion f1) adamc@675: | _ => NONE) adamc@675: | _ => quantifiers (c, 0) adamc@674: end adamc@674: adamc@677: fun inclusion (classes : class CM.map, init, inclusions, f, e : exp) = adamc@677: let adamc@677: fun search (f, fs) = adamc@677: if f = init then adamc@677: NONE adamc@677: else if CS.member (fs, f) then adamc@677: SOME fs adamc@677: else adamc@677: let adamc@677: val fs = CS.add (fs, f) adamc@677: in adamc@677: case CM.find (classes, f) of adamc@677: NONE => SOME fs adamc@677: | SOME {inclusions = fs', ...} => adamc@677: CM.foldli (fn (f', _, fs) => adamc@677: case fs of adamc@677: NONE => NONE adamc@677: | SOME fs => search (f', fs)) (SOME fs) fs' adamc@677: end adamc@677: in adamc@677: case search (f, CS.empty) of adamc@677: SOME _ => CM.insert (inclusions, f, e) adamc@677: | NONE => (ErrorMsg.errorAt (#2 e) "Type class inclusion would create a cycle"; adamc@677: inclusions) adamc@677: end adamc@677: adamc@9: fun pushENamedAs (env : env) x n t = adamc@211: let adamc@211: val classes = #classes env adamc@674: val classes = case rule_in t of adamc@211: NONE => classes adamc@675: | SOME (f, rule) => adamc@403: case CM.find (classes, f) of adamc@403: NONE => classes adamc@403: | SOME class => adamc@403: let adamc@675: val e = (ENamed n, #2 t) adamc@675: adamc@675: val class = adamc@675: case rule of adamc@675: Normal (nvars, hyps, x) => adamc@675: {ground = KM.insert (#ground class, (x, nvars), (hyps, e)), adamc@675: inclusions = #inclusions class} adamc@675: | Inclusion f' => adamc@675: {ground = #ground class, adamc@677: inclusions = inclusion (classes, f, #inclusions class, f', e)} adamc@403: in adamc@403: CM.insert (classes, f, class) adamc@403: end adamc@211: in adamc@623: {renameK = #renameK env, adamc@623: relK = #relK env, adamc@623: adamc@623: 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@471: fun checkENamed (env : env) n = adamc@471: Option.isSome (IM.find (#namedE env, n)) adamc@471: 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@623: {renameK = #renameK env, adamc@623: relK = #relK env, adamc@623: adamc@623: 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@563: | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) adamc@563: | 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@467: fun sgnS_con' (arg as (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@467: | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1), adamc@467: (sgnS_con' arg (#1 c2), #2 c2)) adamc@216: | _ => c adamc@216: adamc@674: fun sgnS_class_name (arg as (m1, ms', (sgns, strs, cons))) nm = adamc@674: case nm of adamc@674: ClProj (m1, ms, x) => adamc@674: (case IM.find (strs, m1) of adamc@674: NONE => nm adamc@674: | SOME m1x => ClProj (m1, ms' @ m1x :: ms, x)) adamc@674: | ClNamed n => adamc@674: (case IM.find (cons, n) of adamc@674: NONE => nm adamc@674: | SOME nx => ClProj (m1, ms', nx)) adamc@674: adamc@674: fun sgnS_class_key (arg as (m1, ms', (sgns, strs, cons))) k = adamc@674: case k of adamc@674: CkProj (m1, ms, x) => adamc@674: (case IM.find (strs, m1) of adamc@674: NONE => k adamc@674: | SOME m1x => CkProj (m1, ms' @ m1x :: ms, x)) adamc@674: | CkNamed n => adamc@674: (case IM.find (cons, n) of adamc@674: NONE => k adamc@674: | SOME nx => CkProj (m1, ms', nx)) adamc@674: | CkApp (k1, k2) => CkApp (sgnS_class_key arg k1, adamc@674: sgnS_class_key arg k2) adamc@674: | _ => k adamc@674: 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@563: | SgiClassAbs (x, n, _) => found (x, n) adamc@563: | SgiClass (x, n, _, _) => found (x, n) adamc@674: | SgiVal (x, n, c) => adamc@674: (case rule_in c of adamc@674: NONE => default () adamc@675: | SOME (cn, rule) => adamc@674: let adamc@675: val globalizeN = sgnS_class_name (m1, ms, fmap) adamc@674: val globalize = sgnS_class_key (m1, ms, fmap) adamc@216: adamc@674: fun unravel c = adamc@674: case c of adamc@674: ClNamed n => adamc@674: ((case lookupCNamed env n of adamc@674: (_, _, SOME c') => adamc@674: (case class_name_in c' of adamc@674: NONE => c adamc@674: | SOME k => unravel k) adamc@674: | _ => c) adamc@674: handle UnboundNamed _ => c) adamc@674: | _ => c adamc@674: adamc@674: val nc = adamc@674: case cn of adamc@674: ClNamed f => IM.find (newClasses, f) adamc@674: | _ => NONE adamc@674: in adamc@674: case nc of adamc@674: NONE => adamc@419: let adamc@419: val classes = adamc@419: case CM.find (classes, cn) of adamc@419: NONE => classes adamc@419: | SOME class => adamc@419: let adamc@675: val e = (EModProj (m1, ms, x), adamc@675: #2 sgn) adamc@675: adamc@675: val class = adamc@675: case rule of adamc@675: Normal (nvars, hyps, a) => adamc@675: {ground = adamc@675: KM.insert (#ground class, (globalize a, nvars), adamc@675: (map (fn (n, k) => adamc@675: (globalizeN n, adamc@675: globalize k)) hyps, e)), adamc@675: inclusions = #inclusions class} adamc@675: | Inclusion f' => adamc@675: {ground = #ground class, adamc@677: inclusions = inclusion (classes, cn, adamc@677: #inclusions class, adamc@675: globalizeN f', e)} adamc@419: in adamc@419: CM.insert (classes, cn, class) adamc@419: end adamc@419: in adamc@419: (classes, adamc@419: newClasses, adamc@419: fmap, adamc@419: env) adamc@419: end adamc@674: | SOME fx => adamc@674: let adamc@674: val cn = ClProj (m1, ms, fx) adamc@419: adamc@674: val classes = adamc@674: case CM.find (classes, cn) of adamc@674: NONE => classes adamc@674: | SOME class => adamc@674: let adamc@675: val e = (EModProj (m1, ms, x), #2 sgn) adamc@675: adamc@675: val class = adamc@675: case rule of adamc@675: Normal (nvars, hyps, a) => adamc@675: {ground = adamc@675: KM.insert (#ground class, (globalize a, nvars), adamc@675: (map (fn (n, k) => adamc@675: (globalizeN n, adamc@675: globalize k)) hyps, e)), adamc@675: inclusions = #inclusions class} adamc@675: | Inclusion f' => adamc@675: {ground = #ground class, adamc@677: inclusions = inclusion (classes, cn, adamc@677: #inclusions class, adamc@675: globalizeN f', e)} adamc@674: in adamc@674: CM.insert (classes, cn, class) adamc@674: end adamc@674: in adamc@674: (classes, adamc@674: newClasses, adamc@674: fmap, adamc@674: env) adamc@674: end adamc@674: end) 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@623: {renameK = #renameK env, adamc@623: relK = #relK env, adamc@623: adamc@623: 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@341: val k = (KType, loc) adamc@341: val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs adamc@341: adamc@341: val env = pushCNamedAs env x n k' 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@341: val k = (KType, loc) adamc@341: val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs adamc@341: adamc@341: val env = pushCNamedAs env x n k' (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@563: | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE adamc@563: | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c) adamc@459: 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@341: | SgiDatatype (x, _, xs, _) => adamc@158: if x = field then adamc@341: let adamc@341: val k = (KType, #2 sgn) adamc@341: val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs adamc@341: in adamc@341: SOME (k', NONE) adamc@341: end adamc@341: else adamc@341: NONE adamc@341: | SgiDatatypeImp (x, _, m1, ms, x', xs, _) => adamc@341: if x = field then adamc@341: let adamc@341: val k = (KType, #2 sgn) adamc@341: val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs adamc@341: in adamc@341: SOME (k', SOME (CModProj (m1, ms, x'), #2 sgn)) adamc@341: end adamc@158: else adamc@158: NONE adamc@563: | SgiClassAbs (x, _, k) => if x = field then adamc@563: SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), NONE) adamc@563: else adamc@563: NONE adamc@563: | SgiClass (x, _, k, c) => if x = field then adamc@563: SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), SOME c) adamc@563: else adamc@563: 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@467: val base = (CNamed n, #2 sgn) adamc@467: val nxs = length xs adamc@467: val base = ListUtil.foldli (fn (i, _, base) => adamc@467: (CApp (base, adamc@467: (CRel (nxs - i - 1), #2 sgn)), adamc@467: #2 sgn)) adamc@467: base xs adamc@467: adamc@191: val t = adamc@191: case to of adamc@467: NONE => base adamc@467: | SOME t => (TFun (t, base), #2 sgn) adamc@191: val k = (KType, #2 sgn) adamc@191: in adamc@467: foldr (fn (x, t) => (TCFun (Implicit, 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@563: | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) adamc@563: | 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@447: fun edeclBinds env (d, loc) = adamc@447: case d of adamc@447: EDVal (x, t, _) => pushERel env x t adamc@447: | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis adamc@447: 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@341: 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@705: | DTable (tn, x, n, c, _, cc) => adamc@205: let adamc@705: val ct = (CModProj (tn, [], "sql_table"), loc) adamc@705: val ct = (CApp (ct, c), loc) adamc@705: val ct = (CApp (ct, cc), loc) adamc@338: in adamc@705: pushENamedAs env x n ct adamc@338: end adamc@338: | DSequence (tn, x, n) => adamc@338: let adamc@338: val t = (CModProj (tn, [], "sql_sequence"), loc) adamc@205: in adamc@205: pushENamedAs env x n t adamc@205: end adamc@563: | DClass (x, n, k, c) => adamc@213: let adamc@563: val k = (KArrow (k, (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@459: | DCookie (tn, x, n, c) => adamc@459: let adamc@459: val t = (CApp ((CModProj (tn, [], "cookie"), loc), c), loc) adamc@459: in adamc@459: pushENamedAs env x n t adamc@459: end 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