{-# LANGUAGE LambdaCase #-}

module Telomare.Decompiler where

import Control.Comonad.Cofree (Cofree ((:<)))
import Control.Monad (foldM, liftM2)
import qualified Control.Monad.State as State
import Data.List (intercalate)
import qualified Data.Map as Map
import Data.Semigroup (Max (..))
import Telomare

decompileUPT :: UnprocessedParsedTerm -> String
decompileUPT :: UnprocessedParsedTerm -> String
decompileUPT =
  let lineLimit :: Integer
lineLimit = Integer
120
      -- "hello"
      showS :: String -> State.State Int String
      showS :: String -> State Int String
showS String
s = let indent :: Int
indent = forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s in forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify (forall a. Num a => a -> a -> a
+ Int
indent) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure String
s
      drawIndent :: State Int String
drawIndent = forall s (m :: * -> *). MonadState s m => m s
State.get forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Int
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate Int
n Char
' ')
      drawList :: [State Int String] -> State Int String
drawList = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
      needsParens :: UnprocessedParsedTerm -> Bool
needsParens = \case -- will need parens if on right side of application
        AppUP UnprocessedParsedTerm
_ UnprocessedParsedTerm
_ -> Bool
True
        LamUP String
_ UnprocessedParsedTerm
_ -> Bool
True
        LeftUP UnprocessedParsedTerm
_  -> Bool
True
        RightUP UnprocessedParsedTerm
_ -> Bool
True
        TraceUP UnprocessedParsedTerm
_ -> Bool
True
        LetUP [(String, UnprocessedParsedTerm)]
_ UnprocessedParsedTerm
_ -> Bool
True
        ITEUP {}  -> Bool
True
        UnprocessedParsedTerm
_         -> Bool
False
      needsFirstParens :: UnprocessedParsedTerm -> Bool
needsFirstParens = \case
        LamUP String
_ UnprocessedParsedTerm
_ -> Bool
True
        LetUP [(String, UnprocessedParsedTerm)]
_ UnprocessedParsedTerm
_ -> Bool
True
        ITEUP {}  -> Bool
True
        UnprocessedParsedTerm
_         -> Bool
False
      drawParens :: UnprocessedParsedTerm -> State Int String
drawParens UnprocessedParsedTerm
x = if UnprocessedParsedTerm -> Bool
needsParens UnprocessedParsedTerm
x
        then [State Int String] -> State Int String
drawList [String -> State Int String
showS String
" (", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
x, String -> State Int String
showS String
")"]
        else [State Int String] -> State Int String
drawList [String -> State Int String
showS String
" ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
x]
      drawFirstParens :: UnprocessedParsedTerm -> State Int String
drawFirstParens UnprocessedParsedTerm
x = if UnprocessedParsedTerm -> Bool
needsFirstParens UnprocessedParsedTerm
x
        then [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"(", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
x, String -> State Int String
showS String
")"]
        else UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
x
      draw :: UnprocessedParsedTerm -> State.State Int String
      draw :: UnprocessedParsedTerm -> State Int String
draw = \case
          VarUP String
s -> String -> State Int String
showS String
s
          ITEUP UnprocessedParsedTerm
i UnprocessedParsedTerm
t UnprocessedParsedTerm
e -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"if ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
i, String -> State Int String
showS String
" then ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
t, String -> State Int String
showS String
" else ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
e]
          LetUP ((String
firstName, UnprocessedParsedTerm
firstDef):[(String, UnprocessedParsedTerm)]
bindingsXS) UnprocessedParsedTerm
in_ -> if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, UnprocessedParsedTerm)]
bindingsXS
            then [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"let ", String -> State Int String
showS String
firstName, String -> State Int String
showS String
" = ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
firstDef, String -> State Int String
showS String
" in ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
in_]
            else do
            Int
startIn <- forall s (m :: * -> *). MonadState s m => m s
State.get
            String
l <- String -> State Int String
showS String
"let "
            Int
startBind <- forall s (m :: * -> *). MonadState s m => m s
State.get
            String
