{-# OPTIONS --safe --without-K #-}
module Reflection.Utils.Records where

open import Meta.Prelude
open import Meta.Init

open import Data.List using (map)
open import Class.DecEq using (_==_)

open import Reflection.AST.Term using (_⋯⟅∷⟆_)
open import Reflection.TCM.Syntax using (_>>=_)
open import Reflection.Utils.Reduction using (headReduce; resolveToName)
import Agda.Builtin.Reflection as B using (TC)

mkRecord : List (Name × Term) → Term
mkRecord fs = pat-lam (map (λ (fn , e) → clause [] [ vArg (proj fn) ] e) fs) []

updateField : List Name → Term → Name → Term → Term
updateField fs rexp fn fexp =
  flip pat-lam [] $ flip map fs $ λ f →
    clause [] [ vArg (proj f) ] $
      if f == fn then fexp else (f ∙⟦ rexp ⟧)

------------------------------------------------------------------------
-- Projecting reasonable terms of fields out of record value
--
-- Getting a field from a record value in such a way that we don't
-- reduce too little or to much is quite delicate. For example, from the
-- semiring ℚ, the `1#` field should give us `1ℚ`, never its `mkℚ ...`
-- unfolding. `projectField` handles this appropriately.

private
  fieldFuel : ℕ
  fieldFuel = 

module _ (k : ℕ) (r : Term) (f : Name) where

  fieldProjection : Term
  fieldProjection = def f (k ⋯⟅∷⟆ r ⟨∷⟩ [])

  projectField : B.TC Term
  projectField = do
    r' ← headReduce fieldFuel r
    resolveToName (stuckOn r') fieldFuel fieldProjection
    where
      stuckOn : Term → List Name
      stuckOn (def nm _) = nm ∷ []
      stuckOn _          = []