adamc@29: (* Copyright (c) 2008, Adam Chlipala adamc@29: * All rights reserved. adamc@29: * adamc@29: * Redistribution and use in source and binary forms, with or without adamc@29: * modification, are permitted provided that the following conditions are met: adamc@29: * adamc@29: * - Redistributions of source code must retain the above copyright notice, adamc@29: * this list of conditions and the following disclaimer. adamc@29: * - Redistributions in binary form must reproduce the above copyright notice, adamc@29: * this list of conditions and the following disclaimer in the documentation adamc@29: * and/or other materials provided with the distribution. adamc@29: * - The names of contributors may not be used to endorse or promote products adamc@29: * derived from this software without specific prior written permission. adamc@29: * adamc@29: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@29: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@29: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@29: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@29: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@29: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@29: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@29: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@29: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@29: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@29: * POSSIBILITY OF SUCH DAMAGE. adamc@29: *) adamc@29: adamc@29: structure CjrEnv :> CJR_ENV = struct adamc@29: adamc@29: open Cjr adamc@29: adamc@29: structure IM = IntBinaryMap adamc@29: adamc@29: adamc@29: exception UnboundRel of int adamc@29: exception UnboundNamed of int adamc@29: exception UnboundF of int adamc@101: exception UnboundStruct of int adamc@29: adamc@29: type env = { adamc@166: datatypes : (string * (string * int * typ option) list) IM.map, adamc@181: constructors : (string * typ option * int) IM.map, adamc@29: adamc@29: numRelE : int, adamc@29: relE : (string * typ) list, adamc@29: namedE : (string * typ) IM.map, adamc@29: adamc@101: structs : (string * typ) list IM.map adamc@29: } adamc@29: adamc@29: val empty = { adamc@166: datatypes = IM.empty, adamc@181: constructors = IM.empty, adamc@29: adamc@29: numRelE = 0, adamc@29: relE = [], adamc@29: namedE = IM.empty, adamc@29: adamc@101: structs = IM.empty adamc@29: } adamc@29: adamc@166: fun pushDatatype (env : env) x n xncs = adamc@166: {datatypes = IM.insert (#datatypes env, n, (x, xncs)), adamc@182: constructors = foldl (fn ((x, n', to), constructors) => adamc@182: IM.insert (constructors, n', (x, to, n))) adamc@181: (#constructors env) xncs, adamc@29: adamc@29: numRelE = #numRelE env, adamc@29: relE = #relE env, adamc@29: namedE = #namedE env, adamc@29: adamc@101: structs = #structs env} adamc@29: adamc@166: fun lookupDatatype (env : env) n = adamc@166: case IM.find (#datatypes env, n) of adamc@29: NONE => raise UnboundNamed n adamc@29: | SOME x => x adamc@29: adamc@181: fun lookupConstructor (env : env) n = adamc@181: case IM.find (#constructors env, n) of adamc@181: NONE => raise UnboundNamed n adamc@181: | SOME x => x adamc@181: adamc@29: fun pushERel (env : env) x t = adamc@166: {datatypes = #datatypes env, adamc@181: constructors = #constructors env, adamc@29: adamc@29: numRelE = #numRelE env + 1, adamc@29: relE = (x, t) :: #relE env, adamc@29: namedE = #namedE env, adamc@29: adamc@101: structs = #structs env} adamc@29: adamc@29: fun lookupERel (env : env) n = adamc@29: (List.nth (#relE env, n)) adamc@29: handle Subscript => raise UnboundRel n adamc@29: adamc@29: fun countERels (env : env) = #numRelE env adamc@29: adamc@29: fun listERels (env : env) = #relE env adamc@29: adamc@29: fun pushENamed (env : env) x n t = adamc@166: {datatypes = #datatypes env, adamc@181: constructors = #constructors env, adamc@29: adamc@29: numRelE = #numRelE env, adamc@29: relE = #relE env, adamc@29: namedE = IM.insert (#namedE env, n, (x, t)), adamc@29: adamc@101: structs = #structs env} adamc@29: adamc@29: fun lookupENamed (env : env) n = adamc@29: case IM.find (#namedE env, n) of adamc@29: NONE => raise UnboundNamed n adamc@29: | SOME x => x adamc@29: adamc@101: fun pushStruct (env : env) n xts = adamc@166: {datatypes = #datatypes env, adamc@181: constructors = #constructors env, adamc@101: adamc@101: numRelE = #numRelE env, adamc@101: relE = #relE env, adamc@101: namedE = #namedE env, adamc@101: adamc@101: structs = IM.insert (#structs env, n, xts)} adamc@101: adamc@101: fun lookupStruct (env : env) n = adamc@101: case IM.find (#structs env, n) of adamc@101: NONE => raise UnboundStruct n adamc@101: | SOME x => x adamc@101: adamc@109: fun declBinds env (d, loc) = adamc@29: case d of adamc@165: DDatatype (x, n, xncs) => adamc@165: let adamc@166: val env = pushDatatype env x n xncs adamc@165: in adamc@168: foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype (n, xncs), loc) adamc@168: | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype (n, xncs), loc)), loc)) adamc@165: env xncs adamc@165: end adamc@165: | DStruct (n, xts) => pushStruct env n xts adamc@165: | DVal (x, n, t, _) => pushENamed env x n t adamc@121: | DFun (fx, n, args, ran, _) => adamc@121: let adamc@121: val t = foldl (fn ((_, arg), t) => (TFun (arg, t), loc)) ran args adamc@121: in adamc@121: pushENamed env fx n t adamc@121: end adamc@129: | DFunRec vis => adamc@129: foldl (fn ((fx, n, args, ran, _), env) => adamc@129: let adamc@129: val t = foldl (fn ((_, arg), t) => (TFun (arg, t), loc)) ran args adamc@129: in adamc@129: pushENamed env fx n t adamc@129: end) env vis adamc@165: adamc@29: adamc@29: end