content: module T1874 where
  
  {-@ LIQUID "--exact-data-cons" @-}
  {-@ LIQUID "--reflection"      @-}
  {-@ LIQUID "--ple"             @-}
  
  import Language.Haskell.Liquid.ProofCombinators
  
  data Ty = TInt | TFun Ty Ty
  
  {-@
  type FunTy = { t : Ty | isFunTy t }
  data Ty = TInt | TFun Ty Ty
  @-}
  
  {-@ measure isFunTy @-}
  isFunTy :: Ty -> Bool
  isFunTy (TFun _ _) = True
  isFunTy _ = False
  
  {- reflect funResTy @-}
  {-@ measure funResTy @-}
  {-@ funResTy :: FunTy -> Ty @-}
  funResTy :: Ty -> Ty
  funResTy (TFun _ b) = b
  
  {-@ measure funArgTy @-}
  {-@ funArgTy :: FunTy -> Ty @-}
  funArgTy :: Ty -> Ty
  funArgTy (TFun a _) = a
  
  {-@
  type FunExp = { e : Exp | isFunTy (exprType e) }
  type ExpT T = { e : Exp | T = exprType e }
  data Exp
    = Var Ty Int
    | Lam Ty Exp
    | App (e1 :: FunExp) (ExpT (funArgTy (exprType e1)))
  @-}
  
  data Exp
    = Var Ty Int
    | Lam Ty Exp
    | App Exp Exp
  
  {-@ measure exprType @-}
  exprType :: Exp -> Ty
  exprType (Var ty _) = ty
  exprType (Lam ty e) = TFun ty (exprType e)
  exprType (App e1 _) = funResTy (exprType e1)
  
  
  {-@ typeAppLam_prop :: ty:Ty -> e0:Exp -> e1:Exp -> { exprType (App (Lam ty e0) e1) = exprType e0 } @-}
  typeAppLam_prop :: Ty -> Exp -> Exp -> Proof
  typeAppLam_prop _ _ _ = trivial *** QED
  
  {-@ step :: e:Exp -> Maybe (ExpT (exprType e)) @-}
  step :: Exp -> Maybe Exp
  step e0 = case e0 of
      Var{} -> Nothing
      Lam{} -> Nothing
      App e1 e2 -> case step e1 of
        Just e1' -> Just (App e1' e2)
        Nothing -> case step e2 of
          Just e2' -> Just (App e1 e2')
          Nothing -> case e1 of
            Lam ty e11 ->
                Just e11 -- ? typeAppLam_prop ty e11 e2
            _ -> Nothing
  