{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
module Agda.Builtin.Reflection where
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Word
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Agda.Builtin.Char
open import Agda.Builtin.Float
open import Agda.Builtin.Int
open import Agda.Builtin.Sigma
open import Agda.Primitive
postulate Name : Set
{-# BUILTIN QNAME Name #-}
primitive
primQNameEquality : Name → Name → Bool
primQNameLess : Name → Name → Bool
primShowQName : Name → String
data Associativity : Set where
left-assoc : Associativity
right-assoc : Associativity
non-assoc : Associativity
data Precedence : Set where
related : Float → Precedence
unrelated : Precedence
data Fixity : Set 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 #-}
{-# COMPILE GHC Associativity = data MAlonzo.RTE.Assoc (MAlonzo.RTE.LeftAssoc | MAlonzo.RTE.RightAssoc | MAlonzo.RTE.NonAssoc) #-}
{-# COMPILE GHC Precedence = data MAlonzo.RTE.Precedence (MAlonzo.RTE.Related | MAlonzo.RTE.Unrelated) #-}
{-# COMPILE GHC Fixity = data MAlonzo.RTE.Fixity (MAlonzo.RTE.Fixity) #-}
{-# COMPILE JS Associativity = function (x,v) { return v[x](); } #-}
{-# COMPILE JS left-assoc = "left-assoc" #-}
{-# COMPILE JS right-assoc = "right-assoc" #-}
{-# COMPILE JS non-assoc = "non-assoc" #-}
{-# COMPILE JS Precedence =
function (x,v) {
if (x === "unrelated") { return v[x](); } else { return v["related"](x); }} #-}
{-# COMPILE JS related = function(x) { return x; } #-}
{-# COMPILE JS unrelated = "unrelated" #-}
{-# COMPILE JS Fixity = function (x,v) { return v["fixity"](x["assoc"], x["prec"]); } #-}
{-# COMPILE JS fixity = function (x) { return function (y) { return { "assoc": x, "prec": y}; }; } #-}
primitive
primQNameFixity : Name → Fixity
primQNameToWord64s : Name → Σ Word64 (λ _ → Word64)
postulate Meta : Set
{-# BUILTIN AGDAMETA Meta #-}
primitive
primMetaEquality : Meta → Meta → Bool
primMetaLess : Meta → Meta → Bool
primShowMeta : Meta → String
primMetaToNat : Meta → Nat
data Visibility : Set where
visible hidden instance′ : Visibility
{-# BUILTIN HIDING Visibility #-}
{-# BUILTIN VISIBLE visible #-}
{-# BUILTIN HIDDEN hidden #-}
{-# BUILTIN INSTANCE instance′ #-}
data Relevance : Set where
relevant irrelevant : Relevance
{-# BUILTIN RELEVANCE Relevance #-}
{-# BUILTIN RELEVANT relevant #-}
{-# BUILTIN IRRELEVANT irrelevant #-}
data Quantity : Set where
quantity-0 quantity-ω : Quantity
{-# BUILTIN QUANTITY Quantity #-}
{-# BUILTIN QUANTITY-0 quantity-0 #-}
{-# BUILTIN QUANTITY-ω quantity-ω #-}
data Modality : Set where
modality : (r : Relevance) (q : Quantity) → Modality
{-# BUILTIN MODALITY Modality #-}
{-# BUILTIN MODALITY-CONSTRUCTOR modality #-}
data ArgInfo : Set where
arg-info : (v : Visibility) (m : Modality) → ArgInfo
data Arg {a} (A : Set a) : Set a where
arg : (i : ArgInfo) (x : A) → Arg A
{-# BUILTIN ARGINFO ArgInfo #-}
{-# BUILTIN ARGARGINFO arg-info #-}
{-# BUILTIN ARG Arg #-}
{-# BUILTIN ARGARG arg #-}
data Blocker : Set where
blockerAny : List Blocker → Blocker
blockerAll : List Blocker → Blocker
blockerMeta : Meta → Blocker
{-# BUILTIN AGDABLOCKER Blocker #-}
{-# BUILTIN AGDABLOCKERANY blockerAny #-}
{-# BUILTIN AGDABLOCKERALL blockerAll #-}
{-# BUILTIN AGDABLOCKERMETA blockerMeta #-}
data Abs {a} (A : Set a) : Set a where
abs : (s : String) (x : A) → Abs A
{-# BUILTIN ABS Abs #-}
{-# BUILTIN ABSABS abs #-}
data Literal : Set 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 #-}
data Term : Set
data Sort : Set
data Pattern : Set
data Clause : Set
Type = Term
Telescope = List (Σ String λ _ → Arg Type)
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 Type) (b : Abs Type) → 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
data Clause where
clause : (tel : Telescope) (ps : List (Arg Pattern)) (t : Term) → Clause
absurd-clause : (tel : Telescope) (ps : List (Arg Pattern)) → Clause
{-# 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 AGDAPATCON con #-}
{-# BUILTIN AGDAPATDOT dot #-}
{-# BUILTIN AGDAPATVAR var #-}
{-# BUILTIN AGDAPATLIT lit #-}
{-# BUILTIN AGDAPATPROJ proj #-}
{-# BUILTIN AGDAPATABSURD absurd #-}
{-# BUILTIN AGDACLAUSECLAUSE clause #-}
{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
data Definition : Set 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
{-# 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 #-}
data ErrorPart : Set where
strErr : String → ErrorPart
termErr : Term → ErrorPart
pattErr : Pattern → ErrorPart
nameErr : Name → ErrorPart
{-# BUILTIN AGDAERRORPART ErrorPart #-}
{-# BUILTIN AGDAERRORPARTSTRING strErr #-}
{-# BUILTIN AGDAERRORPARTTERM termErr #-}
{-# BUILTIN AGDAERRORPARTPATT pattErr #-}
{-# BUILTIN AGDAERRORPARTNAME nameErr #-}
postulate
TC : ∀ {a} → Set a → Set a
returnTC : ∀ {a} {A : Set a} → A → TC A
bindTC : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
unify : Term → Term → TC ⊤
typeError : ∀ {a} {A : Set a} → List ErrorPart → TC A
inferType : Term → TC Type
checkType : Term → Type → TC Term
normalise : Term → TC Term
reduce : Term → TC Term
catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A
quoteTC : ∀ {a} {A : Set a} → A → TC Term
unquoteTC : ∀ {a} {A : Set a} → Term → TC A
quoteωTC : ∀ {A : Setω} → A → TC Term
getContext : TC Telescope
extendContext : ∀ {a} {A : Set a} → String → Arg Type → TC A → TC A
inContext : ∀ {a} {A : Set a} → Telescope → TC A → TC A
freshName : String → TC Name
declareDef : Arg Name → Type → TC ⊤
declarePostulate : Arg Name → Type → TC ⊤
declareData : Name → Nat → Type → TC ⊤
defineData : Name → List (Σ Name (λ _ → Type)) → TC ⊤
defineFun : Name → List Clause → TC ⊤
getType : Name → TC Type
getDefinition : Name → TC Definition
blockTC : ∀ {a} {A : Set a} → Blocker → TC A
commitTC : TC ⊤
isMacro : Name → TC Bool
pragmaForeign : String → String → TC ⊤
pragmaCompile : String → Name → String → TC ⊤
withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
askNormalisation : TC Bool
withReconstructed : ∀ {a} {A : Set a} → Bool → TC A → TC A
askReconstructed : TC Bool
withExpandLast : ∀ {a} {A : Set a} → Bool → TC A → TC A
askExpandLast : TC Bool
withReduceDefs : ∀ {a} {A : Set a} → (Σ Bool λ _ → List Name) → TC A → TC A
askReduceDefs : TC (Σ Bool λ _ → List Name)
formatErrorParts : List ErrorPart → TC String
debugPrint : String → Nat → List ErrorPart → TC ⊤
noConstraints : ∀ {a} {A : Set a} → TC A → TC A
runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A
getInstances : Meta → TC (List Term)
{-# 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 AGDATCMDECLAREDATA declareData #-}
{-# BUILTIN AGDATCMDEFINEDATA defineData #-}
{-# BUILTIN AGDATCMDEFINEFUN defineFun #-}
{-# BUILTIN AGDATCMGETTYPE getType #-}
{-# BUILTIN AGDATCMGETDEFINITION getDefinition #-}
{-# BUILTIN AGDATCMBLOCK blockTC #-}
{-# BUILTIN AGDATCMCOMMIT commitTC #-}
{-# BUILTIN AGDATCMISMACRO isMacro #-}
{-# BUILTIN AGDATCMPRAGMAFOREIGN pragmaForeign #-}
{-# BUILTIN AGDATCMPRAGMACOMPILE pragmaCompile #-}
{-# BUILTIN AGDATCMWITHNORMALISATION withNormalisation #-}
{-# BUILTIN AGDATCMWITHRECONSTRUCTED withReconstructed #-}
{-# BUILTIN AGDATCMWITHEXPANDLAST withExpandLast #-}
{-# BUILTIN AGDATCMWITHREDUCEDEFS withReduceDefs #-}
{-# BUILTIN AGDATCMASKNORMALISATION askNormalisation #-}
{-# BUILTIN AGDATCMASKRECONSTRUCTED askReconstructed #-}
{-# BUILTIN AGDATCMASKEXPANDLAST askExpandLast #-}
{-# BUILTIN AGDATCMASKREDUCEDEFS askReduceDefs #-}
{-# BUILTIN AGDATCMFORMATERRORPARTS formatErrorParts #-}
{-# BUILTIN AGDATCMDEBUGPRINT debugPrint #-}
{-# BUILTIN AGDATCMNOCONSTRAINTS noConstraints #-}
{-# BUILTIN AGDATCMRUNSPECULATIVE runSpeculative #-}
{-# BUILTIN AGDATCMGETINSTANCES getInstances #-}
{-# COMPILE JS returnTC = _ => _ => _ => undefined #-}
{-# COMPILE JS bindTC = _ => _ => _ => _ =>
_ => _ => undefined #-}
{-# COMPILE JS unify = _ => _ => undefined #-}
{-# COMPILE JS typeError = _ => _ => _ => undefined #-}
{-# COMPILE JS inferType = _ => undefined #-}
{-# COMPILE JS checkType = _ => _ => undefined #-}
{-# COMPILE JS normalise = _ => undefined #-}
{-# COMPILE JS reduce = _ => undefined #-}
{-# COMPILE JS catchTC = _ => _ => _ => _ => undefined #-}
{-# COMPILE JS quoteTC = _ => _ => _ => undefined #-}
{-# COMPILE JS unquoteTC = _ => _ => _ => undefined #-}
{-# COMPILE JS quoteωTC = _ => _ => undefined #-}
{-# COMPILE JS getContext = undefined #-}
{-# COMPILE JS extendContext = _ => _ => _ => _ => _ => undefined #-}
{-# COMPILE JS inContext = _ => _ => _ => _ => undefined #-}
{-# COMPILE JS freshName = _ => undefined #-}
{-# COMPILE JS declareDef = _ => _ => undefined #-}
{-# COMPILE JS declarePostulate = _ => _ => undefined #-}
{-# COMPILE JS declareData = _ => _ => _ => undefined #-}
{-# COMPILE JS defineData = _ => _ => undefined #-}
{-# COMPILE JS defineFun = _ => _ => undefined #-}
{-# COMPILE JS getType = _ => undefined #-}
{-# COMPILE JS getDefinition = _ => undefined #-}
{-# COMPILE JS blockTC = _ => _ => undefined #-}
{-# COMPILE JS commitTC = undefined #-}
{-# COMPILE JS isMacro = _ => undefined #-}
{-# COMPILE JS pragmaForeign = _ => _ => undefined #-}
{-# COMPILE JS pragmaCompile = _ => _ => _ => undefined #-}
{-# COMPILE JS withNormalisation = _ => _ => _ => _ => undefined #-}
{-# COMPILE JS withReconstructed = _ => _ => _ => _ => undefined #-}
{-# COMPILE JS withExpandLast = _ => _ => _ => _ => undefined #-}
{-# COMPILE JS withReduceDefs = _ => _ => _ => _ => undefined #-}
{-# COMPILE JS askNormalisation = undefined #-}
{-# COMPILE JS askReconstructed = undefined #-}
{-# COMPILE JS askExpandLast = undefined #-}
{-# COMPILE JS askReduceDefs = undefined #-}
{-# COMPILE JS debugPrint = _ => _ => _ => undefined #-}
{-# COMPILE JS noConstraints = _ => _ => _ => undefined #-}
{-# COMPILE JS runSpeculative = _ => _ => _ => undefined #-}
{-# COMPILE JS getInstances = _ => undefined #-}
private
filter : (Name → Bool) → List Name → List Name
filter p [] = []
filter p (x ∷ xs) with p x
... | true = x ∷ filter p xs
... | false = filter p xs
_∈_ : Name → List Name → Bool
n ∈ [] = false
n ∈ (n' ∷ l) with primQNameEquality n n'
... | true = true
... | false = n ∈ l
_∉_ : Name → List Name → Bool
n ∉ l with n ∈ l
... | true = false
... | false = true
_++_ : List Name → List Name → List Name
[] ++ l = l
(x ∷ xs) ++ l = x ∷ (xs ++ l)
combineReduceDefs : (Σ Bool λ _ → List Name) → (Σ Bool λ _ → List Name) → (Σ Bool λ _ → List Name)
combineReduceDefs (true , defs₁) (true , defs₂) = (true , filter (_∈ defs₁) defs₂)
combineReduceDefs (false , defs₁) (true , defs₂) = (true , filter (_∉ defs₁) defs₂)
combineReduceDefs (true , defs₁) (false , defs₂) = (true , filter (_∉ defs₂) defs₁)
combineReduceDefs (false , defs₁) (false , defs₂) = (false , defs₁ ++ defs₂)
onlyReduceDefs dontReduceDefs : ∀ {a} {A : Set a} → List Name → TC A → TC A
onlyReduceDefs defs x = bindTC askReduceDefs (λ exDefs → withReduceDefs (combineReduceDefs (true , defs) exDefs) x)
dontReduceDefs defs x = bindTC askReduceDefs (λ exDefs → withReduceDefs (combineReduceDefs (false , defs) exDefs) x)
blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A
blockOnMeta m = blockTC (blockerMeta m)
{-# WARNING_ON_USAGE onlyReduceDefs "DEPRECATED: Use `withReduceDefs` instead of `onlyReduceDefs`" #-}
{-# WARNING_ON_USAGE dontReduceDefs "DEPRECATED: Use `withReduceDefs` instead of `dontReduceDefs`" #-}