open import 1Lab.Path
open import 1Lab.Type hiding (absurd)

open import Data.Product.NAry
open import Data.List.Base
open import Data.Vec.Base
open import Data.Bool

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 <> "  ")