------------------------------------------------------------------------
-- The Agda standard library
--
-- Terms used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.AST.Term where

open import Data.List.Base as List                     hiding (_++_)
open import Data.List.Properties                       using (∷-dec)
open import Data.Nat.Base                              using (; zero; suc)
import Data.Nat.Properties as 
open import Data.Product.Base                          using (_×_; _,_; <_,_>; uncurry; map₁)
open import Data.Product.Properties                    using (,-injective)
open import Data.Maybe.Base                            using (Maybe; just; nothing)
open import Data.String.Base                           using (String)
open import Data.String.Properties as String           hiding (_≟_)
open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)

open import Reflection.AST.Abstraction
open import Reflection.AST.Argument
open import Reflection.AST.Argument.Information using (visibility)
open import Reflection.AST.Argument.Visibility as Visibility hiding (_≟_)
import Reflection.AST.Literal as Literal
import Reflection.AST.Meta as Meta
open import Reflection.AST.Name as Name using (Name)

------------------------------------------------------------------------
-- Re-exporting the builtin type and constructors

open import Agda.Builtin.Reflection as Builtin public
  using (Sort; Type; Term; Clause; Pattern)

open Term public
  renaming (agda-sort to sort)

open Sort    public
open Clause  public
open Pattern public

------------------------------------------------------------------------
-- Handy synonyms

Clauses : Set
Clauses = List Clause

Telescope : Set
Telescope = List (String × Arg Type)

-- Pattern synonyms for more compact presentation

pattern vLam s t           = lam visible   (abs s t)
pattern hLam s t           = lam hidden    (abs s t)
pattern iLam s t           = lam instance′ (abs s t)
pattern Π[_∶_]_ s a ty     = pi a (abs s ty)
pattern vΠ[_∶_]_ s a ty    = Π[ s  (vArg a) ] ty
pattern hΠ[_∶_]_ s a ty    = Π[ s  (hArg a) ] ty
pattern iΠ[_∶_]_ s a ty    = Π[ s  (iArg a) ] ty

------------------------------------------------------------------------
-- Utility functions

getName : Term  Maybe Name
getName (con c args) = just c
getName (def f args) = just f
getName _            = nothing

