content: {-@ LIQUID "--reflection"  @-}
  {-@ LIQUID "--ple"         @-}
  
  module Data.Lattice where
  
  import Liquid.ProofCombinators 
  
  class Lattice l where
      canFlowTo :: l -> l -> Bool
      meet :: l -> l -> l
      join :: l -> l -> l
      bot  :: l 
  
      {-@ lawFlowReflexivity :: l : l -> {canFlowTo l l} @-}
      lawFlowReflexivity :: l -> ()
      {-@ lawFlowAntisymmetry :: a : l -> {b : l | canFlowTo a b && canFlowTo b a} -> {a == b} @-}
      lawFlowAntisymmetry :: l -> l -> ()
      {-@ lawFlowTransitivity :: a:l -> b:l-> c:l -> {(canFlowTo a b && canFlowTo b c) => canFlowTo a c} @-}
      lawFlowTransitivity :: l -> l -> l -> ()
  
      {-@ lawMeet :: x : l -> y : l -> w : l -> {(canFlowTo (meet x y) x && canFlowTo (meet x y) y && ((canFlowTo w x && canFlowTo w y) => canFlowTo w (meet x y)))} @-}
      lawMeet :: l -> l -> l -> ()
      {-@ lawJoin :: x : l -> y : l -> w : l -> {(canFlowTo x (join x y) && canFlowTo y (join x y) && ((canFlowTo x w && canFlowTo y w) => canFlowTo (join x y) w))} @-}
      lawJoin :: l -> l -> l -> ()
      {-@ lawBot :: x : l -> { canFlowTo bot x } @-}
      lawBot  :: l -> ()
  
  {-@ joinCanFlowTo 
   :: Lattice l
   => l1 : l
   -> l2 : l
   -> l3 : l
   -> {canFlowTo l1 l3 && canFlowTo l2 l3 <=> canFlowTo (join l1 l2) l3}
   @-}
  joinCanFlowTo :: Lattice l => l -> l -> l -> ()
  joinCanFlowTo l1 l2 l3 = lawJoin l1 l2 l3 &&& unjoinCanFlowTo l1 l2 l3 
  
  
  {-@ unjoinCanFlowTo 
   :: Lattice l
   => l1:l -> l2:l -> l3:l 
   -> {canFlowTo (join l1 l2) l3 => (canFlowTo l1 l3 && canFlowTo l2 l3)}
   @-}
  unjoinCanFlowTo :: Lattice l => l -> l -> l -> ()
  unjoinCanFlowTo l1 l2 l3
    =     lawJoin l1 l2 l3  
      &&& lawFlowTransitivity l1 (l1 `join` l2) l3
      &&& lawFlowTransitivity l2 (l1 `join` l2) l3
  
  {-@ notJoinCanFlowTo 
   :: Lattice l 
   => a : l 
   -> b : l 
   -> c : {l | not (canFlowTo a c)}
   -> {not (canFlowTo (join a b) c)}
   @-}
  notJoinCanFlowTo :: Lattice l => l -> l -> l -> ()
  notJoinCanFlowTo l1 l2 l3 = unjoinCanFlowTo l1 l2 l3
  
  {-@ meetCanFlowTo 
   :: Lattice l
   => l1 : l
   -> l2 : l
   -> l3 : l
   -> {canFlowTo l1 l2 && canFlowTo l1 l3 <=> canFlowTo l1 (meet l2 l3)}
   @-}
  meetCanFlowTo :: Lattice l => l -> l -> l -> ()
  meetCanFlowTo l1 l2 l3 = lawMeet l2 l3 l1 &&& unmeetCanFlowTo l1 l2 l3 
  
  
  {-@ unmeetCanFlowTo 
   :: Lattice l
   => l1:l -> l2:l -> l3:l 
   -> {canFlowTo l1 (meet l2 l3) => (canFlowTo l1 l2 && canFlowTo l1 l3)}
   @-}
  unmeetCanFlowTo :: Lattice l => l -> l -> l -> ()
  unmeetCanFlowTo l1 l2 l3
    =     lawMeet l2 l3 l1
      &&& lawFlowTransitivity l1 (l2 `meet` l3) l2
      &&& lawFlowTransitivity l1 (l2 `meet` l3) l3
  
  {-@ notMeetCanFlowTo 
   :: Lattice l 
   => a : l 
   -> b : l 
   -> c : {l | not (canFlowTo a c)}
   -> {not (canFlowTo a (meet b c))}
   @-}
  notMeetCanFlowTo :: Lattice l => l -> l -> l -> ()
  notMeetCanFlowTo l1 l2 l3 = unmeetCanFlowTo l1 l2 l3
  
  {-@ notCanFlowTo 
   :: Lattice l 
   => a : l 
   -> b : l 
   -> c : l
   -> {(not (canFlowTo b a) && canFlowTo b c) => not (canFlowTo c a)}
   @-}
  notCanFlowTo :: Lattice l => l -> l -> l -> ()
  notCanFlowTo a b c = lawFlowTransitivity b c a
  
  {-@ unmeetCanFlowToItself :: Lattice l => a:l -> b:l 
    -> { canFlowTo (meet a b) a && canFlowTo (meet a b) b } @-}
  unmeetCanFlowToItself :: Lattice l => l -> l -> ()
  unmeetCanFlowToItself x y = lawMeet x y x
  
  {-@ unjoinCanFlowToItself :: Lattice l => a:l -> b:l 
    -> { canFlowTo a (join a b) && canFlowTo b (join a b) } @-}
  unjoinCanFlowToItself :: Lattice l => l -> l -> ()
  unjoinCanFlowToItself x y = lawJoin x y x
   
  