-- | Replace DSL-bound variable in a term
var :: DSL -> Name -> PTerm -> Int -> PTerm
var dsl n t i = v' i t where
    v' i (PRef fc hl x) | x == n =
        case dsl_var dsl of
            Nothing -> PElabError (Msg "No 'variable' defined in dsl")
            Just v -> PApp fc v [pexp (mkVar fc i)]
    v' i (PLam fc n nfc ty sc)
        | Nothing <- dsl_lambda dsl
            = PLam fc n nfc ty (v' i sc)
        | otherwise = PLam fc n nfc (v' i ty) (v' (i + 1) sc)
    v' i (PLet fc rc n nfc ty val sc)
        | Nothing <- dsl_let dsl
            = PLet fc rc n nfc (v' i ty) (v' i val) (v' i sc)
        | otherwise = PLet fc rc n nfc (v' i ty) (v' i val) (v' (i + 1) sc)
    v' i (PPi p n fc ty sc)
        | Nothing <- dsl_pi dsl
            = PPi p n fc (v' i ty) (v' i sc)
        | otherwise = PPi p n fc (v' i ty) (v' (i+1) sc)
    v' i (PTyped l r)    = PTyped (v' i l) (v' i r)
    v' i (PApp f x as)   = PApp f (v' i x) (fmap (fmap (v' i)) as)
    v' i (PWithApp f x a) = PWithApp f (v' i x) (v' i a)
    v' i (PCase f t as)  = PCase f (v' i t) (fmap (pmap (v' i)) as)
    v' i (PPair f hls p l r) = PPair f hls p (v' i l) (v' i r)
    v' i (PDPair f hls p l t r) = PDPair f hls p (v' i l) (v' i t) (v' i r)
    v' i (PAlternative ms a as) = PAlternative ms a $ map (v' i) as
    v' i (PHidden t)     = PHidden (v' i t)
    v' i (PIdiom f t)    = PIdiom f (v' i t)
    v' i (PDoBlock ds)   = PDoBlock (map (fmap (v' i)) ds)
    v' i (PNoImplicits t) = PNoImplicits (v' i t)
    v' i t = t

    mkVar fc 0 = case index_first dsl of
                   Nothing -> PElabError (Msg "No index_first defined")
                   Just f  -> setFC fc f
    mkVar fc n = case index_next dsl of
                   Nothing -> PElabError (Msg "No index_next defined")
                   Just f -> PApp fc f [pexp (mkVar fc (n-1))]

    setFC fc (PRef _ _ n) = PRef fc [] n
    setFC fc (PApp _ f xs) = PApp fc (setFC fc f) (map (fmap (setFC fc)) xs)
    setFC fc t = t
