content: -- D. Sannella. M Fourman, H. Peng and P. Wadler
  -- Introduction to Computation: Haskell, Logic and Automata
  -- Undergraduate Topics in Computer Science, Springer (2021)
  -- ISBN 978-3-030-76907
  
  -- Chapter 16 : Expression Trees
  
  module Chap16_expression_trees where
  
  import Data.List (nub)
  
  import Test.QuickCheck (Arbitrary, arbitrary, sized, oneof)
  import Control.Monad (liftM, liftM2)
  
  -- Arithmetic expressions
  
  data Exp = Lit Int
           | Add Exp Exp
           | Mul Exp Exp
    deriving Eq
  
  e0 = Add (Lit 1) (Mul (Lit 2) (Lit 3))
  e1 = Mul (Add (Lit 1) (Lit 2)) (Lit 3)
  e2 = Add e0 (Mul (Lit 4) e1)
  
  showExp :: Exp -> String
  showExp (Lit n)   = show n
  showExp (Add e f) = par (showExp e ++ " + " ++ showExp f)
  showExp (Mul e f) = par (showExp e ++ " * " ++ showExp f)
  
  par :: String -> String
  par s = "(" ++ s ++ ")"
  
  instance Show Exp where
    show e = showExp e
  
  -- Evaluating arithmetic expressions
  
  evalExp :: Exp -> Int
  evalExp (Lit n)   = n
  evalExp (Add e f) = evalExp e + evalExp f
  evalExp (Mul e f) = evalExp e * evalExp f
  
  i0 = evalExp e0
  
  i1 = evalExp e1
  
  i2 = evalExp e2
  
  -- Arithmetic expressions with infix constructors
  
  data Exp' = Lit' Int
            | Exp' `ADD` Exp'
            | Exp' `MUL` Exp'
    deriving Eq
  
  e0' = Lit' 1 `ADD` (Lit' 2 `MUL` Lit' 3)
  e1' = (Lit' 1 `ADD` Lit' 2) `MUL` Lit' 3
  e2' = e0' `ADD` ((Lit' 4) `MUL` e1')
  
  instance Show Exp' where
    show (Lit' n)     = show n
    show (e `ADD` f) = par (show e ++ " + " ++ show f)
    show (e `MUL` f) = par (show e ++ " * " ++ show f)
  
  evalExp' :: Exp' -> Int
  evalExp' (Lit' n)     = n
  evalExp' (e `ADD` f) = evalExp' e + evalExp' f
  evalExp' (e `MUL` f) = evalExp' e * evalExp' f
  
  data Exp'' = Lit'' Int
           | Exp'' :+: Exp''
           | Exp'' :*: Exp''
    deriving Eq
  
  e0'' = Lit'' 1 :+: (Lit'' 2 :*: Lit'' 3)
  e1'' = (Lit'' 1 :+: Lit'' 2) :*: Lit'' 3
  e2'' = e0'' :+: ((Lit'' 4) :*: e1'')
  
  instance Show Exp'' where
    show (Lit'' n)   = show n
    show (e :+: f) = par (show e ++ " + " ++ show f)
    show (e :*: f) = par (show e ++ " * " ++ show f)
  
  evalExp'' :: Exp'' -> Int
  evalExp'' (Lit'' n)   = n
  evalExp'' (e :+: f) = evalExp'' e + evalExp'' f
  evalExp'' (e :*: f) = evalExp'' e * evalExp'' f
  
  -- Propositions
  
  type Name = String
  data Prop = Var Name
            | F
            | T
            | Not Prop
            | Prop :||: Prop
            | Prop :&&: Prop
    deriving Eq
  
  p0 = Var "a" :&&: Not (Var "a")
  p1 = (Var "a" :&&: Var "b")
       :||: (Not (Var "a") :&&: Not (Var "b"))
  p2 = (Var "a" :&&: Not (Var "b")
                :&&: (Var "c" :||: (Var "d" :&&: Var "b"))
           :||: (Not (Var "b") :&&: Not (Var "a")))
       :&&: Var "c"
  
  instance Show Prop where
    show (Var x)    = x
    show F          = "F"
    show T          = "T"
    show (Not p)    = par ("not " ++ show p)
    show (p :||: q) = par (show p ++ " || " ++ show q)
    show (p :&&: q) = par (show p ++ " && " ++ show q)
  
  -- Evaluating propositions
  
  type Valn = Name -> Bool
  
  evalProp :: Valn -> Prop -> Bool
  evalProp vn (Var x)    = vn x
  evalProp vn F          = False
  evalProp vn T          = True
  evalProp vn (Not p)    = not (evalProp vn p)
  evalProp vn (p :||: q) = evalProp vn p || evalProp vn q
  evalProp vn (p :&&: q) = evalProp vn p && evalProp vn q
  
  valn :: Valn
  valn "a" = True
  valn "b" = True
  valn "c" = False
  valn "d" = True
  
  b0 = evalProp valn p0
  
  b1 = evalProp valn p1
  
  b2 = evalProp valn p2
  
  -- Satisfiability of propositions
  
  type Names = [Name]
  
  names :: Prop -> Names
  names (Var x)    = [x]
  names F          = []
  names T          = []
  names (Not p)    = names p
  names (p :||: q) = nub (names p ++ names q)
  names (p :&&: q) = nub (names p ++ names q)
  
  n0 = names p0
  
  n1 = names p1
  
  n2 = names p2
  
  empty :: Valn
  empty y = error "undefined"
  
  extend :: Valn -> Name -> Bool -> Valn
  extend vn x b y | x == y    = b
                  | otherwise = vn y
  
  valns :: Names -> [Valn]
  valns [] = [ empty ]
  valns (x:xs)
           = [ extend vn x b | vn <- valns xs, b <- [True, False] ]
  
  satisfiable :: Prop -> Bool
  satisfiable p = or [ evalProp vn p | vn <- valns (names p) ]
  
  bs0 = [ evalProp vn p0 | vn <- valns (names p0) ]
  
  bss0 = satisfiable p0
  
  bs1 = [ evalProp vn p1 | vn <- valns (names p1) ]
  
  bss1 = satisfiable p1
  
  bs2 = [ evalProp vn p2 | vn <- valns (names p2) ]
  
  bss2 = satisfiable p2
  
  -- Structural induction
  
  simplify :: Exp -> Exp
  simplify (Lit n)     = Lit n
  simplify (e `Add` f)
    | e' == Lit 0      = f'
    | f' == Lit 0      = e'
    | otherwise        = e' `Add` f'
    where e' = simplify e
          f' = simplify f
  simplify (e `Mul` f) = (simplify e) `Mul` (simplify f)
  
  -- Mutual recursion
  
  data Exp''' = Lit''' Int
              | Add''' Exp''' Exp'''
              | Mul''' Exp''' Exp'''
              | If Cond Exp''' Exp'''
    deriving Eq
    
  data Cond = Eq Exp''' Exp'''
            | Lt Exp''' Exp'''
            | Gt Exp''' Exp'''
    deriving Eq
  
  me0 = Add''' (Lit''' 1) (Mul''' (Lit''' 2) (Lit''' 3))
  me1 = Mul''' (Add''' (Lit''' 1) (Lit''' 2)) (Lit''' 3)
  mc0 = Lt me0 me1
  me2 = If mc0 me0 me1
  
  instance Show Exp''' where
    show (Lit''' n)   = show n
    show (Add''' e f) = par (show e ++ " + " ++ show f)
    show (Mul''' e f) = par (show e ++ " * " ++ show f)
    show (If c e f)   = "if " ++ show c
                              ++ " then " ++ show e
                              ++ " else " ++ show f
  
  instance Show Cond where
    show (Eq e f) = show e ++ " == " ++ show f
    show (Lt e f) = show e ++ " < " ++ show f
    show (Gt e f) = show e ++ " > " ++ show f
  
  evalExp''' :: Exp''' -> Int
  evalExp''' (Lit''' n)   = n
  evalExp''' (Add''' e f) = evalExp''' e + evalExp''' f
  evalExp''' (Mul''' e f) = evalExp''' e * evalExp''' f
  evalExp''' (If c e f)   = if evalCond c then evalExp''' e
                            else evalExp''' f
                       
  evalCond:: Cond -> Bool
  evalCond (Eq e f) = evalExp''' e == evalExp''' f
  evalCond (Lt e f) = evalExp''' e < evalExp''' f
  evalCond (Gt e f) = evalExp''' e > evalExp''' f
  
  i0''' = evalExp''' me0
  
  i1''' = evalExp''' me1
  
  b0''' = evalCond mc0
  
  i2''' = evalExp''' me2
  
  -- Exercise 5
  
  instance Arbitrary Prop where
    arbitrary = sized prop
      where
        prop n | n<=0 = oneof [liftM Var arbitrary,
                               return T,
                               return F]
               | otherwise
                      = oneof [liftM Not subprop,
                               liftM2 (:||:) subprop subprop,
                               liftM2 (:&&:) subprop subprop]
          where subprop = prop (n `div` 2)
  