adamc@2: (* Copyright (c) 2008, Adam Chlipala adamc@2: * All rights reserved. adamc@2: * adamc@2: * Redistribution and use in source and binary forms, with or without adamc@2: * modification, are permitted provided that the following conditions are met: adamc@2: * adamc@2: * - Redistributions of source code must retain the above copyright notice, adamc@2: * this list of conditions and the following disclaimer. adamc@2: * - Redistributions in binary form must reproduce the above copyright notice, adamc@2: * this list of conditions and the following disclaimer in the documentation adamc@2: * and/or other materials provided with the distribution. adamc@2: * - The names of contributors may not be used to endorse or promote products adamc@2: * derived from this software without specific prior written permission. adamc@2: * adamc@2: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@2: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@2: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@2: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@2: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@2: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@2: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@2: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@2: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@2: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@2: * POSSIBILITY OF SUCH DAMAGE. adamc@2: *) adamc@2: adamc@2: structure Elab = struct adamc@2: adamc@2: type 'a located = 'a ErrorMsg.located adamc@2: adamc@2: datatype kind' = adamc@2: KType adamc@2: | KArrow of kind * kind adamc@2: | KName adamc@2: | KRecord of kind adamc@82: | KUnit adamc@207: | KTuple of kind list adamc@2: adamc@2: | KError adamc@76: | KUnif of ErrorMsg.span * string * kind option ref adamc@2: adamc@623: | KRel of int adamc@623: | KFun of string * kind adamc@623: adamc@2: withtype kind = kind' located adamc@2: adamc@2: datatype explicitness = adamc@2: Explicit adamc@2: | Implicit adamc@2: adamc@334: datatype auto_instantiate = adamc@334: Instantiate adamc@334: | LeaveAlone adamc@334: adamc@2: datatype con' = adamc@2: TFun of con * con adamc@2: | TCFun of explicitness * string * kind * con adamc@2: | TRecord of con adamc@2: adamc@2: | CRel of int adamc@2: | CNamed of int adamc@34: | CModProj of int * string list * string adamc@2: | CApp of con * con adamc@8: | CAbs of string * kind * con adamc@345: | CDisjoint of auto_instantiate * con * con * con adamc@2: adamc@623: | CKAbs of string * con adamc@623: | CKApp of con * kind adamc@623: | TKFun of string * con adamc@623: adamc@2: | CName of string adamc@2: adamc@2: | CRecord of kind * (con * con) list adamc@2: | CConcat of con * con adamc@621: | CMap of kind * kind adamc@2: adamc@82: | CUnit adamc@82: adamc@207: | CTuple of con list adamc@207: | CProj of con * int adamc@207: adamc@2: | CError adamc@76: | CUnif of ErrorMsg.span * kind * string * con option ref adamc@2: adamc@2: withtype con = con' located adamc@2: adamc@188: datatype datatype_kind = adamc@188: Enum adamc@198: | Option adamc@188: | Default adamc@188: adamc@171: datatype patCon = adamc@171: PConVar of int adamc@171: | PConProj of int * string list * string adamc@171: adamc@171: datatype pat' = adamc@171: PWild adamc@182: | PVar of string * con adamc@173: | PPrim of Prim.t adamc@191: | PCon of datatype_kind * patCon * con list * pat option adamc@182: | PRecord of (string * pat * con) list adamc@171: adamc@171: withtype pat = pat' located adamc@171: adamc@9: datatype exp' = adamc@14: EPrim of Prim.t adamc@14: | ERel of int adamc@9: | ENamed of int adamc@34: | EModProj of int * string list * string adamc@9: | EApp of exp * exp adamc@26: | EAbs of string * con * con * exp adamc@9: | ECApp of exp * con adamc@9: | ECAbs of explicitness * string * kind * exp adamc@9: adamc@623: | EKAbs of string * exp adamc@623: | EKApp of exp * kind adamc@623: adamc@29: | ERecord of (con * exp * con) list adamc@12: | EField of exp * con * { field : con, rest : con } adamc@445: | EConcat of exp * con * exp * con adamc@149: | ECut of exp * con * { field : con, rest : con } adamc@493: | ECutMulti of exp * con * { rest : con } adamc@12: adamc@182: | ECase of exp * (pat * exp) list * { disc : con, result : con } adamc@171: adamc@9: | EError adamc@228: | EUnif of exp option ref adamc@9: adamc@447: | ELet of edecl list * exp adamc@447: adamc@447: and edecl' = adamc@447: EDVal of string * con * exp adamc@447: | EDValRec of (string * con * exp) list adamc@447: adamc@9: withtype exp = exp' located adamc@447: and edecl = edecl' located adamc@9: adamc@31: datatype sgn_item' = adamc@31: SgiConAbs of string * int * kind adamc@31: | SgiCon of string * int * kind * con adamc@191: | SgiDatatype of string * int * string list * (string * int * con option) list adamc@191: | SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list adamc@31: | SgiVal of string * int * con adamc@31: | SgiStr of string * int * sgn adamc@59: | SgiSgn of string * int * sgn adamc@88: | SgiConstraint of con * con adamc@563: | SgiClassAbs of string * int * kind adamc@563: | SgiClass of string * int * kind * con adamc@31: adamc@31: and sgn' = adamc@31: SgnConst of sgn_item list adamc@31: | SgnVar of int adamc@41: | SgnFun of string * int * sgn * sgn adamc@42: | SgnWhere of sgn * string * con adamc@59: | SgnProj of int * string list * string adamc@31: | SgnError adamc@31: adamc@31: withtype sgn_item = sgn_item' located adamc@31: and sgn = sgn' located adamc@31: adamc@2: datatype decl' = adamc@5: DCon of string * int * kind * con adamc@191: | DDatatype of string * int * string list * (string * int * con option) list adamc@191: | DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list adamc@9: | DVal of string * int * con * exp adamc@123: | DValRec of (string * int * con * exp) list adamc@31: | DSgn of string * int * sgn adamc@31: | DStr of string * int * sgn * str adamc@48: | DFfiStr of string * int * sgn adamc@88: | DConstraint of con * con adamc@109: | DExport of int * sgn * str adamc@205: | DTable of int * string * int * con adamc@338: | DSequence of int * string * int adamc@563: | DClass of string * int * kind * con adamc@271: | DDatabase of string adamc@459: | DCookie of int * string * int * con adamc@31: adamc@31: and str' = adamc@31: StrConst of decl list adamc@31: | StrVar of int adamc@34: | StrProj of str * string adamc@41: | StrFun of string * int * sgn * sgn * str adamc@44: | StrApp of str * str adamc@31: | StrError adamc@2: adamc@2: withtype decl = decl' located adamc@31: and str = str' located adamc@31: adamc@2: type file = decl list adamc@2: adamc@2: end