-- Copyright 2020-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
-- http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.
{-# LANGUAGE CPP #-}
{-# LANGUAGE NegativeLiterals #-}
{-# LANGUAGE TypeOperators #-}
module DoubleNegation where
-- HLint doesn't parse the thing we're trying to test here, so shut it up.
#if !defined(__HLINT__)
import Data.Fin.Int (Fin)
import Data.Word (Word8)
import Data.Type.Equality ((:~:)(Refl))
import Data.SInt (SInt)
-- Turns out you can have both syntactic negation and a negative literal in the
-- same pattern/expression. We should not have a bug when doing that.
x0 :: Int -> String
x0 x = case x of
-1 -> "-1"
- -2 -> "2...?"
_ -> "_"
-- Make sure we in fact get proof for +2 out of matching on @- -2@.
x1 :: SInt n -> Maybe (n :~: 2)
x1 x = case x of
- -2 -> Just Refl
_ -> Nothing
x2 :: Word8
x2 = - -8
x3 :: Fin 5
x3 = - -4
x4 :: SInt 2 -> SInt 2
x4 x = case x of
- -2 -> x
_ -> x
#endif