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

tycasePi etc don't actually need a scope of (S d)

Browse source
This commit is contained in:
rhiannon morris 2023-08-24 17:45:37 +02:00
parent 688204f1a4
commit a24ebe0702
1 changed files with 12 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
lib/Quox/Reduce.idr
View file

@ -261,11 +261,8 @@ coeScoped ty p q loc (S names (N body)) =
S names $ N $ E $ Coe ty p q body loc S names $ N $ E $ Coe ty p q body loc
export covering export covering CanWhnf Term Reduce.isRedexT
CanWhnf Term Reduce.isRedexT export covering CanWhnf Elim Reduce.isRedexE
export covering
CanWhnf Elim Reduce.isRedexE
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
||| performs the minimum work required to recompute the type of an elim. ||| performs the minimum work required to recompute the type of an elim.
@ -295,13 +292,14 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
computeElimType (Comp {ty, _}) = pure ty computeElimType (Comp {ty, _}) = pure ty
computeElimType (TypeCase {ret, _}) = pure ret computeElimType (TypeCase {ret, _}) = pure ret
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
||| for π.(x : A) → B, returns (A, B); ||| for π.(x : A) → B, returns (A, B);
||| for an elim returns a pair of type-cases that will reduce to that; ||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error ||| for other intro forms error
private covering private covering
tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
Eff Whnf (Term (S d) n, ScopeTerm (S d) n) Eff Whnf (Term d n, ScopeTerm d n)
tycasePi (Pi {arg, res, _}) = pure (arg, res) tycasePi (Pi {arg, res, _}) = pure (arg, res)
tycasePi (E e) {tnf} = do tycasePi (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf} ty <- computeElimType defs ctx e @{noOr2 tnf}
@ -318,8 +316,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
||| for an elim returns a pair of type-cases that will reduce to that; ||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error ||| for other intro forms error
private covering private covering
tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
Eff Whnf (Term (S d) n, ScopeTerm (S d) n) Eff Whnf (Term d n, ScopeTerm d n)
tycaseSig (Sig {fst, snd, _}) = pure (fst, snd) tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
tycaseSig (E e) {tnf} = do tycaseSig (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf} ty <- computeElimType defs ctx e @{noOr2 tnf}
@ -336,8 +334,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
||| for an elim returns a type-case that will reduce to that; ||| for an elim returns a type-case that will reduce to that;
||| for other intro forms error ||| for other intro forms error
private covering private covering
tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
Eff Whnf (Term (S d) n) Eff Whnf (Term d n)
tycaseBOX (BOX {ty, _}) = pure ty tycaseBOX (BOX {ty, _}) = pure ty
tycaseBOX (E e) {tnf} = do tycaseBOX (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf} ty <- computeElimType defs ctx e @{noOr2 tnf}
@ -348,9 +346,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
||| for an elim returns five type-cases that will reduce to that; ||| for an elim returns five type-cases that will reduce to that;
||| for other intro forms error ||| for other intro forms error
private covering private covering
tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
Eff Whnf (Term (S d) n, Term (S d) n, DScopeTerm (S d) n, Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term d n)
Term (S d) n, Term (S d) n)
tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r) tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
tycaseEq (E e) {tnf} = do tycaseEq (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf} ty <- computeElimType defs ctx e @{noOr2 tnf}