-- 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.
module FinPatterns where
import Data.Fin.Int (Fin)
-- Easy: we know @n@ statically, and don't need the provided constraints.
simpleMatch :: Fin 4 -> String
simpleMatch x = case x of
0 -> "0"
1 -> "1"
_ -> "2 or 3"
-- Harder: we have to compare against 0/1 without knowing it's in range.
polyMatch :: Fin n -> String
polyMatch x = case x of
0 -> "0"
1 -> "1"
_ -> "unknown"
-- Even harder: comparing against 2 has to prove that 2 is in range.
usingEvidence :: Fin n -> Maybe (Fin n)
usingEvidence x = case x of
2 -> Just 2
_ -> Nothing