-- 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 ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module PolyLiterals where
import DependentLiterals (IntLiteral, HasBasicLiterals)
import Data.Vec.Short (Vec, (!))
import qualified Data.Vec.Short as V
import GHC.TypeNats (CmpNat)
import Data.Fin.Int (Fin, (+!))
-- Will be exported from Fin, later.
type m < n = CmpNat m n ~ 'LT
xx0 :: Int
xx0 = f (V.fromList [0, 2, 3, 7] :: Vec 4 Int)
where
f v = v ! 2
xx1 :: Fin 4
xx1 = f (0 :: Fin 4)
where
f x = 1 +! x
x0 :: IntLiteral 4 a => a
x0 = 4
x1 :: HasBasicLiterals a => a
x1 = 4
x2 :: HasBasicLiterals a => a
x2 = x0
x3 :: Fin 4
x3 = x
where
x = 3
theFin :: Fin n -> Fin n
theFin = id
x4 :: Fin 4
x4 = x
where
x = theFin 3
x5 :: Fin 4
x5 = x
where
x :: IntLiteral 3 a => a
x = 3
x6 :: (3 < n) => Fin n
x6 = x
where
x = 3
x7 :: (3 < n) => Fin n
x7 = x
where
x = theFin 3