sdfsdf.idr

data Name : Type where
     UN : String -> Name -- user written name
     MN : String -> Int -> Name -- machine generated name

-- In the term representation, we represent local variables as an index into
-- a list of bound names:
data IsVar : Name -> Nat -> List Name -> Type where
     First : IsVar n Z (n :: ns)
     Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

-- And, sometimes, it's convenient to manipulate variables separately.
-- Note the erasure properties of the following definition (it is just a Nat
-- at run time)
data Var : List Name -> Type where
     MkVar : {i : Nat} -> (0 p : IsVar n i vars) -> Var vars

-- 1. Remove all references to the most recently bound variable
dropFirst : List (Var (v :: vs)) -> List (Var vs)
dropFirst [] = []
dropFirst (MkVar First :: xs) = dropFirst xs
dropFirst (MkVar (Later x) :: xs) = MkVar x :: dropFirst xs

-- 2. Add a reference to a variable in the middle of a scope - we'll need 
-- something like this later.
-- Note: The type here isn't quite right, you'll need to modify it slightly.
insertName : {outer : _} -> Var (outer ++ inner) -> Var (outer ++ n :: inner)
insertName {outer = []} v = MkVar First
insertName {outer = (x :: xs)} (MkVar First) = MkVar First -- ???
insertName {outer = (x :: xs)} (MkVar (Later v))
  = let MkVar d = insertName (MkVar v) in MkVar (Later d)
-- this feels all kinda wrong, but working via 
-- insertName : Var (m :: outer ++ inner) -> Var (m :: outer ++ n :: inner)
-- wasn't working out either

insertFront : (ys : List Name) -> Var xs -> Var (ys ++ xs)
insertFront [] x = x
insertFront (y :: ys) x = let MkVar d = insertFront ys x in MkVar (Later d)

-- insertFront' : (ys : List Name) -> Var xs -> Var (xs ++ ys)
-- insertFront' [] x = ?Dsffd
-- insertFront' (y :: ys) x = ?dsf -- let MkVar d = insertFront ys x in MkVar (Later d)

insertName' : {outer : _} -> Var (outer ++ inner) -> Var (outer ++ n :: inner)
insertName' {outer = []} v = MkVar First
insertName' {outer = (x::xs)} (MkVar First) = ?sdfsdf
insertName' {outer = (x::xs)} (MkVar (Later y))
  = insertFront [x] (insertName' {outer = xs} (MkVar y))

insertFront : (ys : List Name) -> Var xs -> Var (ys ++ xs)
insertFront [] x = x
insertFront (y :: ys) x = let MkVar d = insertFront ys x in MkVar (Later d)

insertName' : {outer : _} -> Var (outer ++ inner) -> Var (outer ++ n :: inner)
insertName' {outer = []} v = MkVar First
insertName' {outer = (x::xs)} vars
  = insertFront [x] (insertName' {outer = xs} vars)

{-
Error(s) building file src/Foo.idr: While processing right hand side of
insertName'. Can't solve constraint between: x :: (xs ++ inner) and xs ++ inner.

src/Foo.idr:39:47--39:51
    |
 39 |   = insertFront [x] (insertName' {outer = xs} vars)
    |                                               ^^^^
-}