{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE CPP                   #-}

import Control.Monad
import qualified Language.Lua as LUA -- from language-lua
import Generics.MultiRec hiding (show)
import Generics.MultiRec.Transformations.Main

-- From https://github.com/leafo/lapis/commits/629c559094df41694bea0a33a2be75115c544dad/lapis/application.lua
files :: [FilePath]
files = ["examples/LUA_project/" ++ f
        | f <- [ "application.lua." ++ show n | n <- [1..90] ] ]

--------------------------------------------------------------------------------
-- Main
--------------------------------------------------------------------------------
main :: IO ()
main = do
  putStrLn "Parsing"
  psr <- forM files $ LUA.parseFile
  let ps = [ (p,f) | (Right p,f) <- zip psr files ]
  putStrLn "Diffing"
  forM_ (zip ps (tail ps)) $ \((p1,f1),(p2,f2)) -> do
    putStrLn $ f1 ++ " --> " ++ f2
    let df = diff Block p1 p2
    print $ length df
    print $ apply Block p1 df == Just p2

--------------------------------------------------------------------------------
-- Multirec instance
--------------------------------------------------------------------------------
data AST :: * -> * where
  Stat :: AST LUA.Stat
  Exp :: AST LUA.Exp
  Var :: AST LUA.Var
  Binop :: AST LUA.Binop
  Unop :: AST LUA.Unop
  PrefixExp :: AST LUA.PrefixExp
  TableField :: AST LUA.TableField
  Block :: AST LUA.Block
  FunName :: AST LUA.FunName
  FunBody :: AST LUA.FunBody
  FunCall :: AST LUA.FunCall
  FunArg :: AST LUA.FunArg

deriving instance Ord LUA.Stat
deriving instance Ord LUA.Exp
deriving instance Ord LUA.Var
deriving instance Ord LUA.Binop
deriving instance Ord LUA.Unop
deriving instance Ord LUA.PrefixExp
deriving instance Ord LUA.TableField
deriving instance Ord LUA.Block
deriving instance Ord LUA.FunName
deriving instance Ord LUA.FunBody
deriving instance Ord LUA.FunCall
deriving instance Ord LUA.FunArg


#if OLD_APPROACH
instance Transform AST

instance OrdI AST where
  indexI Stat = 0
  indexI Exp = 1
  indexI Var = 2
  indexI Binop = 3
  indexI Unop = 4
  indexI PrefixExp = 5
  indexI TableField = 6
  indexI Block = 7
  indexI FunName = 8
  indexI FunBody = 9
  indexI FunCall = 10
  indexI FunArg = 11
#else
type instance Ixs AST = '[ LUA.Stat, LUA.Exp, LUA.Var, LUA.Binop, LUA.Unop, LUA.PrefixExp, LUA.TableField, LUA.Block, LUA.FunName, LUA.FunBody, LUA.FunCall, LUA.FunArg ]
#endif

-- Automatically generated and manually edited
data Assign
data FunCall
data Label
data Break
data Goto
data Do
data While
data Repeat
data If
data ForRange
data ForIn
data FunAssign
data LocalFunAssign
data LocalAssign
data EmptyStat
instance Constructor Assign where
  conName _ = "Assign"
instance Constructor FunCall where
  conName _ = "FunCall"
instance Constructor Label where
  conName _ = "Label"
instance Constructor Break where
  conName _ = "Break"
instance Constructor Goto where
  conName _ = "Goto"
instance Constructor Do where
  conName _ = "Do"
instance Constructor While where
  conName _ = "While"
instance Constructor Repeat where
  conName _ = "Repeat"
instance Constructor If where
  conName _ = "If"
instance Constructor ForRange where
  conName _ = "ForRange"
instance Constructor ForIn where
  conName _ = "ForIn"
instance Constructor FunAssign where
  conName _ = "FunAssign"
instance Constructor LocalFunAssign where
  conName _ = "LocalFunAssign"
instance Constructor LocalAssign where
  conName _ = "LocalAssign"
instance Constructor EmptyStat where
  conName _ = "EmptyStat"
data Nil
data LBool
data Number
data LString
data Vararg
data EFunDef
data PrefixExp
data TableConst
data Binop
data Unop
instance Constructor Nil where
  conName _ = "Nil"
instance Constructor LBool where
  conName _ = "Bool"
instance Constructor Number where
  conName _ = "Number"
instance Constructor LString where
  conName _ = "String"
instance Constructor Vararg where
  conName _ = "Vararg"
instance Constructor EFunDef where
  conName _ = "EFunDef"
instance Constructor PrefixExp where
  conName _ = "PrefixExp"
instance Constructor TableConst where
  conName _ = "TableConst"
instance Constructor Binop where
  conName _ = "Binop"
instance Constructor Unop where
  conName _ = "Unop"
data VarName
data Select
data SelectName
instance Constructor VarName where
  conName _ = "VarName"
instance Constructor Select where
  conName _ = "Select"
instance Constructor SelectName where
  conName _ = "SelectName"
data Add
data Sub
data Mul
data Div
data Exp
data Mod
data Concat
data LT
data LTE
data GT
data GTE
data EQ
data NEQ
data And
data Or
instance Constructor Add where
  conName _ = "Add"
instance Constructor Sub where
  conName _ = "Sub"
instance Constructor Mul where
  conName _ = "Mul"
instance Constructor Div where
  conName _ = "Div"
instance Constructor Exp where
  conName _ = "Exp"
instance Constructor Mod where
  conName _ = "Mod"
instance Constructor Concat where
  conName _ = "Concat"
instance Constructor LT where
  conName _ = "LT"
instance Constructor LTE where
  conName _ = "LTE"
instance Constructor GT where
  conName _ = "GT"
instance Constructor GTE where
  conName _ = "GTE"
instance Constructor EQ where
  conName _ = "EQ"
instance Constructor NEQ where
  conName _ = "NEQ"
instance Constructor And where
  conName _ = "And"
instance Constructor Or where
  conName _ = "Or"
data Neg
data Not
data Len
instance Constructor Neg where
  conName _ = "Neg"
instance Constructor Not where
  conName _ = "Not"
instance Constructor Len where
  conName _ = "Len"
data PEVar
data PEFunCall
data Paren
instance Constructor PEVar where
  conName _ = "PEVar"
instance Constructor PEFunCall where
  conName _ = "PEFunCall"
instance Constructor Paren where
  conName _ = "Paren"
data ExpField
data NamedField
data Field
instance Constructor ExpField where
  conName _ = "ExpField"
instance Constructor NamedField where
  conName _ = "NamedField"
instance Constructor Field where
  conName _ = "Field"
data Block
instance Constructor Block where
  conName _ = "Block"
data FunName
instance Constructor FunName where
  conName _ = "FunName"
data FunBody
instance Constructor FunBody where
  conName _ = "FunBody"
data NormalFunCall
data MethodCall
instance Constructor NormalFunCall where
  conName _ = "NormalFunCall"
instance Constructor MethodCall where
  conName _ = "MethodCall"
data Args
data TableArg
data StringArg
instance Constructor Args where
  conName _ = "Args"
instance Constructor TableArg where
  conName _ = "TableArg"
instance Constructor StringArg where
  conName _ = "StringArg"

type instance PF AST = (:+:) ((:>:)
  ((:+:) (C Assign ((:*:) ((:.:) [] (I LUA.Var)) ((:.:) [] (I LUA.Exp))))
  ((:+:) (C FunCall (I LUA.FunCall))
  ((:+:) (C Label (K LUA.Name))
  ((:+:) (C Break U)
  ((:+:) (C Goto (K LUA.Name))
  ((:+:) (C Do (I LUA.Block))
  ((:+:) (C While ((:*:) (I LUA.Exp) (I LUA.Block)))
  ((:+:) (C Repeat ((:*:) (I LUA.Block) (I LUA.Exp)))
  ((:+:) (C If ((:*:) ((:.:) [] ((:*:) (I LUA.Exp) (I LUA.Block))) ((:.:) Maybe (I LUA.Block)))) -- Manually changed, is it correct?
  ((:+:) (C ForRange ((:*:) (K LUA.Name) ((:*:) (I LUA.Exp) ((:*:) (I LUA.Exp) ((:*:) ((:.:) Maybe (I LUA.Exp)) (I LUA.Block))))))
  ((:+:) (C ForIn ((:*:) ((:.:) [] (K LUA.Name)) ((:*:) ((:.:) [] (I LUA.Exp)) (I LUA.Block))))
  ((:+:) (C FunAssign ((:*:) (I LUA.FunName) (I LUA.FunBody)))
  ((:+:) (C LocalFunAssign ((:*:) (K LUA.Name) (I LUA.FunBody)))
  ((:+:) (C LocalAssign ((:*:) ((:.:) [] (K LUA.Name)) ((:.:) Maybe ((:.:) [] (I LUA.Exp)))))
   (C EmptyStat U))))))))))))))) LUA.Stat) ((:+:) ((:>:)
  ((:+:) (C Nil U)
  ((:+:) (C LBool (K Bool))
  ((:+:) (C Number (K String))
  ((:+:) (C LString (K String))
  ((:+:) (C Vararg U)
  ((:+:) (C EFunDef (I LUA.FunBody))
  ((:+:) (C PrefixExp (I LUA.PrefixExp))
  ((:+:) (C TableConst ((:.:) [] (I LUA.TableField)))
  ((:+:) (C Binop ((:*:) (I LUA.Binop) ((:*:) (I LUA.Exp) (I LUA.Exp))))
   (C Unop ((:*:) (I LUA.Unop) (I LUA.Exp)))))))))))) LUA.Exp) ((:+:) ((:>:)
  ((:+:) (C VarName (K LUA.Name))
  ((:+:) (C Select ((:*:) (I LUA.PrefixExp) (I LUA.Exp))) (C SelectName ((:*:) (I LUA.PrefixExp) (K LUA.Name))))) LUA.Var) ((:+:) ((:>:)
  ((:+:) (C Add U)
  ((:+:) (C Sub U)
  ((:+:) (C Mul U)
  ((:+:) (C Div U)
  ((:+:) (C Exp U)
  ((:+:) (C Mod U)
  ((:+:) (C Concat U)
  ((:+:) (C LT U)
  ((:+:) (C LTE U)
  ((:+:) (C GT U)
  ((:+:) (C GTE U)
  ((:+:) (C EQ U)
  ((:+:) (C NEQ U)
  ((:+:) (C And U) (C Or U))))))))))))))) LUA.Binop)
  ((:+:) ((:>:)
  ((:+:) (C Neg U)
  ((:+:) (C Not U) (C Len U))) LUA.Unop)
  ((:+:) ((:>:)
  ((:+:) (C PEVar (I LUA.Var))
  ((:+:) (C PEFunCall (I LUA.FunCall)) (C Paren (I LUA.Exp)))) LUA.PrefixExp)
  ((:+:) ((:>:)
  ((:+:) (C ExpField ((:*:) (I LUA.Exp) (I LUA.Exp)))
  ((:+:) (C NamedField ((:*:) (K LUA.Name) (I LUA.Exp))) (C Field (I LUA.Exp)))) LUA.TableField)
  ((:+:) ((:>:) (C Block ((:*:) ((:.:) [] (I LUA.Stat)) ((:.:) Maybe ((:.:) [] (I LUA.Exp))))) LUA.Block)
  ((:+:) ((:>:) (C FunName ((:*:) (K LUA.Name) ((:*:) ((:.:) [] (K LUA.Name)) ((:.:) Maybe (K LUA.Name))))) LUA.FunName)
  ((:+:) ((:>:) (C FunBody ((:*:) ((:.:) [] (K LUA.Name)) ((:*:) (K Bool) (I LUA.Block)))) LUA.FunBody)
  ((:+:) ((:>:)
  ((:+:) (C NormalFunCall ((:*:) (I LUA.PrefixExp) (I LUA.FunArg))) (C MethodCall ((:*:) (I LUA.PrefixExp) ((:*:) (K LUA.Name) (I LUA.FunArg))))) LUA.FunCall) ((:>:)
  ((:+:) (C Args ((:.:) [] (I LUA.Exp)))
  ((:+:) (C TableArg ((:.:) [] (I LUA.TableField))) (C StringArg (K String)))) LUA.FunArg)))))))))))

instance El AST LUA.Stat where
  proof = Stat
instance El AST LUA.Exp where
  proof = Exp
instance El AST LUA.Var where
  proof = Var
instance El AST LUA.Binop where
  proof = Binop
instance El AST LUA.Unop where
  proof = Unop
instance El AST LUA.PrefixExp where
  proof = PrefixExp
instance El AST LUA.TableField where
  proof = TableField
instance El AST LUA.Block where
  proof = Block
instance El AST LUA.FunName where
  proof = FunName
instance El AST LUA.FunBody where
  proof = FunBody
instance El AST LUA.FunCall where
  proof = FunCall
instance El AST LUA.FunArg where
  proof = FunArg
instance Fam AST where
  from Stat (LUA.Assign f0 f1)
    = L (Tag
           (L (C ((:*:)
                    ((D . (fmap (I . I0))) f0) ((D . (fmap (I . I0))) f1)))))
  from Stat (LUA.FunCall f0)
    = L (Tag (R (L (C ((I . I0) f0)))))
  from Stat (LUA.Label f0) = L (Tag (R (R (L (C (K f0))))))
  from Stat LUA.Break = L (Tag (R (R (R (L (C U))))))
  from Stat (LUA.Goto f0) = L (Tag (R (R (R (R (L (C (K f0))))))))
  from Stat (LUA.Do f0)
    = L (Tag (R (R (R (R (R (L (C ((I . I0) f0)))))))))
  from Stat (LUA.While f0 f1)
    = L (Tag
           (R (R (R (R (R (R (L (C ((:*:)
                                      ((I . I0) f0) ((I . I0) f1)))))))))))
  from Stat (LUA.Repeat f0 f1)
    = L (Tag
           (R (R (R (R (R (R (R (L (C ((:*:)
                                         ((I . I0) f0) ((I . I0) f1))))))))))))
  from Stat (LUA.If f0 f1)
    = L (Tag
           (R (R (R (R (R (R (R (R (L (C ((:*:)
                                            (D [((I . I0) e :*: (I . I0) b) | (e, b) <- f0])
                                            ((D . (fmap (I . I0))) f1)))))))))))))
  from Stat (LUA.ForRange f0 f1 f2 f3 f4)
    = L (Tag
           (R (R (R (R (R (R (R (R (R (L (C ((:*:)
                                               (K f0)
                                               ((:*:)
                                                  ((I . I0) f1)
                                                  ((:*:)
                                                     ((I . I0) f2)
                                                     ((:*:)
                                                        ((D . (fmap (I . I0))) f3)
                                                        ((I . I0) f4)))))))))))))))))
  from Stat (LUA.ForIn f0 f1 f2)
    = L (Tag
           (R (R (R (R (R (R (R (R (R (R (L (C ((:*:)
                                                  ((D . (fmap K)) f0)
                                                  ((:*:)
                                                     ((D . (fmap (I . I0))) f1)
                                                     ((I . I0) f2))))))))))))))))
  from Stat (LUA.FunAssign f0 f1)
    = L (Tag
           (R (R (R (R (R (R (R (R (R (R (R (L (C ((:*:)
                                                     ((I . I0) f0) ((I . I0) f1))))))))))))))))
  from Stat (LUA.LocalFunAssign f0 f1)
    = L (Tag
           (R (R (R (R (R (R (R (R (R (R (R (R (L (C ((:*:)
                                                        (K f0) ((I . I0) f1)))))))))))))))))
  from Stat (LUA.LocalAssign f0 f1)
    = L (Tag
           (R (R (R (R (R (R (R (R (R (R (R (R (R (L (C ((:*:)
                                                           ((D . (fmap K)) f0)
                                                           ((D . (fmap (D . (fmap (I . I0)))))
                                                              f1))))))))))))))))))
  from Stat LUA.EmptyStat
    = L (Tag
           (R (R (R (R (R (R (R (R (R (R (R (R (R (R (C U))))))))))))))))
  from Exp LUA.Nil = R (L (Tag (L (C U))))
  from Exp (LUA.Bool f0) = R (L (Tag (R (L (C (K f0))))))
  from Exp (LUA.Number f0) = R (L (Tag (R (R (L (C (K f0)))))))
  from Exp (LUA.String f0) = R (L (Tag (R (R (R (L (C (K f0))))))))
  from Exp LUA.Vararg = R (L (Tag (R (R (R (R (L (C U))))))))
  from Exp (LUA.EFunDef f0)
    = R (L (Tag (R (R (R (R (R (L (C ((I . I0) f0))))))))))
  from Exp (LUA.PrefixExp f0)
    = R (L (Tag (R (R (R (R (R (R (L (C ((I . I0) f0)))))))))))
  from Exp (LUA.TableConst f0)
    = R (L (Tag
              (R (R (R (R (R (R (R (L (C ((D . (fmap (I . I0))) f0))))))))))))
  from Exp (LUA.Binop f0 f1 f2)
    = R (L (Tag
              (R (R (R (R (R (R (R (R (L (C ((:*:)
                                               ((I . I0) f0)
                                               ((:*:) ((I . I0) f1) ((I . I0) f2)))))))))))))))
  from Exp (LUA.Unop f0 f1)
    = R (L (Tag
              (R (R (R (R (R (R (R (R (R (C ((:*:)
                                               ((I . I0) f0) ((I . I0) f1))))))))))))))
  from Var (LUA.VarName f0) = R (R (L (Tag (L (C (K f0))))))
  from Var (LUA.Select f0 f1)
    = R (R (L (Tag (R (L (C ((:*:) ((I . I0) f0) ((I . I0) f1))))))))
  from Var (LUA.SelectName f0 f1)
    = R (R (L (Tag (R (R (C ((:*:) ((I . I0) f0) (K f1))))))))
  from Binop LUA.Add = R (R (R (L (Tag (L (C U))))))
  from Binop LUA.Sub = R (R (R (L (Tag (R (L (C U)))))))
  from Binop LUA.Mul = R (R (R (L (Tag (R (R (L (C U))))))))
  from Binop LUA.Div = R (R (R (L (Tag (R (R (R (L (C U)))))))))
  from Binop LUA.Exp
    = R (R (R (L (Tag (R (R (R (R (L (C U))))))))))
  from Binop LUA.Mod = R (R (R (L (Tag (R (R (R (R (R (L (C U)))))))))))
  from Binop LUA.Concat
    = R (R (R (L (Tag (R (R (R (R (R (R (L (C U))))))))))))
  from Binop LUA.LT
    = R (R (R (L (Tag (R (R (R (R (R (R (R (L (C U)))))))))))))
  from Binop LUA.LTE
    = R (R (R (L (Tag (R (R (R (R (R (R (R (R (L (C U))))))))))))))
  from Binop LUA.GT
    = R (R (R (L (Tag (R (R (R (R (R (R (R (R (R (L (C U)))))))))))))))
  from Binop LUA.GTE
    = R (R (R (L (Tag
                    (R (R (R (R (R (R (R (R (R (R (L (C U))))))))))))))))
  from Binop LUA.EQ
    = R (R (R (L (Tag
                    (R (R (R (R (R (R (R (R (R (R (R (L (C U)))))))))))))))))
  from Binop LUA.NEQ
    = R (R (R (L (Tag
                    (R (R (R (R (R (R (R (R (R (R (R (R (L (C U))))))))))))))))))
  from Binop LUA.And
    = R (R (R (L (Tag
                    (R (R (R (R (R (R (R (R (R (R (R (R (R (L (C U)))))))))))))))))))
  from Binop LUA.Or
    = R (R (R (L (Tag
                    (R (R (R (R (R (R (R (R (R (R (R (R (R (R (C U)))))))))))))))))))
  from Unop LUA.Neg = R (R (R (R (L (Tag (L (C U)))))))
  from Unop LUA.Not = R (R (R (R (L (Tag (R (L (C U))))))))
  from Unop LUA.Len = R (R (R (R (L (Tag (R (R (C U))))))))
  from PrefixExp (LUA.PEVar f0)
    = R (R (R (R (R (L (Tag (L (C ((I . I0) f0)))))))))
  from PrefixExp (LUA.PEFunCall f0)
    = R (R (R (R (R (L (Tag (R (L (C ((I . I0) f0))))))))))
  from PrefixExp (LUA.Paren f0)
    = R (R (R (R (R (L (Tag (R (R (C ((I . I0) f0))))))))))
  from TableField (LUA.ExpField f0 f1)
    = R (R (R (R (R (R (L (Tag
                             (L (C ((:*:) ((I . I0) f0) ((I . I0) f1)))))))))))
  from TableField (LUA.NamedField f0 f1)
    = R (R (R (R (R (R (L (Tag
                             (R (L (C ((:*:) (K f0) ((I . I0) f1))))))))))))
  from TableField (LUA.Field f0)
    = R (R (R (R (R (R (L (Tag (R (R (C ((I . I0) f0)))))))))))
  from Block (LUA.Block f0 f1)
    = R (R (R (R (R (R (R (L (Tag
                                (C ((:*:)
                                      ((D . (fmap (I . I0))) f0)
                                      ((D . (fmap (D . (fmap (I . I0))))) f1)))))))))))
  from FunName (LUA.FunName f0 f1 f2)
    = R (R (R (R (R (R (R (R (L (Tag
                                   (C ((:*:)
                                         (K f0)
                                         ((:*:)
                                            ((D . (fmap K)) f1) ((D . (fmap K)) f2)))))))))))))
  from FunBody (LUA.FunBody f0 f1 f2)
    = R (R (R (R (R (R (R (R (R (L (Tag
                                      (C ((:*:)
                                            ((D . (fmap K)) f0)
                                            ((:*:) (K f1) ((I . I0) f2))))))))))))))
  from FunCall (LUA.NormalFunCall f0 f1)
    = R (R (R (R (R (R (R (R (R (R (L (Tag
                                         (L (C ((:*:) ((I . I0) f0) ((I . I0) f1)))))))))))))))
  from FunCall (LUA.MethodCall f0 f1 f2)
    = R (R (R (R (R (R (R (R (R (R (L (Tag
                                         (R (C ((:*:)
                                                  ((I . I0) f0)
                                                  ((:*:) (K f1) ((I . I0) f2))))))))))))))))
  from FunArg (LUA.Args f0)
    = R (R (R (R (R (R (R (R (R (R (R (Tag
                                         (L (C ((D . (fmap (I . I0))) f0))))))))))))))
  from FunArg (LUA.TableArg f0)
    = R (R (R (R (R (R (R (R (R (R (R (Tag
                                         (R (L (C ((D . (fmap (I . I0))) f0)))))))))))))))
  from FunArg (LUA.StringArg f0)
    = R (R (R (R (R (R (R (R (R (R (R (Tag
                                         (R (R (C (K f0)))))))))))))))
  to Stat (L (Tag (L (C ((:*:) f0 f1)))))
    = LUA.Assign
        (((fmap (unI0 . unI)) . unD) f0) (((fmap (unI0 . unI)) . unD) f1)
  to Stat (L (Tag (R (L (C f0)))))
    = LUA.FunCall ((unI0 . unI) f0)
  to Stat (L (Tag (R (R (L (C f0)))))) = LUA.Label (unK f0)
  to Stat (L (Tag (R (R (R (L (C U))))))) = LUA.Break
  to Stat (L (Tag (R (R (R (R (L (C f0)))))))) = LUA.Goto (unK f0)
  to Stat (L (Tag (R (R (R (R (R (L (C f0)))))))))
    = LUA.Do ((unI0 . unI) f0)
  to Stat (L (Tag (R (R (R (R (R (R (L (C ((:*:) f0 f1)))))))))))
    = LUA.While ((unI0 . unI) f0) ((unI0 . unI) f1)
  to Stat (L (Tag (R (R (R (R (R (R (R (L (C ((:*:) f0 f1))))))))))))
    = LUA.Repeat ((unI0 . unI) f0) ((unI0 . unI) f1)
  to
    Stat
    (L (Tag (R (R (R (R (R (R (R (R (L (C ((:*:) f0 f1)))))))))))))
    = LUA.If
        [((unI0 . unI) e, (unI0 . unI) b)  | (e :*: b) <- unD f0]
        (((fmap (unI0 . unI)) . unD) f1)
  to
    Stat
    (L (Tag (R (R (R (R (R (R (R (R (R (L (C ((:*:) f0
                                                    ((:*:) f1
                                                           ((:*:) f2
                                                                  ((:*:) f3 f4)))))))))))))))))
    = LUA.ForRange
        (unK f0)
        ((unI0 . unI) f1)
        ((unI0 . unI) f2)
        (((fmap (unI0 . unI)) . unD) f3)
        ((unI0 . unI) f4)
  to
    Stat
    (L (Tag (R (R (R (R (R (R (R (R (R (R (L (C ((:*:) f0
                                                       ((:*:) f1 f2))))))))))))))))
    = LUA.ForIn
        (((fmap unK) . unD) f0)
        (((fmap (unI0 . unI)) . unD) f1)
        ((unI0 . unI) f2)
  to
    Stat
    (L (Tag (R (R (R (R (R (R (R (R (R (R (R (L (C ((:*:) f0
                                                          f1))))))))))))))))
    = LUA.FunAssign ((unI0 . unI) f0) ((unI0 . unI) f1)
  to
    Stat
    (L (Tag (R (R (R (R (R (R (R (R (R (R (R (R (L (C ((:*:) f0
                                                             f1)))))))))))))))))
    = LUA.LocalFunAssign (unK f0) ((unI0 . unI) f1)
  to
    Stat
    (L (Tag (R (R (R (R (R (R (R (R (R (R (R (R (R (L (C ((:*:) f0
                                                                f1))))))))))))))))))
    = LUA.LocalAssign
        (((fmap unK) . unD) f0)
        (((fmap ((fmap (unI0 . unI)) . unD)) . unD) f1)
  to
    Stat
    (L (Tag (R (R (R (R (R (R (R (R (R (R (R (R (R (R (C U)))))))))))))))))
    = LUA.EmptyStat
  to Exp (R (L (Tag (L (C U))))) = LUA.Nil
  to Exp (R (L (Tag (R (L (C f0)))))) = LUA.Bool (unK f0)
  to Exp (R (L (Tag (R (R (L (C f0))))))) = LUA.Number (unK f0)
  to Exp (R (L (Tag (R (R (R (L (C f0)))))))) = LUA.String (unK f0)
  to Exp (R (L (Tag (R (R (R (R (L (C U))))))))) = LUA.Vararg
  to Exp (R (L (Tag (R (R (R (R (R (L (C f0))))))))))
    = LUA.EFunDef ((unI0 . unI) f0)
  to Exp (R (L (Tag (R (R (R (R (R (R (L (C f0)))))))))))
    = LUA.PrefixExp ((unI0 . unI) f0)
  to Exp (R (L (Tag (R (R (R (R (R (R (R (L (C f0))))))))))))
    = LUA.TableConst (((fmap (unI0 . unI)) . unD) f0)
  to
    Exp
    (R (L (Tag (R (R (R (R (R (R (R (R (L (C ((:*:) f0
                                                    ((:*:) f1 f2)))))))))))))))
    = LUA.Binop
        ((unI0 . unI) f0) ((unI0 . unI) f1) ((unI0 . unI) f2)
  to
    Exp
    (R (L (Tag (R (R (R (R (R (R (R (R (R (C ((:*:) f0 f1))))))))))))))
    = LUA.Unop ((unI0 . unI) f0) ((unI0 . unI) f1)
  to Var (R (R (L (Tag (L (C f0)))))) = LUA.VarName (unK f0)
  to Var (R (R (L (Tag (R (L (C ((:*:) f0 f1))))))))
    = LUA.Select ((unI0 . unI) f0) ((unI0 . unI) f1)
  to Var (R (R (L (Tag (R (R (C ((:*:) f0 f1))))))))
    = LUA.SelectName ((unI0 . unI) f0) (unK f1)
  to Binop (R (R (R (L (Tag (L (C U))))))) = LUA.Add
  to Binop (R (R (R (L (Tag (R (L (C U)))))))) = LUA.Sub
  to Binop (R (R (R (L (Tag (R (R (L (C U))))))))) = LUA.Mul
  to Binop (R (R (R (L (Tag (R (R (R (L (C U)))))))))) = LUA.Div
  to Binop (R (R (R (L (Tag (R (R (R (R (L (C U)))))))))))
    = LUA.Exp
  to Binop (R (R (R (L (Tag (R (R (R (R (R (L (C U)))))))))))) = LUA.Mod
  to Binop (R (R (R (L (Tag (R (R (R (R (R (R (L (C U)))))))))))))
    = LUA.Concat
  to
    Binop
    (R (R (R (L (Tag (R (R (R (R (R (R (R (L (C U))))))))))))))
    = LUA.LT
  to
    Binop
    (R (R (R (L (Tag (R (R (R (R (R (R (R (R (L (C U)))))))))))))))
    = LUA.LTE
  to
    Binop
    (R (R (R (L (Tag (R (R (R (R (R (R (R (R (R (L (C U))))))))))))))))
    = LUA.GT
  to
    Binop
    (R (R (R (L (Tag (R (R (R (R (R (R (R (R (R (R (L (C U)))))))))))))))))
    = LUA.GTE
  to
    Binop
    (R (R (R (L (Tag (R (R (R (R (R (R (R (R (R (R (R (L (C U))))))))))))))))))
    = LUA.EQ
  to
    Binop
    (R (R (R (L (Tag (R (R (R (R (R (R (R (R (R (R (R (R (L (C U)))))))))))))))))))
    = LUA.NEQ
  to
    Binop
    (R (R (R (L (Tag (R (R (R (R (R (R (R (R (R (R (R (R (R (L (C U))))))))))))))))))))
    = LUA.And
  to
    Binop
    (R (R (R (L (Tag (R (R (R (R (R (R (R (R (R (R (R (R (R (R (C U))))))))))))))))))))
    = LUA.Or
  to Unop (R (R (R (R (L (Tag (L (C U)))))))) = LUA.Neg
  to Unop (R (R (R (R (L (Tag (R (L (C U))))))))) = LUA.Not
  to Unop (R (R (R (R (L (Tag (R (R (C U))))))))) = LUA.Len
  to PrefixExp (R (R (R (R (R (L (Tag (L (C f0)))))))))
    = LUA.PEVar ((unI0 . unI) f0)
  to PrefixExp (R (R (R (R (R (L (Tag (R (L (C f0))))))))))
    = LUA.PEFunCall ((unI0 . unI) f0)
  to PrefixExp (R (R (R (R (R (L (Tag (R (R (C f0))))))))))
    = LUA.Paren ((unI0 . unI) f0)
  to
    TableField
    (R (R (R (R (R (R (L (Tag (L (C ((:*:) f0 f1)))))))))))
    = LUA.ExpField ((unI0 . unI) f0) ((unI0 . unI) f1)
  to
    TableField
    (R (R (R (R (R (R (L (Tag (R (L (C ((:*:) f0 f1))))))))))))
    = LUA.NamedField (unK f0) ((unI0 . unI) f1)
  to TableField (R (R (R (R (R (R (L (Tag (R (R (C f0)))))))))))
    = LUA.Field ((unI0 . unI) f0)
  to Block (R (R (R (R (R (R (R (L (Tag (C ((:*:) f0 f1)))))))))))
    = LUA.Block
        (((fmap (unI0 . unI)) . unD) f0)
        (((fmap ((fmap (unI0 . unI)) . unD)) . unD) f1)
  to
    FunName
    (R (R (R (R (R (R (R (R (L (Tag (C ((:*:) f0
                                              ((:*:) f1 f2)))))))))))))
    = LUA.FunName
        (unK f0) (((fmap unK) . unD) f1) (((fmap unK) . unD) f2)
  to
    FunBody
    (R (R (R (R (R (R (R (R (R (L (Tag (C ((:*:) f0
                                                 ((:*:) f1 f2))))))))))))))
    = LUA.FunBody
        (((fmap unK) . unD) f0) (unK f1) ((unI0 . unI) f2)
  to
    FunCall
    (R (R (R (R (R (R (R (R (R (R (L (Tag (L (C ((:*:) f0
                                                       f1)))))))))))))))
    = LUA.NormalFunCall ((unI0 . unI) f0) ((unI0 . unI) f1)
  to
    FunCall
    (R (R (R (R (R (R (R (R (R (R (L (Tag (R (C ((:*:) f0
                                                       ((:*:) f1 f2))))))))))))))))
    = LUA.MethodCall ((unI0 . unI) f0) (unK f1) ((unI0 . unI) f2)
  to
    FunArg
    (R (R (R (R (R (R (R (R (R (R (R (Tag (L (C f0))))))))))))))
    = LUA.Args (((fmap (unI0 . unI)) . unD) f0)
  to
    FunArg
    (R (R (R (R (R (R (R (R (R (R (R (Tag (R (L (C f0)))))))))))))))
    = LUA.TableArg (((fmap (unI0 . unI)) . unD) f0)
  to
    FunArg
    (R (R (R (R (R (R (R (R (R (R (R (Tag (R (R (C f0)))))))))))))))
    = LUA.StringArg (unK f0)

instance EqS AST where
  eqS Stat Stat = Just Refl
  eqS Exp Exp = Just Refl
  eqS Var Var = Just Refl
  eqS Binop Binop = Just Refl
  eqS Unop Unop = Just Refl
  eqS PrefixExp PrefixExp = Just Refl
  eqS TableField TableField = Just Refl
  eqS Block Block = Just Refl
  eqS FunName FunName = Just Refl
  eqS FunBody FunBody = Just Refl
  eqS FunCall FunCall = Just Refl
  eqS FunArg FunArg = Just Refl
  eqS _ _ = Nothing