fb <- [State Int String] -> State Int String
drawList [String -> State Int String
showS String
firstName, String -> State Int String
showS String
" = ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
firstDef, forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"\n"]
            let drawOne :: (String, UnprocessedParsedTerm) -> State Int String
drawOne (String
name, UnprocessedParsedTerm
upt) = do
                  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put Int
startBind
                  [State Int String] -> State Int String
drawList [State Int String
drawIndent, String -> State Int String
showS String
name, String -> State Int String
showS String
" = ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
upt, forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"\n"]
            String
displayedBindings <- forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (String, UnprocessedParsedTerm) -> State Int String
drawOne [(String, UnprocessedParsedTerm)]
bindingsXS
            forall s (m :: * -> *). MonadState s m => s -> m ()
State.put Int
startIn
            forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [forall (f :: * -> *) a. Applicative f => a -> f a
pure String
l, forall (f :: * -> *) a. Applicative f => a -> f a
pure String
fb, forall (f :: * -> *) a. Applicative f => a -> f a
pure String
displayedBindings, State Int String
drawIndent, String -> State Int String
showS String
"in ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
in_]
          ListUP [UnprocessedParsedTerm]
l -> let insertCommas :: [State Int String] -> [State Int String]
insertCommas []     = []
                          insertCommas [State Int String
x]    = [State Int String
x]
                          insertCommas (State Int String
x:[State Int String]
xs) = State Int String
x forall a. a -> [a] -> [a]
: String -> State Int String
showS String
"," forall a. a -> [a] -> [a]
: [State Int String] -> [State Int String]
insertCommas [State Int String]
xs
                      in [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"[", forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. [State Int String] -> [State Int String]
insertCommas forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UnprocessedParsedTerm -> State Int String
draw [UnprocessedParsedTerm]
l, String -> State Int String
showS String
"]" ]
          IntUP Int
x -> String -> State Int String
showS forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Int
x
          StringUP String
s -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"\"", String -> State Int String
showS String
s, String -> State Int String
showS String
"\""]
          PairUP UnprocessedParsedTerm
a UnprocessedParsedTerm
b -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"(", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
a, String -> State Int String
showS String
",", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
b, String -> State Int String
showS String
")"]
          AppUP UnprocessedParsedTerm
f UnprocessedParsedTerm
x -> [State Int String] -> State Int String
drawList [UnprocessedParsedTerm -> State Int String
drawFirstParens UnprocessedParsedTerm
f, UnprocessedParsedTerm -> State Int String
drawParens UnprocessedParsedTerm
x]
          -- TODO flatten nested lambdas
          LamUP String
n UnprocessedParsedTerm
x -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"\\", String -> State Int String
showS String
n, String -> State Int String
showS String
" -> ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
x]
          ChurchUP Int
n -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"$", String -> State Int String
showS forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Int
n]
          UnsizedRecursionUP UnprocessedParsedTerm
t UnprocessedParsedTerm
r UnprocessedParsedTerm
b -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"{", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
t, String -> State Int String
showS String
",", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
r, String -> State Int String
showS String
",", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
b, String -> State Int String
showS String
"}"]
          LeftUP UnprocessedParsedTerm
x -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"left ", UnprocessedParsedTerm -> State Int String
drawParens UnprocessedParsedTerm
x]
          RightUP UnprocessedParsedTerm
x -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"right ", UnprocessedParsedTerm -> State Int String
drawParens UnprocessedParsedTerm
x]
          TraceUP UnprocessedParsedTerm
x -> [State Int String] -> State Int String
drawList [String -> State Int String
showS String
"trace ", UnprocessedParsedTerm -> State Int String
drawParens UnprocessedParsedTerm
x]
          CheckUP UnprocessedParsedTerm
c UnprocessedParsedTerm
x -> [State Int String] -> State Int String
drawList [UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
x, String -> State Int String
showS String
" : ", UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
c]

  in \UnprocessedParsedTerm
