Compare commits
15 Commits
629434c752
...
124637c946
Author | SHA1 | Date |
---|---|---|
rhiannon morris | 124637c946 | |
rhiannon morris | 33abbf659e | |
rhiannon morris | 326db52204 | |
rhiannon morris | ddfbca7fcc | |
rhiannon morris | aca953c518 | |
rhiannon morris | b61ace9c7d | |
rhiannon morris | 9e702dd03d | |
rhiannon morris | 92870fe716 | |
rhiannon morris | a7673f901f | |
rhiannon morris | 5580f90e8d | |
rhiannon morris | fa09aaf228 | |
rhiannon morris | 6eccfeef52 | |
rhiannon morris | f0d3529f63 | |
rhiannon morris | cd330c1092 | |
rhiannon morris | 865772d512 |
|
@ -10,7 +10,6 @@ def boolω : 1.Bool → [ω.Bool] =
|
|||
def if : 0.(A : ★) → 1.Bool → ω.A → ω.A → A =
|
||||
λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f };
|
||||
|
||||
-- [todo]: universe lifting
|
||||
def0 If : 1.Bool → 0.★ → 0.★ → ★ =
|
||||
λ b T F ⇒ case1 b return ★ of { 'true ⇒ T; 'false ⇒ F };
|
||||
|
||||
|
|
|
@ -74,10 +74,6 @@ public export
|
|||
DefsState : Type -> Type
|
||||
DefsState = StateL DEFS Definitions
|
||||
|
||||
export
|
||||
defs : Has DefsReader fs => Eff fs Definitions
|
||||
defs = askAt DEFS
|
||||
|
||||
|
||||
public export %inline
|
||||
lookupElim : {d, n : Nat} -> Name -> Definitions -> Maybe (Elim d n)
|
||||
|
|
|
@ -347,9 +347,10 @@ parameters (defs : Definitions)
|
|||
-- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
|
||||
compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
|
||||
compareType (extendDim sTy.name One ctx) sTy.one tTy.one
|
||||
let ty = case !mode of Super => sTy; _ => tTy
|
||||
local_ Equal $ do
|
||||
Term.compare0 ctx sTy.zero sl tl
|
||||
Term.compare0 ctx sTy.one sr tr
|
||||
Term.compare0 ctx ty.zero sl tl
|
||||
Term.compare0 ctx ty.one sr tr
|
||||
|
||||
compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
|
||||
-- ------------------
|
||||
|
@ -636,7 +637,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
|
|||
private
|
||||
runCompare : (Definitions -> EqContext n -> DSubst d 0 -> Equal_ ()) ->
|
||||
Equal ()
|
||||
runCompare act = fromEqual_ $ eachFace $ act !defs
|
||||
runCompare act = fromEqual_ $ eachFace $ act !(askAt DEFS)
|
||||
|
||||
namespace Term
|
||||
export covering
|
||||
|
|
|
@ -9,6 +9,11 @@ import Syntax.PreorderReasoning
|
|||
|
||||
%default total
|
||||
|
||||
infixl 8 `shiftL`, `shiftR`
|
||||
infixl 7 .&.
|
||||
infixl 6 `xor`
|
||||
infixl 5 .|.
|
||||
|
||||
|
||||
public export
|
||||
data LTE' : Nat -> Nat -> Type where
|
||||
|
@ -119,3 +124,86 @@ spread mask subj = go 1 (halfRec mask) subj 0 where
|
|||
go bit (HalfRecOdd _ rec) subj res = case half subj of
|
||||
HalfOdd subj => go (bit + bit) rec subj (res + bit)
|
||||
HalfEven subj => go (bit + bit) rec subj res
|
||||
|
||||
|
||||
|
||||
public export
|
||||
data BitwiseRec : Nat -> Nat -> Type where
|
||||
BwDone : BitwiseRec 0 0
|
||||
Bw00 : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
|
||||
BitwiseRec (m + m) (n + n)
|
||||
Bw01 : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
|
||||
BitwiseRec (m + m) (S (n + n))
|
||||
Bw10 : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
|
||||
BitwiseRec (S (m + m)) (n + n)
|
||||
Bw11 : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
|
||||
BitwiseRec (S (m + m)) (S (n + n))
|
||||
|
||||
export
|
||||
bitwiseRec : (m, n : Nat) -> BitwiseRec m n
|
||||
bitwiseRec m n = go (halfRec m) (halfRec n) where
|
||||
go : forall m, n. HalfRec m -> HalfRec n -> BitwiseRec m n
|
||||
go HalfRecZ HalfRecZ = BwDone
|
||||
go HalfRecZ (HalfRecEven n nr) = Bw00 0 n $ go HalfRecZ nr
|
||||
go HalfRecZ (HalfRecOdd n nr) = Bw01 0 n $ go HalfRecZ nr
|
||||
go (HalfRecEven m mr) HalfRecZ = Bw00 m 0 $ go mr HalfRecZ
|
||||
go (HalfRecEven m mr) (HalfRecEven n nr) = Bw00 m n $ go mr nr
|
||||
go (HalfRecEven m mr) (HalfRecOdd n nr) = Bw01 m n $ go mr nr
|
||||
go (HalfRecOdd m mr) HalfRecZ = Bw10 m 0 $ go mr HalfRecZ
|
||||
go (HalfRecOdd m mr) (HalfRecEven n nr) = Bw10 m n $ go mr nr
|
||||
go (HalfRecOdd m mr) (HalfRecOdd n nr) = Bw11 m n $ go mr nr
|
||||
|
||||
export
|
||||
bitwise : (Bool -> Bool -> Bool) -> Nat -> Nat -> Nat
|
||||
bitwise f m n = go 1 (bitwiseRec m n) 0 where
|
||||
one : Bool -> Bool -> Nat -> Nat -> Nat
|
||||
one p q bit res = if f p q then bit + res else res
|
||||
go : forall m, n. Nat -> BitwiseRec m n -> Nat -> Nat
|
||||
go bit BwDone res = res
|
||||
go bit (Bw00 m n rec) res = go (bit + bit) rec $ one False False bit res
|
||||
go bit (Bw01 m n rec) res = go (bit + bit) rec $ one False True bit res
|
||||
go bit (Bw10 m n rec) res = go (bit + bit) rec $ one True False bit res
|
||||
go bit (Bw11 m n rec) res = go (bit + bit) rec $ one True True bit res
|
||||
|
||||
export
|
||||
(.&.) : Nat -> Nat -> Nat
|
||||
(.&.) = bitwise $ \p, q => p && q
|
||||
|
||||
private %foreign "scheme:blodwen-and"
|
||||
primAnd : Nat -> Nat -> Nat
|
||||
%transform "NatExtra.(.&.)" NatExtra.(.&.) m n = primAnd m n
|
||||
|
||||
export
|
||||
(.|.) : Nat -> Nat -> Nat
|
||||
(.|.) = bitwise $ \p, q => p || q
|
||||
|
||||
private %foreign "scheme:blodwen-or"
|
||||
primOr : Nat -> Nat -> Nat
|
||||
%transform "NatExtra.(.|.)" NatExtra.(.|.) m n = primOr m n
|
||||
|
||||
export
|
||||
xor : Nat -> Nat -> Nat
|
||||
xor = bitwise (/=)
|
||||
|
||||
private %foreign "scheme:blodwen-xor"
|
||||
primXor : Nat -> Nat -> Nat
|
||||
%transform "NatExtra.xor" NatExtra.xor m n = primXor m n
|
||||
|
||||
|
||||
export
|
||||
shiftL : Nat -> Nat -> Nat
|
||||
shiftL n 0 = n
|
||||
shiftL n (S i) = shiftL (n + n) i
|
||||
|
||||
private %foreign "scheme:blodwen-shl"
|
||||
primShiftL : Nat -> Nat -> Nat
|
||||
%transform "NatExtra.shiftL" NatExtra.shiftL n i = primShiftL n i
|
||||
|
||||
export
|
||||
shiftR : Nat -> Nat -> Nat
|
||||
shiftR n 0 = n
|
||||
shiftR n (S i) = shiftL (floorHalf n) i
|
||||
|
||||
private %foreign "scheme:blodwen-shr"
|
||||
primShiftR : Nat -> Nat -> Nat
|
||||
%transform "NatExtra.shiftR" NatExtra.shiftR n i = primShiftR n i
|
||||
|
|
|
@ -255,7 +255,6 @@ mutual
|
|||
t => let ctx = MkNameContexts (map fromPatVar ds) (map fromPatVar ns) in
|
||||
throw $ AnnotationNeeded t.loc ctx t
|
||||
|
||||
-- [todo] use SN if the var is named but still unused
|
||||
private
|
||||
fromPTermTScope : {s : Nat} -> Context' PatVar d -> Context' PatVar n ->
|
||||
SnocVect s PatVar -> PTerm ->
|
||||
|
|
|
@ -6,6 +6,8 @@ import System.File
|
|||
|
||||
import Quox.Pretty
|
||||
|
||||
%hide Text.PrettyPrint.Prettyprinter.Doc.infixr.(<++>)
|
||||
|
||||
|
||||
public export
|
||||
TypeError, LexError, ParseError : Type
|
||||
|
|
|
@ -14,7 +14,6 @@ import Control.Eff
|
|||
%default total
|
||||
|
||||
|
||||
-- [fixme] rename this to Whnf and the interface to CanWhnf
|
||||
public export
|
||||
Whnf : List (Type -> Type)
|
||||
Whnf = [NameGen, Except Error]
|
||||
|
|
|
@ -133,7 +133,6 @@ data Term where
|
|||
||| dimension closure/suspended substitution
|
||||
DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
|
||||
|
||||
||| first argument `d` is dimension scope size, second `n` is term scope size
|
||||
public export
|
||||
data Elim where
|
||||
||| free variable, possibly with a displacement (see @crude, or @mugen for a
|
||||
|
|
|
@ -58,11 +58,12 @@ pbname (_, x, _) = x
|
|||
private
|
||||
record SplitPi d n where
|
||||
constructor MkSplitPi
|
||||
{0 inner : Nat}
|
||||
binds : Telescope (PiBind d) n inner
|
||||
cod : Term d inner
|
||||
|
||||
private
|
||||
splitPi : Telescope (PiBind d) n inner -> Term d inner -> SplitPi d n
|
||||
splitPi : Telescope (PiBind d) n n' -> Term d n' -> SplitPi d n
|
||||
splitPi binds (Pi qty arg res _) =
|
||||
splitPi (binds :< (qty, res.name, arg)) $
|
||||
assert_smaller res $ pushSubsts' res.term
|
||||
|
@ -87,7 +88,7 @@ prettyPiBind1 pi x dnames tnames s = hcat <$> sequence
|
|||
private
|
||||
prettyPiBinds : {opts : _} ->
|
||||
BContext d -> BContext n ->
|
||||
Telescope (PiBind d) n inner ->
|
||||
Telescope (PiBind d) n n' ->
|
||||
Eff Pretty (SnocList (Doc opts))
|
||||
prettyPiBinds _ _ [<] = pure [<]
|
||||
prettyPiBinds dnames tnames (binds :< (q, x, t)) =
|
||||
|
@ -103,11 +104,12 @@ SigBind d n = (BindName, Term d n)
|
|||
private
|
||||
record SplitSig d n where
|
||||
constructor MkSplitSig
|
||||
{0 inner : Nat}
|
||||
binds : Telescope (SigBind d) n inner
|
||||
last : Term d inner
|
||||
|
||||
private
|
||||
splitSig : Telescope (SigBind d) n inner -> Term d inner -> SplitSig d n
|
||||
splitSig : Telescope (SigBind d) n n' -> Term d n' -> SplitSig d n
|
||||
splitSig binds (Sig fst snd _) =
|
||||
splitSig (binds :< (snd.name, fst)) $
|
||||
assert_smaller snd $ pushSubsts' snd.term
|
||||
|
@ -129,7 +131,7 @@ prettySigBind1 x dnames tnames s = hcat <$> sequence
|
|||
private
|
||||
prettySigBinds : {opts : _} ->
|
||||
BContext d -> BContext n ->
|
||||
Telescope (SigBind d) n inner ->
|
||||
Telescope (SigBind d) n n' ->
|
||||
Eff Pretty (SnocList (Doc opts))
|
||||
prettySigBinds _ _ [<] = pure [<]
|
||||
prettySigBinds dnames tnames (binds :< (x, t)) =
|
||||
|
@ -163,6 +165,7 @@ NameChunks = SnocList (NameSort, SnocList BindName)
|
|||
private
|
||||
record SplitLams d n where
|
||||
constructor MkSplitLams
|
||||
{0 dinner, ninner : Nat}
|
||||
dnames : BTelescope d dinner
|
||||
tnames : BTelescope n ninner
|
||||
chunks : NameChunks
|
||||
|
@ -178,9 +181,9 @@ where
|
|||
if s == s' then xss :< (s', xs :< y)
|
||||
else xss :< (s', xs) :< (s, [< y])
|
||||
|
||||
go : BTelescope d dinner -> BTelescope n ninner ->
|
||||
go : BTelescope d d' -> BTelescope n n' ->
|
||||
SnocList (NameSort, SnocList BindName) ->
|
||||
Term dinner ninner -> SplitLams d n
|
||||
Term d' n' -> SplitLams d n
|
||||
go dnames tnames chunks (Lam b _) =
|
||||
go dnames (tnames :< b.name) (push T b.name chunks) $
|
||||
assert_smaller b $ pushSubsts' b.term
|
||||
|
@ -235,6 +238,7 @@ prettyDTApps dnames tnames f xs = do
|
|||
private
|
||||
record CaseArm opts d n where
|
||||
constructor MkCaseArm
|
||||
{0 dinner, ninner : Nat}
|
||||
pat : Doc opts
|
||||
dbinds : BTelescope d dinner -- 🍴
|
||||
tbinds : BTelescope n ninner
|
||||
|
|
|
@ -10,7 +10,7 @@ import Data.SnocVect
|
|||
namespace CanDSubst
|
||||
public export
|
||||
interface CanDSubst (0 tm : TermLike) where
|
||||
(//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
|
||||
(//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n
|
||||
|
||||
||| does the minimal reasonable work:
|
||||
||| - deletes the closure around an atomic constant like `TYPE`
|
||||
|
@ -25,7 +25,7 @@ CanDSubst Term where
|
|||
s // th = DCloT $ Sub s th
|
||||
|
||||
private
|
||||
subDArgs : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
|
||||
subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
|
||||
subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
|
||||
subDArgs e th = DCloE $ Sub e th
|
||||
|
||||
|
@ -47,16 +47,16 @@ CanDSubst Elim where
|
|||
|
||||
namespace DSubst.ScopeTermN
|
||||
export %inline
|
||||
(//) : ScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
|
||||
ScopeTermN s dto n
|
||||
(//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
|
||||
ScopeTermN s d2 n
|
||||
S ns (Y body) // th = S ns $ Y $ body // th
|
||||
S ns (N body) // th = S ns $ N $ body // th
|
||||
|
||||
namespace DSubst.DScopeTermN
|
||||
export %inline
|
||||
(//) : {s : Nat} ->
|
||||
DScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
|
||||
DScopeTermN s dto n
|
||||
DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
|
||||
DScopeTermN s d2 n
|
||||
S ns (Y body) // th = S ns $ Y $ body // pushN s th
|
||||
S ns (N body) // th = S ns $ N $ body // th
|
||||
|
||||
|
@ -83,7 +83,7 @@ CanSubstSelf (Elim d) where
|
|||
namespace CanTSubst
|
||||
public export
|
||||
interface CanTSubst (0 tm : TermLike) where
|
||||
(//) : tm d from -> Lazy (TSubst d from to) -> tm d to
|
||||
(//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
|
||||
|
||||
||| does the minimal reasonable work:
|
||||
||| - deletes the closure around an atomic constant like `TYPE`
|
||||
|
@ -103,16 +103,15 @@ CanTSubst Term where
|
|||
namespace ScopeTermN
|
||||
export %inline
|
||||
(//) : {s : Nat} ->
|
||||
ScopeTermN s d from -> Lazy (TSubst d from to) ->
|
||||
ScopeTermN s d to
|
||||
ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
|
||||
ScopeTermN s d n2
|
||||
S ns (Y body) // th = S ns $ Y $ body // pushN s th
|
||||
S ns (N body) // th = S ns $ N $ body // th
|
||||
|
||||
namespace DScopeTermN
|
||||
export %inline
|
||||
(//) : {s : Nat} ->
|
||||
DScopeTermN s d from -> Lazy (TSubst d from to) ->
|
||||
DScopeTermN s d to
|
||||
DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
|
||||
S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
|
||||
S ns (N body) // th = S ns $ N $ body // th
|
||||
|
||||
|
@ -125,8 +124,7 @@ export %inline
|
|||
|
||||
|
||||
export %inline
|
||||
comp : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
|
||||
TSubst dto from to
|
||||
comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
|
||||
comp th ps ph = map (// th) ps . ph
|
||||
|
||||
|
||||
|
@ -205,8 +203,8 @@ public export
|
|||
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 dto from to ->
|
||||
tm dfrom from -> Subset (tm dto to) (No . isClo)
|
||||
pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
|
||||
tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
|
||||
|
||||
public export
|
||||
0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
|
||||
|
@ -230,8 +228,7 @@ parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
|
|||
pushSubsts s = pushSubstsWith id id s
|
||||
|
||||
export %inline
|
||||
pushSubstsWith' : DSubst dfrom dto -> TSubst dto from to ->
|
||||
tm dfrom from -> tm dto to
|
||||
pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
|
||||
pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
|
||||
|
||||
export %inline
|
||||
|
@ -334,8 +331,7 @@ private %inline
|
|||
CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
(r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
|
||||
CompHY {ty, p, q, val, r, zero, one, loc} =
|
||||
-- [fixme] maintain location of existing B VZ
|
||||
let ty' = SY ty.names $ ty.term // (B VZ noLoc ::: shift 2) in
|
||||
let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
|
||||
Comp {
|
||||
ty = dsub1 ty q, p, q,
|
||||
val = E $ Coe ty p q val val.loc, r,
|
||||
|
|
|
@ -8,10 +8,10 @@ import public Quox.OPE
|
|||
|
||||
|
||||
export
|
||||
Tighten (Shift from) where
|
||||
Tighten (Shift f) where
|
||||
-- `OPE m n` is a spicy `m ≤ n`,
|
||||
-- and `Shift from n` is a (different) spicy `from ≤ n`
|
||||
-- so the value is `from ≤ m` (as a `Shift`), if that is the case
|
||||
-- and `Shift f n` is a (different) spicy `f ≤ n`
|
||||
-- so the value is `f ≤ m` (as a `Shift`), if that is the case
|
||||
tighten _ SZ = Nothing
|
||||
tighten Id by = Just by
|
||||
tighten (Drop p) (SS by) = tighten p by
|
||||
|
@ -26,12 +26,12 @@ Tighten Dim where
|
|||
|
||||
export
|
||||
tightenSub : (forall m, n. OPE m n -> env n -> Maybe (env m)) ->
|
||||
OPE to1 to2 -> Subst env from to2 -> Maybe (Subst env from to1)
|
||||
OPE t1 t2 -> Subst env f t2 -> Maybe (Subst env f t1)
|
||||
tightenSub f p (Shift by) = [|Shift $ tighten p by|]
|
||||
tightenSub f p (t ::: th) = [|f p t !::: tightenSub f p th|]
|
||||
|
||||
export
|
||||
Tighten env => Tighten (Subst env from) where
|
||||
Tighten env => Tighten (Subst env f) where
|
||||
tighten p th = tightenSub tighten p th
|
||||
|
||||
|
||||
|
|
|
@ -76,5 +76,6 @@ one' i = (one i).snd
|
|||
public export
|
||||
record SomeOPE n where
|
||||
constructor MkOPE
|
||||
{0 scope : Nat}
|
||||
{mask : Nat}
|
||||
0 ope : OPE m n mask
|
||||
0 ope : OPE scope n mask
|
||||
|
|
|
@ -6,36 +6,166 @@ import public Quox.Thin.View
|
|||
import public Quox.Thin.List
|
||||
import public Quox.Thin.Cover
|
||||
import Data.DPair
|
||||
import Data.Nat
|
||||
import Control.Function
|
||||
|
||||
%default total
|
||||
|
||||
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
|
||||
|
||||
namespace Coprod
|
||||
public export
|
||||
data Comps : OPE scope n scopeMask ->
|
||||
OPEList scope -> OPEList n -> Type where
|
||||
Nil : Comps sub [] []
|
||||
(::) : Comp sub inner full ->
|
||||
Comps sub inners fulls ->
|
||||
Comps sub (inner :: inners) (full :: fulls)
|
||||
%name Comps comps
|
||||
|
||||
public export
|
||||
record Coprod (fulls : OPEList n) where
|
||||
constructor MkCoprod
|
||||
{scopeMask : Nat}
|
||||
{0 sub : OPE scope n scopeMask}
|
||||
inners : OPEList scope
|
||||
0 comps : Comps sub inners fulls
|
||||
0 cov : Cover inners
|
||||
%name Coprod cop
|
||||
|
||||
export
|
||||
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)
|
||||
0 compsLength : Comps s ts us -> length ts = length us
|
||||
compsLength [] = Refl
|
||||
compsLength (_ :: comps) = cong S $ compsLength comps
|
||||
|
||||
-- [todo] n-ary coprod
|
||||
|
||||
export
|
||||
coprodNil : Coprod []
|
||||
coprodNil = MkCoprod [] [] [] {sub = zero}
|
||||
|
||||
private
|
||||
coprodHead : {n : Nat} -> (opes : OPEList (S n)) ->
|
||||
Either (Cover1 opes) (All IsDrop opes)
|
||||
coprodHead [] = Right []
|
||||
coprodHead (ope :: opes) = case view ope of
|
||||
DropV {} => case coprodHead opes of
|
||||
Left cov1 => Left $ There cov1
|
||||
Right drops => Right $ ItIsDrop :: drops
|
||||
KeepV {} => Left Here
|
||||
|
||||
|
||||
private
|
||||
0 compsConsDrop : (opes : OPEList (S n)) ->
|
||||
All IsDrop opes ->
|
||||
All2 IsTail opes tails ->
|
||||
Comps sub inners tails -> Comps (drop sub) inners opes
|
||||
compsConsDrop [] [] [] [] = []
|
||||
compsConsDrop (Drop ope Refl :: opes) (ItIsDrop :: ds) (DropT :: ts) (c :: cs) =
|
||||
DropZ c :: compsConsDrop opes ds ts cs
|
||||
compsConsDrop (_ :: _) [] _ _ impossible
|
||||
|
||||
private
|
||||
coprodConsDrop : (0 opes : OPEList (S n)) ->
|
||||
(0 ds : All IsDrop opes) ->
|
||||
(0 ts : All2 IsTail opes tails) ->
|
||||
Coprod tails -> Coprod opes
|
||||
coprodConsDrop opes ds ts (MkCoprod inners comps cov) =
|
||||
MkCoprod inners (compsConsDrop opes ds ts comps) cov
|
||||
|
||||
|
||||
private
|
||||
copyHeads : {m : Nat} ->
|
||||
(src : OPEList (S m)) -> (tgt : OPEList n) ->
|
||||
(0 eq : length src = length tgt) => OPEList (S n)
|
||||
copyHeads [] [] = []
|
||||
copyHeads (s :: ss) (t :: ts) =
|
||||
case view s of
|
||||
DropV mask ope => drop t :: copyHeads ss ts @{inj S eq}
|
||||
KeepV mask ope => keep t :: copyHeads ss ts @{inj S eq}
|
||||
|
||||
private
|
||||
0 copyHeadsComps : (eq : length outers = length inners) ->
|
||||
All2 IsTail outers tails ->
|
||||
Comps sub inners tails ->
|
||||
Comps (keep sub) (copyHeads outers inners) outers
|
||||
copyHeadsComps _ [] [] = []
|
||||
copyHeadsComps eq (DropT {eq = eq2} :: ps) ((c :: cs) {full}) =
|
||||
let (Refl) = eq2 in -- coverage checker weirdness
|
||||
rewrite viewDrop full Refl in
|
||||
KDZ c :: copyHeadsComps (inj S eq) ps cs
|
||||
copyHeadsComps eq (KeepT {eq = eq2} :: ps) ((c :: cs) {full}) =
|
||||
let (Refl) = eq2 in
|
||||
rewrite viewKeep full Refl in
|
||||
KeepZ c :: copyHeadsComps (inj S eq) ps cs
|
||||
|
||||
-- should be erased (coverage checker weirdness)
|
||||
-- it is possibly https://github.com/idris-lang/Idris2/issues/1417 that keeps
|
||||
-- happening. not 100% sure
|
||||
private
|
||||
cover1CopyHeads : {m : Nat} ->
|
||||
(ss : OPEList (S m)) -> (ts : OPEList n) ->
|
||||
(eq : length ss = length ts) ->
|
||||
(cov1 : Cover1 ss) -> Cover1 (copyHeads ss ts)
|
||||
cover1CopyHeads (Keep s Refl :: ss) (t :: ts) eq Here =
|
||||
rewrite viewKeep s Refl in Here
|
||||
cover1CopyHeads (s :: ss) (t :: ts) eq (There c) with (view s)
|
||||
cover1CopyHeads (Drop {} :: ss) (t :: ts) eq (There c) | DropV {} =
|
||||
There $ cover1CopyHeads ss ts (inj S eq) c
|
||||
cover1CopyHeads (Keep {} :: ss) (t :: ts) eq (There c) | KeepV {} =
|
||||
Here
|
||||
|
||||
private
|
||||
copyHeadsTails : {m : Nat} ->
|
||||
(ss : OPEList (S m)) -> (ts : OPEList n) ->
|
||||
(eq : length ss = length ts) ->
|
||||
All2 IsTail (copyHeads ss ts) ts
|
||||
copyHeadsTails [] [] eq = []
|
||||
copyHeadsTails (s :: ss) (t :: ts) eq with (view s)
|
||||
copyHeadsTails (Drop ope Refl :: ss) (t :: ts) eq | DropV mask ope =
|
||||
DropT :: copyHeadsTails ss ts (inj S eq)
|
||||
copyHeadsTails (Keep ope Refl :: ss) (t :: ts) eq | KeepV mask ope =
|
||||
KeepT :: copyHeadsTails ss ts (inj S eq)
|
||||
|
||||
private
|
||||
coprodConsKeep : {n : Nat} ->
|
||||
(opes : OPEList (S n)) ->
|
||||
{0 tails : OPEList n} ->
|
||||
(cov1 : Cover1 opes) ->
|
||||
(0 ts : All2 IsTail opes tails) ->
|
||||
Coprod tails -> Coprod opes
|
||||
coprodConsKeep opes cov1 ts (MkCoprod inners comps cov) =
|
||||
MkCoprod
|
||||
(copyHeads opes inners @{all2Length ts `trans` sym (compsLength comps)})
|
||||
(copyHeadsComps _ ts comps)
|
||||
((cover1CopyHeads {cov1, _} :: cov) @{copyHeadsTails {}})
|
||||
|
||||
|
||||
export
|
||||
coprod : {n : Nat} -> (opes : OPEList n) -> Coprod opes
|
||||
|
||||
private
|
||||
coprod0 : (opes : OPEList 0) -> Coprod opes
|
||||
|
||||
private
|
||||
coprodS : {n : Nat} -> (opes : OPEList (S n)) -> Coprod opes
|
||||
|
||||
coprod {n = 0} opes = coprod0 opes
|
||||
coprod {n = S n} opes = coprodS opes
|
||||
|
||||
coprod0 [] = coprodNil
|
||||
coprod0 (ope :: opes) with %syntactic 0 (zeroIsStop ope) | (coprod opes)
|
||||
coprod0 (Stop :: opes)
|
||||
| ItIsStop | MkCoprod {sub} inners comps cov
|
||||
with %syntactic 0 (zeroIsStop sub)
|
||||
coprod0 (Stop :: opes)
|
||||
| ItIsStop | MkCoprod {sub = Stop} inners comps cov | ItIsStop
|
||||
= MkCoprod (Stop :: inners) (StopZ :: comps) []
|
||||
|
||||
coprodS [] = coprodNil
|
||||
coprodS opes =
|
||||
let hs = heads opes
|
||||
Element ts tprf = tails_ opes
|
||||
tcop = coprod $ assert_smaller opes ts
|
||||
in
|
||||
case coprodHead opes of
|
||||
Left cov1 => coprodConsKeep opes cov1 tprf tcop
|
||||
Right drops => coprodConsDrop opes drops tprf tcop
|
||||
|
|
|
@ -24,3 +24,4 @@ data Cover1 where
|
|||
Here : Cover1 (Keep ope eq :: opes)
|
||||
There : Cover1 opes -> Cover1 (ope :: opes)
|
||||
%name Cover1 cov1
|
||||
%builtin Natural Cover1
|
||||
|
|
|
@ -16,17 +16,17 @@ data OPEList : Nat -> Type where
|
|||
(::) : {mask : Nat} -> (0 ope : OPE m n mask) -> OPEList n -> OPEList n
|
||||
%name OPEList opes
|
||||
|
||||
export
|
||||
public export
|
||||
length : OPEList n -> Nat
|
||||
length [] = 0
|
||||
length (_ :: opes) = S $ length opes
|
||||
|
||||
export
|
||||
public export
|
||||
toList : OPEList n -> List (SomeOPE n)
|
||||
toList [] = []
|
||||
toList (ope :: opes) = MkOPE ope :: toList opes
|
||||
|
||||
export
|
||||
public export
|
||||
fromList : List (SomeOPE n) -> OPEList n
|
||||
fromList [] = []
|
||||
fromList (MkOPE ope :: xs) = ope :: fromList xs
|
||||
|
@ -56,6 +56,11 @@ namespace All2
|
|||
All2 p (a :: as) (b :: bs)
|
||||
%name All2.All2 ps, qs
|
||||
|
||||
export
|
||||
0 all2Length : {p : Rel m n} -> All2 p ss ts -> length ss = length ts
|
||||
all2Length [] = Refl
|
||||
all2Length (p :: ps) = cong S $ all2Length ps
|
||||
|
||||
namespace Any
|
||||
public export
|
||||
data Any : Pred n -> OPEList n -> Type where
|
||||
|
@ -108,7 +113,6 @@ 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)
|
||||
|
|
|
@ -3,6 +3,7 @@ module Quox.Thin.View
|
|||
import public Quox.Thin.Base
|
||||
import Quox.NatExtra
|
||||
import Data.Singleton
|
||||
import Data.SnocVect
|
||||
|
||||
%default total
|
||||
|
||||
|
@ -74,3 +75,29 @@ outerInnerZero Stop = Refl
|
|||
export
|
||||
0 outerMaskZero : OPE m 0 mask -> mask = 0
|
||||
outerMaskZero Stop = Refl
|
||||
|
||||
export
|
||||
0 viewStop : view Stop = StopV
|
||||
viewStop = Refl
|
||||
|
||||
export
|
||||
0 viewDrop : (ope : OPE m n mask) -> (eq : mask2 = mask + mask) ->
|
||||
view (Drop {mask} ope eq) = DropV mask ope
|
||||
viewDrop ope eq with (view (Drop ope eq))
|
||||
viewDrop ope Refl | DropV _ ope = Refl
|
||||
|
||||
export
|
||||
0 viewKeep : (ope : OPE m n mask) -> (eq : mask2 = S (mask + mask)) ->
|
||||
view (Keep {mask} ope eq) = KeepV mask ope
|
||||
viewKeep ope eq with (view (Keep ope eq))
|
||||
viewKeep ope Refl | KeepV _ ope = Refl
|
||||
|
||||
|
||||
namespace SnocVect
|
||||
export
|
||||
select : {n, mask : Nat} -> (0 ope : OPE m n mask) ->
|
||||
SnocVect n a -> SnocVect m a
|
||||
select ope sx with (view ope)
|
||||
select _ [<] | StopV = [<]
|
||||
select _ (sx :< x) | DropV _ ope = select ope sx
|
||||
select _ (sx :< x) | KeepV _ ope = select ope sx :< x
|
||||
|
|
|
@ -163,7 +163,7 @@ mutual
|
|||
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
|
||||
TC (CheckResult' n)
|
||||
toCheckType ctx sg t ty = do
|
||||
u <- expectTYPE !defs ctx ty.loc ty
|
||||
u <- expectTYPE !(askAt DEFS) ctx ty.loc ty
|
||||
expectEqualQ t.loc Zero sg.fst
|
||||
checkTypeNoWrap ctx t (Just u)
|
||||
pure $ zeroFor ctx
|
||||
|
@ -178,7 +178,7 @@ mutual
|
|||
check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Lam body loc) ty = do
|
||||
(qty, arg, res) <- expectPi !defs ctx ty.loc ty
|
||||
(qty, arg, res) <- expectPi !(askAt DEFS) ctx ty.loc ty
|
||||
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
|
||||
-- with ρ ≤ σπ
|
||||
let qty' = sg.fst * qty
|
||||
|
@ -189,7 +189,7 @@ mutual
|
|||
check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Pair fst snd loc) ty = do
|
||||
(tfst, tsnd) <- expectSig !defs ctx ty.loc ty
|
||||
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty
|
||||
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
|
||||
qfst <- checkC ctx sg fst tfst
|
||||
let tsnd = sub1 tsnd (Ann fst tfst fst.loc)
|
||||
|
@ -201,7 +201,7 @@ mutual
|
|||
check' ctx sg t@(Enum {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Tag t loc) ty = do
|
||||
tags <- expectEnum !defs ctx ty.loc ty
|
||||
tags <- expectEnum !(askAt DEFS) ctx ty.loc ty
|
||||
-- if t ∈ ts
|
||||
unless (t `elem` tags) $ throw $ TagNotIn loc t tags
|
||||
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
|
||||
|
@ -210,7 +210,7 @@ mutual
|
|||
check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (DLam body loc) ty = do
|
||||
(ty, l, r) <- expectEq !defs ctx ty.loc ty
|
||||
(ty, l, r) <- expectEq !(askAt DEFS) ctx ty.loc ty
|
||||
let ctx' = extendDim body.name ctx
|
||||
ty = ty.term
|
||||
body = body.term
|
||||
|
@ -226,17 +226,17 @@ mutual
|
|||
check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Zero {}) ty = do
|
||||
expectNat !defs ctx ty.loc ty
|
||||
expectNat !(askAt DEFS) ctx ty.loc ty
|
||||
pure $ zeroFor ctx
|
||||
|
||||
check' ctx sg (Succ n {}) ty = do
|
||||
expectNat !defs ctx ty.loc ty
|
||||
expectNat !(askAt DEFS) ctx ty.loc ty
|
||||
checkC ctx sg n ty
|
||||
|
||||
check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Box val loc) ty = do
|
||||
(q, ty) <- expectBOX !defs ctx ty.loc ty
|
||||
(q, ty) <- expectBOX !(askAt DEFS) ctx ty.loc ty
|
||||
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
|
||||
valout <- checkC ctx sg val ty
|
||||
-- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
|
||||
|
@ -314,7 +314,7 @@ mutual
|
|||
-- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
|
||||
case u of
|
||||
Just u => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
|
||||
Nothing => ignore $ expectTYPE !defs ctx e.loc infres.type
|
||||
Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type
|
||||
-- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
|
||||
|
||||
|
||||
|
@ -333,7 +333,7 @@ mutual
|
|||
|
||||
infer' ctx sg (F x u loc) = do
|
||||
-- if π·x : A {≔ s} in global context
|
||||
g <- lookupFree x loc !defs
|
||||
g <- lookupFree x loc !(askAt DEFS)
|
||||
-- if σ ≤ π
|
||||
expectCompatQ loc sg.fst g.qty.fst
|
||||
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
|
||||
|
@ -355,7 +355,7 @@ mutual
|
|||
infer' ctx sg (App fun arg loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
|
||||
funres <- inferC ctx sg fun
|
||||
(qty, argty, res) <- expectPi !defs ctx fun.loc funres.type
|
||||
(qty, argty, res) <- expectPi !(askAt DEFS) ctx fun.loc funres.type
|
||||
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
|
||||
argout <- checkC ctx (subjMult sg qty) arg argty
|
||||
-- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + πΣ₂
|
||||
|
@ -372,7 +372,7 @@ mutual
|
|||
pairres <- inferC ctx sg pair
|
||||
-- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
|
||||
checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
|
||||
(tfst, tsnd) <- expectSig !defs ctx pair.loc pairres.type
|
||||
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx pair.loc pairres.type
|
||||
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
|
||||
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
|
||||
-- with ρ₁, ρ₂ ≤ πσ
|
||||
|
@ -391,7 +391,7 @@ mutual
|
|||
infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
|
||||
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
|
||||
tres <- inferC ctx sg t
|
||||
ttags <- expectEnum !defs ctx t.loc tres.type
|
||||
ttags <- expectEnum !(askAt DEFS) ctx t.loc tres.type
|
||||
-- if 1 ≤ π, OR there is only zero or one option
|
||||
unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ loc One pi
|
||||
-- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
|
||||
|
@ -415,7 +415,7 @@ mutual
|
|||
-- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
|
||||
nres <- inferC ctx sg n
|
||||
let nat = nres.type
|
||||
expectNat !defs ctx n.loc nat
|
||||
expectNat !(askAt DEFS) ctx n.loc nat
|
||||
-- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
|
||||
checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
|
||||
-- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
|
||||
|
@ -439,7 +439,7 @@ mutual
|
|||
infer' ctx sg (CaseBox pi box ret body loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
|
||||
boxres <- inferC ctx sg box
|
||||
(q, ty) <- expectBOX !defs ctx box.loc boxres.type
|
||||
(q, ty) <- expectBOX !(askAt DEFS) ctx box.loc boxres.type
|
||||
-- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
|
||||
checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
|
||||
-- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
|
||||
|
@ -457,7 +457,7 @@ mutual
|
|||
infer' ctx sg (DApp fun dim loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
|
||||
InfRes {type, qout} <- inferC ctx sg fun
|
||||
ty <- fst <$> expectEq !defs ctx fun.loc type
|
||||
ty <- fst <$> expectEq !(askAt DEFS) ctx fun.loc type
|
||||
-- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
|
||||
pure $ InfRes {type = dsub1 ty dim, qout}
|
||||
|
||||
|
@ -485,7 +485,7 @@ mutual
|
|||
-- if σ = 0
|
||||
expectEqualQ loc Zero sg.fst
|
||||
-- if Ψ, Γ ⊢₀ e ⇒ Type u
|
||||
u <- expectTYPE !defs ctx ty.loc . type =<< inferC ctx szero ty
|
||||
u <- expectTYPE !(askAt DEFS) ctx ty.loc . type =<< inferC ctx szero ty
|
||||
-- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
|
||||
checkTypeC ctx ret Nothing
|
||||
-- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
|
||||
|
|
|
@ -69,7 +69,7 @@ namespace TContext
|
|||
zeroFor ctx = Zero <$ ctx
|
||||
|
||||
private
|
||||
extendLen : Telescope a from to -> Singleton from -> Singleton to
|
||||
extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2
|
||||
extendLen [<] x = x
|
||||
extendLen (tel :< _) x = [|S $ extendLen tel x|]
|
||||
|
||||
|
@ -89,7 +89,7 @@ namespace TyContext
|
|||
null ctx = null ctx.dnames && null ctx.tnames
|
||||
|
||||
export %inline
|
||||
extendTyN : CtxExtension d from to -> TyContext d from -> TyContext d to
|
||||
extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
|
||||
extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
|
||||
let (qs, xs, ss) = unzip3 xss in
|
||||
MkTyContext {
|
||||
|
@ -172,7 +172,7 @@ namespace EqContext
|
|||
null ctx = null ctx.dnames && null ctx.tnames
|
||||
|
||||
export %inline
|
||||
extendTyN : CtxExtension 0 from to -> EqContext from -> EqContext to
|
||||
extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
|
||||
extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
|
||||
let (qs, xs, ss) = unzip3 xss in
|
||||
MkEqContext {
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
collection = "nightly-230522"
|
||||
collection = "nightly-230622"
|
||||
|
||||
[custom.all.tap]
|
||||
type = "git"
|
||||
|
|
|
@ -34,7 +34,7 @@ ToInfo Error' where
|
|||
M = Eff [Except Error', DefsReader]
|
||||
|
||||
inj : TC a -> M a
|
||||
inj act = rethrow $ mapFst TCError $ runTC !defs act
|
||||
inj act = rethrow $ mapFst TCError $ runTC !(askAt DEFS) act
|
||||
|
||||
|
||||
reflTy : Term d n
|
||||
|
|
Loading…
Reference in New Issue