use copatterns to define Sheaves; fully eta-expand

Author: plt-amy

src/1Lab/Reflection/Copattern.agda

@@ -29,31 +29,40 @@ make-copattern declare? def-name tm tp = do
 
       -- Agda will insert implicits when defining copatterns even
       -- with 'withExpandLast true', so we need to do implicit instantiation
-      -- by hand. First, we strip off all leading implicits from the field type.
-      let (implicit-tele , tp) = pi-impl-view field-tp
-      let nimplicits = length implicit-tele
-      let clause-tele = tele ++ implicit-tele
-
-      -- Construct the pattern portion of the clause, making sure to bind
-      -- all implicit variables. Note that copattern projections are always visible.
-      let pat =
-            tel→pats nimplicits tele ++
-            arg (set-visibility visible field-info) (proj field-name) ∷
-            tel→pats 0 implicit-tele
-
-      -- Construct the body of the clause, making sure to apply all arguments
-      -- bound outside the copattern match, and instantiate all implicit arguments.
-      -- We also need to apply all of the implicit arguments to 'tm'.
+      -- by hand. There are also cases where it's better to fully
+      -- eta-expand than not (e.g. the 'helper' we're expanding has a
+      -- field defined by lazy matching, which does not reduce unless
+      -- applied, and would cause duplication of the big input term). So
+      -- we fully eta-expand clauses here.
+      -- First, we strip off all leading quantifiers from the field
+      -- type.
+      let
+        (field-tele , tp) = pi-view field-tp
+        nargs = length field-tele
+        clause-tele = tele ++ field-tele
+
+      -- Construct the pattern portion of the clause, making sure to
+      -- bind all variables. Note that copattern projections are always
+      -- visible.
+      let
+        pat = tel→pats nargs tele ++
+          arg (set-visibility visible field-info) (proj field-name) ∷
+          tel→pats 0 field-tele
+
+      -- Construct the body of the clause, making sure to apply all
+      -- arguments bound outside the copattern match, and apply the
+      -- eta-expanded arguments. We also need to apply all of the
+      -- implicit arguments to 'tm'.
       body ←
         in-context (reverse clause-tele) $
-        reduce (def field-name (argN (raise nimplicits inst-tm) ∷ tel→args 0 implicit-tele))
+        reduce (def field-name (raise nargs inst-tm v∷ tel→args 0 field-tele))
 
       -- Construct the final clause.
       pure $ clause clause-tele pat body
 
   -- Define a copattern binding, and predeclare its type if required.
   case declare? of λ where
-    true → declare (argN def-name) tp
+    true  → declare (argN def-name) tp <|> pure tt
     false → pure tt
 
   -- Construct the final copattern.
@@ -82,6 +91,17 @@ repack-record tm tp = do
   -- Builld a pointwise repacking.
   pure (tel→lam tele (con ctor args))
 
+-- Helper for the 'define' macros; Unifies the given goal with the type
+-- of the given function, if it has been defined. If the function has
+-- not been defined, and the first argument is 'false', then an error is
+-- raised.
+type-for : String → Bool → Name → Term → TC ⊤
+type-for tac decl? fun goal with decl?
+... | true  = (unify goal =<< get-type fun) <|> pure tt
+... | false = (unify goal =<< get-type fun) <|> typeError
+  [ "define-" , strErr tac , ": the function " , nameErr fun , " should already have been declared."
+  ]
+
 --------------------------------------------------------------------------------
 -- Usage
 
@@ -94,8 +114,10 @@ If you wish to give the binding a type annotation, you can also use
 >  copat : Your-type
 >  unquoteDecl copat = declare-copattern copat thing-to-be-expanded
 
-All features of non-recursive records are supported, including instance
-fields and fields with implicit arguments.
+Note that, in this case, the thing-to-be-expanded must have exactly the
+same type as the binding `copat`. All features of non-recursive records
+are supported, including instance fields and fields with implicit
+arguments.
 
 These macros also allow you to lift functions 'A → some-record-type'
 into copattern definitions. Note that Agda will generate meta for
@@ -109,10 +131,13 @@ declare-copattern {A = A} nm x = do
   `A ← quoteTC A
   make-copattern true nm `x `A
 
-define-copattern : ∀ {ℓ} {A : Type ℓ} → Name → A → TC ⊤
-define-copattern {A = A} nm x = do
-  `x ← quoteTC x
+define-copattern
+  : ∀ {ℓ} (nm : Name)
+  → {@(tactic (type-for "copattern" true nm)) A : Type ℓ}
+  → A → TC ⊤
+define-copattern nm {A = A} x = do
   `A ← quoteTC A
+  `x ← define-abbrev nm "value" `A =<< quoteTC x
   make-copattern false nm `x `A
 
 {-
@@ -121,32 +146,19 @@ they cannot be quoted into any `Type ℓ`. With this in mind,
 we also provide a pair of macros that work over `Typeω` instead.
 -}
 
--- Helper for the 'define' macros; Unifies the given goal with the type
--- of the given function, if it has been defined. If the function has
--- not been defined, and the first argument is 'false', then an error is
--- raised.
-type-for : Bool → Name → Term → TC ⊤
-type-for decl? fun goal with decl?
-... | true  = (unify goal =<< get-type fun) <|> pure tt
-... | false = (unify goal =<< get-type fun) <|> typeError
-  [ "define-copattern-levels: the function " , nameErr fun , " should already have been declared."
-  ]
-
-declare-copattern-levels
-  : (nm : Name) {@(tactic (type-for true nm)) U : Typeω}
-  → U → TC ⊤
-declare-copattern-levels nm A = do
+declare-copatternω : ∀ {U : Typeω} → Name → U → TC ⊤
+declare-copatternω nm A = do
   `A ← quoteωTC A
   -- Cannot quote things in type Typeω, but we can infer their type.
   `U ← infer-type `A
   make-copattern true nm `A `U
 
