open import 1Lab.Reflection hiding (reverse)
open import 1Lab.Type

open import Data.Dec.Base
open import Data.Fin.Base

module 1Lab.Reflection.Variables where

--------------------------------------------------------------------------------
-- Variable Binding for Terms
--
-- Many reflection tasks will require us to construct abstract
-- syntax trees representing reified expressions, which we will
-- use to construct a normal form. This works fine up until we
-- need to start finding normal forms for equational theories
-- with some sort of commutativity. For instance, which expression
-- should we prefer: 'x + y' or 'y + x'?
--
-- The first solution we may try here is to impose some ordering on
-- `Term`, and then sort our lists. However, trying to define this
-- ordering is complex, and it's not even clear if we /can/ impose
-- a meaningful ordering.
--
-- The next solution is to try and order the variables by the
-- time they are /introduced/, which is what this module aims to do.
-- We introduce a type 'Variables', which is intended to be an abstract
-- source of variable expressions. This allows us to produce fresh
-- (already quoted) variables of type 'Fin', which can be inserted
-- into the syntax tree while it's being constructed.
--
-- Once the syntax trees have been completed, we can grab an
-- environment using the aptly named 'environment' function.
-- This returns a (already quoted) environment 'Vec A n',
-- which allows us to easily build up quoted
-- calls to our normalization functions rather easily.

-- We π the wisdom that reversing a list/vector is a type
-- error!
data Env {β} (A : Type β) : Nat β Type β where
[] : Env A zero
_β·_ : β {n} β Env A n β A β Env A (suc n)

record Variables {a} (A : Type a) : Type a where
constructor mk-variables
field
{nvars} : Nat
-- We store the bindings in reverse order so that it's
-- cheap to add a new one.
bound : Env A nvars
variables : Term β Maybe Term

open Variables

private variable
a b : Level
A : Type a
n : Nat

empty-vars : Variables A
empty-vars = mk-variables [] (Ξ» _ β nothing)

private
bind : Term β Term β (Term β Maybe Term) β Term β Maybe Term
bind tm tm-var lookup tm' with lookup tm' | tm β‘? tm'
... | just tm'-var | _     = just tm'-var
... | nothing      | yes _ = just tm-var
... | nothing      | no _  = nothing

fin-term : Nat β Term
fin-term zero = con (quote fzero) (unknown hβ· [])
fin-term (suc n) = con (quote fsuc) (unknown hβ· fin-term n vβ· [])

env-rec : (Mot : Nat β Type b) β
(β {n} β Mot n β A β Mot (suc n)) β
Mot zero β
Env A n β Mot n
env-rec Mot _β·*_ []* []       = []*
env-rec Mot _β·*_ []* (xs β· x) = env-rec (Mot β suc) _β·*_ ([]* β·* x) xs

reverse : Env A n β Vec A n
reverse {A = A} env = env-rec (Vec A) (Ξ» xs x β x β· xs) [] env

-- Get the variable associated with a term, binding a new
-- one as need be. Note that this returns the variable
-- as a quoted term!
bind-var : Variables A β Term β TC (Term Γ Variables A)
bind-var vs tm with variables vs tm
... | just v = do
pure (v , vs)
... | nothing = do
a β unquoteTC tm
let v = fin-term (nvars vs)
let vs' = mk-variables (bound vs β· a)
(bind tm v (variables vs))
pure (v , vs')

environment : Variables A β TC (Term Γ Term)
environment vs = do
env β quoteTC (reverse (bound vs))
size β quoteTC (nvars vs)
pure (size , env)