-- "n ⋯⟨∷⟩ xs" prepends "n" visible unknown arguments to the list of
-- arguments. Useful when constructing the list of arguments for a
-- function with initial inferrable arguments.
infixr 5 _⋯⟨∷⟩_
_⋯⟨∷⟩_ :   Args Term  Args Term
zero  ⋯⟨∷⟩ xs = xs
suc i ⋯⟨∷⟩ xs = unknown ⟨∷⟩ (i ⋯⟨∷⟩ xs)
{-# INLINE _⋯⟨∷⟩_ #-}

-- "n ⋯⟅∷⟆ xs" prepends "n" hidden unknown arguments to the list of
-- arguments. Useful when constructing the list of arguments for a
-- function with initial implicit arguments.
infixr 5 _⋯⟅∷⟆_
_⋯⟅∷⟆_ :   Args Term  Args Term
zero  ⋯⟅∷⟆ xs = xs
suc i ⋯⟅∷⟆ xs = unknown ⟅∷⟆ (i ⋯⟅∷⟆ xs)
{-# INLINE _⋯⟅∷⟆_ #-}

-- Strips off any pi bindings returning the list of variables removed
-- and the eventual body of the expression, e.g.
--
--   stripPis `∀ x {y} → f x y` = (["x", "y"], f x y)
stripPis : Term  List (String × Arg Type) × Term
stripPis (Π[ s  t ] x) = map₁ ((s , t) ∷_) (stripPis x)
stripPis x              = [] , x

prependLams : List (String × Visibility)  Term  Term
prependLams xs t = foldr  {(s , v) t  lam v (abs s t)}) t (reverse xs)

prependHLams : List String  Term  Term
prependHLams vs = prependLams (List.map (_, hidden) vs)

prependVLams : List String  Term  Term
prependVLams vs = prependLams (List.map (_, visible) vs)

------------------------------------------------------------------------
-- Decidable equality

clause-injective₁ :  {tel tel′ ps ps′ b b′}  clause tel ps b  clause tel′ ps′ b′  tel  tel′
clause-injective₁ refl = refl

clause-injective₂ :  {tel tel′ ps ps′ b b′}  clause tel ps b  clause tel′ ps′ b′  ps  ps′
clause-injective₂ refl = refl

clause-injective₃ :  {tel tel′ ps ps′ b b′}  clause tel ps b  clause tel′ ps′ b′  b  b′
clause-injective₃ refl = refl

clause-injective :  {tel tel′ ps ps′ b b′}  clause tel ps b  clause tel′ ps′ b′  tel  tel′ × ps  ps′ × b  b′
clause-injective = < clause-injective₁ , < clause-injective₂ , clause-injective₃ > >

absurd-clause-injective₁ :  {tel tel′ ps ps′}  absurd-clause tel ps  absurd-clause tel′ ps′  tel  tel′
absurd-clause-injective₁ refl = refl

absurd-clause-injective₂ :  {tel tel′ ps ps′}  absurd-clause tel ps  absurd-clause tel′ ps′  ps  ps′
absurd-clause-injective₂ refl = refl

absurd-clause-injective :  {tel tel′ ps ps′}  absurd-clause tel ps  absurd-clause tel′ ps′  tel  tel′ × ps  ps′
absurd-clause-injective = < absurd-clause-injective₁ , absurd-clause-injective₂ >

infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_
        _≟-Clause_ _≟-Clauses_ _≟_
        _≟-Sort_ _≟-Pattern_ _≟-Patterns_ _≟-Telescope_

_≟-AbsTerm_  : DecidableEquality (Abs Term)
_≟-AbsType_  : DecidableEquality (Abs Type)
_≟-ArgTerm_  : DecidableEquality (Arg Term)
_≟-ArgType_  : DecidableEquality (Arg Type)
_≟-Args_     : DecidableEquality (Args Term)
_≟-Clause_   : DecidableEquality Clause
_≟-Clauses_  : DecidableEquality Clauses
_≟_          : DecidableEquality Term
_≟-Sort_     : DecidableEquality Sort
_≟-Patterns_ : DecidableEquality (Args Pattern)
_≟-Pattern_  : DecidableEquality Pattern

-- Decidable equality 'transformers'
-- We need to inline these because the terms are not sized so
-- termination would not obvious if we were to use higher-order
-- functions such as Data.List.Properties' ≡-dec

abs s a ≟-AbsTerm abs s′ a′ = unAbs-dec (a  a′)
abs s a ≟-AbsType abs s′ a′ = unAbs-dec (a  a′)
arg i a ≟-ArgTerm arg i′ a′ = unArg-dec (a  a′)
arg i a ≟-ArgType arg i′ a′ = unArg-dec (a  a′)

[]       ≟-Args []       = yes refl
(x  xs) ≟-Args (y  ys) = ∷-dec (x ≟-ArgTerm y) (xs ≟-Args ys)
[]       ≟-Args (_  _)  = no λ()
(_  _)  ≟-Args []       = no λ()

[]       ≟-Clauses []       = yes refl
(x  xs) ≟-Clauses (y  ys) = ∷-dec (x ≟-Clause y) (xs ≟-Clauses ys)
[]       ≟-Clauses (_  _)  = no λ()
(_  _)  ≟-Clauses []       = no λ()

_≟-Telescope_ : DecidableEquality Telescope
[] ≟-Telescope [] = yes refl
((x , t)  tel) ≟-Telescope ((x′ , t′)  tel′) = ∷-dec
  (map′ (uncurry (cong₂ _,_)) ,-injective ((x String.≟ x′) ×-dec (t ≟-ArgTerm t′)))
  (tel ≟-Telescope tel′)
[] ≟-Telescope (_  _) = no λ ()
(_  _) ≟-Telescope [] = no λ ()

clause tel ps b ≟-Clause clause tel′ ps′ b′ =
  map′  (tel≡tel′ , ps≡ps′ , b≡b′)  cong₂ (uncurry clause) (cong₂ _,_ tel≡tel′ ps≡ps′) b≡b′)
           clause-injective
           (tel ≟-Telescope tel′ ×-dec ps ≟-Patterns ps′ ×-dec b  b′)
