quox/lib/Quox/Syntax/Var.idr

331 lines
9.5 KiB
Idris

module Quox.Syntax.Var
import public Quox.Loc
import public Quox.Name
import Quox.Pretty
import Quox.OPE
import Data.Nat
import Data.List
import Data.Vect
import public Quox.Decidable
import Data.Bool.Decidable
import Data.DPair
%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
public export %inline Cast (Var n) Nat where cast = (.nat)
public export %inline Cast (Var n) Integer where cast = cast . cast {to = Nat}
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
public export %inline Injective VS where injective Refl = Refl
export Uninhabited (Var 0) where uninhabited _ impossible
export Uninhabited (VZ = VS i) where uninhabited _ impossible
export Uninhabited (VS i = VZ) where uninhabited _ impossible
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
parameters {auto _ : Pretty.HasEnv m}
private
prettyIndex : Nat -> m (Doc a)
prettyIndex i =
ifUnicode (pretty $ pack $ map sup $ unpack $ show i) ("#" <+> pretty i)
where
sup : Char -> Char
sup c = case c of
'0' => ''; '1' => '¹'; '2' => '²'; '3' => '³'; '4' => ''
'5' => ''; '6' => ''; '7' => ''; '8' => ''; '9' => ''; _ => c
||| `prettyVar hlok hlerr names i` pretty prints the de Bruijn index `i`.
|||
||| If it is within the bounds of `names`, then it uses the name at that index,
||| highlighted as `hlok`. Otherwise it is just printed as a number highlighted
||| as `hlerr`.
export
prettyVar' : HL -> HL -> SnocList BaseName -> Nat -> m (Doc HL)
prettyVar' hlok hlerr names i =
case lookupS i names of
Just x => hlF' hlok $ prettyM x
Nothing => pure $ hl hlerr $ "#" <+> pretty i
export
prettyVar : HL -> HL -> SnocList BaseName -> Var n -> m (Doc HL)
prettyVar hlok hlerr names i = prettyVar' hlok hlerr names i.nat
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
V i = fromNatWith i p
export %inline
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
public export
toNatInj : {i, j : Var n} -> i.nat = j.nat -> i = j
toNatInj {i = VZ} {j = VZ} Refl = Refl
toNatInj {i = VZ} {j = (VS i)} Refl impossible
toNatInj {i = (VS i)} {j = VZ} Refl impossible
toNatInj {i = (VS i)} {j = (VS j)} prf = cong VS $ toNatInj $ injective prf
public export %inline Injective (.nat) where injective = toNatInj
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
-- to be an instance of <https://github.com/idris-lang/Idris2/issues/1259>?
export
weak : (0 p : m `LTE` n) -> Var m -> Var n
weak p i = fromNatWith i.nat $ transitive (toNatLT i) p
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
weakCorrect LTEZero _ impossible
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
interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
public export %inline
fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
fromVar x = fromVarLoc x loc
public export FromVar Var where fromVarLoc x _ = x
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
public export
data LT : Rel (Var n) where
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
GT : Rel (Var n)
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
export Uninhabited (i `Var.LT` i) where uninhabited (LTS p) = uninhabited p
export Uninhabited (VS i `LT` VZ) where uninhabited _ impossible
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
export
isLT : Dec2 Var.LT
isLT i j = reflectToDec $ ltReflect i j
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
%name Compare cmp
export
compareS : Compare i j o -> Compare (VS i) (VS j) o
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)
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
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
export
0 compareSelf : Compare i i o -> o = EQ
compareSelf p = rewrite compare2 p in compareNatDiag i.nat
export
0 comparePSelf : (i : Var n) -> Compare i i EQ
comparePSelf i = rewrite sym $ compareNatDiag i.nat in compareP i i
public export
data LTE : Rel (Var n) where
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
export
Transitive (Var n) LTE where
transitive LTEZ q = LTEZ
transitive (LTES p) (LTES q) = LTES $ transitive p q
export
Antisymmetric (Var n) LTE where
antisymmetric LTEZ LTEZ = Refl
antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q
export
splitLTE : {j : Var n} -> i `LTE` j -> Either (i = j) (i `LT` j)
splitLTE {j = VZ} LTEZ = Left Refl
splitLTE {j = VS _} LTEZ = Right LTZ
splitLTE (LTES p) with (splitLTE p)
_ | Left eq = Left $ cong VS eq
_ | Right lt = Right $ LTS lt
export Uninhabited (VS i `LTE` VZ) where uninhabited _ impossible
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
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
eqReflect (VS i) (VS j) with (eqReflect i j) | (i == j)
_ | RTrue yes | True = RTrue $ cong VS yes
_ | RFalse no | False = RFalse $ no . injective
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