rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

WIP: co-de bruijn #12

Closed
rhi wants to merge 12 commits from 🥚🛁 into 🐉
pull from: 🥚🛁
merge into: rhi:🐉
Conversation 1 Commits 12 Files changed 27 +2428 -994
27 changed files with 2428 additions and 994 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
examples/all.quox
View file

@ -1,6 +1,7 @@
load "misc.quox" load "misc.quox"
load "bool.quox" load "bool.quox"
load "either.quox" load "either.quox"
load "maybe.quox"
load "nat.quox" load "nat.quox"
load "pair.quox" load "pair.quox"
load "list.quox" load "list.quox"

69
examples/maybe.quox Normal file
View file

@ -0,0 +1,69 @@
load "misc.quox"
load "either.quox"
namespace maybe {
def0 Tag : ★ = {nothing, just}
def0 Payload : ω.Tag → ω.★ → ★ =
λ tag A ⇒ caseω tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
def0 Maybe : ω.★ → ★ =
λ A ⇒ (t : Tag) × Payload t A
def tag : 0.(A : ★) → ω.(Maybe A) → Tag =
λ _ x ⇒ caseω x return Tag of { (tag, _) ⇒ tag }
def Nothing : 0.(A : ★) → Maybe A =
λ _ ⇒ ('nothing, 'true)
def Just : 0.(A : ★) → 1.A → Maybe A =
λ _ x ⇒ ('just, x)
def0 IsJustTag : ω.Tag → ★ =
λ t ⇒ caseω t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
def0 IsJust : 0.(A : ★) → ω.(Maybe A) → ★ =
λ A x ⇒ IsJustTag (tag A x)
def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
λ A x ⇒
caseω tag A x return t ⇒ Dec (IsJustTag t) of {
'just ⇒ Yes True 'true;
'nothing ⇒ No False (λ x ⇒ x)
}
def0 nothing-unique :
0.(A : ★) → ω.(x : True) → ('nothing, x) ≡ Nothing A : Maybe A =
λ A x ⇒
caseω x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of {
'true ⇒ δ _ ⇒ ('nothing, 'true)
}
def elim :
0.(A : ★) →
0.(P : 0.(Maybe A) → ★) →
ω.(P (Nothing A)) →
ω.(ω.(x : A) → P (Just A x)) →
1.(x : Maybe A) → P x =
λ A P n j x ⇒
caseω x return x' ⇒ P x' of {
(tag, payload) ⇒
(caseω tag
return t ⇒
0.(eq : tag ≡ t : Tag) → P (t, coe (i ⇒ Payload (eq @i) A) payload)
of {
'nothing ⇒
λ eq ⇒
caseω coe (i ⇒ Payload (eq @i) A) payload
return p ⇒ P ('nothing, p)
of { 'true ⇒ n };
'just ⇒ λ eq ⇒ j (coe (i ⇒ Payload (eq @i) A) payload)
}) (δ _ ⇒ tag)
}
}
def0 Maybe = maybe.Maybe
def0 Just = maybe.Just
def0 Nothing = maybe.Nothing

37
lib/Quox/Context.idr
View file

@ -6,12 +6,16 @@ import Quox.Name
import Data.DPair import Data.DPair
import Data.Nat import Data.Nat
import Data.Fin
import Data.Singleton
import Data.SnocList import Data.SnocList
import Data.SnocVect import Data.SnocVect
import Data.Vect import Data.Vect
import Control.Monad.Identity import Control.Monad.Identity
import Derive.Prelude
%default total %default total
%language ElabReflection
||| a sequence of bindings under an existing context. each successive element ||| a sequence of bindings under an existing context. each successive element
@ -83,6 +87,13 @@ export %inline
toSnocList' : Telescope' a _ _ -> SnocList a toSnocList' : Telescope' a _ _ -> SnocList a
toSnocList' = toSnocListWith id toSnocList' = toSnocListWith id
export %inline
toSnocListRelevant : {n1 : Nat} -> Telescope tm n1 n2 -> SnocList (n ** tm n)
toSnocListRelevant tel = toSnocList' $ snd $ go tel where
go : Telescope tm n1 n2' -> (Singleton n2', Telescope' (n ** tm n) n1 n2')
go [<] = (Val n1, [<])
go (tel :< x) = let (Val n, tel) = go tel in (Val (S n), tel :< (n ** x))
export %inline export %inline
toList : Telescope tm _ _ -> List (Exists tm) toList : Telescope tm _ _ -> List (Exists tm)
toList = toListWith (Evidence _) toList = toListWith (Evidence _)
@ -136,34 +147,34 @@ tel ++ (sx :< x) = (tel ++ sx) :< x
public export public export
getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) -> getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
Shift len out -> Context tm len -> Var len -> tm out Shift len out -> Context tm len -> Fin len -> tm out
getShiftWith shft by (ctx :< t) VZ = t `shft` ssDown by getShiftWith shft by (ctx :< t) FZ = t `shft` ssDown by
getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (ssDown by) ctx i getShiftWith shft by (ctx :< t) (FS i) = getShiftWith shft (ssDown by) ctx i
public export %inline public export %inline
getShift : CanShift tm => Shift len out -> Context tm len -> Var len -> tm out getShift : CanShift tm => Shift len out -> Context tm len -> Fin len -> tm out
getShift = getShiftWith (//) getShift = getShiftWith (//)
public export %inline public export %inline
getWith : (forall from, to. tm from -> Shift from to -> tm to) -> getWith : (forall from, to. tm from -> Shift from to -> tm to) ->
Context tm len -> Var len -> tm len Context tm len -> Fin len -> tm len
getWith shft = getShiftWith shft SZ getWith shft = getShiftWith shft SZ
infixl 8 !! infixl 8 !!
public export %inline public export %inline
(!!) : CanShift tm => Context tm len -> Var len -> tm len (!!) : CanShift tm => Context tm len -> Fin len -> tm len
(!!) = getWith (//) (!!) = getWith (//)
infixl 8 !!! infixl 8 !!!
public export %inline public export %inline
(!!!) : Context' tm len -> Var len -> tm (!!!) : Context' tm len -> Fin len -> tm
(!!!) = getWith const (!!!) = getWith const
public export public export
find : Alternative f => find : Alternative f =>
(forall n. tm n -> Bool) -> Context tm len -> f (Var len) (forall n. tm n -> Bool) -> Context tm len -> f (Fin len)
find p [<] = empty find p [<] = empty
find p (ctx :< x) = (guard (p x) $> VZ) <|> (VS <$> find p ctx) find p (ctx :< x) = (guard (p x) $> FZ) <|> (FS <$> find p ctx)
export export
@ -320,6 +331,14 @@ export %inline
where Show (Exists tm) where showPrec d t = showPrec d t.snd where Show (Exists tm) where showPrec d t = showPrec d t.snd
export
implementation [ShowTelRelevant]
{n1 : Nat} -> ({n : Nat} -> Show (f n)) => Show (Telescope f n1 n2)
where
showPrec d = showPrec d . toSnocListRelevant
where Show (n : Nat ** f n) where showPrec d (_ ** t) = showPrec d t
parameters {opts : LayoutOpts} {0 tm : Nat -> Type} parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
(nameHL : HL) (nameHL : HL)
(pterm : forall n. BContext n -> tm n -> Eff Pretty (Doc opts)) (pterm : forall n. BContext n -> tm n -> Eff Pretty (Doc opts))

44
lib/Quox/FinExtra.idr Normal file
View file

@ -0,0 +1,44 @@
module Quox.FinExtra
import public Data.Fin
import Quox.Decidable
public export
data LT : Rel (Fin n) where
LTZ : FZ `LT` FS i
LTS : i `LT` j -> FS i `LT` FS j
%builtin Natural FinExtra.LT
%name FinExtra.LT lt
public export %inline
GT : Rel (Fin n)
GT = flip LT
export
Transitive (Fin n) LT where
transitive LTZ (LTS _) = LTZ
transitive (LTS p) (LTS q) = LTS $ transitive p q
export Uninhabited (i `FinExtra.LT` i) where uninhabited (LTS p) = uninhabited p
export Uninhabited (FS i `LT` FZ) where uninhabited _ impossible
public export
data Compare : Rel (Fin n) where
IsLT : (lt : i `LT` j) -> Compare i j
IsEQ : Compare i i
IsGT : (gt : i `GT` j) -> Compare i j
%name Compare cmp
export
compareS : Compare i j -> Compare (FS i) (FS j)
compareS (IsLT lt) = IsLT (LTS lt)
compareS IsEQ = IsEQ
compareS (IsGT gt) = IsGT (LTS gt)
export
compareP : (i, j : Fin n) -> Compare i j
compareP FZ FZ = IsEQ
compareP FZ (FS j) = IsLT LTZ
compareP (FS i) FZ = IsGT LTZ
compareP (FS i) (FS j) = compareS $ compareP i j

152
lib/Quox/NatExtra.idr
View file

@ -1,12 +1,19 @@
module Quox.NatExtra module Quox.NatExtra
import public Data.Nat import public Data.Nat
import public Data.Nat.Views
import Data.Nat.Division import Data.Nat.Division
import Data.SnocList import Data.SnocList
import Data.Vect import Data.Vect
import Syntax.PreorderReasoning
%default total %default total
infixl 8 `shiftL`, `shiftR`
infixl 7 .&.
infixl 6 `xor`
infixl 5 .|.
public export public export
data LTE' : Nat -> Nat -> Type where data LTE' : Nat -> Nat -> Type where
@ -55,3 +62,148 @@ parameters {base : Nat} {auto 0 _ : base `GTE` 2} (chars : Vect base Char)
export export
showHex : Nat -> String showHex : Nat -> String
showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF" showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF"
export
0 notEvenOdd : (a, b : Nat) -> Not (a + a = S (b + b))
notEvenOdd 0 b prf = absurd prf
notEvenOdd (S a) b prf =
notEvenOdd b a $ Calc $
|~ b + b
~~ a + S a ..<(inj S prf)
~~ S (a + a) ..<(plusSuccRightSucc {})
export
0 doubleInj : (m, n : Nat) -> m + m = n + n -> m = n
doubleInj 0 0 _ = Refl
doubleInj (S m) (S n) prf =
cong S $ doubleInj m n $
inj S $ Calc $
|~ S (m + m)
~~ m + S m ...(plusSuccRightSucc {})
~~ n + S n ...(inj S prf)
~~ S (n + n) ..<(plusSuccRightSucc {})
export
0 halfDouble : (n : Nat) -> half (n + n) = HalfEven n
halfDouble n with (half (n + n)) | (n + n) proof nn
_ | HalfOdd k | S (k + k) = void $ notEvenOdd n k nn
_ | HalfEven k | k + k = rewrite doubleInj n k nn in Refl
export
floorHalf : Nat -> Nat
floorHalf k = case half k of
HalfOdd n => n
HalfEven n => n
||| like in intercal ☺
|||
||| take all the bits of `subj` that are set in `mask`, and squish them down
||| towards the lsb
public export
select : (mask, subj : Nat) -> Nat
select mask subj = go 1 (halfRec mask) subj 0 where
go : forall mask. Nat -> HalfRec mask -> Nat -> Nat -> Nat
go bit HalfRecZ subj res = res
go bit (HalfRecEven _ rec) subj res = go bit rec (floorHalf subj) res
go bit (HalfRecOdd _ rec) subj res = case half subj of
HalfOdd subj => go (bit + bit) rec subj (res + bit)
HalfEven subj => go (bit + bit) rec subj res
||| take the i least significant bits of subj (where i = popCount mask),
||| and place them where mask's set bits are
|||
||| left inverse of select if mask .|. subj = mask
public export
spread : (mask, subj : Nat) -> Nat
spread mask subj = go 1 (halfRec mask) subj 0 where
go : forall mask. Nat -> HalfRec mask -> Nat -> Nat -> Nat
go bit HalfRecZ subj res = res
go bit (HalfRecEven _ rec) subj res = go (bit + bit) rec subj res
go bit (HalfRecOdd _ rec) subj res = case half subj of
HalfOdd subj => go (bit + bit) rec subj (res + bit)
HalfEven subj => go (bit + bit) rec subj res
public export
data BitwiseRec : Nat -> Nat -> Type where
BwDone : BitwiseRec 0 0
Bw00 : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
BitwiseRec (m + m) (n + n)
Bw01 : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
BitwiseRec (m + m) (S (n + n))
Bw10 : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
BitwiseRec (S (m + m)) (n + n)
Bw11 : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
BitwiseRec (S (m + m)) (S (n + n))
export
bitwiseRec : (m, n : Nat) -> BitwiseRec m n
bitwiseRec m n = go (halfRec m) (halfRec n) where
go : forall m, n. HalfRec m -> HalfRec n -> BitwiseRec m n
go HalfRecZ HalfRecZ = BwDone
go HalfRecZ (HalfRecEven n nr) = Bw00 0 n $ go HalfRecZ nr
go HalfRecZ (HalfRecOdd n nr) = Bw01 0 n $ go HalfRecZ nr
go (HalfRecEven m mr) HalfRecZ = Bw00 m 0 $ go mr HalfRecZ
go (HalfRecEven m mr) (HalfRecEven n nr) = Bw00 m n $ go mr nr
go (HalfRecEven m mr) (HalfRecOdd n nr) = Bw01 m n $ go mr nr
go (HalfRecOdd m mr) HalfRecZ = Bw10 m 0 $ go mr HalfRecZ
go (HalfRecOdd m mr) (HalfRecEven n nr) = Bw10 m n $ go mr nr
go (HalfRecOdd m mr) (HalfRecOdd n nr) = Bw11 m n $ go mr nr
public export
bitwise : (Bool -> Bool -> Bool) -> Nat -> Nat -> Nat
bitwise f m n = go 1 (bitwiseRec m n) 0 where
one : Bool -> Bool -> Nat -> Nat -> Nat
one p q bit res = if f p q then bit + res else res
go : forall m, n. Nat -> BitwiseRec m n -> Nat -> Nat
go bit BwDone res = res
go bit (Bw00 m n rec) res = go (bit + bit) rec $ one False False bit res
go bit (Bw01 m n rec) res = go (bit + bit) rec $ one False True bit res
go bit (Bw10 m n rec) res = go (bit + bit) rec $ one True False bit res
go bit (Bw11 m n rec) res = go (bit + bit) rec $ one True True bit res
public export
(.&.) : Nat -> Nat -> Nat
(.&.) = bitwise $ \p, q => p && q
private %foreign "scheme:blodwen-and"
primAnd : Nat -> Nat -> Nat
%transform "NatExtra.(.&.)" NatExtra.(.&.) m n = primAnd m n
public export
(.|.) : Nat -> Nat -> Nat
(.|.) = bitwise $ \p, q => p || q
private %foreign "scheme:blodwen-or"
primOr : Nat -> Nat -> Nat
%transform "NatExtra.(.|.)" NatExtra.(.|.) m n = primOr m n
public export
xor : Nat -> Nat -> Nat
xor = bitwise (/=)
private %foreign "scheme:blodwen-xor"
primXor : Nat -> Nat -> Nat
%transform "NatExtra.xor" NatExtra.xor m n = primXor m n
public export
shiftL : Nat -> Nat -> Nat
shiftL n 0 = n
shiftL n (S i) = shiftL (n + n) i
private %foreign "scheme:blodwen-shl"
primShiftL : Nat -> Nat -> Nat
%transform "NatExtra.shiftL" NatExtra.shiftL n i = primShiftL n i
public export
shiftR : Nat -> Nat -> Nat
shiftR n 0 = n
shiftR n (S i) = shiftL (floorHalf n) i
private %foreign "scheme:blodwen-shr"
primShiftR : Nat -> Nat -> Nat
%transform "NatExtra.shiftR" NatExtra.shiftR n i = primShiftR n i

116
lib/Quox/Syntax/Dim.idr
View file

@ -1,15 +1,18 @@
module Quox.Syntax.Dim module Quox.Syntax.Dim
import Quox.Loc import Quox.Thin
import Quox.Name
import Quox.Syntax.Var import Quox.Syntax.Var
import Quox.Syntax.Subst import Quox.Syntax.Subst
import Quox.Pretty import Quox.Pretty
import Quox.Name
import Quox.Loc
import Quox.Context import Quox.Context
import Decidable.Equality import Decidable.Equality
import Control.Function import Control.Function
import Derive.Prelude import Derive.Prelude
import Data.DPair
import Data.SnocVect
%default total %default total
%language ElabReflection %language ElabReflection
@ -39,38 +42,48 @@ DecEq DimConst where
public export public export
data Dim : Nat -> Type where data Dim : Nat -> Type where
K : DimConst -> Loc -> Dim d K : DimConst -> Loc -> Dim 0
B : Var d -> Loc -> Dim d B : Loc -> Dim 1
%name Dim.Dim p, q %name Dim.Dim p, q
%runElab deriveIndexed "Dim" [Eq, Ord, Show] %runElab deriveIndexed "Dim" [Eq, Ord, Show]
public export
DimT : Nat -> Type
DimT = Thinned Dim
public export %inline
KT : DimConst -> Loc -> DimT d
KT e loc = Th zero $ K e loc
||| `endsOr l r x p` returns `ends l r ε` if `p` is a constant ε, and ||| `endsOr l r x p` returns `ends l r ε` if `p` is a constant ε, and
||| `x` otherwise. ||| `x` otherwise.
public export public export
endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
endsOr l r x (K e _) = ends l r e endsOr l r x (K e _) = ends l r e
endsOr l r x (B _ _) = x endsOr l r x (B _) = x
export export
Located (Dim d) where Located (Dim d) where
(K _ loc).loc = loc (K _ loc).loc = loc
(B _ loc).loc = loc (B loc).loc = loc
export export
Relocatable (Dim d) where Relocatable (Dim d) where
setLoc loc (K e _) = K e loc setLoc loc (K e _) = K e loc
setLoc loc (B i _) = B i loc setLoc loc (B _) = B loc
export parameters {opts : LayoutOpts}
prettyDimConst : {opts : _} -> DimConst -> Eff Pretty (Doc opts) export
prettyDimConst = hl Dim . text . ends "0" "1" prettyDimConst : DimConst -> Eff Pretty (Doc opts)
prettyDimConst = hl Dim . text . ends "0" "1"
export export
prettyDim : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts) prettyDim : {d : Nat} -> BContext d -> DimT d -> Eff Pretty (Doc opts)
prettyDim names (K e _) = prettyDimConst e prettyDim names (Th _ (K e _)) = prettyDimConst e
prettyDim names (B i _) = prettyDBind $ names !!! i prettyDim names (Th i (B _)) = prettyDBind $ names !!! i.fin
public export %inline public export %inline
@ -83,57 +96,54 @@ DSubst : Nat -> Nat -> Type
DSubst = Subst Dim DSubst = Subst Dim
public export FromVar Dim where fromVarLoc = B -- public export FromVar Dim where fromVarLoc = B
export -- export
CanShift Dim where -- CanShift Dim where
K e loc // _ = K e loc -- K e loc // _ = K e loc
B i loc // by = B (i // by) loc -- B i loc // by = B (i // by) loc
export export %inline FromVar Dim where var = B
export %inline
CanSubstSelf Dim where CanSubstSelf Dim where
K e loc // _ = K e loc Th _ (K e loc) // _ = KT e loc
B i loc // th = getLoc th i loc Th i (B loc) // th = get th i.fin
export Uninhabited (B i loc1 = K e loc2) where uninhabited _ impossible export Uninhabited (B loc1 = K e loc2) where uninhabited _ impossible
export Uninhabited (K e loc1 = B i loc2) where uninhabited _ impossible export Uninhabited (K e loc1 = B loc2) where uninhabited _ impossible
public export -- public export
data Eqv : Dim d1 -> Dim d2 -> Type where -- data Eqv : Dim d1 -> Dim d2 -> Type where
EK : K e _ `Eqv` K e _ -- EK : K e _ `Eqv` K e _
EB : i `Eqv` j -> B i _ `Eqv` B j _ -- EB : i `Eqv` j -> B i _ `Eqv` B j _
export Uninhabited (K e l1 `Eqv` B i l2) where uninhabited _ impossible -- export Uninhabited (K e l1 `Eqv` B i l2) where uninhabited _ impossible
export Uninhabited (B i l1 `Eqv` K e l2) where uninhabited _ impossible -- export Uninhabited (B i l1 `Eqv` K e l2) where uninhabited _ impossible
export -- export
injectiveB : B i loc1 `Eqv` B j loc2 -> i `Eqv` j -- injectiveB : B i loc1 `Eqv` B j loc2 -> i `Eqv` j
injectiveB (EB e) = e -- injectiveB (EB e) = e
export -- export
injectiveK : K e loc1 `Eqv` K f loc2 -> e = f -- injectiveK : K e loc1 `Eqv` K f loc2 -> e = f
injectiveK EK = Refl -- injectiveK EK = Refl
public export -- public export
decEqv : Dec2 Dim.Eqv -- decEqv : Dec2 Dim.Eqv
decEqv (K e _) (K f _) = case decEq e f of -- decEqv (K e _) (K f _) = case decEq e f of
Yes Refl => Yes EK -- Yes Refl => Yes EK
No n => No $ n . injectiveK -- No n => No $ n . injectiveK
decEqv (B i _) (B j _) = case decEqv i j of -- decEqv (B i _) (B j _) = case decEqv i j of
Yes y => Yes $ EB y -- Yes y => Yes $ EB y
No n => No $ \(EB y) => n y -- No n => No $ \(EB y) => n y
decEqv (B _ _) (K _ _) = No absurd -- decEqv (B _ _) (K _ _) = No absurd
decEqv (K _ _) (B _ _) = No absurd -- decEqv (K _ _) (B _ _) = No absurd
||| abbreviation for a bound variable like `BV 4` instead of ||| abbreviation for a bound variable like `BV 4` instead of
||| `B (VS (VS (VS (VS VZ))))` ||| `B (VS (VS (VS (VS VZ))))`
public export %inline public export %inline
BV : (i : Nat) -> (0 _ : LT i d) => (loc : Loc) -> Dim d BV : (i : Fin d) -> (loc : Loc) -> DimT d
BV i loc = B (V i) loc BV i loc = Th (one' i) $ B loc
export
weakD : (by : Nat) -> Dim d -> Dim (by + d)
weakD by p = p // shift by

225
lib/Quox/Syntax/DimEq.idr
View file

@ -6,11 +6,14 @@ import public Quox.Syntax.Subst
import public Quox.Context import public Quox.Context
import Quox.Pretty import Quox.Pretty
import Quox.Name import Quox.Name
import Quox.Thin
import Quox.FinExtra
import Data.Maybe import Data.Maybe
import Data.Nat import Data.Nat
import Data.DPair import Data.DPair
import Data.Fun.Graph import Data.Fun.Graph
import Data.SnocVect
import Decidable.Decidable import Decidable.Decidable
import Decidable.Equality import Decidable.Equality
import Derive.Prelude import Derive.Prelude
@ -21,7 +24,7 @@ import Derive.Prelude
public export public export
DimEq' : Nat -> Type DimEq' : Nat -> Type
DimEq' = Context (Maybe . Dim) DimEq' = Context (Maybe . DimT)
public export public export
@ -29,7 +32,12 @@ data DimEq : Nat -> Type where
ZeroIsOne : DimEq d ZeroIsOne : DimEq d
C : (eqs : DimEq' d) -> DimEq d C : (eqs : DimEq' d) -> DimEq d
%name DimEq eqs %name DimEq eqs
%runElab deriveIndexed "DimEq" [Eq, Ord, Show] %runElab deriveIndexed "DimEq" [Eq]
export
Show (DimEq d) where
showPrec d ZeroIsOne = "ZeroIsOne"
showPrec d (C eq') = showCon d "C" $ showArg eq' @{ShowTelRelevant}
public export public export
@ -72,7 +80,7 @@ toMaybe (Just x) = Just x
export export
fromGround' : Context' DimConst d -> DimEq' d fromGround' : Context' DimConst d -> DimEq' d
fromGround' [<] = [<] fromGround' [<] = [<]
fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc) fromGround' (ctx :< e) = fromGround' ctx :< Just (KT e noLoc)
export export
fromGround : Context' DimConst d -> DimEq d fromGround : Context' DimConst d -> DimEq d
@ -94,39 +102,40 @@ new = C new'
public export %inline public export %inline
get' : DimEq' d -> Var d -> Maybe (Dim d) get' : DimEq' d -> Fin d -> Maybe (DimT d)
get' = getWith $ \p, by => map (// by) p get' = getWith $ \p, by => map (// by) p
public export %inline public export %inline
getVar : DimEq' d -> Var d -> Loc -> Dim d getShift' : Shift len out -> DimEq' len -> Fin len -> Maybe (DimT out)
getVar eqs i loc = fromMaybe (B i loc) $ get' eqs i
public export %inline
getShift' : Shift len out -> DimEq' len -> Var len -> Maybe (Dim out)
getShift' = getShiftWith $ \p, by => map (// by) p getShift' = getShiftWith $ \p, by => map (// by) p
public export %inline public export %inline
get : DimEq' d -> Dim d -> Dim d get : {d : Nat} -> DimEq' d -> DimT d -> DimT d
get _ (K e loc) = K e loc get eqs p@(Th _ (K {})) = p
get eqs (B i loc) = getVar eqs i loc get eqs p@(Th i (B _)) = fromMaybe p $ get' eqs i.fin
public export %inline public export %inline
equal : DimEq d -> (p, q : Dim d) -> Bool equal : {d : Nat} -> DimEq d -> (p, q : DimT d) -> Bool
equal ZeroIsOne p q = True equal ZeroIsOne p q = True
equal (C eqs) p q = get eqs p == get eqs q equal (C eqs) p q = get eqs p == get eqs q
infixl 7 :<? infixl 7 :<?
export %inline export %inline
(:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d) (:<?) : {d : Nat} -> DimEq d -> Maybe (DimT d) -> DimEq (S d)
ZeroIsOne :<? d = ZeroIsOne ZeroIsOne :<? d = ZeroIsOne
C eqs :<? d = C $ eqs :< map (get eqs) d C eqs :<? d = C $ eqs :< map (get eqs) d
private %inline private %inline
ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d) isVar : {d : Nat} -> Fin d -> DimT d -> Bool
ifVar i p = map $ \q => if q == B i noLoc then p else q isVar i (Th j (B _)) = i == j.fin
isVar i (Th _ (K {})) = False
private %inline
ifVar : {d : Nat} -> Fin d -> DimT d -> Maybe (DimT d) -> Maybe (DimT d)
ifVar i p = map $ \q => if isVar i q then p else q
-- (using decEq instead of (==) because of the proofs below) -- (using decEq instead of (==) because of the proofs below)
private %inline private %inline
@ -135,43 +144,45 @@ checkConst e f eqs = if isYes $ e `decEq` f then C eqs else ZeroIsOne
export export
setConst : Var d -> DimConst -> Loc -> DimEq' d -> DimEq d setConst : {d : Nat} -> Fin d -> DimConst -> Loc -> DimEq' d -> DimEq d
setConst VZ e loc (eqs :< Nothing) = setConst FZ e loc (eqs :< Nothing) =
C $ eqs :< Just (K e loc) C $ eqs :< Just (KT e loc)
setConst VZ e _ (eqs :< Just (K f loc)) = setConst FZ e _ (eqs :< Just (Th _ (K f loc))) =
checkConst e f $ eqs :< Just (K f loc) checkConst e f $ eqs :< Just (KT f loc)
setConst VZ e loc (eqs :< Just (B i _)) = setConst FZ e loc (eqs :< Just (Th j (B _))) =
setConst i e loc eqs :<? Just (K e loc) setConst j.fin e loc eqs :<? Just (KT e loc)
setConst (VS i) e loc (eqs :< p) = setConst (FS i) e loc (eqs :< p) =
setConst i e loc eqs :<? ifVar i (K e loc) p setConst i e loc eqs :<? ifVar i (KT e loc) p
mutual mutual
private private
setVar' : (i, j : Var d) -> (0 _ : i `LT` j) -> Loc -> DimEq' d -> DimEq d setVar' : {d : Nat} ->
setVar' VZ (VS i) LTZ loc (eqs :< Nothing) = (i, j : Fin d) -> (0 _ : i `LT` j) -> Loc -> DimEq' d -> DimEq d
C eqs :<? Just (B i loc) setVar' FZ (FS i) LTZ loc (eqs :< Nothing) =
setVar' VZ (VS i) LTZ loc (eqs :< Just (K e eloc)) = C eqs :<? Just (BV i loc)
setConst i e loc eqs :<? Just (K e eloc) setVar' FZ (FS i) LTZ loc (eqs :< Just (Th _ (K e eloc))) =
setVar' VZ (VS i) LTZ loc (eqs :< Just (B j jloc)) = setConst i e loc eqs :<? Just (KT e eloc)
setVar i j loc jloc eqs :<? Just (if j > i then B j jloc else B i loc) setVar' FZ (FS i) LTZ loc (eqs :< Just (Th j (B jloc))) =
setVar' (VS i) (VS j) (LTS lt) loc (eqs :< p) = let j = j.fin in
setVar' i j lt loc eqs :<? ifVar i (B j loc) p setVar i j loc jloc eqs :<? Just (if j > i then BV j jloc else BV i loc)
setVar' (FS i) (FS j) (LTS lt) loc (eqs :< p) =
setVar' i j lt loc eqs :<? ifVar i (BV j loc) p
export %inline export %inline
setVar : (i, j : Var d) -> Loc -> Loc -> DimEq' d -> DimEq d setVar : {d : Nat} -> (i, j : Fin d) -> Loc -> Loc -> DimEq' d -> DimEq d
setVar i j li lj eqs with (compareP i j) | (compare i.nat j.nat) setVar i j li lj eqs with (compareP i j)
setVar i j li lj eqs | IsLT lt | LT = setVar' i j lt lj eqs setVar i j li lj eqs | IsLT lt = setVar' i j lt lj eqs
setVar i i li lj eqs | IsEQ | EQ = C eqs setVar i i li lj eqs | IsEQ = C eqs
setVar i j li lj eqs | IsGT gt | GT = setVar' j i gt li eqs setVar i j li lj eqs | IsGT gt = setVar' j i gt li eqs
export %inline export %inline
set : (p, q : Dim d) -> DimEq d -> DimEq d set : {d : Nat} -> (p, q : DimT d) -> DimEq d -> DimEq d
set _ _ ZeroIsOne = ZeroIsOne set _ _ ZeroIsOne = ZeroIsOne
set (K e eloc) (K f floc) (C eqs) = checkConst e f eqs set (Th _ (K e _)) (Th _ (K f _)) (C eqs) = checkConst e f eqs
set (K e eloc) (B i iloc) (C eqs) = setConst i e eloc eqs set (Th _ (K e el)) (Th j (B _)) (C eqs) = setConst j.fin e el eqs
set (B i iloc) (K e eloc) (C eqs) = setConst i e eloc eqs set (Th i (B _)) (Th _ (K e el)) (C eqs) = setConst i.fin e el eqs
set (B i iloc) (B j jloc) (C eqs) = setVar i j iloc jloc eqs set (Th i (B il)) (Th j (B jl)) (C eqs) = setVar i.fin j.fin il jl eqs
public export %inline public export %inline
@ -179,97 +190,99 @@ Split : Nat -> Type
Split d = (DimEq' d, DSubst (S d) d) Split d = (DimEq' d, DSubst (S d) d)
export %inline export %inline
split1 : DimConst -> Loc -> DimEq' (S d) -> Maybe (Split d) split1 : {d : Nat} -> DimConst -> Loc -> DimEq' (S d) -> Maybe (Split d)
split1 e loc eqs = case setConst VZ e loc eqs of split1 e loc eqs = case setConst 0 e loc eqs of
ZeroIsOne => Nothing ZeroIsOne => Nothing
C (eqs :< _) => Just (eqs, K e loc ::: id) C (eqs :< _) => Just (eqs, id (B loc) :< KT e loc)
export %inline export %inline
split : Loc -> DimEq' (S d) -> List (Split d) split : {d : Nat} -> Loc -> DimEq' (S d) -> List (Split d)
split loc eqs = toList (split1 Zero loc eqs) <+> toList (split1 One loc eqs) split loc eqs = toList (split1 Zero loc eqs) <+> toList (split1 One loc eqs)
export export
splits' : Loc -> DimEq' d -> List (DSubst d 0) splits' : {d : Nat} -> Loc -> DimEq' d -> List (DSubst d 0)
splits' _ [<] = [id] splits' _ [<] = [[<]]
splits' loc eqs@(_ :< _) = splits' loc eqs@(_ :< _) =
[th . ph | (eqs', th) <- split loc eqs, ph <- splits' loc eqs'] [th . ph | (eqs', th) <- split loc eqs, ph <- splits' loc eqs']
||| the Loc is put into each of the DimConsts ||| the Loc is put into each of the DimConsts
export %inline export %inline
splits : Loc -> DimEq d -> List (DSubst d 0) splits : {d : Nat} -> Loc -> DimEq d -> List (DSubst d 0)
splits _ ZeroIsOne = [] splits _ ZeroIsOne = []
splits loc (C eqs) = splits' loc eqs splits loc (C eqs) = splits' loc eqs
private -- private
0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') -> -- 0 newGetShift : (d : Nat) -> (i : Fin d) -> (by : Shift d d') ->
getShift' by (new' {d}) i = Nothing -- getShift' by (new' {d}) i = Nothing
newGetShift (S d) VZ by = Refl -- newGetShift (S d) FZ by = Refl
newGetShift (S d) (VS i) by = newGetShift d i (ssDown by) -- newGetShift (S d) (FS i) by = newGetShift d i (ssDown by)
export -- export
0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing -- 0 newGet' : (d : Nat) -> (i : Fin d) -> get' (new' {d}) i = Nothing
newGet' d i = newGetShift d i SZ -- newGet' d i = newGetShift d i SZ
export -- export
0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p -- 0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
newGet d (K e _) = Refl -- newGet d (K e _) = Refl
newGet d (B i _) = rewrite newGet' d i in Refl -- newGet d (B i _) = rewrite newGet' d i in Refl
export -- export
0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs -- 0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
setSelf p ZeroIsOne = Refl -- setSelf p ZeroIsOne = Refl
setSelf (K Zero _) (C eqs) = Refl -- setSelf (K Zero _) (C eqs) = Refl
setSelf (K One _) (C eqs) = Refl -- setSelf (K One _) (C eqs) = Refl
setSelf (B i _) (C eqs) with (compareP i i) | (compare i.nat i.nat) -- setSelf (B i _) (C eqs) with (compareP i i) | (compare i.nat i.nat)
_ | IsLT lt | LT = absurd lt -- _ | IsLT lt | LT = absurd lt
_ | IsEQ | EQ = Refl -- _ | IsEQ | EQ = Refl
_ | IsGT gt | GT = absurd gt -- _ | IsGT gt | GT = absurd gt
private parameters {opts : LayoutOpts}
prettyDVars : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts)) private
prettyDVars = traverse prettyDBind . toSnocList' prettyDVars : {d : Nat} -> BContext d -> Eff Pretty (SnocList (Doc opts))
prettyDVars = traverse prettyDBind . toSnocList'
private private
prettyCst : {opts : _} -> BContext d -> Dim d -> Dim d -> Eff Pretty (Doc opts) prettyCst : {d : Nat} -> BContext d -> DimT d -> DimT d -> Eff Pretty (Doc opts)
prettyCst dnames p q = prettyCst dnames p q =
hsep <$> sequence [prettyDim dnames p, cstD, prettyDim dnames q] hsep <$> sequence [prettyDim dnames p, cstD, prettyDim dnames q]
private private
prettyCsts : {opts : _} -> BContext d -> DimEq' d -> prettyCsts : {d : Nat} -> BContext d -> DimEq' d ->
Eff Pretty (SnocList (Doc opts)) Eff Pretty (SnocList (Doc opts))
prettyCsts [<] [<] = pure [<] prettyCsts [<] [<] = pure [<]
prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
prettyCsts dnames (eqs :< Just q) = prettyCsts dnames (eqs :< Just q) =
[|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 noLoc) (weakD 1 q)|] [|prettyCsts (tail dnames) eqs :<
prettyCst dnames (BV 0 noLoc) (weak 1 q)|]
export export
prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts) prettyDimEq' : {d : Nat} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
prettyDimEq' dnames eqs = do prettyDimEq' dnames eqs = do
vars <- prettyDVars dnames vars <- prettyDVars dnames
eqs <- prettyCsts dnames eqs eqs <- prettyCsts dnames eqs
let prec = if length vars <= 1 && null eqs then Arg else Outer let prec = if length vars <= 1 && null eqs then Arg else Outer
parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
export export
prettyDimEq : {opts : _} -> BContext d -> DimEq d -> Eff Pretty (Doc opts) prettyDimEq : {d : Nat} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
prettyDimEq dnames ZeroIsOne = do prettyDimEq dnames ZeroIsOne = do
vars <- prettyDVars dnames vars <- prettyDVars dnames
cst <- prettyCst [<] (K Zero noLoc) (K One noLoc) cst <- prettyCst [<] (KT Zero noLoc) (KT One noLoc)
pure $ separateTight !commaD $ vars :< cst pure $ separateTight !commaD $ vars :< cst
prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs
public export public export
wf' : DimEq' d -> Bool wf' : {d : Nat} -> DimEq' d -> Bool
wf' [<] = True wf' [<] = True
wf' (eqs :< Nothing) = wf' eqs wf' (eqs :< Nothing) = wf' eqs
wf' (eqs :< Just (K e _)) = wf' eqs wf' (eqs :< Just (Th _ (K {}))) = wf' eqs
wf' (eqs :< Just (B i _)) = isNothing (get' eqs i) && wf' eqs wf' (eqs :< Just (Th i (B _))) = isNothing (get' eqs i.fin) && wf' eqs
public export public export
wf : DimEq d -> Bool wf : {d : Nat} -> DimEq d -> Bool
wf ZeroIsOne = True wf ZeroIsOne = True
wf (C eqs) = wf' eqs wf (C eqs) = wf' eqs

14
lib/Quox/Syntax/Shift.idr
View file

@ -1,9 +1,11 @@
module Quox.Syntax.Shift module Quox.Syntax.Shift
import public Quox.Syntax.Var import public Quox.Syntax.Var
import public Quox.Thin
import Data.Nat import Data.Nat
import Data.So import Data.So
import Data.DPair
%default total %default total
@ -220,3 +222,15 @@ namespace CanShift
public export %inline public export %inline
[Const] CanShift (\_ => a) where x // _ = x [Const] CanShift (\_ => a) where x // _ = x
export
shiftOPE : {mask : Nat} -> (0 ope : OPE m n mask) ->
Shift n n' -> Subset Nat (OPE m n')
shiftOPE ope SZ = Element _ ope
shiftOPE ope (SS by) =
let Element _ ope = shiftOPE ope by in Element _ $ drop ope
export
CanShift (Thinned f) where
Th ope tm // by = Th (shiftOPE ope by).snd tm

