quox/lib/Quox/Syntax/Shift.idr

211 lines
6 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Quox.Syntax.Shift
import public Quox.Syntax.Var
import Quox.Pretty
import Data.Nat
import Data.So
%default total
||| represents the difference between a smaller scope and a larger one.
public export
data Shift : (0 from, to : Nat) -> Type where
SZ : Shift from from
SS : Shift from to -> Shift from (S to)
%name Shift by, bz
%builtin Natural Shift
public export
(.nat) : Shift from to -> Nat
(SZ).nat = Z
(SS by).nat = S by.nat
%transform "Shift.(.nat)" Shift.(.nat) = believe_me
public export Cast (Shift from to) Nat where cast = (.nat)
public export Cast (Shift from to) Integer where cast = cast . cast {to = Nat}
export Eq (Shift from to) where (==) = (==) `on` (.nat)
export Ord (Shift from to) where compare = compare `on` (.nat)
||| shift equivalence, ignoring indices
public export
data Eqv : Shift from1 to1 -> Shift from2 to2 -> Type where
EqSZ : SZ `Eqv` SZ
EqSS : by `Eqv` bz -> SS by `Eqv` SS bz
%name Eqv e
||| two equivalent shifts are equal if they have the same indices.
export
0 fromEqv : by `Eqv` bz -> by = bz
fromEqv EqSZ = Refl
fromEqv (EqSS e) = cong SS $ fromEqv e
||| two equal shifts are equivalent.
export
0 toEqv : by = bz -> by `Eqv` bz
toEqv Refl {by = SZ} = EqSZ
toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl
export
0 shiftDiff : (by : Shift from to) -> to = by.nat + from
shiftDiff SZ = Refl
shiftDiff (SS by) = cong S $ shiftDiff by
export
0 shiftVarLT : (by : Shift from to) -> (i : Var from) ->
by.nat + i.nat `LT` to
shiftVarLT by i =
rewrite plusSuccRightSucc by.nat i.nat in
transitive
(plusLteMonotoneLeft by.nat (S i.nat) from (toNatLT i))
(replace {p=(`LTE` to)} (shiftDiff by) reflexive)
public export
fromNat : (by : Nat) -> Shift from (by + from)
fromNat Z = SZ
fromNat (S by) = SS $ fromNat by
%transform "Shift.fromNat" Shift.fromNat x = believe_me x
public export
fromNat0 : (by : Nat) -> Shift 0 by
fromNat0 by = rewrite sym $ plusZeroRightNeutral by in fromNat by
export
0 fromToNat : (by : Shift from to) -> by `Eqv` fromNat by.nat {from}
fromToNat SZ = EqSZ
fromToNat (SS by) = EqSS $ fromToNat by
export
0 toFromNat : (from, by : Nat) -> by = (fromNat by {from}).nat
toFromNat from 0 = Refl
toFromNat from (S k) = cong S $ toFromNat from k
export
0 toNatInj' : (by : Shift from1 to1) -> (bz : Shift from2 to2) ->
by.nat = bz.nat -> by `Eqv` bz
toNatInj' SZ SZ prf = EqSZ
toNatInj' (SS by) (SS bz) prf = EqSS $ toNatInj' by bz $ injective prf
toNatInj' (SS by) SZ Refl impossible
export
0 toNatInj : {by, bz : Shift from to} -> by.nat = bz.nat -> by = bz
toNatInj {by, bz} e = fromEqv $ toNatInj' by bz e
export %inline
Injective Shift.(.nat) where injective eq = irrelevantEq $ toNatInj eq
public export
ssDown : Shift (S from) to -> Shift from to
ssDown SZ = SS SZ
ssDown (SS by) = SS (ssDown by)
export
0 ssDownEqv : (by : Shift (S from) to) -> ssDown by `Eqv` SS by
ssDownEqv SZ = EqSS EqSZ
ssDownEqv (SS by) = EqSS $ ssDownEqv by
%transform "Shift.ssDown" ssDown by = believe_me (SS by)
public export
shift : Shift from to -> Var from -> Var to
shift SZ i = i
shift (SS by) i = VS $ shift by i
private
shiftViaNat' : (by : Shift from to) -> (i : Var from) ->
(0 p : by.nat + i.nat `LT` to) -> Var to
shiftViaNat' by i p = V $ by.nat + i.nat
private
shiftViaNat : Shift from to -> Var from -> Var to
shiftViaNat by i = shiftViaNat' by i $ shiftVarLT by i
private
0 shiftViaNatCorrect : (by : Shift from to) -> (i : Var from) ->
(0 p : by.nat + i.nat `LT` to) ->
shiftViaNat' by i p = shift by i
shiftViaNatCorrect SZ i (LTESucc p) = fromToNat i _
shiftViaNatCorrect (SS by) i (LTESucc p) = cong VS $ shiftViaNatCorrect by i p
%transform "Shift.shift" shift = shiftViaNat
infixl 9 .
public export
(.) : Shift from mid -> Shift mid to -> Shift from to
by . SZ = by
by . SS bz = SS $ by . bz
private
0 compNatProof : (by : Shift from mid) -> (bz : Shift mid to) ->
to = by.nat + bz.nat + from
compNatProof by bz =
shiftDiff bz >>>
cong (bz.nat +) (shiftDiff by) >>>
plusAssociative bz.nat by.nat from >>>
cong (+ from) (plusCommutative bz.nat by.nat)
where
infixr 0 >>>
0 (>>>) : a = b -> b = c -> a = c
x >>> y = trans x y
private
compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) ->
Shift from (by.nat + bz.nat + from)
compViaNat' by bz = fromNat $ by.nat + bz.nat
private
compViaNat : (by : Shift from mid) -> (bz : Shift mid to) -> Shift from to
compViaNat by bz = rewrite compNatProof by bz in compViaNat' by bz
private
0 compViaNatCorrect : (by : Shift from mid) -> (bz : Shift mid to) ->
by . bz `Eqv` compViaNat' by bz
compViaNatCorrect by SZ =
rewrite plusZeroRightNeutral by.nat in fromToNat by
compViaNatCorrect by (SS bz) =
rewrite sym $ plusSuccRightSucc by.nat bz.nat in
EqSS $ compViaNatCorrect by bz
%transform "Shift.(.)" Shift.(.) = compViaNat
||| `prettyShift bnd unicode prec by` pretty-prints the shift `by`, with the
||| following arguments:
|||
||| * `by : Shift from to`
||| * `bnd : HL` is the highlight used for bound variables of this kind
||| * `unicode : Bool` is whether to use unicode characters in the output
||| * `prec : PPrec` is the surrounding precedence level
export
prettyShift : Pretty.HasEnv m => (bnd : HL) -> Shift from to -> m (Doc HL)
prettyShift bnd by =
parensIfM Outer $ hsep $
[hl bnd !(ifUnicode "𝑖" "i"), hl Delim !(ifUnicode "" ":="),
hl bnd $ !(ifUnicode "𝑖+" "i+") <+> pretty by.nat]
||| prints using the `TVar` highlight for variables
export PrettyHL (Shift from to) where prettyM = prettyShift TVar
infixl 8 //
public export
interface CanShift f where
(//) : f from -> Shift from to -> f to
export CanShift Var where i // by = shift by i
namespace CanShift
public export
[Map] (Functor f, CanShift tm) => CanShift (f . tm) where
x // by = map (// by) x
public export
[Const] CanShift (\_ => a) where x // _ = x