module reflection-ex where

open import Data.Bool
open import Data.String
open import Data.Nat

postulate Name : Set
{-# BUILTIN QNAME Name #-}

primitive
  primQNameEquality : Name → Name → Bool
  primQNameLess     : Name → Name → Bool
  primShowQName     : Name → String

nameOfNat : Name
nameOfNat = quote ℕ

isNat : Name → Bool
isNat (quote ℕ) = true
isNat _           = false

postulate Meta : Set
{-# BUILTIN AGDAMETA Meta #-}

primitive
  primMetaEquality : Meta → Meta → Bool
  primMetaLess     : Meta → Meta → Bool
  primShowMeta     : Meta → String

open import Data.Word 
open import Data.Float 
open import Data.Char 

data Literal : Set where
  nat    : (n : ℕ)    → 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 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      #-}


open import Data.List

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 Abs (A : Set) : Set where
  abs : (s : String) (x : A) → Abs A

{-# BUILTIN ABS    Abs #-}
{-# BUILTIN ABSABS abs #-}

data Term : Set
data Sort : Set
data Clause : Set
Type = Term

data Term where
  var       : (x : ℕ) (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 -- Treated as '_' when unquoting.

data Sort where
  set     : (t : Term) → Sort -- A Set of a given (possibly neutral) level.
  lit     : (n : ℕ) → Sort  -- A Set of a given concrete level.
  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 : ℕ) (cs : List Name) → Definition  -- parameters and constructors
  record-type : (c : Name) (fs : List (Arg Name)) →         -- c: name of record constructor
                Definition                                  -- fs: fields
  data-cons   : (d : Name) → Definition                     -- d: name of data type
  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    #-}

-- Error messages can contain embedded names and terms.
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


{-# BUILTIN AGDATCM       TC       #-}
{-# BUILTIN AGDATCMRETURN returnTC #-}
{-# BUILTIN AGDATCMBIND   bindTC   #-}

open import Data.Unit
open import Data.Product

postulate
  -- Unify two terms, potentially solving metavariables in the process.
  unify : Term → Term → TC ⊤

  -- Throw a type error. Can be caught by catchTC.
  typeError : ∀ {a} {A : Set a} → List ErrorPart → TC A

  -- Block a type checking computation on a metavariable. This will abort
  -- the computation and restart it (from the beginning) when the
  -- metavariable is solved.
  blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A

  -- Prevent current solutions of metavariables from being rolled back in
  -- case 'blockOnMeta' is called.
  commitTC : TC ⊤

  -- Backtrack and try the second argument if the first argument throws a
  -- type error.
  catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A

  -- Infer the type of a given term
  inferType : Term → TC Type

  -- Check a term against a given type. This may resolve implicit arguments
  -- in the term, so a new refined term is returned. Can be used to create
  -- new metavariables: newMeta t = checkType unknown t
  checkType : Term → Type → TC Term

  -- Compute the normal form of a term.
  normalise : Term → TC Term

  -- Compute the weak head normal form of a term.
  reduce : Term → TC Term
-- Get the current context. Returns the context in reverse order, so that
  -- it is indexable by deBruijn index. Note that the types in the context are
  -- valid in the rest of the context. To use in the current context they need
  -- to be weakened by 1 + their position in the list.
  getContext : TC (List (Arg Type))

  -- Extend the current context with a variable of the given type.
  extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A

  -- Set the current context. Takes a context telescope with the outer-most
  -- entry first, in contrast to 'getContext'. Each type should be valid in the
  -- context formed by the preceding elements in the list.
  inContext : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A

  -- Quote a value, returning the corresponding Term.
  quoteTC : ∀ {a} {A : Set a} → A → TC Term

  -- Unquote a Term, returning the corresponding value.
  unquoteTC : ∀ {a} {A : Set a} → Term → TC A

  -- Create a fresh name.
  freshName : String → TC Name

  -- Declare a new function of the given type. The function must be defined
  -- later using 'defineFun'. Takes an Arg Name to allow declaring instances
  -- and irrelevant functions. The Visibility of the Arg must not be hidden.
  declareDef : Arg Name → Type → TC ⊤

  -- Declare a new postulate of the given type. The Visibility of the Arg
  -- must not be hidden. It fails when executed from command-line with --safe
  -- option.
  declarePostulate : Arg Name → Type → TC ⊤

  -- Define a declared function. The function may have been declared using
  -- 'declareDef' or with an explicit type signature in the program.
  defineFun : Name → List Clause → TC ⊤

  -- Get the type of a defined name. Replaces 'primNameType'.
  getType : Name → TC Type

  -- Get the definition of a defined name. Replaces 'primNameDefinition'.
  getDefinition : Name → TC Definition

  -- Check if a name refers to a macro
  isMacro : Name → TC Bool

  -- Change the behaviour of inferType, checkType, quoteTC, getContext
  -- to normalise (or not) their results. The default behaviour is no
  -- normalisation.
  withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A

  -- Prints the third argument if the corresponding verbosity level is turned
  -- on (with the -v flag to Agda).
  debugPrint : String → ℕ → List ErrorPart → TC ⊤

  -- Fail if the given computation gives rise to new, unsolved
  -- "blocking" constraints.
  noConstraints : ∀ {a} {A : Set 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 : Set a} → TC (Σ A λ _ → Bool) → TC A

{-# BUILTIN AGDATCMUNIFY              unify              #-}
{-# BUILTIN AGDATCMTYPEERROR          typeError          #-}
{-# BUILTIN AGDATCMBLOCKONMETA        blockOnMeta        #-}
{-# BUILTIN AGDATCMCATCHERROR         catchTC            #-}
{-# BUILTIN AGDATCMINFERTYPE          inferType          #-}
{-# BUILTIN AGDATCMCHECKTYPE          checkType          #-}
{-# BUILTIN AGDATCMNORMALISE          normalise          #-}
{-# BUILTIN AGDATCMREDUCE             reduce             #-}
{-# BUILTIN AGDATCMGETCONTEXT         getContext         #-}
{-# BUILTIN AGDATCMEXTENDCONTEXT      extendContext      #-}
{-# BUILTIN AGDATCMINCONTEXT          inContext          #-}
{-# BUILTIN AGDATCMQUOTETERM          quoteTC            #-}
{-# BUILTIN AGDATCMUNQUOTETERM        unquoteTC          #-}
{-# BUILTIN AGDATCMFRESHNAME          freshName          #-}
{-# BUILTIN AGDATCMDECLAREDEF         declareDef         #-}
{-# BUILTIN AGDATCMDECLAREPOSTULATE   declarePostulate   #-}
{-# BUILTIN AGDATCMDEFINEFUN          defineFun          #-}
{-# BUILTIN AGDATCMGETTYPE            getType            #-}
{-# BUILTIN AGDATCMGETDEFINITION      getDefinition      #-}
{-# BUILTIN AGDATCMCOMMIT             commitTC           #-}
{-# BUILTIN AGDATCMISMACRO            isMacro            #-}
{-# BUILTIN AGDATCMWITHNORMALISATION  withNormalisation  #-}
{-# BUILTIN AGDATCMDEBUGPRINT         debugPrint         #-}
{-# BUILTIN AGDATCMNOCONSTRAINTS      noConstraints      #-}
{-# BUILTIN AGDATCMRUNSPECULATIVE     runSpeculative     #-}

macro
    plus-to-times : Term → Term → TC ⊤
    plus-to-times (def (quote _+_) (a ∷ b ∷ [])) hole = unify hole (def (quote _*_) (a ∷ b ∷ []))
    plus-to-times v hole = unify hole v

open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )

thm : (a b : ℕ) → plus-to-times (a + b) ≡ a * b
thm a b = refl

postulate magic : Type → Term

macro
  by-magic : Term → TC ⊤
  by-magic hole =
    bindTC (inferType hole) λ goal →
    unify hole (magic goal)

open import Relation.Nullary

-- thm1 : {P NP : Set} → ¬ P ≡ NP
-- thm1 = ? by-magic

--unquoteDecl x₁ .. x ₙ = m
--unquoteDef  x₁ .. x ₙ = m

-- Defining: id-name {A} x = x
defId : (id-name : Name) → TC ⊤
defId id-name = do
  defineFun id-name
    [ clause
      ( arg (arg-info hidden relevant) (var "A")
      ∷ arg (arg-info visible relevant) (var "x")
      ∷ [] )
      (var 0 [])
    ]

id : {A : Set} (x : A) → A
unquoteDef id = defId id

open import Level  renaming  ( suc to succ ; zero  to Zero )

mkId : (id-name : Name) → TC ⊤
mkId id-name = 
  do
    ty ← quoteTC ({A : Set} (x : A) → A)
    declareDef (arg (arg-info visible relevant) id-name) ty
    defId id-name   
  where
        _>>=_  : {a : Level} {B A : Set a} (m : TC B) (f : (x : B) → TC A) → TC A
        _>>=_  = bindTC
        _>>_  : {a : Level} {B A : Set a} (m : TC B) (m' : TC A) → TC A
        _>>_  x y = bindTC x ( λ _ → y )


mkId' : (id-name : Name) → TC ⊤
mkId' id-name = 
    bindTC
        ( quoteTC ({A : Set} (x : A) → A) )
        ( λ ty → bindTC (declareDef (arg (arg-info visible relevant) id-name) ty )
        ( λ _ → defId id-name) )

lemma1 : ( x : Name  ) → mkId x ≡ mkId' x
lemma1 x = refl

unquoteDecl id′ = mkId id′