Mercurial > urweb
view src/elab_env.sml @ 39:02f42e9a1825
Corify removes modules
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 19 Jun 2008 12:39:22 -0400 |
parents | 44b5405e74c7 |
children | 1405d8c26790 |
line wrap: on
line source
(* Copyright (c) 2008, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: * * - Redistributions of source code must retain the above copyright notice, * this list of conditions and the following disclaimer. * - Redistributions in binary form must reproduce the above copyright notice, * this list of conditions and the following disclaimer in the documentation * and/or other materials provided with the distribution. * - The names of contributors may not be used to endorse or promote products * derived from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE * POSSIBILITY OF SUCH DAMAGE. *) structure ElabEnv :> ELAB_ENV = struct open Elab structure U = ElabUtil structure IM = IntBinaryMap structure SM = BinaryMapFn(struct type ord_key = string val compare = String.compare end) exception UnboundRel of int exception UnboundNamed of int (* AST utility functions *) exception SynUnif val liftConInCon = U.Con.mapB {kind = fn k => k, con = fn bound => fn c => case c of CRel xn => if xn < bound then c else CRel (xn + 1) (*| CUnif _ => raise SynUnif*) | _ => c, bind = fn (bound, U.Con.Rel _) => bound + 1 | (bound, _) => bound} val lift = liftConInCon 0 (* Back to environments *) datatype 'a var' = Rel' of int * 'a | Named' of int * 'a datatype 'a var = NotBound | Rel of int * 'a | Named of int * 'a type env = { renameC : kind var' SM.map, relC : (string * kind) list, namedC : (string * kind * con option) IM.map, renameE : con var' SM.map, relE : (string * con) list, namedE : (string * con) IM.map, renameSgn : (int * sgn) SM.map, sgn : (string * sgn) IM.map, renameStr : (int * sgn) SM.map, str : (string * sgn) IM.map } val namedCounter = ref 0 val empty = { renameC = SM.empty, relC = [], namedC = IM.empty, renameE = SM.empty, relE = [], namedE = IM.empty, renameSgn = SM.empty, sgn = IM.empty, renameStr = SM.empty, str = IM.empty } fun pushCRel (env : env) x k = let val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) | x => x) (#renameC env) in {renameC = SM.insert (renameC, x, Rel' (0, k)), relC = (x, k) :: #relC env, namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), renameE = #renameE env, relE = map (fn (x, c) => (x, lift c)) (#relE env), namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), renameSgn = #renameSgn env, sgn = #sgn env, renameStr = #renameStr env, str = #str env } end fun lookupCRel (env : env) n = (List.nth (#relC env, n)) handle Subscript => raise UnboundRel n fun pushCNamedAs (env : env) x n k co = {renameC = SM.insert (#renameC env, x, Named' (n, k)), relC = #relC env, namedC = IM.insert (#namedC env, n, (x, k, co)), renameE = #renameE env, relE = #relE env, namedE = #namedE env, renameSgn = #renameSgn env, sgn = #sgn env, renameStr = #renameStr env, str = #str env} fun pushCNamed env x k co = let val n = !namedCounter in namedCounter := n + 1; (pushCNamedAs env x n k co, n) end fun lookupCNamed (env : env) n = case IM.find (#namedC env, n) of NONE => raise UnboundNamed n | SOME x => x fun lookupC (env : env) x = case SM.find (#renameC env, x) of NONE => NotBound | SOME (Rel' x) => Rel x | SOME (Named' x) => Named x fun pushERel (env : env) x t = let val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) | x => x) (#renameE env) in {renameC = #renameC env, relC = #relC env, namedC = #namedC env, renameE = SM.insert (renameE, x, Rel' (0, t)), relE = (x, t) :: #relE env, namedE = #namedE env, renameSgn = #renameSgn env, sgn = #sgn env, renameStr = #renameStr env, str = #str env} end fun lookupERel (env : env) n = (List.nth (#relE env, n)) handle Subscript => raise UnboundRel n fun pushENamedAs (env : env) x n t = {renameC = #renameC env, relC = #relC env, namedC = #namedC env, renameE = SM.insert (#renameE env, x, Named' (n, t)), relE = #relE env, namedE = IM.insert (#namedE env, n, (x, t)), renameSgn = #renameSgn env, sgn = #sgn env, renameStr = #renameStr env, str = #str env} fun pushENamed env x t = let val n = !namedCounter in namedCounter := n + 1; (pushENamedAs env x n t, n) end fun lookupENamed (env : env) n = case IM.find (#namedE env, n) of NONE => raise UnboundNamed n | SOME x => x fun lookupE (env : env) x = case SM.find (#renameE env, x) of NONE => NotBound | SOME (Rel' x) => Rel x | SOME (Named' x) => Named x fun pushSgnNamedAs (env : env) x n sgis = {renameC = #renameC env, relC = #relC env, namedC = #namedC env, renameE = #renameE env, relE = #relE env, namedE = #namedE env, renameSgn = SM.insert (#renameSgn env, x, (n, sgis)), sgn = IM.insert (#sgn env, n, (x, sgis)), renameStr = #renameStr env, str = #str env} fun pushSgnNamed env x sgis = let val n = !namedCounter in namedCounter := n + 1; (pushSgnNamedAs env x n sgis, n) end fun lookupSgnNamed (env : env) n = case IM.find (#sgn env, n) of NONE => raise UnboundNamed n | SOME x => x fun lookupSgn (env : env) x = SM.find (#renameSgn env, x) fun pushStrNamedAs (env : env) x n sgis = {renameC = #renameC env, relC = #relC env, namedC = #namedC env, renameE = #renameE env, relE = #relE env, namedE = #namedE env, renameSgn = #renameSgn env, sgn = #sgn env, renameStr = SM.insert (#renameStr env, x, (n, sgis)), str = IM.insert (#str env, n, (x, sgis))} fun pushStrNamed env x sgis = let val n = !namedCounter in namedCounter := n + 1; (pushStrNamedAs env x n sgis, n) end fun lookupStrNamed (env : env) n = case IM.find (#str env, n) of NONE => raise UnboundNamed n | SOME x => x fun lookupStr (env : env) x = SM.find (#renameStr env, x) fun declBinds env (d, _) = case d of DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) | DVal (x, n, t, _) => pushENamedAs env x n t | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn fun sgiBinds env (sgi, _) = case sgi of SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) | SgiVal (x, n, t) => pushENamedAs env x n t | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn fun sgnSeek f sgis = let fun seek (sgis, strs, cons) = case sgis of [] => NONE | (sgi, _) :: sgis => case f sgi of SOME v => SOME (v, (strs, cons)) | NONE => case sgi of SgiConAbs (x, n, _) => seek (sgis, strs, IM.insert (cons, n, x)) | SgiCon (x, n, _, _) => seek (sgis, strs, IM.insert (cons, n, x)) | SgiVal _ => seek (sgis, strs, cons) | SgiStr (x, n, _) => seek (sgis, IM.insert (strs, n, x), cons) in seek (sgis, IM.empty, IM.empty) end fun id x = x fun unravelStr (str, _) = case str of StrVar x => (x, []) | StrProj (str, m) => let val (x, ms) = unravelStr str in (x, ms @ [m]) end | _ => raise Fail "unravelStr" fun sgnS_con (str, (strs, cons)) c = case c of CModProj (m1, ms, x) => (case IM.find (strs, m1) of NONE => c | SOME m1x => let val (m1, ms') = unravelStr str in CModProj (m1, ms' @ m1x :: ms, x) end) | CNamed n => (case IM.find (cons, n) of NONE => c | SOME nx => let val (m1, ms) = unravelStr str in CModProj (m1, ms, nx) end) | _ => c fun sgnSubCon (str, (strs, cons)) = ElabUtil.Con.map {kind = id, con = sgnS_con (str, (strs, cons))} fun sgnSubSgn (str, (strs, cons)) = ElabUtil.Sgn.map {kind = id, con = sgnS_con (str, (strs, cons)), sgn_item = id, sgn = id} fun projectCon env {sgn = (sgn, _), str, field} = case sgn of SgnConst sgis => (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE | _ => NONE) sgis of NONE => NONE | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) | SgnVar n => let val (_, sgn) = lookupSgnNamed env n in projectCon env {sgn = sgn, str = str, field = field} end | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) fun projectVal env {sgn = (sgn, _), str, field} = case sgn of SgnConst sgis => (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of NONE => NONE | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)) | SgnVar n => let val (_, sgn) = lookupSgnNamed env n in projectVal env {sgn = sgn, str = str, field = field} end | SgnError => SOME (CError, ErrorMsg.dummySpan) fun projectStr env {sgn = (sgn, _), str, field} = case sgn of SgnConst sgis => (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of NONE => NONE | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) | SgnVar n => let val (_, sgn) = lookupSgnNamed env n in projectStr env {sgn = sgn, str = str, field = field} end | SgnError => SOME (SgnError, ErrorMsg.dummySpan) val ktype = (KType, ErrorMsg.dummySpan) fun bbind env x = #1 (pushCNamed env x ktype NONE) val basis = empty val basis = bbind basis "int" val basis = bbind basis "float" val basis = bbind basis "string" end