1(****************************************************************************
2*Copyright 2008
3*  Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, Fabien Renaud,
4*  Zach Snow
5****************************************************************************)
6(****************************************************************************
7* This file is part of Teyjus.
8*
9* Teyjus is free software: you can redistribute it and/or modify
10* it under the terms of the GNU General Public License as published by
11* the Free Software Foundation, either version 3 of the License, or
12* (at your option) any later version.
13*
14* Teyjus is distributed in the hope that it will be useful,
15* but WITHOUT ANY WARRANTY; without even the implied warranty of
16* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
17* GNU General Public License for more details.
18*
19* You should have received a copy of the GNU General Public License
20* along with Teyjus.  If not, see <http://www.gnu.org/licenses/>.
21****************************************************************************)
22
23
24(* explicit_term term add_sing top_level :
25 * Given an aterm term, returns the term with every lambda prolog connective
26 * explicit i.e. there are no more :- , pi =>
27 * The result depends on:
28 * - add_sing indicating if the resulting aterm should be a
29 * single element of a list (false for the top call in parsefront)
30 * - top_level indicating if the aterm is at the top level
31 *  (true for the top call in parsefront, false in all the other cases)
32 *  This helps to determine if Pervasive.implconstant should be read as
33 *  :- or =>  as well as if a given predicate should be embedded in a list *)
34val explicit_term : Absyn.aterm -> bool -> bool ->  Absyn.aterm
35
36(* Add introduced constants and modify defined types in the .sig file
37 * in the following way: * every "o" which is not in a target position is
38 * replaced by "list o" *)
39val add_constants : Absyn.amodule -> Absyn.amodule
40
41(* For the type of the constant const every "o" except the one in the target
42 *  position is replaced by "list o".
43 * For instance (A -> o) -> o is transformed into (A -> list o) -> o *)
44val explicit_const_ty : Absyn.aconstant -> Absyn.aconstant
45
46(* The interpreter for explicit clauses *)
47val interpreter_mod : string
48val interpreter_sig : string
49
50(* The symbols we use: clause, fact, ... *)
51val explicit_constants : Absyn.aconstant list
52