(*
02157 - Functional Programming
Mandatory assignment 3: Solver for Propositional Logic

Solved by:
Alexander Rosenberg Johansen
s145706


*)

//For required patternmatching by FSharp, that would denote a pattern not designed for
exception Error of string
//1.
type Prop = | A of string
            | Dis of Prop * Prop
            | Con of Prop * Prop
            | Neg of Prop


//2.
//dml is short for de Morgan laws
//Argument: Prop, a recursive type responding to a property tree
//Result: Prop, now modified to match the de Morgan Law (dml)
//recursively going over every vertex in the Prop-tree and matches it with the de Morgan Law, modifying the prop if match exists
let rec dml :Prop -> Prop = function
    | Neg(Con(p1,p2))    -> Dis(dml (Neg(p1)), dml (Neg(p2)))   //dml case: "¬(a ∧ b) is equivalent to (¬a) ∨ (¬b)"
    | Neg(Dis(p1,p2))    -> Con(dml (Neg(p1)), dml (Neg(p2)))   //dml case: "¬(a ∨ b) is equivalent to (¬a) ∧ (¬b)"
    | Neg(Neg(p))        -> dml p                               //dml case: "¬(¬a) is equivalent to a"
    | A(p)               -> A(p)                //Base case
    | Dis(p1,p2)         -> Dis(dml p1, dml p2) //Not a "dml", branching
    | Con(p1,p2)         -> Con(dml p1, dml p2) //Not a "dml", branching
    | Neg(p)             -> Neg(dml p)          //Not a "dml", branching


//3.
//dl is short for distributed law
//Argument: Prop
//Result: Prop, now modified to match the Distributed Law (dl)
//recursively going over every vertex in the Prop-tree and matches it with the Distributed Law, modifying the prop if match exists
let rec dl :Prop -> Prop = function
  //  |Con(a,Dis(b,c)) -> Dis(Con(dl a,dl b),Con(dl a,dl c))   //dl case: "a ∧ (b ∨ c) is equivalent to (a ∧ b) ∨ (a ∧ c)"
  |Con(a,Dis(b,c)) -> Dis(dl (Con(a,b)), dl (Con(a,c)))
  //  |Con(Dis(a,b),c) -> Dis(Con(dl a,dl c),Con(dl b,dl c))   //dl case: "(a ∨ b) ∧ c is equivalent to (a ∧ c) ∨ (b ∧ c)"
  |Con(Dis(a,b),c) -> Dis(dl (Con(a,c)), dl (Con(b,c)))
    |A(p)               -> A(p)             //Base case
    |Dis(p1,p2)         -> Dis(dl p1,dl p2) //Not a "dl", branching
    |Con(p1,p2)         -> Con(dl p1,dl p2) //Not a "dl", branching
    |Neg(p)             -> Neg(dl p)        //Not a "dl", branching

//4.1
//Argument: Prop
//Result: Set<Prop> of Prop literals
//recursively going over the prop to find literals, packing these literals in a set, set is used to avoid doubles
//Setting this function as private to dnfToSet would be preferable
let rec litOf :Prop -> Set<Prop> = function
    |A(p)       -> Set [A(p)]               //Base-case, literal found!
    |Neg(A(p))  -> Set [Neg(A(p))]          //Base-case, literal found!
    |Con(p1,p2) -> let setP1 = litOf p1     //For ease of reading
                   let setP2 = litOf p2     //For ease of reading
                   Set.union setP1 setP2    //Unions the Conjunction
    |p          -> raise (Error("litOf cannot resolve"))  //incomplete Pattern matches, should not happen

//Simple function to check for having either a literal or a negation of a literal.
//Setting this function as private to dnfToSet would be preferable
let auxNegOrA :Prop*Prop -> bool = function
    |A(p1),A(p2)      -> true
    |Neg(p1),A(p2)    -> true
    |A(p1),Neg(p2)    -> true
    |Neg(p1),Neg(p2)  -> true
    |p1,p2          -> false
