{-

doctest -DDOCTEST OldSyntax.hs

-}





-- {-# LANGUAGE DeriveFunctor #-}
-- {-# LANGUAGE DeriveFoldable #-}
-- {-# LANGUAGE DeriveTraversable #-}
-- {-# LANGUAGE DeriveGeneric #-}

-- {-# LANGUAGE BangPatterns #-}

-- {-# LANGUAGE TypeSynonymInstances #-}

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE CPP #-}


-- {-# OPTIONS_GHC -cpp -DPiForallInstalled #-}

-- -- {-# LANGUAGE TemplateHaskell #-}

-- -- {-# LANGUAGE LambdaCase #-}

-- -- {-# LANGUAGE RecordWildCards #-}



{-|

Copyright :  (c) Andreas Reuleaux 2015-2018
License   :  BSD2
Maintainer:  Andreas Reuleaux <rx@a-rx.info>
Stability :  experimental
Portability: non-portable

bound variables can be wrapped (and unwrapped)
with their textual representation, for they can contribute to the calculation
of their position info

-}




module OldWrap
       (

         module OldWrap

       )

       where



import OldSyntax


import Bound.Scope
-- import Bound.Name
-- import Bound


-- import Pire.Syntax.Binder
-- import Pire.Syntax.GetNm


-- import Pire.Utils

import Control.Lens


import Data.List (elemIndex)
import Data.Bifunctor

-- -- import OldParser


-- for the doctests

#ifdef DOCTEST

import OldParser
import OldNoPos



-- import ParseUtils
-- import Data.Function


#endif


{-|

>>> nopos $ parse expr_ "\\  x . x  a"
LamPAs_ (LamTok "\\" (Ws "  ")) [(RuntimeP,Binder_ "x" (Ws " "),Annot Nothing)] (Dot "." (Ws " ")) (Scope (Ws_ (V (B 0)) (Ws "  ") :@ Ws_ (V (F (V "a"))) (Ws "")))

>>> wrap $ nopos $ parse expr_ "\\  x . x  a"
LamPAs_ (LamTok "\\" (Ws "  ")) [(RuntimeP,Binder_ "x" (Ws " "),Annot Nothing)] (Dot "." (Ws " ")) (Scope (Ws_ (BndV "x" (V (B 0))) (Ws "  ") :@ Ws_ (V (F (V "a"))) (Ws "")))

>>> wrap $ nopos $ parse expr_ "\\yy . a (\\a . x a)"
LamPAs_ (LamTok "\\" (Ws "")) [(RuntimeP,Binder_ "yy" (Ws " "),Annot Nothing)] (Dot "." (Ws " ")) (Scope (Ws_ (V (F (V "a"))) (Ws " ") :@ Paren_ (ParenOpen "(" (Ws "")) (LamPAs_ (LamTok "\\" (Ws "")) [(RuntimeP,Binder_ "a" (Ws " "),Annot Nothing)] (Dot "." (Ws " ")) (Scope (Ws_ (V (F (V (F (V "x"))))) (Ws " ") :@ Ws_ (BndV "a" (V (B 0))) (Ws "")))) (ParenClose ")" (Ws ""))))


wrapping of PiP - expr first

>>> wrap $ nopos $ parse expr "(x:A) -> B x"
PiP RuntimeP (PatVar "x") (V "A") (Scope (V (F (V "B")) :@ BndV "x" (V (B ()))))

now w/ expr_, that's more interesting

-- -- >>> wrap $ nopos $ parse expr_ "A -> B"
-- -- PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (Binder "_") (Ws_ (V "A") (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws "")))

-- -- >>> wrap $ nopos $ parse expr_ "A -> B"
-- -- PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (InvisibleBinder 0) (Ws_ (V "A") (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws "")))

>>> wrap $ nopos $ parse expr_ "A -> B"
PiP_ RuntimeP (InferredAnn_ (V "_") (Ws_ (V "A") (Ws " "))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws "")))




-- -- >>> unwrap $ wrap $ nopos $ parse expr_ "A -> B"
-- -- PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (Binder "_") (Ws_ (V "A") (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws "")))
-- -- >>>


-- -- -- -- >>> unwrap $ wrap $ nopos $ parse expr_ "A -> B"
-- -- -- -- PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (InvisibleBinder 0) (Ws_ (V "A") (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws "")))


>>> unwrap $ wrap $ nopos $ parse expr_ "A -> B"
PiP_ RuntimeP (InferredAnn_ (V "_") (Ws_ (V "A") (Ws " "))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws "")))





-- -- -- -- >>> wrap $ nopos $ parse expr_ "(x:A) -> B x"
-- -- -- -- PiP_ RuntimeP (Ann_ (Paren_ (ParenOpen "(" (Ws "")) (WitnessedAnnBnd_ (Binder_ "x" (Ws "")) (Colon ":" (Ws "")) (Ws_ (V "A") (Ws ""))) (ParenClose ")" (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws " ") :@ Ws_ (BndV "x" (V (B ()))) (Ws "")))


-- -- -- -- >>> unwrap $ wrap $ nopos $ parse expr_ "(x:A) -> B x"
-- -- -- -- PiP_ RuntimeP (Ann_ (Paren_ (ParenOpen "(" (Ws "")) (WitnessedAnnBnd_ (Binder_ "x" (Ws "")) (Colon ":" (Ws "")) (Ws_ (V "A") (Ws ""))) (ParenClose ")" (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws " ") :@ Ws_ (V (B ())) (Ws "")))



>>> unwrap $ wrap $ nopos $ parse expr_ "(x:A) -> B x"
PiP_ RuntimeP (Paren_ (ParenOpen "(" (Ws "")) (WitnessedAnn_ (Ws_ (V "x") (Ws "")) (Colon ":" (Ws "")) (Ws_ (V "A") (Ws ""))) (ParenClose ")" (Ws " "))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws " ") :@ Ws_ (V (B ())) (Ws "")))



-- -- >>> wrap $ nopos $ parse expr_ "(B -> C) -> A"
-- -- PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (Binder "_1") (Paren_ (ParenOpen "(" (Ws "")) (PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (Binder "_") (Ws_ (V "B") (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "C"))) (Ws "")))) (ParenClose ")" (Ws " "))))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "A"))) (Ws "")))
-- -- >>>


