------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflection utilities for List
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Reflection where

open import Data.List.Base
open import Reflection.AST.Term
open import Reflection.AST.Argument

------------------------------------------------------------------------
-- Type

`List : Term  Term
`List `A = def (quote List) (1 ⋯⟅∷⟆ `A ⟨∷⟩ [])

------------------------------------------------------------------------
-- Constructors

`[] : Term
`[] = con (quote List.[]) (2 ⋯⟅∷⟆ [])

infixr 5 _`∷_

_`∷_ : Term  Term  Term
x `∷ xs = con (quote List._∷_) (2 ⋯⟅∷⟆ x ⟨∷⟩ xs ⟨∷⟩ [])

------------------------------------------------------------------------
-- Patterns

-- Can't be used on the RHS as the omitted args aren't inferable
pattern `[]`       = con (quote List.[])  _
pattern _`∷`_ x xs = con (quote List._∷_) (_  _  x ⟨∷⟩ xs ⟨∷⟩ _)