content: {-@ LIQUID "--reflection"     @-}
  {-@ LIQUID "--ple"            @-}
  {-@ LIQUID "--no-termination" @-}
  
  module Tmp where
  
  import Prelude hiding (lookup)
  
  data Wff = Var Int
           | Not Wff
           | Wff :|: Wff
           | Wff :&: Wff
           deriving (Eq, Ord)
  
  data NNF = Atom Bool Int
           | NOr NNF NNF
           | NAnd NNF NNF
  
  {-@ reflect toWff @-}
  toWff :: NNF -> Wff
  toWff (Atom True i) = Var i
  toWff (Atom False i) = Not (Var i)
  toWff (NOr f g) = toWff f :|: toWff g
  toWff (NAnd f g) = toWff f :&: toWff g
  
  {-@ reflect lookup @-}
  lookup :: [a] -> a -> Int -> a
  lookup []     def _ = def
  lookup (v:_)  _   0 = v
  lookup (_:vs) def k = lookup vs def (k-1)
  
  {-@ reflect eval @-}
  eval :: [Bool] -> Wff -> Bool
  eval s (Var i)   = lookup s False i
  eval s (f :&: g) = eval s f && eval s g
  eval s (f :|: g) = (eval s f) || (eval s g)
  eval s (Not f)   = not (eval s f)
  
  {-@ reflect evalNNF @-}
  evalNNF :: [Bool] -> NNF -> Bool
  evalNNF s (Atom True i)  = lookup s False i
  evalNNF s (Atom False i) = not (lookup s False i)
  evalNNF s (NOr p q)      = evalNNF s p || evalNNF s q
  evalNNF s (NAnd p q)     = evalNNF s p && evalNNF s q
  
  {-@ toNNF :: s:[Bool] -> p:Wff -> { q: NNF | eval s p = evalNNF s q } @-}
  toNNF :: [Bool] -> Wff -> NNF
  toNNF _ (Var i)  = Atom True i
  toNNF s (Not p)         = case p of
                              Not p -> let glub = toNNF s p in glub
                              _     -> undefined
  toNNF _ _        = undefined 
  
  