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