8000 Delete unused `glue1` bindings by ncfavier · Pull Request #7021 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Delete unused glue1 bindings #7021

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Dec 5, 2023
Merged

Delete unused glue1 bindings #7021

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 8 additions & 5 deletions src/full/Agda/TypeChecking/Primitive/Cubical/Base.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -272,17 +272,20 @@ instance Reduce a => Reduce (FamilyOrNot a) where
-- | For the Kan operations in @Glue@ and @hcomp {Type}@, we optimise
-- evaluation a tiny bit by differentiating the term produced when
-- evaluating a Kan operation by itself vs evaluating it under @unglue@.
-- (See @headStop@ below.)
data TermPosition
= Head
| Eliminated
deriving (Eq,Show)

-- | If we're computing a Kan operation for one of the "unstable" type
-- formers (@Glue@, @hcomp {Type}@), this tells us whether the type will
-- reduce further, and whether we should care.
-- | Kan operations for the "unstable" type formers (@Glue@, @hcomp {Type}@) are
-- computed "negatively": they never actually produce a @glue φ t a@ term. Instead,
-- we block the computation unless such a term would reduce further, which happens
-- in two cases:
--
-- When should we care? When we're in the 'Head' 'TermPosition'. When
-- will the type reduce further? When @φ@, its formula, is not i1.
-- * when the formula @φ@ is i1, in which case we reduce to @t@;
-- * when we're under an @unglue@, i.e. in 'Eliminated' 'TermPosition', in which case
-- we reduce to @a@.
headStop :: PureTCM m => TermPosition -> m Term -> m Bool
headStop tpos phi
| Head <- tpos = do
Expand Down
13 changes: 2 additions & 11 deletions src/full/Agda/TypeChecking/Primitive/Cubical/Glue.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,14 +22,13 @@ import Agda.TypeChecking.Primitive.Cubical.Base
import Agda.TypeChecking.Reduce
( reduceB' )
import Agda.TypeChecking.Substitute
( absBody, apply, sort, subst, applyE )
( absBody, apply, sort, applyE )

import Agda.Syntax.Common
( Hiding(..), Cubical(..), Arg(..)
( Cubical(..), Arg(..)
, ConOrigin(..), ProjOrigin(..)
, Relevance(..)
, setRelevance
, setHiding
)
import Agda.Syntax.Internal

Expand Down Expand Up @@ -106,7 +105,6 @@ doGlueKanOp (HCompOp psi u u0) (IsNot (la, lb, bA, phi, bT, e)) tpos = do
getTermLocal = getTerm $ getBuiltinId builtinHComp ++ " for " ++ getBuiltinId builtinGlue
tHComp <- getTermLocal builtinHComp
tEFun <- getTermLocal builtinEquivFun
tglue <- getTermLocal builtin_glue
tunglue <- getTermLocal builtin_unglue
io <- getTermLocal builtinIOne
tItIsOne <- getTermLocal builtinItIsOne
Expand Down Expand Up @@ -148,7 +146,6 @@ doGlueKanOp (TranspOp psi u0) (IsFam (la, lb, bA, phi, bT, e)) tpos = do
tEFun <- getTermLocal builtinEquivFun
tEProof <- getTermLocal builtinEquivProof
toutS <- getTermLocal builtinSubOut
tglue <- getTermLocal builtin_glue
tunglue <- getTermLocal builtin_unglue
io <- getTermLocal builtinIOne
iz <- getTermLocal builtinIZero
Expand All @@ -168,12 +165,6 @@ doGlueKanOp (TranspOp psi u0) (IsFam (la, lb, bA, phi, bT, e)) tpos = do
<@> (imax phi (ineg i))
<@> u0
[psi,u0] <- mapM (open . unArg) [ignoreBlocking psi,u0]

-- glue1 t a = glue la[i1/i] lb[i1/i] bA[i1/i] phi[i1/i] bT[i1/i] e[i1/i] t a
glue1 <- do
g <- open $ (tglue `apply`) . map ((setHiding Hidden) . (subst 0 io)) $ [la, lb, bA, phi, bT, e]
return $ \ t a -> g <@> t <@> a

[la, lb, bA, phi, bT, e] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [la, lb, bA, phi, bT, e]

-- Andreas, 2022-03-24, fixing #5838
Expand Down
9 changes: 1 addition & 8 deletions src/full/Agda/TypeChecking/Primitive/Cubical/HCompU.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ import Agda.TypeChecking.Primitive.Cubical.Base
import Agda.TypeChecking.Reduce
( reduceB', reduceB )
import Agda.TypeChecking.Substitute
( absBody, apply, sort, subst, applyE )
( absBody, apply, sort, applyE )

import Agda.Utils.Functor
import Agda.Utils.Maybe
Expand All @@ -58,7 +58,6 @@ doHCompUKanOp (HCompOp psi u u0) (IsNot (la, phi, bT, bA)) tpos = do
iz <- getTermLocal builtinIZero
tHComp <- getTermLocal builtinHComp
tTransp <- getTermLocal builtinTrans
tglue <- getTermLocal builtin_glueU
tunglue <- getTermLocal builtin_unglueU
tLSuc <- getTermLocal builtinLevelSuc
tSubIn <- getTermLocal builtinSubIn
Expand Down Expand Up @@ -124,12 +123,6 @@ doHCompUKanOp (TranspOp psi u0) (IsFam (la, phi, bT, bA)) tpos = do
<@> u0

[psi, u0] <- mapM (open . unArg) [ignoreBlocking psi, u0]
glue1 <- do
tglue <- cl $ getTermLocal builtin_glueU
[la, phi, bT, bA] <- mapM (open . unArg . subst 0 io) $ [la, phi, bT, bA]
let bAS = pure tSubIn <#> (pure tLSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <@> bA
g <- (open =<<) $ pure tglue <#> la <#> phi <#> bT <#> bAS
return $ \ t a -> g <@> t <@> a

[la, phi, bT, bA] <- mapM (\a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [la, phi, bT, bA]

Expand Down
0