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