{-# OPTIONS --without-K #-}
module Agda.Builtin.Reflection where
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
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
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 : Int → 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
postulate Meta : Set
{-# BUILTIN AGDAMETA Meta #-}
primitive
primMetaEquality : Meta → Meta → Bool
primMetaLess : Meta → Meta → Bool
primShowMeta : Meta → String
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 ArgInfo : Set where
arg-info : (v : Visibility) (r : Relevance) → ArgInfo
data Arg (A : Set) : Set where
arg : (i : ArgInfo) (x : A) → Arg A
{-# BUILTIN ARGINFO ArgInfo #-}
{-# BUILTIN ARGARGINFO arg-info #-}
{-# BUILTIN ARG Arg #-}
{-# BUILTIN ARGARG arg #-}
data Abs (A : Set) : Set where
abs : (s : String) (x : A) → Abs A
{-# BUILTIN ABS Abs #-}
{-# BUILTIN ABSABS abs #-}
data Literal : Set where
nat : (n : Nat) → 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 AGDALITFLOAT float #-}
{-# BUILTIN AGDALITCHAR char #-}
{-# BUILTIN AGDALITSTRING string #-}
{-# BUILTIN AGDALITQNAME name #-}
{-# BUILTIN AGDALITMETA meta #-}
data Pattern : Set where
con : (c : Name) (ps : List (Arg Pattern)) → Pattern
dot : Pattern
var : (s : String) → Pattern
lit : (l : Literal) → Pattern
proj : (f : Name) → Pattern
absurd : Pattern
{-# BUILTIN AGDAPATTERN Pattern #-}
{-# BUILTIN AGDAPATCON con #-}
{-# BUILTIN AGDAPATDOT dot #-}
{-# BUILTIN AGDAPATVAR var #-}
{-# BUILTIN AGDAPATLIT lit #-}
{-# BUILTIN AGDAPATPROJ proj #-}
{-# BUILTIN AGDAPATABSURD absurd #-}
data Sort : Set
data Clause : Set
data Term : Set
Type = 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 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
unknown : Sort
data Clause where
clause : (ps : List (Arg Pattern)) (t : Term) → Clause
absurd-clause : (ps : List (Arg Pattern)) → Clause
{-# BUILTIN AGDASORT Sort #-}
{-# BUILTIN AGDATERM Term #-}
{-# 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 AGDASORTUNSUPPORTED unknown #-}
{-# 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
nameErr : Name → ErrorPart
{-# BUILTIN AGDAERRORPART ErrorPart #-}
{-# BUILTIN AGDAERRORPARTSTRING strErr #-}
{-# BUILTIN AGDAERRORPARTTERM termErr #-}
{-# 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
getContext : TC (List (Arg Type))
extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A
inContext : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A
freshName : String → TC Name
declareDef : Arg Name → Type → TC ⊤
defineFun : Name → List Clause → TC ⊤
getType : Name → TC Type
getDefinition : Name → TC Definition
blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A
commitTC : TC ⊤
isMacro : Name → TC Bool
withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
debugPrint : String → Nat → List ErrorPart → TC ⊤
{-# 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 AGDATCMGETCONTEXT getContext #-}
{-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-}
{-# BUILTIN AGDATCMINCONTEXT inContext #-}
{-# BUILTIN AGDATCMFRESHNAME freshName #-}
{-# BUILTIN AGDATCMDECLAREDEF declareDef #-}
{-# BUILTIN AGDATCMDEFINEFUN defineFun #-}
{-# BUILTIN AGDATCMGETTYPE getType #-}
{-# BUILTIN AGDATCMGETDEFINITION getDefinition #-}
{-# BUILTIN AGDATCMBLOCKONMETA blockOnMeta #-}
{-# BUILTIN AGDATCMCOMMIT commitTC #-}
{-# BUILTIN AGDATCMISMACRO isMacro #-}
{-# BUILTIN AGDATCMWITHNORMALISATION withNormalisation #-}
{-# BUILTIN AGDATCMDEBUGPRINT debugPrint #-}