(--

This file defines the interface for a representation of propositional
logical formulae, i.e., boolean expressions.  The kinds of logical
expressions are true and false literals, variables, conjunctions
(and), disjunctions (or), negations (not), and implications (=>).
Logical formulae should be represented in canonical form, as
possible-disjunctions of possible-conjunctions of possibly-negated
atoms, which are literals and variables; implications are rewritten
into simpler forms.  I.e., if constructing a logical expression whose
form is on the left (where A, B, and C are arbitrary canonical logical
formulae), rewrite it into the equivalent logical expression whose
form is on the right:

not(A and B)    -> (not A) or (not B)   [move not inside and]
not(A or B)     -> (not A) and (not B)  [move not inside or]
(A or B) and C  -> (A and C) or (B and C) [move and inside or]
A and (B or C)  -> (A and B) or (A and C) [move and inside or]
A and (B and C) -> (A and B) and C      [make and left-associative]
A or (B or C)   -> (A or B) or C        [make or left-associative]
A implies B     -> (not A) or B         [express in simpler form]

--)

-- the abstract "superclass" of all logical formulae
abstract object Formula isa comparable[Formula];

-- there should be Formulae with names True and False, i.e.,
-- True:Formula
-- False:Formula
-- (hint: use concrete objects for these one-of-a-kind formulae)

-- create a new variable formula for a variable of the given name:
signature Variable(name:string):Formula;

-- return the negation of the argument formula, in canonical form
signature Not(Formula):Formula;

-- return the conjunction of the argument formulae, in canonical form
signature And(Formula, Formula):Formula;

-- return the disjunction of the argument formulae, in canonical form
signature Or(Formula, Formula):Formula;

-- return the canonical formula representing "f1 implies f2"
signature Implies(Formula, Formula):Formula;


-- return whether the two formula are *structurally* equal
signature =(Formula, Formula):bool;

-- return a printable string representing the formula
signature print_string(Formula):string;

-- evaluate the formula, given a mapping from variable names to
-- their truth values [assumes that all variables in the formula
-- have mappings in bindings]
signature evaluate(Formula, bindings:table[string,bool]):bool;

-- invoke the argument closure on each variable name occurring in the formula
signature varsDo(Formula, &(string):void):void;

-- return whether or not the formula is a tautology, i.e., whether
-- the formula is always true for all assignments of variables in it
-- [EXTRA CREDIT]
signature isTautology(Formula):bool;