Display form matching, including for projections, works on the head symbol of the term currently being reified. This means that display forms on projections can only match if the term is put in 'prefix form', i.e. unSpine. This means that the reification code shows all projections with display forms in prefix, even if none of the display forms match. A minimal reproducer is attached.
{-# OPTIONS --postfix-projections #-}module_ whereopenimportAgda.Builtin.EqualityrecordFoo:Set1wherefieldproj:SetopenFoopostulateAB:FooAp:Set{-# DISPLAY Foo.proj A = Ap #-}_:B.proj≡A.proj_=refl{-
The terms
proj B
and
Ap
are not equal at type Set
when checking that the expression refl has type proj B ≡ Ap
-}We prefixize projections that have display forms before doing any case analysis on the term, and use the resulting head/spine to try display form matching. Display form matching receives only the head name and the eliminations.
case unSpine' prefixize v of
I.Def x es -> do
reportS "reify.def" 80 $ "reifying def" <+> pretty x
(x, es) <- reifyPathPConstAsPath x es
reifyDisplayForm x es $ reifyDef expandAnonDefs x es
-- | Find a matching display form for @q es@.
-- In essence this tries to rewrite @q es@ with any
-- display form @q ps --> dt@ and returns the instantiated
-- @dt@ if successful. First match wins.
displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)
I think a better idea for the control flow in reifyTerm would instead weave unSpine and display form matching, and only continue to case analysis on the term if no display forms matched. Note that to preserve today's behaviour when display forms do match, the "nondeterminism" in unSpine has to be outside-in, i.e., for foo x .p1 y .p2, we should try (where $ f = Apply f, .pN = Proj pN in the spine):
displayForm p2 [$ p1 (foo x)]
displayForm p1 [$ foo x, $ y, .p2]
displayForm foo [$ x, .p1, $ y, .p2]