infix 5 -- ==> <=> ;
infix 3 >>;
infix 0 || @@;
infix 4 &&;
infix << <<<;

functor PROPOSITION() : PROPOSITIONSIG =
    struct
	exception Proposition of string


	(******* Types *************)
	type Name = string

	datatype Term = ^^ of string
	  | ?  of string
	and Predicate = % of string
	  | ==

	datatype Type = Type of Name | Either of Type list | Object;

	datatype 'a TypedList = TypedList of ('a list * Type) list

	fun (TypedList a) @@ (TypedList b) = TypedList(a @ b); (* join two TypedLists *)
	fun forgetTypes (TypedList ts) = List.concat (map #1 ts) 

	(******** Printing ********)
	fun term2string (^^ x) = x | term2string (? x) = "?"^x

	fun printList p [] = "" 
	  | printList p [h] = p h  
	  | printList p (h :: t) = p h ^ " " ^ printList p t
 
	fun printType (Type n) = n 
	  | printType (Either ts) = "(Either " ^ printList printType ts ^ ")"
	  | printType Object = "Object";
      
	fun printTypedList (TypedList ts) s = 
	    printList (fn (xs,t) =>  printList (fn ^^ x => x | ? x => "?" ^ x) (map s xs)) ts 

	fun member [] _ = false 
	  | member (h :: t) x = x = h orelse member t x

	local
	    fun (^^ s) << (^^ t) = s < (t:string)
	      | (? s) << (? t) = s < (t:string)
	      | (? s) << (^^ t) = true
	      | _ << _ = false;

	    fun insert c [] = [c]
	      | insert c (cs as h :: t) = 
		if c << h then c :: cs 
		else if c = h then cs
		     else h :: insert c t
	in

	    fun sorted <<< [] = sorted
	      | sorted <<< (h :: t) = insert h sorted <<< t
	    fun unique [] = []
	      | unique (h :: t) =   unique t <<< h
	end

	fun objects theTypes theConstants (Type t) =
	    let fun withType []               t' = []
		  | withType ((os,t'') :: tl) t' = 
		    if Type t' = t'' then 
			withType tl t' @ os
		    else  
			withType  tl  t'
		fun subTypes  []               t' = [ t']
		  | subTypes  ((ts,t'') :: tl) t' = 
		    if Type t' = t'' then 
			subTypes tl t' @ List.concat (map (subTypes theTypes) ts)
		    else  
			subTypes tl t'
	    in
		unique (map (withType theConstants) (subTypes theTypes  t))
	    end
	  | objects theTypes [] Object = []
	  | objects theTypes ((os,t'') :: tl) Object =  objects theTypes tl Object <<< os
	  | objects theTypes theConstants (Either ts) = unique (map (objects theTypes theConstants) ts);

	(* a substitution maps variables to constants (Term -> Term)
	 substitutions types constants parameters 
	 is a list of all well-typed substitutions instantiating the parameters *)
	fun substitutions types constants [] = [fn x => x]
	  | substitutions types constants (([],_) :: r) = substitutions types constants r
	  | substitutions types constants ((x :: xs, t) :: r) =
	    let val cs = objects types constants t
		fun sx g c  = (fn x' => 
			       if x' = x 
				   then c 
			       else g x') (* like g except sx g c x = c *)
	    in
		List.concat
		(map (fn g => map (sx g) cs ) 
		 (substitutions types constants ((xs,t) ::r))
		 )
	    end
	local structure Dict = DICTIONARY(type Key = Term)
	in
	    fun subst types constants [] ss = ss
	      | subst types constants (([],_) :: r) ss = subst types constants r ss
	      | subst types constants ((x :: xs, t) :: r) ss =
		subst types constants ((xs,t) ::r)
		let val cs = objects types constants t
		    fun sx g c  = Dict.enter ((x,c),g)
		in
		    ( List.concat
		     ( map (fn g => map (sx g) cs ) ss )
		     )
		end 
	    fun substitutions (TypedList types) (TypedList constants) (TypedList params) = 
		let fun f x y =  Dict.lookup x y handle Lookup => y
		in
		    map f (subst types constants params [Dict.empty])
		end
	end

	datatype Lit = !! of Predicate * Term list
	(* declare an ordering *)
	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

	fun mkLit x = !! x

	fun tr s (!!(p, xs)) = !!(p, map s xs)

	fun (% s) << (% t) = s < (t:string)
	  | == << % _ = true
	  | _ << _ = false ;

        fun insert c [] = [c]
	  | insert c (cs as h :: t) = 
	    if c << h then c :: cs 
	    else if c = h then cs
	    else h :: insert c t
	infix <<<

	fun sorted <<< [] = sorted
	  | sorted <<< (h :: t) = insert h sorted <<< t

	fun uniquePredicates [] = []
	  | uniquePredicates (h :: t) =   uniquePredicates t <<< h

	fun predicatesInFormula (A (!!(predicate,_))) = [predicate]
	  | predicatesInFormula (p && q)     = predicatesInFormula p <<< predicatesInFormula q
	  | predicatesInFormula (p || q)     = predicatesInFormula p <<< predicatesInFormula q
	  | predicatesInFormula (p ==> q)    = predicatesInFormula p <<< predicatesInFormula q
	  | predicatesInFormula (p <=> q)    = predicatesInFormula p <<< predicatesInFormula q
	  | predicatesInFormula (&&& ps)     = uniquePredicates (map  predicatesInFormula ps)
	  | predicatesInFormula (||| ps)     = uniquePredicates (map  predicatesInFormula ps)
	  | predicatesInFormula (ALL (_, p)) = predicatesInFormula p
	  | predicatesInFormula (EXS (_, p)) = predicatesInFormula p
	  | predicatesInFormula (~ p)        = predicatesInFormula p
	  | predicatesInFormula _            = [] (* T and F *)

	fun fold f e [] = e | fold f e (h :: t) = fold f (f (e, h)) t

	fun lit2string (!! (%p, [])) =  "(" ^ p ^ ")"
	  | lit2string (!! (%p, (x :: xs))) =  "(" ^ fold (fn (e,h) => e ^ " " ^ h) 
	                                        (p ^ " " ^ term2string x) 
	                                                (map term2string xs) 
	                                            ^")"
	  | lit2string (!! (==, [x,y])) =  "(" ^ term2string x ^ " = " ^ term2string y ^ ")"
	  | lit2string (!! (==, xs)) = "(aux)"

	fun simp (x && T) = x
	  | simp (x && F) = F
	  | simp (x || F) = x
	  | simp (x || T) = T 
	  | simp (T && x) = x
	  | simp (F && x) = F
	  | simp (F || x) = x
	  | simp (T || x) = T
	  | simp x = x

	fun form2string T = "T" | form2string F = "F" 
	  | form2string (A a) = lit2string a
	  | form2string (p && q) = "(" ^ form2string p ^ " && " ^ form2string q ^")"
	  | form2string (p || q) = "(" ^ form2string p ^ " || " ^ form2string q ^")"
	  | form2string (~ p) = " ~" ^ form2string p
	  | form2string (ALL(ts,f)) = " Forall " ^ "FIXME: vars go here" ^ " (" ^ form2string f ^ ")"
	  | form2string (EXS (ts,f)) = " Exists " ^ "FIXME: vars go here" ^ " (" ^ form2string f ^ ")"
	  (* FIXME: put in proper prinitng of Terms for Forall and Exists*)
	  | form2string x = PolyML.makestring x

    end