x -> forall s a. State s a -> s -> a
State.evalState (UnprocessedParsedTerm -> State Int String
draw UnprocessedParsedTerm
x) Int
0
  {-
      safeTail s = if null s then [] else tail s
      showMem s = do
        let indent = length . last . takeWhile (not . null) . iterate (safeTail . dropWhile (/= '\n')) $ s
        if elem '\n' s
          then State.put indent
          else State.modify (+ indent)
        pure s
      draw oneLine =
        let showTwo a b = undefined --let long =
            showLine l = do
              indent <- State.get
              let long = intercalate " " l
                         in if length long > lineLimit
                            then

-}
              {-m
          drawLineOr x y = if not oneLine && draw
-}

decompileTerm1 :: Term1 -> UnprocessedParsedTerm
decompileTerm1 :: Term1 -> UnprocessedParsedTerm
decompileTerm1 = \case
  LocTag
_ :< ParserTermF String String Term1
TZeroF -> Int -> UnprocessedParsedTerm
IntUP Int
0
  LocTag
_ :< TPairF Term1
a Term1
b -> UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
PairUP (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
a) (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
b)
  LocTag
_ :< TVarF String
n -> String -> UnprocessedParsedTerm
VarUP String
n
  LocTag
_ :< TAppF Term1
f Term1
x -> UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
f) (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
x)
  LocTag
_ :< TCheckF Term1
c Term1
x -> UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
CheckUP (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
c) (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
x)
  LocTag
_ :< TITEF Term1
i Term1
t Term1
e ->UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
ITEUP (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
i) (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
t) (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
e)
  LocTag
_ :< TLeftF Term1
x -> UnprocessedParsedTerm -> UnprocessedParsedTerm
LeftUP (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
x)
  LocTag
_ :< TRightF Term1
x -> UnprocessedParsedTerm -> UnprocessedParsedTerm
RightUP (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
x)
  LocTag
_ :< TTraceF Term1
x -> UnprocessedParsedTerm -> UnprocessedParsedTerm
TraceUP (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
x)
  LocTag
_ :< TLamF (Open String
n) Term1
x -> String -> UnprocessedParsedTerm -> UnprocessedParsedTerm
LamUP String
n (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
x)
  LocTag
_ :< TLamF (Closed String
n) Term1
x -> String -> UnprocessedParsedTerm -> UnprocessedParsedTerm
LamUP String
n (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
x) -- not strictly equivalent
  LocTag
_ :< TLimitedRecursionF Term1
t Term1
r Term1
b -> UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
UnsizedRecursionUP (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
t) (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
r) (Term1 -> UnprocessedParsedTerm
decompileTerm1 Term1
b)

decompileTerm2 :: Term2 -> Term1
decompileTerm2 :: Term2 -> Term1
decompileTerm2 =
  let nameSupply :: [String]
nameSupply = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> [a] -> [a]
:[]) [Char
'a'..Char
'z'] forall a. Semigroup a => a -> a -> a
<> ([String
x forall a. Semigroup a => a -> a -> a
<> String
y | String
x <- [String]
nameSupply, String
y <- [String]
nameSupply]))
      getName :: Int -> String
getName Int
n = if Int
n forall a. Ord a => a -> a -> Bool
< Int
0
        then forall a. [a] -> a
head [String]
nameSupply
        else [String]
nameSupply forall a. [a] -> Int -> a
!! Int
n
      go :: Term2
         -> (Max Int, Term1)
      go :: Term2 -> (Max Int, Term1)
go = \case
        LocTag
anno :< ParserTermF () Int Term2
TZeroF -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. ParserTermF l v r
TZeroF
        LocTag
