quox/lib/Quox/Var.idr

302 lines
8.4 KiB
Idris
Raw Normal View History

2023-09-20 15:56:59 -04:00
module Quox.Var
2021-07-20 16:05:19 -04:00
2023-05-01 21:06:25 -04:00
import public Quox.Loc
import public Quox.Name
import Quox.OPE
2021-07-20 16:05:19 -04:00
import Data.Nat
import Data.List
import Data.Vect
2023-01-09 17:43:23 -05:00
import public Quox.Decidable
2022-02-26 20:17:42 -05:00
import Data.Bool.Decidable
2023-01-09 17:43:23 -05:00
import Data.DPair
2021-07-20 16:05:19 -04:00
%default total
public export
data Var : Nat -> Type where
VZ : Var (S n)
VS : Var n -> Var (S n)
%name Var i, j
%builtin Natural Var
public export
(.nat) : Var n -> Nat
(VZ).nat = 0
(VS i).nat = S i.nat
%transform "Var.(.nat)" Var.(.nat) i = believe_me i
2022-02-26 19:47:55 -05:00
public export %inline Cast (Var n) Nat where cast = (.nat)
public export %inline Cast (Var n) Integer where cast = cast . cast {to = Nat}
2021-07-20 16:05:19 -04:00
2022-02-26 19:47:55 -05:00
export %inline Eq (Var n) where i == j = i.nat == j.nat
export %inline Ord (Var n) where compare i j = compare i.nat j.nat
export %inline Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat
2021-07-20 16:05:19 -04:00
2022-02-26 20:17:42 -05:00
public export %inline Injective VS where injective Refl = Refl
2023-01-12 10:03:09 -05:00
export Uninhabited (Var 0) where uninhabited _ impossible
export Uninhabited (VZ = VS i) where uninhabited _ impossible
export Uninhabited (VS i = VZ) where uninhabited _ impossible
2021-07-20 16:05:19 -04:00
2023-05-01 21:06:25 -04:00
public export
data Eqv : Var m -> Var n -> Type where
EZ : VZ `Eqv` VZ
ES : i `Eqv` j -> VS i `Eqv` VS j
%name Var.Eqv e
export
decEqv : Dec2 Eqv
decEqv VZ VZ = Yes EZ
decEqv VZ (VS i) = No $ \case _ impossible
decEqv (VS i) VZ = No $ \case _ impossible
decEqv (VS i) (VS j) =
case decEqv i j of
Yes y => Yes $ ES y
No n => No $ \(ES y) => n y
private
lookupS : Nat -> SnocList a -> Maybe a
lookupS _ [<] = Nothing
lookupS Z (sx :< x) = Just x
lookupS (S i) (sx :< x) = lookupS i sx
2021-07-20 16:05:19 -04:00
public export
fromNatWith : (i : Nat) -> (0 p : i `LT` n) -> Var n
fromNatWith Z (LTESucc _) = VZ
fromNatWith (S i) (LTESucc p) = VS $ fromNatWith i p
%transform "Var.fromNatWith" fromNatWith i p = believe_me i
public export %inline
V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
2023-03-10 15:52:29 -05:00
V i = fromNatWith i p
2021-07-20 16:05:19 -04:00
export %inline
2021-07-20 16:05:19 -04:00
tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
tryFromNat n i =
case i `isLT` n of
Yes p => pure $ fromNatWith i p
No _ => empty
export
0 toNatLT : (i : Var n) -> i.nat `LT` n
toNatLT VZ = LTESucc LTEZero
toNatLT (VS i) = LTESucc $ toNatLT i
2022-02-26 20:17:42 -05:00
public export
toNatInj : {i, j : Var n} -> i.nat = j.nat -> i = j
2021-07-20 16:05:19 -04:00
toNatInj {i = VZ} {j = VZ} Refl = Refl
toNatInj {i = VZ} {j = (VS i)} Refl impossible
toNatInj {i = (VS i)} {j = VZ} Refl impossible
2022-02-26 20:17:42 -05:00
toNatInj {i = (VS i)} {j = (VS j)} prf = cong VS $ toNatInj $ injective prf
public export %inline Injective (.nat) where injective = toNatInj
2021-07-20 16:05:19 -04:00
export
0 fromToNat : (i : Var n) -> (p : i.nat `LT` n) -> fromNatWith i.nat p = i
fromToNat VZ (LTESucc p) = Refl
fromToNat (VS i) (LTESucc p) = rewrite fromToNat i p in Refl
export
0 toFromNat : (i : Nat) -> (p : i `LT` n) -> (fromNatWith i p).nat = i
toFromNat 0 (LTESucc x) = Refl
toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
-- not using %transform like other things because weakSpec requires the proof
-- to be relevant. but since only `LTESucc` is ever possible that seems
2022-02-26 19:48:37 -05:00
-- to be an instance of <https://github.com/idris-lang/Idris2/issues/1259>?
2021-07-20 16:05:19 -04:00
export
weak : (0 p : m `LTE` n) -> Var m -> Var n
weak p i = fromNatWith i.nat $ transitive (toNatLT i) p
2021-07-20 16:05:19 -04:00
public export
0 weakSpec : m `LTE` n -> Var m -> Var n
weakSpec LTEZero _ impossible
weakSpec (LTESucc p) VZ = VZ
weakSpec (LTESucc p) (VS i) = VS $ weakSpec p i
export
0 weakSpecCorrect : (p : m `LTE` n) -> (i : Var m) -> (weakSpec p i).nat = i.nat
weakSpecCorrect LTEZero _ impossible
weakSpecCorrect (LTESucc x) VZ = Refl
weakSpecCorrect (LTESucc x) (VS i) = cong S $ weakSpecCorrect x i
export
0 weakCorrect : (p : m `LTE` n) -> (i : Var m) -> (weak p i).nat = i.nat
2022-02-26 19:28:19 -05:00
weakCorrect LTEZero _ impossible
2021-07-20 16:05:19 -04:00
weakCorrect (LTESucc p) VZ = Refl
weakCorrect (LTESucc p) (VS i) = cong S $ weakCorrect p i
export
0 weakIsSpec : (p : m `LTE` n) -> (i : Var m) -> weak p i = weakSpec p i
weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
public export
2023-05-01 21:06:25 -04:00
interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
2021-07-20 16:05:19 -04:00
2023-05-01 21:06:25 -04:00
public export FromVar Var where fromVarLoc x _ = x
2021-12-23 13:01:24 -05:00
export
tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
(n : Nat) -> Vect n (tm n)
tabulateV f 0 = []
tabulateV f (S n) = f VZ :: tabulateV (f . VS) n
export
allVars : (n : Nat) -> Vect n (Var n)
allVars n = tabulateV id n
2021-12-23 13:01:24 -05:00
public export
2023-01-09 17:43:23 -05:00
data LT : Rel (Var n) where
2021-12-23 13:01:24 -05:00
LTZ : VZ `LT` VS i
LTS : i `LT` j -> VS i `LT` VS j
%builtin Natural Var.LT
%name Var.LT lt
public export %inline
2023-01-09 17:43:23 -05:00
GT : Rel (Var n)
2021-12-23 13:01:24 -05:00
i `GT` j = j `LT` i
export
Transitive (Var n) LT where
transitive LTZ (LTS _) = LTZ
transitive (LTS p) (LTS q) = LTS $ transitive p q
2021-12-23 13:01:24 -05:00
export Uninhabited (i `Var.LT` i) where uninhabited (LTS p) = uninhabited p
export Uninhabited (VS i `LT` VZ) where uninhabited _ impossible
2023-01-12 10:03:09 -05:00
export
ltReflect : LT {n} `Reflects2` (<)
ltReflect VZ VZ = RFalse absurd
ltReflect VZ (VS j) = RTrue LTZ
ltReflect (VS i) VZ = RFalse absurd
ltReflect (VS i) (VS j) with (ltReflect i j) | (i < j)
_ | RTrue yes | True = RTrue $ LTS yes
_ | RFalse no | False = RFalse $ \case LTS p => no p
2021-12-23 13:01:24 -05:00
export
2023-01-09 17:43:23 -05:00
isLT : Dec2 Var.LT
2023-01-12 10:03:09 -05:00
isLT i j = reflectToDec $ ltReflect i j
2021-12-23 13:01:24 -05:00
public export
data Compare : (i, j : Var n) -> Ordering -> Type where
IsLT : (lt : i `LT` j) -> Compare i j LT
IsEQ : Compare i i EQ
IsGT : (gt : i `GT` j) -> Compare i j GT
2021-12-23 13:01:24 -05:00
%name Compare cmp
export
compareS : Compare i j o -> Compare (VS i) (VS j) o
2021-12-23 13:01:24 -05:00
compareS (IsLT lt) = IsLT (LTS lt)
compareS IsEQ = IsEQ
compareS (IsGT gt) = IsGT (LTS gt)
export
compareP : (i, j : Var n) -> Compare i j (compare i j)
2021-12-23 13:01:24 -05:00
compareP VZ VZ = IsEQ
compareP VZ (VS j) = IsLT LTZ
compareP (VS i) VZ = IsGT LTZ
compareP (VS i) (VS j) = compareS $ compareP i j
2023-01-12 10:03:09 -05:00
export
0 compare2 : Compare {n} i j o -> o = compare i j
compare2 (IsLT LTZ) = Refl
compare2 (IsLT (LTS lt)) = compare2 (IsLT lt)
compare2 IsEQ = sym $ compareNatDiag i.nat
compare2 (IsGT LTZ) = Refl
compare2 (IsGT (LTS gt)) = compare2 $ IsGT gt
compare2 _ {n = 0} = absurd i
2022-02-26 19:50:01 -05:00
export
0 compareSelf : Compare i i o -> o = EQ
2023-01-12 10:03:09 -05:00
compareSelf p = rewrite compare2 p in compareNatDiag i.nat
2022-02-26 19:50:01 -05:00
export
0 comparePSelf : (i : Var n) -> Compare i i EQ
comparePSelf i = rewrite sym $ compareNatDiag i.nat in compareP i i
2022-02-26 19:50:01 -05:00
2021-12-23 13:01:24 -05:00
public export
2023-01-09 17:43:23 -05:00
data LTE : Rel (Var n) where
2021-12-23 13:01:24 -05:00
LTEZ : VZ `LTE` j
LTES : i `LTE` j -> VS i `LTE` VS j
export
Reflexive (Var n) LTE where
reflexive {x = VZ} = LTEZ
reflexive {x = VS i} = LTES reflexive
2021-12-23 13:01:24 -05:00
export
Transitive (Var n) LTE where
transitive LTEZ q = LTEZ
transitive (LTES p) (LTES q) = LTES $ transitive p q
2021-12-23 13:01:24 -05:00
export
Antisymmetric (Var n) LTE where
antisymmetric LTEZ LTEZ = Refl
antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q
2021-12-23 13:01:24 -05:00
export
2022-02-26 19:49:42 -05:00
splitLTE : {j : Var n} -> i `LTE` j -> Either (i = j) (i `LT` j)
2021-12-23 13:01:24 -05:00
splitLTE {j = VZ} LTEZ = Left Refl
splitLTE {j = VS _} LTEZ = Right LTZ
splitLTE (LTES p) with (splitLTE p)
2023-01-12 10:03:09 -05:00
_ | Left eq = Left $ cong VS eq
_ | Right lt = Right $ LTS lt
2022-02-26 20:17:42 -05:00
2023-01-12 10:03:09 -05:00
export Uninhabited (VS i `LTE` VZ) where uninhabited _ impossible
2022-02-26 20:17:42 -05:00
2023-01-12 10:03:09 -05:00
export
lteReflect : (i, j : Var n) -> (LTE i j) `Reflects` (i <= j)
lteReflect VZ VZ = RTrue LTEZ
lteReflect VZ (VS j) = RTrue LTEZ
lteReflect (VS i) VZ = RFalse absurd
lteReflect (VS i) (VS j) with (lteReflect i j) | (i <= j)
_ | RTrue yes | True = RTrue (LTES yes)
_ | RFalse no | False = RFalse $ \case LTES lte => no lte
2022-02-26 20:17:42 -05:00
public export
eqReflect : (i, j : Var n) -> (i = j) `Reflects` (i == j)
eqReflect VZ VZ = RTrue Refl
eqReflect VZ (VS i) = RFalse absurd
eqReflect (VS i) VZ = RFalse absurd
2023-01-09 17:45:21 -05:00
eqReflect (VS i) (VS j) with (eqReflect i j) | (i == j)
_ | RTrue yes | True = RTrue $ cong VS yes
_ | RFalse no | False = RFalse $ no . injective
2022-02-26 20:17:42 -05:00
public export %inline
varDecEq : (i, j : Var n) -> Dec (i = j)
varDecEq i j = reflectToDec $ eqReflect i j
-- justified by eqReflect [citation needed]
private %inline
decEqFromBool : (i, j : Var n) -> Dec (i = j)
decEqFromBool i j =
if i == j then Yes $ believe_me $ Refl {x = 0}
else No $ id . believe_me
%transform "Var.decEq" varDecEq = decEqFromBool
public export %inline DecEq (Var n) where decEq = varDecEq
export
Tighten Var where
tighten Id i = Just i
tighten (Drop p) VZ = Nothing
tighten (Drop p) (VS i) = tighten p i
tighten (Keep p) VZ = Just VZ
tighten (Keep p) (VS i) = VS <$> tighten p i