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@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) adam@1303: | CUnif (nl, loc, k, s, r) => CUnif (nl+1, loc, k, s, r) 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: adam@1303: fun mliftConInCon by c = adam@1303: if by = 0 then adam@1303: c adam@1303: else adam@1303: U.Con.mapB {kind = fn _ => fn k => k, adam@1303: con = fn bound => fn c => adam@1303: case c of adam@1303: CRel xn => adam@1303: if xn < bound then adam@1303: c adam@1303: else adam@1303: CRel (xn + by) adam@1303: | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r) adam@1303: | _ => c, adam@1303: bind = fn (bound, U.Con.RelC _) => bound + 1 adam@1303: | (bound, _) => bound} 0 c adam@1303: adam@1303: val () = U.mliftConInCon := mliftConInCon adam@1303: 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) adam@1303: | CUnif (nl, loc, k, s, r) => CUnif (nl+1, loc, k, s, r) 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@711: fun class_name_out cn = adamc@711: case cn of adamc@711: ClNamed n => (CNamed n, ErrorMsg.dummySpan) adamc@711: | ClProj x => (CModProj x, ErrorMsg.dummySpan) adamc@711: 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@711: type class = {ground : (con * exp) list, adamc@711: rules : (int * con list * con * exp) list} adamc@711: val empty_class = {ground = [], adamc@711: rules = []} 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@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@711: classes = CM.map (fn cl => {ground = map (fn (c, e) => adamc@711: (liftKindInCon 0 c, adamc@711: e)) adamc@711: (#ground cl), adamc@711: rules = #rules cl}) adamc@711: (#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@711: {ground = map (fn (c, e) => adamc@711: (liftConInCon 0 c, adamc@711: e)) adamc@711: (#ground class), adamc@711: rules = #rules 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@711: fun listClasses (env : env) = adamc@711: map (fn (cn, {ground, rules}) => adamc@711: (class_name_out cn, adamc@711: ground adamc@711: @ map (fn (nvs, cs, c, e) => adamc@711: let adamc@711: val loc = #2 c adamc@711: val c = foldr (fn (c', c) => (TFun (c', c), loc)) c cs adamc@711: val c = ListUtil.foldli (fn (n, (), c) => (TCFun (Explicit, adamc@711: "x" ^ Int.toString n, adamc@711: (KError, loc), adamc@711: c), loc)) adamc@711: c (List.tabulate (nvs, fn _ => ())) adamc@711: in adamc@711: (c, e) adamc@711: end) rules)) (CM.listItemsi (#classes env)) adamc@711: 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) adam@1303: | 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@711: fun class_head_in c = adamc@711: case #1 c of adamc@711: CApp (f, _) => class_head_in f adam@1303: | CUnif (_, _, _, _, ref (SOME c)) => class_head_in c adamc@711: | _ => class_name_in c adamc@211: adamc@711: exception Unify adamc@711: adamc@711: fun unifyKinds (k1, k2) = adamc@711: case (#1 k1, #1 k2) of adamc@711: (KType, KType) => () adamc@711: | (KArrow (d1, r1), KArrow (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2)) adamc@711: | (KName, KName) => () adamc@711: | (KRecord k1, KRecord k2) => unifyKinds (k1, k2) adamc@711: | (KUnit, KUnit) => () adamc@711: | (KTuple ks1, KTuple ks2) => (ListPair.appEq unifyKinds (ks1, ks2) adamc@711: handle ListPair.UnequalLengths => raise Unify) adamc@711: | (KUnif (_, _, ref (SOME k1)), _) => unifyKinds (k1, k2) adamc@711: | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2) adamc@711: | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify adamc@711: | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2) adamc@711: | _ => raise Unify adamc@711: adamc@904: fun eqCons (c1, c2) = adamc@904: case (#1 c1, #1 c2) of adam@1303: (CUnif (nl, _, _, _, ref (SOME c1)), _) => eqCons (mliftConInCon nl c1, c2) adam@1303: | (_, CUnif (nl, _, _, _, ref (SOME c2))) => eqCons (c1, mliftConInCon nl c2) adamc@904: adamc@904: | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify adamc@904: adamc@904: | (TFun (d1, r1), TFun (d2, r2)) => (eqCons (d1, d2); eqCons (r1, r2)) adamc@904: | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); eqCons (r1, r2)) adamc@904: | (TRecord c1, TRecord c2) => eqCons (c1, c2) adamc@904: | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) => adamc@904: (eqCons (a1, a2); eqCons (b1, b2); eqCons (c1, c2)) adamc@904: adamc@904: | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify adamc@904: | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) => adamc@904: if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify adamc@904: | (CApp (f1, x1), CApp (f2, x2)) => (eqCons (f1, f2); eqCons (x1, x2)) adamc@904: | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); eqCons (b1, b2)) adamc@904: adamc@904: | (CKAbs (_, b1), CKAbs (_, b2)) => eqCons (b1, b2) adamc@904: | (CKApp (c1, k1), CKApp (c2, k2)) => (eqCons (c1, c2); unifyKinds (k1, k2)) adamc@904: | (TKFun (_, c1), TKFun (_, c2)) => eqCons (c1, c2) adamc@904: adamc@904: | (CName s1, CName s2) => if s1 = s2 then () else raise Unify adamc@904: adamc@904: | (CRecord (k1, xcs1), CRecord (k2, xcs2)) => adamc@904: (unifyKinds (k1, k2); adamc@904: ListPair.appEq (fn ((x1, c1), (x2, c2)) => (eqCons (x1, x2); eqCons (c1, c2))) (xcs1, xcs2) adamc@904: handle ListPair.UnequalLengths => raise Unify) adamc@904: | (CConcat (f1, x1), CConcat (f2, x2)) => (eqCons (f1, f2); eqCons (x1, x2)) adamc@904: | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2)) adamc@904: adamc@904: | (CUnit, CUnit) => () adamc@904: adamc@904: | (CTuple cs1, CTuple cs2) => (ListPair.appEq (eqCons) (cs1, cs2) adamc@904: handle ListPair.UnequalLengths => raise Unify) adamc@904: | (CProj (c1, n1), CProj (c2, n2)) => (eqCons (c1, c2); adamc@904: if n1 = n2 then () else raise Unify) adamc@904: adamc@904: | _ => raise Unify adamc@904: adam@1325: fun unifyCons (hnorm : con -> con) rs = adamc@674: let adamc@711: fun unify d (c1, c2) = adam@1325: case (#1 (hnorm c1), #1 (hnorm c2)) of adam@1303: (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2) adam@1303: | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2) adamc@711: adamc@750: | (CUnif _, _) => () adamc@750: adamc@711: | (c1', CRel n2) => adamc@711: if n2 < d then adamc@711: case c1' of adamc@711: CRel n1 => if n1 = n2 then () else raise Unify adamc@711: | _ => raise Unify adamc@711: else if n2 - d >= length rs then adamc@711: case c1' of adamc@711: CRel n1 => if n1 = n2 - length rs then () else raise Unify adamc@711: | _ => raise Unify adamc@711: else adamc@711: let adamc@711: val r = List.nth (rs, n2 - d) adamc@711: in adamc@711: case !r of adamc@711: NONE => r := SOME c1 adamc@904: | SOME c2 => eqCons (c1, c2) adamc@711: end adamc@711: adamc@711: | (TFun (d1, r1), TFun (d2, r2)) => (unify d (d1, d2); unify d (r1, r2)) adamc@711: | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (d + 1) (r1, r2)) adamc@711: | (TRecord c1, TRecord c2) => unify d (c1, c2) adamc@711: | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) => adamc@711: (unify d (a1, a2); unify d (b1, b2); unify d (c1, c2)) adamc@711: adamc@711: | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify adamc@711: | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) => adamc@711: if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify adamc@711: | (CApp (f1, x1), CApp (f2, x2)) => (unify d (f1, f2); unify d (x1, x2)) adamc@711: | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (d + 1) (b1, b2)) adamc@711: adamc@711: | (CKAbs (_, b1), CKAbs (_, b2)) => unify d (b1, b2) adamc@711: | (CKApp (c1, k1), CKApp (c2, k2)) => (unify d (c1, c2); unifyKinds (k1, k2)) adamc@711: | (TKFun (_, c1), TKFun (_, c2)) => unify d (c1, c2) adamc@711: adamc@711: | (CName s1, CName s2) => if s1 = s2 then () else raise Unify adamc@711: adamc@711: | (CRecord (k1, xcs1), CRecord (k2, xcs2)) => adamc@711: (unifyKinds (k1, k2); adamc@711: ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify d (x1, x2); unify d (c1, c2))) (xcs1, xcs2) adamc@711: handle ListPair.UnequalLengths => raise Unify) adamc@711: | (CConcat (f1, x1), CConcat (f2, x2)) => (unify d (f1, f2); unify d (x1, x2)) adamc@711: | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2)) adamc@711: adamc@711: | (CUnit, CUnit) => () adamc@711: adamc@711: | (CTuple cs1, CTuple cs2) => (ListPair.appEq (unify d) (cs1, cs2) adamc@711: handle ListPair.UnequalLengths => raise Unify) adamc@711: | (CProj (c1, n1), CProj (c2, n2)) => (unify d (c1, c2); adamc@711: if n1 = n2 then () else raise Unify) adamc@711: adamc@711: | _ => raise Unify adamc@674: in adamc@711: unify adamc@674: end adamc@674: adam@1325: fun tryUnify hnorm nRs (c1, c2) = adamc@674: let adamc@711: val rs = List.tabulate (nRs, fn _ => ref NONE) adamc@674: in adam@1325: (unifyCons hnorm rs 0 (c1, c2); adamc@711: SOME (map (fn r => case !r of adamc@711: NONE => raise Unify adamc@711: | SOME c => c) rs)) adamc@711: handle Unify => NONE adamc@674: end adamc@674: adamc@711: fun unifySubst (rs : con list) = adamc@711: U.Con.mapB {kind = fn _ => fn k => k, adamc@711: con = fn d => fn c => adamc@711: case c of adamc@711: CRel n => adamc@711: if n < d then adamc@711: c adamc@711: else adamc@711: #1 (List.nth (rs, n - d)) adamc@711: | _ => c, adamc@711: bind = fn (d, U.Con.RelC _) => d + 1 adamc@711: | (d, _) => d} adamc@711: 0 adamc@711: adamc@753: exception Bad of con * con adamc@750: adamc@754: val hasUnif = U.Con.exists {kind = fn _ => false, adam@1303: con = fn CUnif (_, _, _, _, ref NONE) => true adamc@754: | _ => false} adamc@754: adamc@754: fun startsWithUnif c = adamc@754: let adamc@754: fun firstArg (c, acc) = adamc@754: case #1 c of adamc@754: CApp (f, x) => firstArg (f, SOME x) adamc@754: | _ => acc adamc@754: in adamc@754: case firstArg (c, NONE) of adamc@754: NONE => false adamc@754: | SOME x => hasUnif x adamc@754: end adamc@754: adamc@753: fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = adamc@674: let adamc@711: fun resolve c = adamc@711: let adamc@711: fun doHead f = adamc@711: case CM.find (#classes env, f) of adamc@711: NONE => NONE adamc@711: | SOME class => adamc@711: let adamc@711: val loc = #2 c adamc@675: adamc@753: fun generalize (c as (_, loc)) = adamc@753: case #1 c of adamc@753: CApp (f, x) => adamc@753: let adamc@753: val (f, equate) = generalize f adamc@753: adamc@753: fun isRecord () = adamc@753: let adamc@753: val rk = ref NONE adamc@753: val k = (KUnif (loc, "k", rk), loc) adamc@753: val r = ref NONE adam@1303: val rc = (CUnif (0, loc, k, "x", r), loc) adamc@753: in adamc@753: ((CApp (f, rc), loc), adamc@753: fn () => (if consEq (rc, x) then adamc@753: true adamc@753: else adamc@753: (raise Bad (rc, x); adamc@753: false)) adamc@753: andalso equate ()) adamc@753: end adamc@753: in adamc@753: case #1 x of adamc@753: CConcat _ => isRecord () adamc@753: | CRecord _ => isRecord () adamc@753: | _ => ((CApp (f, x), loc), equate) adamc@753: end adamc@753: | _ => (c, fn () => true) adamc@753: adamc@753: val (c, equate) = generalize c adamc@753: adamc@711: fun tryRules rules = adamc@711: case rules of adamc@675: [] => NONE adamc@711: | (nRs, cs, c', e) :: rules' => adam@1325: case tryUnify hnorm nRs (c, c') of adamc@711: NONE => tryRules rules' adamc@711: | SOME rs => adamc@675: let adamc@711: val eos = map (resolve o unifySubst rs) cs adamc@675: in adamc@750: if List.exists (not o Option.isSome) eos adamc@753: orelse not (equate ()) adamc@753: orelse not (consEq (c, unifySubst rs c')) then adamc@711: tryRules rules' adamc@711: else adamc@711: let adamc@711: val es = List.mapPartial (fn x => x) eos adamc@711: adamc@711: val e = foldr (fn (c, e) => (ECApp (e, c), loc)) e rs adamc@711: val e = foldl (fn (e', e) => (EApp (e, e'), loc)) e es adamc@711: in adamc@711: SOME e adamc@711: end adamc@675: end adamc@711: adamc@711: fun rules () = tryRules (#rules class) adamc@711: adamc@711: fun tryGrounds ces = adamc@711: case ces of adamc@711: [] => rules () adamc@711: | (c', e) :: ces' => adam@1325: case tryUnify hnorm 0 (c, c') of adamc@711: NONE => tryGrounds ces' adamc@711: | SOME _ => SOME e adamc@675: in adamc@711: tryGrounds (#ground class) adamc@675: end adamc@711: in adamc@754: if startsWithUnif c then adamc@754: NONE adamc@754: else adamc@754: case #1 c of adamc@754: TRecord c => adamc@754: (case #1 (hnorm c) of adamc@754: CRecord (_, xts) => adamc@754: let adamc@754: fun resolver (xts, acc) = adamc@754: case xts of adamc@754: [] => SOME (ERecord acc, #2 c) adamc@754: | (x, t) :: xts => adamc@754: let adamc@754: val t = hnorm t adamc@750: adamc@754: val t = case t of adamc@754: (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc) adamc@754: | _ => t adamc@754: in adamc@754: case resolve t of adamc@754: NONE => NONE adamc@754: | SOME e => resolver (xts, (x, e, t) :: acc) adamc@754: end adamc@754: in adamc@754: resolver (xts, []) adamc@754: end adamc@754: | _ => NONE) adamc@754: | _ => adamc@754: case class_head_in c of adamc@754: SOME f => doHead f adamc@754: | _ => NONE adamc@711: end adamc@674: in adamc@711: resolve 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@711: {ground = map (fn (c, e) => (c, liftExp e)) (#ground class), adamc@711: rules = #rules class}) (#classes env) adamc@711: val classes = case class_head_in t of adamc@211: NONE => classes adamc@711: | SOME f => adamc@403: case CM.find (classes, f) of adamc@403: NONE => classes adamc@403: | SOME class => adamc@403: let adamc@711: val class = {ground = (t, (ERel 0, #2 t)) :: #ground class, adamc@711: rules = #rules 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@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@711: (case class_head_in hyp of adamc@711: SOME _ => clauses (c, hyp :: hyps) adamc@711: | NONE => NONE) adamc@674: | _ => adamc@711: case class_head_in c of adamc@674: NONE => NONE adamc@711: | SOME f => SOME (f, nvars, rev hyps, c) adamc@674: in adamc@674: clauses (c, []) adamc@674: end adamc@674: in adamc@711: quantifiers (c, 0) 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@711: | SOME (f, nvs, cs, c) => 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@711: {ground = #ground class, adamc@711: rules = (nvs, cs, c, e) :: #rules class} 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@805: | SgiDatatype dts => (sgns, strs, foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts) 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@805: SgiDatatype dts => foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts 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@721: fun sgnS_con' (m1, ms', (sgns, strs, cons)) = adamc@721: U.Con.map {kind = fn x => x, adamc@721: con = fn c => adamc@721: case c of adamc@721: CModProj (m1, ms, x) => adamc@721: (case IM.find (strs, m1) of adamc@721: NONE => c adamc@721: | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) adamc@721: | CNamed n => adamc@721: (case IM.find (cons, n) of adamc@721: NONE => c adamc@721: | SOME nx => CModProj (m1, ms', nx)) adamc@721: | _ => 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@1058: | SOME sgn => hnormSgn env 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@849: fun manifest (m, ms, loc) = adamc@849: foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms adamc@849: 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@849: let adamc@849: val str = manifest (m1, ms, #2 sgi) adamc@849: val sgn' = sgnSubSgn (str, fmap) sgn adamc@849: in adamc@849: (enrichClasses env classes (m1, ms @ [x]) sgn', adamc@849: newClasses, adamc@849: sgiSeek (#1 sgi, fmap), adamc@849: env) adamc@849: end 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@711: | SOME (cn, nvs, cs, c) => adamc@674: let adamc@711: val loc = #2 c adamc@721: val globalize = sgnS_con' (m1, ms, fmap) 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@711: val e = (EModProj (m1, ms, x), #2 sgn) adamc@675: adamc@675: val class = adamc@711: {ground = #ground class, adamc@711: rules = (nvs, adamc@711: map globalize cs, adamc@711: globalize c, adamc@711: e) :: #rules class} 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@711: {ground = #ground class, adamc@711: rules = (nvs, adamc@711: map globalize cs, adamc@711: globalize c, adamc@711: e) :: #rules class} 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@805: | SgiDatatype dts => adamc@211: let adamc@805: fun doOne ((x, n, xs, xncs), env) = adamc@805: let adamc@805: val k = (KType, loc) adamc@805: val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs adamc@341: adamc@805: val env = pushCNamedAs env x n k' NONE adamc@805: in adamc@805: foldl (fn ((x', n', to), env) => adamc@805: let adamc@805: val t = adamc@805: case to of adamc@805: NONE => (CNamed n, loc) adamc@805: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@805: adamc@805: val k = (KType, loc) adamc@805: val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs adamc@805: in adamc@805: pushENamedAs env x' n' t adamc@805: end) adamc@805: env xncs adamc@805: end adamc@211: in adamc@805: foldl doOne env dts 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@711: | SgiClassAbs (x, n, k) => pushCNamedAs env x n k NONE adamc@711: | SgiClass (x, n, k, c) => pushCNamedAs env x n k (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@805: | SgiDatatype dts => adamc@805: (case List.find (fn (x, _, xs, _) => x = field) dts of adamc@805: SOME (_, _, xs, _) => adamc@805: let adamc@805: val k = (KType, #2 sgn) adamc@805: val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs adamc@805: in adamc@805: SOME (k', NONE) adamc@805: end adamc@805: | NONE => 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@805: (case sgnSeek (fn SgiDatatype dts => adamc@805: (case List.find (fn (x, _, _, _) => x = field) dts of adamc@805: SOME (_, _, xs, xncs) => SOME (xs, xncs) adamc@805: | NONE => 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@805: case sgnSeek (fn SgiDatatype dts => adamc@805: let adamc@805: fun search dts = adamc@805: case dts of adamc@805: [] => NONE adamc@805: | (_, n, xs, xncs) :: dts => adamc@805: case consider (n, xs, xncs) of adamc@805: NONE => search dts adamc@805: | v => v adamc@805: in adamc@805: search dts adamc@805: end 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@805: | SgiDatatype dts => adamc@805: let adamc@805: fun search dts = adamc@805: case dts of adamc@805: [] => NONE adamc@805: | (_, n, xs, xncs) :: dts => adamc@805: case seek (n, xs, xncs) of adamc@805: NONE => search dts adamc@805: | v => v adamc@805: in adamc@805: search dts adamc@805: end 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@805: | SgiDatatype dts => seek (sgis, sgns, strs, adamc@805: foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts, 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@825: fun patBinds env (p, loc) = adamc@825: case p of adamc@825: PWild => env adamc@825: | PVar (x, t) => pushERel env x t adamc@825: | PPrim _ => env adamc@825: | PCon (_, _, _, NONE) => env adamc@825: | PCon (_, _, _, SOME p) => patBinds env p adamc@825: | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps adamc@825: adamc@1272: fun patBindsN (p, _) = adamc@1272: case p of adamc@1272: PWild => 0 adamc@1272: | PVar _ => 1 adamc@1272: | PPrim _ => 0 adamc@1272: | PCon (_, _, _, NONE) => 0 adamc@1272: | PCon (_, _, _, SOME p) => patBindsN p adamc@1272: | PRecord xps => foldl (fn ((_, p, _), n) => patBindsN p + n) 0 xps adamc@1272: adamc@447: fun edeclBinds env (d, loc) = adamc@447: case d of adamc@825: EDVal (p, _, _) => patBinds env p 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@805: | DDatatype dts => adamc@157: let adamc@805: fun doOne ((x, n, xs, xncs), env) = adamc@805: let adamc@805: val k = (KType, loc) adamc@805: val nxs = length xs adamc@805: val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) => adamc@805: ((CApp (tb, (CRel (nxs - i - 1), loc)), loc), adamc@805: (KArrow (k, kb), loc))) adamc@805: ((CNamed n, loc), k) xs adamc@805: adamc@805: val env = pushCNamedAs env x n kb NONE adamc@805: val env = pushDatatype env n xs xncs adamc@805: in adamc@805: foldl (fn ((x', n', to), env) => adamc@805: let adamc@805: val t = adamc@805: case to of adamc@805: NONE => tb adamc@805: | SOME t => (TFun (t, tb), loc) adamc@805: val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs adamc@805: in adamc@805: pushENamedAs env x' n' t adamc@805: end) adamc@805: env xncs adamc@805: end adamc@157: in adamc@805: foldl doOne env dts 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@707: | DTable (tn, x, n, c, _, pc, _, cc) => adamc@205: let adamc@705: val ct = (CModProj (tn, [], "sql_table"), loc) adamc@705: val ct = (CApp (ct, c), loc) adamc@707: val ct = (CApp (ct, (CConcat (pc, cc), loc)), 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@754: | DView (tn, x, n, _, c) => adamc@754: let adamc@754: val ct = (CModProj (tn, [], "sql_view"), loc) adamc@754: val ct = (CApp (ct, c), loc) adamc@754: in adamc@754: pushENamedAs env x n ct adamc@754: 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@720: | DStyle (tn, x, n) => adamc@718: let adamc@720: val t = (CModProj (tn, [], "css_class"), loc) adamc@718: in adamc@718: pushENamedAs env x n t adamc@718: end adamc@1075: | DTask _ => env adamc@1199: | DPolicy _ => env adam@1294: | DOnError _ => env adamc@157: adamc@2: end