233
lib/Quox/Syntax/Subst.idr
View file

@ -1,10 +1,9 @@
module Quox.Syntax.Subst module Quox.Syntax.Subst
import public Quox.Syntax.Shift import Quox.Thin
import Quox.Syntax.Var import Quox.Loc
import Quox.Name
import Data.Nat import Data.DPair
import Data.List import Data.List
import Data.SnocVect import Data.SnocVect
import Derive.Prelude import Derive.Prelude
@ -14,149 +13,159 @@ import Derive.Prelude
public export public export
data Subst : (Nat -> Type) -> Nat -> Nat -> Type where Subst : (Nat -> Type) -> Nat -> Nat -> Type
Shift : Shift from to -> Subst env from to Subst env from to = SnocVect from (Lazy (Thinned env to))
(:::) : (t : Lazy (env to)) -> Subst env from to -> Subst env (S from) to
%name Subst th, ph, ps
infixr 7 !:::
||| in case the automatic laziness insertion gets confused
public export public export
(!:::) : env to -> Subst env from to -> Subst env (S from) to Subst2 : (Nat -> Nat -> Type) -> Nat -> Nat -> Nat -> Type
t !::: ts = t ::: ts Subst2 env d from to = SnocVect from (Lazy (Thinned2 env d to))
private public export
Repr : (Nat -> Type) -> Nat -> Type get : Subst env f t -> Fin f -> Thinned env t
Repr f to = (List (f to), Nat) get (sx :< x) FZ = x
get (sx :< x) (FS i) = get sx i
private
repr : Subst f from to -> Repr f to
repr (Shift by) = ([], by.nat)
repr (t ::: th) = let (ts, i) = repr th in (t::ts, i)
export Eq (f to) => Eq (Subst f from to) where (==) = (==) `on` repr public export
export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr interface FromVar (0 term : Nat -> Type) where
export Show (f to) => Show (Subst f from to) where show = show . repr var : Loc -> term 1
public export
0 FromVar2 : (Nat -> Nat -> Type) -> Type
FromVar2 t = FromVar (t 0)
public export
varT : FromVar term => Fin n -> Loc -> Thinned term n
varT i loc = Th (one' i) (var loc)
public export
varT2 : FromVar2 term => Fin n -> Loc -> Thinned2 term d n
varT2 i loc = Th2 zero (one' i) (var loc)
infixl 8 // infixl 8 //
namespace CanSubstSelf
public export
interface FromVar term => CanSubstSelf term where
(//) : {f : Nat} -> Thinned term f -> Subst term f t -> Thinned term t
namespace CanSubstSelf2
public export
interface FromVar2 term => CanSubstSelf2 term where
(//) : {f : Nat} -> Thinned2 term d f ->
Subst2 term d f t -> Thinned2 term d t
public export public export
interface FromVar term => CanSubstSelf term where (.) : {mid : Nat} -> CanSubstSelf f =>
(//) : term from -> Lazy (Subst term from to) -> term to Subst f from mid -> Subst f mid to -> Subst f from to
th . ph = map (\(Delay x) => x // ph) th
infixr 9 .%
public export
(.%) : {mid : Nat} -> CanSubstSelf2 f =>
Subst2 f d from mid -> Subst2 f d mid to -> Subst2 f d from to
th .% ph = map (\(Delay x) => x // ph) th
public export public export
getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to tabulate : (n : Nat) -> SnocVect n (Fin n)
getLoc (Shift by) i loc = fromVarLoc (shift by i) loc tabulate n = go n id where
getLoc (t ::: th) VZ _ = t go : (n : Nat) -> (Fin n -> Fin n') -> SnocVect n (Fin n')
getLoc (t ::: th) (VS i) loc = getLoc th i loc go 0 f = [<]
go (S n) f = go n (f . FS) :< f FZ
public export public export
CanSubstSelf Var where id : FromVar term => {n : Nat} -> (under : Nat) -> Loc ->
i // Shift by = shift by i Subst term n (n + under)
VZ // (t ::: th) = t id under loc =
VS i // (t ::: th) = i // th map (\i => delay $ varT (weakenN under i) loc) (tabulate n)
public export %inline
shift : (by : Nat) -> Subst env from (by + from)
shift by = Shift $ fromNat by
public export %inline
shift0 : (by : Nat) -> Subst env 0 by
shift0 by = rewrite sym $ plusZeroRightNeutral by in Shift $ fromNat by
public export public export
(.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to id2 : FromVar2 term => {n : Nat} -> Loc -> Subst2 term d n n
Shift by . Shift bz = Shift $ by . bz id2 loc = map (\i => delay $ varT2 i loc) $ tabulate n
Shift SZ . ph = ph
Shift (SS by) . (t ::: th) = Shift by . th
(t ::: th) . ph = (t // ph) ::: (th . ph)
public export %inline
id : Subst f n n
id = shift 0
public export
traverse : Applicative m =>
(f to -> m (g to)) -> Subst f from to -> m (Subst g from to)
traverse f (Shift by) = pure $ Shift by
traverse f (t ::: th) = [|f t !::: traverse f th|]
-- not in terms of traverse because this map can maintain laziness better
public export
map : (f to -> g to) -> Subst f from to -> Subst g from to
map f (Shift by) = Shift by
map f (t ::: th) = f t ::: map f th
public export %inline
push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
push th = fromVar VZ ::: (th . shift 1)
-- [fixme] a better way to do this?
public export
pushN : CanSubstSelf f => (s : Nat) ->
Subst f from to -> Subst f (s + from) (s + to)
pushN 0 th = th
pushN (S s) th =
rewrite plusSuccRightSucc s from in
rewrite plusSuccRightSucc s to in
pushN s $ fromVar VZ ::: (th . shift 1)
public export
drop1 : Subst f (S from) to -> Subst f from to
drop1 (Shift by) = Shift $ ssDown by
drop1 (t ::: th) = th
public export
fromSnocVect : SnocVect s (f n) -> Subst f (s + n) n
fromSnocVect [<] = id
fromSnocVect (xs :< x) = x ::: fromSnocVect xs
public export %inline
one : f n -> Subst f (S n) n
one x = fromSnocVect [< x]
||| whether two substitutions with the same codomain have the same shape
||| (the same number of terms and the same shift at the end). if so, they
||| also have the same domain
export export
cmpShape : Subst env from1 to -> Subst env from2 to -> select : {n, mask : Nat} -> (0 ope : OPE m n mask) ->
Either Ordering (from1 = from2) SnocVect n a -> SnocVect m a
cmpShape (Shift by) (Shift bz) = cmpLen by bz select ope sx with %syntactic (view ope)
cmpShape (Shift _) (_ ::: _) = Left LT select _ [<] | StopV = [<]
cmpShape (_ ::: _) (Shift _) = Left GT select _ (sx :< x) | DropV _ ope = select ope sx
cmpShape (_ ::: th) (_ ::: ph) = cong S <$> cmpShape th ph select _ (sx :< x) | KeepV _ ope = select ope sx :< x
export
opeToFins : {n, mask : Nat} ->
(0 ope : OPE m n mask) -> SnocVect m (Fin n)
opeToFins ope = select ope $ tabulate n
export
shift : FromVar term => {from : Nat} ->
(n : Nat) -> Loc -> Subst term from (n + from)
shift n loc = map (\i => delay $ varT (shift n i) loc) $ tabulate from
public export
pushN : CanSubstSelf term => {to : Nat} -> (by : Nat) ->
Subst term from to -> Loc -> Subst term (by + from) (by + to)
pushN by th loc =
rewrite plusCommutative by from in
(th . shift by loc) ++ id to loc
public export %inline
push : CanSubstSelf f => {to : Nat} ->
Subst f from to -> Loc -> Subst f (S from) (S to)
push = pushN 1
public export %inline
one : Thinned f n -> Subst f 1 n
one x = [< x]
||| whether two substitutions with the same codomain have the same domain
export
cmpShape : SnocVect m a -> SnocVect n a -> Either Ordering (m = n)
cmpShape [<] [<] = Right Refl
cmpShape [<] (sx :< _) = Left LT
cmpShape (sx :< _) [<] = Left GT
cmpShape (sx :< _) (sy :< _) = cong S <$> cmpShape sx sy
public export public export
record WithSubst tm env n where record WithSubst tm env n where
constructor Sub constructor Sub
term : tm from term : tm from
subst : Lazy (Subst env from n) subst : Subst env from n
{-
export export
(Eq (env n), forall n. Eq (tm n)) => Eq (WithSubst tm env n) where (forall n. Eq (env n), forall n. Eq (tm n)) =>
Eq (WithSubst tm env n) where
Sub t1 s1 == Sub t2 s2 = Sub t1 s1 == Sub t2 s2 =
case cmpShape s1 s2 of case cmpShape s1 s2 of
Left _ => False Left _ => False
Right Refl => t1 == t2 && s1 == s2 Right Refl =>
t1 == t2 && concat @{All} (zipWith ((==) `on` force) s1 s2)
export export
(Ord (env n), forall n. Ord (tm n)) => Ord (WithSubst tm env n) where (forall n. Ord (env n), forall n. Ord (tm n)) =>
Ord (WithSubst tm env n) where
Sub t1 s1 `compare` Sub t2 s2 = Sub t1 s1 `compare` Sub t2 s2 =
case cmpShape s1 s2 of case cmpShape s1 s2 of
Left o => o Left o => o
Right Refl => compare (t1, s1) (t2, s2) Right Refl =>
compare t1 t2 <+> concat (zipWith (compare `on` force) s1 s2)
export %hint export %hint
ShowWithSubst : (Show (env n), forall n. Show (tm n)) => ShowWithSubst : {n : Nat} ->
(forall n. Show (env n), forall n. Show (tm n)) =>
Show (WithSubst tm env n) Show (WithSubst tm env n)
ShowWithSubst = deriveShow ShowWithSubst = deriveShow where
Show (Lazy (Thinned env n)) where showPrec d = showPrec d . force
-}
public export
record WithSubst2 tm env d n where
constructor Sub2
term : tm d from
subst : Subst2 env d from n

620
lib/Quox/Syntax/Term/Base.idr
View file

@ -1,5 +1,6 @@
module Quox.Syntax.Term.Base module Quox.Syntax.Term.Base
import public Quox.Thin
import public Quox.Syntax.Var import public Quox.Syntax.Var
import public Quox.Syntax.Shift import public Quox.Syntax.Shift
import public Quox.Syntax.Subst import public Quox.Syntax.Subst
@ -18,9 +19,6 @@ import Data.Maybe
import Data.Nat import Data.Nat
import public Data.So import public Data.So
import Data.String import Data.String
import public Data.SortedMap
import public Data.SortedMap.Dependent
import public Data.SortedSet
import Derive.Prelude import Derive.Prelude
%default total %default total
@ -46,345 +44,300 @@ TagVal : Type
TagVal = String TagVal = String
||| type-checkable terms, which consists of types and constructor forms.
|||
||| first argument `d` is dimension scope size; second `n` is term scope size
public export public export
data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where data Term : (d, n : Nat) -> Type
Y : (body : f (s + n)) -> ScopedBody s f n %name Term s, t, r
N : (body : f n) -> ScopedBody s f n
%name ScopedBody body
export %inline %hint ||| inferrable terms, which consists of elimination forms like application and
EqScopedBody : (forall n. Eq (f n)) => Eq (ScopedBody s f n) ||| `case` (as well as other terms with an annotation)
EqScopedBody = deriveEq |||
||| first argument `d` is dimension scope size; second `n` is term scope size
export %inline %hint
ShowScopedBody : (forall n. Show (f n)) => Show (ScopedBody s f n)
ShowScopedBody = deriveShow
||| a scoped term with names
public export public export
record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where data Elim : (d, n : Nat) -> Type
constructor S %name Elim e, f
names : BContext s
body : ScopedBody s f n
%name Scoped body
export %inline
(forall n. Eq (f n)) => Eq (Scoped s f n) where
s == t = s.body == t.body
export %inline %hint
ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
ShowScoped = deriveShow
infixl 8 :# public export
infixl 9 :@, :% ScopeTermN : Nat -> TermLike
mutual ScopeTermN s d n = ScopedN s (\n => Term d n) n
public export
TSubst : TSubstLike
TSubst d = Subst $ \n => Elim d n
||| first argument `d` is dimension scope size; public export
||| second `n` is term scope size DScopeTermN : Nat -> TermLike
public export DScopeTermN s d n = ScopedN s (\d => Term d n) d
data Term : (d, n : Nat) -> Type where
||| type of types
TYPE : (l : Universe) -> (loc : Loc) -> Term d n
||| function type public export
Pi : (qty : Qty) -> (arg : Term d n) -> ScopeTerm : TermLike
(res : ScopeTerm d n) -> (loc : Loc) -> Term d n ScopeTerm = ScopeTermN 1
||| function term
Lam : (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
||| pair type public export
Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> (loc : Loc) -> Term d n DScopeTerm : TermLike
||| pair value DScopeTerm = DScopeTermN 1
Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
||| enumeration type
Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
||| enumeration value
Tag : (tag : TagVal) -> (loc : Loc) -> Term d n
||| equality type
Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> (loc : Loc) -> Term d n
||| equality term
DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n
||| natural numbers (temporary until 𝐖 gets added)
Nat : (loc : Loc) -> Term d n
-- [todo] can these be elims?
Zero : (loc : Loc) -> Term d n
Succ : (p : Term d n) -> (loc : Loc) -> Term d n
||| "box" (package a value up with a certain quantity)
BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
Box : (val : Term d n) -> (loc : Loc) -> Term d n
||| elimination
E : (e : Elim d n) -> Term d n
||| term closure/suspended substitution
CloT : WithSubst (Term d) (Elim d) n -> Term d n
||| dimension closure/suspended substitution
DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
%name Term s, t, r
||| first argument `d` is dimension scope size, second `n` is term scope size
public export
data Elim : (d, n : Nat) -> Type where
||| free variable, possibly with a displacement (see @crude, or @mugen for a
||| more abstract and formalised take)
|||
||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
F : (x : Name) -> (u : Universe) -> (loc : Loc) -> Elim d n
||| bound variable
B : (i : Var n) -> (loc : Loc) -> Elim d n
||| term application
App : (fun : Elim d n) -> (arg : Term d n) -> (loc : Loc) -> Elim d n
||| pair destruction
|||
||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
CasePair : (qty : Qty) -> (pair : Elim d n) ->
(ret : ScopeTerm d n) ->
(body : ScopeTermN 2 d n) ->
(loc : Loc) ->
Elim d n
||| enum matching
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
(ret : ScopeTerm d n) ->
(arms : CaseEnumArms d n) ->
(loc : Loc) ->
Elim d n
||| nat matching
CaseNat : (qty, qtyIH : Qty) -> (nat : Elim d n) ->
(ret : ScopeTerm d n) ->
(zero : Term d n) ->
(succ : ScopeTermN 2 d n) ->
(loc : Loc) ->
Elim d n
||| unboxing
CaseBox : (qty : Qty) -> (box : Elim d n) ->
(ret : ScopeTerm d n) ->
(body : ScopeTerm d n) ->
(loc : Loc) ->
Elim d n
||| dim application
DApp : (fun : Elim d n) -> (arg : Dim d) -> (loc : Loc) -> Elim d n
||| type-annotated term
Ann : (tm, ty : Term d n) -> (loc : Loc) -> Elim d n
||| coerce a value along a type equality, or show its coherence
||| [@xtt; §2.1.1]
Coe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
(val : Term d n) -> (loc : Loc) -> Elim d n
||| "generalised composition" [@xtt; §2.1.2]
Comp : (ty : Term d n) -> (p, q : Dim d) ->
(val : Term d n) -> (r : Dim d) ->
(zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
||| match on types. needed for b.s. of coercions [@xtt; §2.2]
TypeCase : (ty : Elim d n) -> (ret : Term d n) ->
(arms : TypeCaseArms d n) -> (def : Term d n) ->
(loc : Loc) ->
Elim d n
||| term closure/suspended substitution
CloE : WithSubst (Elim d) (Elim d) n -> Elim d n
||| dimension closure/suspended substitution
DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
%name Elim e, f
public export
CaseEnumArms : TermLike
CaseEnumArms d n = SortedMap TagVal (Term d n)
public export
TypeCaseArms : TermLike
TypeCaseArms d n = SortedDMap TyConKind (\k => TypeCaseArmBody k d n)
public export
TypeCaseArm : TermLike
TypeCaseArm d n = (k ** TypeCaseArmBody k d n)
public export
TypeCaseArmBody : TyConKind -> TermLike
TypeCaseArmBody k = ScopeTermN (arity k)
public export public export
ScopeTermN, DScopeTermN : Nat -> TermLike TermT : TermLike
ScopeTermN s d n = Scoped s (Term d) n TermT = Thinned2 (\d, n => Term d n)
DScopeTermN s d n = Scoped s (\d => Term d n) d
public export public export
ScopeTerm, DScopeTerm : TermLike ElimT : TermLike
ScopeTerm = ScopeTermN 1 ElimT = Thinned2 (\d, n => Elim d n)
DScopeTerm = DScopeTermN 1
mutual
export %hint
EqTerm : Eq (Term d n)
EqTerm = assert_total {a = Eq (Term d n)} deriveEq
export %hint public export
EqElim : Eq (Elim d n) DimArg : TermLike
EqElim = assert_total {a = Eq (Elim d n)} deriveEq DimArg d n = Dim d
mutual
export %hint
ShowTerm : Show (Term d n)
ShowTerm = assert_total {a = Show (Term d n)} deriveShow
export %hint data Term where
ShowElim : Show (Elim d n) ||| type of types
ShowElim = assert_total {a = Show (Elim d n)} deriveShow TYPE : (l : Universe) -> (loc : Loc) -> Term 0 0
||| scope which ignores all its binders ||| function type
public export %inline Pi : Qty -> Subterms [Term, ScopeTerm] d n -> Loc -> Term d n
SN : {s : Nat} -> f n -> Scoped s f n ||| function value
SN = S (replicate s $ BN Unused noLoc) . N Lam : ScopeTerm d n -> Loc -> Term d n
||| scope which uses its binders ||| pair type
public export %inline Sig : Subterms [Term, ScopeTerm] d n -> Loc -> Term d n
SY : BContext s -> f (s + n) -> Scoped s f n ||| pair value
SY ns = S ns . Y Pair : Subterms [Term, Term] d n -> Loc -> Term d n
public export %inline ||| enum type
name : Scoped 1 f n -> BindName Enum : List TagVal -> Loc -> Term 0 0
name (S [< x] _) = x ||| enum value
Tag : TagVal -> Loc -> Term 0 0
public export %inline ||| equality type
(.name) : Scoped 1 f n -> BindName Eq : Subterms [DScopeTerm, Term, Term] d n -> Loc -> Term d n
s.name = name s ||| equality value
DLam : DScopeTerm d n -> Loc -> Term d n
||| more convenient Pi ||| natural numbers (temporary until 𝐖 gets added)
public export %inline Nat : Loc -> Term 0 0
PiY : (qty : Qty) -> (x : BindName) -> Zero : Loc -> Term 0 0
(arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n Succ : Term d n -> Loc -> Term 0 0
PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
||| more convenient Lam ||| package a value with a quantity
public export %inline ||| e.g. a value of [ω. A], when unpacked, can be used ω times,
LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n ||| even if the box itself is linear
LamY {x, body, loc} = Lam {body = SY [< x] body, loc} BOX : Qty -> Term d n -> Loc -> Term d n
Box : Term d n -> Loc -> Term d n
public export %inline E : Elim d n -> Term d n
LamN : (body : Term d n) -> (loc : Loc) -> Term d n
LamN {body, loc} = Lam {body = SN body, loc}
||| non dependent function type ||| term closure/suspended substitution
public export %inline CloT : WithSubst2 Term Elim d n -> Term d n
Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n ||| dimension closure/suspended substitution
Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc} DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
||| more convenient Sig public export
public export %inline data Elim where
SigY : (x : BindName) -> (fst : Term d n) -> ||| free variable, possibly with a displacement (see @crude, or @mugen for a
(snd : Term d (S n)) -> (loc : Loc) -> Term d n ||| more abstract and formalised take)
SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc} |||
||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
F : Name -> Universe -> Loc -> Elim 0 0
||| bound variable
B : Loc -> Elim 0 1
||| non dependent pair type ||| term application
public export %inline App : Subterms [Elim, Term] d n -> Loc -> Elim d n
And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
||| more convenient Eq ||| pair match
public export %inline ||| - the subterms are, in order: [head, return type, body]
EqY : (i : BindName) -> (ty : Term (S d) n) -> ||| - the quantity is that of the head, and since pairs only have one
(l, r : Term d n) -> (loc : Loc) -> Term d n ||| constructor, can be 0
EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc} CasePair : Qty -> Subterms [Elim, ScopeTerm, ScopeTermN 2] d n ->
Loc -> Elim d n
||| more convenient DLam ||| enum match
public export %inline CaseEnum : Qty -> (arms : List TagVal) ->
DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n Subterms (Elim :: ScopeTerm :: (Term <$ arms)) d n ->
DLamY {i, body, loc} = DLam {body = SY [< i] body, loc} Loc -> Elim d n
public export %inline ||| nat match
DLamN : (body : Term d n) -> (loc : Loc) -> Term d n CaseNat : Qty -> Qty ->
DLamN {body, loc} = DLam {body = SN body, loc} Subterms [Elim, ScopeTerm, Term, ScopeTermN 2] d n ->
Loc -> Elim d n
||| box match
CaseBox : Qty -> Subterms [Elim, ScopeTerm, ScopeTerm] d n -> Loc -> Elim d n
||| dim application
DApp : Subterms [Elim, DimArg] d n -> Loc -> Elim d n
||| type-annotated term
Ann : Subterms [Term, Term] d n -> Loc -> Elim d n
||| coerce a value along a type equality, or show its coherence
||| [@xtt; §2.1.1]
Coe : Subterms [DScopeTerm, DimArg, DimArg, Term] d n ->
Loc -> Elim d n
||| "generalised composition" [@xtt; §2.1.2]
Comp : Subterms [Term, DimArg, DimArg, Term,
DimArg, DScopeTerm, DScopeTerm] d n ->
Loc -> Elim d n
||| match on types. needed for b.s. of coercions [@xtt; §2.2]
TypeCase : Subterms [Elim, Term, -- head, type
Term, -- ★
ScopeTermN 2, -- pi
ScopeTermN 2, -- sig
Term, -- enum
ScopeTermN 5, -- eq
Term, -- nat
ScopeTerm -- box
] d n -> Loc -> Elim d n
||| term closure/suspended substitution
CloE : WithSubst2 Elim Elim d n -> Elim d n
||| dimension closure/suspended substitution
DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
-- this kills the idris ☹
-- export %hint
-- EqTerm : Eq (Term d n)
-- export %hint
-- EqElim : Eq (Elim d n)
-- EqTerm = deriveEq
-- EqElim = deriveEq
-- mutual
-- export %hint
-- ShowTerm : Show (Term d n)
-- ShowTerm = assert_total {a = Show (Term d n)} deriveShow
-- export %hint
-- ShowElim : Show (Elim d n)
-- ShowElim = assert_total {a = Show (Elim d n)} deriveShow
-- ||| scope which ignores all its binders
-- public export %inline
-- SN : {s : Nat} -> f n -> Scoped s f n
-- SN = S (replicate s $ BN Unused noLoc) . N
-- ||| scope which uses its binders
-- public export %inline
-- SY : BContext s -> f (s + n) -> Scoped s f n
-- SY ns = S ns . Y
-- public export %inline
-- name : Scoped 1 f n -> BindName
-- name (S [< x] _) = x
-- public export %inline
-- (.name) : Scoped 1 f n -> BindName
-- s.name = name s
-- ||| more convenient Pi
-- public export %inline
-- PiY : (qty : Qty) -> (x : BindName) ->
-- (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
-- PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
-- ||| more convenient Lam
-- public export %inline
-- LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
-- LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
-- public export %inline
-- LamN : (body : Term d n) -> (loc : Loc) -> Term d n
-- LamN {body, loc} = Lam {body = SN body, loc}
-- ||| non dependent function type
-- public export %inline
-- Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
-- Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
-- ||| more convenient Sig
-- public export %inline
-- SigY : (x : BindName) -> (fst : Term d n) ->
-- (snd : Term d (S n)) -> (loc : Loc) -> Term d n
-- SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
-- ||| non dependent pair type
-- public export %inline
-- And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
-- And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
-- ||| more convenient Eq
-- public export %inline
-- EqY : (i : BindName) -> (ty : Term (S d) n) ->
-- (l, r : Term d n) -> (loc : Loc) -> Term d n
-- EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
-- ||| more convenient DLam
-- public export %inline
-- DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
-- DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
-- public export %inline
-- DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
-- DLamN {body, loc} = DLam {body = SN body, loc}
-- ||| non dependent equality type
-- public export %inline
-- Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
-- Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
||| non dependent equality type
public export %inline
Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
||| same as `F` but as a term ||| same as `F` but as a term
public export %inline public export %inline
FT : Name -> Universe -> Loc -> Term d n FT : Name -> Universe -> Loc -> Term 0 0
FT x u loc = E $ F x u loc FT x u loc = E $ F x u loc
||| abbreviation for a bound variable like `BV 4` instead of ||| abbreviation for a bound variable like `BV 4` instead of
||| `B (VS (VS (VS (VS VZ))))` ||| `B (VS (VS (VS (VS VZ))))`
public export %inline public export %inline
BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n BV : (i : Fin n) -> (loc : Loc) -> ElimT d n
BV i loc = B (V i) loc BV i loc = Th2 zero (one' i) $ B loc
||| same as `BV` but as a term ||| same as `BV` but as a term
public export %inline public export %inline
BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n BVT : (i : Fin n) -> (loc : Loc) -> TermT d n
BVT i loc = E $ BV i loc BVT i loc = Th2 zero (one' i) $ E $ B loc
public export public export
makeNat : Nat -> Loc -> Term d n makeNat : Nat -> Loc -> Term 0 0
makeNat 0 loc = Zero loc makeNat 0 loc = Zero loc
makeNat (S k) loc = Succ (makeNat k loc) loc makeNat (S k) loc = Succ (makeNat k loc) loc
public export %inline
enum : List TagVal -> Loc -> Term d n
enum ts loc = Enum (SortedSet.fromList ts) loc
public export %inline
typeCase : Elim d n -> Term d n ->
List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
public export %inline
typeCase1Y : Elim d n -> Term d n ->
(k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
(loc : Loc) ->
{default (Nat loc) def : Term d n} ->
Elim d n
typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
export export
Located (Elim d n) where Located (Elim d n) where
(F _ _ loc).loc = loc (F _ _ loc).loc = loc
(B _ loc).loc = loc (B loc).loc = loc
(App _ _ loc).loc = loc (App _ loc).loc = loc
(CasePair _ _ _ _ loc).loc = loc (CasePair _ _ loc).loc = loc
(CaseEnum _ _ _ _ loc).loc = loc (CaseEnum _ _ _ loc).loc = loc
(CaseNat _ _ _ _ _ _ loc).loc = loc (CaseNat _ _ _ loc).loc = loc
(CaseBox _ _ _ _ loc).loc = loc (CaseBox _ _ loc).loc = loc
(DApp _ _ loc).loc = loc (DApp _ loc).loc = loc
(Ann _ _ loc).loc = loc (Ann _ loc).loc = loc
(Coe _ _ _ _ loc).loc = loc (Coe _ loc).loc = loc
(Comp _ _ _ _ _ _ _ loc).loc = loc (Comp _ loc).loc = loc
(TypeCase _ _ _ _ loc).loc = loc (TypeCase _ loc).loc = loc
(CloE (Sub e _)).loc = e.loc (CloE (Sub2 e _)).loc = e.loc
(DCloE (Sub e _)).loc = e.loc (DCloE (Sub e _)).loc = e.loc
export export
Located (Term d n) where Located (Term d n) where
(TYPE _ loc).loc = loc (TYPE _ loc).loc = loc
(Pi _ _ _ loc).loc = loc (Pi _ _ loc).loc = loc
(Lam _ loc).loc = loc (Lam _ loc).loc = loc
(Sig _ _ loc).loc = loc (Sig _ loc).loc = loc
(Pair _ _ loc).loc = loc (Pair _ loc).loc = loc
(Enum _ loc).loc = loc (Enum _ loc).loc = loc
(Tag _ loc).loc = loc (Tag _ loc).loc = loc
(Eq _ _ _ loc).loc = loc (Eq _ loc).loc = loc
(DLam _ loc).loc = loc (DLam _ loc).loc = loc
(Nat loc).loc = loc (Nat loc).loc = loc
(Zero loc).loc = loc (Zero loc).loc = loc
@ -392,72 +345,43 @@ Located (Term d n) where
(BOX _ _ loc).loc = loc (BOX _ _ loc).loc = loc
(Box _ loc).loc = loc (Box _ loc).loc = loc
(E e).loc = e.loc (E e).loc = e.loc
(CloT (Sub t _)).loc = t.loc (CloT (Sub2 t _)).loc = t.loc
(DCloT (Sub t _)).loc = t.loc (DCloT (Sub t _)).loc = t.loc
export
Located1 f => Located (ScopedBody s f n) where
(Y t).loc = t.loc
(N t).loc = t.loc
export
Located1 f => Located (Scoped s f n) where
t.loc = t.body.loc
export export
Relocatable (Elim d n) where Relocatable (Elim d n) where
setLoc loc (F x u _) = F x u loc setLoc loc (F x u _) = F x u loc
setLoc loc (B i _) = B i loc setLoc loc (B _) = B loc
setLoc loc (App fun arg _) = App fun arg loc setLoc loc (App ts _) = App ts loc
setLoc loc (CasePair qty pair ret body _) = setLoc loc (CasePair qty ts _) = CasePair qty ts loc
CasePair qty pair ret body loc setLoc loc (CaseEnum qty arms ts _) = CaseEnum qty arms ts loc
setLoc loc (CaseEnum qty tag ret arms _) = setLoc loc (CaseNat qty qtyIH ts _) = CaseNat qty qtyIH ts loc
CaseEnum qty tag ret arms loc setLoc loc (CaseBox qty ts _) = CaseBox qty ts loc
setLoc loc (CaseNat qty qtyIH nat ret zero succ _) = setLoc loc (DApp ts _) = DApp ts loc
CaseNat qty qtyIH nat ret zero succ loc setLoc loc (Ann ts _) = Ann ts loc
setLoc loc (CaseBox qty box ret body _) = setLoc loc (Coe ts _) = Coe ts loc
CaseBox qty box ret body loc setLoc loc (Comp ts _) = Comp ts loc
setLoc loc (DApp fun arg _) = setLoc loc (TypeCase ts _) = TypeCase ts loc
DApp fun arg loc setLoc loc (CloE (Sub2 term subst)) = CloE $ Sub2 (setLoc loc term) subst
setLoc loc (Ann tm ty _) = setLoc loc (DCloE (Sub term subst)) = DCloE $ Sub (setLoc loc term) subst
Ann tm ty loc
setLoc loc (Coe ty p q val _) =
Coe ty p q val loc
setLoc loc (Comp ty p q val r zero one _) =
Comp ty p q val r zero one loc
setLoc loc (TypeCase ty ret arms def _) =
TypeCase ty ret arms def loc
setLoc loc (CloE (Sub term subst)) =
CloE $ Sub (setLoc loc term) subst
setLoc loc (DCloE (Sub term subst)) =
DCloE $ Sub (setLoc loc term) subst
export export
Relocatable (Term d n) where Relocatable (Term d n) where
setLoc loc (TYPE l _) = TYPE l loc setLoc loc (TYPE l _) = TYPE l loc
setLoc loc (Pi qty arg res _) = Pi qty arg res loc setLoc loc (Pi qty ts _) = Pi qty ts loc
setLoc loc (Lam body _) = Lam body loc setLoc loc (Lam body _) = Lam body loc
setLoc loc (Sig fst snd _) = Sig fst snd loc setLoc loc (Sig ts _) = Sig ts loc
setLoc loc (Pair fst snd _) = Pair fst snd loc setLoc loc (Pair ts _) = Pair ts loc
setLoc loc (Enum cases _) = Enum cases loc setLoc loc (Enum cases _) = Enum cases loc
setLoc loc (Tag tag _) = Tag tag loc setLoc loc (Tag tag _) = Tag tag loc
setLoc loc (Eq ty l r _) = Eq ty l r loc setLoc loc (Eq ts _) = Eq ts loc
setLoc loc (DLam body _) = DLam body loc setLoc loc (DLam body _) = DLam body loc
setLoc loc (Nat _) = Nat loc setLoc loc (Nat _) = Nat loc
setLoc loc (Zero _) = Zero loc setLoc loc (Zero _) = Zero loc
setLoc loc (Succ p _) = Succ p loc setLoc loc (Succ p _) = Succ p loc
setLoc loc (BOX qty ty _) = BOX qty ty loc setLoc loc (BOX qty ty _) = BOX qty ty loc
setLoc loc (Box val _) = Box val loc setLoc loc (Box val _) = Box val loc
setLoc loc (E e) = E $ setLoc loc e setLoc loc (E e) = E $ setLoc loc e
setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst setLoc loc (CloT (Sub2 term subst)) = CloT $ Sub2 (setLoc loc term) subst
setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst
export
Relocatable1 f => Relocatable (ScopedBody s f n) where
setLoc loc (Y body) = Y $ setLoc loc body
setLoc loc (N body) = N $ setLoc loc body
export
Relocatable1 f => Relocatable (Scoped s f n) where
setLoc loc (S names body) = S (setLoc loc <$> names) (setLoc loc body)

4
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -18,11 +18,11 @@ prettyUniverse = hl Universe . text . show
export export
prettyTerm : {opts : _} -> BContext d -> BContext n -> Term d n -> prettyTerm : {opts : _} -> BContext d -> BContext n -> TermT d n ->
Eff Pretty (Doc opts) Eff Pretty (Doc opts)
export export
prettyElim : {opts : _} -> BContext d -> BContext n -> Elim d n -> prettyElim : {opts : _} -> BContext d -> BContext n -> ElimT d n ->
Eff Pretty (Doc opts) Eff Pretty (Doc opts)
private private

796
lib/Quox/Syntax/Term/Subst.idr
View file

@ -2,374 +2,462 @@ module Quox.Syntax.Term.Subst
import Quox.No import Quox.No
import Quox.Syntax.Term.Base import Quox.Syntax.Term.Base
import Quox.Syntax.Term.Tighten import Quox.Syntax.Subst
import Data.SnocVect import Data.SnocVect
import Data.Singleton
%default total %default total
namespace CanDSubst
public export
interface CanDSubst (0 tm : TermLike) where
(//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n
||| does the minimal reasonable work: infixl 8 ///
||| - deletes the closure around an atomic constant like `TYPE`
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level dim-closure
||| - otherwise, wraps in a new closure
export
CanDSubst Term where
s // Shift SZ = s
TYPE l loc // _ = TYPE l loc
DCloT (Sub s ph) // th = DCloT $ Sub s $ ph . th
s // th = DCloT $ Sub s th
private parameters {0 f : Nat -> Nat -> Type}
subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n private
subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc th0 : f 0 0 -> Thinned2 f d n
subDArgs e th = DCloE $ Sub e th th0 = Th2 zero zero
||| does the minimal reasonable work: private
||| - deletes the closure around a term variable th1 : {d, n : Nat} -> f d n -> Thinned2 f d n
||| - deletes an identity substitution th1 = Th2 id' id'
||| - composes (lazily) with an existing top-level dim-closure
||| - immediately looks up bound variables in a
||| top-level sequence of dimension applications
||| - otherwise, wraps in a new closure
export
CanDSubst Elim where
e // Shift SZ = e
F x u loc // _ = F x u loc
B i loc // _ = B i loc
e@(DApp {}) // th = subDArgs e th
DCloE (Sub e ph) // th = DCloE $ Sub e $ ph . th
e // th = DCloE $ Sub e th
namespace DSubst.ScopeTermN private dsubTerm : {d1, d2, n : Nat} -> Term d1 n -> DSubst d1 d2 -> TermT d2 n
export %inline private dsubElim : {d1, d2, n : Nat} -> Elim d1 n -> DSubst d1 d2 -> ElimT d2 n
(//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
ScopeTermN s d2 n
S ns (Y body) // th = S ns $ Y $ body // th
S ns (N body) // th = S ns $ N $ body // th
namespace DSubst.DScopeTermN dsubTerm (TYPE l loc) th = th0 $ TYPE l loc
export %inline dsubTerm (Enum strs loc) th = th0 $ Enum strs loc
(//) : {s : Nat} -> dsubTerm (Tag str loc) th = th0 $ Tag str loc
DScopeTermN s d1 n -> Lazy (DSubst d1 d2) -> dsubTerm (Nat loc) th = th0 $ Nat loc
DScopeTermN s d2 n dsubTerm (Zero loc) th = th0 $ Zero loc
S ns (Y body) // th = S ns $ Y $ body // pushN s th dsubTerm (E e) th =
S ns (N body) // th = S ns $ N $ body // th let Th2 dope tope e' = dsubElim e th in
Th2 dope tope $ E e'
dsubTerm (DCloT (Sub t ph)) th = th1 $ DCloT $ Sub t $ ph . th
dsubTerm t th = th1 $ DCloT $ Sub t th
dsubElim (F x l loc) th = th0 $ F x l loc
export %inline FromVar (Elim d) where fromVarLoc = B dsubElim (B loc) th = Th2 zero id' $ B loc
export %inline FromVar (Term d) where fromVarLoc = E .: fromVar dsubElim (DCloE (Sub e ph)) th = th1 $ DCloE $ Sub e $ ph . th
dsubElim e th = th1 $ DCloE $ Sub e th
||| does the minimal reasonable work:
||| - deletes the closure around a *free* name
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level closure
||| - immediately looks up a bound variable
||| - otherwise, wraps in a new closure
export
CanSubstSelf (Elim d) where
F x u loc // _ = F x u loc
B i loc // th = getLoc th i loc
CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
e // th = case force th of
Shift SZ => e
th => CloE $ Sub e th
namespace CanTSubst
public export
interface CanTSubst (0 tm : TermLike) where
(//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE`
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level closure
||| - goes inside `E` in case it is a simple variable or something
||| - otherwise, wraps in a new closure
export
CanTSubst Term where
TYPE l loc // _ = TYPE l loc
E e // th = E $ e // th
CloT (Sub s ph) // th = CloT $ Sub s $ ph . th
s // th = case force th of
Shift SZ => s
th => CloT $ Sub s th
namespace ScopeTermN
export %inline
(//) : {s : Nat} ->
ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
ScopeTermN s d n2
S ns (Y body) // th = S ns $ Y $ body // pushN s th
S ns (N body) // th = S ns $ N $ body // th
namespace DScopeTermN
export %inline
(//) : {s : Nat} ->
DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
S ns (N body) // th = S ns $ N $ body // th
export %inline CanShift (Term d) where s // by = s // Shift by
export %inline CanShift (Elim d) where e // by = e // Shift by
export %inline
{s : Nat} -> CanShift (ScopeTermN s d) where
b // by = b // Shift by
export %inline
comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
comp th ps ph = map (// th) ps . ph
public export %inline
dweakT : (by : Nat) -> Term d n -> Term (by + d) n
dweakT by t = t // shift by
public export %inline
dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
dweakE by t = t // shift by
public export %inline
weakT : (by : Nat) -> Term d n -> Term d (by + n)
weakT by t = t // shift by
public export %inline
weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
weakE by t = t // shift by
parameters {s : Nat}
namespace ScopeTermBody
export %inline
(.term) : ScopedBody s (Term d) n -> Term d (s + n)
(Y b).term = b
(N b).term = weakT s b
namespace ScopeTermN
export %inline
(.term) : ScopeTermN s d n -> Term d (s + n)
t.term = t.body.term
namespace DScopeTermBody
export %inline
(.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
(Y b).term = b
(N b).term = dweakT s b
namespace DScopeTermN
export %inline
(.term) : DScopeTermN s d n -> Term (s + d) n
t.term = t.body.term
export %inline
subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
subN (S _ (Y body)) es = body // fromSnocVect es
subN (S _ (N body)) _ = body
export %inline
sub1 : ScopeTerm d n -> Elim d n -> Term d n
sub1 t e = subN t [< e]
export %inline
dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
dsubN (S _ (Y body)) ps = body // fromSnocVect ps
dsubN (S _ (N body)) _ = body
export %inline
dsub1 : DScopeTerm d n -> Dim d -> Term d n
dsub1 t p = dsubN t [< p]
public export %inline
(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
body.zero = dsub1 body $ K Zero loc
public export %inline
(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
body.one = dsub1 body $ K One loc
public export
0 CloTest : TermLike -> Type
CloTest tm = forall d, n. tm d n -> Bool
interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
public export
0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
NotClo = No . isClo
public export
0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
PushSubsts tm isClo => TermLike
NonClo tm d n = Subset (tm d n) NotClo
public export %inline
nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
(t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
nclo t = Element t nc
parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
||| if the input term has any top-level closures, push them under one layer of
||| syntax
export %inline
pushSubsts : tm d n -> NonClo tm d n
pushSubsts s = pushSubstsWith id id s
export %inline
pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
export %inline
pushSubsts' : tm d n -> tm d n
pushSubsts' s = fst $ pushSubsts s
mutual mutual
public export namespace Term
isCloT : CloTest Term export
isCloT (CloT {}) = True (///) : {d1, d2, n : Nat} -> TermT d1 n -> DSubst d1 d2 -> TermT d2 n
isCloT (DCloT {}) = True Th2 dope tope term /// th =
isCloT (E e) = isCloE e let Val tscope = appOpe n tope; Val dscope = appOpe d1 dope
isCloT _ = False Th2 dope' tope' term' = dsubTerm term (select dope th)
in
Th2 dope' (tope . tope') term'
public export namespace Elim
isCloE : CloTest Elim export
isCloE (CloE {}) = True (///) : {d1, d2, n : Nat} -> ElimT d1 n -> DSubst d1 d2 -> ElimT d2 n
isCloE (DCloE {}) = True Th2 dope tope elim /// th =
isCloE _ = False let Val tscope = appOpe n tope; Val dscope = appOpe d1 dope
Th2 dope' tope' elim' = dsubElim elim (select dope th)
mutual in
export Th2 dope' (tope . tope') elim'
PushSubsts Term Subst.isCloT where
pushSubstsWith th ph (TYPE l loc) =
nclo $ TYPE l loc
pushSubstsWith th ph (Pi qty a body loc) =
nclo $ Pi qty (a // th // ph) (body // th // ph) loc
pushSubstsWith th ph (Lam body loc) =
nclo $ Lam (body // th // ph) loc
pushSubstsWith th ph (Sig a b loc) =
nclo $ Sig (a // th // ph) (b // th // ph) loc
pushSubstsWith th ph (Pair s t loc) =
nclo $ Pair (s // th // ph) (t // th // ph) loc
pushSubstsWith th ph (Enum tags loc) =
nclo $ Enum tags loc
pushSubstsWith th ph (Tag tag loc) =
nclo $ Tag tag loc
pushSubstsWith th ph (Eq ty l r loc) =
nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
pushSubstsWith th ph (DLam body loc) =
nclo $ DLam (body // th // ph) loc
pushSubstsWith _ _ (Nat loc) =
nclo $ Nat loc
pushSubstsWith _ _ (Zero loc) =
nclo $ Zero loc
pushSubstsWith th ph (Succ n loc) =
nclo $ Succ (n // th // ph) loc
pushSubstsWith th ph (BOX pi ty loc) =
nclo $ BOX pi (ty // th // ph) loc
pushSubstsWith th ph (Box val loc) =
nclo $ Box (val // th // ph) loc
pushSubstsWith th ph (E e) =
let Element e nc = pushSubstsWith th ph e in nclo $ E e
pushSubstsWith th ph (CloT (Sub s ps)) =
pushSubstsWith th (comp th ps ph) s
pushSubstsWith th ph (DCloT (Sub s ps)) =
pushSubstsWith (ps . th) ph s
export
PushSubsts Elim Subst.isCloE where
pushSubstsWith th ph (F x u loc) =
nclo $ F x u loc
pushSubstsWith th ph (B i loc) =
let res = getLoc ph i loc in
case nchoose $ isCloE res of
Left yes => assert_total pushSubsts res
Right no => Element res no
pushSubstsWith th ph (App f s loc) =
nclo $ App (f // th // ph) (s // th // ph) loc
pushSubstsWith th ph (CasePair pi p r b loc) =
nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
pushSubstsWith th ph (CaseEnum pi t r arms loc) =
nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
(map (\b => b // th // ph) arms) loc
pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
(z // th // ph) (s // th // ph) loc
pushSubstsWith th ph (CaseBox pi x r b loc) =
nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
pushSubstsWith th ph (DApp f d loc) =
nclo $ DApp (f // th // ph) (d // th) loc
pushSubstsWith th ph (Ann s a loc) =
nclo $ Ann (s // th // ph) (a // th // ph) loc
pushSubstsWith th ph (Coe ty p q val loc) =
nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
pushSubstsWith th ph (Comp ty p q val r zero one loc) =
nclo $ Comp (ty // th // ph) (p // th) (q // th)
(val // th // ph) (r // th)
(zero // th // ph) (one // th // ph) loc
pushSubstsWith th ph (TypeCase ty ret arms def loc) =
nclo $ TypeCase (ty // th // ph) (ret // th // ph)
(map (\t => t // th // ph) arms) (def // th // ph) loc
pushSubstsWith th ph (CloE (Sub e ps)) =
pushSubstsWith th (comp th ps ph) e
pushSubstsWith th ph (DCloE (Sub e ps)) =
pushSubstsWith (ps . th) ph e
private %inline public export
CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> TSubst : Nat -> Nat -> Nat -> Type
(r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n TSubst = Subst2 Elim
CompHY {ty, p, q, val, r, zero, one, loc} =
let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
Comp {
ty = dsub1 ty q, p, q,
val = E $ Coe ty p q val val.loc, r,
-- [fixme] better locations for these vars?
zero = SY zero.names $ E $
Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
one = SY one.names $ E $
Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
loc
}
public export %inline
CompH' : (ty : DScopeTerm d n) ->
(p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
(zero : DScopeTerm d n) ->
(one : DScopeTerm d n) ->
(loc : Loc) ->
Elim d n
CompH' {ty, p, q, val, r, zero, one, loc} =
case dsqueeze ty of
S _ (N ty) => Comp {ty, p, q, val, r, zero, one, loc}
S _ (Y _) => CompHY {ty, p, q, val, r, zero, one, loc}
||| heterogeneous composition, using Comp and Coe (and subst) public export %inline FromVar (Elim 0) where var = B
|||
||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ } export CanSubstSelf2 Elim
||| ≔
||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r { private subTerm : {d, n1, n2 : Nat} -> Term d n1 -> TSubst d n1 n2 -> TermT d n2
||| 0 j ⇒ coe [i ⇒ A] @j @q t₀; private subElim : {d, n1, n2 : Nat} -> Elim d n1 -> TSubst d n1 n2 -> ElimT d n2
||| 1 j ⇒ coe [i ⇒ A] @j @q t₁
||| } subTerm (TYPE l loc) th = th0 $ TYPE l loc
public export %inline subTerm (Nat loc) th = th0 $ Nat loc
CompH : (i : BindName) -> (ty : Term (S d) n) -> subTerm (Zero loc) th = th0 $ Zero loc
(p, q : Dim d) -> (val : Term d n) -> (r : Dim d) -> subTerm (E e) th = let Th2 dope tope e' = subElim e th in Th2 dope tope $ E e'
(j0 : BindName) -> (zero : Term (S d) n) -> subTerm (CloT (Sub2 s ph)) th = th1 $ CloT $ Sub2 s $ ph .% th
(j1 : BindName) -> (one : Term (S d) n) -> subTerm s th = th1 $ CloT $ Sub2 s th
(loc : Loc) ->
Elim d n subElim (F x k loc) th = th0 $ F x k loc
CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} = subElim (B loc) [< e] = e
CompH' {ty = SY [< i] ty, p, q, val, r, subElim (CloE (Sub2 e ph)) th = th1 $ CloE $ Sub2 e $ ph .% th
zero = SY [< j0] zero, one = SY [< j0] one, loc} subElim e th = th1 $ CloE $ Sub2 e th
export
CanSubstSelf2 Elim where
Th2 dope tope elim // th =
let
th' = select tope th
in
?sube2
-- namespace CanDSubst
-- public export
-- interface CanDSubst (0 tm : TermLike) where
-- (//) : {d1 : Nat} -> Thinned2 tm d1 n -> Lazy (DSubst d1 d2) ->
-- Thinned2 tm d2 n
-- ||| does the minimal reasonable work:
-- ||| - deletes the closure around an atomic constant like `TYPE`
-- ||| - deletes an identity substitution
-- ||| - composes (lazily) with an existing top-level dim-closure
-- ||| - otherwise, wraps in a new closure
-- export
-- CanDSubst Term where
-- Th2 _ _ (TYPE l loc) // _ = Th2 zero zero $ TYPE l loc
-- Th2 i j (DCloT (Sub s ph)) // th =
-- Th2 ?i' j $ DCloT $ Sub s $ ph . ?th'
-- Th2 i j s // th = ?sdf -- DCloT $ Sub s th
-- -- private
-- -- subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
-- -- subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
-- -- subDArgs e th = DCloE $ Sub e th
-- -- ||| does the minimal reasonable work:
-- -- ||| - deletes the closure around a term variable
-- -- ||| - deletes an identity substitution
-- -- ||| - composes (lazily) with an existing top-level dim-closure
-- -- ||| - immediately looks up bound variables in a
-- -- ||| top-level sequence of dimension applications
-- -- ||| - otherwise, wraps in a new closure
-- -- export
-- -- CanDSubst Elim where
-- -- e // Shift SZ = e
-- -- F x u loc // _ = F x u loc
-- -- B i loc // _ = B i loc
-- -- e@(DApp {}) // th = subDArgs e th
-- -- DCloE (Sub e ph) // th = DCloE $ Sub e $ ph . th
-- -- e // th = DCloE $ Sub e th
-- -- namespace DSubst.ScopeTermN
-- -- export %inline
-- -- (//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
-- -- ScopeTermN s d2 n
-- -- S ns (Y body) // th = S ns $ Y $ body // th
-- -- S ns (N body) // th = S ns $ N $ body // th
-- -- namespace DSubst.DScopeTermN
-- -- export %inline
-- -- (//) : {s : Nat} ->
-- -- DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
-- -- DScopeTermN s d2 n
-- -- S ns (Y body) // th = S ns $ Y $ body // pushN s th
-- -- S ns (N body) // th = S ns $ N $ body // th
-- -- export %inline FromVar (Elim d) where fromVarLoc = B
-- -- export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
-- -- ||| does the minimal reasonable work:
-- -- ||| - deletes the closure around a *free* name
-- -- ||| - deletes an identity substitution
-- -- ||| - composes (lazily) with an existing top-level closure
-- -- ||| - immediately looks up a bound variable
-- -- ||| - otherwise, wraps in a new closure
-- -- export
-- -- CanSubstSelf (Elim d) where
-- -- F x u loc // _ = F x u loc
-- -- B i loc // th = getLoc th i loc
-- -- CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
-- -- e // th = case force th of
-- -- Shift SZ => e
-- -- th => CloE $ Sub e th
-- -- namespace CanTSubst
-- -- public export
-- -- interface CanTSubst (0 tm : TermLike) where
-- -- (//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
-- -- ||| does the minimal reasonable work:
-- -- ||| - deletes the closure around an atomic constant like `TYPE`
-- -- ||| - deletes an identity substitution
-- -- ||| - composes (lazily) with an existing top-level closure
-- -- ||| - goes inside `E` in case it is a simple variable or something
-- -- ||| - otherwise, wraps in a new closure
-- -- export
-- -- CanTSubst Term where
-- -- TYPE l loc // _ = TYPE l loc
-- -- E e // th = E $ e // th
-- -- CloT (Sub s ph) // th = CloT $ Sub s $ ph . th
-- -- s // th = case force th of
-- -- Shift SZ => s
-- -- th => CloT $ Sub s th
-- -- namespace ScopeTermN
-- -- export %inline
-- -- (//) : {s : Nat} ->
-- -- ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
-- -- ScopeTermN s d n2
-- -- S ns (Y body) // th = S ns $ Y $ body // pushN s th
-- -- S ns (N body) // th = S ns $ N $ body // th
-- -- namespace DScopeTermN
-- -- export %inline
-- -- (//) : {s : Nat} ->
-- -- DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
-- -- S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
-- -- S ns (N body) // th = S ns $ N $ body // th
-- -- export %inline CanShift (Term d) where s // by = s // Shift by
-- -- export %inline CanShift (Elim d) where e // by = e // Shift by
-- -- export %inline
-- -- {s : Nat} -> CanShift (ScopeTermN s d) where
-- -- b // by = b // Shift by
-- -- export %inline
-- -- comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
-- -- comp th ps ph = map (// th) ps . ph
-- -- public export %inline
-- -- dweakT : (by : Nat) -> Term d n -> Term (by + d) n
-- -- dweakT by t = t // shift by
-- -- public export %inline
-- -- dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
-- -- dweakE by t = t // shift by
-- -- public export %inline
-- -- weakT : (by : Nat) -> Term d n -> Term d (by + n)
-- -- weakT by t = t // shift by
-- -- public export %inline
-- -- weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
-- -- weakE by t = t // shift by
-- -- parameters {s : Nat}
-- -- namespace ScopeTermBody
-- -- export %inline
-- -- (.term) : ScopedBody s (Term d) n -> Term d (s + n)
-- -- (Y b).term = b
-- -- (N b).term = weakT s b
-- -- namespace ScopeTermN
-- -- export %inline
-- -- (.term) : ScopeTermN s d n -> Term d (s + n)
-- -- t.term = t.body.term
-- -- namespace DScopeTermBody
-- -- export %inline
-- -- (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
-- -- (Y b).term = b
-- -- (N b).term = dweakT s b
-- -- namespace DScopeTermN
-- -- export %inline
-- -- (.term) : DScopeTermN s d n -> Term (s + d) n
-- -- t.term = t.body.term
-- -- export %inline
-- -- subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
-- -- subN (S _ (Y body)) es = body // fromSnocVect es
-- -- subN (S _ (N body)) _ = body
-- -- export %inline
-- -- sub1 : ScopeTerm d n -> Elim d n -> Term d n
-- -- sub1 t e = subN t [< e]
-- -- export %inline
-- -- dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
-- -- dsubN (S _ (Y body)) ps = body // fromSnocVect ps
-- -- dsubN (S _ (N body)) _ = body
-- -- export %inline
-- -- dsub1 : DScopeTerm d n -> Dim d -> Term d n
-- -- dsub1 t p = dsubN t [< p]
-- -- public export %inline
-- -- (.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
-- -- body.zero = dsub1 body $ K Zero loc
-- -- public export %inline
-- -- (.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
-- -- body.one = dsub1 body $ K One loc
-- -- public export
-- -- 0 CloTest : TermLike -> Type
-- -- CloTest tm = forall d, n. tm d n -> Bool
-- -- interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
-- -- pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
-- -- tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
-- -- public export
-- -- 0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
-- -- NotClo = No . isClo
-- -- public export
-- -- 0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
-- -- PushSubsts tm isClo => TermLike
-- -- NonClo tm d n = Subset (tm d n) NotClo
-- -- public export %inline
-- -- nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
-- -- (t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
-- -- nclo t = Element t nc
-- -- parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
-- -- ||| if the input term has any top-level closures, push them under one layer of
-- -- ||| syntax
-- -- export %inline
-- -- pushSubsts : tm d n -> NonClo tm d n
-- -- pushSubsts s = pushSubstsWith id id s
-- -- export %inline
-- -- pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
-- -- pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
-- -- export %inline
-- -- pushSubsts' : tm d n -> tm d n
-- -- pushSubsts' s = fst $ pushSubsts s
-- -- mutual
-- -- public export
-- -- isCloT : CloTest Term
-- -- isCloT (CloT {}) = True
-- -- isCloT (DCloT {}) = True
-- -- isCloT (E e) = isCloE e
-- -- isCloT _ = False
-- -- public export
-- -- isCloE : CloTest Elim
-- -- isCloE (CloE {}) = True
-- -- isCloE (DCloE {}) = True
-- -- isCloE _ = False
-- -- mutual
-- -- export
-- -- PushSubsts Term Subst.isCloT where
-- -- pushSubstsWith th ph (TYPE l loc) =
-- -- nclo $ TYPE l loc
-- -- pushSubstsWith th ph (Pi qty a body loc) =
-- -- nclo $ Pi qty (a // th // ph) (body // th // ph) loc
-- -- pushSubstsWith th ph (Lam body loc) =
-- -- nclo $ Lam (body // th // ph) loc
-- -- pushSubstsWith th ph (Sig a b loc) =
-- -- nclo $ Sig (a // th // ph) (b // th // ph) loc
-- -- pushSubstsWith th ph (Pair s t loc) =
-- -- nclo $ Pair (s // th // ph) (t // th // ph) loc
-- -- pushSubstsWith th ph (Enum tags loc) =
-- -- nclo $ Enum tags loc
-- -- pushSubstsWith th ph (Tag tag loc) =
-- -- nclo $ Tag tag loc
-- -- pushSubstsWith th ph (Eq ty l r loc) =
-- -- nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
-- -- pushSubstsWith th ph (DLam body loc) =
-- -- nclo $ DLam (body // th // ph) loc
-- -- pushSubstsWith _ _ (Nat loc) =
-- -- nclo $ Nat loc
-- -- pushSubstsWith _ _ (Zero loc) =
-- -- nclo $ Zero loc
-- -- pushSubstsWith th ph (Succ n loc) =
-- -- nclo $ Succ (n // th // ph) loc
-- -- pushSubstsWith th ph (BOX pi ty loc) =
-- -- nclo $ BOX pi (ty // th // ph) loc
-- -- pushSubstsWith th ph (Box val loc) =
-- -- nclo $ Box (val // th // ph) loc
-- -- pushSubstsWith th ph (E e) =
-- -- let Element e nc = pushSubstsWith th ph e in nclo $ E e
-- -- pushSubstsWith th ph (CloT (Sub s ps)) =
-- -- pushSubstsWith th (comp th ps ph) s
-- -- pushSubstsWith th ph (DCloT (Sub s ps)) =
-- -- pushSubstsWith (ps . th) ph s
-- -- export
-- -- PushSubsts Elim Subst.isCloE where
-- -- pushSubstsWith th ph (F x u loc) =
-- -- nclo $ F x u loc
-- -- pushSubstsWith th ph (B i loc) =
-- -- let res = getLoc ph i loc in
-- -- case nchoose $ isCloE res of
-- -- Left yes => assert_total pushSubsts res
-- -- Right no => Element res no
-- -- pushSubstsWith th ph (App f s loc) =
-- -- nclo $ App (f // th // ph) (s // th // ph) loc
-- -- pushSubstsWith th ph (CasePair pi p r b loc) =
-- -- nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
-- -- pushSubstsWith th ph (CaseEnum pi t r arms loc) =
-- -- nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
-- -- (map (\b => b // th // ph) arms) loc
-- -- pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
-- -- nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
-- -- (z // th // ph) (s // th // ph) loc
-- -- pushSubstsWith th ph (CaseBox pi x r b loc) =
-- -- nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
-- -- pushSubstsWith th ph (DApp f d loc) =
-- -- nclo $ DApp (f // th // ph) (d // th) loc
-- -- pushSubstsWith th ph (Ann s a loc) =
-- -- nclo $ Ann (s // th // ph) (a // th // ph) loc
-- -- pushSubstsWith th ph (Coe ty p q val loc) =
-- -- nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
-- -- pushSubstsWith th ph (Comp ty p q val r zero one loc) =
-- -- nclo $ Comp (ty // th // ph) (p // th) (q // th)
-- -- (val // th // ph) (r // th)
-- -- (zero // th // ph) (one // th // ph) loc
-- -- pushSubstsWith th ph (TypeCase ty ret arms def loc) =
-- -- nclo $ TypeCase (ty // th // ph) (ret // th // ph)
-- -- (map (\t => t // th // ph) arms) (def // th // ph) loc
-- -- pushSubstsWith th ph (CloE (Sub e ps)) =
-- -- pushSubstsWith th (comp th ps ph) e
-- -- pushSubstsWith th ph (DCloE (Sub e ps)) =
-- -- pushSubstsWith (ps . th) ph e
-- -- private %inline
-- -- CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
-- -- (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
-- -- CompHY {ty, p, q, val, r, zero, one, loc} =
-- -- let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
-- -- Comp {
-- -- ty = dsub1 ty q, p, q,
-- -- val = E $ Coe ty p q val val.loc, r,
-- -- -- [fixme] better locations for these vars?
-- -- zero = SY zero.names $ E $
-- -- Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
-- -- one = SY one.names $ E $
-- -- Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
-- -- loc
-- -- }
-- -- public export %inline
-- -- CompH' : (ty : DScopeTerm d n) ->
-- -- (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-- -- (zero : DScopeTerm d n) ->
-- -- (one : DScopeTerm d n) ->
-- -- (loc : Loc) ->
-- -- Elim d n
-- -- CompH' {ty, p, q, val, r, zero, one, loc} =
-- -- case dsqueeze ty of
-- -- S _ (N ty) => Comp {ty, p, q, val, r, zero, one, loc}
-- -- S _ (Y _) => CompHY {ty, p, q, val, r, zero, one, loc}
-- -- ||| heterogeneous composition, using Comp and Coe (and subst)
-- -- |||
-- -- ||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
-- -- ||| ≔
-- -- ||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
-- -- ||| 0 j ⇒ coe [i ⇒ A] @j @q t₀;
-- -- ||| 1 j ⇒ coe [i ⇒ A] @j @q t₁
-- -- ||| }
-- -- public export %inline
-- -- CompH : (i : BindName) -> (ty : Term (S d) n) ->
-- -- (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-- -- (j0 : BindName) -> (zero : Term (S d) n) ->
-- -- (j1 : BindName) -> (one : Term (S d) n) ->
-- -- (loc : Loc) ->
-- -- Elim d n
-- -- CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
-- -- CompH' {ty = SY [< i] ty, p, q, val, r,
-- -- zero = SY [< j0] zero, one = SY [< j0] one, loc}

9
lib/Quox/Syntax/Var.idr
View file

@ -138,15 +138,6 @@ export
weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect 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 export
tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) -> tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
(n : Nat) -> Vect n (tm n) (n : Nat) -> Vect n (tm n)

13
lib/Quox/Thin.idr Normal file
View file

@ -0,0 +1,13 @@
module Quox.Thin
import public Quox.Thin.Base
import public Quox.Thin.View
import public Quox.Thin.Eqv
import public Quox.Thin.Cons
import public Quox.Thin.List
import public Quox.Thin.Append
import public Quox.Thin.Comp
import public Quox.Thin.Cover
import public Quox.Thin.Coprod
import public Quox.Thin.Split
import public Quox.Thin.Term

27
lib/Quox/Thin/Append.idr Normal file
View file

@ -0,0 +1,27 @@
module Quox.Thin.Append
import public Quox.Thin.Base
import public Quox.Thin.View
import Data.DPair
%default total
public export
app' : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Exists (OPE (m1 + m2) (n1 + n2))
app' Stop ope2 = Evidence _ ope2
app' (Drop ope1 Refl) ope2 = Evidence _ $ Drop (app' ope1 ope2).snd Refl
app' (Keep ope1 Refl) ope2 = Evidence _ $ Keep (app' ope1 ope2).snd Refl
public export
(++) : {n1, n2, mask1, mask2 : Nat} ->
(0 ope1 : OPE m1 n1 mask1) -> (0 ope2 : OPE m2 n2 mask2) ->
Subset Nat (OPE (m1 + m2) (n1 + n2))
ope1 ++ ope2 with %syntactic (view ope1)
Stop ++ ope2 | StopV = Element _ ope2
Drop ope1 Refl ++ ope2 | DropV mask ope1 =
Element _ $ Drop (ope1 ++ ope2).snd Refl
Keep ope1 Refl ++ ope2 | KeepV mask ope1 =
Element _ $ Keep (ope1 ++ ope2).snd Refl
-- [todo] this mask is just (mask1 << n2) | mask2
-- prove it and add %transform

81
lib/Quox/Thin/Base.idr Normal file
View file

@ -0,0 +1,81 @@
module Quox.Thin.Base
import Data.Fin
import Data.DPair
%default total
||| "order preserving embeddings", for recording a correspondence between a
||| smaller scope and part of a larger one. the third argument is a bitmask
||| representing this OPE, unique for a given `n`.
public export
data OPE : (m, n, mask : Nat) -> Type where
[search m n]
Stop : OPE 0 0 0
Drop : OPE m n mask -> mask' = mask + mask -> OPE m (S n) mask'
Keep : OPE m n mask -> mask' = (S (mask + mask)) -> OPE (S m) (S n) mask'
%name OPE ope
export
Show (OPE m n mask) where
showPrec d Stop = "Stop"
showPrec d (Drop ope Refl) = showCon d "Drop" $ showArg ope ++ " Refl"
showPrec d (Keep ope Refl) = showCon d "Keep" $ showArg ope ++ " Refl"
public export %inline
drop : OPE m n mask -> OPE m (S n) (mask + mask)
drop ope = Drop ope Refl
public export %inline
keep : OPE m n mask -> OPE (S m) (S n) (S (mask + mask))
keep ope = Keep ope Refl
public export
data IsStop : OPE m n mask -> Type where ItIsStop : IsStop Stop
public export
data IsDrop : OPE m n mask -> Type where ItIsDrop : IsDrop (Drop ope eq)
public export
data IsKeep : OPE m n mask -> Type where ItIsKeep : IsKeep (Keep ope eq)
export
0 zeroIsStop : (ope : OPE m 0 mask) -> IsStop ope
zeroIsStop Stop = ItIsStop
||| everything selected
public export
id : {m : Nat} -> Subset Nat (OPE m m)
id {m = 0} = Element _ Stop
id {m = S m} = Element _ $ Keep id.snd Refl
public export %inline
0 id' : {m : Nat} -> OPE m m (fst (Base.id {m}))
id' = id.snd
||| nothing selected
public export
zero : {m : Nat} -> OPE 0 m 0
zero {m = 0} = Stop
zero {m = S m} = Drop zero Refl
||| a single slot selected
public export
one : Fin n -> Subset Nat (OPE 1 n)
one FZ = Element _ $ keep zero
one (FS i) = Element _ $ drop (one i).snd
public export %inline
0 one' : (i : Fin n) -> OPE 1 n (one i).fst
one' i = (one i).snd
public export
record SomeOPE n where
constructor MkOPE
{0 scope : Nat}
{mask : Nat}
0 ope : OPE scope n mask

55
lib/Quox/Thin/Comp.idr Normal file
View file

@ -0,0 +1,55 @@
module Quox.Thin.Comp
import public Quox.Thin.Base
import public Quox.Thin.View
import Quox.NatExtra
import Data.Singleton
%default total
||| inductive definition of OPE composition
public export
data Comp : (l : OPE n p mask1) -> (r : OPE m n mask2) ->
(res : OPE m p mask3) -> Type where
[search l r]
StopZ : Comp Stop Stop Stop
DropZ : Comp a b c -> Comp (Drop a Refl) b (Drop c Refl)
KeepZ : Comp a b c -> Comp (Keep a Refl) (Keep b Refl) (Keep c Refl)
KDZ : Comp a b c -> Comp (Keep a Refl) (Drop b Refl) (Drop c Refl)
public export
record CompResult (ope1 : OPE n p mask1) (ope2 : OPE m n mask2) where
constructor MkComp
{mask : Nat}
{0 ope : OPE m p mask}
0 comp : Comp ope1 ope2 ope
%name CompResult comp
||| compose two OPEs, if the middle scope size is already known at runtime
export
comp' : {n, p, mask1, mask2 : Nat} ->
(0 ope1 : OPE n p mask1) -> (0 ope2 : OPE m n mask2) ->
CompResult ope1 ope2
comp' ope1 ope2 with %syntactic (view ope1) | (view ope2)
comp' Stop Stop | StopV | StopV =
MkComp StopZ
comp' (Drop ope1 Refl) ope2 | DropV _ ope1 | _ =
MkComp $ DropZ (comp' ope1 ope2).comp
comp' (Keep ope1 Refl) (Drop ope2 Refl) | KeepV _ ope1 | DropV _ ope2 =
MkComp $ KDZ (comp' ope1 ope2).comp
comp' (Keep ope1 Refl) (Keep ope2 Refl) | KeepV _ ope1 | KeepV _ ope2 =
MkComp $ KeepZ (comp' ope1 ope2).comp
||| compose two OPEs, after recomputing the middle scope size using `appOpe`
export
comp : {p, mask1, mask2 : Nat} ->
(0 ope1 : OPE n p mask1) -> (0 ope2 : OPE m n mask2) ->
CompResult ope1 ope2
comp ope1 ope2 = let Val n = appOpe p ope1 in comp' ope1 ope2
-- [todo] is there a quick way to compute the mask of comp?
export
0 (.) : (ope1 : OPE n p mask1) -> (ope2 : OPE m n mask2) ->
OPE m p (comp ope1 ope2).mask
ope1 . ope2 = (comp ope1 ope2).ope

74
lib/Quox/Thin/Cons.idr Normal file
View file

@ -0,0 +1,74 @@
module Quox.Thin.Cons
import public Quox.Thin.Base
import Quox.Thin.Eqv
import Quox.Thin.View
import Data.DPair
import Control.Relation
%default total
public export
data IsHead : (ope : OPE m (S n) mask) -> Bool -> Type where
[search ope]
DropH : IsHead (Drop ope eq) False
KeepH : IsHead (Keep ope eq) True
public export
data IsTail : (full : OPE m (S n) mask) -> OPE m' n mask' -> Type where
[search full]
DropT : IsTail (Drop ope eq) ope
KeepT : IsTail (Keep ope eq) ope
public export
record Uncons (ope : OPE m (S n) mask) where
constructor MkUncons
0 head : Bool
{tailMask : Nat}
0 tail : OPE scope n tailMask
{auto isHead : IsHead ope head}
{auto 0 isTail : IsTail ope tail}
public export
uncons : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Uncons ope
uncons ope with %syntactic (view ope)
uncons (Drop ope Refl) | DropV _ ope = MkUncons False ope
uncons (Keep ope Refl) | KeepV _ ope = MkUncons True ope
public export
head : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Exists $ IsHead ope
head ope = Evidence _ (uncons ope).isHead
public export
record Tail (ope : OPE m (S n) mask) where
constructor MkTail
{tailMask : Nat}
0 tail : OPE scope n tailMask
{auto 0 isTail : IsTail ope tail}
public export
tail : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Tail ope
tail ope = let u = uncons ope in MkTail u.tail @{u.isTail}
export
cons : {mask : Nat} -> (head : Bool) -> (0 tail : OPE m n mask) ->
Subset Nat (OPE (if head then S m else m) (S n))
cons False tail = Element _ $ drop tail
cons True tail = Element _ $ keep tail
export
0 consEquiv' : (self : OPE m' (S n) mask') ->
(head : Bool) -> (tail : OPE m n mask) ->
IsHead self head -> IsTail self tail ->
(cons head tail).snd `Eqv` self
consEquiv' (Drop tail _) False tail DropH DropT = EqvDrop reflexive
consEquiv' (Keep tail _) True tail KeepH KeepT = EqvKeep reflexive
export
0 consEquiv : (full : OPE m' (S n) mask') ->
(cons (uncons full).head (uncons full).tail).snd `Eqv` full
consEquiv full with %syntactic (uncons full)
_ | MkUncons head tail {isHead, isTail} =
consEquiv' full head tail isHead isTail

171
lib/Quox/Thin/Coprod.idr Normal file
View file

@ -0,0 +1,171 @@
module Quox.Thin.Coprod
import public Quox.Thin.Base
import public Quox.Thin.Comp
import public Quox.Thin.View
import public Quox.Thin.List
import public Quox.Thin.Cover
import Data.DPair
import Data.Nat
import Control.Function
%default total
namespace Coprod
public export
data Comps : OPE scope n scopeMask ->
OPEList scope -> OPEList n -> Type where
Nil : Comps sub [] []
(::) : Comp sub inner full ->
Comps sub inners fulls ->
Comps sub (inner :: inners) (full :: fulls)
%name Comps comps
public export
record Coprod (fulls : OPEList n) where
constructor MkCoprod
{scopeMask : Nat}
{0 sub : OPE scope n scopeMask}
inners : OPEList scope
0 comps : Comps sub inners fulls
0 cov : Cover inners
%name Coprod cop
export
0 compsLength : Comps s ts us -> length ts = length us
compsLength [] = Refl
compsLength (_ :: comps) = cong S $ compsLength comps
export
coprodNil : Coprod []
coprodNil = MkCoprod [] [] [] {sub = zero}
private
coprodHead : {n : Nat} -> (opes : OPEList (S n)) ->
Either (Cover1 opes) (All IsDrop opes)
coprodHead [] = Right []
coprodHead (ope :: opes) = case view ope of
DropV {} => case coprodHead opes of
Left cov1 => Left $ There cov1
Right drops => Right $ ItIsDrop :: drops
KeepV {} => Left Here
private
0 compsConsDrop : (opes : OPEList (S n)) ->
All IsDrop opes ->
All2 IsTail opes tails ->
Comps sub inners tails -> Comps (drop sub) inners opes
compsConsDrop [] [] [] [] = []
compsConsDrop (Drop ope Refl :: opes) (ItIsDrop :: ds) (DropT :: ts) (c :: cs) =
DropZ c :: compsConsDrop opes ds ts cs
compsConsDrop (_ :: _) [] _ _ impossible
private
coprodConsDrop : (0 opes : OPEList (S n)) ->
(0 ds : All IsDrop opes) ->
(0 ts : All2 IsTail opes tails) ->
Coprod tails -> Coprod opes
coprodConsDrop opes ds ts (MkCoprod inners comps cov) =
MkCoprod inners (compsConsDrop opes ds ts comps) cov
private
copyHeads : {m : Nat} ->
(src : OPEList (S m)) -> (tgt : OPEList n) ->
(0 eq : length src = length tgt) => OPEList (S n)
copyHeads [] [] = []
copyHeads (s :: ss) (t :: ts) =
case view s of
DropV mask ope => drop t :: copyHeads ss ts @{inj S eq}
KeepV mask ope => keep t :: copyHeads ss ts @{inj S eq}
private
0 copyHeadsComps : (eq : length outers = length inners) ->
All2 IsTail outers tails ->
Comps sub inners tails ->
Comps (keep sub) (copyHeads outers inners) outers
copyHeadsComps _ [] [] = []
copyHeadsComps eq (DropT {eq = eq2} :: ps) ((c :: cs) {full}) =
let (Refl) = eq2 in -- coverage checker weirdness
rewrite viewDrop full Refl in
KDZ c :: copyHeadsComps (inj S eq) ps cs
copyHeadsComps eq (KeepT {eq = eq2} :: ps) ((c :: cs) {full}) =
let (Refl) = eq2 in
rewrite viewKeep full Refl in
KeepZ c :: copyHeadsComps (inj S eq) ps cs
-- should be erased (coverage checker weirdness)
-- it is possibly https://github.com/idris-lang/Idris2/issues/1417 that keeps
-- happening. not 100% sure
private
cover1CopyHeads : {m : Nat} ->
(ss : OPEList (S m)) -> (ts : OPEList n) ->
(eq : length ss = length ts) ->
(cov1 : Cover1 ss) -> Cover1 (copyHeads ss ts)
cover1CopyHeads (Keep s Refl :: ss) (t :: ts) eq Here =
rewrite viewKeep s Refl in Here
cover1CopyHeads (s :: ss) (t :: ts) eq (There c) with (view s)
cover1CopyHeads (Drop {} :: ss) (t :: ts) eq (There c) | DropV {} =
There $ cover1CopyHeads ss ts (inj S eq) c
cover1CopyHeads (Keep {} :: ss) (t :: ts) eq (There c) | KeepV {} =
Here
private
copyHeadsTails : {m : Nat} ->
(ss : OPEList (S m)) -> (ts : OPEList n) ->
(eq : length ss = length ts) ->
All2 IsTail (copyHeads ss ts) ts
copyHeadsTails [] [] eq = []
copyHeadsTails (s :: ss) (t :: ts) eq with (view s)
copyHeadsTails (Drop ope Refl :: ss) (t :: ts) eq | DropV mask ope =
DropT :: copyHeadsTails ss ts (inj S eq)
copyHeadsTails (Keep ope Refl :: ss) (t :: ts) eq | KeepV mask ope =
KeepT :: copyHeadsTails ss ts (inj S eq)
private
coprodConsKeep : {n : Nat} ->
(opes : OPEList (S n)) ->
{0 tails : OPEList n} ->
(cov1 : Cover1 opes) ->
(0 ts : All2 IsTail opes tails) ->
Coprod tails -> Coprod opes
coprodConsKeep opes cov1 ts (MkCoprod inners comps cov) =
MkCoprod
(copyHeads opes inners @{all2Length ts `trans` sym (compsLength comps)})
(copyHeadsComps _ ts comps)
((cover1CopyHeads {cov1, _} :: cov) @{copyHeadsTails {}})
export
coprod : {n : Nat} -> (opes : OPEList n) -> Coprod opes
private
coprod0 : (opes : OPEList 0) -> Coprod opes
private
coprodS : {n : Nat} -> (opes : OPEList (S n)) -> Coprod opes
coprod {n = 0} opes = coprod0 opes
coprod {n = S n} opes = coprodS opes
coprod0 [] = coprodNil
coprod0 (ope :: opes) with %syntactic 0 (zeroIsStop ope) | (coprod opes)
coprod0 (Stop :: opes)
| ItIsStop | MkCoprod {sub} inners comps cov
with %syntactic 0 (zeroIsStop sub)
coprod0 (Stop :: opes)
| ItIsStop | MkCoprod {sub = Stop} inners comps cov | ItIsStop
= MkCoprod (Stop :: inners) (StopZ :: comps) []
coprodS [] = coprodNil
coprodS opes =
let hs = heads opes
Element ts tprf = tails_ opes
tcop = coprod $ assert_smaller opes ts
in
case coprodHead opes of
Left cov1 => coprodConsKeep opes cov1 tprf tcop
Right drops => coprodConsDrop opes drops tprf tcop

27
lib/Quox/Thin/Cover.idr Normal file
View file

@ -0,0 +1,27 @@
module Quox.Thin.Cover
import public Quox.Thin.Base
import public Quox.Thin.List
%default total
||| an OPE list is a cover if at least one of the OPEs has `Keep` as the head,
||| and the tails are also a cover
|||
||| in @egtbs it is a binary relation which is fine for ×ᵣ but i don't want to
||| write my AST in universe-of-syntaxes style. sorry
public export data Cover : OPEList n -> Type
||| the "`Keep` in the head" condition of a cover
public export data Cover1 : OPEList n -> Type
data Cover where
Nil : Cover opes {n = 0}
(::) : Cover1 opes -> All2 IsTail opes tails => Cover tails -> Cover opes
%name Cover cov
data Cover1 where
Here : Cover1 (Keep ope eq :: opes)
There : Cover1 opes -> Cover1 (ope :: opes)
%name Cover1 cov1
%builtin Natural Cover1

128
lib/Quox/Thin/Eqv.idr Normal file
View file

@ -0,0 +1,128 @@
module Quox.Thin.Eqv
import public Quox.Thin.Base
import public Quox.Thin.View
import Quox.NatExtra
import Syntax.PreorderReasoning
%default total
infix 6 `Eqv`
private
uip : (p, q : a = b) -> p = q
uip Refl Refl = Refl
public export
data Eqv : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type where
EqvStop : Eqv Stop Stop
EqvDrop : {0 p : OPE m1 n1 mask1} ->
{0 q : OPE m2 n2 mask2} ->
Eqv p q -> Eqv (Drop p eq1) (Drop q eq2)
EqvKeep : {0 p : OPE m1 n1 mask1} ->
{0 q : OPE m2 n2 mask2} ->
Eqv p q -> Eqv (Keep p eq1) (Keep q eq2)
%name Eqv eqv
export Uninhabited (Stop `Eqv` Drop p e) where uninhabited _ impossible
export Uninhabited (Stop `Eqv` Keep p e) where uninhabited _ impossible
export Uninhabited (Drop p e `Eqv` Stop) where uninhabited _ impossible
export Uninhabited (Drop p e `Eqv` Keep q f) where uninhabited _ impossible
export Uninhabited (Keep p e `Eqv` Stop) where uninhabited _ impossible
export Uninhabited (Keep p e `Eqv` Drop q f) where uninhabited _ impossible
export
Reflexive (OPE m n mask) Eqv where
reflexive {x = Stop} = EqvStop
reflexive {x = Drop {}} = EqvDrop reflexive
reflexive {x = Keep {}} = EqvKeep reflexive
export
symmetric : p `Eqv` q -> q `Eqv` p
symmetric EqvStop = EqvStop
symmetric (EqvDrop eqv) = EqvDrop $ symmetric eqv
symmetric (EqvKeep eqv) = EqvKeep $ symmetric eqv
export
transitive : p `Eqv` q -> q `Eqv` r -> p `Eqv` r
transitive EqvStop EqvStop = EqvStop
transitive (EqvDrop eqv1) (EqvDrop eqv2) = EqvDrop (transitive eqv1 eqv2)
transitive (EqvKeep eqv1) (EqvKeep eqv2) = EqvKeep (transitive eqv1 eqv2)
private
recompute' : {mask1, mask2, n1, n2 : Nat} ->
(0 p : OPE m1 n1 mask1) -> (0 q : OPE m2 n2 mask2) ->
(0 eqv : p `Eqv` q) -> p `Eqv` q
recompute' p q eqv with %syntactic (view p) | (view q)
recompute' Stop Stop _ | StopV | StopV = EqvStop
recompute' (Drop p _) (Drop q _) eqv | DropV _ p | DropV _ q =
EqvDrop $ recompute' {eqv = let EqvDrop e = eqv in e, _}
recompute' (Keep p _) (Keep q _) eqv | KeepV _ p | KeepV _ q =
EqvKeep $ recompute' {eqv = let EqvKeep e = eqv in e, _}
recompute' (Drop p _) (Keep q _) eqv | DropV _ p | KeepV _ q =
void $ absurd eqv
recompute' (Keep p _) (Drop q _) eqv | KeepV _ p | DropV _ q =
void $ absurd eqv
private
recompute : {mask1, mask2, n1, n2 : Nat} ->
{0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
(0 _ : p `Eqv` q) -> p `Eqv` q
recompute eqv = recompute' {eqv, _}
export
eqvIndices : {0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
p `Eqv` q -> (m1 = m2, n1 = n2, mask1 = mask2)
eqvIndices EqvStop = (Refl, Refl, Refl)
eqvIndices (EqvDrop eqv {eq1 = Refl, eq2 = Refl}) =
let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
eqvIndices (EqvKeep eqv {eq1 = Refl, eq2 = Refl}) =
let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
export
0 eqvMask : (p : OPE m1 n mask1) -> (q : OPE m2 n mask2) ->
mask1 = mask2 -> p `Eqv` q
eqvMask Stop Stop _ = EqvStop
eqvMask (Drop ope1 Refl) (Drop {mask = mm2} ope2 eq2) Refl =
EqvDrop $ eqvMask ope1 ope2 (doubleInj _ _ eq2)
eqvMask (Drop ope1 Refl) (Keep ope2 eq2) Refl =
void $ notEvenOdd _ _ eq2
eqvMask (Keep ope1 eq1) (Keep ope2 eq2) Refl =
EqvKeep $ eqvMask ope1 ope2 (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
eqvMask (Keep ope1 eq1) (Drop ope2 eq2) Refl =
void $ notEvenOdd _ _ $ trans (sym eq2) eq1
export
0 eqvEq : (p, q : OPE m n mask) -> p `Eqv` q -> p === q
eqvEq Stop Stop EqvStop = Refl
eqvEq (Drop p eq1) (Drop q eq2) (EqvDrop eqv)
with %syntactic (doubleInj _ _ $ trans (sym eq1) eq2)
_ | Refl = cong2 Drop (eqvEq p q eqv) (uip eq1 eq2)
eqvEq (Keep p eq1) (Keep q eq2) (EqvKeep eqv)
with %syntactic (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
_ | Refl = cong2 Keep (eqvEq p q eqv) (uip eq1 eq2)
export
0 eqvEq' : (p : OPE m1 n1 mask1) -> (q : OPE m2 n2 mask2) ->
p `Eqv` q -> p ~=~ q
eqvEq' p q eqv = let (Refl, Refl, Refl) = eqvIndices eqv in eqvEq p q eqv
export
0 maskEqInner : (0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
mask1 = mask2 -> m1 = m2
maskEqInner Stop Stop _ = Refl
maskEqInner (Drop ope1 Refl) (Drop ope2 Refl) eq =
maskEqInner ope1 ope2 (doubleInj _ _ eq)
maskEqInner (Keep ope1 Refl) (Keep ope2 Refl) eq =
cong S $ maskEqInner ope1 ope2 $ doubleInj _ _ $ inj S eq
maskEqInner (Drop ope1 Refl) (Keep ope2 Refl) eq = void $ notEvenOdd _ _ eq
maskEqInner (Keep {mask = mask1'} ope1 eq1) (Drop {mask = mask2'} ope2 eq2) eq =
-- matching on eq1, eq2, or eq here triggers that weird coverage bug ☹
void $ notEvenOdd _ _ $ Calc $
|~ mask2' + mask2'
~~ mask2 ..<(eq2)
~~ mask1 ..<(eq)
~~ S (mask1' + mask1') ...(eq1)

127
lib/Quox/Thin/List.idr Normal file
View file

@ -0,0 +1,127 @@
module Quox.Thin.List
import public Quox.Thin.Base
import public Quox.Thin.Cons
import Data.DPair
import Data.Nat
import Control.Function
%default total
||| a list of OPEs of a given outer scope size
||| (at runtime just the masks)
public export
data OPEList : Nat -> Type where
Nil : OPEList n
(::) : {mask : Nat} -> (0 ope : OPE m n mask) -> OPEList n -> OPEList n
%name OPEList opes
public export
length : OPEList n -> Nat
length [] = 0
length (_ :: opes) = S $ length opes
public export
toList : OPEList n -> List (SomeOPE n)
toList [] = []
toList (ope :: opes) = MkOPE ope :: toList opes
public export
fromList : List (SomeOPE n) -> OPEList n
fromList [] = []
fromList (MkOPE ope :: xs) = ope :: fromList xs
public export
0 Pred : Nat -> Type
Pred n = forall m, mask. OPE m n mask -> Type
public export
0 Rel : Nat -> Nat -> Type
Rel n1 n2 = forall m1, m2, mask1, mask2.
OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type
namespace All
public export
data All : Pred n -> OPEList n -> Type where
Nil : {0 p : Pred n} -> All p []
(::) : {0 p : Pred n} -> p ope -> All p opes -> All p (ope :: opes)
%name All.All ps, qs
namespace All2
public export
data All2 : Rel n1 n2 -> OPEList n1 -> OPEList n2 -> Type where
Nil : {0 p : Rel n1 n2} -> All2 p [] []
(::) : {0 p : Rel n1 n2} -> p a b -> All2 p as bs ->
All2 p (a :: as) (b :: bs)
%name All2.All2 ps, qs
export
0 all2Length : {p : Rel m n} -> All2 p ss ts -> length ss = length ts
all2Length [] = Refl
all2Length (p :: ps) = cong S $ all2Length ps
namespace Any
public export
data Any : Pred n -> OPEList n -> Type where
Here : {0 p : Pred n} -> p ope -> Any p (ope :: opes)
There : {0 p : Pred n} -> Any p opes -> Any p (ope :: opes)
%name Any.Any p, q
export
{0 p : Pred n} -> Uninhabited (Any p []) where uninhabited _ impossible
export
all : {0 p : Pred n} ->
(forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> p ope) ->
(opes : OPEList n) -> All p opes
all f [] = []
all f (ope :: opes) = f ope :: all f opes
export
allDec : {0 p : Pred n} ->
(forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> Dec (p ope)) ->
(opes : OPEList n) -> Dec (All p opes)
allDec f [] = Yes []
allDec f (ope :: opes) = case f ope of
Yes y => case allDec f opes of
Yes ys => Yes $ y :: ys
No k => No $ \(_ :: ps) => k ps
No k => No $ \(p :: _) => k p
export
anyDec : {0 p : Pred n} ->
(forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> Dec (p ope)) ->
(opes : OPEList n) -> Dec (Any p opes)
anyDec f [] = No absurd
anyDec f (ope :: opes) = case f ope of
Yes y => Yes $ Here y
No nh => case anyDec f opes of
Yes y => Yes $ There y
No nt => No $ \case Here h => nh h; There t => nt t
export
unconses : {n : Nat} -> (opes : OPEList (S n)) -> All Uncons opes
unconses = all uncons
export
heads : {n : Nat} -> (opes : OPEList (S n)) -> All (Exists . IsHead) opes
heads = all head
export
tails : {n : Nat} -> (opes : OPEList (S n)) -> All Tail opes
tails = all tail
export
tails_ : {n : Nat} -> (opes : OPEList (S n)) ->
Subset (OPEList n) (All2 IsTail opes)
tails_ [] = Element [] []
tails_ (ope :: opes) = Element _ $ (tail ope).isTail :: (tails_ opes).snd
export
conses : (heads : List Bool) -> (tails : OPEList n) ->
(0 len : length heads = length tails) =>
OPEList (S n)
conses [] [] = []
conses (h :: hs) (t :: ts) = snd (cons h t) :: conses hs ts @{inj S len}

57
lib/Quox/Thin/Split.idr Normal file
View file

@ -0,0 +1,57 @@
module Quox.Thin.Split
import public Quox.Thin.Base
import public Quox.Thin.View
import public Quox.Thin.Eqv
import public Quox.Thin.Append
import public Quox.Thin.Cover
import Data.DPair
import Control.Relation
%default total
public export
record Chunks m n where
constructor MkChunks
{leftMask : Nat}
{rightMask : Nat}
0 left : OPE m (m + n) leftMask
0 right : OPE n (m + n) rightMask
{auto 0 isCover : Cover [left, right]}
%name Chunks chunks
export
chunks : (m, n : Nat) -> Chunks m n
chunks 0 0 = MkChunks Stop Stop
chunks 0 (S n) =
let MkChunks l r = chunks 0 n in
MkChunks (Drop l Refl) (Keep r Refl)
chunks (S m) n =
let MkChunks l r = chunks m n in
MkChunks (Keep l Refl) (Drop r Refl)
-- [todo] the masks here are just ((2 << m) - 1) << n and (2 << n) - 1
public export
record SplitAt m n1 n2 (ope : OPE m (n1 + n2) mask) where
constructor MkSplitAt
{leftMask, rightMask : Nat}
{0 leftScope, rightScope : Nat}
0 left : OPE leftScope n1 leftMask
0 right : OPE rightScope n2 rightMask
0 scopePrf : m = leftScope + rightScope
0 opePrf : ope `Eqv` (left `app'` right).snd
%name SplitAt split
export
splitAt : (n1 : Nat) -> {n2, mask : Nat} -> (0 ope : OPE m (n1 + n2) mask) ->
SplitAt m n1 n2 ope
splitAt 0 ope = MkSplitAt zero ope Refl reflexive
splitAt (S n1) ope with %syntactic (view ope)
splitAt (S n1) (Drop ope Refl) | DropV _ ope with %syntactic (splitAt n1 ope)
_ | MkSplitAt left right scopePrf opePrf =
MkSplitAt (Drop left Refl) right scopePrf (EqvDrop opePrf)
splitAt (S n1) (Keep ope Refl) | KeepV _ ope with %syntactic (splitAt n1 ope)
_ | MkSplitAt left right scopePrf opePrf =
MkSplitAt (Keep left Refl) right (cong S scopePrf) (EqvKeep opePrf)

216
lib/Quox/Thin/Term.idr Normal file
View file

@ -0,0 +1,216 @@
module Quox.Thin.Term
import public Quox.Thin.Base
import public Quox.Thin.Comp
import public Quox.Thin.List
import Quox.Thin.Eqv
import public Quox.Thin.Cover
import Quox.Thin.Append
import Quox.Name
import Quox.Loc
import Data.DPair
import public Data.List.Quantifiers
import Data.Vect
import Data.Singleton
import Decidable.Equality
%default total
private
cmpMask : (m, n : Nat) -> Either Ordering (m = n)
cmpMask 0 0 = Right Refl
cmpMask 0 (S n) = Left LT
cmpMask (S m) 0 = Left GT
cmpMask (S m) (S n) = map (cong S) $ cmpMask m n
public export
record Thinned f n where
constructor Th
{0 scope : Nat}
{scopeMask : Nat}
0 ope : OPE scope n scopeMask
term : f scope
%name Thinned s, t, u
export
(forall n. Eq (f n)) => Eq (Thinned f n) where
s == t = case cmpMask s.scopeMask t.scopeMask of
Left _ => False
Right eq => s.term == (rewrite maskEqInner s.ope t.ope eq in t.term)
export
(forall n. Ord (f n)) => Ord (Thinned f n) where
compare s t = case cmpMask s.scopeMask t.scopeMask of
Left o => o
Right eq => compare s.term (rewrite maskEqInner s.ope t.ope eq in t.term)
export
{n : Nat} -> (forall s. Show (f s)) => Show (Thinned f n) where
showPrec d (Th ope term) =
showCon d "Th" $ showArg (unVal $ maskToOpe ope) ++ showArg term
export
(forall n. Located (f n)) => Located (Thinned f n) where
term.loc = term.term.loc
export
(forall n. Relocatable (f n)) => Relocatable (Thinned f n) where
setLoc loc = {term $= setLoc loc}
namespace Thinned
export
pure : {n : Nat} -> f n -> Thinned f n
pure term = Th id.snd term
export
join : {n : Nat} -> Thinned (Thinned f) n -> Thinned f n
join (Th ope1 (Th ope2 term)) = Th (ope1 . ope2) term
export
weak : {n : Nat} -> (by : Nat) -> Thinned f n -> Thinned f (by + n)
weak by (Th ope term) = Th (zero ++ ope).snd term
public export
record ScopedN (s : Nat) (f : Nat -> Type) (n : Nat) where
constructor S
names : Vect s BindName
{0 scope : Nat}
{mask : Nat}
0 ope : OPE scope s mask
body : f (scope + n)
export
(forall n. Eq (f n)) => Eq (ScopedN s f n) where
s1 == s2 = case decEq s1.mask s2.mask of
Yes eq =>
s1.names == s2.names &&
s1.body == (rewrite maskEqInner s1.ope s2.ope eq in s2.body)
No _ => False
export
{s : Nat} -> (forall n. Show (f n)) => Show (ScopedN s f n) where
showPrec d (S ns ope body) = showCon d "S" $
showArg ns ++ showArg (unVal $ maskToOpe ope) ++ showArg body
public export
Scoped : (Nat -> Type) -> Nat -> Type
Scoped d n = ScopedN 1 d n
(.name) : Scoped f n -> BindName
(S {names = [x], _}).name = x
export
(forall n. Located (f n)) => Located (ScopedN s f n) where
s.loc = s.body.loc
export
(forall n. Relocatable (f n)) => Relocatable (ScopedN s f n) where
setLoc loc = {body $= setLoc loc}
public export
record Thinned2 f d n where
constructor Th2
{0 dscope, tscope : Nat}
{dmask, tmask : Nat}
0 dope : OPE dscope d dmask
0 tope : OPE tscope n tmask
term : f dscope tscope
%name Thinned2 term
export
(forall d, n. Eq (f d n)) => Eq (Thinned2 f d n) where
s == t = case (decEq s.dmask t.dmask, decEq s.tmask t.tmask) of
(Yes deq, Yes teq) =>
s.term == (rewrite maskEqInner s.dope t.dope deq in
rewrite maskEqInner s.tope t.tope teq in t.term)
_ => False
export
{d, n : Nat} -> (forall sd, sn. Show (f sd sn)) => Show (Thinned2 f d n) where
showPrec d (Th2 dope tope term) =
showCon d "Th2" $
showArg (unVal $ maskToOpe dope) ++
showArg (unVal $ maskToOpe tope) ++
showArg term
export
(forall d, n. Located (f d n)) => Located (Thinned2 f d n) where
term.loc = term.term.loc
export
(forall d, n. Relocatable (f d n)) => Relocatable (Thinned2 f d n) where
setLoc loc = {term $= setLoc loc}
namespace Thinned2
export
pure : {d, n : Nat} -> f d n -> Thinned2 f d n
pure term = Th2 id.snd id.snd term
export
join : {d, n : Nat} -> Thinned2 (Thinned2 f) d n -> Thinned2 f d n
join (Th2 dope1 tope1 (Th2 dope2 tope2 term)) =
Th2 (dope1 . dope2) (tope1 . tope2) term
export
weak : {d, n : Nat} -> (dby, nby : Nat) ->
Thinned2 f d n -> Thinned2 f (dby + d) (nby + n)
weak dby nby (Th2 dope tope term) =
Th2 (zero ++ dope).snd (zero ++ tope).snd term
namespace TermList
public export
data Element : (Nat -> Nat -> Type) ->
OPE dscope d dmask -> OPE tscope n tmask -> Type where
T : f dscope tscope ->
{dmask : Nat} -> (0 dope : OPE dscope d dmask) ->
{tmask : Nat} -> (0 tope : OPE tscope n tmask) ->
Element f dope tope
%name TermList.Element s, t, u
export
elementEq : (forall d, n. Eq (f d n)) =>
Element {d, n} f dope1 tope1 -> Element {d, n} f dope2 tope2 ->
Bool
elementEq (T s dope1 tope1 {dmask = dm1, tmask = tm1})
(T t dope2 tope2 {dmask = dm2, tmask = tm2}) =
case (decEq dm1 dm2, decEq tm1 tm2) of
(Yes deq, Yes teq) =>
s == (rewrite maskEqInner dope1 dope2 deq in
rewrite maskEqInner tope1 tope2 teq in t)
_ => False
public export
data TermList : List (Nat -> Nat -> Type) ->
OPEList d -> OPEList n -> Type where
Nil : TermList [] [] []
(::) : Element f dope tope ->
TermList fs dopes topes ->
TermList (f :: fs) (dope :: dopes) (tope :: topes)
%name TermList ss, ts, us
export
termListEq : All (\f => forall d, n. Eq (f d n)) fs =>
TermList {d, n} fs dopes1 topes1 ->
TermList {d, n} fs dopes2 topes2 ->
Bool
termListEq [] [] = True
termListEq (s :: ss) (t :: ts) @{eq :: eqs} =
elementEq s t && termListEq ss ts
public export
record Subterms (fs : List (Nat -> Nat -> Type)) d n where
constructor Sub
{0 dopes : OPEList d}
{0 topes : OPEList n}
terms : TermList fs dopes topes
0 dcov : Cover dopes
0 tcov : Cover topes
%name Subterms ss, ts, us
export
All (\f => forall d, n. Eq (f d n)) fs => Eq (Subterms fs d n) where
ss == ts = ss.terms `termListEq` ts.terms

100
lib/Quox/Thin/View.idr Normal file
View file

@ -0,0 +1,100 @@
module Quox.Thin.View
import public Quox.Thin.Base
import Quox.NatExtra
import Data.Singleton
import Data.SnocVect
import Data.Fin
%default total
public export
data View : OPE m n mask -> Type where
StopV : View Stop
DropV : (mask : Nat) -> (0 ope : OPE m n mask) -> View (Drop ope Refl)
KeepV : (mask : Nat) -> (0 ope : OPE m n mask) -> View (Keep ope Refl)
%name View.View v
private
0 stopEqs : OPE m 0 mask -> (m = 0, mask = 0)
stopEqs Stop = (Refl, Refl)
private
0 fromStop : (ope : OPE 0 0 0) -> ope = Stop
fromStop Stop = Refl
private
0 fromDrop : (ope : OPE m (S n) (k + k)) ->
(inner : OPE m n k ** ope === Drop inner Refl)
fromDrop (Drop ope eq) with %syntactic (doubleInj _ _ eq)
fromDrop (Drop ope Refl) | Refl = (ope ** Refl)
fromDrop (Keep ope eq) = void $ notEvenOdd _ _ eq
private
0 fromKeep : (ope : OPE (S m) (S n) (S (k + k))) ->
(inner : OPE m n k ** ope === Keep inner Refl)
fromKeep (Drop ope eq) = void $ notEvenOdd _ _ $ sym eq
fromKeep (Keep ope eq) with %syntactic (doubleInj _ _ $ inj S eq)
fromKeep (Keep ope Refl) | Refl = (ope ** Refl)
private
0 keepIsSucc : (ope : OPE m n (S (k + k))) -> IsSucc m
keepIsSucc (Drop ope eq) = void $ notEvenOdd _ _ $ sym eq
keepIsSucc (Keep ope _) = ItIsSucc
export
view : {0 m : Nat} -> {n, mask : Nat} -> (0 ope : OPE m n mask) -> View ope
view {n = 0} ope with %syntactic 0 (fst $ stopEqs ope) | 0 (snd $ stopEqs ope)
_ | Refl | Refl = rewrite fromStop ope in StopV
view {n = S n} ope with %syntactic (half mask)
_ | HalfOdd mask' with %syntactic 0 (keepIsSucc ope)
_ | ItIsSucc with %syntactic 0 (fromKeep ope)
_ | (ope' ** eq) = rewrite eq in KeepV mask' ope'
_ | HalfEven mask' with %syntactic 0 (fromDrop ope)
_ | (ope' ** eq) = rewrite eq in DropV mask' ope'
export
(.fin) : {n, mask : Nat} -> (0 ope : OPE 1 n mask) -> Fin n
ope.fin with (view ope)
_.fin | DropV _ ope = FS ope.fin
_.fin | KeepV _ ope = FZ
export
appOpe : {0 m : Nat} -> (n : Nat) -> {mask : Nat} ->
(0 ope : OPE m n mask) -> Singleton m
appOpe n ope with %syntactic (view ope)
appOpe 0 Stop | StopV = Val 0
appOpe (S n) (Drop ope' _) | DropV _ ope' = appOpe n ope'
appOpe (S n) (Keep ope' _) | KeepV _ ope' = [|S $ appOpe n ope'|]
export
maskToOpe : {n, mask : Nat} -> (0 ope : OPE m n mask) -> Singleton ope
maskToOpe ope with %syntactic (view ope)
maskToOpe Stop | StopV = [|Stop|]
maskToOpe (Drop ope Refl) | DropV k ope = [|drop $ maskToOpe ope|]
maskToOpe (Keep ope Refl) | KeepV k ope = [|keep $ maskToOpe ope|]
export
0 outerInnerZero : OPE m 0 mask -> m = 0
outerInnerZero Stop = Refl
export
0 outerMaskZero : OPE m 0 mask -> mask = 0
outerMaskZero Stop = Refl
export
0 viewStop : view Stop = StopV
viewStop = Refl
export
0 viewDrop : (ope : OPE m n mask) -> (eq : mask2 = mask + mask) ->
view (Drop {mask} ope eq) = DropV mask ope
viewDrop ope eq with %syntactic (view (Drop ope eq))
viewDrop ope Refl | DropV _ ope = Refl
export
0 viewKeep : (ope : OPE m n mask) -> (eq : mask2 = S (mask + mask)) ->
view (Keep {mask} ope eq) = KeepV mask ope
viewKeep ope eq with %syntactic (view (Keep ope eq))
viewKeep ope Refl | KeepV _ ope = Refl

13
lib/quox-lib.ipkg
View file

@ -16,8 +16,19 @@ modules =
Quox.Decidable, Quox.Decidable,
Quox.No, Quox.No,
Quox.Loc, Quox.Loc,
Quox.OPE,
Quox.Pretty, Quox.Pretty,
Quox.Thin.Base,
Quox.Thin.View,
Quox.Thin.Eqv,
Quox.Thin.Cons,
Quox.Thin.List,
Quox.Thin.Append,
Quox.Thin.Comp,
Quox.Thin.Cover,
Quox.Thin.Coprod,
Quox.Thin.Split,
Quox.Thin.Term,
Quox.Thin,
Quox.Syntax, Quox.Syntax,
Quox.Syntax.Dim, Quox.Syntax.Dim,
Quox.Syntax.DimEq, Quox.Syntax.DimEq,

13
quox.bib
View file

@ -366,3 +366,16 @@
url = {https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf}, url = {https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf},
doi = {10.1007/s10990-006-0480-6}, doi = {10.1007/s10990-006-0480-6},
} }
@article{egtbs,
doi = {10.4204/eptcs.275.6},
url = {https://doi.org/10.4204%2Feptcs.275.6},
year = 2018,
month = {jul},
publisher = {Open Publishing Association},
volume = {275},
pages = {53--69},
author = {Conor McBride},
title = {Everybody's Got To Be Somewhere},
journal = {Electronic Proceedings in Theoretical Computer Science}
}