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

open import Data.Product.NAry
open import Data.String.Show
open import Data.List.Base
open import Data.Dec.Base
open import Data.Vec.Base
open import Data.Bool

open import Meta.Append

module 1Lab.Reflection where

open import Data.String.Base public
open import Meta.Traversable public
open import Data.Float.Base public
open import Data.Maybe.Base public
open import Data.Word.Base public
open import Meta.Idiom public
open import Meta.Bind public
open import Meta.Alt public

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

open import Data.Reflection.Fixity   public
open import Data.Reflection.Name     public
open import Data.Reflection.Meta     public
open import Data.Reflection.Argument public
open import Data.Reflection.Abs      public
open import Data.Reflection.Literal  public
open import Data.Reflection.Term     public
open import Data.Reflection.Error    public

The TC monadπŸ”—

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

private module P where
  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 ⊀
    infer-type        : Term β†’ TC Term
    check-type        : 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
    extend-context    : βˆ€ {a} {A : Type a} β†’ String β†’ Arg Term β†’ TC A β†’ TC A
    in-context        : βˆ€ {a} {A : Type a} β†’ Telescope β†’ TC A β†’ TC A
    freshName         : String β†’ TC Name
    declare           : Arg Name β†’ Term β†’ TC ⊀
    declare-postulate : Arg Name β†’ Term β†’ TC ⊀
    define-function   : Name β†’ List Clause β†’ TC ⊀
    get-type          : Name β†’ TC Term
    get-definition    : Name β†’ TC Definition
    blockTC           : βˆ€ {a} {A : Type a} β†’ Blocker β†’ TC A
    commitTC          : TC ⊀
    isMacro           : Name β†’ TC Bool

    typeError         : βˆ€ {a} {A : Type a} β†’ List ErrorPart β†’ TC A
    formatErrorParts  : List ErrorPart β†’ TC String
    debugPrint        : String β†’ Nat β†’ List ErrorPart β†’ TC ⊀

  -- If 'true', makes the following primitives also normalise
  -- their results: infer-type, check-type, quoteTC, get-type, 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:
  -- get-definition, normalise, reduce, infer-type, check-type 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 computation at the type level, allowing use of erased things.
    work-on-types : βˆ€ {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'.
    run-speculative : βˆ€ {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).
    get-instances : Meta β†’ TC (List Term)

    declareData      : Name β†’ Nat β†’ Term β†’ TC ⊀
    defineData       : Name β†’ List (Name Γ— Quantity Γ— Term) β†’ TC ⊀
And now we bind the whole shebang above to the BUILTINs that Agda knows about. 
  {-# BUILTIN AGDATCM                  TC                         #-}
  {-# BUILTIN AGDATCMRETURN            returnTC                   #-}
  {-# BUILTIN AGDATCMBIND              bindTC                     #-}
  {-# BUILTIN AGDATCMUNIFY             unify                      #-}
  {-# BUILTIN AGDATCMTYPEERROR         typeError                  #-}
  {-# BUILTIN AGDATCMINFERTYPE         infer-type                 #-}
  {-# BUILTIN AGDATCMCHECKTYPE         check-type                 #-}
  {-# BUILTIN AGDATCMNORMALISE         normalise                  #-}
  {-# BUILTIN AGDATCMREDUCE            reduce                     #-}
  {-# BUILTIN AGDATCMCATCHERROR        catchTC                    #-}
  {-# BUILTIN AGDATCMQUOTETERM         quoteTC                    #-}
  {-# BUILTIN AGDATCMUNQUOTETERM       unquoteTC                  #-}
  {-# BUILTIN AGDATCMQUOTEOMEGATERM    quoteωTC                   #-}
  {-# BUILTIN AGDATCMGETCONTEXT        getContext                 #-}
  {-# BUILTIN AGDATCMEXTENDCONTEXT     extend-context             #-}
  {-# BUILTIN AGDATCMINCONTEXT         in-context                 #-}
  {-# BUILTIN AGDATCMFRESHNAME         freshName                  #-}
  {-# BUILTIN AGDATCMDECLAREDEF        declare                    #-}
  {-# BUILTIN AGDATCMDECLAREPOSTULATE  declare-postulate          #-}
  {-# BUILTIN AGDATCMDEFINEFUN         define-function            #-}
  {-# BUILTIN AGDATCMGETTYPE           get-type                   #-}
  {-# BUILTIN AGDATCMGETDEFINITION     get-definition             #-}
  {-# 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 AGDATCMWORKONTYPES       work-on-types              #-}
  {-# BUILTIN AGDATCMRUNSPECULATIVE    run-speculative            #-}
  {-# BUILTIN AGDATCMGETINSTANCES      get-instances              #-}
  {-# BUILTIN AGDATCMDECLAREDATA       declareData                #-}
  {-# BUILTIN AGDATCMDEFINEDATA        defineData                 #-}

open P
  hiding ( returnTC ; bindTC ; catchTC )
  public

instance
  Map-TC : Map (eff TC)
  Map-TC .Map.map f x = P.bindTC x Ξ» x β†’ P.returnTC (f x)

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

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

  Alt-TC : Alt (eff TC)
  Alt-TC .Alt.fail  = P.typeError mempty
  Alt-TC .Alt._<|>_ = P.catchTC

Reflection helpersπŸ”—

Args : Type
Args = List (Arg Term)

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

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

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

extend-context* : βˆ€ {a} {A : Type a} β†’ Telescope β†’ TC A β†’ TC A
extend-context* [] a = a
extend-context* ((nm , tm) ∷ xs) a = extend-context nm tm (extend-context* xs a)

new-meta : Term β†’ TC Term
new-meta ty = do
  mv ← check-type 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 _) ← check-type unknown ty
    where _ β†’ typeError "impossible new-meta'"
  debugPrint "tactic.meta" 70
    [ "Created new meta " , termErr tm , " of type " , termErr tm ]
  pure (mv , tm)

block-on-meta : βˆ€ {a} {A : Type a} β†’ Meta β†’ TC A
block-on-meta m = blockTC (blocker-meta m)

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

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

infer-tel : Telescope β†’ Args
infer-tel tel = (Ξ» (_ , arg ai _) β†’ arg ai unknown) <$> tel

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

-- Run a TC computation and reset the state after. If the returned value
-- makes references to metas generated in the reset computation, you'll
-- probably get __IMPOSSIBLE__s!
resetting : βˆ€ {β„“} {A : Type β„“} β†’ TC A β†’ TC A
resetting k = run-speculative ((_, false) <$> k)

all-metas-in : Term β†’ List Blocker
all-metas-in tm = go tm [] where
  go  : Term β†’ List Blocker β†’ List Blocker
  go* : List (Arg Term) β†’ List Blocker β†’ List Blocker

  go (var _ args)             acc = go* args acc
  go (con _ args)             acc = go* args acc
  go (def _ args)             acc = go* args acc
  go (lam _ (abs _ t))        acc = go t acc
  go (pat-lam cs args)        acc = acc
  go (pi (arg _ a) (abs _ b)) acc = go a (go b acc)
  go (agda-sort s)            acc = acc
  go (lit l)                  acc = acc
  go (meta x args)            acc = go* args (blocker-meta x ∷ acc)
  go unknown                  acc = acc

  go* []             acc = acc
  go* (arg _ x ∷ xs) acc = go x (go* xs acc)

wait-for-type : Term β†’ TC Term
wait-for-type tm with all-metas-in tm
... | [] = pure tm
... | it = blockTC (blocker-all it)

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

blocking-meta : Term β†’ Maybe Blocker
blocking-meta* : List (Arg Term) β†’ Maybe Blocker

blocking-meta (var x as)       = nothing
blocking-meta (con c as)       = nothing
blocking-meta (def f as)       = blocking-meta* as
blocking-meta (lam v t)        = nothing
blocking-meta (pat-lam _ as)   = blocking-meta* as
blocking-meta (pi a (abs _ b)) = blocking-meta b
blocking-meta (agda-sort s)    = nothing
blocking-meta (lit l)          = nothing
blocking-meta (meta x _)       = just (blocker-meta x)
blocking-meta unknown          = nothing

blocking-meta* (arg (arginfo visible _)   tm ∷ _) = blocking-meta tm
blocking-meta* (arg (arginfo instance' _) tm ∷ _) = blocking-meta tm
blocking-meta* (arg (arginfo hidden _)    tm ∷ as) = blocking-meta* as

blocking-meta* [] = nothing

reduceB : Term β†’ TC Term
reduceB tm = do
  tm' ← reduce tm
  case blocking-meta tm' of Ξ» where
    (just b) β†’ blockTC b
    nothing  β†’ pure tm'

-- The first argument decides whether we want a PathP.
unapply-path' : Bool β†’ Term β†’ TC (Maybe (Term Γ— Term Γ— Term))
unapply-path' true red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) = do
  pure (just (T , x , y))
unapply-path' false 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' true tm = reduce tm >>= Ξ» where
  tm@(meta _ _) β†’ do
    (Tmv , T) ← new-meta' (pi (argN (quoteTerm I)) (abs "i" (def (quote Type) (unknown v∷ []))))
    l ← new-meta (meta Tmv (quoteTerm i0 v∷ []))
    r ← new-meta (meta Tmv (quoteTerm i1 v∷ []))
    unify tm (def (quote PathP) (T v∷ l v∷ r v∷ []))
    traverse wait-for-type (l ∷ r ∷ [])
    pure (just (T , l , r))

  red@(def (quote PathP) (T v∷ l v∷ r v∷ [])) β†’ do
    pure (just (T , l , r))

  _ β†’ pure nothing

unapply-path' pathp 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))
  _ β†’ pure nothing

unapply-path unapply-pathp : Term β†’ TC (Maybe (Term Γ— Term Γ— Term))
unapply-path = unapply-path' false
unapply-pathp = unapply-path' true

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

instance
  Has-visibility-Telescope : Has-visibility Telescope
  Has-visibility-Telescope .set-visibility v tel = Γ—-mapβ‚‚ (set-visibility v) <$> tel

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

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