module COSPhw2_FOL where

import Data.List

---------- SYNTAX ----------


-- Variables and Constants: a variable consists of a String (e.g. "x" or "y")
-- and possibly one or more indices (a list of integers);
-- a constant is simply a string

type Name     = String 
type Index    = [Int]
data Variable = Variable Name Index deriving (Eq,Ord)
data Constant = Constant Name       deriving (Eq,Ord)

-- SimpleTerm: terms are either variables or constants; 
-- we don't consider other function symbols

data SimpleTerm = Var Variable | Cons Constant deriving (Eq,Ord)

-- this specifies how we want to display terms:
instance Show SimpleTerm where
  show (Cons (Constant name)) = name                          
  show (Var (Variable name []))  = name
  show (Var (Variable name [i])) = name ++ show i
  show (Var (Variable name is )) = name ++ showInts is
     where showInts []     = "" 
           showInts [i]    = show i  
           showInts (i:is) = show i ++ "_" ++ showInts is

-- Formulas

data Formula a = Atom String [a]
               | Eq a a
               | Neg  (Formula a)
               | Impl (Formula a) (Formula a) 
               | Equi (Formula a) (Formula a)
               | Conj [Formula a]
               | Disj [Formula a] 
               | Forall Variable (Formula a)
               | Exists Variable (Formula a)
               deriving Eq

-- this specifies how we want to display formulas:
instance Show a => Show (Formula a) where 
  show (Atom s [])   = s
  show (Atom s xs)   = s ++ show xs 
  show (Eq t1 t2)    = show t1 ++ "==" ++ show t2
  show (Neg form)    = '~' : (show form)
  show (Impl f1 f2)  = "(" ++ show f1 ++ "==>" 
                           ++ show f2 ++ ")"
  show (Equi f1 f2)  = "(" ++ show f1 ++ "<=>" 
                           ++ show f2 ++ ")"
  show (Conj [])     = "true" 
  show (Conj fs)     = showCj fs
    where showCj []     = ""
          showCj [f]    = show f
          showCj (f:fs) = "(" ++ show f ++ " /\\ " ++ showCj fs ++ ")"
  show (Disj [])     = "false" 
  show (Disj fs)     = showDj fs 
    where showDj []     = ""
          showDj [f]    = show f
          showDj (f:fs) = "(" ++ show f ++ " \\/ " ++ showDj fs ++ ")"
  show (Forall v f)  = "Forall " ++  show (Var v) ++ (' ' : show f)
  show (Exists v f)  = "Exists " ++  show (Var v) ++ (' ' : show f)


-- some example formulas:
f0a = Atom "Alice" [Cons (Constant "a")]
f0b = Atom "Princess" [Var (Variable "x" [])]
f0c = Conj [f0a,f0b]
f1  = Exists (Variable "x" []) (Atom "Princess" [Var (Variable "x" [])] )
f2  = Forall (Variable "x" []) (Atom "Hate" [Cons (Constant "a"),
                                              Var  (Variable "x" []) ] )


-------- SEMANTICS ---------

-- MODEL

-- what counts as an entity:

data Entity = A | B | C | D | E | F | G
            | H | I | J | K | L | M | N 
            | O | P | Q | R | S | T | U 
            | V | W | X | Y | Z | Unspec
     deriving (Eq,Show,Bounded,Enum)

-- we take the domain of entities in our model to include all the
-- entities we have defined above 
domain :: [Entity]
domain =  [minBound..maxBound] 

-- one-place predicates denote sets (lists); we define them with
-- a characteristic function which given an entity, returns True iff
-- that entity is an element of the set denoted by the predicate, else
-- it returns False.

type OnePlacePred = Entity -> Bool

-- examples of one-place predicates
princess, laugh :: OnePlacePred
princess = \x -> elem x [A,B,C]
laugh = \x -> elem x [B]

-- two-place predicates denote sets of pairs (lists of pairs); we
-- define them with a characteristic function which given two
-- entities, returns True iff the pair made up of those entities is an
-- element of the set denoted by the predicate, els it returns False.

type TwoPlacePred = Entity -> Entity -> Bool

-- examples of two-place predicates
hate, admire :: TwoPlacePred
hate   = \x -> \y -> elem (x,y) [(A,B),(C,A)]
admire = \x -> \y -> elem (x,y) [(B,A),(G,P)]


-- INTERPRETATION FUNCTIONS

-- Interp: interpretation function for predicates. 
-- given a predicate (a String) and its arguments (a list of
-- entities), it retuns either True or False
-- It returns True iff the arguments are in the denotation of the
-- predicate, as specified in the model.

type Interp = String -> [Entity] -> Bool

-- an example interpretation function:
int :: Interp
int "Princess" = \ [x] -> princess x
int "Hate" = \ [x,y] -> hate x y

-- ConsInterp: interpretation function for constants
-- given a constant, it returns an entity
-- (we do not consider any other type of functions)

type ConsInterp = Constant -> Entity

-- an example constant interpretation function:
consInt :: ConsInterp
consInt (Constant "Alice") = A 


-- VARIABLE ASSIGNMENTS

-- Assignment: given a variable, it returns an entity. 

type Assignment = Variable -> Entity

-- an example variable assignment:
ass :: Assignment
ass (Variable "x" []) = D
ass (Variable "y" []) = B
ass (Variable "z" []) = C


-- change: a function that changes an assignment g into a different
-- assignment that differs from g only on the value it assigns to
-- variable x. Needed for the interpretation of quantified formulas.
-- Given an assignment g, a variable x and an entity d, it returns a
-- new assignment where x is assigned to d

change :: Assignment -> Variable -> Entity -> Assignment
change g x d = \ v -> if x == v then d else g v



-- EVALUATION

-- termEval: given a constant interpretation function (ConsInterp) a
-- variable assignment (Assignment) and a simple term (SimpleTerm),
-- it returns an entity in the domain. 
-- If the term is a variable, it applies the variable assignment (g), 
-- if it is a constant, it applies the constant interpretation function (ci)

termEval :: ConsInterp -> Assignment -> SimpleTerm -> Entity
termEval ci g (Var v) = g v
termEval ci g (Cons c) = ci c


-- eval: the evaluation funtion for formulas. Given a domain of
-- entities, an interpretation function (for predicates), a constant
-- interpretation function, a variable assignment, and a formula with
-- simple terms, it returns either True or False.

eval ::
    [Entity]    -> 
    Interp      -> 
    ConsInterp  -> 
    Assignment  -> 
    Formula SimpleTerm -> Bool

eval dom i ci = eval' where 
    eval' g (Atom str ts) = i str (map (termEval ci g) ts)
    eval' g (Eq   t1 t2)  = (termEval ci g t1) == (termEval ci g t2) 
    eval' g (Neg  f)      = not (eval' g f)
    eval' g (Impl f1 f2)  = not ((eval' g f1) && 
                                  not (eval' g f2))
    eval' g (Equi f1 f2)  = (eval' g f1) == (eval' g f2)
    eval' g (Conj fs)     = and (map (eval' g) fs)
    eval' g (Disj fs)     = or  (map (eval' g) fs)
    eval' g (Forall v f)  = and [ eval' (change g v d) f | d <- dom ]
    eval' g (Exists v f)  = or  [ eval' (change g v d) f | d <- dom ]