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