1 /*-----------------------------------------------------------------------
2 
3 File  : cte_typecheck.h
4 
5 Author: Simon Cruanes
6 
7 Contents
8 
9   Type checking and inference for Simple types
10 
11   Copyright 2011 by the author.
12   This code is released under the GNU General Public Licence.
13   See the file COPYING in the main CLIB directory for details.
14   Run "eprover -h" for contact information.
15 
16 Changes
17 
18 <1>   Mon Jul  8 17:15:05 CEST 2013
19       New
20 
21 -----------------------------------------------------------------------*/
22 
23 #ifndef CTE_TYPECHECK
24 
25 #define CTE_TYPECHECK
26 
27 #include <cte_signature.h>
28 #include <cte_termtypes.h>
29 
30 /*---------------------------------------------------------------------*/
31 /*                    Data type declarations                           */
32 /*---------------------------------------------------------------------*/
33 
34 
35 /*---------------------------------------------------------------------*/
36 /*                Exported Functions and Variables                     */
37 /*---------------------------------------------------------------------*/
38 
39 bool     TypeCheckConsistent(Sig_p sig, Term_p term);
40 void     TypeInferSort(Sig_p sig, Term_p term);
41 void     TypeDeclareIsPredicate(Sig_p sig, Term_p term);
42 void     TypeDeclareIsNotPredicate(Sig_p sig, Term_p term);
43 
44 #endif
45 
46 /*---------------------------------------------------------------------*/
47 /*                        End of File                                  */
48 /*---------------------------------------------------------------------*/
49