-define-copattern-levels
-  : (nm : Name) {@(tactic (type-for false nm)) U : Typeω}
+define-copatternω
+  : (nm : Name) {@(tactic (type-for "copatternω" false nm)) U : Typeω}
   → U → TC ⊤
-define-copattern-levels nm A = do
-  `A ← quoteωTC A
+define-copatternω nm A = do
   `U ← get-type nm
+  `A ← define-abbrev nm "value" `U =<< quoteωTC A
   make-copattern false nm `A `U
 
 {-
@@ -206,7 +218,11 @@ private module Test where
   zero-unused-param = record { actual = 0 }
 
   one-unused-param : ∀ {n} → Unused n
-  unquoteDef one-unused-param = define-copattern one-unused-param zero-unused-param
+  unquoteDef one-unused-param = declare-copattern one-unused-param zero-unused-param
+  -- This is a type error:
+  -- unquoteDef one-unused-param = define-copattern one-unused-param zero-unused-param
+  -- because the 'define' macro propagates the type of the thing being
+  -- defined inwards.
 
   -- Functions into records that are universe polymorphic
   neat : ∀ {ℓ} {A : Type ℓ} → A → Record A
@@ -217,11 +233,11 @@ private module Test where
   -- Implicit insertion is correct for the define- macro, since the type
   -- of the function is given.
   cool : ∀ {ℓ} {A : Type ℓ} → A → Record A
-  unquoteDef cool = define-copattern-levels cool neat
+  unquoteDef cool = define-copatternω cool neat
 
   -- Eta-expanders
   expander : ∀ {m n : Nat} → Unused m → Unused n
   unquoteDef expander = define-eta-expansion expander
 
   -- Raises a type error: the function should have a declaration.
-  -- unquoteDecl uncool = define-copattern-levels uncool neat
+  -- unquoteDecl uncool = define-copatternω uncool neat

src/1Lab/Reflection/Signature.agda

@@ -211,6 +211,18 @@ helper-function def-nm suf ty cls = do
     _  → define-function nm cls
   pure nm
 
+-- Given a well-typed `val : ty`, return a definitionally-equal atomic
+-- term equal to `val`, potentially by lifting it into the signature.
+-- See 'helper-function' for the naming scheme.
+define-abbrev : Name → String → Term → Term → TC Term
+define-abbrev def-nm suf ty val with is-atomic-tree? val
+... | true  = pure val
+... | false = do
+  let (tel , _) = pi-impl-view ty
+  nm ← helper-function def-nm suf ty
+    [ clause tel (tel→pats 0 tel) (apply-tm* val (tel→args 0 tel)) ]
+  pure (def₀ nm)
+
 private
   make-args : Nat → List (Arg Nat) → List (Arg Term)
   make-args n xs = reverse $ map (λ (arg ai i) → arg ai (var (n - i - 1) [])) xs

src/1Lab/Reflection/Subst.agda

@@ -142,7 +142,7 @@ subst-tm ρ (agda-sort s) with s
 subst-tel ρ []                    = []
 subst-tel ρ ((x , arg ai t) ∷ xs) = (x , arg ai (subst-tm ρ t)) ∷ subst-tel (liftS 1 ρ) xs
 
-subst-clause σ (clause tel ps t)      = clause (subst-tel σ tel) ps (subst-tm (wkS (length tel) σ) t)
+subst-clause σ (clause tel ps t)      = clause (subst-tel σ tel) ps (subst-tm (liftS (length tel) σ) t)
 subst-clause σ (absurd-clause tel ps) = absurd-clause (subst-tel σ tel) ps
 
 _<#>_ : Term → Arg Term → Term

src/Cat/Abelian/Images.lagda.md

@@ -53,8 +53,8 @@ images : ∀ {A B} (f : Hom A B) → Image C f
 images f = im where
   the-img : ↓Obj (const! (cut f)) Forget-full-subcat
   the-img .x = tt
-  the-img .y .object = cut (Ker.kernel (Coker.coeq f))
-  the-img .y .witness {c} = kernels-are-subobjects C ∅ _ (Ker.has-is-kernel _)
+  the-img .y .fst = cut (Ker.kernel (Coker.coeq f))
+  the-img .y .snd {c} = kernels-are-subobjects C ∅ _ (Ker.has-is-kernel _)
 ```
 
 Break $f$ down as an epi $p : A \epi \ker (\coker f)$ followed by a mono
@@ -128,7 +128,7 @@ a (unique) map $\coker (\ker f) \to X$ s.t. the triangle above commutes!
       where abstract
         path : other .map .map ∘ 0m ≡ other .map .map ∘ kernel f .Kernel.kernel
         path =
-          other .y .witness _ _ $ sym $
+          other .y .snd _ _ $ sym $
                 pulll (other .map .commutes)
             ·· Ker.equal f
             ·· ∅.zero-∘r _
@@ -154,14 +154,14 @@ is the image of $f$.
                           (coker-ker≃ker-coker f .is-invertible.invr))) refl
               ∙ pullr (Coker.factors _) ∙ other .map .commutes)
         (sym (decompose f .snd ∙ assoc _ _ _))
-    factor .sq = /-Hom-path $ sym $ other .y .witness _ _ $
+    factor .sq = /-Hom-path $ sym $ other .y .snd _ _ $
       pulll (factor .β .commutes)
       ∙ the-img .map .commutes
       ·· sym (other .map .commutes)
-      ·· ap (other .y .object .map ∘_) (intror refl)
+      ·· ap (other .y .fst .map ∘_) (intror refl)
 
     unique : ∀ x → factor ≡ x
-    unique x = ↓Hom-path _ _ refl $ /-Hom-path $ other .y .witness _ _ $
+    unique x = ↓Hom-path _ _ refl $ /-Hom-path $ other .y .snd _ _ $
       sym (x .β .commutes ∙ sym (factor .β .commutes))
 ```
 </details>

src/Cat/Diagram/Equaliser/RegularMono.lagda.md

@@ -43,7 +43,7 @@ is an [[equaliser]] of some pair of arrows $g, h : b \to c$.
       {c}       : Ob
       arr₁ arr₂ : Hom b c
       has-is-eq : is-equaliser C arr₁ arr₂ f
-  
+
     open is-equaliser has-is-eq public
 ```
 
@@ -53,7 +53,7 @@ are in fact monomorphisms:
 ```agda
     is-regular-mono→is-mono : is-monic f
     is-regular-mono→is-mono = is-equaliser→is-monic _ has-is-eq
-  
+
   open is-regular-mono using (is-regular-mono→is-mono) public
 ```
 
@@ -126,7 +126,7 @@ $\phi \circ i_2 = \rm{arr_2}$.
 ```agda
     phi : Hom f⊔f.coapex reg.c
     phi = f⊔f.universal reg.equal
-  
+
     open is-effective-mono
     mon : is-effective-mono C f
     mon .cokernel = f⊔f.coapex
@@ -201,20 +201,20 @@ the code below demonstrates.
     → M-image C (is-regular-mono C , is-regular-mono→is-mono) f
   is-effective-mono→image {f = f} mon = im where
     module eff = is-effective-mono mon
-  
+
     itself : ↓Obj _ _
     itself .x = tt
-    itself .y = restrict (cut f) eff.is-effective-mono→is-regular-mono
+    itself .y = cut f , eff.is-effective-mono→is-regular-mono
     itself .map = record { map = id ; commutes = idr _ }
-  
+
     im : Initial _
     im .bot = itself
     im .has⊥ other = contr hom unique where
       hom : ↓Hom _ _ itself other
       hom .α = tt
       hom .β = other .map
       hom .sq = trivial!
-  
+
       unique : ∀ x → hom ≡ x
       unique x = ↓Hom-path _ _ refl
         (ext (intror refl ∙ ap map (x .sq) ∙ elimr refl))

src/Cat/Diagram/Image.lagda.md

@@ -124,18 +124,18 @@ is the image object, and $m$ is the inclusion map:
 
 ```agda
     Im : Ob
-    Im = im .bot .y .object .domain
+    Im = im .bot .y .fst .domain
 
     Im→codomain : Hom Im b
-    Im→codomain = im .bot .y .object .map
+    Im→codomain = im .bot .y .fst .map
 ```
 
 Furthermore, this map is both an inclusion (since $M$ is a class of
 monomorphisms), and an $M$-inclusion at that:
 
 ```agda
     Im→codomain-is-M : M .fst Im→codomain
-    Im→codomain-is-M = im .bot .y .witness
+    Im→codomain-is-M = im .bot .y .snd
 
     Im→codomain-is-monic : is-monic Im→codomain
     Im→codomain-is-monic = M .snd Im→codomain-is-M
@@ -175,7 +175,7 @@ through $k$:
     universal m M i p = im .has⊥ obj .centre .β .map where
       obj : ↓Obj _ _
       obj .x = tt
-      obj .y = restrict (cut m) M
+      obj .y = cut m , M
       obj .map = record { map = i ; commutes = p }
 
     universal-factors

src/Cat/Functor/Algebra.lagda.md

@@ -603,7 +603,7 @@ forms a full subcategory of $\cC$.
   private module Free-algebras = Cat.Reasoning Free-algebras
   module Free-alg (α : Free-algebras.Ob) where
     -- Rexport stuff in a more user-friendly format
-    open Free-object (α .witness) public
+    open Free-object (α .snd) public
 
     ob : Ob
     ob = free .fst