anno :< TPairF Term2
a Term2
b -> (\Term1
x Term1
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TPairF Term1
x Term1
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> (Max Int, Term1)
go Term2
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term2 -> (Max Int, Term1)
go Term2
b
        LocTag
anno :< TVarF Int
n ->  (forall a. a -> Max a
Max Int
n, LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF (Int -> String
getName Int
n))
        LocTag
anno :< TAppF Term2
f Term2
x -> (\Term1
y Term1
z -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TAppF Term1
y Term1
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> (Max Int, Term1)
go Term2
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term2 -> (Max Int, Term1)
go Term2
x
        LocTag
anno :< TCheckF Term2
c Term2
x -> (\Term1
y Term1
z -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TCheckF Term1
y Term1
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> (Max Int, Term1)
go Term2
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term2 -> (Max Int, Term1)
go Term2
x
        LocTag
anno :< TITEF Term2
i Term2
t Term2
e -> (\Term1
x Term1
y Term1
z -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> r -> ParserTermF l v r
TITEF Term1
x Term1
y Term1
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> (Max Int, Term1)
go Term2
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term2 -> (Max Int, Term1)
go Term2
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term2 -> (Max Int, Term1)
go Term2
e
        LocTag
anno :< TLeftF Term2
x -> (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l v r. r -> ParserTermF l v r
TLeftF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> (Max Int, Term1)
go Term2
x
        LocTag
anno :< TRightF Term2
x -> (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l v r. r -> ParserTermF l v r
TRightF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> (Max Int, Term1)
go Term2
x
        LocTag
anno :< TTraceF Term2
x -> (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l v r. r -> ParserTermF l v r
TTraceF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> (Max Int, Term1)
go Term2
x
        LocTag
anno :< TLamF (Open ()) Term2
x -> (\(Max Int
n, Term1
r) -> (forall a. a -> Max a
Max Int
n, (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall a b. (a -> b) -> a -> b
$ forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Open (Int -> String
getName Int
n)) Term1
r)) forall a b. (a -> b) -> a -> b
$ Term2 -> (Max Int, Term1)
go Term2
x -- warning, untested
        LocTag
anno :< TLamF (Closed ()) Term2
x -> (\(Max Int
n, Term1
r) -> (forall a. a -> Max a
Max Int
0, (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall a b. (a -> b) -> a -> b
$ forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed (Int -> String
getName Int
n)) Term1
r)) forall a b. (a -> b) -> a -> b
$ Term2 -> (Max Int, Term1)
go Term2
x
        LocTag
anno :< TLimitedRecursionF Term2
t Term2
r Term2
b -> (\Term1
x Term1
y Term1
z -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> r -> ParserTermF l v r
TLimitedRecursionF Term1
x Term1
y Term1
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> (Max Int, Term1)
go Term2
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term2 -> (Max Int, Term1)
go Term2
r forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term2 -> (Max Int, Term1)
go Term2
b
  in forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term2 -> (Max Int, Term1)
go

decompileFragMap :: Map.Map FragIndex (Cofree (FragExprF a) LocTag) -> Term2
decompileFragMap :: forall a. Map FragIndex (Cofree (FragExprF a) LocTag) -> Term2
decompileFragMap Map FragIndex (Cofree (FragExprF a) LocTag)
tm =
  let decomp :: Cofree (FragExprF a) LocTag
             -> Term2
      decomp :: forall a. Cofree (FragExprF a) LocTag -> Term2
decomp = let recur :: Cofree (FragExprF a) LocTag -> Term2
recur = forall a. Cofree (FragExprF a) LocTag -> Term2
decomp in \case
        LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
ZeroFragF -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. ParserTermF l v r
TZeroF
        LocTag
anno :< PairFragF Cofree (FragExprF a) LocTag
a Cofree (FragExprF a) LocTag
b -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TPairF (forall a. Cofree (FragExprF a) LocTag -> Term2
recur Cofree (FragExprF a) LocTag
a) (forall a. Cofree (FragExprF a) LocTag -> Term2
recur Cofree (FragExprF a) LocTag
b)
        LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
EnvFragF -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF Int
0
        LocTag
anno :< SetEnvFragF Cofree (FragExprF a) LocTag
x -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TAppF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed ()) (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TAppF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TLeftF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF Int
0))
                                                                                         (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TRightF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF Int
0))))
                                               (forall a. Cofree (FragExprF a) LocTag -> Term2
recur Cofree (FragExprF a) LocTag
x)
        LocTag
anno :< DeferFragF FragIndex
ind -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< (forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed ()) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Cofree (FragExprF a) LocTag -> Term2
recur forall a b. (a -> b) -> a -> b
$ Map FragIndex (Cofree (FragExprF a) LocTag)
tm forall k a. Ord k => Map k a -> k -> a
Map.! FragIndex
ind)
        LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
AbortFragF -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed ()) (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Open ())
                                            (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TCheckF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed ()) (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF Int
1))
                                                             (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF Int
0)))
        LocTag
