-- 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 ScopedTypeVariables #-}
module SIntPatterns where
import Data.Fin.Int (Fin)
import Data.SInt (SInt)
import GHC.TypeNats (KnownNat)
import TestUtils (showTyped)
-- Easy: just match on the right value.
x0 :: SInt 2 -> String
x0 x = case x of
2 -> "2"
_ -> "inconceivable"
-- We can match on multiple values for unknown SNats.
x1 :: SInt n -> String
x1 x = case x of
0 -> "0"
1 -> "1"
_ -> "other"
-- When matching literals, we get an equality proof. Inside each arm we know
-- @n@ statically and GHC will natively solve KnownNat constraints for it.
x2 :: forall n. SInt n -> String
x2 x = case x of
0 -> "uninhabited"
1 -> f 0
4 -> f 2
16 -> f 7
_ -> "whatever"
where
f :: KnownNat n => Fin n -> String
f = showTyped