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
22type symbol = Symbol.symbol
23type pos = Errormsg.pos
24
25type pidkind =
26  | CVID
27  | ConstID
28  | AVID
29  | VarID
30
31type psymbol = Symbol of symbol * pidkind * pos
32
33type ptype =
34  | Atom of symbol * pidkind * pos
35  | App of ptype * ptype * pos
36  | Arrow of ptype * ptype * pos
37  | ErrorType
38
39type pabstractedsymbol = AbstractedSymbol of (symbol * ptype option * pos)
40
41type ptypeabbrev = TypeAbbrev of psymbol * psymbol list * ptype * pos
42
43type pterm =
44  | SeqTerm of pterm list * pos
45  | ListTerm of pterm list * pos
46  | ConsTerm of pterm list * pterm * pos
47  | LambdaTerm of pabstractedsymbol * pterm list * pos
48  | IdTerm of (symbol * ptype option * pidkind * pos)
49  | RealTerm of float * pos
50  | IntTerm of int * pos
51  | StringTerm of string * pos
52  | ErrorTerm
53
54type pclause = Clause of pterm
55
56type pconstant = Constant of psymbol list * ptype option * pos
57
58type pkind = Kind of psymbol list * int option * pos
59
60type pfixitykind =
61  | Infix of pos
62  | Infixl of pos
63  | Infixr of pos
64  | Prefix of pos
65  | Prefixr of pos
66  | Postfix of pos
67  | Postfixl of pos
68
69type pfixity = Fixity of psymbol list * pfixitykind * int * pos
70
71type pmodule =
72  | Module of string * pconstant list * pconstant list *
73      pconstant list * pconstant list * pconstant list * pfixity list *
74      pkind list * pkind list * ptypeabbrev list * pclause list *
75      psymbol list * psymbol list * psymbol list * psymbol list
76  | Signature of string * pconstant list * pconstant list *
77      pconstant list * pkind list *
78      ptypeabbrev list * pfixity list * psymbol list * psymbol list
79
80
81let string_of_pos pos = Errormsg.string_of_pos pos
82
83let map_with_commas f list = String.concat ", " (List.map f list)
84
85let rec string_of_termlist list =
86  map_with_commas string_of_term list
87
88and string_of_abstractedsymbol = function
89  | AbstractedSymbol(tsym, Some t, pos) ->
90      "AbstractedSymbol(" ^ (Symbol.name tsym) ^ ", " ^
91        (string_of_type t) ^ ", " ^ (string_of_pos pos) ^ ")"
92  | AbstractedSymbol(tsym, None, pos) ->
93      "AbstractedSymbol(" ^ (Symbol.name tsym) ^ ", " ^
94      (string_of_pos pos) ^ ")"
95
96and string_of_term = function
97  | SeqTerm(tlist, pos) ->
98      "SeqTerm([" ^ (string_of_termlist tlist) ^ "], " ^
99        (string_of_pos pos) ^ ")"
100  | ListTerm(tlist, pos) ->
101      "ListTerm([" ^ (string_of_termlist tlist) ^ "], " ^
102        (string_of_pos pos) ^ ")"
103  | ConsTerm(tlist, t, pos) ->
104      "ConsTerm([" ^ (string_of_termlist tlist) ^ "], " ^
105        (string_of_term t) ^ ", " ^ (string_of_pos pos) ^ ")"
106  | IdTerm(sym, None, k, pos) ->
107      "IdTerm(" ^ (Symbol.name sym) ^ ", " ^ (string_of_idkind k) ^ ", " ^
108        (string_of_pos pos) ^ ")"
109  | IdTerm(sym, Some t, k, pos) ->
110      "IdTerm(" ^ (Symbol.name sym) ^ ", " ^ (string_of_type t) ^ ", " ^
111        (string_of_idkind k) ^ ", " ^ (string_of_pos pos) ^ ")"
112  | RealTerm(r, pos) ->
113      "RealTerm(" ^ (string_of_float r) ^ ", " ^
114        (string_of_pos pos) ^ ")"
115  | IntTerm(i, pos) ->
116      "IntTerm(" ^ (string_of_int i) ^ ", " ^
117        (string_of_pos pos) ^ ")"
118  | StringTerm(s, pos) ->
119      "StringTerm(" ^ s ^ ", " ^ (string_of_pos pos) ^ ")"
120  | LambdaTerm(lt, t, pos) ->
121      "LambdaTerm([" ^ (string_of_abstractedsymbol lt) ^ "], " ^
122        (string_of_termlist t) ^ ", " ^ (string_of_pos pos) ^ ")"
123  | ErrorTerm ->
124      "Error"
125
126and string_of_idkind = function
127  | CVID -> "CVID"
128  | ConstID -> "ConstID"
129  | AVID -> "AVID"
130  | VarID -> "VarID"
131
132and string_of_type = function
133  | Atom(sym, k, pos) ->
134      "Atom(" ^ (Symbol.name sym) ^ ", " ^ (string_of_idkind k) ^ ", " ^
135        (string_of_pos pos) ^ ")"
136  | App(t1, t2, pos) ->
137      "App(" ^ (string_of_type t1) ^ ", " ^ (string_of_type t2) ^ ", " ^
138        (string_of_pos pos) ^ ")"
139  | Arrow(t1, t2, pos) ->
140      "Arrow(" ^ (string_of_type t1) ^ ", " ^ (string_of_type t2) ^ ", " ^
141         (string_of_pos pos) ^ ")"
142  | ErrorType ->
143      "Error"
144
145let string_of_symbol = function
146  | Symbol(sym, k, pos) ->
147      "Symbol(" ^ (Symbol.name sym) ^ ", " ^ (string_of_idkind k) ^ ", " ^
148        (string_of_pos pos) ^ ")"
149
150let string_of_symbollist list =
151  map_with_commas string_of_symbol list
152
153let string_of_constant = function
154  | Constant(symlist, Some t, pos) ->
155      "Constant(" ^ (string_of_symbollist symlist) ^
156        ", " ^ (string_of_type t) ^ ", " ^ (string_of_pos pos) ^ ")"
157  | Constant(symlist, None, pos) ->
158      "Constant(" ^ (string_of_symbollist symlist) ^
159        ", " ^ (string_of_pos pos) ^ ")"
160
161let string_of_typeabbrev = function
162  | TypeAbbrev(name, arglist, ty, pos) ->
163      "TypeAbbrev(" ^ (string_of_symbol name) ^
164        (string_of_symbollist arglist) ^ ", " ^
165        (string_of_type ty) ^ ", " ^ (string_of_pos pos) ^ ")"
166
167let string_of_fixitykind = function
168  | Infix(pos) -> "Infix(" ^ (string_of_pos pos) ^ ") "
169  | Infixl(pos) -> "Infixl(" ^ (string_of_pos pos) ^ ") "
170  | Infixr(pos) -> "Infixr(" ^ (string_of_pos pos) ^ ") "
171  | Prefix(pos) -> "Prefix(" ^ (string_of_pos pos) ^ ") "
172  | Prefixr(pos) -> "Prefixr(" ^ (string_of_pos pos) ^ ") "
173  | Postfix(pos) -> "Postfix(" ^ (string_of_pos pos) ^ ") "
174  | Postfixl(pos) -> "Postfixl(" ^ (string_of_pos pos) ^ ") "
175
176let string_of_fixity = function
177  | Fixity(names, k, prec, pos) ->
178      "Fixity(" ^ (string_of_symbollist names) ^
179        ", " ^ (string_of_fixitykind k) ^ ", " ^ (string_of_int prec) ^ ", " ^
180        (string_of_pos pos) ^ ")"
181
182let string_of_kind = function
183  | Kind(symlist, Some i, pos) ->
184      "Kind(" ^ (string_of_symbollist symlist) ^
185        ", " ^ (string_of_int i) ^ ", " ^ (string_of_pos pos) ^ ")"
186  | Kind(symlist, None, pos) ->
187      "Kind(" ^ (string_of_symbollist symlist) ^
188        ", " ^ (string_of_pos pos) ^ ")"
189
190let string_of_clause = function
191  | Clause(ts) -> "Clause(" ^ (string_of_term ts) ^ ")"
192
193(********************************************************************
194 * printPreAbsyn:
195 *  Prints all information about a preabsyn module.
196 ********************************************************************)
197let printPreAbsyn m out =
198  (* Text output functions *)
199  let output_line s = output_string out (s ^ "\n") in
200  let output_list f list = List.iter (fun t -> output_line (f t)) list in
201    match m with
202      | Module(name, gconstants, lconstants, cconstants, uconstants,
203               econstants, fixities, gkinds, lkinds, tabbrevs, clauses,
204               accummod, accumsig, usesig, impmods) ->
205          output_line ("Module: " ^ name) ;
206          output_line "Constants:" ;
207          output_list string_of_constant gconstants ;
208          output_list string_of_constant lconstants ;
209          output_list string_of_constant cconstants ;
210          output_line "" ;
211          output_line "Kinds:" ;
212          output_list string_of_kind gkinds ;
213          output_line "" ;
214          output_list string_of_kind lkinds ;
215          output_line "Type Abbrevs:" ;
216          output_list string_of_typeabbrev tabbrevs ;
217          output_line "Clauses:" ;
218          output_list string_of_clause clauses ;
219          output_line "Fixities:" ;
220          output_list string_of_fixity fixities
221
222      | Signature(name, gconstants, _, _, gkinds, tabbrevs,
223                  fixities, accumsig, usig) ->
224          output_line ("Signature: " ^ name) ;
225          output_line "Constants:" ;
226          output_list string_of_constant gconstants ;
227          output_line "Kinds:" ;
228          output_list string_of_kind gkinds ;
229          output_line "Type Abbrevs:" ;
230          output_list string_of_typeabbrev tabbrevs
231
232let getFixityPos = function
233  | Infix(pos) -> pos
234  | Infixl(pos) -> pos
235  | Infixr(pos) -> pos
236  | Prefix(pos) -> pos
237  | Prefixr(pos) -> pos
238  | Postfix(pos) -> pos
239  | Postfixl(pos) -> pos
240
241let getTermPos = function
242  | SeqTerm(_, pos) -> pos
243  | ListTerm(_, pos) -> pos
244  | ConsTerm(_, _, pos) -> pos
245  | IdTerm(_, _, _, pos) -> pos
246  | RealTerm(_, pos) -> pos
247  | IntTerm(_, pos) -> pos
248  | StringTerm(_, pos) -> pos
249  | LambdaTerm(_,_,pos) -> pos
250  | ErrorTerm ->
251      Errormsg.impossible Errormsg.none "Preabsyn.getTermPos: invalid term"
252
253let getClauseTerm = function
254  Clause(t) -> t
255
256let getModuleClauses = function
257  | Module(_, _, _, _, _, _, _, _, _, _, clauses, _, _, _, _) -> clauses
258  | _ ->
259      Errormsg.impossible Errormsg.none
260        "Preabsyn.getModuleClauses: invalid module"
261