anno :< GateFragF Cofree (FragExprF a) LocTag
l Cofree (FragExprF a) LocTag
r -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed ()) (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> r -> ParserTermF l v r
TITEF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF Int
0) (forall a. Cofree (FragExprF a) LocTag -> Term2
recur Cofree (FragExprF a) LocTag
r) (forall a. Cofree (FragExprF a) LocTag -> Term2
recur Cofree (FragExprF a) LocTag
l))
        LocTag
anno :< LeftFragF Cofree (FragExprF a) LocTag
x -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TLeftF (forall a. Cofree (FragExprF a) LocTag -> Term2
recur Cofree (FragExprF a) LocTag
x)
        LocTag
anno :< RightFragF Cofree (FragExprF a) LocTag
x -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TRightF (forall a. Cofree (FragExprF a) LocTag -> Term2
recur Cofree (FragExprF a) LocTag
x)
        LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
TraceFragF -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed ()) (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TTraceF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF Int
0))
        LocTag
anno :< AuxFragF a
_ -> forall a. HasCallStack => String -> a
error String
"decompileFragMap: TODO AuxFrag" -- TLimitedRecursion
  in forall a. Cofree (FragExprF a) LocTag -> Term2
decomp forall a b. (a -> b) -> a -> b
$ forall a. Map FragIndex a -> a
rootFrag Map FragIndex (Cofree (FragExprF a) LocTag)
tm

decompileTerm4 :: Term4 -> Term2
decompileTerm4 :: Term4 -> Term2
decompileTerm4 (Term4 Map FragIndex (Cofree (FragExprF Void) LocTag)
tm) = forall a. Map FragIndex (Cofree (FragExprF a) LocTag) -> Term2
decompileFragMap Map FragIndex (Cofree (FragExprF Void) LocTag)
tm

decompileTerm3 :: Term3 -> Term2
decompileTerm3 :: Term3 -> Term2
decompileTerm3 (Term3 Map FragIndex FragExprUR
tm) = forall a. Map FragIndex (Cofree (FragExprF a) LocTag) -> Term2
decompileFragMap forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map FragExprUR
-> Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag
unFragExprUR Map FragIndex FragExprUR
tm

decompileIExpr :: IExpr -> Term4
decompileIExpr :: IExpr -> Term4
decompileIExpr IExpr
x = let build :: IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build = \case
                         IExpr
Zero     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a
ZeroFrag
                         Pair IExpr
a IExpr
b -> (\Cofree (FragExprF Void) LocTag
x Cofree (FragExprF Void) LocTag
y -> LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> r -> FragExprF a r
PairFragF Cofree (FragExprF Void) LocTag
x Cofree (FragExprF Void) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
b
                         IExpr
Env      -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a
EnvFrag
                         SetEnv IExpr
x -> (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a r. r -> FragExprF a r
SetEnvFragF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
x
                         Gate IExpr
l IExpr
r -> (\Cofree (FragExprF Void) LocTag
x Cofree (FragExprF Void) LocTag
y -> LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> r -> FragExprF a r
GateFragF Cofree (FragExprF Void) LocTag
x Cofree (FragExprF Void) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
r
                         PLeft IExpr
x  -> (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a r. r -> FragExprF a r
LeftFragF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
x
                         PRight IExpr
x -> (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a r. r -> FragExprF a r
RightFragF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
x
                         IExpr
Trace    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a
TraceFrag
                         Defer IExpr
x  -> forall a b. Show a => BreakState' a b -> BreakState' a b
deferF forall a b. (a -> b) -> a -> b
$ IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
x
                   in Map FragIndex (Cofree (FragExprF Void) LocTag) -> Term4
Term4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b.
BreakState' a b -> Map FragIndex (Cofree (FragExprF a) LocTag)
buildFragMap forall a b. (a -> b) -> a -> b
$ forall {b}.
IExpr
-> StateT
     (b, FragIndex, Map FragIndex (Cofree (FragExprF Void) LocTag))
     Identity
     (Cofree (FragExprF Void) LocTag)
build IExpr
x