absurd-clause tel ps ≟-Clause absurd-clause tel′ ps′ =
  map′ (uncurry (cong₂ absurd-clause))
           absurd-clause-injective
           (tel ≟-Telescope tel′ ×-dec ps ≟-Patterns ps′)
clause _ _ _      ≟-Clause absurd-clause _ _ = no λ()
absurd-clause _ _ ≟-Clause clause _ _ _      = no λ()

var-injective₁ :  {x x′ args args′}  Term.var x args  var x′ args′  x  x′
var-injective₁ refl = refl

var-injective₂ :  {x x′ args args′}  Term.var x args  var x′ args′  args  args′
var-injective₂ refl = refl

var-injective :   {x x′ args args′}  var x args  var x′ args′  x  x′ × args  args′
var-injective = < var-injective₁ , var-injective₂ >

con-injective₁ :  {c c′ args args′}  Term.con c args  con c′ args′  c  c′
con-injective₁ refl = refl

con-injective₂ :  {c c′ args args′}  Term.con c args  con c′ args′  args  args′
con-injective₂ refl = refl

con-injective :  {c c′ args args′}  con c args  con c′ args′  c  c′ × args  args′
con-injective = < con-injective₁ , con-injective₂ >

def-injective₁ :  {f f′ args args′}  def f args  def f′ args′  f  f′
def-injective₁ refl = refl

def-injective₂ :  {f f′ args args′}  def f args  def f′ args′  args  args′
def-injective₂ refl = refl

def-injective :  {f f′ args args′}  def f args  def f′ args′  f  f′ × args  args′
def-injective = < def-injective₁ , def-injective₂ >

meta-injective₁ :  {x x′ args args′}  meta x args  meta x′ args′  x  x′
meta-injective₁ refl = refl

meta-injective₂ :  {x x′ args args′}  meta x args  meta x′ args′  args  args′
meta-injective₂ refl = refl

meta-injective :  {x x′ args args′}  meta x args  meta x′ args′  x  x′ × args  args′
meta-injective = < meta-injective₁ , meta-injective₂ >

lam-injective₁ :  {v v′ t t′}  lam v t  lam v′ t′  v  v′
lam-injective₁ refl = refl

lam-injective₂ :  {v v′ t t′}  lam v t  lam v′ t′  t  t′
lam-injective₂ refl = refl

lam-injective :  {v v′ t t′}  lam v t  lam v′ t′  v  v′ × t  t′
lam-injective = < lam-injective₁ , lam-injective₂ >

pat-lam-injective₁ :  {cs cs′ args args′}  pat-lam cs args  pat-lam cs′ args′  cs  cs′
pat-lam-injective₁ refl = refl

pat-lam-injective₂ :  {cs cs′ args args′}  pat-lam cs args  pat-lam cs′ args′  args  args′
pat-lam-injective₂ refl = refl

pat-lam-injective :  {cs cs′ args args′}  pat-lam cs args  pat-lam cs′ args′  cs  cs′ × args  args′
pat-lam-injective = < pat-lam-injective₁ , pat-lam-injective₂ >

pi-injective₁ :  {t₁ t₁′ t₂ t₂′}  pi t₁ t₂  pi t₁′ t₂′  t₁  t₁′
pi-injective₁ refl = refl

pi-injective₂ :  {t₁ t₁′ t₂ t₂′}  pi t₁ t₂  pi t₁′ t₂′  t₂  t₂′
pi-injective₂ refl = refl

