(*  
 *  This file is a component of PropPlan a model-based planner
 *  Copyright (C) 2000-2007  Michael Paul Fourman

 *  This program is free software: you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License as published by
 *  the Free Software Foundation, either version 3 of the License, or
 *  (at your option) any later version.

 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU General Public License for more details.

 *  You should have received a copy of the GNU General Public License
 *  along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
infix 5 -- ==> ;
infix 3 >>;
infix 0 || @@;
infix 4 &&;

signature PROPOSITIONSIG = 
    sig 
	eqtype Name

datatype Term = ^^ of Name
  | ?  of Name

and Predicate = % of Name
  | ==
 
datatype Type = Type of Name | Either of Type list | Object

datatype 'a TypedList = TypedList of ('a list * Type) list
val forgetTypes : 'a TypedList -> 'a list
val @@ : 'a TypedList * 'a TypedList -> 'a TypedList
val printType : Type -> string
val printTypedList : Term TypedList -> (Term -> Term) -> string
  val substitutions :
     Name TypedList ->
     Term TypedList -> Term TypedList -> (Term -> Term) list 
datatype Lit = !! of Predicate * Term list
(* val < : Lit * Lit -> bool *)
val mkLit : Predicate * Term list -> Lit

datatype
    Formula =
        && of Formula * Formula
      | &&& of Formula list
      | ==> of Formula * Formula
      | <=> of Formula * Formula
      | A of Lit
      | F
      | T
      | || of Formula * Formula
      | ||| of Formula list
      | ~ of Formula
      | ALL of Term TypedList * Formula
      | EXS of Term TypedList * Formula
      | GOAL of Formula
      | INIT of Formula
      | LT  of (int *  Term TypedList) * Formula
      | GT  of (int *  Term TypedList) * Formula
      | EQ  of (int *  Term TypedList) * Formula
      | GE  of (int *  Term TypedList) * Formula
      | LE  of (int *  Term TypedList) * Formula

val tr : (Term -> Term)  -> Lit -> Lit 
val predicatesInFormula : Formula -> Predicate list
val uniquePredicates :  Predicate list list ->  Predicate list
val lit2string : Lit -> string
val form2string : Formula -> string

val simp : Formula -> Formula

end