module 1Lab.Reflection where

open import Prim.Data.String public
open import Prim.Data.Float public
open import Prim.Data.Maybe public
open import Data.Maybe.Base using (maybe→alt) public
open import Prim.Data.Word public
open import Meta.Traverse public
open import Meta.Idiom public
open import Meta.Bind public
open import Meta.Alt public

open Data.Vec.Base using (Vec ; [] ; _∷_ ; lookup ; tabulate) public
open Data.Product.NAry using ([_]) public
open Data.List.Base public
open Data.Bool public

MetaprogrammingπŸ”—

Here, we bind and define helpers for Agda’s clunky metaprogramming facilities.

QNamesπŸ”—

The β€œQ” is for qualified.

postulate Name : Type
{-# BUILTIN QNAME Name #-}

primitive
  primQNameEquality : Name β†’ Name β†’ Bool
  primQNameLess     : Name β†’ Name β†’ Bool
  primShowQName     : Name β†’ String

Fixity declarationsπŸ”—

The fixity of an identifier is given by an associativity (left, right or neither), and a precedence.

data Associativity : Type where
  left-assoc  : Associativity
  right-assoc : Associativity
  non-assoc   : Associativity

data Precedence : Type where
  related   : Float β†’ Precedence
  unrelated : Precedence

data Fixity : Type where
  fixity : Associativity β†’ Precedence β†’ Fixity

{-# BUILTIN ASSOC      Associativity #-}
{-# BUILTIN ASSOCLEFT  left-assoc    #-}
{-# BUILTIN ASSOCRIGHT right-assoc   #-}
{-# BUILTIN ASSOCNON   non-assoc     #-}

{-# BUILTIN PRECEDENCE    Precedence #-}
{-# BUILTIN PRECRELATED   related    #-}
{-# BUILTIN PRECUNRELATED unrelated  #-}

{-# BUILTIN FIXITY       Fixity #-}
{-# BUILTIN FIXITYFIXITY fixity #-}

primitive
  primQNameFixity : Name β†’ Fixity
  primQNameToWord64s : Name β†’ Word64 Γ— Word64

MetavariablesπŸ”—

Metavariables are reflected, essentially, as natural numbers. Thus they can be shown and tested for equality.

postulate Meta : Type
{-# BUILTIN AGDAMETA Meta #-}

primitive
  primMetaEquality : Meta β†’ Meta β†’ Bool
  primMetaLess     : Meta β†’ Meta β†’ Bool
  primShowMeta     : Meta β†’ String
  primMetaToNat    : Meta β†’ Nat

data Blocker : Type where
  blockerAny  : List Blocker β†’ Blocker
  blockerAll  : List Blocker β†’ Blocker
  blockerMeta : Meta β†’ Blocker

{-# BUILTIN AGDABLOCKER     Blocker #-}
{-# BUILTIN AGDABLOCKERANY  blockerAny #-}
{-# BUILTIN AGDABLOCKERALL  blockerAll #-}
{-# BUILTIN AGDABLOCKERMETA blockerMeta #-}

ArgumentsπŸ”—

An argument is the data that specifies the domain of a pi-abstraction. More than just a type, arguments have a visibility, a relevance, and a Quantity.

-- Arguments can be (visible), {hidden}, or {{instance}}.
data Visibility : Type where
  visible hidden instanceβ€² : Visibility

{-# BUILTIN HIDING   Visibility #-}
{-# BUILTIN VISIBLE  visible    #-}
{-# BUILTIN HIDDEN   hidden     #-}
{-# BUILTIN INSTANCE instanceβ€²  #-}

-- Arguments can be relevant or irrelevant.
data Relevance : Type where
  relevant irrelevant : Relevance

{-# BUILTIN RELEVANCE  Relevance  #-}
{-# BUILTIN RELEVANT   relevant   #-}
{-# BUILTIN IRRELEVANT irrelevant #-}

-- Arguments also have a quantity.
data Quantity : Type where
  quantity-0 quantity-Ο‰ : Quantity

{-# BUILTIN QUANTITY   Quantity   #-}
{-# BUILTIN QUANTITY-0 quantity-0 #-}
{-# BUILTIN QUANTITY-Ο‰ quantity-Ο‰ #-}

Packaging a Relevance and a Quantity gets you a Modality; A modality and a Visibility make an ArgInfo. An ArgInfo and something else makes an Arg. Got it?

record Modality : Type where
  constructor modality
  field
    r : Relevance
    q : Quantity

{-# BUILTIN MODALITY             Modality #-}
{-# BUILTIN MODALITY-CONSTRUCTOR modality #-}

record ArgInfo : Type where
  constructor arginfo
  field
    arg-vis : Visibility
    arg-modality : Modality

record Arg {a} (A : Type a) : Type a where
  constructor arg
  field
    arg-info : ArgInfo
    unarg : A

{-# BUILTIN ARGINFO    ArgInfo  #-}
{-# BUILTIN ARGARGINFO arginfo #-}
{-# BUILTIN ARG        Arg      #-}
{-# BUILTIN ARGARG     arg      #-}

AbstractionsπŸ”—

Pairs of strings and things are called Abstractions.

record Abs {a} (A : Type a) : Type a where
  constructor abs
  field
    abs-name : String
    abs-binder : A

{-# BUILTIN ABS    Abs #-}
{-# BUILTIN ABSABS abs #-}

LiteralsπŸ”—

Reflecting all of Agda’s built-in types, we have Literals. As a bonus, there are also metavariable literals!

data Literal : Type where
  nat    : (n : Nat)    β†’ Literal
  word64 : (n : Word64) β†’ Literal
  float  : (x : Float)  β†’ Literal
  char   : (c : Char)   β†’ Literal
  string : (s : String) β†’ Literal
  name   : (x : Name)   β†’ Literal
  meta   : (x : Meta)   β†’ Literal

{-# BUILTIN AGDALITERAL   Literal #-}
{-# BUILTIN AGDALITNAT    nat     #-}
{-# BUILTIN AGDALITWORD64 word64  #-}
{-# BUILTIN AGDALITFLOAT  float   #-}
{-# BUILTIN AGDALITCHAR   char    #-}
{-# BUILTIN AGDALITSTRING string  #-}
{-# BUILTIN AGDALITQNAME  name    #-}
{-# BUILTIN AGDALITMETA   meta    #-}

Agda’s syntaxπŸ”—

And now we finally get to Agda’s syntax.

data Term    : Type
data Sort    : Type
data Pattern : Type
data Clause  : Type
Telescope = List (String Γ— Arg Term)

data Term where
  var       : (x : Nat) (args : List (Arg Term)) β†’ Term
  con       : (c : Name) (args : List (Arg Term)) β†’ Term
  def       : (f : Name) (args : List (Arg Term)) β†’ Term
  lam       : (v : Visibility) (t : Abs Term) β†’ Term
  pat-lam   : (cs : List Clause) (args : List (Arg Term)) β†’ Term
  pi        : (a : Arg Term) (b : Abs Term) β†’ Term
  agda-sort : (s : Sort) β†’ Term
  lit       : (l : Literal) β†’ Term
  meta      : (x : Meta) β†’ List (Arg Term) β†’ Term
  unknown   : Term

data Sort where
  set     : (t : Term) β†’ Sort
  lit     : (n : Nat) β†’ Sort
  prop    : (t : Term) β†’ Sort
  propLit : (n : Nat) β†’ Sort
  inf     : (n : Nat) β†’ Sort
  unknown : Sort

data Pattern where
  con    : (c : Name) (ps : List (Arg Pattern)) β†’ Pattern
  dot    : (t : Term)    β†’ Pattern
  var    : (x : Nat)     β†’ Pattern
  lit    : (l : Literal) β†’ Pattern
  proj   : (f : Name)    β†’ Pattern
  absurd : (x : Nat)     β†’ Pattern  -- absurd patterns counts as variables

data Clause where
  clause        : (tel : Telescope) (ps : List (Arg Pattern)) (t : Term) β†’ Clause
  absurd-clause : (tel : Telescope) (ps : List (Arg Pattern)) β†’ Clause

data Definition : Type where
  function    : (cs : List Clause) β†’ Definition
  data-type   : (pars : Nat) (cs : List Name) β†’ Definition
  record-type : (c : Name) (fs : List (Arg Name)) β†’ Definition
  data-cons   : (d : Name) β†’ Definition
  axiom       : Definition
  prim-fun    : Definition

The TC monadπŸ”—

To drive meta computations, we have the TC monad, reflecting Agda’s TCM monad.

data ErrorPart : Type where
  strErr  : String β†’ ErrorPart
  termErr : Term β†’ ErrorPart
  pattErr : Pattern β†’ ErrorPart
  nameErr : Name β†’ ErrorPart

instance
  String-ErrorPart : IsString ErrorPart
  String-ErrorPart .IsString.Constraint _ = ⊀
  String-ErrorPart .IsString.fromString s = strErr s

postulate
  TC               : βˆ€ {a} β†’ Type a β†’ Type a
  returnTC         : βˆ€ {a} {A : Type a} β†’ A β†’ TC A
  bindTC           : βˆ€ {a b} {A : Type a} {B : Type b} β†’ TC A β†’ (A β†’ TC B) β†’ TC B
  unify            : Term β†’ Term β†’ TC ⊀
  typeError        : βˆ€ {a} {A : Type a} β†’ List ErrorPart β†’ TC A
  inferType        : Term β†’ TC Term
  checkType        : Term β†’ Term β†’ TC Term
  normalise        : Term β†’ TC Term
  reduce           : Term β†’ TC Term
  catchTC          : βˆ€ {a} {A : Type a} β†’ TC A β†’ TC A β†’ TC A
  quoteTC          : βˆ€ {a} {A : Type a} β†’ A β†’ TC Term
  unquoteTC        : βˆ€ {a} {A : Type a} β†’ Term β†’ TC A
  quoteΟ‰TC         : βˆ€ {A : TypeΟ‰} β†’ A β†’ TC Term
  getContext       : TC Telescope
  extendContext    : βˆ€ {a} {A : Type a} β†’ String β†’ Arg Term β†’ TC A β†’ TC A
  inContext        : βˆ€ {a} {A : Type a} β†’ Telescope β†’ TC A β†’ TC A
  freshName        : String β†’ TC Name
  declareDef       : Arg Name β†’ Term β†’ TC ⊀
  declarePostulate : Arg Name β†’ Term β†’ TC ⊀
  defineFun        : Name β†’ List Clause β†’ TC ⊀
  getType          : Name β†’ TC Term
  getDefinition    : Name β†’ TC Definition
  blockTC          : βˆ€ {a} {A : Type a} β†’ Blocker β†’ TC A
  commitTC         : TC ⊀
  isMacro          : Name β†’ TC Bool

  formatErrorParts : List ErrorPart β†’ TC String

  -- Prints the third argument if the corresponding verbosity level is turned
  -- on (with the -v flag to Agda).
  debugPrint : String β†’ Nat β†’ List ErrorPart β†’ TC ⊀

  -- If 'true', makes the following primitives also normalise
  -- their results: inferType, checkType, quoteTC, getType, and getContext
  withNormalisation : βˆ€ {a} {A : Type a} β†’ Bool β†’ TC A β†’ TC A
  askNormalisation  : TC Bool

  -- If 'true', makes the following primitives to reconstruct hidden arguments:
  -- getDefinition, normalise, reduce, inferType, checkType and getContext
  withReconstructed : βˆ€ {a} {A : Type a} β†’ Bool β†’ TC A β†’ TC A
  askReconstructed  : TC Bool

  -- Whether implicit arguments at the end should be turned into metavariables
  withExpandLast : βˆ€ {a} {A : Type a} β†’ Bool β†’ TC A β†’ TC A
  askExpandLast  : TC Bool

  -- White/blacklist specific definitions for reduction while executing the TC computation
  -- 'true' for whitelist, 'false' for blacklist
  withReduceDefs : βˆ€ {a} {A : Type a} β†’ (Ξ£ Bool Ξ» _ β†’ List Name) β†’ TC A β†’ TC A
  askReduceDefs  : TC (Ξ£ Bool Ξ» _ β†’ List Name)

  -- Fail if the given computation gives rise to new, unsolved
  -- "blocking" constraints.
  noConstraints : βˆ€ {a} {A : Type a} β†’ TC A β†’ TC A

  -- Run the given TC action and return the first component. Resets to
  -- the old TC state if the second component is 'false', or keep the
  -- new TC state if it is 'true'.
  runSpeculative : βˆ€ {a} {A : Type a} β†’ TC (Ξ£ A Ξ» _ β†’ Bool) β†’ TC A

  -- Get a list of all possible instance candidates for the given meta
  -- variable (it does not have to be an instance meta).
  getInstances : Meta β†’ TC (List Term)

  declareData      : Name β†’ Nat β†’ Term β†’ TC ⊀
  defineData       : Name β†’ List (Ξ£ Name (Ξ» _ β†’ Term)) β†’ TC ⊀
And now we bind the whole shebang above to the BUILTINs that Agda knows about.
{-# BUILTIN AGDATERM      Term    #-}
{-# BUILTIN AGDASORT      Sort    #-}
{-# BUILTIN AGDAPATTERN   Pattern #-}
{-# BUILTIN AGDACLAUSE    Clause  #-}

{-# BUILTIN AGDATERMVAR         var       #-}
{-# BUILTIN AGDATERMCON         con       #-}
{-# BUILTIN AGDATERMDEF         def       #-}
{-# BUILTIN AGDATERMMETA        meta      #-}
{-# BUILTIN AGDATERMLAM         lam       #-}
{-# BUILTIN AGDATERMEXTLAM      pat-lam   #-}
{-# BUILTIN AGDATERMPI          pi        #-}
{-# BUILTIN AGDATERMSORT        agda-sort #-}
{-# BUILTIN AGDATERMLIT         lit       #-}
{-# BUILTIN AGDATERMUNSUPPORTED unknown   #-}

{-# BUILTIN AGDASORTSET         set     #-}
{-# BUILTIN AGDASORTLIT         lit     #-}
{-# BUILTIN AGDASORTPROP        prop    #-}
{-# BUILTIN AGDASORTPROPLIT     propLit #-}
{-# BUILTIN AGDASORTINF         inf     #-}
{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}

{-# BUILTIN AGDAERRORPART       ErrorPart #-}
{-# BUILTIN AGDAERRORPARTSTRING strErr    #-}
{-# BUILTIN AGDAERRORPARTTERM   termErr   #-}
{-# BUILTIN AGDAERRORPARTPATT   pattErr   #-}
{-# BUILTIN AGDAERRORPARTNAME   nameErr   #-}

{-# BUILTIN AGDADEFINITION                Definition  #-}
{-# BUILTIN AGDADEFINITIONFUNDEF          function    #-}
{-# BUILTIN AGDADEFINITIONDATADEF         data-type   #-}
{-# BUILTIN AGDADEFINITIONRECORDDEF       record-type #-}
{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons   #-}
{-# BUILTIN AGDADEFINITIONPOSTULATE       axiom       #-}
{-# BUILTIN AGDADEFINITIONPRIMITIVE       prim-fun    #-}

{-# BUILTIN AGDAPATCON    con     #-}
{-# BUILTIN AGDAPATDOT    dot     #-}
{-# BUILTIN AGDAPATVAR    var     #-}
{-# BUILTIN AGDAPATLIT    lit     #-}
{-# BUILTIN AGDAPATPROJ   proj    #-}
{-# BUILTIN AGDAPATABSURD absurd  #-}

{-# BUILTIN AGDACLAUSECLAUSE clause        #-}
{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
{-# BUILTIN AGDATCM                           TC                         #-}
{-# BUILTIN AGDATCMRETURN                     returnTC                   #-}
{-# BUILTIN AGDATCMBIND                       bindTC                     #-}
{-# BUILTIN AGDATCMUNIFY                      unify                      #-}
{-# BUILTIN AGDATCMTYPEERROR                  typeError                  #-}
{-# BUILTIN AGDATCMINFERTYPE                  inferType                  #-}
{-# BUILTIN AGDATCMCHECKTYPE                  checkType                  #-}
{-# BUILTIN AGDATCMNORMALISE                  normalise                  #-}
{-# BUILTIN AGDATCMREDUCE                     reduce                     #-}
{-# BUILTIN AGDATCMCATCHERROR                 catchTC                    #-}
{-# BUILTIN AGDATCMQUOTETERM                  quoteTC                    #-}
{-# BUILTIN AGDATCMUNQUOTETERM                unquoteTC                  #-}
{-# BUILTIN AGDATCMQUOTEOMEGATERM             quoteωTC                   #-}
{-# BUILTIN AGDATCMGETCONTEXT                 getContext                 #-}
{-# BUILTIN AGDATCMEXTENDCONTEXT              extendContext              #-}
{-# BUILTIN AGDATCMINCONTEXT                  inContext                  #-}
{-# BUILTIN AGDATCMFRESHNAME                  freshName                  #-}
{-# BUILTIN AGDATCMDECLAREDEF                 declareDef                 #-}
{-# BUILTIN AGDATCMDECLAREPOSTULATE           declarePostulate           #-}
{-# BUILTIN AGDATCMDEFINEFUN                  defineFun                  #-}
{-# BUILTIN AGDATCMGETTYPE                    getType                    #-}
{-# BUILTIN AGDATCMGETDEFINITION              getDefinition              #-}
{-# BUILTIN AGDATCMBLOCK                      blockTC                    #-}
{-# BUILTIN AGDATCMCOMMIT                     commitTC                   #-}
{-# BUILTIN AGDATCMISMACRO                    isMacro                    #-}
{-# BUILTIN AGDATCMWITHNORMALISATION          withNormalisation          #-}
{-# BUILTIN AGDATCMFORMATERRORPARTS           formatErrorParts           #-}
{-# BUILTIN AGDATCMDEBUGPRINT                 debugPrint                 #-}
{-# BUILTIN AGDATCMWITHRECONSTRUCTED          withReconstructed          #-}
{-# BUILTIN AGDATCMWITHEXPANDLAST             withExpandLast             #-}
{-# BUILTIN AGDATCMWITHREDUCEDEFS             withReduceDefs             #-}
{-# BUILTIN AGDATCMASKNORMALISATION           askNormalisation           #-}
{-# BUILTIN AGDATCMASKRECONSTRUCTED           askReconstructed           #-}
{-# BUILTIN AGDATCMASKEXPANDLAST              askExpandLast              #-}
{-# BUILTIN AGDATCMASKREDUCEDEFS              askReduceDefs              #-}
{-# BUILTIN AGDATCMNOCONSTRAINTS              noConstraints              #-}
{-# BUILTIN AGDATCMRUNSPECULATIVE             runSpeculative             #-}
{-# BUILTIN AGDATCMGETINSTANCES               getInstances               #-}
{-# BUILTIN AGDATCMDECLAREDATA                declareData                #-}
{-# BUILTIN AGDATCMDEFINEDATA                 defineData                 #-}

instance
  Map-TC : Map (eff TC)
  Map-TC .Map._<$>_ f x = bindTC x Ξ» x β†’ returnTC (f x)

  Idiom-TC : Idiom (eff TC)
  Idiom-TC .Idiom.pure = returnTC
  Idiom-TC .Idiom._<*>_ f g = bindTC f Ξ» f β†’ bindTC g Ξ» g β†’ pure (f g)

  Bind-TC : Bind (eff TC)
  Bind-TC .Bind._>>=_ = bindTC

  Alt-TC : Alt (eff TC)
  Alt-TC .Alt.failβ€² xs = typeError [ strErr xs ]
  Alt-TC .Alt._<|>_ = catchTC

Reflection helpersπŸ”—

argH0 argH argN : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ Arg A
argH = arg (arginfo hidden (modality relevant quantity-Ο‰))
argH0 = arg (arginfo hidden (modality relevant quantity-0))
argN = arg (arginfo visible (modality relevant quantity-Ο‰))

Fun : βˆ€ {β„“ β„“'} β†’ Type β„“ β†’ Type β„“' β†’ Type (β„“ βŠ” β„“')
Fun A B = A β†’ B

idfun : βˆ€ {β„“} (A : Type β„“) β†’ A β†’ A
idfun A x = x

underAbs : βˆ€ {β„“} {A : Type β„“} β†’ Term β†’ TC A β†’ TC A
underAbs (lam v (abs nm _)) m = extendContext nm (arg (arginfo v (modality relevant quantity-Ο‰)) unknown) m
underAbs (pi a (abs nm _)) m = extendContext nm a m
underAbs _ m = m

new-meta : Term β†’ TC Term
new-meta ty = do
  mv ← checkType unknown ty
  debugPrint "tactic.meta" 70
    [ "Created new meta " , termErr mv , " of type " , termErr ty ]
  pure mv

new-metaβ€² : Term β†’ TC (Meta Γ— Term)
new-metaβ€² ty = do
  tm@(meta mv _) ← checkType unknown ty
    where _ β†’ typeError $ [ "impossible new-metaβ€²" ]
  debugPrint "tactic.meta" 70
    [ "Created new meta " , termErr tm , " of type " , termErr tm ]
  pure (mv , tm)

blockOnMeta   : βˆ€ {a} {A : Type a} β†’ Meta β†’ TC A
blockOnMeta m = blockTC (blockerMeta m)

vlam : String β†’ Term β†’ Term
vlam nam body = lam visible (abs nam body)

pattern _v∷_ t xs = arg (arginfo visible (modality relevant quantity-Ο‰)) t ∷ xs
pattern _h∷_ t xs = arg (arginfo hidden (modality relevant quantity-Ο‰)) t ∷ xs
pattern _hm∷_ t xs = arg (arginfo hidden (modality relevant _)) t ∷ xs

infixr 30 _v∷_ _h∷_ _hm∷_

infer-hidden : Nat β†’ List (Arg Term) β†’ List (Arg Term)
infer-hidden zero xs = xs
infer-hidden (suc n) xs = unknown h∷ infer-hidden n xs

getName : Term β†’ Maybe Name
getName (def x _) = just x
getName (con x _) = just x
getName _ = nothing

_name=?_ : Name β†’ Name β†’ Bool
x name=? y = primQNameEquality x y

_visibility=?_ : Visibility β†’ Visibility β†’ Bool
visible visibility=? visible = true
hidden visibility=? hidden = true
instanceβ€² visibility=? instanceβ€² = true
_ visibility=? _ = false

-- [TODO: Reed M, 06/05/2022] We don't actually use any fancy modalities
-- anywhere AFAICT, so let's ignore those.
_arginfo=?_ : ArgInfo β†’ ArgInfo β†’ Bool
arginfo v₁ m₁ arginfo=? arginfo vβ‚‚ mβ‚‚ = (v₁ visibility=? vβ‚‚)

arg=? : βˆ€ {a} {A : Type a} β†’ (A β†’ A β†’ Bool) β†’ Arg A β†’ Arg A β†’ Bool
arg=? eq=? (arg i₁ x) (arg iβ‚‚ y) = and (i₁ arginfo=? iβ‚‚) (eq=? x y)

-- We want to compare terms up to Ξ±-equivalence, so we ignore binder
-- names.
abs=? : βˆ€ {a} {A : Type a} β†’ (A β†’ A β†’ Bool) β†’ Abs A β†’ Abs A β†’ Bool
abs=? eq=? (abs _ x) (abs _ y) = eq=? x y

{-# TERMINATING #-}
-- [TODO: Reed M, 06/05/2022] Finish this

_term=?_ : Term β†’ Term β†’ Bool
var nm₁ args₁ term=? var nmβ‚‚ argsβ‚‚ = and (nm₁ == nmβ‚‚) (all=? (arg=? _term=?_) args₁ argsβ‚‚)
con c₁ args₁ term=? con cβ‚‚ argsβ‚‚ = and (c₁ name=? cβ‚‚) (all=? (arg=? _term=?_) args₁ argsβ‚‚)
def f₁ args₁ term=? def fβ‚‚ argsβ‚‚ = and (f₁ name=? fβ‚‚) (all=? (arg=? _term=?_) args₁ argsβ‚‚)
lam v₁ t₁ term=? lam vβ‚‚ tβ‚‚ = and (v₁ visibility=? vβ‚‚) (abs=? _term=?_ t₁ tβ‚‚)
pat-lam cs₁ args₁ term=? pat-lam csβ‚‚ argsβ‚‚ = false
pi a₁ b₁ term=? pi aβ‚‚ bβ‚‚ = and (arg=? _term=?_ a₁ aβ‚‚) (abs=? _term=?_ b₁ bβ‚‚)
agda-sort s term=? tβ‚‚ = false
lit l term=? tβ‚‚ = false
meta x x₁ term=? tβ‚‚ = false
unknown term=? tβ‚‚ = false
_ term=? _ = false

β€œrefl” : Term
β€œrefl” = def (quote refl) []

wait-for-args : List (Arg Term) β†’ TC (List (Arg Term))
wait-for-type : Term β†’ TC Term

wait-for-type (var x args) = var x <$> wait-for-args args
wait-for-type (con c args) = con c <$> wait-for-args args
wait-for-type (def f args) = def f <$> wait-for-args args
wait-for-type (lam v (abs x t)) = pure (lam v (abs x t))
wait-for-type (pat-lam cs args) = pure (pat-lam cs args)
wait-for-type (pi (arg i a) (abs x b)) = do
  a ← wait-for-type a
  b ← wait-for-type b
  pure (pi (arg i a) (abs x b))
wait-for-type (agda-sort s) = pure (agda-sort s)
wait-for-type (lit l) = pure (lit l)
wait-for-type (meta x x₁) = blockOnMeta x
wait-for-type unknown = pure unknown

wait-for-args [] = pure []
wait-for-args (arg i a ∷ xs) = ⦇ ⦇ (arg i) (wait-for-type a) ⦈ ∷ wait-for-args xs ⦈

wait-just-a-bit : Term β†’ TC Term
wait-just-a-bit (meta m _) = blockOnMeta m
wait-just-a-bit tm = pure tm

unapply-path : Term β†’ TC (Maybe (Term Γ— Term Γ— Term))
unapply-path red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) = do
  domain ← new-meta (def (quote Type) (l v∷ []))
  ty ← pure (def (quote Path) (domain v∷ x v∷ y v∷ []))
  debugPrint "tactic" 50
    [ "(no reduction) unapply-path: got a "
    , termErr red
    , " but I really want it to be "
    , termErr ty
    ]
  unify red ty
  pure (just (domain , x , y))
unapply-path tm = reduce tm >>= Ξ» where
  tm@(meta _ _) β†’ do
    dom ← new-meta (def (quote Type) (unknown v∷ []))
    l ← new-meta dom
    r ← new-meta dom
    unify tm (def (quote Path) (dom v∷ l v∷ r v∷ []))
    traverse wait-for-type (l ∷ r ∷ [])
    pure (just (dom , l , r))
  red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) β†’ do
    domain ← new-meta (def (quote Type) (l v∷ []))
    ty ← pure (def (quote Path) (domain v∷ x v∷ y v∷ []))
    debugPrint "tactic" 50
      [ "unapply-path: got a "
      , termErr red
      , " but I really want it to be "
      , termErr ty
      ]
    unify red ty
    pure (just (domain , x , y))
  _ β†’ returnTC nothing

get-boundary : Term β†’ TC (Maybe (Term Γ— Term))
get-boundary tm = unapply-path tm >>= Ξ» where
  (just (_ , x , y)) β†’ pure (just (x , y))
  nothing            β†’ pure nothing

Debugging ToolsπŸ”—

debug! : βˆ€ {β„“} {A : Type β„“} β†’ Term β†’ TC A
debug! tm = typeError ("[DEBUG]: " ∷ termErr tm ∷ [])

quote-repr-macro : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ Term β†’  TC ⊀
quote-repr-macro a hole = do
  tm ← quoteTC a
  repr ← quoteTC tm
  typeError $ "The term\n  "
    ∷ termErr tm
    ∷ "\nHas quoted representation\n  "
    ∷ termErr repr ∷ []

macro
  quote-repr! : βˆ€ {β„“ β„“β€²} {A : Type β„“} {B : Type β„“β€²} β†’ A β†’ Term β†’ TC ⊀
  quote-repr! a = quote-repr-macro a

instance
  IsString-Error : IsString (List ErrorPart)
  IsString-Error .IsString.Constraint _ = ⊀
  IsString-Error .fromString s = fromString s ∷ []

unify-loudly : Term β†’ Term β†’ TC ⊀
unify-loudly a b = do
  debugPrint "tactic" 50 $ termErr a ∷ " =? " ∷ termErr b ∷ []
  unify a b

print-depth : String β†’ Nat β†’ Nat β†’ List ErrorPart β†’ TC ⊀
print-depth key level nesting es = debugPrint key level $
  strErr (nest nesting ("[" <> primShowNat nesting <> "]  ")) ∷ es
  where
    _<>_ : String β†’ String β†’ String
    _<>_ = primStringAppend
    infixr 10 _<>_

    nest : Nat β†’ String β†’ String
    nest zero s = s
    nest (suc x) s = nest x (s <> "  ")