content: {-@ LIQUID "--reflection"  @-}
  {-@ LIQUID "--ple"         @-}
  
  module Verifier () where 
  
  import           ProofCombinators
  import qualified State as S
  import           Expressions  
  import           Imp 
  import           BigStep hiding (And)
  import           Axiomatic 
  
  imports = (FH undefined undefined undefined)
  
  ----------------------------------------------------------------
  -- TODO: Move into FloydHoare.hs 
  ----------------------------------------------------------------
  
  ----------------------------------------------------------------
  -- | Lets build a 'verify'-er
  ----------------------------------------------------------------
  
  {-@ verify :: p:_ -> c:_ -> q:_ -> Valid (vc' p c q) -> () @-}
  verify :: Assertion -> ICom -> Assertion -> Valid -> () 
  verify _ _ _ _ = () 
  
  ----------------------------------------------------------------
  ex1   :: () -> ()
  ex1 _ = verify p c q (\_ -> ()) 
    where 
      p = tt                                    -- { true } 
      c = IAssign "x" (N 5)                     --    x := 5
      q = Equal (V "x") (N 5)                   -- { x == 5 }
  
  ----------------------------------------------------------------
  
  ex2   :: () -> () 
  ex2 _ = verify p c q (\_ -> ()) 
    where 
      p = Equal (V "x") (N 2)                   -- { x = 2 } 
      c = IAssign "x" (Plus (V "x") (N 1))      --    x := x + 1
      q = Equal (V "x") (N 3)                   -- { x = 3 }
  
  ----------------------------------------------------------------
  
  ex2a   :: () -> () 
  ex2a _ = verify p c q (\_ -> ()) 
    where 
      p  = Equal (V "x") (N 2)                   -- { x = 2 } 
      c  = c1 `ISeq` c1                          --    x := x + 1 
      c1 = IAssign "x" (Plus (V "x") (N 1))      --    x := x + 1
      q  = Equal (V "x") (N 4)                   -- { x = 4 }
  
  ----------------------------------------------------------------
  
  ex4  :: () -> () 
  ex4 _  = verify p (c1 `ISeq` c2) q (\_ -> ()) 
    where 
      p  = tt                                    -- { True } 
      c1 = IAssign "x" (N 5)                     --    x := 5 
      c2 = IAssign "y" (V "x")                   --    y := x 
      q  = Equal (V "y") (N 5)                   -- { y = 5 }
  
  ----------------------------------------------------------------
  ex5  :: () -> () 
  ex5 _ = verify p c q (\_ -> ()) 
    where 
      p = ((V "x") `Equal` (N 2)) `bAnd` 
          ((V "x") `Equal` (N 3))                -- { x = 2 && x = 3} 
      c = IAssign "x" (N 5)                      --    x := 5
      q = V "x" `Equal` N 0                      -- { x = 0}
  
  ----------------------------------------------------------------
  
  ex8  :: () -> () 
  ex8 _ = verify p c q (\_ -> ()) 
    where 
      p = tt                                     -- { true } 
      c = IWhile i tt ISkip                      --    WHILE_i true SKIP 
      q = ff                                     -- { false }
      i = tt -- undefined -- TODO: In class
  
  ----------------------------------------------------------------
  
  ex9  :: () -> () 
  ex9 _ = verify p c q (\_ -> ()) 
    where 
      p = Equal (V "x") (N 0)                    -- { x = 0 } 
      c = IWhile i (Leq (V "x") (N 0))           --   WHILE_i (x <= 0) DO
            (IAssign "x" (Plus (V "x") (N 1)))   --     x := x + 1
      q = Equal (V "x") (N 1)                    -- { x = 1 } 
      i = undefined -- TODO: In class
  
  ----------------------------------------------------------------
  ex10  :: () -> () 
  ex10 _ = verify p c q (\_ -> ()) 
    where 
      p = Equal (V "x") (N 1)                    -- { x = 1 } 
      c = IWhile i (Not (Leq (V "x") (N 0)))     --   WHILE_i not (x <= 0) DO
            (IAssign "x" (Plus (V "x") (N 1)))   --     x := x + 1
      q = Equal (V "x") (N 100)                  -- { x = 100 } 
      i = undefined -- TODO: In class
  
  -------------------------------------------------------------------------------
  -- | Example 1: branching
  -------------------------------------------------------------------------------
  
  bx1 :: () -> () 
  bx1 _ = verify p c q (\_ -> ()) 
    where 
      p = tt                                     -- { true } 
      c = IIf (Equal (V "x") (N 0))              --   IF x == 0 
              (IAssign "y" (N 2))                --     THEN y := 2
              (IAssign "y" (Plus (V "x") (N 1))) --     ELSE y := x + 1
      q = Leq (V "x") (V "y")                    -- { x <= y } 
  
  -------------------------------------------------------------------------------
  -- | Example 2: Swapping Using Addition and Subtraction 
  -------------------------------------------------------------------------------
  
  bx2 :: () -> () 
  bx2 _ = verify p c q (\_ -> ()) 
    where 
      p =      (V "x" `Equal` V "a") 
        `bAnd` (V "y" `Equal` V "b")                -- { x = a && y = b } 
      c =      IAssign "x" (Plus  (V "x") (V "y"))  --     x := x + y
        `ISeq` IAssign "y" (Minus (V "x") (V "y"))  --     y := x - y
        `ISeq` IAssign "x" (Minus (V "x") (V "y"))  --     x := x - y
      q =      (V "x" `Equal` V "b")                -- { x = a && y = b } 
        `bAnd` (V "y" `Equal` V "a") 
  
  
  -------------------------------------------------------------------------------
  -- | Example 4: Reduce to Zero  
  -------------------------------------------------------------------------------
  
  bx4 :: () -> () 
  bx4 _ = verify p c q (\_ -> ()) 
    where 
      p = tt                                      -- { true } 
      c = IWhile i (Not (Equal (V "x") (N 0)))    --   WHILE not (x == 0) DO: 
            (IAssign "x" (Minus (V "x") (N 1)))   --     x := x - 1
      q = (V "x" `Equal` N 0)                     -- { x = 0 } 
      i = tt 
  
  
  
  
  