var :: DSL -> Name -> PTerm -> Int -> PTerm
var dsl n t i = v' i t where
    v' i (PRef fc hl x) | x == n =
        case dsl_var dsl of
            Nothing -> PElabError (Msg "No 'variable' defined in dsl")
            Just v -> PApp fc v [pexp (mkVar fc i)]
    v' i (PLam fc n nfc ty sc)
        | Nothing <- dsl_lambda dsl
            = PLam fc n nfc ty (v' i sc)
        | otherwise = PLam fc n nfc (v' i ty) (v' (i + 1) sc)
    v' i (PLet fc rc n nfc ty val sc)
        | Nothing <- dsl_let dsl
            = PLet fc rc n nfc (v' i ty) (v' i val) (v' i sc)
        | otherwise = PLet fc rc n nfc (v' i ty) (v' i val) (v' (i + 1) sc)
    v' i (PPi p n fc ty sc)
        | Nothing <- dsl_pi dsl
            = PPi p n fc (v' i ty) (v' i sc)
        | otherwise = PPi p n fc (v' i ty) (v' (i+1) sc)
    v' i (PTyped l r)    = PTyped (v' i l) (v' i r)
    v' i (PApp f x as)   = PApp f (v' i x) (fmap (fmap (v' i)) as)
    v' i (PWithApp f x a) = PWithApp f (v' i x) (v' i a)
    v' i (PCase f t as)  = PCase f (v' i t) (fmap (pmap (v' i)) as)
    v' i (PPair f hls p l r) = PPair f hls p (v' i l) (v' i r)
    v' i (PDPair f hls p l t r) = PDPair f hls p (v' i l) (v' i t) (v' i r)
    v' i (PAlternative ms a as) = PAlternative ms a $ map (v' i) as
    v' i (PHidden t)     = PHidden (v' i t)
    v' i (PIdiom f t)    = PIdiom f (v' i t)
    v' i (PDoBlock ds)   = PDoBlock (map (fmap (v' i)) ds)
    v' i (PNoImplicits t) = PNoImplicits (v' i t)
    v' i t = t

    mkVar fc 0 = case index_first dsl of
                   Nothing -> PElabError (Msg "No index_first defined")
                   Just f  -> setFC fc f
    mkVar fc n = case index_next dsl of
                   Nothing -> PElabError (Msg "No index_next defined")
                   Just f -> PApp fc f [pexp (mkVar fc (n-1))]

    setFC fc (PRef _ _ n) = PRef fc [] n
    setFC fc (PApp _ f xs) = PApp fc (setFC fc f) (map (fmap (setFC fc)) xs)
    setFC fc t = t
var dsl n t i = v' i t where
    v' i (PRef fc hl x) | x == n =
        case dsl_var dsl of
            Nothing -> PElabError (Msg "No 'variable' defined in dsl")
            Just v -> PApp fc v [pexp (mkVar fc i)]
    v' i (PLam fc n nfc ty sc)
        | Nothing <- dsl_lambda dsl
            = PLam fc n nfc ty (v' i sc)
        | otherwise = PLam fc n nfc (v' i ty) (v' (i + 1) sc)
    v' i (PLet fc rc n nfc ty val sc)
        | Nothing <- dsl_let dsl
            = PLet fc rc n nfc (v' i ty) (v' i val) (v' i sc)
        | otherwise = PLet fc rc n nfc (v' i ty) (v' i val) (v' (i + 1) sc)
    v' i (PPi p n fc ty sc)
        | Nothing <- dsl_pi dsl
            = PPi p n fc (v' i ty) (v' i sc)
        | otherwise = PPi p n fc (v' i ty) (v' (i+1) sc)
    v' i (PTyped l r)    = PTyped (v' i l) (v' i r)
    v' i (PApp f x as)   = PApp f (v' i x) (fmap (fmap (v' i)) as)
    v' i (PWithApp f x a) = PWithApp f (v' i x) (v' i a)
    v' i (PCase f t as)  = PCase f (v' i t) (fmap (pmap (v' i)) as)
    v' i (PPair f hls p l r) = PPair f hls p (v' i l) (v' i r)
    v' i (PDPair f hls p l t r) = PDPair f hls p (v' i l) (v' i t) (v' i r)
    v' i (PAlternative ms a as) = PAlternative ms a $ map (v' i) as
    v' i (PHidden t)     = PHidden (v' i t)
    v' i (PIdiom f t)    = PIdiom f (v' i t)
    v' i (PDoBlock ds)   = PDoBlock (map (fmap (v' i)) ds)
    v' i (PNoImplicits t) = PNoImplicits (v' i t)
    v' i t = t

    mkVar fc 0 = case index_first dsl of
                   Nothing -> PElabError (Msg "No index_first defined")
                   Just f  -> setFC fc f
    mkVar fc n = case index_next dsl of
                   Nothing -> PElabError (Msg "No index_next defined")
                   Just f -> PApp fc f [pexp (mkVar fc (n-1))]

    setFC fc (PRef _ _ n) = PRef fc [] n
    setFC fc (PApp _ f xs) = PApp fc (setFC fc f) (map (fmap (setFC fc)) xs)
    setFC fc t = t