pi-injective :  {t₁ t₁′ t₂ t₂′}  pi t₁ t₂  pi t₁′ t₂′  t₁  t₁′ × t₂  t₂′
pi-injective = < pi-injective₁ , pi-injective₂ >

sort-injective :  {x y}  sort x  sort y  x  y
sort-injective refl = refl

lit-injective :  {x y}  lit x  lit y  x  y
lit-injective refl = refl

set-injective :  {x y}  set x  set y  x  y
set-injective refl = refl

slit-injective :  {x y}  Sort.lit x  lit y  x  y
slit-injective refl = refl

prop-injective :  {x y}  prop x  prop y  x  y
prop-injective refl = refl

propLit-injective :  {x y}  propLit x  propLit y  x  y
propLit-injective refl = refl

inf-injective :  {x y}  inf x  inf y  x  y
inf-injective refl = refl

var x args  var x′ args′ =
  map′ (uncurry (cong₂ var)) var-injective (x ℕ.≟ x′ ×-dec args ≟-Args args′)
con c args  con c′ args′ =
  map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×-dec args ≟-Args args′)
def f args  def f′ args′ =
  map′ (uncurry (cong₂ def)) def-injective (f Name.≟ f′ ×-dec args ≟-Args args′)
meta x args  meta x′ args′ =
  map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≟ x′   ×-dec args ≟-Args args′)
lam v t     lam v′ t′    =
  map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≟ v′ ×-dec t ≟-AbsTerm t′)
pat-lam cs args  pat-lam cs′ args′ =
  map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≟-Clauses cs′ ×-dec args ≟-Args args′)
pi t₁ t₂    pi t₁′ t₂′   =
  map′ (uncurry (cong₂ pi))  pi-injective (t₁ ≟-ArgType t₁′  ×-dec t₂ ≟-AbsType t₂′)
sort s      sort s′      = map′ (cong sort)  sort-injective (s ≟-Sort s′)
lit l       lit l′       = map′ (cong lit)   lit-injective (l Literal.≟ l′)
unknown     unknown      = yes refl

