remove IsQty interface
This commit is contained in:
parent
5fdba77d04
commit
ba2818a865
24 changed files with 729 additions and 889 deletions
|
|
@ -1,91 +1,144 @@
|
|||
||| quantities count how many times a bound variable is used [@nuttin; @qtt].
|
||||
|||
|
||||
||| i tried grtt [@grtt] for a bit but i think it was more complex than
|
||||
||| it's worth in a language that has other stuff going on too
|
||||
module Quox.Syntax.Qty
|
||||
|
||||
import Quox.Pretty
|
||||
import Quox.Name
|
||||
import public Quox.Decidable
|
||||
import Quox.Decidable
|
||||
import Data.DPair
|
||||
import Derive.Prelude
|
||||
|
||||
%default total
|
||||
%language ElabReflection
|
||||
|
||||
|
||||
||| the possibilities we care about are:
|
||||
|||
|
||||
||| - 0: a variable is used only at compile time, not run time
|
||||
||| - 1: a variable is used exactly once at run time
|
||||
||| - ω (or #): don't care. an ω variable *can* also be used 0/1 time
|
||||
public export
|
||||
data Qty = Zero | One | Any
|
||||
%name Qty.Qty pi, rh
|
||||
|
||||
%runElab derive "Qty" [Eq, Ord, Show]
|
||||
|
||||
|
||||
export
|
||||
PrettyHL Qty where
|
||||
prettyM pi = hl Qty <$>
|
||||
case pi of
|
||||
Zero => pure "0"
|
||||
One => pure "1"
|
||||
Any => ifUnicode "ω" "#"
|
||||
|
||||
||| prints in a form that can be a suffix of "case"
|
||||
public export
|
||||
prettySuffix : Pretty.HasEnv m => Qty -> m (Doc HL)
|
||||
prettySuffix = prettyM
|
||||
|
||||
public export
|
||||
interface Eq q => IsQty q where
|
||||
zero, one, any : q
|
||||
DecEq Qty where
|
||||
decEq Zero Zero = Yes Refl
|
||||
decEq Zero One = No $ \case _ impossible
|
||||
decEq Zero Any = No $ \case _ impossible
|
||||
decEq One Zero = No $ \case _ impossible
|
||||
decEq One One = Yes Refl
|
||||
decEq One Any = No $ \case _ impossible
|
||||
decEq Any Zero = No $ \case _ impossible
|
||||
decEq Any One = No $ \case _ impossible
|
||||
decEq Any Any = Yes Refl
|
||||
|
||||
(+), (*) : q -> q -> q
|
||||
lub : q -> q -> Maybe q
|
||||
|
||||
||| true if bindings of this quantity will be erased
|
||||
||| and must not be runtime relevant
|
||||
IsZero : Pred q
|
||||
isZero : Dec1 IsZero
|
||||
zeroIsZero : IsZero zero
|
||||
||| e.g. if in the expression `(s, t)`, the variable `x` is
|
||||
||| used π times in `s` and ρ times in `t`, then it's used
|
||||
||| (π + ρ) times in the whole expression
|
||||
public export
|
||||
(+) : Qty -> Qty -> Qty
|
||||
Zero + rh = rh
|
||||
pi + Zero = pi
|
||||
_ + _ = Any
|
||||
|
||||
||| true if bindings of this quantity can be used any number of times.
|
||||
||| this is needed for natural elimination
|
||||
IsAny : Pred q
|
||||
isAny : Dec1 IsAny
|
||||
anyIsAny : IsAny any
|
||||
||| e.g. if a function `f` uses its argument π times,
|
||||
||| and `f x` occurs in a σ context, then `x` is used `πσ` times overall
|
||||
public export
|
||||
(*) : Qty -> Qty -> Qty
|
||||
Zero * _ = Zero
|
||||
_ * Zero = Zero
|
||||
One * rh = rh
|
||||
pi * One = pi
|
||||
Any * Any = Any
|
||||
|
||||
||| ``p `Compat` q`` if it is ok for a binding of quantity `q` to be used
|
||||
||| exactly `p` times. e.g. ``1 `Compat` 1``, ``1 `Compat` ω``.
|
||||
||| if ``π `lub` ρ`` exists, then both `π` and `ρ` must be compatible with it
|
||||
Compat : Rel q
|
||||
compat : Dec2 Compat
|
||||
||| "π ≤ ρ"
|
||||
|||
|
||||
||| if a variable is bound with quantity ρ, then it can be used with a total
|
||||
||| quantity π as long as π ≤ ρ. for example, an ω variable can be used any
|
||||
||| number of times, so π ≤ ω for any π.
|
||||
public export
|
||||
compat : Qty -> Qty -> Bool
|
||||
compat pi Any = True
|
||||
compat pi rh = pi == rh
|
||||
|
||||
||| true if it is ok for this quantity to appear for the
|
||||
||| subject of a typing judgement [@qtt, §2.3].
|
||||
IsSubj : Pred q
|
||||
isSubj : Dec1 IsSubj
|
||||
zeroIsSubj : forall pi. IsZero pi -> IsSubj pi
|
||||
oneIsSubj : IsSubj one
|
||||
timesSubj : forall pi, rh. IsSubj pi -> IsSubj rh -> IsSubj (pi * rh)
|
||||
|
||||
||| true if it is ok for a global definition to have this
|
||||
||| quantity. so not exact usage counts, maybe.
|
||||
IsGlobal : Pred q
|
||||
isGlobal : Dec1 IsGlobal
|
||||
zeroIsGlobal : forall pi. IsZero pi -> IsGlobal pi
|
||||
anyIsGlobal : forall pi. IsAny pi -> IsGlobal pi
|
||||
||| "π ∧ ρ"
|
||||
|||
|
||||
||| returns some quantity τ where π ≤ τ and ρ ≤ τ, if one exists.
|
||||
public export
|
||||
lub : Qty -> Qty -> Maybe Qty
|
||||
lub p q =
|
||||
if p == Any || q == Any then Just Any
|
||||
else if p == q then Just p
|
||||
else Nothing
|
||||
|
||||
||| prints in a form that can be a suffix of "case"
|
||||
prettySuffix : Pretty.HasEnv m => q -> m (Doc HL)
|
||||
|
||||
||| to maintain subject reduction, only 0 or 1 can occur
|
||||
||| for the subject of a typing judgment. see @qtt, §2.3 for more detail
|
||||
public export
|
||||
isSubj : Qty -> Bool
|
||||
isSubj Zero = True
|
||||
isSubj One = True
|
||||
isSubj Any = False
|
||||
|
||||
public export
|
||||
0 SQty : (q : Type) -> IsQty q => Type
|
||||
SQty q = Subset q IsSubj
|
||||
SQty : Type
|
||||
SQty = Subset Qty $ So . isSubj
|
||||
|
||||
public export %inline
|
||||
szero : IsQty q => SQty q
|
||||
szero = Element zero $ zeroIsSubj zeroIsZero
|
||||
|
||||
public export %inline
|
||||
sone : IsQty q => SQty q
|
||||
sone = Element one oneIsSubj
|
||||
szero, sone : SQty
|
||||
szero = Element Zero Oh
|
||||
sone = Element One Oh
|
||||
|
||||
||| "σ ⨴ π"
|
||||
|||
|
||||
||| ``sg `subjMult` pi`` is equal to `pi` if it is zero, otherwise it
|
||||
||| is equal to `sg`.
|
||||
public export %inline
|
||||
subjMult : IsQty q => SQty q -> q -> SQty q
|
||||
subjMult sg pi = case isZero pi of
|
||||
Yes y => Element pi $ zeroIsSubj y
|
||||
No _ => sg
|
||||
||| σ ⨭ π is 0 if either of σ or π are, otherwise it is σ.
|
||||
public export
|
||||
subjMult : SQty -> Qty -> SQty
|
||||
subjMult _ Zero = szero
|
||||
subjMult sg _ = sg
|
||||
|
||||
|
||||
||| it doesn't make much sense for a top level declaration to have a
|
||||
||| quantity of 1, so the only distinction is whether it is present
|
||||
||| at runtime at all or not
|
||||
public export
|
||||
isGlobal : Qty -> Bool
|
||||
isGlobal Zero = True
|
||||
isGlobal One = False
|
||||
isGlobal Any = True
|
||||
|
||||
public export
|
||||
0 GQty : (q : Type) -> IsQty q => Type
|
||||
GQty q = Subset q IsGlobal
|
||||
GQty : Type
|
||||
GQty = Subset Qty $ So . isGlobal
|
||||
|
||||
public export
|
||||
gzero, gany : GQty
|
||||
gzero = Element Zero Oh
|
||||
gany = Element Any Oh
|
||||
|
||||
||| when checking a definition, a 0 definition is checked at 0,
|
||||
||| but an ω definition is checked at 1 since ω isn't a subject quantity
|
||||
public export %inline
|
||||
gzero : IsQty q => GQty q
|
||||
gzero = Element zero $ zeroIsGlobal zeroIsZero
|
||||
|
||||
public export %inline
|
||||
gany : IsQty q => GQty q
|
||||
gany = Element any $ anyIsGlobal anyIsAny
|
||||
|
||||
export %inline
|
||||
globalToSubj : IsQty q => GQty q -> SQty q
|
||||
globalToSubj q = if isYes $ isZero q.fst then szero else sone
|
||||
globalToSubj : GQty -> SQty
|
||||
globalToSubj (Element Zero _) = szero
|
||||
globalToSubj (Element Any _) = sone
|
||||
|
|
|
|||
|
|
@ -1,143 +0,0 @@
|
|||
module Quox.Syntax.Qty.Three
|
||||
|
||||
import Quox.Pretty
|
||||
import public Quox.Syntax.Qty
|
||||
import Derive.Prelude
|
||||
|
||||
%default total
|
||||
%language ElabReflection
|
||||
|
||||
|
||||
public export
|
||||
data Three = Zero | One | Any
|
||||
%name Three pi, rh
|
||||
|
||||
%runElab derive "Three" [Eq, Ord, Show]
|
||||
|
||||
|
||||
export
|
||||
PrettyHL Three where
|
||||
prettyM pi = hl Qty <$>
|
||||
case pi of
|
||||
Zero => pure "0"
|
||||
One => pure "1"
|
||||
Any => ifUnicode "ω" "#"
|
||||
|
||||
public export
|
||||
DecEq Three where
|
||||
decEq Zero Zero = Yes Refl
|
||||
decEq Zero One = No $ \case _ impossible
|
||||
decEq Zero Any = No $ \case _ impossible
|
||||
decEq One Zero = No $ \case _ impossible
|
||||
decEq One One = Yes Refl
|
||||
decEq One Any = No $ \case _ impossible
|
||||
decEq Any Zero = No $ \case _ impossible
|
||||
decEq Any One = No $ \case _ impossible
|
||||
decEq Any Any = Yes Refl
|
||||
|
||||
|
||||
public export
|
||||
plus : Three -> Three -> Three
|
||||
plus Zero rh = rh
|
||||
plus pi Zero = pi
|
||||
plus _ _ = Any
|
||||
|
||||
public export
|
||||
times : Three -> Three -> Three
|
||||
times Zero _ = Zero
|
||||
times _ Zero = Zero
|
||||
times One rh = rh
|
||||
times pi One = pi
|
||||
times Any Any = Any
|
||||
|
||||
public export
|
||||
lub3 : Three -> Three -> Maybe Three
|
||||
lub3 p q =
|
||||
if p == Any || q == Any then Just Any
|
||||
else if p == q then Just p
|
||||
else Nothing
|
||||
|
||||
public export
|
||||
data Compat3 : Rel Three where
|
||||
CmpRefl : Compat3 rh rh
|
||||
CmpAny : Compat3 rh Any
|
||||
|
||||
public export
|
||||
compat3 : Dec2 Compat3
|
||||
compat3 pi rh with (decEq pi rh) | (decEq rh Any)
|
||||
compat3 pi pi | Yes Refl | _ = Yes CmpRefl
|
||||
compat3 pi Any | No _ | Yes Refl = Yes CmpAny
|
||||
compat3 pi rh | No ne | No na =
|
||||
No $ \case CmpRefl => ne Refl; CmpAny => na Refl
|
||||
|
||||
|
||||
public export
|
||||
data IsSubj3 : Pred Three where
|
||||
SZero : IsSubj3 Zero
|
||||
SOne : IsSubj3 One
|
||||
|
||||
public export
|
||||
isSubj3 : Dec1 IsSubj3
|
||||
isSubj3 Zero = Yes SZero
|
||||
isSubj3 One = Yes SOne
|
||||
isSubj3 Any = No $ \case _ impossible
|
||||
|
||||
public export
|
||||
timesSubj3 : forall pi, rh. IsSubj3 pi -> IsSubj3 rh -> IsSubj3 (times pi rh)
|
||||
timesSubj3 SZero SZero = SZero
|
||||
timesSubj3 SZero SOne = SZero
|
||||
timesSubj3 SOne SZero = SZero
|
||||
timesSubj3 SOne SOne = SOne
|
||||
|
||||
|
||||
public export
|
||||
data IsGlobal3 : Pred Three where
|
||||
GZero : IsGlobal3 Zero
|
||||
GAny : IsGlobal3 Any
|
||||
|
||||
public export
|
||||
isGlobal3 : Dec1 IsGlobal3
|
||||
isGlobal3 Zero = Yes GZero
|
||||
isGlobal3 One = No $ \case _ impossible
|
||||
isGlobal3 Any = Yes GAny
|
||||
|
||||
|
||||
public export
|
||||
IsQty Three where
|
||||
zero = Zero
|
||||
one = One
|
||||
any = Any
|
||||
|
||||
(+) = plus
|
||||
(*) = times
|
||||
|
||||
lub = lub3
|
||||
|
||||
IsZero = Equal Zero
|
||||
isZero = decEq Zero
|
||||
zeroIsZero = Refl
|
||||
|
||||
IsAny = Equal Three.Any
|
||||
isAny = decEq Any
|
||||
anyIsAny = Refl
|
||||
|
||||
Compat = Compat3
|
||||
compat = compat3
|
||||
|
||||
IsSubj = IsSubj3
|
||||
isSubj = isSubj3
|
||||
zeroIsSubj = \Refl => SZero
|
||||
oneIsSubj = SOne
|
||||
timesSubj = timesSubj3
|
||||
|
||||
IsGlobal = IsGlobal3
|
||||
isGlobal = isGlobal3
|
||||
zeroIsGlobal = \Refl => GZero
|
||||
anyIsGlobal = \Refl => GAny
|
||||
|
||||
prettySuffix = pretty0M
|
||||
|
||||
|
||||
export Uninhabited (IsGlobal3 One) where uninhabited _ impossible
|
||||
|
||||
export Uninhabited (IsSubj3 Any) where uninhabited _ impossible
|
||||
|
|
@ -7,7 +7,6 @@ import public Quox.Syntax.Qty
|
|||
import public Quox.Syntax.Dim
|
||||
import public Quox.Name
|
||||
import public Quox.Context
|
||||
-- import public Quox.OPE
|
||||
|
||||
import Quox.Pretty
|
||||
|
||||
|
|
@ -25,11 +24,11 @@ import public Data.SortedSet
|
|||
|
||||
public export
|
||||
0 TermLike : Type
|
||||
TermLike = Type -> Nat -> Nat -> Type
|
||||
TermLike = Nat -> Nat -> Type
|
||||
|
||||
public export
|
||||
0 TSubstLike : Type
|
||||
TSubstLike = Type -> Nat -> Nat -> Nat -> Type
|
||||
TSubstLike = Nat -> Nat -> Nat -> Type
|
||||
|
||||
public export
|
||||
0 Universe : Type
|
||||
|
|
@ -44,112 +43,111 @@ infixl 9 :@, :%
|
|||
mutual
|
||||
public export
|
||||
0 TSubst : TSubstLike
|
||||
TSubst q d = Subst $ Elim q d
|
||||
TSubst d = Subst $ Elim d
|
||||
|
||||
||| first argument `q` is quantity type;
|
||||
||| second argument `d` is dimension scope size;
|
||||
||| third `n` is term scope size
|
||||
||| first argument `d` is dimension scope size;
|
||||
||| second `n` is term scope size
|
||||
public export
|
||||
data Term : TermLike where
|
||||
||| type of types
|
||||
TYPE : (l : Universe) -> Term q d n
|
||||
TYPE : (l : Universe) -> Term d n
|
||||
|
||||
||| function type
|
||||
Pi : (qty : q) -> (arg : Term q d n) ->
|
||||
(res : ScopeTerm q d n) -> Term q d n
|
||||
Pi : (qty : Qty) -> (arg : Term d n) ->
|
||||
(res : ScopeTerm d n) -> Term d n
|
||||
||| function term
|
||||
Lam : (body : ScopeTerm q d n) -> Term q d n
|
||||
Lam : (body : ScopeTerm d n) -> Term d n
|
||||
|
||||
||| pair type
|
||||
Sig : (fst : Term q d n) -> (snd : ScopeTerm q d n) -> Term q d n
|
||||
Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> Term d n
|
||||
||| pair value
|
||||
Pair : (fst, snd : Term q d n) -> Term q d n
|
||||
Pair : (fst, snd : Term d n) -> Term d n
|
||||
|
||||
||| enumeration type
|
||||
Enum : (cases : SortedSet TagVal) -> Term q d n
|
||||
Enum : (cases : SortedSet TagVal) -> Term d n
|
||||
||| enumeration value
|
||||
Tag : (tag : TagVal) -> Term q d n
|
||||
Tag : (tag : TagVal) -> Term d n
|
||||
|
||||
||| equality type
|
||||
Eq : (ty : DScopeTerm q d n) -> (l, r : Term q d n) -> Term q d n
|
||||
Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> Term d n
|
||||
||| equality term
|
||||
DLam : (body : DScopeTerm q d n) -> Term q d n
|
||||
DLam : (body : DScopeTerm d n) -> Term d n
|
||||
|
||||
||| natural numbers (temporary until 𝐖 gets added)
|
||||
Nat : Term q d n
|
||||
Nat : Term d n
|
||||
-- [todo] can these be elims?
|
||||
Zero : Term q d n
|
||||
Succ : (p : Term q d n) -> Term q d n
|
||||
Zero : Term d n
|
||||
Succ : (p : Term d n) -> Term d n
|
||||
|
||||
||| "box" (package a value up with a certain quantity)
|
||||
BOX : (qty : q) -> (ty : Term q d n) -> Term q d n
|
||||
Box : (val : Term q d n) -> Term q d n
|
||||
BOX : (qty : Qty) -> (ty : Term d n) -> Term d n
|
||||
Box : (val : Term d n) -> Term d n
|
||||
|
||||
||| elimination
|
||||
E : (e : Elim q d n) -> Term q d n
|
||||
E : (e : Elim d n) -> Term d n
|
||||
|
||||
||| term closure/suspended substitution
|
||||
CloT : (tm : Term q d from) -> (th : Lazy (TSubst q d from to)) ->
|
||||
Term q d to
|
||||
CloT : (tm : Term d from) -> (th : Lazy (TSubst d from to)) ->
|
||||
Term d to
|
||||
||| dimension closure/suspended substitution
|
||||
DCloT : (tm : Term q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
|
||||
Term q dto n
|
||||
DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
|
||||
Term dto n
|
||||
|
||||
||| first argument `d` is dimension scope size, second `n` is term scope size
|
||||
public export
|
||||
data Elim : TermLike where
|
||||
||| free variable
|
||||
F : (x : Name) -> Elim q d n
|
||||
F : (x : Name) -> Elim d n
|
||||
||| bound variable
|
||||
B : (i : Var n) -> Elim q d n
|
||||
B : (i : Var n) -> Elim d n
|
||||
|
||||
||| term application
|
||||
(:@) : (fun : Elim q d n) -> (arg : Term q d n) -> Elim q d n
|
||||
(:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
|
||||
|
||||
||| pair destruction
|
||||
|||
|
||||
||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
|
||||
||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
|
||||
CasePair : (qty : q) -> (pair : Elim q d n) ->
|
||||
(ret : ScopeTerm q d n) ->
|
||||
(body : ScopeTermN 2 q d n) ->
|
||||
Elim q d n
|
||||
CasePair : (qty : Qty) -> (pair : Elim d n) ->
|
||||
(ret : ScopeTerm d n) ->
|
||||
(body : ScopeTermN 2 d n) ->
|
||||
Elim d n
|
||||
|
||||
||| enum matching
|
||||
CaseEnum : (qty : q) -> (tag : Elim q d n) ->
|
||||
(ret : ScopeTerm q d n) ->
|
||||
(arms : CaseEnumArms q d n) ->
|
||||
Elim q d n
|
||||
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
|
||||
(ret : ScopeTerm d n) ->
|
||||
(arms : CaseEnumArms d n) ->
|
||||
Elim d n
|
||||
|
||||
||| nat matching
|
||||
CaseNat : (qty, qtyIH : q) -> (nat : Elim q d n) ->
|
||||
(ret : ScopeTerm q d n) ->
|
||||
(zero : Term q d n) ->
|
||||
(succ : ScopeTermN 2 q d n) ->
|
||||
Elim q d n
|
||||
CaseNat : (qty, qtyIH : Qty) -> (nat : Elim d n) ->
|
||||
(ret : ScopeTerm d n) ->
|
||||
(zero : Term d n) ->
|
||||
(succ : ScopeTermN 2 d n) ->
|
||||
Elim d n
|
||||
|
||||
||| unboxing
|
||||
CaseBox : (qty : q) -> (box : Elim q d n) ->
|
||||
(ret : ScopeTerm q d n) ->
|
||||
(body : ScopeTerm q d n) ->
|
||||
Elim q d n
|
||||
CaseBox : (qty : Qty) -> (box : Elim d n) ->
|
||||
(ret : ScopeTerm d n) ->
|
||||
(body : ScopeTerm d n) ->
|
||||
Elim d n
|
||||
|
||||
||| dim application
|
||||
(:%) : (fun : Elim q d n) -> (arg : Dim d) -> Elim q d n
|
||||
(:%) : (fun : Elim d n) -> (arg : Dim d) -> Elim d n
|
||||
|
||||
||| type-annotated term
|
||||
(:#) : (tm, ty : Term q d n) -> Elim q d n
|
||||
(:#) : (tm, ty : Term d n) -> Elim d n
|
||||
|
||||
||| term closure/suspended substitution
|
||||
CloE : (el : Elim q d from) -> (th : Lazy (TSubst q d from to)) ->
|
||||
Elim q d to
|
||||
CloE : (el : Elim d from) -> (th : Lazy (TSubst d from to)) ->
|
||||
Elim d to
|
||||
||| dimension closure/suspended substitution
|
||||
DCloE : (el : Elim q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
|
||||
Elim q dto n
|
||||
DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
|
||||
Elim dto n
|
||||
|
||||
public export
|
||||
0 CaseEnumArms : TermLike
|
||||
CaseEnumArms q d n = SortedMap TagVal (Term q d n)
|
||||
CaseEnumArms d n = SortedMap TagVal (Term d n)
|
||||
|
||||
||| a scoped term with names
|
||||
public export
|
||||
|
|
@ -165,8 +163,8 @@ mutual
|
|||
|
||||
public export
|
||||
0 ScopeTermN, DScopeTermN : Nat -> TermLike
|
||||
ScopeTermN s q d n = Scoped s (Term q d) n
|
||||
DScopeTermN s q d n = Scoped s (\d => Term q d n) d
|
||||
ScopeTermN s d n = Scoped s (Term d) n
|
||||
DScopeTermN s d n = Scoped s (\d => Term d n) d
|
||||
|
||||
public export
|
||||
0 ScopeTerm, DScopeTerm : TermLike
|
||||
|
|
@ -198,58 +196,58 @@ s.name = name s
|
|||
|
||||
||| more convenient Pi
|
||||
public export %inline
|
||||
Pi_ : (qty : q) -> (x : BaseName) ->
|
||||
(arg : Term q d n) -> (res : Term q d (S n)) -> Term q d n
|
||||
Pi_ : (qty : Qty) -> (x : BaseName) ->
|
||||
(arg : Term d n) -> (res : Term d (S n)) -> Term d n
|
||||
Pi_ {qty, x, arg, res} = Pi {qty, arg, res = S [< x] $ Y res}
|
||||
|
||||
||| non dependent function type
|
||||
public export %inline
|
||||
Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n
|
||||
Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
|
||||
Arr {qty, arg, res} = Pi {qty, arg, res = SN res}
|
||||
|
||||
||| more convenient Sig
|
||||
public export %inline
|
||||
Sig_ : (x : BaseName) -> (fst : Term q d n) ->
|
||||
(snd : Term q d (S n)) -> Term q d n
|
||||
Sig_ : (x : BaseName) -> (fst : Term d n) ->
|
||||
(snd : Term d (S n)) -> Term d n
|
||||
Sig_ {x, fst, snd} = Sig {fst, snd = S [< x] $ Y snd}
|
||||
|
||||
||| non dependent pair type
|
||||
public export %inline
|
||||
And : (fst, snd : Term q d n) -> Term q d n
|
||||
And : (fst, snd : Term d n) -> Term d n
|
||||
And {fst, snd} = Sig {fst, snd = SN snd}
|
||||
|
||||
||| more convenient Eq
|
||||
public export %inline
|
||||
Eq_ : (i : BaseName) -> (ty : Term q (S d) n) ->
|
||||
(l, r : Term q d n) -> Term q d n
|
||||
Eq_ : (i : BaseName) -> (ty : Term (S d) n) ->
|
||||
(l, r : Term d n) -> Term d n
|
||||
Eq_ {i, ty, l, r} = Eq {ty = S [< i] $ Y ty, l, r}
|
||||
|
||||
||| non dependent equality type
|
||||
public export %inline
|
||||
Eq0 : (ty, l, r : Term q d n) -> Term q d n
|
||||
Eq0 : (ty, l, r : Term d n) -> Term d n
|
||||
Eq0 {ty, l, r} = Eq {ty = SN ty, l, r}
|
||||
|
||||
||| same as `F` but as a term
|
||||
public export %inline
|
||||
FT : Name -> Term q d n
|
||||
FT : Name -> Term d n
|
||||
FT = E . F
|
||||
|
||||
||| abbreviation for a bound variable like `BV 4` instead of
|
||||
||| `B (VS (VS (VS (VS VZ))))`
|
||||
public export %inline
|
||||
BV : (i : Nat) -> (0 _ : LT i n) => Elim q d n
|
||||
BV : (i : Nat) -> (0 _ : LT i n) => Elim d n
|
||||
BV i = B $ V i
|
||||
|
||||
||| same as `BV` but as a term
|
||||
public export %inline
|
||||
BVT : (i : Nat) -> (0 _ : LT i n) => Term q d n
|
||||
BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
|
||||
BVT i = E $ BV i
|
||||
|
||||
public export
|
||||
makeNat : Nat -> Term q d n
|
||||
makeNat : Nat -> Term d n
|
||||
makeNat 0 = Zero
|
||||
makeNat (S k) = Succ $ makeNat k
|
||||
|
||||
public export
|
||||
enum : List TagVal -> Term q d n
|
||||
enum : List TagVal -> Term d n
|
||||
enum = Enum . SortedSet.fromList
|
||||
|
|
|
|||
|
|
@ -54,10 +54,10 @@ prettyUniverse = hl Syntax . pretty
|
|||
|
||||
|
||||
public export
|
||||
data WithQty q a = MkWithQty q a
|
||||
data WithQty a = MkWithQty Qty a
|
||||
|
||||
export
|
||||
PrettyHL q => PrettyHL a => PrettyHL (WithQty q a) where
|
||||
PrettyHL a => PrettyHL (WithQty a) where
|
||||
prettyM (MkWithQty q x) = do
|
||||
q <- pretty0M q
|
||||
x <- withPrec Arg $ prettyM x
|
||||
|
|
@ -76,9 +76,9 @@ PrettyHL a => PrettyHL (Binder a) where
|
|||
|
||||
|
||||
export
|
||||
prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q =>
|
||||
prettyBindType : PrettyHL a => PrettyHL b =>
|
||||
Pretty.HasEnv m =>
|
||||
Maybe q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
|
||||
Maybe Qty -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
|
||||
prettyBindType q x s arr t = do
|
||||
bind <- case q of
|
||||
Nothing => pretty0M $ MkBinder x s
|
||||
|
|
@ -128,9 +128,9 @@ prettyArms =
|
|||
traverse (\(xs, l, r) => prettyArm T xs l r)
|
||||
|
||||
export
|
||||
prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => IsQty q =>
|
||||
Pretty.HasEnv m =>
|
||||
q -> a -> BaseName -> b -> List (SnocList BaseName, Doc HL, c) ->
|
||||
prettyCase : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
|
||||
Qty -> a -> BaseName -> b ->
|
||||
List (SnocList BaseName, Doc HL, c) ->
|
||||
m (Doc HL)
|
||||
prettyCase pi elim r ret arms = do
|
||||
caseq <- (caseD <+>) <$> prettySuffix pi
|
||||
|
|
@ -167,20 +167,20 @@ prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
|
|||
prettyBoxVal val = bracks <$> pretty0M val
|
||||
|
||||
export
|
||||
toNatLit : Term q d n -> Maybe Nat
|
||||
toNatLit : Term d n -> Maybe Nat
|
||||
toNatLit Zero = Just 0
|
||||
toNatLit (Succ n) = [|S $ toNatLit n|]
|
||||
toNatLit _ = Nothing
|
||||
|
||||
private
|
||||
eterm : Term q d n -> Exists (Term q d)
|
||||
eterm : Term d n -> Exists (Term d)
|
||||
eterm = Evidence n
|
||||
|
||||
|
||||
parameters (showSubsts : Bool)
|
||||
mutual
|
||||
export covering
|
||||
[TermSubst] IsQty q => PrettyHL q => PrettyHL (Term q d n) using ElimSubst
|
||||
[TermSubst] PrettyHL (Term d n) using ElimSubst
|
||||
where
|
||||
prettyM (TYPE l) =
|
||||
parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
|
||||
|
|
@ -198,7 +198,7 @@ parameters (showSubsts : Bool)
|
|||
t <- withPrec Times $ prettyM t
|
||||
parensIfM Times $ asep [s <++> !timesD, t]
|
||||
prettyM (Sig s (S [< x] (Y t))) =
|
||||
prettyBindType {q} Nothing x s !timesD t
|
||||
prettyBindType Nothing x s !timesD t
|
||||
prettyM (Pair s t) =
|
||||
let GotPairs {init, last, _} = getPairs' [< s] t in
|
||||
prettyTuple $ toList $ init :< last
|
||||
|
|
@ -248,7 +248,7 @@ parameters (showSubsts : Bool)
|
|||
prettyM $ pushSubstsWith' th id s
|
||||
|
||||
export covering
|
||||
[ElimSubst] IsQty q => PrettyHL q => PrettyHL (Elim q d n) using TermSubst
|
||||
[ElimSubst] PrettyHL (Elim d n) using TermSubst
|
||||
where
|
||||
prettyM (F x) =
|
||||
hl' Free <$> prettyM x
|
||||
|
|
@ -297,23 +297,20 @@ parameters (showSubsts : Bool)
|
|||
prettyM $ pushSubstsWith' th id e
|
||||
|
||||
export covering
|
||||
prettyTSubst : Pretty.HasEnv m => IsQty q => PrettyHL q =>
|
||||
TSubst q d from to -> m (Doc HL)
|
||||
prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
|
||||
prettyTSubst s =
|
||||
prettySubstM (prettyM @{ElimSubst}) (!ask).tnames TVar "[" "]" s
|
||||
|
||||
export covering %inline
|
||||
IsQty q => PrettyHL q => PrettyHL (Term q d n) where
|
||||
prettyM = prettyM @{TermSubst False}
|
||||
PrettyHL (Term d n) where prettyM = prettyM @{TermSubst False}
|
||||
|
||||
export covering %inline
|
||||
IsQty q => PrettyHL q => PrettyHL (Elim q d n) where
|
||||
prettyM = prettyM @{ElimSubst False}
|
||||
PrettyHL (Elim d n) where prettyM = prettyM @{ElimSubst False}
|
||||
|
||||
|
||||
export covering
|
||||
prettyTerm : IsQty q => PrettyHL q => (unicode : Bool) ->
|
||||
prettyTerm : (unicode : Bool) ->
|
||||
(dnames : NContext d) -> (tnames : NContext n) ->
|
||||
Term q d n -> Doc HL
|
||||
Term d n -> Doc HL
|
||||
prettyTerm unicode dnames tnames term =
|
||||
pretty0With unicode (toSnocList' dnames) (toSnocList' tnames) term
|
||||
|
|
|
|||
|
|
@ -63,26 +63,26 @@ NotDApp = No . isDApp
|
|||
infixl 9 :@@
|
||||
||| apply multiple arguments at once
|
||||
public export %inline
|
||||
(:@@) : Elim q d n -> List (Term q d n) -> Elim q d n
|
||||
(:@@) : Elim d n -> List (Term d n) -> Elim d n
|
||||
f :@@ ss = foldl (:@) f ss
|
||||
|
||||
public export
|
||||
record GetArgs q d n where
|
||||
record GetArgs d n where
|
||||
constructor GotArgs
|
||||
fun : Elim q d n
|
||||
args : List (Term q d n)
|
||||
fun : Elim d n
|
||||
args : List (Term d n)
|
||||
0 notApp : NotApp fun
|
||||
|
||||
mutual
|
||||
export %inline
|
||||
getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
|
||||
getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
|
||||
getArgs' fun0 args =
|
||||
let Element fun nc = pushSubsts fun0 in
|
||||
getArgsNc (assert_smaller fun0 fun) args
|
||||
|
||||
private
|
||||
getArgsNc : (e : Elim q d n) -> (0 nc : NotClo e) =>
|
||||
List (Term q d n) -> GetArgs q d n
|
||||
getArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
|
||||
List (Term d n) -> GetArgs d n
|
||||
getArgsNc fun args = case nchoose $ isApp fun of
|
||||
Left y => let f :@ a = fun in getArgs' f (a :: args)
|
||||
Right n => GotArgs {fun, args, notApp = n}
|
||||
|
|
@ -91,33 +91,33 @@ mutual
|
|||
||| application then the list is just empty.
|
||||
||| looks through substitutions for applications.
|
||||
export %inline
|
||||
getArgs : Elim q d n -> GetArgs q d n
|
||||
getArgs : Elim d n -> GetArgs d n
|
||||
getArgs e = getArgs' e []
|
||||
|
||||
|
||||
infixl 9 :%%
|
||||
||| apply multiple dimension arguments at once
|
||||
public export %inline
|
||||
(:%%) : Elim q d n -> List (Dim d) -> Elim q d n
|
||||
(:%%) : Elim d n -> List (Dim d) -> Elim d n
|
||||
f :%% ss = foldl (:%) f ss
|
||||
|
||||
public export
|
||||
record GetDArgs q d n where
|
||||
record GetDArgs d n where
|
||||
constructor GotDArgs
|
||||
fun : Elim q d n
|
||||
fun : Elim d n
|
||||
args : List (Dim d)
|
||||
0 notDApp : NotDApp fun
|
||||
|
||||
mutual
|
||||
export %inline
|
||||
getDArgs' : Elim q d n -> List (Dim d) -> GetDArgs q d n
|
||||
getDArgs' : Elim d n -> List (Dim d) -> GetDArgs d n
|
||||
getDArgs' fun0 args =
|
||||
let Element fun nc = pushSubsts fun0 in
|
||||
getDArgsNc (assert_smaller fun0 fun) args
|
||||
|
||||
private
|
||||
getDArgsNc : (e : Elim q d n) -> (0 nc : NotClo e) =>
|
||||
List (Dim d) -> GetDArgs q d n
|
||||
getDArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
|
||||
List (Dim d) -> GetDArgs d n
|
||||
getDArgsNc fun args = case nchoose $ isDApp fun of
|
||||
Left y => let f :% d = fun in getDArgs' f (d :: args)
|
||||
Right n => GotDArgs {fun, args, notDApp = n}
|
||||
|
|
@ -125,46 +125,46 @@ mutual
|
|||
||| splits a dimension application into its head and arguments. if it's not an
|
||||
||| d application then the list is just empty
|
||||
export %inline
|
||||
getDArgs : Elim q d n -> GetDArgs q d n
|
||||
getDArgs : Elim d n -> GetDArgs d n
|
||||
getDArgs e = getDArgs' e []
|
||||
|
||||
|
||||
infixr 1 :\\
|
||||
public export
|
||||
absN : NContext m -> Term q d (m + n) -> Term q d n
|
||||
absN : NContext m -> Term d (m + n) -> Term d n
|
||||
absN [<] s = s
|
||||
absN (xs :< x) s = absN xs $ Lam $ SY [< x] s
|
||||
|
||||
public export %inline
|
||||
(:\\) : NContext m -> Term q d (m + n) -> Term q d n
|
||||
(:\\) : NContext m -> Term d (m + n) -> Term d n
|
||||
(:\\) = absN
|
||||
|
||||
|
||||
infixr 1 :\\%
|
||||
public export
|
||||
dabsN : NContext m -> Term q (m + d) n -> Term q d n
|
||||
dabsN : NContext m -> Term (m + d) n -> Term d n
|
||||
dabsN [<] s = s
|
||||
dabsN (xs :< x) s = dabsN xs $ DLam $ SY [< x] s
|
||||
|
||||
public export %inline
|
||||
(:\\%) : NContext m -> Term q (m + d) n -> Term q d n
|
||||
(:\\%) : NContext m -> Term (m + d) n -> Term d n
|
||||
(:\\%) = dabsN
|
||||
|
||||
|
||||
public export
|
||||
record GetLams q d n where
|
||||
record GetLams d n where
|
||||
constructor GotLams
|
||||
{0 lams, rest : Nat}
|
||||
names : NContext lams
|
||||
body : Term q d rest
|
||||
body : Term d rest
|
||||
0 eq : lams + n = rest
|
||||
0 notLam : NotLam body
|
||||
|
||||
mutual
|
||||
export %inline
|
||||
getLams' : forall lams, rest.
|
||||
NContext lams -> Term q d rest -> (0 eq : lams + n = rest) ->
|
||||
GetLams q d n
|
||||
NContext lams -> Term d rest -> (0 eq : lams + n = rest) ->
|
||||
GetLams d n
|
||||
getLams' xs s0 eq =
|
||||
let Element s nc = pushSubsts s0 in
|
||||
getLamsNc xs (assert_smaller s0 s) eq
|
||||
|
|
@ -172,33 +172,33 @@ mutual
|
|||
private
|
||||
getLamsNc : forall lams, rest.
|
||||
NContext lams ->
|
||||
(t : Term q d rest) -> (0 nc : NotClo t) =>
|
||||
(t : Term d rest) -> (0 nc : NotClo t) =>
|
||||
(0 eq : lams + n = rest) ->
|
||||
GetLams q d n
|
||||
GetLams d n
|
||||
getLamsNc xs s Refl = case nchoose $ isLam s of
|
||||
Left y => let Lam (S [< x] body) = s in
|
||||
getLams' (xs :< x) (assert_smaller s body.term) Refl
|
||||
Right n => GotLams xs s Refl n
|
||||
|
||||
export %inline
|
||||
getLams : Term q d n -> GetLams q d n
|
||||
getLams : Term d n -> GetLams d n
|
||||
getLams s = getLams' [<] s Refl
|
||||
|
||||
|
||||
public export
|
||||
record GetDLams q d n where
|
||||
record GetDLams d n where
|
||||
constructor GotDLams
|
||||
{0 lams, rest : Nat}
|
||||
names : NContext lams
|
||||
body : Term q rest n
|
||||
body : Term rest n
|
||||
0 eq : lams + d = rest
|
||||
0 notDLam : NotDLam body
|
||||
|
||||
mutual
|
||||
export %inline
|
||||
getDLams' : forall lams, rest.
|
||||
NContext lams -> Term q rest n -> (0 eq : lams + d = rest) ->
|
||||
GetDLams q d n
|
||||
NContext lams -> Term rest n -> (0 eq : lams + d = rest) ->
|
||||
GetDLams d n
|
||||
getDLams' xs s0 eq =
|
||||
let Element s nc = pushSubsts s0 in
|
||||
getDLamsNc xs (assert_smaller s0 s) eq
|
||||
|
|
@ -206,41 +206,41 @@ mutual
|
|||
private
|
||||
getDLamsNc : forall lams, rest.
|
||||
NContext lams ->
|
||||
(t : Term q rest n) -> (0 nc : NotClo t) =>
|
||||
(t : Term rest n) -> (0 nc : NotClo t) =>
|
||||
(0 eq : lams + d = rest) ->
|
||||
GetDLams q d n
|
||||
GetDLams d n
|
||||
getDLamsNc is s Refl = case nchoose $ isDLam s of
|
||||
Left y => let DLam (S [< i] body) = s in
|
||||
getDLams' (is :< i) (assert_smaller s body.term) Refl
|
||||
Right n => GotDLams is s Refl n
|
||||
|
||||
export %inline
|
||||
getDLams : Term q d n -> GetDLams q d n
|
||||
getDLams : Term d n -> GetDLams d n
|
||||
getDLams s = getDLams' [<] s Refl
|
||||
|
||||
|
||||
public export
|
||||
record GetPairs q d n where
|
||||
record GetPairs d n where
|
||||
constructor GotPairs
|
||||
init : SnocList $ Term q d n
|
||||
last : Term q d n
|
||||
init : SnocList $ Term d n
|
||||
last : Term d n
|
||||
notPair : NotPair last
|
||||
|
||||
mutual
|
||||
export %inline
|
||||
getPairs' : SnocList (Term q d n) -> Term q d n -> GetPairs q d n
|
||||
getPairs' : SnocList (Term d n) -> Term d n -> GetPairs d n
|
||||
getPairs' ss t0 =
|
||||
let Element t nc = pushSubsts t0 in getPairsNc ss (assert_smaller t0 t)
|
||||
|
||||
private
|
||||
getPairsNc : SnocList (Term q d n) ->
|
||||
(t : Term q d n) -> (0 nc : NotClo t) =>
|
||||
GetPairs q d n
|
||||
getPairsNc : SnocList (Term d n) ->
|
||||
(t : Term d n) -> (0 nc : NotClo t) =>
|
||||
GetPairs d n
|
||||
getPairsNc ss t = case nchoose $ isPair t of
|
||||
Left y => let Pair s t = t in
|
||||
getPairs' (ss :< s) t
|
||||
Right n => GotPairs ss t n
|
||||
|
||||
export
|
||||
getPairs : Term q d n -> GetPairs q d n
|
||||
getPairs : Term d n -> GetPairs d n
|
||||
getPairs = getPairs' [<]
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ import Data.SnocVect
|
|||
|
||||
namespace CanDSubst
|
||||
public export
|
||||
interface CanDSubst (0 tm : Nat -> Nat -> Type) where
|
||||
interface CanDSubst (0 tm : TermLike) where
|
||||
(//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
|
||||
|
||||
||| does the minimal reasonable work:
|
||||
|
|
@ -17,14 +17,14 @@ namespace CanDSubst
|
|||
||| - composes (lazily) with an existing top-level dim-closure
|
||||
||| - otherwise, wraps in a new closure
|
||||
export
|
||||
CanDSubst (Term q) where
|
||||
CanDSubst Term where
|
||||
s // Shift SZ = s
|
||||
TYPE l // _ = TYPE l
|
||||
DCloT s ph // th = DCloT s $ ph . th
|
||||
s // th = DCloT s th
|
||||
|
||||
private
|
||||
subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
|
||||
subDArgs : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
|
||||
subDArgs (f :% d) th = subDArgs f th :% (d // th)
|
||||
subDArgs e th = DCloE e th
|
||||
|
||||
|
|
@ -36,7 +36,7 @@ subDArgs e th = DCloE e th
|
|||
||| top-level sequence of dimension applications
|
||||
||| - otherwise, wraps in a new closure
|
||||
export
|
||||
CanDSubst (Elim q) where
|
||||
CanDSubst Elim where
|
||||
e // Shift SZ = e
|
||||
F x // _ = F x
|
||||
B i // _ = B i
|
||||
|
|
@ -46,22 +46,22 @@ CanDSubst (Elim q) where
|
|||
|
||||
namespace DSubst.ScopeTermN
|
||||
export %inline
|
||||
(//) : ScopeTermN s q dfrom n -> Lazy (DSubst dfrom dto) ->
|
||||
ScopeTermN s q dto n
|
||||
(//) : ScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
|
||||
ScopeTermN s dto 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 q dfrom n -> Lazy (DSubst dfrom dto) ->
|
||||
DScopeTermN s q dto n
|
||||
DScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
|
||||
DScopeTermN s dto 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 q d) where fromVar = B
|
||||
export %inline FromVar (Term q d) where fromVar = E . fromVar
|
||||
export %inline FromVar (Elim d) where fromVar = B
|
||||
export %inline FromVar (Term d) where fromVar = E . fromVar
|
||||
|
||||
|
||||
||| does the minimal reasonable work:
|
||||
|
|
@ -71,7 +71,7 @@ export %inline FromVar (Term q d) where fromVar = E . fromVar
|
|||
||| - immediately looks up a bound variable
|
||||
||| - otherwise, wraps in a new closure
|
||||
export
|
||||
CanSubstSelf (Elim q d) where
|
||||
CanSubstSelf (Elim d) where
|
||||
F x // _ = F x
|
||||
B i // th = th !! i
|
||||
CloE e ph // th = assert_total CloE e $ ph . th
|
||||
|
|
@ -82,7 +82,7 @@ CanSubstSelf (Elim q d) where
|
|||
namespace CanTSubst
|
||||
public export
|
||||
interface CanTSubst (0 tm : TermLike) where
|
||||
(//) : tm q d from -> Lazy (TSubst q d from to) -> tm q d to
|
||||
(//) : tm d from -> Lazy (TSubst d from to) -> tm d to
|
||||
|
||||
||| does the minimal reasonable work:
|
||||
||| - deletes the closure around an atomic constant like `TYPE`
|
||||
|
|
@ -102,135 +102,135 @@ CanTSubst Term where
|
|||
namespace ScopeTermN
|
||||
export %inline
|
||||
(//) : {s : Nat} ->
|
||||
ScopeTermN s q d from -> Lazy (TSubst q d from to) ->
|
||||
ScopeTermN s q d to
|
||||
ScopeTermN s d from -> Lazy (TSubst d from to) ->
|
||||
ScopeTermN s d to
|
||||
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 q d from -> Lazy (TSubst q d from to) ->
|
||||
DScopeTermN s q d to
|
||||
DScopeTermN s d from -> Lazy (TSubst d from to) ->
|
||||
DScopeTermN s d to
|
||||
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 q d) where s // by = s // Shift by
|
||||
export %inline CanShift (Elim q d) where e // by = e // Shift by
|
||||
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 q d) where
|
||||
{s : Nat} -> CanShift (ScopeTermN s d) where
|
||||
b // by = b // Shift by
|
||||
|
||||
|
||||
export %inline
|
||||
comp : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
|
||||
TSubst q dto from to
|
||||
comp : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
|
||||
TSubst dto from to
|
||||
comp th ps ph = map (// th) ps . ph
|
||||
|
||||
|
||||
public export %inline
|
||||
dweakT : {by : Nat} -> Term q d n -> Term q (by + d) n
|
||||
dweakT : {by : Nat} -> Term d n -> Term (by + d) n
|
||||
dweakT t = t // shift by
|
||||
|
||||
public export %inline
|
||||
dweakE : {by : Nat} -> Elim q d n -> Elim q (by + d) n
|
||||
dweakE : {by : Nat} -> Elim d n -> Elim (by + d) n
|
||||
dweakE t = t // shift by
|
||||
|
||||
|
||||
public export %inline
|
||||
weakT : {default 1 by : Nat} -> Term q d n -> Term q d (by + n)
|
||||
weakT : {default 1 by : Nat} -> Term d n -> Term d (by + n)
|
||||
weakT t = t // shift by
|
||||
|
||||
public export %inline
|
||||
weakE : {default 1 by : Nat} -> Elim q d n -> Elim q d (by + n)
|
||||
weakE : {default 1 by : Nat} -> Elim d n -> Elim d (by + n)
|
||||
weakE t = t // shift by
|
||||
|
||||
|
||||
parameters {s : Nat}
|
||||
namespace ScopeTermBody
|
||||
export %inline
|
||||
(.term) : ScopedBody s (Term q d) n -> Term q d (s + n)
|
||||
(.term) : ScopedBody s (Term d) n -> Term d (s + n)
|
||||
(Y b).term = b
|
||||
(N b).term = weakT b {by = s}
|
||||
|
||||
namespace ScopeTermN
|
||||
export %inline
|
||||
(.term) : ScopeTermN s q d n -> Term q d (s + n)
|
||||
(.term) : ScopeTermN s d n -> Term d (s + n)
|
||||
t.term = t.body.term
|
||||
|
||||
namespace DScopeTermBody
|
||||
export %inline
|
||||
(.term) : ScopedBody s (\d => Term q d n) d -> Term q (s + d) n
|
||||
(.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
|
||||
(Y b).term = b
|
||||
(N b).term = dweakT b {by = s}
|
||||
|
||||
namespace DScopeTermN
|
||||
export %inline
|
||||
(.term) : DScopeTermN s q d n -> Term q (s + d) n
|
||||
(.term) : DScopeTermN s d n -> Term (s + d) n
|
||||
t.term = t.body.term
|
||||
|
||||
|
||||
export %inline
|
||||
subN : ScopeTermN s q d n -> SnocVect s (Elim q d n) -> Term q d n
|
||||
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 q d n -> Elim q d n -> Term q d n
|
||||
sub1 : ScopeTerm d n -> Elim d n -> Term d n
|
||||
sub1 t e = subN t [< e]
|
||||
|
||||
export %inline
|
||||
dsubN : DScopeTermN s q d n -> SnocVect s (Dim d) -> Term q d n
|
||||
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 q d n -> Dim d -> Term q d n
|
||||
dsub1 : DScopeTerm d n -> Dim d -> Term d n
|
||||
dsub1 t p = dsubN t [< p]
|
||||
|
||||
|
||||
public export %inline
|
||||
(.zero) : DScopeTerm q d n -> Term q d n
|
||||
(.zero) : DScopeTerm d n -> Term d n
|
||||
body.zero = dsub1 body $ K Zero
|
||||
|
||||
public export %inline
|
||||
(.one) : DScopeTerm q d n -> Term q d n
|
||||
(.one) : DScopeTerm d n -> Term d n
|
||||
body.one = dsub1 body $ K One
|
||||
|
||||
|
||||
public export
|
||||
0 CloTest : TermLike -> Type
|
||||
CloTest tm = forall q, d, n. tm q d n -> Bool
|
||||
CloTest tm = forall d, n. tm d n -> Bool
|
||||
|
||||
interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
|
||||
pushSubstsWith : DSubst dfrom dto -> TSubst q dto from to ->
|
||||
tm q dfrom from -> Subset (tm q dto to) (No . isClo)
|
||||
pushSubstsWith : DSubst dfrom dto -> TSubst dto from to ->
|
||||
tm dfrom from -> Subset (tm dto to) (No . isClo)
|
||||
|
||||
public export
|
||||
0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm q d n)
|
||||
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 q d n = Subset (tm q d n) NotClo
|
||||
NonClo tm d n = Subset (tm d n) NotClo
|
||||
|
||||
public export %inline
|
||||
nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
|
||||
(t : tm q d n) -> (0 nc : NotClo t) => NonClo tm q d n
|
||||
(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 q d n -> NonClo tm q d n
|
||||
pushSubsts : tm d n -> NonClo tm d n
|
||||
pushSubsts s = pushSubstsWith id id s
|
||||
|
||||
export %inline
|
||||
pushSubstsWith' : DSubst dfrom dto -> TSubst q dto from to ->
|
||||
tm q dfrom from -> tm q dto to
|
||||
pushSubstsWith' : DSubst dfrom dto -> TSubst dto from to ->
|
||||
tm dfrom from -> tm dto to
|
||||
pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
|
||||
|
||||
mutual
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue