infix IMPLIES;

local
    structure Basic     = BASIC()
    structure Keyword   = KEYWORD(Basic)
    structure Instream  = TextIO
    structure Lex       = LEXICAL(structure Basic = Basic and Keyword = Keyword and StreamIO = TextIO.StreamIO )
    structure Parse     = PARSE(Lex)
    structure Prop      = Proposition
    structure Dict      = DICTIONARY(type Key = Prop.Term)

    structure Bdd = LOGIC();


    structure Parser = FORMULA(structure Parse = Parse and Prop = Prop and Dict = Dict and StreamIO = TextIO.StreamIO)
(*
    sharing type Planner.Bdd.Lit = Parser.Lit
	    sharing type Vars.Key = Planner.Bdd.Var
		    sharing type Parser.Formula = Planner.Bdd.Formula
			    sharing type Planner.Bdd.TypedList = Parser.TypedList
				    sharing type Planner.Bdd.Term = Parser.Term
					*)
    open Parser Bdd;
in
    infix mem
    fun x mem (h :: t) = x = h orelse x mem t | _ mem [] = false
    exception Error = Bdd.Error
    exception SynError = Parser.SynError
    val start = Bdd.bdd_start;
    val sift = Bdd.SIFT;
    val window = STABLE_WINDOW;
    val reordering = Bdd.REORDERING;
    
    val readDomain = Parser.readDomain

    datatype BDD_STATS = BDD_STATS of {size:int,states:int,variables:int}
    datatype SATISFYING_VALUATION =  SATISFYING_VALUATION of string list

    fun mkBdd (Domain{
		      name : Name, 
		      types: Name TypedList, 
		      fact: Formula,
		      axiom: Formula,
		      predicates: AtomicFormulaSkeleton list,
		      relations: AtomicFormulaSkeleton list,
		      constants: Term TypedList
		      } 
	       )
	       =
	let val _ = Bdd.bdd_restart()
	    val FF = Bdd.FALSE() and TT = Bdd.TRUE() 
	    val bddFact = eval types constants (V o lit2var) fact
	    
	    val rels = map (fn (p,s)=>p) relations
	    (* instantiations of relations will be mapped to true or false*)

	    fun isTrue instantiated =
		let val theAtom = V(lit2var instantiated) (* create or reuse  bdd *)
		in
		   if ++bddFact IMPLIES theAtom then TT else FF
		end
		
	    fun testEq [x,y] = if x = y then TT else FF

	    (* translate atoms, using FF or TT for relations *)
	    fun translate ss atom =
		let val instantiated as !!(p,xs) =  ss atom
		in  if p = op == then
		    testEq xs
		    else
			if p mem rels
			    then isTrue instantiated
			else
			    V(lit2var instantiated)
		end
	    fun I x = x
	    val bdd = Bdd.eval types constants (translate I) axiom
	    val support = map Bdd.var2lit (Bdd.SUPPORT bdd)

	    fun nstates f =  Bdd.STATES f
            fun size f = Bdd.SIZE f
	    val valuation = 
		case (Bdd.SAT bdd) of
		    Some vars => map (lit2string o var2lit) vars
	      | None => ["NO SATISFYING VALUATION"]
	in
	    (BDD_STATS{size=size bdd,states=nstates bdd, variables=List.length support},
	     SATISFYING_VALUATION valuation)
	end;

val vo = VO;

fun propsat domainName =
		let val domainFile = TextIO.openIn domainName
		    val domain = readDomain (TextIO.getInstream domainFile)
			(* TextIO.flushOut  TextIO.stdOut*)

		in 
		    (TextIO.closeIn domainFile;
                     mkBdd domain)
		end

fun install () = ( 
		  PolyML.commit(); 
		  start();
		  reordering sift;
		  TextIO.output( TextIO.stdOut,
				"\n\n Welcome to PropSat \n\n" 
				^ " propsat : string -> BDD_STATS * SATISFYING VALUATION \n\n"
				^ " Usage: propsat <domainFileName> ; \n\n"
				^ " NB format for domains changed \n"
				^ " axiom => axioms    fact => facts \n"
				^ " facts can be universal Horn sentences \n"
				^ " For details see www.inf.ed.ac.uk/teaching/modules/propm/papers/ddl.pdf \n\n"
        )
		  );
    

end