{-# OPTIONS --safe --without-K #-}
module Reflection.Utils.Metas where
 
open import Meta.Prelude
open import Meta.Init
 
import Data.Bool.ListAction as B
open import Data.List
import Reflection.AST.Meta as Meta
 
isMeta : Term → Bool
isMeta = λ where
  (meta _ _) → true
  _          → false
 
mutual
  findMetas : Term → List Term
  findMetas = λ where
    (var _ as) → findMetas* as
    (con _ as) → findMetas* as
    (def _ as) → findMetas* as
    (lam _ (abs _ x)) → findMetas x
    (pat-lam cs as)   → findMetasCl cs ++ findMetas* as
    (pi (arg _ a) (abs _ b)) → findMetas a ++ findMetas b
    (sort _)      → []
    (lit _)       → []
    m@(meta x as) → m ∷ findMetas* as
    unknown       → []
 
  findMetas* : List (Arg Term) → List Term
  findMetas* = λ where
    [] → []
    ((arg _ t) ∷ ts) → findMetas t ++ findMetas* ts
 
  findMetasCl : List Clause → List Term
  findMetasCl = λ where
    [] → []
    (clause _ _ t      ∷ c) → findMetas t ++ findMetasCl c
    (absurd-clause _ _ ∷ c) → findMetasCl c
 
metaId : Term → Maybe Meta
metaId (meta x _) = just x
metaId _          = nothing
 
findMetaIds : Term → List Meta
findMetaIds = mapMaybe metaId ∘ findMetas
 
firstMeta : Term → Maybe Meta
firstMeta = head ∘ findMetaIds
 
shareMeta : List Meta → List Meta → Bool
shareMeta xs ys = B.any (λ x → B.any (Meta._≡ᵇ_ x) ys) xs