1(* ========================================================================= *) 2(* BASIC FIRST-ORDER LOGIC MANIPULATIONS *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6signature mlibTerm = 7sig 8 9type 'a pp = 'a mlibUseful.pp 10type ('a,'b) maplet = ('a, 'b) mlibUseful.maplet 11type 'a quotation = 'a mlibParser.quotation 12type infixities = mlibParser.infixities 13 14(* Datatypes for terms and formulas *) 15datatype term = 16 Var of string 17| Fn of string * term list 18 19datatype formula = 20 True 21| False 22| Atom of term 23| Not of formula 24| And of formula * formula 25| Or of formula * formula 26| Imp of formula * formula 27| Iff of formula * formula 28| Forall of string * formula 29| Exists of string * formula 30 31(* Contructors and destructors *) 32val dest_var : term -> string 33val is_var : term -> bool 34 35val dest_fn : term -> string * term list 36val is_fn : term -> bool 37val fn_name : term -> string 38val fn_args : term -> term list 39val fn_arity : term -> int 40val fn_function : term -> string * int 41 42val mk_const : string -> term 43val dest_const : term -> string 44val is_const : term -> bool 45 46val mk_binop : string -> term * term -> term 47val dest_binop : string -> term -> term * term 48val is_binop : string -> term -> bool 49 50val dest_atom : formula -> term 51val is_atom : formula -> bool 52 53val dest_neg : formula -> formula 54val is_neg : formula -> bool 55 56val list_mk_conj : formula list -> formula 57val strip_conj : formula -> formula list 58val flatten_conj : formula -> formula list 59 60val list_mk_disj : formula list -> formula 61val strip_disj : formula -> formula list 62val flatten_disj : formula -> formula list 63 64val list_mk_forall : string list * formula -> formula 65val strip_forall : formula -> string list * formula 66 67val list_mk_exists : string list * formula -> formula 68val strip_exists : formula -> string list * formula 69 70(* New variables *) 71val new_var : unit -> term 72val new_vars : int -> term list 73 74(* Sizes of terms and formulas *) 75val term_size : term -> int 76val formula_size : formula -> int 77 78(* Total comparison functions for terms and formulas *) 79val term_compare : term * term -> order 80val formula_compare : formula * formula -> order 81 82(* Operations on literals *) 83val mk_literal : bool * formula -> formula 84val dest_literal : formula -> bool * formula 85val is_literal : formula -> bool 86val literal_atom : formula -> formula 87 88(* Operations on formula negations *) 89val negative : formula -> bool 90val positive : formula -> bool 91val negate : formula -> formula 92 93(* Functions and relations in a formula *) 94val functions : formula -> (string * int) list 95val function_names : formula -> string list 96val relations : formula -> (string * int) list 97val relation_names : formula -> string list 98 99(* The equality relation has a special status *) 100val eq_rel : string * int 101val mk_eq : term * term -> formula 102val dest_eq : formula -> term * term 103val is_eq : formula -> bool 104val refl : term -> formula 105val sym : formula -> formula 106val lhs : formula -> term 107val rhs : formula -> term 108val eq_occurs : formula -> bool 109 110(* Free variables *) 111val FVT : term -> string list 112val FVTL : string list -> term list -> string list 113val FV : formula -> string list 114val FVL : string list -> formula list -> string list 115val specialize : formula -> formula 116val generalize : formula -> formula 117 118(* Subterms *) 119val subterm : int list -> term -> term 120val rewrite : (int list, term) maplet -> term -> term 121val subterms : int list -> term -> (int list, term) maplet list 122val literal_subterm : int list -> formula -> term 123val literal_rewrite : (int list, term) maplet -> formula -> formula 124val literal_subterms : formula -> (int list, term) maplet list 125 126(* A datatype to antiquote both terms and formulas *) 127datatype thing = mlibTerm of term | Formula of formula; 128 129(* Operators parsed and printed infix *) 130val infixes : infixities ref 131 132(* Deciding whether a string denotes a variable or constant *) 133val var_string : (string -> bool) ref 134 135(* Parsing *) 136val string_to_term' : infixities -> string -> term (* purely functional *) 137val string_to_formula' : infixities -> string -> formula 138val parse_term' : infixities -> thing quotation -> term 139val parse_formula' : infixities -> thing quotation -> formula 140val string_to_term : string -> term (* uses !infixes *) 141val string_to_formula : string -> formula 142val parse_term : thing quotation -> term 143val parse_formula : thing quotation -> formula 144 145(* Pretty-printing *) 146val pp_term' : infixities -> term pp (* purely functional *) 147val pp_formula' : infixities -> formula pp 148val term_to_string' : infixities -> int -> term -> string 149val formula_to_string' : infixities -> int -> formula -> string 150val pp_term : term pp (* uses !infixes *) 151val pp_formula : formula pp (* and !LINE_LENGTH *) 152val term_to_string : term -> string 153val formula_to_string : formula -> string 154 155end 156