Mercurial > urweb

annotate src/mono_env.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents b4480a56cab7
children d328983dc5a6
rev   line source
adamc@25 1 (* Copyright (c) 2008, Adam Chlipala
adamc@25 2 * All rights reserved.
adamc@25 3 *
adamc@25 4 * Redistribution and use in source and binary forms, with or without
adamc@25 5 * modification, are permitted provided that the following conditions are met:
adamc@25 6 *
adamc@25 7 * - Redistributions of source code must retain the above copyright notice,
adamc@25 8 * this list of conditions and the following disclaimer.
adamc@25 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@25 10 * this list of conditions and the following disclaimer in the documentation
adamc@25 11 * and/or other materials provided with the distribution.
adamc@25 12 * - The names of contributors may not be used to endorse or promote products
adamc@25 13 * derived from this software without specific prior written permission.
adamc@25 14 *
adamc@25 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@25 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@25 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@25 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@25 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@25 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@25 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@25 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@25 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@25 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@25 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@25 26 *)
adamc@25 27
adamc@25 28 structure MonoEnv :> MONO_ENV = struct
adamc@25 29
adamc@25 30 open Mono
adamc@25 31
adamc@25 32 structure IM = IntBinaryMap
adamc@25 33
adamc@25 34
adamc@25 35 exception UnboundRel of int
adamc@25 36 exception UnboundNamed of int
adamc@25 37
adamc@25 38 type env = {
adamc@168 39 datatypes : (string * (string * int * typ option) list) IM.map,
adamc@178 40 constructors : (string * typ option * int) IM.map,
adamc@25 41
adamc@183 42 relE : (string * typ * exp option) list,
adamc@109 43 namedE : (string * typ * exp option * string) IM.map
adamc@25 44 }
adamc@25 45
adamc@25 46 val empty = {
adamc@168 47 datatypes = IM.empty,
adamc@178 48 constructors = IM.empty,
adamc@25 49
adamc@25 50 relE = [],
adamc@25 51 namedE = IM.empty
adamc@25 52 }
adamc@25 53
adamc@168 54 fun pushDatatype (env : env) x n xncs =
adamc@168 55 {datatypes = IM.insert (#datatypes env, n, (x, xncs)),
adamc@182 56 constructors = foldl (fn ((x, n', to), constructors) =>
adamc@182 57 IM.insert (constructors, n', (x, to, n)))
adamc@178 58 (#constructors env) xncs,
adamc@25 59
adamc@25 60 relE = #relE env,
adamc@25 61 namedE = #namedE env}
adamc@25 62
adamc@168 63 fun lookupDatatype (env : env) n =
adamc@168 64 case IM.find (#datatypes env, n) of
adamc@25 65 NONE => raise UnboundNamed n
adamc@25 66 | SOME x => x
adamc@25 67
adamc@178 68 fun lookupConstructor (env : env) n =
adamc@178 69 case IM.find (#constructors env, n) of
adamc@178 70 NONE => raise UnboundNamed n
adamc@178 71 | SOME x => x
adamc@178 72
adamc@800 73 structure U = MonoUtil
adamc@800 74
adamc@800 75 val liftExpInExp =
adamc@800 76 U.Exp.mapB {typ = fn t => t,
adamc@800 77 exp = fn bound => fn e =>
adamc@800 78 case e of
adamc@800 79 ERel xn =>
adamc@800 80 if xn < bound then
adamc@800 81 e
adamc@800 82 else
adamc@800 83 ERel (xn + 1)
adamc@800 84 | _ => e,
adamc@800 85 bind = fn (bound, U.Exp.RelE _) => bound + 1
adamc@800 86 | (bound, _) => bound}
adamc@800 87
adamc@183 88 fun pushERel (env : env) x t eo =
adamc@168 89 {datatypes = #datatypes env,
adamc@178 90 constructors = #constructors env,
adamc@800 91 relE = (x, t, eo) :: map (fn (x, t, eo) => (x, t, Option.map (liftExpInExp 0) eo)) (#relE env),
adamc@25 92 namedE = #namedE env}
adamc@25 93
adamc@25 94 fun lookupERel (env : env) n =
adamc@25 95 (List.nth (#relE env, n))
adamc@25 96 handle Subscript => raise UnboundRel n
adamc@25 97
adamc@109 98 fun pushENamed (env : env) x n t eo s =
adamc@168 99 {datatypes = #datatypes env,
adamc@178 100 constructors = #constructors env,
adamc@25 101
adamc@25 102 relE = #relE env,
adamc@109 103 namedE = IM.insert (#namedE env, n, (x, t, eo, s))}
adamc@25 104
adamc@25 105 fun lookupENamed (env : env) n =
adamc@25 106 case IM.find (#namedE env, n) of
adamc@25 107 NONE => raise UnboundNamed n
adamc@25 108 | SOME x => x
adamc@25 109
adamc@164 110 fun declBinds env (d, loc) =
adamc@25 111 case d of
adamc@808 112 DDatatype dts =>
adamc@808 113 foldl (fn ((x, n, xncs), env) =>
adamc@808 114 let
adamc@808 115 val env = pushDatatype env x n xncs
adamc@808 116 val dt = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), loc)
adamc@808 117 in
adamc@808 118 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt NONE ""
adamc@808 119 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc) NONE "")
adamc@808 120 env xncs
adamc@808 121 end) env dts
adamc@164 122 | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
adamc@126 123 | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis
adamc@109 124 | DExport _ => env
adamc@273 125 | DTable _ => env
adamc@338 126 | DSequence _ => env
adamc@754 127 | DView _ => env
adamc@271 128 | DDatabase _ => env
adamc@569 129 | DJavaScript _ => env
adamc@725 130 | DCookie _ => env
adamc@718 131 | DStyle _ => env
adamc@1075 132 | DTask _ => env
adamc@1199 133 | DPolicy _ => env
adam@1294 134 | DOnError _ => env
adamc@25 135
adamc@179 136 fun patBinds env (p, loc) =
adamc@179 137 case p of
adamc@179 138 PWild => env
adamc@183 139 | PVar (x, t) => pushERel env x t NONE
adamc@179 140 | PPrim _ => env
adamc@188 141 | PCon (_, _, NONE) => env
adamc@188 142 | PCon (_, _, SOME p) => patBinds env p
adamc@182 143 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
adamc@288 144 | PNone _ => env
adamc@288 145 | PSome (_, p) => patBinds env p
adamc@179 146
adamc@567 147 fun patBindsN (p, loc) =
adamc@567 148 case p of
adamc@567 149 PWild => 0
adamc@567 150 | PVar _ => 1
adamc@567 151 | PPrim _ => 0
adamc@567 152 | PCon (_, _, NONE) => 0
adamc@567 153 | PCon (_, _, SOME p) => patBindsN p
adamc@567 154 | PRecord xps => foldl (fn ((_, p, _), count) => count + patBindsN p) 0 xps
adamc@567 155 | PNone _ => 0
adamc@567 156 | PSome (_, p) => patBindsN p
adamc@567 157
adamc@25 158 end