{-# OPTIONS --safe --cubical-compatible --no-sized-types --no-guardedness #-}

module SemanticExplanation.Reflection.View where

open import SemanticExplanation.Base
import Agda.Builtin.Reflection as R

data Head : Set where
  varHead     : Nat → Head
  conHead     : R.Name → Head
  defHead     : R.Name → Head
  litHead     : R.Literal → Head
  sortHead    : R.Sort → Head
  metaHead    : R.Meta → Head
  lamHead     : R.Visibility → Head
  piHead      : Head
  unsupported : Head

record SpineView : Set where
  constructor spine
  field
    head : Head
    args : List (R.Arg R.Term)

viewSpine : R.Term → SpineView
viewSpine (R.var x args) = spine (varHead x) args
viewSpine (R.con c args) = spine (conHead c) args
viewSpine (R.def f args) = spine (defHead f) args
viewSpine (R.lit l) = spine (litHead l) []
viewSpine (R.agda-sort s) = spine (sortHead s) []
viewSpine (R.meta m args) = spine (metaHead m) args
viewSpine (R.lam v _) = spine (lamHead v) []
viewSpine (R.pi _ _) = spine piHead []
viewSpine _ = spine unsupported []

record PiView : Set where
  constructor pi-view
  field
    info     : R.ArgInfo
    hint     : String
    domain   : R.Term
    codomain : R.Term

viewPi : R.Term → Maybe PiView
viewPi (R.pi (R.arg info domain) (R.abs hint codomain)) =
  just (pi-view info hint domain codomain)
viewPi _ = nothing

argTerm : R.Arg R.Term → R.Term
argTerm (R.arg _ term) = term

absTerm : R.Abs R.Term → R.Term
absTerm (R.abs _ term) = term

mutual
  occursAt : Nat → Nat → R.Term → Bool
  occursAt zero target term = true
  occursAt (suc fuel) target (R.var index args) with target ==N index
  ... | true = true
  ... | false = anyArgs fuel target args
  occursAt (suc fuel) target (R.con _ args) = anyArgs fuel target args
  occursAt (suc fuel) target (R.def _ args) = anyArgs fuel target args
  occursAt (suc fuel) target (R.lam _ body) =
    occursAt fuel (suc target) (absTerm body)
  occursAt (suc fuel) target (R.pat-lam _ _) = true
  occursAt (suc fuel) target (R.pi (R.arg _ domain) body)
    with occursAt fuel target domain
  ... | true = true
  ... | false = occursAt fuel (suc target) (absTerm body)
  occursAt (suc fuel) target (R.agda-sort (R.set level)) =
    occursAt fuel target level
  occursAt (suc fuel) target (R.agda-sort (R.prop level)) =
    occursAt fuel target level
  occursAt (suc fuel) target (R.meta _ args) = anyArgs fuel target args
  occursAt (suc fuel) target R.unknown = true
  occursAt (suc fuel) target _ = false

  anyArgs : Nat → Nat → List (R.Arg R.Term) → Bool
  anyArgs fuel target [] = false
  anyArgs fuel target (argument ∷ args) with occursAt fuel target (argTerm argument)
  ... | true = true
  ... | false = anyArgs fuel target args

binderOccurs : PiView → Bool
binderOccurs p = occursAt  zero (PiView.codomain p)