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 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 BUILTIN
s 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 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' 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)) _ β pure 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 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