content: module WhyLH where
  
  {-@ LIQUID "--ple" @-}
  {-@ LIQUID "--exact-data-cons" @-}
  
  -- This test contains the examples of the blogpost at
  -- https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/
  --
  import Language.Haskell.Liquid.ProofCombinators (pleUnfold)
  import Prelude hiding (length, max)
  
  {-@
  
  data UExp
    = UVar Nat
    | ULam Ty UExp
    | UApp { uapp1 :: UExp, uapp2 :: UExp }
   @-}
  -- | Lambda expressions with types at the bindings.
  data UExp
    = UVar Int
    | ULam Ty UExp
    | UApp { uapp1 :: UExp, uapp2 :: UExp }
  
  -- | The types are the types of functions manipulating some opaque type @T@.
  data Ty = T | TyFun Ty Ty
    deriving Eq
  
  -- XXX: Using inline instead of reflect causes verification to fail
  {-@ reflect max @-}
  max :: Int -> Int -> Int
  max a b = pleUnfold (if a > b then a else b)
  
  -- XXX: using max causes verification to fail if not using
  -- --ple-with-undecided-guards. Arguably, PLE should unfold max
  -- since it is not doing pattern matching.
  {-@
  reflect freeVarBound
  freeVarBound :: UExp -> Int
  @-}
  -- | Compute the lowest upper-bound of de Bruijn indices appearing
  -- free in an expression.
  freeVarBound :: UExp -> Int
  freeVarBound (UVar v) = v + 1
  freeVarBound (ULam _ body) = max (freeVarBound body - 1) 0
  freeVarBound (UApp e1 e2) = max (freeVarBound e1) (freeVarBound e2)
  
  {-@
  type UExpN N = { e:UExp | freeVarBound e <= N }
  type ClosedUExp = UExpN 0
  @-}
  
  {-@ exp0 :: ClosedUExp @-}
  exp0 :: UExp
  exp0 = ULam T (UVar 0)
  
  {-@ exp1 :: UExpN 1 @-}
  exp1 :: UExp
  exp1 = UVar 0
  
  {-@ exp2 :: ClosedUExp @-}
  exp2 :: UExp
  exp2 = ULam T (ULam T (UVar 0))
  
  {-@ exp3 :: UExpN 1 @-}
  exp3 :: UExp
  exp3 = ULam T (ULam T (UVar 2))
  
  
  {-@ reflect elemAt @-}
  {-@ elemAt :: xs:[a] -> { i:Int | 0 <= i && i < length xs } -> a @-}
  elemAt :: [a] -> Int -> a
  elemAt (x:_) 0 = x
  elemAt (_:xs) i = elemAt xs (i - 1)
  
  {-@ reflect length @-}
  length :: [a] -> Int
  length [] = 0
  length (_:xs) = 1 + length xs
  
  {-@ reflect inferType @-}
  {-@ inferType :: ctx:[Ty] -> UExpN (length ctx) -> Maybe Ty @-}
  inferType :: [Ty] -> UExp -> Maybe Ty
  inferType ctx (UVar i) = Just (elemAt ctx i)
  inferType ctx (ULam t body) = case inferType (t:ctx) body of
    Just r -> Just (TyFun t r)
    Nothing -> Nothing
  inferType ctx (UApp e0 e1) =
    pleUnfold  -- needed by uappArgT to avoid breaking the verification
               -- in all of these cases
      (case inferType ctx e0 of
        Just (TyFun a r) -> case inferType ctx e1 of
          Just t -> if a == t then Just r else Nothing
          Nothing -> Nothing
        _ -> Nothing
      )
  
  {-@ type WellTypedExp CTX TY = { e:UExp | freeVarBound e <= length CTX && inferType CTX e == Just TY } @-}
  
  {-@ reflect cons @-}
  cons :: a -> [a] -> [a]
  cons = (:)
  
  {-@ exp4 :: WellTypedExp (cons T []) T @-}
  exp4 :: UExp
  exp4 = UVar 0
  
  {-@ exp5 :: WellTypedExp [] (TyFun T T) @-}
  exp5 :: UExp
  exp5 = ULam T (UVar 0)
  
  main :: IO ()
  main = print ()
  
  -- The following functions are an experiment on what LH can infer from
  -- the arguments of a data constructor. Given a well-typed application
  -- @UApp e0 e1@, can LH infer that @e0@ must have a function type and
  -- that the type of @e1@ must match the argument type of @e0@.
  
  {-@ uappArgT :: ctx:[Ty] -> e : { e:UExp | isUApp e && isJustTy (inferType ctx e) } -> { funTyM (inferType ctx (uapp2 e)) (inferType ctx e) == inferType ctx (uapp1 e) } @-}
  uappArgT :: [Ty] -> UExp -> ()
  uappArgT _ _ = ()
  
  {-@ inline isUApp @-}
  isUApp :: UExp -> Bool
  isUApp (UApp _ _) = True
  isUApp _ = False
  
  -- Either inline or both reflect and pleUnfold are needed by `uappArgT`.
  {-@ inline isJustTy @-}
  isJustTy :: Maybe a -> Bool
  isJustTy (Just _) = True
  isJustTy _ = False
  
  {-@ inline funTyM @-}
  funTyM :: Maybe Ty -> Maybe Ty -> Maybe Ty
  funTyM (Just a) (Just b) = Just (TyFun a b)
  funTyM _ _ = Nothing
  