{-# OPTIONS -W #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

-- Here we encode the ``target language'', the language
-- to express denotations (or, meanings)
-- We use the same technique to embed a formal language
-- as the one we used before to embed a fraghment of
-- English (cf. Montague's famous quote).

-- To warm-up, we start with the language of
-- classical propositional logic (without equality)
-- Formula simplification (the interpreter P below)
-- is much easier to explain in the propositional case.

module Prop where

import qualified Data.Set as S

-- Embedding of the language of propositional logic

class Prop lrepr where
  -- Propositional letters 
  pretty'  :: lrepr
  quiet'   :: lrepr
  raining' :: lrepr
  -- (more can be added later)

  true     :: lrepr
  neg      :: lrepr -> lrepr
  conj     :: lrepr -> lrepr -> lrepr

-- sample formulas
fml1 = neg (conj (neg (neg true)) (neg true))
fml2 = quiet' `conj` raining'
fml3 = pretty' `conj` neg raining' `conj` true `conj` pretty'

-- Ex: Where is false and disjunction?
-- How to write TRUE AND (FALSE == (TRUE OR P))






-- Abbreviations
-- They are not part of Prop (not part of the language)
-- Consider them as `abbreviations', of `macros'

false    = neg true
disj x y = neg (conj (neg x) (neg y))

fml4 = true `conj` (false `disj` pretty')

-- I still haven't written the exercise. It remains
-- an exercise. We need to add implication and
-- equivalence.



-- ------------------------------------------------------------------------
-- Models

-- First model: the domain is Bool (Boolean algebra with two
-- constants, True and False)

data R = R { unR :: Bool }

instance Prop R where
  -- One particular interpretation function
  -- interpreting prop letters
  pretty'                = R True
  quiet'                 = R True
  raining'               = R False

  -- Logical part of the model
  true                   = R True
  neg (R True)           = R False
  neg (R False)          = R True
  conj (R True) (R True) = R True
  conj _        _        = R False


-- Evaluate our examples in the model

fml1R = unR fml1
fml2R = unR fml2
fml3R = unR fml3
fml4R = unR fml4

-- Exercise (adv): the instance R has the interpretation
-- of propositional letters wired-in.
-- If we wish to try a different interpretation function,
-- we have to re-write the instance, repeating
-- neg and conj (which stay constant)
-- Re-write R so that the interpretation of propositional
-- letters (I) is a parameter, to be specified by the user.




-- We can give another model: the standard set-theoretical
-- one, in a richer Boolean algebra (posets)

-- Ex: What are the deriving Eq and Ord, and why we need them?

data Event = PP | PQ | PR
	deriving (Eq, Ord, Show)


-- Ex: What is the meaning of the following?
s_top = S.fromList [PP,PQ,PR]


data RS = RS{unRS :: S.Set Event}

instance Prop RS where
  -- One particular interpretation function
  -- interpreting prop letters
  pretty'                = RS (S.singleton PP)
  quiet'                 = RS (S.singleton PQ)
  raining'               = RS (S.singleton PR)

  -- Logical part of the model
  true                   = RS s_top
  neg (RS s)             = RS (S.difference s_top s)
  conj (RS s1) (RS s2)   = RS (S.intersection s1 s2)


fml1RS = unRS fml1
fml2RS = unRS fml2
fml3RS = unRS fml3
fml4RS = unRS fml4

-- Compare  fml3RS vs fml3R and the same for fml4
-- See the difference? Why?
-- fml1R and fml3R were the same; but fml1RS and fml3RS are not
-- Some models are more discriminating...
-- Is it possible to build a model that is even more discriminating?



-- And yet another `model'. Why do we need it?
-- Is it a real model?


data C = C { unC :: String }

instance Prop C where
  pretty'          = C "P"
  quiet'           = C "Q"
  raining'         = C "R"
  true             = C "T"
  neg (C x)        = C ("-" ++ x)
  conj (C x) (C y) = C ("(" ++ x ++ " & " ++ y ++ ")")

fml1C = unC fml1
fml2C = unC fml2
fml3C = unC fml3
fml4C = unC fml4


-- ------------------------------------------------------------------------
-- Simplification: (very) simple inference

-- an instance of a language _transformation_

-- data P0 lrepr = P0{unP0 :: lrepr}
data P0 lrepr = P0 lrepr
unP0 (P0 x) = x

instance (Prop lrepr) => Prop (P0 lrepr) where
  -- is there a weird self-reference in here?
  -- how could this possibly work?
  pretty'            = P0 pretty'
  quiet'             = P0 quiet'
  raining'           = P0 raining'
  true               = P0 true
  neg (P0 x)         = P0 (neg x)
  conj (P0 xs) (P0 ys) = P0 (conj xs ys)


-- How to use P0?


fml1P0C = unC . unP0 $ fml1
fml1P0C' = unC (unP0 fml1)



-- Isn't this stupid?
-- What possible use could be for P0?
-- (if it isn't a rhetorical question, it should be)

-- What is the intended meaning for known?
data P lrepr = P { unP :: lrepr, known :: Maybe Bool }

instance (Prop lrepr) => Prop (P lrepr) where
  pretty'            = P pretty' Nothing
  quiet'             = P quiet' Nothing
  raining'           = P raining' Nothing

  true               = P true (Just True)

  neg (P _ (Just False)) = true
  neg (P _ (Just True))  = P (neg true) (Just False)
  -- Why not to put false on the right-hand side of the above?
  neg (P x _)            = P (neg x) Nothing

  conj (P _ (Just True)) y       = y
  conj x (P _ (Just True))       = x
  conj (P _ (Just False)) _      = false
  conj _ (P _ (Just False))      = false
  conj (P x _) (P y _)           = P (conj x y) Nothing


fml1PC = unC . unP $ fml1
fml2PC = unC . unP $ fml2
fml3PC = unC . unP $ fml3
fml4PC = unC . unP $ fml4

-- It is good. Still we can do better.
-- Can we simplify double-negation and repeated
-- occurrences of the same literal?
-- Does this remind you of normalization?