-- -- -- -- >>> wrap $ nopos $ parse expr_ "(B -> C) -> A"
-- -- -- -- PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (InvisibleBinder 1) (Paren_ (ParenOpen "(" (Ws "")) (PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (InvisibleBinder 0) (Ws_ (V "B") (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "C"))) (Ws "")))) (ParenClose ")" (Ws " "))))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "A"))) (Ws "")))


>>> wrap $ nopos $ parse expr_ "(B -> C) -> A"
PiP_ RuntimeP (InferredAnn_ (V "_1") (Paren_ (ParenOpen "(" (Ws "")) (PiP_ RuntimeP (InferredAnn_ (V "_") (Ws_ (V "B") (Ws " "))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "C"))) (Ws "")))) (ParenClose ")" (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "A"))) (Ws "")))
-}


class Wrap a where
  wrap :: a -> a


class UnWrap a where
  unwrap :: a -> a




-- want substitution on bound vars here: () -> BndV n $ V n, etc
-- maybe not the most elegant thing in the world, but it does the job


wrap' :: Eq a => Expr a a -> Expr a a

wrap' (Ws_ x ws) = Ws_ (wrap' x) ws

wrap' (Brackets_ bo  ex bc) = Brackets_ bo  (wrap' ex) bc


wrap' (Paren x) = Paren $ wrap' x
wrap' (Paren_ po  ex pc) = Paren_ po  (wrap' ex) pc


wrap' (x :@ y) = (wrap' x) :@ (wrap' y)
wrap' (ErasedApp x y) = ErasedApp (wrap' x) (wrap' y)



wrap' (Lam n an sc) = Lam n an $ abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc

wrap' (Lam_ lamtok  binder dot' sc) = Lam_ lamtok binder dot' $ abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc
  where n = (^. name') binder


-- not for Lam'/Lams' -- don't want String


wrap' (ErasedLam n sc) = ErasedLam n $ abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc

wrap' (ErasedLam_ lamtok  binder dot' sc) = ErasedLam_ lamtok binder dot' $ abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc
  where n = (^. name') binder



wrap' (Lams ns sc) = Lams ns $ abstract (`elemIndex` ns) $ wrap' $ splat (\x -> V x) (\i -> let n = ns !! i in BndV n $ V n) sc

wrap' (Lams_ lamtok pas dot' sc) = Lams_ lamtok pas dot' $ abstract (`elemIndex` pas') $ wrap' body
  where
    body = splat (\x -> V x) (\i -> let n = pas' !! i in BndV n $ V n) sc
    pas' = (^. name') <$> pas


