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 Abs
tractions.
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 Literal
s. 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 BUILTIN
s 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 <> " ")