Mercurial > urweb

annotate src/elab.sml @ 1856:3683d1a8c1c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add Sigcheck phase to avoid issues with signatures in global initializers
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Jun 2013 08:18:47 -0400
parents bb942416bf1c
children 1aa9629e3a4c
rev   line source
adam@1639 1 (* Copyright (c) 2008-2011, Adam Chlipala
adamc@2 2 * All rights reserved.
adamc@2 3 *
adamc@2 4 * Redistribution and use in source and binary forms, with or without
adamc@2 5 * modification, are permitted provided that the following conditions are met:
adamc@2 6 *
adamc@2 7 * - Redistributions of source code must retain the above copyright notice,
adamc@2 8 * this list of conditions and the following disclaimer.
adamc@2 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@2 10 * this list of conditions and the following disclaimer in the documentation
adamc@2 11 * and/or other materials provided with the distribution.
adamc@2 12 * - The names of contributors may not be used to endorse or promote products
adamc@2 13 * derived from this software without specific prior written permission.
adamc@2 14 *
adamc@2 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@2 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@2 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@2 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@2 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@2 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@2 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@2 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@2 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@2 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@2 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@2 26 *)
adamc@2 27
adamc@2 28 structure Elab = struct
adamc@2 29
adamc@2 30 type 'a located = 'a ErrorMsg.located
adamc@2 31
adamc@2 32 datatype kind' =
adamc@2 33 KType
adamc@2 34 | KArrow of kind * kind
adamc@2 35 | KName
adamc@2 36 | KRecord of kind
adamc@82 37 | KUnit
adamc@207 38 | KTuple of kind list
adamc@2 39
adamc@2 40 | KError
adam@1639 41 | KUnif of ErrorMsg.span * string * kunif ref
adam@1639 42 | KTupleUnif of ErrorMsg.span * (int * kind) list * kunif ref
adamc@2 43
adamc@623 44 | KRel of int
adamc@623 45 | KFun of string * kind
adamc@623 46
adam@1639 47 and kunif =
adam@1639 48 KUnknown of kind -> bool (* Is the kind a valid unification? *)
adam@1639 49 | KKnown of kind
adam@1639 50
adamc@2 51 withtype kind = kind' located
adamc@2 52
adamc@2 53 datatype explicitness =
adamc@2 54 Explicit
adamc@2 55 | Implicit
adamc@2 56
adamc@2 57 datatype con' =
adamc@2 58 TFun of con * con
adamc@2 59 | TCFun of explicitness * string * kind * con
adamc@2 60 | TRecord of con
adamc@628 61 | TDisjoint of con * con * con
adamc@2 62
adamc@2 63 | CRel of int
adamc@2 64 | CNamed of int
adamc@34 65 | CModProj of int * string list * string
adamc@2 66 | CApp of con * con
adamc@8 67 | CAbs of string * kind * con
adamc@2 68
adamc@623 69 | CKAbs of string * con
adamc@623 70 | CKApp of con * kind
adamc@623 71 | TKFun of string * con
adamc@623 72
adamc@2 73 | CName of string
adamc@2 74
adamc@2 75 | CRecord of kind * (con * con) list
adamc@2 76 | CConcat of con * con
adamc@621 77 | CMap of kind * kind
adamc@2 78
adamc@82 79 | CUnit
adamc@82 80
adamc@207 81 | CTuple of con list
adamc@207 82 | CProj of con * int
adamc@207 83
adamc@2 84 | CError
adam@1639 85 | CUnif of int * ErrorMsg.span * kind * string * cunif ref
adam@1639 86
adam@1639 87 and cunif =
adam@1639 88 Unknown of con -> bool (* Is the constructor a valid unification? *)
adam@1639 89 | Known of con
adamc@2 90
adamc@2 91 withtype con = con' located
adamc@2 92
adamc@731 93 datatype datatype_kind = datatype DatatypeKind.datatype_kind
adamc@188 94
adamc@171 95 datatype patCon =
adamc@171 96 PConVar of int
adamc@171 97 | PConProj of int * string list * string
adamc@171 98
adamc@171 99 datatype pat' =
adamc@171 100 PWild
adamc@182 101 | PVar of string * con
adamc@173 102 | PPrim of Prim.t
adamc@191 103 | PCon of datatype_kind * patCon * con list * pat option
adamc@182 104 | PRecord of (string * pat * con) list
adamc@171 105
adamc@171 106 withtype pat = pat' located
adamc@171 107
adamc@9 108 datatype exp' =
adamc@14 109 EPrim of Prim.t
adamc@14 110 | ERel of int
adamc@9 111 | ENamed of int
adamc@34 112 | EModProj of int * string list * string
adamc@9 113 | EApp of exp * exp
adamc@26 114 | EAbs of string * con * con * exp
adamc@9 115 | ECApp of exp * con
adamc@9 116 | ECAbs of explicitness * string * kind * exp
adamc@9 117
adamc@623 118 | EKAbs of string * exp
adamc@623 119 | EKApp of exp * kind
adamc@623 120
adamc@29 121 | ERecord of (con * exp * con) list
adamc@12 122 | EField of exp * con * { field : con, rest : con }
adamc@445 123 | EConcat of exp * con * exp * con
adamc@149 124 | ECut of exp * con * { field : con, rest : con }
adamc@493 125 | ECutMulti of exp * con * { rest : con }
adamc@12 126
adamc@182 127 | ECase of exp * (pat * exp) list * { disc : con, result : con }
adamc@171 128
adamc@9 129 | EError
adamc@228 130 | EUnif of exp option ref
adamc@9 131
adamc@825 132 | ELet of edecl list * exp * con
adamc@447 133
adamc@447 134 and edecl' =
adamc@825 135 EDVal of pat * con * exp
adamc@447 136 | EDValRec of (string * con * exp) list
adamc@447 137
adamc@9 138 withtype exp = exp' located
adamc@447 139 and edecl = edecl' located
adamc@9 140
adamc@31 141 datatype sgn_item' =
adamc@31 142 SgiConAbs of string * int * kind
adamc@31 143 | SgiCon of string * int * kind * con
adamc@805 144 | SgiDatatype of (string * int * string list * (string * int * con option) list) list
adamc@191 145 | SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
adamc@31 146 | SgiVal of string * int * con
adamc@31 147 | SgiStr of string * int * sgn
adamc@59 148 | SgiSgn of string * int * sgn
adamc@88 149 | SgiConstraint of con * con
adamc@563 150 | SgiClassAbs of string * int * kind
adamc@563 151 | SgiClass of string * int * kind * con
adamc@31 152
adamc@31 153 and sgn' =
adamc@31 154 SgnConst of sgn_item list
adamc@31 155 | SgnVar of int
adamc@41 156 | SgnFun of string * int * sgn * sgn
adamc@42 157 | SgnWhere of sgn * string * con
adamc@59 158 | SgnProj of int * string list * string
adamc@31 159 | SgnError
adamc@31 160
adamc@31 161 withtype sgn_item = sgn_item' located
adamc@31 162 and sgn = sgn' located
adamc@31 163
adamc@2 164 datatype decl' =
adamc@5 165 DCon of string * int * kind * con
adamc@805 166 | DDatatype of (string * int * string list * (string * int * con option) list) list
adamc@191 167 | DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
adamc@9 168 | DVal of string * int * con * exp
adamc@123 169 | DValRec of (string * int * con * exp) list
adamc@31 170 | DSgn of string * int * sgn
adamc@31 171 | DStr of string * int * sgn * str
adamc@48 172 | DFfiStr of string * int * sgn
adamc@88 173 | DConstraint of con * con
adamc@109 174 | DExport of int * sgn * str
adamc@707 175 | DTable of int * string * int * con * exp * con * exp * con
adamc@338 176 | DSequence of int * string * int
adamc@754 177 | DView of int * string * int * exp * con
adamc@271 178 | DDatabase of string
adamc@459 179 | DCookie of int * string * int * con
adamc@720 180 | DStyle of int * string * int
adamc@1075 181 | DTask of exp * exp
adamc@1199 182 | DPolicy of exp
adam@1294 183 | DOnError of int * string list * string
adamc@31 184
adamc@31 185 and str' =
adamc@31 186 StrConst of decl list
adamc@31 187 | StrVar of int
adamc@34 188 | StrProj of str * string
adamc@41 189 | StrFun of string * int * sgn * sgn * str
adamc@44 190 | StrApp of str * str
adamc@31 191 | StrError
adamc@2 192
adamc@2 193 withtype decl = decl' located
adamc@31 194 and str = str' located
adamc@31 195
adamc@2 196 type file = decl list
adamc@2 197
adamc@2 198 end