Q.S.T.Reduce ⇒ Q.Reduce and make it use Definition directly
This commit is contained in:
parent
ae43c324c0
commit
7895fa37e5
8 changed files with 43 additions and 97 deletions
|
|
@ -88,43 +88,3 @@ public export %inline
|
|||
lookupElim : forall isGlobal.
|
||||
Name -> Definitions' q isGlobal -> Maybe (Elim q d n)
|
||||
lookupElim x defs = toElim !(lookup x defs)
|
||||
|
||||
|
||||
parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
|
||||
namespace Term
|
||||
public export %inline
|
||||
isRedex : Term q d n -> Bool
|
||||
isRedex = isRedex $ \x => lookupElim x defs
|
||||
|
||||
public export
|
||||
0 IsRedex, NotRedex : Pred $ Term q d n
|
||||
IsRedex = So . isRedex
|
||||
NotRedex = No . isRedex
|
||||
|
||||
namespace Elim
|
||||
public export %inline
|
||||
isRedex : Elim q d n -> Bool
|
||||
isRedex = isRedex $ \x => lookupElim x defs
|
||||
|
||||
public export
|
||||
0 IsRedex, NotRedex : Pred $ Elim q d n
|
||||
IsRedex = So . isRedex
|
||||
NotRedex = No . isRedex
|
||||
|
||||
public export
|
||||
0 NonRedexElim, NonRedexTerm :
|
||||
(q : Type) -> (d, n : Nat) -> {isGlobal : Pred q} ->
|
||||
Definitions' q isGlobal -> Type
|
||||
NonRedexElim q d n defs = Subset (Elim q d n) (NotRedex defs)
|
||||
NonRedexTerm q d n defs = Subset (Term q d n) (NotRedex defs)
|
||||
|
||||
parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
|
||||
namespace Term
|
||||
export covering %inline
|
||||
whnfD : Term q d n -> NonRedexTerm q d n defs
|
||||
whnfD = whnf $ \x => lookupElim x defs
|
||||
|
||||
namespace Elim
|
||||
export covering %inline
|
||||
whnfD : Elim q d n -> NonRedexElim q d n defs
|
||||
whnfD = whnf $ \x => lookupElim x defs
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
module Quox.Equal
|
||||
|
||||
import public Quox.Syntax
|
||||
import public Quox.Definition
|
||||
import public Quox.Typing
|
||||
import public Control.Monad.Either
|
||||
import public Control.Monad.Reader
|
||||
|
|
@ -83,7 +81,7 @@ parameters (defs : Definitions' q g)
|
|||
public export
|
||||
isSubSing : Term q 0 n -> Bool
|
||||
isSubSing ty =
|
||||
let Element ty nc = whnfD defs ty in
|
||||
let Element ty nc = whnf defs ty in
|
||||
case ty of
|
||||
TYPE _ => False
|
||||
Pi {res, _} => isSubSing res.term
|
||||
|
|
@ -118,9 +116,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
|
||||
compare0 ctx ty s t =
|
||||
wrapErr (WhileComparingT (MkTyContext new ctx) !mode ty s t) $ do
|
||||
let Element ty nty = whnfD defs ty
|
||||
Element s ns = whnfD defs s
|
||||
Element t nt = whnfD defs t
|
||||
let Element ty nty = whnf defs ty
|
||||
Element s ns = whnf defs s
|
||||
Element t nt = whnf defs t
|
||||
tty <- ensureTyCon ty
|
||||
compare0' ctx ty s t
|
||||
|
||||
|
|
@ -192,8 +190,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
export covering %inline
|
||||
compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
|
||||
compareType ctx s t = do
|
||||
let Element s ns = whnfD defs s
|
||||
Element t nt = whnfD defs t
|
||||
let Element s ns = whnf defs s
|
||||
Element t nt = whnf defs t
|
||||
ts <- ensureTyCon s
|
||||
tt <- ensureTyCon t
|
||||
st <- either pure (const $ clashT (TYPE UAny) s t) $
|
||||
|
|
@ -245,7 +243,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
|
||||
compareType' ctx (E e) (E f) = do
|
||||
-- no fanciness needed here cos anything other than a neutral
|
||||
-- has been inlined by whnfD
|
||||
-- has been inlined by whnf
|
||||
Elim.compare0 ctx e f
|
||||
|
||||
||| performs the minimum work required to recompute the type of an elim.
|
||||
|
|
@ -291,8 +289,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
|
||||
compare0 ctx e f =
|
||||
wrapErr (WhileComparingE (MkTyContext new ctx) !mode e f) $ do
|
||||
let Element e ne = whnfD defs e
|
||||
Element f nf = whnfD defs f
|
||||
let Element e ne = whnf defs e
|
||||
Element f nf = whnf defs f
|
||||
-- [fixme] there is a better way to do this "isSubSing" stuff for sure
|
||||
unless (isSubSing defs !(computeElimType ctx e ne)) $
|
||||
compare0' ctx e f ne nf
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
module Quox.Syntax.Term.Reduce
|
||||
module Quox.Reduce
|
||||
|
||||
import Quox.No
|
||||
import Quox.Syntax.Term.Base
|
||||
import Quox.Syntax.Term.Subst
|
||||
import Quox.Syntax
|
||||
import Quox.Definition
|
||||
import Data.Vect
|
||||
import Data.Maybe
|
||||
|
||||
|
|
@ -125,10 +125,6 @@ parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to)
|
|||
pushSubstsWith' e = (pushSubstsWith th ph e).fst
|
||||
|
||||
|
||||
public export 0
|
||||
Lookup : TermLike
|
||||
Lookup q d n = Name -> Maybe $ Elim q d n
|
||||
|
||||
public export %inline
|
||||
isLamHead : Elim {} -> Bool
|
||||
isLamHead (Lam {} :# Pi {}) = True
|
||||
|
|
@ -154,12 +150,12 @@ isAnn : Elim {} -> Bool
|
|||
isAnn (_ :# _) = True
|
||||
isAnn _ = False
|
||||
|
||||
parameters (g : Lookup q d n)
|
||||
parameters (defs : Definitions' q g)
|
||||
mutual
|
||||
namespace Elim
|
||||
public export
|
||||
isRedex : Elim q d n -> Bool
|
||||
isRedex (F x) = isJust $ g x
|
||||
isRedex (F x) {d, n} = isJust $ lookupElim x defs {d, n}
|
||||
isRedex (B _) = False
|
||||
isRedex (f :@ _) = isRedex f || isLamHead f
|
||||
isRedex (CasePair {pair, _}) = isRedex pair || isPairHead pair
|
||||
|
|
@ -188,18 +184,19 @@ parameters (g : Lookup q d n)
|
|||
IsRedex = So . isRedex
|
||||
NotRedex = No . isRedex
|
||||
|
||||
public export
|
||||
0 NonRedexElim, NonRedexTerm : (q, d, n : _) -> Lookup q d n -> Type
|
||||
NonRedexElim q d n g = Subset (Elim q d n) (NotRedex g)
|
||||
NonRedexTerm q d n g = Subset (Term q d n) (NotRedex g)
|
||||
parameters (q : Type) (d, n : Nat) {g : q -> Type} (defs : Definitions' q g)
|
||||
public export
|
||||
0 NonRedexElim, NonRedexTerm : Type
|
||||
NonRedexElim = Subset (Elim q d n) (NotRedex defs)
|
||||
NonRedexTerm = Subset (Term q d n) (NotRedex defs)
|
||||
|
||||
|
||||
parameters (g : Lookup q d n)
|
||||
parameters (defs : Definitions' q g)
|
||||
mutual
|
||||
namespace Elim
|
||||
export covering
|
||||
whnf : Elim q d n -> NonRedexElim q d n g
|
||||
whnf (F x) with (g x) proof eq
|
||||
whnf : Elim q d n -> NonRedexElim q d n defs
|
||||
whnf (F x) with (lookupElim x defs) proof eq
|
||||
_ | Just y = whnf y
|
||||
_ | Nothing = Element (F x) $ rewrite eq in Ah
|
||||
|
||||
|
|
@ -251,7 +248,7 @@ parameters (g : Lookup q d n)
|
|||
|
||||
namespace Term
|
||||
export covering
|
||||
whnf : Term q d n -> NonRedexTerm q d n g
|
||||
whnf : Term q d n -> NonRedexTerm q d n defs
|
||||
whnf t@(TYPE {}) = Element t Ah
|
||||
whnf t@(Pi {}) = Element t Ah
|
||||
whnf t@(Lam {}) = Element t Ah
|
||||
|
|
@ -3,5 +3,4 @@ module Quox.Syntax.Term
|
|||
import public Quox.Syntax.Term.Base
|
||||
import public Quox.Syntax.Term.Split
|
||||
import public Quox.Syntax.Term.Subst
|
||||
import public Quox.Syntax.Term.Reduce
|
||||
import public Quox.Syntax.Term.Pretty
|
||||
|
|
|
|||
|
|
@ -1,14 +1,11 @@
|
|||
module Quox.Typing
|
||||
|
||||
import public Quox.Syntax
|
||||
import public Quox.Context
|
||||
import public Quox.Definition
|
||||
import public Quox.Reduce
|
||||
|
||||
import Data.Nat
|
||||
import public Data.SortedMap
|
||||
import Control.Monad.Either
|
||||
import Control.Monad.Reader
|
||||
import Control.Monad.State
|
||||
import public Control.Monad.Either
|
||||
import Generics.Derive
|
||||
|
||||
%hide TT.Name
|
||||
|
|
@ -206,27 +203,27 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
|
|||
export covering %inline
|
||||
expectTYPE : Term q d n -> m Universe
|
||||
expectTYPE s =
|
||||
case fst $ whnfD defs s of
|
||||
case fst $ whnf defs s of
|
||||
TYPE l => pure l
|
||||
_ => throwError $ ExpectedTYPE s
|
||||
|
||||
export covering %inline
|
||||
expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n)
|
||||
expectPi s =
|
||||
case fst $ whnfD defs s of
|
||||
case fst $ whnf defs s of
|
||||
Pi {qty, arg, res, _} => pure (qty, arg, res)
|
||||
_ => throwError $ ExpectedPi s
|
||||
|
||||
export covering %inline
|
||||
expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n)
|
||||
expectSig s =
|
||||
case fst $ whnfD defs s of
|
||||
case fst $ whnf defs s of
|
||||
Sig {fst, snd, _} => pure (fst, snd)
|
||||
_ => throwError $ ExpectedSig s
|
||||
|
||||
export covering %inline
|
||||
expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n)
|
||||
expectEq s =
|
||||
case fst $ whnfD defs s of
|
||||
case fst $ whnf defs s of
|
||||
Eq {ty, l, r, _} => pure (ty, l, r)
|
||||
_ => throwError $ ExpectedEq s
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue