content: {-@ LIQUID "--reflection"  @-}
  {-@ LIQUID "--ple"         @-}
  {-@ LIQUID "--short-names" @-}
  
  {-@ infixr ++  @-}  -- TODO: Silly to have to rewrite this annotation!
  
  {-# LANGUAGE GADTs #-}
  
  module BigStep where
  
  import           Prelude hiding ((++)) 
  import           ProofCombinators
  import qualified State as S
  import           Expressions hiding (And)
  import           Imp 
  
  {- 
    BStep c s1 s2 
  
    ------------------[BSkip]
      BStep Skip s s
  
  
      s' = set x (aval a s) s
    ----------------------------------[BAssign]
      BStep (x := a) s s'
  
  
      BStep c1 s smid    BStep c2 smid s'
    ----------------------------------------[BSeq]
      BStep (c1; c2) s s' 
  
  
      bval b s1 = TRUE      BStep c1 s s'
    ----------------------------------------
      BStep (If b c1 c2) s s' 
  
      bval b s = FALSE     BStep c2 s s'
    -------------------------------
      BStep (If b c1 c2) s s' 
  
      WHILE 
   -}
  
  --------------------------------------------------------------------------------
  -- | Big-step Semantics 
  --------------------------------------------------------------------------------
  
  data BStepP where
    BStep :: Com -> State -> State -> BStepP 
  
  data BStep where 
    BSkip   :: State -> BStep 
    BAssign :: Vname -> AExp -> State -> BStep 
    BSeq    :: Com   -> Com  -> State  -> State -> State -> BStep -> BStep -> BStep 
    BIfT    :: BExp  -> Com  -> Com   -> State -> State -> BStep -> BStep  
    BIfF    :: BExp  -> Com  -> Com   -> State -> State -> BStep -> BStep
    BWhileF :: BExp  -> Com  -> State -> BStep 
    BWhileT :: BExp  -> Com  -> State -> State -> State -> BStep -> BStep -> BStep 
  
  {-@ data BStep  where 
          BSkip   :: s:State 
                  -> Prop (BStep Skip s s)
          BAssign :: x:Vname -> a:AExp -> s:State 
                  -> Prop (BStep (Assign x a) s (asgn x a s)) 
          BSeq    :: c1:Com -> c2:Com -> s1:State -> s2:State -> s3:State 
                  -> Prop (BStep c1 s1 s2) -> Prop (BStep c2 s2 s3) 
                  -> Prop (BStep (Seq c1 c2) s1 s3)
          BIfT    :: b:BExp -> c1:Com -> c2:Com -> s:{State | bval b s} -> s1:State
                  -> Prop (BStep c1 s s1) -> Prop (BStep (If b c1 c2) s s1)
          BIfF    :: b:BExp -> c1:Com -> c2:Com -> s:{State | not (bval b s)} -> s2:State
                  -> Prop (BStep c2 s s2) -> Prop (BStep (If b c1 c2) s s2)
          BWhileF :: b:BExp -> c:Com -> s:{State | not (bval b s)} 
                  -> Prop (BStep (While b c) s s)
          BWhileT :: b:BExp -> c:Com -> s1:{State | bval b s1} -> s1':State -> s2:State
                  -> Prop (BStep c s1 s1') -> Prop (BStep (While b c) s1' s2)
                  -> Prop (BStep (While b c) s1 s2)
    @-}  
  
  
  {-@ reflect cmd_1 @-}
  cmd_1 = "x" <~ N 5
  
  {-@ reflect cmd_2 @-}
  cmd_2 = "y" <~ (V "x")
  
  {-@ reflect cmd_1_2 @-}
  cmd_1_2 = cmd_1 @@ cmd_2
  
  {-@ reflect prop_set @-}
  prop_set cmd x v s = BStep cmd s (S.set s x v)
  
  {-@ step_1 :: s:State -> Prop (prop_set cmd_1 {"x"} 5 s)  @-}
  step_1 s =  BAssign "x" (N 5) s
  
  {-@ step_2 :: s:{State | S.get s "x" == 5} -> Prop (prop_set cmd_2 {"y"} 5 s) @-}
  step_2 s = BAssign "y" (V "x") s
  
  {-@ step_1_2 :: s:State -> Prop (BStep cmd_1_2 s (S.set (S.set s {"x"} 5) {"y"} 5)) @-}
  step_1_2 s = BSeq cmd_1 cmd_2 s s1 s2 (step_1 s) (step_2 s1)
    where
      s1     = S.set s  "x" 5
      s2     = S.set s1 "y" 5
  
  
  
  -------------------------------------------------------------------------------
  -- | We say `Sim c1 c2` or `c1` is simulated by `c2` if 
  --   the transitions of `c1` are contained within those of `c2`
  -------------------------------------------------------------------------------
  
  {-@ type Sim C1 C2 = s:State -> t:State -> Prop (BStep C1 s t) -> Prop (BStep C2 s t) @-}
  type SimT = State -> State -> BStep -> BStep 
  
  
  ---------------------------------------------------------------------------------
  -- | IMP is Deterministic
  ---------------------------------------------------------------------------------
  
  {- 
  {-@ thm_bigstep_det 
        :: s:_ -> t1:_ -> t2:_ -> c:_
        -> Prop (BStep c s t1) 
        -> Prop (BStep c s t2) 
        -> { t1 == t2 }
    @-}
  thm_bigstep_det :: State -> State -> State -> Com -> BStep -> BStep -> Proof
  
  
  
  
  {- -}
  thm_bigstep_det s t t' Skip         (BSkip {})   (BSkip {})
      = ()
    
  thm_bigstep_det s t t' (Assign x a) (BAssign {}) (BAssign {})
      = ()
    
  thm_bigstep_det s t t' (Seq c1 c2)  (BSeq _ _ _ s1 s2 s_s1 s1_s2) (BSeq _ _ _ s1' s2' s_s1' s1_s2')
      = thm_bigstep_det s1_eq_s1' s2 s2' c2 s1_s2 s1_s2'        
      where s1_eq_s1' = s1 ? thm_bigstep_det s  s1 s1' c1 s_s1  s_s1'
    
  thm_bigstep_det s t t' (If b c1 c2) (BIfT _ _ _ _ _t c1_s_t) (BIfT _ _ _ _ _t' c1_s_t')
      = thm_bigstep_det s t t' c1 c1_s_t c1_s_t'
    
  thm_bigstep_det s t t' (If b c1 c2) (BIfF _ _ _ _ _t c2_s_t) (BIfF _ _ _ _ _t' c2_s_t')
      = thm_bigstep_det s t t' c2 c2_s_t c2_s_t'
    
  thm_bigstep_det s t t' (While b c)  (BWhileF {}) (BWhileF {})
      = ()
    
  thm_bigstep_det s t t' (While b c)  (BWhileT _ _ _ s1 _ s_s1 s1_t) (BWhileT _ _ _ s1' _ s_s1' s1_t')
      = thm_bigstep_det s1_eq_s1' t t' (While b c) s1_t s1_t'   
      where s1_eq_s1' = s1 ? thm_bigstep_det s s1 s1' c s_s1 s_s1'
  
  thm_bigstep_det _ _ _ _  _ _ 
      = impossible "no really" 
    
  -}
  