var x args  con c args′ = no λ()
var x args  def f args′ = no λ()
var x args  lam v t     = no λ()
var x args  pi t₁ t₂    = no λ()
var x args  sort _      = no λ()
var x args  lit _      = no λ()
var x args  meta _ _    = no λ()
var x args  unknown     = no λ()
con c args  var x args′ = no λ()
con c args  def f args′ = no λ()
con c args  lam v t     = no λ()
con c args  pi t₁ t₂    = no λ()
con c args  sort _      = no λ()
con c args  lit _      = no λ()
con c args  meta _ _    = no λ()
con c args  unknown     = no λ()
def f args  var x args′ = no λ()
def f args  con c args′ = no λ()
def f args  lam v t     = no λ()
def f args  pi t₁ t₂    = no λ()
def f args  sort _      = no λ()
def f args  lit _      = no λ()
def f args  meta _ _    = no λ()
def f args  unknown     = no λ()
lam v t     var x args  = no λ()
lam v t     con c args  = no λ()
lam v t     def f args  = no λ()
lam v t     pi t₁ t₂    = no λ()
lam v t     sort _      = no λ()
lam v t     lit _      = no λ()
lam v t     meta _ _    = no λ()
lam v t     unknown     = no λ()
pi t₁ t₂    var x args  = no λ()
pi t₁ t₂    con c args  = no λ()
pi t₁ t₂    def f args  = no λ()
pi t₁ t₂    lam v t     = no λ()
pi t₁ t₂    sort _      = no λ()
pi t₁ t₂    lit _      = no λ()
pi t₁ t₂    meta _ _    = no λ()
pi t₁ t₂    unknown     = no λ()
sort _      var x args  = no λ()
sort _      con c args  = no λ()
sort _      def f args  = no λ()
sort _      lam v t     = no λ()
sort _      pi t₁ t₂    = no λ()
sort _      lit _       = no λ()
sort _      meta _ _    = no λ()
sort _      unknown     = no λ()
lit _      var x args  = no λ()
lit _      con c args  = no λ()
lit _      def f args  = no λ()
lit _      lam v t     = no λ()
lit _      pi t₁ t₂    = no λ()
lit _      sort _      = no λ()
lit _      meta _ _    = no λ()
lit _      unknown     = no λ()
meta _ _    var x args  = no λ()
meta _ _    con c args  = no λ()
meta _ _    def f args  = no λ()
meta _ _    lam v t     = no λ()
meta _ _    pi t₁ t₂    = no λ()
meta _ _    sort _      = no λ()
meta _ _    lit _       = no λ()
meta _ _    unknown     = no λ()
unknown     var x args  = no λ()
unknown     con c args  = no λ()
unknown     def f args  = no λ()
unknown     lam v t     = no λ()
unknown     pi t₁ t₂    = no λ()
unknown     sort _      = no λ()
unknown     lit _       = no λ()
unknown     meta _ _    = no λ()
pat-lam _ _  var x args  = no λ()
pat-lam _ _  con c args  = no λ()
pat-lam _ _  def f args  = no λ()
pat-lam _ _  lam v t     = no λ()
pat-lam _ _  pi t₁ t₂    = no λ()
pat-lam _ _  sort _      = no λ()
pat-lam _ _  lit _       = no λ()
pat-lam _ _  meta _ _    = no λ()
pat-lam _ _  unknown     = no λ()
var x args   pat-lam _ _ = no λ()
con c args   pat-lam _ _ = no λ()
def f args   pat-lam _ _ = no λ()
lam v t      pat-lam _ _ = no λ()
pi t₁ t₂     pat-lam _ _ = no λ()
sort _       pat-lam _ _ = no λ()
lit _        pat-lam _ _ = no λ()
meta _ _     pat-lam _ _ = no λ()
unknown      pat-lam _ _ = no λ()

set t   ≟-Sort set t′  = map′ (cong set) set-injective (t  t′)
lit n   ≟-Sort lit n′  = map′ (cong lit) slit-injective (n ℕ.≟ n′)
prop t   ≟-Sort prop t′  = map′ (cong prop) prop-injective (t  t′)
propLit n   ≟-Sort propLit n′  = map′ (cong propLit) propLit-injective (n ℕ.≟ n′)
inf n   ≟-Sort inf n′  = map′ (cong inf) inf-injective (n ℕ.≟ n′)
unknown ≟-Sort unknown = yes refl
set _   ≟-Sort lit _   = no λ()
set _   ≟-Sort prop _   = no λ()
set _   ≟-Sort propLit _   = no λ()
set _   ≟-Sort inf _   = no λ()
set _   ≟-Sort unknown = no λ()
lit _   ≟-Sort set _   = no λ()
lit _   ≟-Sort prop _   = no λ()
lit _   ≟-Sort propLit _   = no λ()
lit _   ≟-Sort inf _   = no λ()
lit _   ≟-Sort unknown = no λ()
prop _  ≟-Sort set _   = no λ()
prop _  ≟-Sort lit _   = no λ()
prop _  ≟-Sort propLit _   = no λ()
prop _  ≟-Sort inf _   = no λ()
prop _  ≟-Sort unknown   = no λ()
propLit _  ≟-Sort set _   = no λ()
propLit _  ≟-Sort lit _   = no λ()
propLit _  ≟-Sort prop _   = no λ()
propLit _  ≟-Sort inf _   = no λ()
propLit _  ≟-Sort unknown   = no λ()
inf _  ≟-Sort set _   = no λ()
inf _  ≟-Sort lit _   = no λ()
inf _  ≟-Sort prop _   = no λ()
inf _  ≟-Sort propLit _   = no λ()
inf _  ≟-Sort unknown   = no λ()
unknown ≟-Sort set _   = no λ()
unknown ≟-Sort lit _   = no λ()
unknown ≟-Sort prop _   = no λ()
unknown ≟-Sort propLit _   = no λ()
unknown ≟-Sort inf _   = no λ()


