Elaborate-and-give does not respect --postfix-projections

[plt-amy]

{-# OPTIONS --postfix-projections #-}
module asdf where

open import Agda.Primitive
open import Agda.Builtin.Reflection
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.List

module _ {A : Set} {B : A → Set} (x : Σ A B) where
  ai : ArgInfo
  ai = arg-info visible (modality relevant quantity-ω)
  macro
    foo : Term → TC ⊤
    foo goal = unify goal (def (quote fst) (arg ai (var 0 []) ∷ []))

  _ : A
  _ = {! foo  !}

Elaborate-and-giving that interaction point should probably expand to x .fst rather than fst x, since the user asked for --postfix-projections.

[andreasabel]

I identified the source of the problem: the translation ReflectedToAbstract does not recover projections:

agda/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs

Lines 205 to 209 in 82b2b0f

	mkDef :: HasConstInfo m => QName -> m A.Expr
	mkDef f =
	ifM (isMacro . theDef <$> getConstInfo f)
	(return $ A.Macro f)
	(return $ A.Def f)

It only distinguishes A.Macro from A.Def, not A.Proj and A.Con. Fixing this fixes this issue.