packages feed

sbv-14.0: SBVTestSuite/TestSuite/CompileTests/SCase/SCase53.stderr

SCase53.hs:(12,14)-(20,8): Splicing expression
    ghc-internal:GHC.Internal.TH.Quote.quoteExp
      sCase
      " e of\n\
      \               Add (Num i) b | i .> 0   -> i + t b\n\
      \                              | i .> -5  -> t b\n\
      \               Add a b                   -> t a + t b\n\
      \               Zero                      -> 0\n\
      \               Num i                     -> i\n\
      \               Var _                     -> 1\n\
      \               Let _ _ _                 -> 3\n\
      \      "
  ======>
    ite
      ((.&&)
         (isAdd e)
         ((\ _ b
             -> const
                  ((.&&)
                     (isNum (getAdd_1 e)) (let i = getNum_1 (getAdd_1 e) in i .> 0))
                  b)
            (getAdd_1 e) (getAdd_2 e)))
      ((\ _ b -> let i = getNum_1 (getAdd_1 e) in i + t b)
         (getAdd_1 e) (getAdd_2 e))
      (ite
         ((.&&)
            (isAdd e)
            ((\ _ b
                -> const
                     ((.&&)
                        (isNum (getAdd_1 e))
                        (let i = getNum_1 (getAdd_1 e) in i .> negate 5))
                     b)
               (getAdd_1 e) (getAdd_2 e)))
         ((\ _ b -> t b) (getAdd_1 e) (getAdd_2 e))
         (ite
            (isAdd e) ((\ a b -> (t a) + t b) (getAdd_1 e) (getAdd_2 e))
            (ite
               (isZero e) 0
               (ite
                  (isNum e) ((\ i -> i) (getNum_1 e))
                  (ite
                     (isVar e) ((\ _ -> 1) (getVar_1 e))
                     ((\ _ _ _ -> 3) (getLet_1 e) (getLet_2 e) (getLet_3 e)))))))