[Agda] When I try to reduce, I get a meta. (Reflection).

[Apostolis Xekoukoulotakis]

Let me give some context into this question because there may be easier
solutions.

When I ask to get the definition of a function, I get a list of clauses.
Each clause has a list of patterns and a term "t".
If I wanted to manipulate the term t (with functions that the reflection
api provides) , I would have to introduce the context of that particular
function.
Thus given the type of the function and the patterns of the clause, I need
to compute the context.
Since types are dependent, for each pattern, a specific term that
represents this pattern needs to substitute the variable with index 0, of
the next type (in Pi a b).

So, instead of performing a substitution, I instead want to enclose the
type with a lambda and then provide as argument the term I have created
from the specific pattern.
This is the pat variable in the test. It just happens that the type does
not depend in the previous variable.

Maybe there is an easier solution.

It is  important to note though, that neither the type system or the
documentation or the error message provides any information that could help
me correct any mistake I made in the above code.
Maybe this should be a github issue.



On Sun, Jan 19, 2020 at 12:08 AM Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> Can you find the error in this code :
>
> ```agda
>
> module test where
>
> open import Agda.Builtin.Reflection
> open import Reflection
> open import Prelude.Nat
> open import Prelude.Bool
> open import Prelude.Unit
> open import Prelude.List
>
> pat : Term
> pat = pat-lam [ clause [ arg (arg-info visible relevant) (var "ii") ] (def
> (quote Bool) []) ] [ arg (arg-info visible relevant) (var 0 []) ]
>
> macro
>   mm : Term → TC ⊤
>   mm hole
>     = do
>          inContext (arg (arg-info visible relevant) (def (quote Nat) []) ∷
> [])
>            (do
>                t ← reduce pat
>                typeError (termErr t ∷ termErr pat ∷ [])
>                     )
>
> test : ⊤
> test = mm
> ```
>
> Why do I get a meta instead of actually reducing :
> ```
> .../test.agda:27,8-10
> _22 _ (λ { ii → Bool }) _
> when checking that the expression unquote mm has type ⊤
> ```
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200119/0bdd61f5/attachment.html>