adamc@1278: (* Copyright (c) 2008-2010, Adam Chlipala adamc@38: * All rights reserved. adamc@38: * adamc@38: * Redistribution and use in source and binary forms, with or without adamc@38: * modification, are permitted provided that the following conditions are met: adamc@38: * adamc@38: * - Redistributions of source code must retain the above copyright notice, adamc@38: * this list of conditions and the following disclaimer. adamc@38: * - Redistributions in binary form must reproduce the above copyright notice, adamc@38: * this list of conditions and the following disclaimer in the documentation adamc@38: * and/or other materials provided with the distribution. adamc@38: * - The names of contributors may not be used to endorse or promote products adamc@38: * derived from this software without specific prior written permission. adamc@38: * adamc@38: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@38: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@38: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@38: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@38: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@38: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@38: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@38: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@38: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@38: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@38: * POSSIBILITY OF SUCH DAMAGE. adamc@38: *) adamc@38: adamc@38: structure ExplEnv :> EXPL_ENV = struct adamc@38: adamc@38: open Expl adamc@38: adamc@38: structure U = ExplUtil adamc@38: adamc@38: structure IM = IntBinaryMap adamc@38: structure SM = BinaryMapFn(struct adamc@38: type ord_key = string adamc@38: val compare = String.compare adamc@38: end) adamc@38: adamc@38: exception UnboundRel of int adamc@38: exception UnboundNamed of int adamc@38: adamc@38: adamc@38: (* AST utility functions *) adamc@38: adamc@38: exception SynUnif adamc@38: adamc@624: val liftKindInKind = adamc@624: U.Kind.mapB {kind = fn bound => fn k => adamc@624: case k of adamc@624: KRel xn => adamc@624: if xn < bound then adamc@624: k adamc@624: else adamc@624: KRel (xn + 1) adamc@624: | _ => k, adamc@624: bind = fn (bound, _) => bound + 1} adamc@624: adamc@624: val liftKindInCon = adamc@624: U.Con.mapB {kind = fn bound => fn k => adamc@624: case k of adamc@624: KRel xn => adamc@624: if xn < bound then adamc@624: k adamc@624: else adamc@624: KRel (xn + 1) adamc@624: | _ => k, adamc@624: con = fn _ => fn c => c, adamc@624: bind = fn (bound, U.Con.RelK _) => bound + 1 adamc@624: | (bound, _) => bound} adamc@624: adamc@38: val liftConInCon = adamc@624: U.Con.mapB {kind = fn _ => fn k => k, adamc@38: con = fn bound => fn c => adamc@38: case c of adamc@38: CRel xn => adamc@38: if xn < bound then adamc@38: c adamc@38: else adamc@38: CRel (xn + 1) adamc@38: (*| CUnif _ => raise SynUnif*) adamc@38: | _ => c, adamc@624: bind = fn (bound, U.Con.RelC _) => bound + 1 adamc@38: | (bound, _) => bound} adamc@38: adamc@38: val lift = liftConInCon 0 adamc@38: adamc@38: adamc@38: (* Back to environments *) adamc@38: adamc@38: datatype 'a var' = adamc@38: Rel' of int * 'a adamc@38: | Named' of int * 'a adamc@38: adamc@38: datatype 'a var = adamc@38: NotBound adamc@38: | Rel of int * 'a adamc@38: | Named of int * 'a adamc@38: adamc@38: type env = { adamc@624: relK : string list, adamc@624: adamc@38: relC : (string * kind) list, adamc@38: namedC : (string * kind * con option) IM.map, adamc@38: adamc@38: relE : (string * con) list, adamc@38: namedE : (string * con) IM.map, adamc@38: adamc@38: sgn : (string * sgn) IM.map, adamc@38: adamc@38: str : (string * sgn) IM.map adamc@38: } adamc@38: adamc@38: val namedCounter = ref 0 adamc@38: adamc@38: val empty = { adamc@624: relK = [], adamc@624: adamc@38: relC = [], adamc@38: namedC = IM.empty, adamc@38: adamc@38: relE = [], adamc@38: namedE = IM.empty, adamc@38: adamc@38: sgn = IM.empty, adamc@38: adamc@38: str = IM.empty adamc@38: } adamc@38: adamc@624: fun pushKRel (env : env) x = adamc@624: {relK = x :: #relK env, adamc@624: adamc@624: relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env), adamc@624: namedC = #namedC env, adamc@624: adamc@624: relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), adamc@624: namedE = #namedE env, adamc@624: adamc@624: sgn = #sgn env, adamc@624: adamc@624: str = #str env adamc@624: } adamc@624: adamc@624: fun lookupKRel (env : env) n = adamc@624: (List.nth (#relK env, n)) adamc@624: handle Subscript => raise UnboundRel n adamc@624: adamc@38: fun pushCRel (env : env) x k = adamc@624: {relK = #relK env, adamc@38: adamc@624: relC = (x, k) :: #relC env, adamc@624: namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), adamc@38: adamc@624: relE = map (fn (x, c) => (x, lift c)) (#relE env), adamc@624: namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), adamc@38: adamc@624: sgn = #sgn env, adamc@624: adamc@624: str = #str env adamc@624: } adamc@38: adamc@38: fun lookupCRel (env : env) n = adamc@38: (List.nth (#relC env, n)) adamc@38: handle Subscript => raise UnboundRel n adamc@38: adamc@38: fun pushCNamed (env : env) x n k co = adamc@624: {relK = #relK env, adamc@624: adamc@38: relC = #relC env, adamc@38: namedC = IM.insert (#namedC env, n, (x, k, co)), adamc@38: adamc@38: relE = #relE env, adamc@38: namedE = #namedE env, adamc@38: adamc@38: sgn = #sgn env, adamc@38: adamc@38: str = #str env} adamc@38: adamc@38: fun lookupCNamed (env : env) n = adamc@38: case IM.find (#namedC env, n) of adamc@38: NONE => raise UnboundNamed n adamc@38: | SOME x => x adamc@38: adamc@38: fun pushERel (env : env) x t = adamc@624: {relK = #relK env, adamc@38: adamc@624: relC = #relC env, adamc@624: namedC = #namedC env, adamc@38: adamc@624: relE = (x, t) :: #relE env, adamc@624: namedE = #namedE env, adamc@38: adamc@624: sgn = #sgn env, adamc@624: adamc@624: str = #str env} adamc@38: adamc@38: fun lookupERel (env : env) n = adamc@38: (List.nth (#relE env, n)) adamc@38: handle Subscript => raise UnboundRel n adamc@38: adamc@38: fun pushENamed (env : env) x n t = adamc@624: {relK = #relK env, adamc@624: adamc@38: relC = #relC env, adamc@38: namedC = #namedC env, adamc@38: adamc@38: relE = #relE env, adamc@38: namedE = IM.insert (#namedE env, n, (x, t)), adamc@38: adamc@38: sgn = #sgn env, adamc@38: adamc@38: str = #str env} adamc@38: adamc@38: fun lookupENamed (env : env) n = adamc@38: case IM.find (#namedE env, n) of adamc@38: NONE => raise UnboundNamed n adamc@38: | SOME x => x adamc@38: adamc@38: fun pushSgnNamed (env : env) x n sgis = adamc@624: {relK = #relK env, adamc@624: adamc@38: relC = #relC env, adamc@38: namedC = #namedC env, adamc@38: adamc@38: relE = #relE env, adamc@38: namedE = #namedE env, adamc@38: adamc@38: sgn = IM.insert (#sgn env, n, (x, sgis)), adamc@38: adamc@38: str = #str env} adamc@38: adamc@38: fun lookupSgnNamed (env : env) n = adamc@38: case IM.find (#sgn env, n) of adamc@38: NONE => raise UnboundNamed n adamc@38: | SOME x => x adamc@38: adamc@38: fun pushStrNamed (env : env) x n sgis = adamc@624: {relK = #relK env, adamc@624: adamc@38: relC = #relC env, adamc@38: namedC = #namedC env, adamc@38: adamc@38: relE = #relE env, adamc@38: namedE = #namedE env, adamc@38: adamc@38: sgn = #sgn env, adamc@38: adamc@38: str = IM.insert (#str env, n, (x, sgis))} adamc@38: adamc@38: fun lookupStrNamed (env : env) n = adamc@38: case IM.find (#str env, n) of adamc@38: NONE => raise UnboundNamed n adamc@38: | SOME x => x adamc@38: adamc@162: fun declBinds env (d, loc) = adamc@38: case d of adamc@38: DCon (x, n, k, c) => pushCNamed env x n k (SOME c) adamc@806: | DDatatype dts => adamc@162: let adamc@806: fun doOne ((x, n, xs, xncs), env) = adamc@806: let adamc@806: val k = (KType, loc) adamc@806: val nxs = length xs adamc@806: val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) => adamc@806: ((CApp (tb, (CRel (nxs - i - 1), loc)), loc), adamc@806: (KArrow (k, kb), loc))) adamc@806: ((CNamed n, loc), k) xs adamc@806: adamc@806: val env = pushCNamed env x n kb NONE adamc@806: in adamc@806: foldl (fn ((x', n', to), env) => adamc@806: let adamc@806: val t = adamc@806: case to of adamc@806: NONE => tb adamc@806: | SOME t => (TFun (t, tb), loc) adamc@806: val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs adamc@806: in adamc@806: pushENamed env x' n' t adamc@806: end) adamc@806: env xncs adamc@806: end adamc@162: in adamc@806: foldl doOne env dts adamc@162: end adamc@191: | DDatatypeImp (x, n, m, ms, x', xs, xncs) => adamc@162: let adamc@162: val t = (CModProj (m, ms, x'), loc) adamc@162: val env = pushCNamed env x n (KType, loc) (SOME t) adamc@162: adamc@162: val t = (CNamed n, loc) adamc@162: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamed env x' n' t adamc@191: end) adamc@191: env xncs adamc@162: end adamc@38: | DVal (x, n, t, _) => pushENamed env x n t adamc@124: | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis adamc@38: | DSgn (x, n, sgn) => pushSgnNamed env x n sgn adamc@38: | DStr (x, n, sgn, _) => pushStrNamed env x n sgn adamc@48: | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn adamc@109: | DExport _ => env adamc@707: | DTable (tn, x, n, c, _, pc, _, cc) => adamc@246: 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: pushENamed 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@246: in adamc@246: pushENamed env x n t adamc@246: 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: pushENamed env x n ct adamc@754: end adamc@275: | DDatabase _ => env adamc@460: | DCookie (tn, x, n, c) => adamc@460: let adamc@460: val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc) adamc@460: in adamc@460: pushENamed env x n t adamc@460: end adamc@720: | DStyle (tn, x, n) => adamc@718: let adamc@720: val t = (CModProj (tn, [], "css_class"), loc) adamc@718: in adamc@718: pushENamed env x n t adamc@718: end adamc@1075: | DTask _ => env adamc@1199: | DPolicy _ => env adam@1294: | DOnError _ => env adamc@38: adamc@162: fun sgiBinds env (sgi, loc) = adamc@38: case sgi of adamc@38: SgiConAbs (x, n, k) => pushCNamed env x n k NONE adamc@38: | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) adamc@806: | SgiDatatype dts => adamc@162: let adamc@806: fun doOne ((x, n, xs, xncs), env) = adamc@806: let adamc@806: val k = (KType, loc) adamc@806: val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs adamc@806: adamc@806: val env = pushCNamed env x n k' NONE adamc@806: in adamc@806: foldl (fn ((x', n', to), env) => adamc@806: let adamc@806: val t = adamc@806: case to of adamc@806: NONE => (CNamed n, loc) adamc@806: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@806: adamc@806: val k = (KType, loc) adamc@806: val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs adamc@806: in adamc@806: pushENamed env x' n' t adamc@806: end) adamc@806: env xncs adamc@806: end adamc@162: in adamc@806: foldl doOne env dts adamc@162: end adamc@191: | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@162: let adamc@191: val t = (CModProj (m1, ms, x'), loc) adamc@191: val env = pushCNamed env x n (KType, loc) (SOME t) adamc@191: adamc@191: val t = (CNamed n, loc) adamc@162: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamed env x' n' t adamc@191: end) adamc@191: env xncs adamc@162: end adamc@38: | SgiVal (x, n, t) => pushENamed env x n t adamc@64: | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn adamc@38: | SgiStr (x, n, sgn) => pushStrNamed env x n sgn adamc@38: adamc@1278: fun patBinds env (p, loc) = adamc@1278: case p of adamc@1278: PWild => env adamc@1278: | PVar (x, t) => pushERel env x t adamc@1278: | PPrim _ => env adamc@1278: | PCon (_, _, _, NONE) => env adamc@1278: | PCon (_, _, _, SOME p) => patBinds env p adamc@1278: | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps adamc@1278: adamc@38: end