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

rename SQtys to sg (σ)

Browse source
This commit is contained in:
rhiannon morris 2023-09-30 18:31:23 +02:00
parent be8797a3ef
commit 6896c8fcc4
1 changed files with 21 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
lib/Quox/Whnf/ComputeElimType.idr
View file

@ -11,24 +11,26 @@ import Quox.Displace
||| - assumes the elim is already typechecked ||| - assumes the elim is already typechecked
||| - the return value is not reduced ||| - the return value is not reduced
export covering export covering
computeElimType : CanWhnf Term Interface.isRedexT => computeElimType :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE => CanWhnf Elim Interface.isRedexE =>
{d, n : Nat} -> {d, n : Nat} ->
(defs : Definitions) -> WhnfContext d n -> (pi : SQty) -> (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) => (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
Eff Whnf (Term d n) Eff Whnf (Term d n)
||| computes a type and then reduces it to whnf ||| computes a type and then reduces it to whnf
export covering export covering
computeWhnfElimType0 : CanWhnf Term Interface.isRedexT => computeWhnfElimType0 :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE => CanWhnf Elim Interface.isRedexE =>
{d, n : Nat} -> {d, n : Nat} ->
(defs : Definitions) -> WhnfContext d n -> (pi : SQty) -> (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) => (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
Eff Whnf (Term d n) Eff Whnf (Term d n)
computeElimType defs ctx pi e {ne} = computeElimType defs ctx sg e =
case e of case e of
F x u loc => do F x u loc => do
let Just def = lookup x defs let Just def = lookup x defs
@ -39,7 +41,7 @@ computeElimType defs ctx pi e {ne} =
pure $ ctx.tctx !! i pure $ ctx.tctx !! i
App f s loc => App f s loc =>
case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
ty => throw $ ExpectedPi loc ctx.names ty ty => throw $ ExpectedPi loc ctx.names ty
@ -47,12 +49,12 @@ computeElimType defs ctx pi e {ne} =
pure $ sub1 ret pair pure $ sub1 ret pair
Fst pair loc => Fst pair loc =>
case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
Sig {fst, _} => pure fst Sig {fst, _} => pure fst
ty => throw $ ExpectedSig loc ctx.names ty ty => throw $ ExpectedSig loc ctx.names ty
Snd pair loc => Snd pair loc =>
case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
Sig {snd, _} => pure $ sub1 snd $ Fst pair loc Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
ty => throw $ ExpectedSig loc ctx.names ty ty => throw $ ExpectedSig loc ctx.names ty
@ -66,7 +68,7 @@ computeElimType defs ctx pi e {ne} =
pure $ sub1 ret box pure $ sub1 ret box
DApp {fun = f, arg = p, loc} => DApp {fun = f, arg = p, loc} =>
case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
Eq {ty, _} => pure $ dsub1 ty p Eq {ty, _} => pure $ dsub1 ty p
t => throw $ ExpectedEq loc ctx.names t t => throw $ ExpectedEq loc ctx.names t
@ -82,5 +84,5 @@ computeElimType defs ctx pi e {ne} =
TypeCase {ret, _} => TypeCase {ret, _} =>
pure ret pure ret
computeWhnfElimType0 defs ctx pi e = computeWhnfElimType0 defs ctx sg e =
computeElimType defs ctx pi e >>= whnf0 defs ctx pi computeElimType defs ctx sg e >>= whnf0 defs ctx SZero