pat-con-injective₁ :  {c c′ args args′}  Pattern.con c args  con c′ args′  c  c′
pat-con-injective₁ refl = refl

pat-con-injective₂ :  {c c′ args args′}  Pattern.con c args  con c′ args′  args  args′
pat-con-injective₂ refl = refl

pat-con-injective :  {c c′ args args′}  Pattern.con c args  con c′ args′  c  c′ × args  args′
pat-con-injective = < pat-con-injective₁ , pat-con-injective₂ >

pat-var-injective :  {x y}  var x  var y  x  y
pat-var-injective refl = refl

pat-lit-injective :  {x y}  Pattern.lit x  lit y  x  y
pat-lit-injective refl = refl

proj-injective :  {x y}  proj x  proj y  x  y
proj-injective refl = refl

dot-injective :  {x y}  dot x  dot y  x  y
dot-injective refl = refl

absurd-injective :  {x y}  absurd x  absurd y  x  y
absurd-injective refl = refl

con c ps ≟-Pattern con c′ ps′ = map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≟ c′ ×-dec ps ≟-Patterns ps′)
var x    ≟-Pattern var x′     = map′ (cong var) pat-var-injective (x ℕ.≟ x′)
lit l    ≟-Pattern lit l′     = map′ (cong lit) pat-lit-injective (l Literal.≟ l′)
proj a   ≟-Pattern proj a′    = map′ (cong proj) proj-injective (a Name.≟ a′)
dot t    ≟-Pattern dot t′     = map′ (cong dot) dot-injective (t  t′)
absurd x ≟-Pattern absurd x′  = map′ (cong absurd) absurd-injective (x ℕ.≟ x′)

con x x₁ ≟-Pattern dot x₂ = no  ())
con x x₁ ≟-Pattern var x₂ = no  ())
con x x₁ ≟-Pattern lit x₂ = no  ())
con x x₁ ≟-Pattern proj x₂ = no  ())
con x x₁ ≟-Pattern absurd x₂ = no  ())
dot x ≟-Pattern con x₁ x₂ = no  ())
dot x ≟-Pattern var x₁ = no  ())
dot x ≟-Pattern lit x₁ = no  ())
dot x ≟-Pattern proj x₁ = no  ())
dot x ≟-Pattern absurd x₁ = no  ())
var s ≟-Pattern con x x₁ = no  ())
var s ≟-Pattern dot x = no  ())
var s ≟-Pattern lit x = no  ())
var s ≟-Pattern proj x = no  ())
var s ≟-Pattern absurd x = no  ())
lit x ≟-Pattern con x₁ x₂ = no  ())
lit x ≟-Pattern dot x₁ = no  ())
lit x ≟-Pattern var _ = no  ())
lit x ≟-Pattern proj x₁ = no  ())
lit x ≟-Pattern absurd x₁ = no  ())
proj x ≟-Pattern con x₁ x₂ = no  ())
proj x ≟-Pattern dot x₁ = no  ())
proj x ≟-Pattern var _ = no  ())
proj x ≟-Pattern lit x₁ = no  ())
proj x ≟-Pattern absurd x₁ = no  ())
absurd x ≟-Pattern con x₁ x₂ = no  ())
absurd x ≟-Pattern dot x₁ = no  ())
absurd x ≟-Pattern var _ = no  ())
absurd x ≟-Pattern lit x₁ = no  ())
absurd x ≟-Pattern proj x₁ = no  ())

[]             ≟-Patterns []             = yes refl
(arg i p  xs) ≟-Patterns (arg j q  ys) = ∷-dec (unArg-dec (p ≟-Pattern q)) (xs ≟-Patterns ys)

[]      ≟-Patterns (_  _) = no λ()
(_  _) ≟-Patterns []      = no λ()