Compare commits
5 Commits
820347fc68
...
629434c752
Author | SHA1 | Date |
---|---|---|
rhiannon morris | 629434c752 | |
rhiannon morris | e55ecaf5f6 | |
rhiannon morris | 3506b217b1 | |
rhiannon morris | e1e9ca1b80 | |
rhiannon morris | b98b11b100 |
|
@ -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"
|
||||||
|
|
|
@ -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
|
|
@ -1,9 +1,11 @@
|
||||||
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
|
||||||
|
|
||||||
|
@ -55,3 +57,65 @@ 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
|
||||||
|
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
|
||||||
|
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
|
||||||
|
|
|
@ -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,301 @@ 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 : WithSubst (Term d) (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
|
||| first argument `d` is dimension scope size, second `n` is term scope size
|
||||||
public export %inline
|
public export
|
||||||
SigY : (x : BindName) -> (fst : Term d n) ->
|
data Elim where
|
||||||
(snd : Term d (S n)) -> (loc : Loc) -> Term d n
|
||| free variable, possibly with a displacement (see @crude, or @mugen for a
|
||||||
SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
|
||| more abstract and formalised take)
|
||||||
|
|||
|
||||||
|
||| 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 : WithSubst (Elim d) (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 (Sub 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
|
||||||
|
@ -395,69 +349,40 @@ Located (Term d n) where
|
||||||
(CloT (Sub t _)).loc = t.loc
|
(CloT (Sub 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 (Sub term subst)) = CloE $ Sub (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 (Sub term subst)) = CloT $ Sub (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)
|
|
||||||
|
|
|
@ -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
|
|
@ -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
|
|
@ -0,0 +1,80 @@
|
||||||
|
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' : OPE m m Base.id.fst
|
||||||
|
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
|
||||||
|
{mask : Nat}
|
||||||
|
0 ope : OPE m n mask
|
|
@ -0,0 +1,59 @@
|
||||||
|
module Quox.Thin.Comp
|
||||||
|
|
||||||
|
import public Quox.Thin.Base
|
||||||
|
import public Quox.Thin.View
|
||||||
|
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
|
||||||
|
|
||||||
|
-- export
|
||||||
|
-- 0 compMask : (ope1 : OPE n p mask1) -> (ope2 : OPE m n mask2) ->
|
||||||
|
-- (ope3 : OPE m p mask3) -> Comp ope1 ope2 ope3 ->
|
||||||
|
-- mask3 = ?aaa
|
|
@ -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
|
|
@ -0,0 +1,41 @@
|
||||||
|
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
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
|
public export
|
||||||
|
record Coprod2 (ope1 : OPE m1 n mask1) (ope2 : OPE m2 n mask2) where
|
||||||
|
constructor MkCoprod2
|
||||||
|
{sizeMask : Nat}
|
||||||
|
{leftMask : Nat}
|
||||||
|
{rightMask : Nat}
|
||||||
|
{0 sub : OPE size n sizeMask}
|
||||||
|
{0 left : OPE m1 size leftMask}
|
||||||
|
{0 right : OPE m2 size rightMask}
|
||||||
|
0 leftComp : Comp sub left ope1
|
||||||
|
0 rightComp : Comp sub right ope2
|
||||||
|
{auto 0 isCover : Cover [left, right]}
|
||||||
|
%name Coprod2 cop
|
||||||
|
|
||||||
|
export
|
||||||
|
coprod2 : {n, mask1, mask2 : Nat} ->
|
||||||
|
(0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
|
||||||
|
Coprod2 ope1 ope2
|
||||||
|
coprod2 ope1 ope2 with (view ope1) | (view ope2)
|
||||||
|
coprod2 Stop Stop | StopV | StopV = MkCoprod2 StopZ StopZ
|
||||||
|
coprod2 (Drop ope1 Refl) (Drop ope2 Refl) | DropV _ ope1 | DropV _ ope2 =
|
||||||
|
let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (DropZ l) (DropZ r)
|
||||||
|
coprod2 (Drop ope1 Refl) (Keep ope2 Refl) | DropV _ ope1 | KeepV _ ope2 =
|
||||||
|
let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KDZ l) (KeepZ r)
|
||||||
|
coprod2 (Keep ope1 Refl) (Drop ope2 Refl) | KeepV _ ope1 | DropV _ ope2 =
|
||||||
|
let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KeepZ l) (KDZ r)
|
||||||
|
coprod2 (Keep ope1 Refl) (Keep ope2 Refl) | KeepV _ ope1 | KeepV _ ope2 =
|
||||||
|
let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KeepZ l) (KeepZ r)
|
||||||
|
|
||||||
|
-- [todo] n-ary coprod
|
|
@ -0,0 +1,26 @@
|
||||||
|
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
|
|
@ -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)
|
|
@ -0,0 +1,123 @@
|
||||||
|
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
|
||||||
|
|
||||||
|
export
|
||||||
|
length : OPEList n -> Nat
|
||||||
|
length [] = 0
|
||||||
|
length (_ :: opes) = S $ length opes
|
||||||
|
|
||||||
|
export
|
||||||
|
toList : OPEList n -> List (SomeOPE n)
|
||||||
|
toList [] = []
|
||||||
|
toList (ope :: opes) = MkOPE ope :: toList opes
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
-- [fixme] factor this out probably
|
||||||
|
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}
|
|
@ -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)
|
|
@ -0,0 +1,179 @@
|
||||||
|
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.Name
|
||||||
|
import Quox.Loc
|
||||||
|
import Data.DPair
|
||||||
|
import public Data.List.Quantifiers
|
||||||
|
import Data.Vect
|
||||||
|
import Data.Singleton
|
||||||
|
import Decidable.Equality
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
|
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 decEq s.scopeMask t.scopeMask of
|
||||||
|
Yes eq => s.term == (rewrite maskEqInner s.ope t.ope eq in t.term)
|
||||||
|
No _ => False
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
|
||||||
|
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
|
||||||
|
(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
|
||||||
|
|
||||||
|
|
||||||
|
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
|
|
@ -0,0 +1,76 @@
|
||||||
|
module Quox.Thin.View
|
||||||
|
|
||||||
|
import public Quox.Thin.Base
|
||||||
|
import Quox.NatExtra
|
||||||
|
import Data.Singleton
|
||||||
|
|
||||||
|
%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
|
||||||
|
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
|
|
@ -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,
|
||||||
|
|
Loading…
Reference in New Issue