-- missing still
-- wrap' (LamPA eps v annot sc) = ...

wrap' (LamPAs pas sc) = LamPAs pas $ abstract (`elemIndex` pas') $ wrap' body
  where
    body = splat (\x -> V x) (\i -> let n = pas' !! i in BndV n $ V n) sc
    pas' = (^. _2) <$> pas


wrap' (LamPAs_ lamtok pas dot' sc) = LamPAs_ lamtok pas dot' $ abstract (`elemIndex` pas') $ wrap' body
  where
    body = splat (\x -> V x) (\i -> let n = pas' !! i in BndV n $ V n) sc
    pas' = (^. name') . (^. _2) <$> pas



wrap' (PiP eps pat ex sc) = PiP eps pat (wrap' ex) $ abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc
  where n = (^. name') pat





-- wrap' (PiP_ eps ann arr sc) 
--   = PiP_ eps (wrap' ann) arr $ abstract1 nm $ wrap' $ splat (\x -> V x) (\() -> BndV nm $ V nm) sc
--   where nm = (^. name') ann



-- -- -- -- wrap' (Ann_ ex) = Ann_ $ wrap' ex


-- -- wrap' (InferredAnnBnd_ bndr tyA) = InferredAnnBnd_ bndr $ wrap' tyA

-- -- wrap' (WitnessedAnnBnd_ bndr col ty) = WitnessedAnnBnd_ bndr col $ wrap' ty



wrap' (If cond ifbranch elsebranch annot) = If (wrap' cond) (wrap' ifbranch) (wrap' elsebranch) annot
wrap' (If_ iftok  cond thentok ifbranch elsetok elsebranch annot) = If_ iftok (wrap' cond) thentok (wrap' ifbranch) elsetok (wrap' elsebranch) annot



-- -- -- not so easy: over matches wrap c (with c@(Case...))
-- -- wrap' (Case ex matches annot) = Case ex (wrapMatch <$> matches) annot


-- -- -- -- -- -- wrap' (Case_ casetok ex of' mayopen matches mayclose annot) =
-- -- -- -- -- --   (Case_ casetok ex of' mayopen matches' mayclose annot)
-- -- -- -- -- --   where matches' = [(maysemi, wrapMatch match') | (maysemi, match') <- matches]


wrap' (Let n ex sc) = Let n (wrap' ex) $ abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc
wrap' (Let_ lettok bndr eq ex in' sc) = Let_ lettok bndr eq (wrap' ex) in' $ abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc
  where n = (^. name') bndr



wrap' (Sigma n ex sc) = Sigma n (wrap' ex) $ abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc
wrap' (Sigma_ bo bndr colon ex vbar sc bc) = Sigma_ bo bndr colon (wrap' ex) vbar (abstract1 n $ wrap' $ splat (\x -> V x) (\() -> BndV n $ V n) sc) bc
  where n = (^. name') bndr




wrap' (Pcase ex (n1, n2) sc annot) = Pcase (wrap' ex) (n1, n2) (abstract (`elemIndex` [n1, n2]) $ wrap' sc') annot
  where
    sc' = splat (\x -> V x) (\i -> let n = [n1, n2] !! i in BndV n $ V n) sc



wrap' (Pcase_ pcasetok ex oftok po bndr comma bndr2 pc arr sc annot)
  = Pcase_ pcasetok (wrap' ex) oftok po bndr comma bndr2 pc arr (abstract (`elemIndex` ns) $ wrap' $ sc') annot
  where
    ns = (^. name') <$> [bndr, bndr2]
    sc' = splat (\x -> V x) (\i -> let n = ns !! i in BndV n $ V n) sc




wrap' (TyEq ex ex2) = TyEq (wrap' ex) (wrap' ex2)

wrap' (TyEq_ ex eq ex2) = TyEq_ (wrap' ex) eq (wrap' ex2)





wrap' (Position d ex)  = Position d $ wrap' ex




wrap' ex = ex



-- -- -- instance (Eq a, MkVisible a) => Wrap (Expr a a) where
-- -- --   wrap = wrap'


instance (Eq a) => Wrap (Expr a a) where
  wrap = wrap'




wrapMatch (Match pattern' sc) = Match pattern' $ abstract (`elemIndex` ns) $ wrap' $ splat (\x -> V x) (\i -> let n = ns !! i in BndV n $ V n) sc
  where ns = [ (^. name') p | (_, p) <- argPatterns pattern']

wrapMatch (Match_ pattern' arr sc) = Match_ pattern' arr $ abstract (`elemIndex` ns) $ wrap' $ splat (\x -> V x) (\i -> let n = ns !! i in BndV n $ V n) sc
  where ns = [ (^. name') p | (_, p) <- argPatterns pattern']




instance (Eq a) => Wrap (Match a a) where
  wrap = wrapMatch


-- -- -- -- -- instance (Eq a, MkVisible a) => Wrap (Match a a) where
-- -- -- -- --   wrap = wrapMatch



instance (Eq t) => Wrap (Pattern t) where
  wrap = id





wrapDecl (Sig lhs rhs)        = Sig lhs $ wrap rhs
wrapDecl (Sig_ lhs colon rhs) = Sig_ lhs colon $ wrap rhs


wrapDecl (Def lhs rhs)        = Def lhs $ wrap rhs
wrapDecl (Def_ lhs equal rhs) = Def_ lhs equal $ wrap rhs




-- rethink !
-- needed eg. for
-- (silence $ runExceptT $ getModules_ ["samples"] "Nat") >>= return . (\m -> (ezipper $ Mod m) >>= lineColumn 18 12 >>= focus) . last . fromRight'


wrapDecl (Data lhs tele cs)   = Data lhs (wrap tele) $ wrap <$> cs

-- -- wrapDecl (Data_ datatok nm tele colon ty where' mayopen cs myclose) =
-- --   Data_ datatok nm (wrap tele) colon (wrap ty) where' mayopen (wrap <$> cs) myclose


wrapConstructorDef (ConstructorDef delta' tt tele) = ConstructorDef delta' tt $ wrap tele
wrapConstructorDef (ConstructorDef' tt tele)       = ConstructorDef' tt $ wrap tele
wrapConstructorDef (ConstructorDef_ delta' nm mayof tele) = ConstructorDef_ delta' nm mayof $ wrap tele
wrapConstructorDef (ConstructorDef'_  nm mayof tele) = ConstructorDef'_ nm mayof $ wrap tele
-- wrapConstructorDef n@(NoConstructorDef_ {}) = n


instance (Eq a) => Wrap (ConstructorDef a a) where
  wrap = wrapConstructorDef


  -- first from Data.Bifunctor: map wrapConstructorDef on first elem of the pair
instance (Eq a) => Wrap (ConstructorDef a a, b) where
  wrap = first wrapConstructorDef





instance (Eq a) => Wrap (Decl a a) where
  wrap = wrapDecl


instance (Eq a) => Wrap [(Decl a a)] where
  wrap = map wrap






-- wrapM (Module nm imports decls constrs) = Module nm imports (wrap decls) constrs


-- wrapM (Module_ leadingws mtok nm wheretok imports decls constrs) =
--   Module_ leadingws mtok nm wheretok imports (wrap decls) constrs


wrapM m@(Module {})  = over decls wrap m
wrapM m@(Module_ {}) = over decls wrap m



instance (Eq a) => Wrap (Module a a) where
  wrap = wrapM



wrapTele :: (Eq a) => Telescope a a -> Telescope a a

wrapTele EmptyTele = EmptyTele
wrapTele (Cons eps tt ex tele) = Cons eps tt (wrap ex) (wrapTele tele)
wrapTele (ConsInParens_ eps po nm colon ex pc tele) = ConsInParens_ eps po nm colon (wrap ex) pc (wrapTele tele)
wrapTele (ConsWildInParens_ eps po tt ex pc tele) = ConsWildInParens_ eps po tt (wrap ex) pc (wrapTele tele)
wrapTele (ConsInBrackets_ eps bo nm colon ex bc tele) = ConsInBrackets_ eps bo nm colon (wrap ex) bc (wrapTele tele)
wrapTele (Constraint ex1 ex2 tele) = Constraint (wrap ex1) (wrap ex2) (wrapTele tele)
wrapTele (Constraint_ bo ex1 eq ex2 bc tele) = Constraint_ bo (wrap ex1) eq (wrap ex2) bc (wrapTele tele)


instance (Eq a) => Wrap (Telescope a a) where
  wrap = wrapTele






-- --------------------------------------------------
-- unwrapping



-- exmpl
-- unwrap' $ wrap $ desugar $ nopos $ parse simple_expr "\\x.  \\ y . f x a y"


unwrap' :: Expr t a -> Expr t a



unwrap' (BndV _ x) = x

unwrap' (Ws_ x ws) = Ws_ (unwrap' x) ws

unwrap' (Brackets_ bo  ex bc) = Brackets_ bo  (unwrap' ex) bc

unwrap' (Paren x) = Paren $ unwrap' x
unwrap' (Paren_ po  ex pc) = Paren_ po  (unwrap' ex) pc


unwrap' (x :@ y) = (unwrap' x) :@ (unwrap' y)
unwrap' (ErasedApp x y) = ErasedApp (unwrap' x) (unwrap' y)

unwrap' (Lam n an sc) = Lam n  an $ hoistScope unwrap' sc

unwrap' (Lam_ lamtok  binder dot' sc) = Lam_ lamtok binder dot' $ hoistScope unwrap' sc

unwrap' (Lams ns sc) = Lams ns $ hoistScope unwrap' sc
unwrap' (Lams_ lamtok pas dot' sc) = Lams_ lamtok pas dot' $ hoistScope unwrap' sc


-- need to step in the annot as well ?

unwrap' (LamPA (eps, v, annot) sc) = LamPA (eps, v, annot) $ hoistScope unwrap' sc

unwrap' (LamPAs pas sc) = LamPAs pas $ hoistScope unwrap' sc
unwrap' (LamPAs_ lamtok pas dot' sc) = LamPAs_ lamtok pas dot' $ hoistScope unwrap' sc

unwrap' (Position d ex) = Position d $ unwrap' ex


unwrap' (PiP eps n ex sc)     = PiP  eps n (unwrap' ex) $ hoistScope unwrap' sc
unwrap' (PiP_ eps ann arr sc) = PiP_ eps (unwrap' ann) arr $ hoistScope unwrap' sc

-- unwrap' (InferredAnnBnd_ bndr tyA) = InferredAnnBnd_ (visible bndr) $ unwrap' tyA


-- -- unwrap' (Ann_ ex) = Ann_ $ unwrap' ex
-- -- unwrap' (InferredAnnBnd_ bndr tyA) = InferredAnnBnd_ bndr $ unwrap' tyA
-- -- unwrap' (WitnessedAnnBnd_ bndr col ty) = WitnessedAnnBnd_ bndr col $ unwrap' ty

unwrap' (InferredAnn_ bndr tyA)     = InferredAnn_ (unwrap' bndr) $ unwrap' tyA
unwrap' (WitnessedAnn_ bndr col ty) = WitnessedAnn_ (unwrap' bndr) col $ unwrap' ty




unwrap' (If cond ifbranch elsebranch annot) = If (unwrap' cond) (unwrap' ifbranch) (unwrap' elsebranch) annot

unwrap' (If_ iftok  cond thentok ifbranch elsetok elsebranch annot)
  = If_ iftok (unwrap' cond) thentok (unwrap' ifbranch) elsetok (unwrap' elsebranch) annot



-- not so easy: over matches wrap c (with c@(Case...))
unwrap' (Case ex matches annot) = Case ex (unwrapMatch <$> matches) annot


-- unwrap' (Case_ casetok ex of' mayopen matches mayclose annot) =
--   (Case_ casetok ex of' mayopen matches' mayclose annot)
--   where matches' = [(unwrapMatch match', maysemi) | (match', maysemi) <- matches]


-- -- unwrap' (Case_ casetok ex of' mayopen matches mayclose annot) =
-- --   (Case_ casetok ex of' mayopen matches' mayclose annot)
-- --   where matches' = [(maysemi, unwrapMatch match') | (maysemi, match') <- matches]





unwrap' (Let n ex sc) = Let n (unwrap' ex) $ hoistScope unwrap' sc
unwrap' (Let_ lettok bndr eq ex in' sc) = Let_ lettok bndr eq (unwrap' ex) in' $ hoistScope unwrap' sc



unwrap' (Sigma n ex sc) = Sigma n (unwrap' ex) $ hoistScope unwrap' sc
unwrap' (Sigma_ bo bndr colon ex vbar sc bc) = Sigma_ bo bndr colon (unwrap' ex) vbar (hoistScope unwrap' sc) bc


unwrap' (Pcase ex (n, n2) sc annot) = Pcase (unwrap' ex) (n, n2) (hoistScope unwrap' sc) annot
unwrap' (Pcase_ pcasetok ex oftok po bndr comma bndr2 pc arr sc annot)
  = Pcase_ pcasetok (unwrap' ex) oftok po bndr comma bndr2 pc arr (hoistScope unwrap' sc) annot


unwrap' (TyEq ex ex2) = TyEq (unwrap' ex) (unwrap' ex2)
unwrap' (TyEq_ ex eq ex2) = TyEq_ (unwrap' ex) eq (unwrap' ex2)



unwrap' x = x




instance (Eq a) => UnWrap (Expr t a) where
  unwrap = unwrap'




unwrapDecl (Sig lhs rhs)        = Sig lhs $ unwrap rhs
unwrapDecl (Sig_ lhs colon rhs) = Sig_ lhs colon $ unwrap rhs


unwrapDecl (Def lhs rhs)        = Def lhs $ unwrap rhs
unwrapDecl (Def_ lhs equal rhs) = Def_ lhs equal $ unwrap rhs


unwrapDecl (Data lhs tele cs)   = Data lhs (unwrap tele) $ unwrap <$> cs

-- -- unwrapDecl (Data_ datatok nm tele colon ty where' mayopen cs myclose) =
-- --   Data_ datatok nm (unwrap tele) colon (unwrap ty) where' mayopen (unwrap <$> cs) myclose


instance (Eq a) => UnWrap (Decl a a) where
  unwrap = unwrapDecl





instance (Eq a) => UnWrap [(Decl a a)] where
  unwrap = map unwrap



unwrapM m@(Module {})  = over decls unwrap m
unwrapM m@(Module_ {}) = over decls unwrap m


instance (Eq a) => UnWrap (Module a a) where
  unwrap = unwrapM




unwrapMatch (Match  pattern' sc)     = Match  pattern'     $ hoistScope unwrap' sc
unwrapMatch (Match_ pattern' arr sc) = Match_ pattern' arr $ hoistScope unwrap' sc


instance (Eq a) => UnWrap (Match a a) where
  unwrap = unwrapMatch




instance (Eq t) => UnWrap (Pattern t) where
  unwrap = id


unwrapTele :: (Eq a) => Telescope a a -> Telescope a a
unwrapTele EmptyTele = EmptyTele
unwrapTele (Cons eps tt ex tele) = Cons eps tt (unwrap ex) (unwrapTele tele)
unwrapTele (ConsInParens_ eps po nm colon ex pc tele) = ConsInParens_ eps po nm colon (unwrap ex) pc (unwrapTele tele)
unwrapTele (ConsWildInParens_ eps po tt ex pc tele) = ConsWildInParens_ eps po tt (unwrap ex) pc (unwrapTele tele)
unwrapTele (ConsInBrackets_ eps bo nm colon ex bc tele) = ConsInBrackets_ eps bo nm colon (unwrap ex) bc (unwrapTele tele)
unwrapTele (Constraint ex1 ex2 tele) = Constraint (unwrap ex1) (unwrap ex2) (unwrapTele tele)
unwrapTele (Constraint_ bo ex1 eq ex2 bc tele) = Constraint_ bo (unwrap ex1) eq (unwrap ex2) bc (unwrapTele tele)




instance (Eq a) => UnWrap (Telescope a a) where
  unwrap = unwrapTele




unwrapConstructorDef (ConstructorDef delta' tt tele) = ConstructorDef delta' tt $ unwrap tele
unwrapConstructorDef (ConstructorDef' tt tele)       = ConstructorDef' tt $ unwrap tele
unwrapConstructorDef (ConstructorDef_ delta' nm mayof tele) = ConstructorDef_ delta' nm mayof $ unwrap tele
unwrapConstructorDef (ConstructorDef'_  nm mayof tele) = ConstructorDef'_ nm mayof $ unwrap tele
-- unwrapConstructorDef n@(NoConstructorDef_ {}) = n


instance (Eq a) => UnWrap (ConstructorDef a a) where
  unwrap = unwrapConstructorDef


instance (Eq a) => UnWrap (ConstructorDef a a, b) where
  -- first from Data.Bifunctor: map unwrapConstructorDef on first elem of the pair
  unwrap = first unwrapConstructorDef