1(**************************************************************************** 2*Copyright 2008 3* Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, Zach Snow 4****************************************************************************) 5(**************************************************************************** 6* This file is part of Teyjus. 7* 8* Teyjus is free software: you can redistribute it and/or modify 9* it under the terms of the GNU General Public License as published by 10* the Free Software Foundation, either version 3 of the License, or 11* (at your option) any later version. 12* 13* Teyjus is distributed in the hope that it will be useful, 14* but WITHOUT ANY WARRANTY; without even the implied warranty of 15* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 16* GNU General Public License for more details. 17* 18* You should have received a copy of the GNU General Public License 19* along with Teyjus. If not, see <http://www.gnu.org/licenses/>. 20****************************************************************************) 21(********************************************************************** 22*Preabsyn Module: 23* The prebstract syntax for Teyjus. 24**********************************************************************) 25type symbol = Symbol.symbol 26type pos = Errormsg.pos 27 28(* Kinds of Identifiers 29 * CVID and VarID are only distinguished in the preabstract syntax. 30 * There are some subtle differences: 31 * - VarID cannot be bound 32 * - VarID cannot appear in type abbreviations 33 * After the function translateID in parse.ml they merged to the same datatype*) 34type pidkind = 35 | CVID (* Free variable (or bound variable), 36 starting with an uppercase letter *) 37 | ConstID (* A constant (or bound variable), lowercase *) 38 | AVID (* Anonymous variable i.e. an underscore *) 39 | VarID (* Free variable, starting with an underscore *) 40 41(* Symbols 42* A symbol can represent the name of a term, type, module, signature *) 43type psymbol = Symbol of symbol * pidkind * pos 44 45(* Types *) 46type ptype = 47 | Atom of symbol * pidkind * pos 48 | App of ptype * ptype * pos 49 | Arrow of ptype * ptype * pos 50 | ErrorType 51 52(* Symbols for abstracted variables 53* The optional type represents the possible type annotation 54* The pabstractedsymbol of the term 55* x : int \ t 56* is 57* AbstractedSymbol("x", Some(Atom(int, ConstID, _), _)) *) 58type pabstractedsymbol = AbstractedSymbol of (symbol * ptype option * pos) 59 60(* Type abbreviations 61 * For instance, 62 * typeabbrev (bar A) list A -> list A 63 * will be represented as 64 * TypeAbbrev(bar, [Symbol(A, CVID,_)], "list A -> list A",_) 65 * where "list A -> list A" is the ptype representation of list A -> list A 66 * All the symbols appearing in the ptype should be present in the 67 * list of psymbols *) 68type ptypeabbrev = TypeAbbrev of psymbol * psymbol list * ptype * pos 69 70(* Terms *) 71type pterm = 72 (* A sequence of any terms *) 73 | SeqTerm of pterm list * pos 74 (* The usual prolog list notation *) 75 | ListTerm of pterm list * pos 76 (* ConsTerm(x,y,_) represents the prolog list notation [x|y] *) 77 | ConsTerm of pterm list * pterm * pos 78 (* LambdaTerm(x, t,_) represents x\ t 79 * The list here is just a sequence of terms. 80 * It will be translated as a single absyn term *) 81 | LambdaTerm of pabstractedsymbol * pterm list * pos 82 (* An IdTerm is any identifier (constant, kind, term, ...) 83 * with an optional type denoting the possible type annotation *) 84 | IdTerm of (symbol * ptype option * pidkind * pos) 85 | RealTerm of float * pos 86 | IntTerm of int * pos 87 | StringTerm of string * pos 88 | ErrorTerm 89 90(* Every clause (terminated by a period) in the module file 91 * is encapsulated in a SeqTerm and then in a Clause. 92 * The list of all clauses is stocked in the Module datatype *) 93type pclause = Clause of pterm 94 95(* Constants 96 * There are different kind of constants. They are already classified 97 * during the parsing and stored in the different list of the module datatype 98 * (see below for the different kinds) 99 * 100 * A declaration like: 101 * type a, b, c o 102 * will be represented as 103 * Constant(["a";"b";"c"], Some("o"),_) 104 * where "X" is the correct translation of X. 105 * The optional type is set to None when this is a closed, exportdef or useonly 106 * declaration alone (the type is declared somewhere else), e.g. 107 * type p o. 108 * exportdef p. 109 * Otherwise this is the type of the constant defined by the user or in the 110 * pervasives *) 111type pconstant = Constant of psymbol list * ptype option * pos 112 113(* Kinds 114* There are different categories of kinds. They are already classified 115 * during the parsing and stored in the different list of the module datatype 116 * (see below for the different kinds) 117 * 118 * The integer is the arity of the kind. E.g the kind declaration 119 * kind foo type -> type 120 * will be represented as Kind(_, Some 1, _) 121 * The optional integer is set to None when declaring that a kind is local 122 * after its declaration, e.g. 123 * kind foo type. 124 * localkind foo. *) 125type pkind = Kind of psymbol list * int option * pos 126 127(* Fixity *) 128type pfixitykind = 129 | Infix of pos 130 | Infixl of pos 131 | Infixr of pos 132 | Prefix of pos 133 | Prefixr of pos 134 | Postfix of pos 135 | Postfixl of pos 136 137(* The position used is the one of pfixitykind *) 138type pfixity = Fixity of psymbol list * pfixitykind * int * pos 139 140(******************************************************************** 141 * Module: 142 * This type stores information about a preabsyn module. 143 * The pidkind of used, accumulated, imported modules or signatures 144 * are not used. 145 146 * Module: 147 * Name: string 148 * 149 * 150 * Notice that constants declared in the .mod file without a keyword other than 151 * type are stored in the global constants list. This is only later, 152 * at the level of absyn syntax, that the local/exportdef/useonly 153 * constants list will be filled with the set of global constants/... 154 * appearing in the module but not in the signature. 155 * 156 * Global Constants: pconstant list 157 * Local Constants: pconstant list 158 * Closed Constants: pconstant list 159 * Useonly Constants: pconstant list 160 * Exportdef Constants: pconstant list 161 * 162 * Fixities: pfixity list 163 * 164 * Global Kinds: pkind list 165 * Local Kinds: pkind list 166 * 167 * Type Abbreviations: ptypeabbrev list 168 * 169 * Clauses: pterm list 170 * 171 * Accumulated Modules: psymbol list 172 * Accumulated Signatures: psymbol list 173 * Used Signatures: psymbol list 174 * Imported Modules: psymbol list 175 * 176 * Signature: 177 * Name: string 178 * Global Constants: pconstant list 179 * Useonly Constants: pconstant list 180 * Exportdef Constants: pconstant list 181 * 182 * Global Kinds: pkind list 183 * 184 * Type Abbreviations: ptypeabbrevlist 185 * 186 * Accumulated Signatures: psymbol list 187 ********************************************************************) 188type pmodule = 189 | Module of string * pconstant list * pconstant list * 190 pconstant list * pconstant list * pconstant list * pfixity list * 191 pkind list * pkind list * ptypeabbrev list * pclause list * 192 psymbol list * psymbol list * psymbol list * psymbol list 193 | Signature of string * pconstant list * pconstant list * 194 pconstant list * pkind list * 195 ptypeabbrev list * pfixity list * psymbol list * psymbol list 196 197val printPreAbsyn : pmodule -> out_channel -> unit 198 199 200(* Accessors *) 201val getFixityPos : pfixitykind -> pos 202val getTermPos : pterm -> pos 203val getModuleClauses : pmodule -> pclause list 204val getClauseTerm : pclause -> pterm 205 206val string_of_term : pterm -> string 207val string_of_type : ptype -> string 208