//4.2
//Argument: Prop, which matches the de Morgan Law and Distributed Law
//Result: Set<Set<Prop>> for a collection of basic conjunctions
//recursively goes over every disjunction, uses litOf :Prop -> Set<Prop> to get the literals, denoted "Basic conjunct", where after each conjunt is placed into the total set
let rec dnfToSet :Prop -> Set<Set<Prop>> = function
    |Dis(p1,p2)  -> Set.union (dnfToSet(p1))  (dnfToSet(p2))
    |Con(p1,p2) when auxNegOrA(p1,p2) -> Set.add (litOf (Con(p1,p2))) Set.empty
    |Con(p1,p2) -> Set.union (dnfToSet(p1)) (dnfToSet(p2))
    |p           -> Set.add (litOf (p)) Set.empty

//Argument: Prop
//Result: Prop
//an auxilary function to negate(flip) a literal
let auxIsConsistent :Prop -> Prop = function
    |A(p)       -> Neg(A(p))
    |Neg(p)     -> p
    |p          -> raise (Error("litOf cannot resolve"))

//5.1
//Argument: Set<Prop>
//Result: bool to figure if there exists a pair of complementary literals, "False" if so, else "True"
//Setting this function as private to removeInconsistent would be preferable
let rec isConsistent :Set<Prop> -> bool = function
    |latSet ->  let comparisonSet = Set.foldBack(fun x set -> if Set.contains (auxIsConsistent x) (Set.remove x latSet) then Set.add x Set.empty else set) latSet Set.empty
                if Set.intersect latSet comparisonSet <> Set.empty then false else true

//5.2
//Argument: Set<Set<Prop>>
//Result: Set<Set<Prop>> now with inconsistent literals removed
//Uses Set.filter to remove all inconsistent literals
let removeInconsistent :Set<Set<Prop>> -> Set<Set<Prop>> = function
    |allThemLats -> Set.filter(fun x -> (isConsistent x)) allThemLats

//6.1
//Calls all previous functions to get a DNF set
let toDNFsets :Prop -> Set<Set<Prop>> = function
    |p   -> removeInconsistent (dnfToSet (dl (dml p)))

//6.2
//Logical equivalence
let impl :Prop*Prop -> Prop = function
    |a,b -> Dis(Neg(a),b)

//6.3
//Logical equivalence
let iff :Prop*Prop -> Prop = function
    |a,b -> Con(impl(a,b), impl(b,a))

//6.4
//Solving
//• ((¬p) ⇒ (¬q)) ⇒ (p ⇒ q)
//• ((¬p) ⇒ (¬q)) ⇒ (q ⇒ p)
//Setting literals for
let p = A("p")
let q = A("q")
let negP = Neg(p)
let negQ = Neg(q)

let first1 = impl(negP,negQ)
let first2 = impl(p,q)
let propFirst = impl(first1,first2)
let resFirst = toDNFsets propFirst //((¬p) ⇒ (¬q)) ⇒ (p ⇒ q)

let second1 = first1
let second2 = impl(q,p)
let propSecond = impl(second1,second2)
let resSecond = toDNFsets propSecond //((¬p) ⇒ (¬q)) ⇒ (q ⇒ p)

//7
//I cannot figure the propositional logic, but an implementation would rely on finding consistent basic conjuncts through a toDNFsets call

//8.1
//Argument: int
//Result: Prop with n Conjunctions of Disjunctions
let rec badProp :int -> Prop = function
    |1 -> Dis(A("p"+ string 1),A("q" + string 1))
    |n -> Con(Dis(A("p" + string n),A("q" + string n)),badProp(n-1))

//Simple testcases to prove every function in the toDNFsets chain
let testBadProp = badProp 4
let testDML = dml testBadProp
let testDL = dl testDML
let testDnfToSets = dnfToSet testDL
let testRemoveInconsistent = removeInconsistent testDnfToSets

//8.2
//Tests badProp n
//KNOWN ERROR: Only gives 2*N as opposed to 2**n = 2^n, maybe because my dl function doesn't "pack" my Props correctly?
let testToDNFsets = toDNFsets testBadProp