Translation from intuitionistic logic to S4

ModalIntuitionistic.hs

module ModalIntuitionistic
  where

data Prop
  = V String
  | Not Prop
  | And Prop Prop
  | Or Prop Prop
  | Prop :=> Prop
  | Box Prop
  deriving (Show)

-- From https://twitter.com/rg9119/status/1662874684403359744
prop :: Prop
prop =
  (And (V "A" :=> (V "A" :=> V "B"))
       ((V "A" :=> V "B") :=> V "A"))
    :=>
  V "B"

lem :: Prop
lem = Or (V "A") (Not (V "A"))

-- Based on https://cs.stackexchange.com/a/22267
translate :: Prop -> Prop
translate (Box _) = error "translate: Box"
translate (V n) = V n
translate (And a b) = And (translate a) (translate b)
translate (Or a b) = Or (Box (translate a)) (Box (translate b))
translate (a :=> b) = Box (translate a) :=> translate b
translate (Not a) = Not (Box (translate a)) -- Based on translating (a :=> F), which would be (Box (translate a) :=> F). That reduces to what we have here

ppr :: Prop -> String
ppr (V n) = n
ppr (And x y) = pprP x ++ " ∧ " ++ pprP y
ppr (Or x y) = pprP x ++ " ∨ " ++ pprP y
ppr (x :=> y) = pprP x ++ " → " ++ pprP y
ppr (Not x) = "¬ " ++ pprP x
ppr (Box x) = "□ " ++ pprP x

pprP :: Prop -> String
pprP p
  | isNested p = "(" ++ ppr p ++ ")"
  | otherwise = ppr p

isNested :: Prop -> Bool
isNested (V _) = False
isNested _ = True