search

isovector / haskell-language-server

Integration point for ghcide and haskell-ide-engine. One IDE to rule them all.
Apache License 2.0
0 stars 2 forks source link

abominable, pestilentenial CPS #40

Closed isovector closed 3 years ago

isovector commented 3 years ago 

quickspec_laws :: [(String, Property)]
quickspec_laws =
  [ ( "commit t empty = t"
    , property $
        \ (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit t empty :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= t)
  , ( "commit empty t = t"
    , property $
        \ (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit empty t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= t)
  , ( "throw err >> x = throw err"
    , property $
        \ (err :: Bool)
          (x :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (throw err >> x :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= throw err)
  , ( "commit (lift eff) t = lift eff"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (lift eff) t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= lift eff)
  , ( "put s >> empty = empty"
    , property $
        \ (s :: Word8) ->
            (put s >> empty :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= empty)
  , ( "commit (commit t t2) t3 = commit t (commit t2 t3)"
    , property $
        \ (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t3 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (commit t t2) t3 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit t (commit t2 t3))
  , ( "commit (throw err) (throw err2) = throw err2"
    , property $
        \ (err :: Bool) (err2 :: Bool) ->
            (commit (throw err) (throw err2) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= throw err2)
  , ( "commit (throw err) (lift eff) = lift eff"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (err :: Bool) ->
            (commit (throw err) (lift eff) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= lift eff)
  , ( "put s >> throw err = throw err"
    , property $
        \ (err :: Bool) (s :: Word8) ->
            (put s >> throw err :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= throw err)
  , ( "commit (throw err) t >> t2 = commit (throw err) (t >> t2)"
    , property $
        \ (err :: Bool)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (throw err) t >> t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (throw err) (t >> t2))
  , ( "(lift eff >> t) <|> t2 = lift eff >> (t <|> t2)"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            ((lift eff >> t) <|> t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= lift eff >> (t <|> t2))
  , ( "commit (t <|> lift eff) t2 = commit t t2 <|> lift eff"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (t <|> lift eff) t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit t t2 <|> lift eff)
  , ( "commit (lift eff <|> t) t2 = lift eff <|> commit t t2"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (lift eff <|> t) t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= lift eff <|> commit t t2)
  , ( "commit (lift eff >> t) t2 = lift eff >> commit t t2"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (lift eff >> t) t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= lift eff >> commit t t2)
  , ( "commit t t2 <|> commit t3 t2 = commit (t <|> t3) t2"
    , property $
        \ (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t3 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit t t2 <|> commit t3 t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (t <|> t3) t2)
  , ( "(throw err <|> throw err2) >> x = (throw err <|> throw err2) >> y"
    , property $
        \ (err :: Bool)
          (err2 :: Bool)
          (x :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (y :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            ((throw err <|> throw err2) >> x :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= (throw err <|> throw err2) >> y)
  , ( "commit t (throw err) >> throw err = commit (t >> empty) (throw err)"
    , property $
        \ (err :: Bool)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit t (throw err) >> throw err :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (t >> empty) (throw err))
  , ( "commit (throw err) t >> throw err = commit (throw err) (t >> empty)"
    , property $
        \ (err :: Bool)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (throw err) t >> throw err :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (throw err) (t >> empty))
  , ( "commit (x >> empty) t >> t2 = commit (x >> empty) (t >> t2)"
    , property $
        \ (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (x :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (x >> empty) t >> t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (x >> empty) (t >> t2))
  , ( "(put s >> lift eff) >> x = lift eff >> (put s >> x)"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (s :: Word8)
          (x :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            ((put s >> lift eff) >> x :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= lift eff >> (put s >> x))
  , ( "commit (throw err) (t <|> throw err2) = commit (throw err) t <|> throw err2"
    , property $
        \ (err :: Bool)
          (err2 :: Bool)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (throw err) (t <|> throw err2) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (throw err) t <|> throw err2)
  , ( "throw err <|> commit (throw err2) t = commit (throw err2) (throw err <|> t)"
    , property $
        \ (err :: Bool)
          (err2 :: Bool)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (throw err <|> commit (throw err2) t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (throw err2) (throw err <|> t))
  , ( "commit (throw err) (commit t (throw err2)) = commit t (throw err2)"
    , property $
        \ (err :: Bool)
          (err2 :: Bool)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (throw err) (commit t (throw err2)) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit t (throw err2))
  , ( "commit (t >> throw err) (throw err2) = commit (t >> empty) (throw err2)"
    , property $
        \ (err :: Bool)
          (err2 :: Bool)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (t >> throw err) (throw err2) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (t >> empty) (throw err2))
  , ( "commit (t >> lift eff) (throw err) = commit t (throw err) >> lift eff"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (err :: Bool)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (t >> lift eff) (throw err) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit t (throw err) >> lift eff)
  , ( "commit (put s >> lift eff) t = put s >> lift eff"
    , property $
        \ (eff :: StateT (Maybe Word8) Identity Int)
          (s :: Word8)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit (put s >> lift eff) t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= put s >> lift eff)
  , ( "put s >> (put s2 >> x) = put s2 >> x"
    , property $
        \ (s :: Word8)
          (s2 :: Word8)
          (x :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (put s >> (put s2 >> x) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= put s2 >> x)
  , ( "put s >> (t <|> throw err) = (put s >> t) <|> throw err"
    , property $
        \ (err :: Bool)
          (s :: Word8)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (put s >> (t <|> throw err) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= (put s >> t) <|> throw err)
  , ( "put s >> (throw err <|> t) = throw err <|> (put s >> t)"
    , property $
        \ (err :: Bool)
          (s :: Word8)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (put s >> (throw err <|> t) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= throw err <|> (put s >> t))
  , ( "put s >> commit t (throw err) = commit (put s >> t) (throw err)"
    , property $
        \ (err :: Bool)
          (s :: Word8)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (put s >> commit t (throw err) :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (put s >> t) (throw err))
  , ( "put s >> commit (throw err) t = commit (throw err) (put s >> t)"
    , property $
        \ (err :: Bool)
          (s :: Word8)
          (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (put s >> commit (throw err) t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit (throw err) (put s >> t))
  , ( "commit t (t2 >> empty) >> empty = commit t t2 >> empty"
    , property $
        \ (t :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int)
          (t2 :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) ->
            (commit t (t2 >> empty) >> empty :: TacticT Judgement Term Bool Word8 (StateT (Maybe Word8) Identity) Int) =~= commit t t2 >> empty)
  ]