(**** FORMULA.ML,v 1.1 2004/08/09 22:04:03 neilb Exp ****)

infix 5 -- ==> ;
infix 3 >>;
infix 0 ||;

infix 4 &&;

functor FORMULA (structure Parse : PARSE where type instream = TextIO.StreamIO.instream
	      structure Prop : PROPOSITIONSIG where type Name = string
		  )(*:PDDLSIG*) =
    struct
	open Prop;
	open Parse;
    
	type AtomicFormulaSkeleton = Predicate * Term TypedList

	datatype DomainDef =
	    Types of Name TypedList
	  | Constants of Term TypedList
	  | Predicates of AtomicFormulaSkeleton list
	  | Relations of AtomicFormulaSkeleton list
          | Axiom of Formula 
          | Fact of Formula

	fun getTypes  [] = TypedList []
	  | getTypes  (Types tl :: t) = tl @@ getTypes t
	  | getTypes (_ :: t) = getTypes t

	fun getConstants [] = TypedList []
	  | getConstants (Constants tl :: t) = tl @@ getConstants t
	  | getConstants (_ :: t) = getConstants t

	fun getPredicates [] = []
	  | getPredicates (Predicates tl :: t) = tl @ getPredicates t
	  | getPredicates (_ :: t) = getPredicates t

	fun getRelations [] = []
	  | getRelations (Relations tl :: t) = tl @ getRelations t
	  | getRelations (_ :: t) = getRelations t

 
	fun getAxiom [] = []
	  | getAxiom (Axiom tl :: t) = tl :: getAxiom t
	  | getAxiom (_ :: t) = getAxiom t
 
	fun getFact [] = []
	  | getFact (Fact tl :: t) = tl :: getFact t
	  | getFact (_ :: t) = getFact t

	datatype Domain = Domain of {name: Name,
				     types: Name TypedList, 
				     constants: Term TypedList, 
				     predicates: AtomicFormulaSkeleton list, 
				     relations: AtomicFormulaSkeleton list, 
				     axiom: Formula,
				     fact: Formula
				     }


	fun mkDomain (name, defs) = Domain{name = name,
					   types= getTypes defs, 
					   constants = getConstants defs, 
					   predicates = getPredicates defs,
					   relations = getRelations defs,
					   axiom = &&&(getAxiom defs),
					   fact = &&&(getFact defs)
					   }


	fun K x y = x

	fun seq p toks = (p -- repeat p >> op ::) toks

	val name = id 

	fun literal t toks =
	    ( atomic_formula t                                
	  ||  $"(" :- $"not" :- atomic_formula t -: $")"     >> Prop.~
	      ) toks
	and atomic_formula t toks = 
	    ( $"(" :- predicate -- repeat t -: $")"          >> (Prop.A o Prop.mkLit)
	     ) toks
	and term toks =
	    ( name                                           >> ^^
	  ||  variable                                          
	      ) toks
	and predicate toks =
	    ( name                                           >> %
	  ||  $"="                                           >> K (op ==)
	      ) toks
	and variable toks =
	    ( $"?" :- name                                   >> ? 
	     ) toks 

	fun pddltype toks = 
	    ( name                                            >> Type
	  ||  $"(" :- $"either" :- seq pddltype -: $")"       >> Either
	    ||  $"object"                                     >> K Object
		) toks

	(*PDDL Types *)
	(*NB the PDDL subset definition (DRAFT 1 Feb14) appears flawed here *)
	fun typed x toks =
	    ( (seq x -: $"-" -- pddltype) 
             ||   seq x                                        >> (fn x => (x,Object))
	     ) toks 

	fun typed_list x toks = 
	    (
	     repeat (typed x)                                  >> TypedList
	     ) toks 

	(********************************  Figure 3 ************************************************************)
	fun formula toks = 
	    (    literal term
	  || $"(" :- $"not" :- formula -: $")"                      >> Prop.~ 
	   || $"(" :- $"and" :- repeat formula -: $")"               >> Prop.&&& (* don't insist on *)
	    || $"(" :- $"or"  :- repeat formula -: $")"               >> Prop.||| (* a sequence here *)
	     || $"(" :- $"imply" :- formula -- formula  -: $")"        >> Prop.==>
	     || $"(" :- $"iff" :- formula -- formula  -: $")"          >> Prop.<=>
	|| $"(" :- $"exists" :- $"(" :- typed_list variable -: $")" -- formula  -: $")" >> Prop.EXS
	 || $"(" :- $"forall" :- $"(" :- typed_list variable -: $")" -- formula  -: $")" >> Prop.ALL
	   || $"(" :- $"<" :- ## -- $"(" :- typed_list variable -: $")" -- formula  -: $")" >> Prop.LT
	    || $"(" :- $"=" :- ## -- $"(" :- typed_list variable -: $")" -- formula  -: $")" >> Prop.EQ
             || $"(" :- $">" :- ## -- $"(" :- typed_list variable -: $")" -- formula  -: $")" >> Prop.GT
	      || $"(" :- $"=<" :- ## -- $"(" :- typed_list variable -: $")" -- formula  -: $")" >> Prop.LE
	       || $"(" :- $">=" :- ## -- $"(" :- typed_list variable -: $")" -- formula  -: $")" >> Prop.GE
		  ) toks

	fun positive_formula toks = 
	    (    atomic_formula term
	   || $"(" :- $"and" :- repeat positive_formula -: $")"               >> Prop.&&& 
	 || $"(" :- $"forall" :- $"(" :- typed_list variable -: $")" -- positive_formula  -: $")" >> Prop.ALL
		  ) toks

	fun horn_formula toks = 
	    (    positive_formula 
	     || $"(" :- $"imply" :- positive_formula -- positive_formula  -: $")"        >> Prop.==>
	 || $"(" :- $"forall" :- $"(" :- typed_list variable -: $")" -- horn_formula  -: $")" >> Prop.ALL 
		  ) toks



	fun atomic_formula_skeleton toks =
	    ( $"(" :- predicate -- typed_list variable -: $")"  
	     ) toks

	fun def toks = 
	    ( $"(" :- $":" :- $"types" :- typed_list name -: $")"        >> Types
	  ||  $"(" :- $":" :- $"constants" :- typed_list term -: $")"    >> Constants
	  ||  $"(" :- $":" :- $"axioms" :- repeat formula -: $")"                >> (Axiom o &&&)
	  ||  $"(" :- $":" :- $"facts" :- repeat horn_formula -: $")"                >> (Fact o &&&) 
	  ||  $"(" :- $":" :- $"predicates" :- repeat atomic_formula_skeleton -: $")"     >> Predicates
	  ||  $"(" :- $":" :- $"relations" :- repeat atomic_formula_skeleton -: $")"     >> Relations
	      )toks

	fun domain toks =
	    ( $"(" :- $"define" :- $"(" :- $"domain" :- name -: $")" 
	     -- repeat def 
	     -: $")" >> mkDomain
	     ) toks


	fun readDomain f  = Parse.reader domain f

    end