-- For GHC version 7.10 or higher

{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
{-# LANGUAGE LambdaCase #-}

{-# OPTIONS_GHC -fno-warn-unused-binds #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}

module AbsCubicaltt ( Tree(..)
, Module
, Imp
, Decl
, ExpWhere
, Exp
, Dir
, System
, Face
, Side
, Formula
, Branch
, Label
, Tele
, PTele
, AIdent
, CIdent
, HoleIdent
, johnMajorEq
, module ComposOpCubicaltt ) where

import Prelude ((.), (>), (&&), (==))
import Prelude (Int, (.), (>), (&&), (==))
import qualified Prelude as P

import ComposOpCubicaltt

data Tag = Module_ | Imp_ | Decl_ | ExpWhere_ | Exp_ | Dir_ | System_ | Face_ | Side_ | Formula_ | Branch_ | Label_ | Tele_ | PTele_ | AIdent_ | CIdent_ | HoleIdent_
type Module = Tree 'Module_
type Imp = Tree 'Imp_
type Decl = Tree 'Decl_
type ExpWhere = Tree 'ExpWhere_
type Exp = Tree 'Exp_
type Dir = Tree 'Dir_
type System = Tree 'System_
type Face = Tree 'Face_
type Side = Tree 'Side_
type Formula = Tree 'Formula_
type Branch = Tree 'Branch_
type Label = Tree 'Label_
type Tele = Tree 'Tele_
type PTele = Tree 'PTele_
type AIdent = Tree 'AIdent_
type CIdent = Tree 'CIdent_
type HoleIdent = Tree 'HoleIdent_

data Tree (a :: Tag) where
  Module :: AIdent -> [Imp] -> [Decl] -> Tree 'Module_
  Import :: AIdent -> Tree 'Imp_
  DeclData :: AIdent -> [Tele] -> [Label] -> Tree 'Decl_
  DeclDef :: AIdent -> [Tele] -> Exp -> ExpWhere -> Tree 'Decl_
  DeclHData :: AIdent -> [Tele] -> [Label] -> Tree 'Decl_
  DeclMutual :: [Decl] -> Tree 'Decl_
  DeclOpaque :: AIdent -> Tree 'Decl_
  DeclSplit :: AIdent -> [Tele] -> Exp -> [Branch] -> Tree 'Decl_
  DeclTransparent :: AIdent -> Tree 'Decl_
  DeclTransparentAll :: Tree 'Decl_
  DeclUndef :: AIdent -> [Tele] -> Exp -> Tree 'Decl_
  NoWhere :: Exp -> Tree 'ExpWhere_
  Where :: Exp -> [Decl] -> Tree 'ExpWhere_
  App :: Exp -> Exp -> Tree 'Exp_
  AppFormula :: Exp -> Formula -> Tree 'Exp_
  Comp :: Exp -> Exp -> System -> Tree 'Exp_
  Fill :: Exp -> Exp -> System -> Tree 'Exp_
  Fst :: Exp -> Tree 'Exp_
  Fun :: Exp -> Exp -> Tree 'Exp_
  Glue :: Exp -> System -> Tree 'Exp_
  GlueElem :: Exp -> System -> Tree 'Exp_
  HComp :: Exp -> Exp -> System -> Tree 'Exp_
  Hole :: HoleIdent -> Tree 'Exp_
  Id :: Exp -> Exp -> Exp -> Tree 'Exp_
  IdJ :: Exp -> Exp -> Exp -> Exp -> Exp -> Exp -> Tree 'Exp_
  IdPair :: Exp -> System -> Tree 'Exp_
  Lam :: [PTele] -> Exp -> Tree 'Exp_
  Let :: [Decl] -> Exp -> Tree 'Exp_
  PCon :: AIdent -> Exp -> Tree 'Exp_
  PLam :: [AIdent] -> Exp -> Tree 'Exp_
  Pair :: Exp -> [Exp] -> Tree 'Exp_
  PathP :: Exp -> Exp -> Exp -> Tree 'Exp_
  Pi :: [PTele] -> Exp -> Tree 'Exp_
  Sigma :: [PTele] -> Exp -> Tree 'Exp_
  Snd :: Exp -> Tree 'Exp_
  Split :: Exp -> [Branch] -> Tree 'Exp_
  Trans :: Exp -> Exp -> Tree 'Exp_
  U :: Tree 'Exp_
  UnGlueElem :: Exp -> System -> Tree 'Exp_
  Var :: AIdent -> Tree 'Exp_
  Dir0 :: Tree 'Dir_
  Dir1 :: Tree 'Dir_
  System :: [Side] -> Tree 'System_
  Face :: AIdent -> Dir -> Tree 'Face_
  Side :: [Face] -> Exp -> Tree 'Side_
  Atom :: AIdent -> Tree 'Formula_
  Conj :: Formula -> CIdent -> Formula -> Tree 'Formula_
  Dir :: Dir -> Tree 'Formula_
  Disj :: Formula -> Formula -> Tree 'Formula_
  Neg :: Formula -> Tree 'Formula_
  OBranch :: AIdent -> [AIdent] -> ExpWhere -> Tree 'Branch_
  PBranch :: AIdent -> [AIdent] -> [AIdent] -> ExpWhere -> Tree 'Branch_
  OLabel :: AIdent -> [Tele] -> Tree 'Label_
  PLabel :: AIdent -> [Tele] -> [AIdent] -> System -> Tree 'Label_
  Tele :: AIdent -> [AIdent] -> Exp -> Tree 'Tele_
  PTele :: Exp -> Exp -> Tree 'PTele_
  AIdent :: ((Int,Int),P.String) -> Tree 'AIdent_
  CIdent ::P.String -> Tree 'CIdent_
  HoleIdent :: ((Int,Int),P.String) -> Tree 'HoleIdent_

instance Compos Tree where
  compos r a f = \case
    Module aIdent imps decls -> r Module `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) imps `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) decls
    Import aIdent -> r Import `a` f aIdent
    DeclData aIdent teles labels -> r DeclData `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) teles `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) labels
    DeclDef aIdent teles exp expWhere -> r DeclDef `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) teles `a` f exp `a` f expWhere
    DeclHData aIdent teles labels -> r DeclHData `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) teles `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) labels
    DeclMutual decls -> r DeclMutual `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) decls
    DeclOpaque aIdent -> r DeclOpaque `a` f aIdent
    DeclSplit aIdent teles exp branchs -> r DeclSplit `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) teles `a` f exp `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) branchs
    DeclTransparent aIdent -> r DeclTransparent `a` f aIdent
    DeclUndef aIdent teles exp -> r DeclUndef `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) teles `a` f exp
    NoWhere exp -> r NoWhere `a` f exp
    Where exp decls -> r Where `a` f exp `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) decls
    App exp1 exp2 -> r App `a` f exp1 `a` f exp2
    AppFormula exp formula -> r AppFormula `a` f exp `a` f formula
    Comp exp1 exp2 system -> r Comp `a` f exp1 `a` f exp2 `a` f system
    Fill exp1 exp2 system -> r Fill `a` f exp1 `a` f exp2 `a` f system
    Fst exp -> r Fst `a` f exp
    Fun exp1 exp2 -> r Fun `a` f exp1 `a` f exp2
    Glue exp system -> r Glue `a` f exp `a` f system
    GlueElem exp system -> r GlueElem `a` f exp `a` f system
    HComp exp1 exp2 system -> r HComp `a` f exp1 `a` f exp2 `a` f system
    Hole holeIdent -> r Hole `a` f holeIdent
    Id exp1 exp2 exp3 -> r Id `a` f exp1 `a` f exp2 `a` f exp3
    IdJ exp1 exp2 exp3 exp4 exp5 exp6 -> r IdJ `a` f exp1 `a` f exp2 `a` f exp3 `a` f exp4 `a` f exp5 `a` f exp6
    IdPair exp system -> r IdPair `a` f exp `a` f system
    Lam pTeles exp -> r Lam `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) pTeles `a` f exp
    Let decls exp -> r Let `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) decls `a` f exp
    PCon aIdent exp -> r PCon `a` f aIdent `a` f exp
    PLam aIdents exp -> r PLam `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) aIdents `a` f exp
    Pair exp exps -> r Pair `a` f exp `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) exps
    PathP exp1 exp2 exp3 -> r PathP `a` f exp1 `a` f exp2 `a` f exp3
    Pi pTeles exp -> r Pi `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) pTeles `a` f exp
    Sigma pTeles exp -> r Sigma `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) pTeles `a` f exp
    Snd exp -> r Snd `a` f exp
    Split exp branchs -> r Split `a` f exp `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) branchs
    Trans exp1 exp2 -> r Trans `a` f exp1 `a` f exp2
    UnGlueElem exp system -> r UnGlueElem `a` f exp `a` f system
    Var aIdent -> r Var `a` f aIdent
    System sides -> r System `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) sides
    Face aIdent dir -> r Face `a` f aIdent `a` f dir
    Side faces exp -> r Side `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) faces `a` f exp
    Atom aIdent -> r Atom `a` f aIdent
    Conj formula1 cIdent formula2 -> r Conj `a` f formula1 `a` f cIdent `a` f formula2
    Dir dir -> r Dir `a` f dir
    Disj formula1 formula2 -> r Disj `a` f formula1 `a` f formula2
    Neg formula -> r Neg `a` f formula
    OBranch aIdent aIdents expWhere -> r OBranch `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) aIdents `a` f expWhere
    PBranch aIdent aIdents1 aIdents2 expWhere -> r PBranch `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) aIdents1 `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) aIdents2 `a` f expWhere
    OLabel aIdent teles -> r OLabel `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) teles
    PLabel aIdent teles aIdents system -> r PLabel `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) teles `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) aIdents `a` f system
    Tele aIdent aIdents exp -> r Tele `a` f aIdent `a` P.foldr (\ x z -> r (:) `a` f x `a` z) (r []) aIdents `a` f exp
    PTele exp1 exp2 -> r PTele `a` f exp1 `a` f exp2
    t -> r t

instance P.Show (Tree c) where
  showsPrec n = \case
    AIdent str -> opar . P.showString "AIdent" . P.showChar ' ' . P.showsPrec 1 str . cpar
    CIdent str -> opar . P.showString "CIdent" . P.showChar ' ' . P.showsPrec 1 str . cpar
    HoleIdent str -> opar . P.showString "HoleIdent" . P.showChar ' ' . P.showsPrec 1 str . cpar
    Module aIdent imps decls -> opar . P.showString "Module" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 imps . P.showChar ' ' . P.showsPrec 1 decls . cpar
    Import aIdent -> opar . P.showString "Import" . P.showChar ' ' . P.showsPrec 1 aIdent . cpar
    DeclData aIdent teles labels -> opar . P.showString "DeclData" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 teles . P.showChar ' ' . P.showsPrec 1 labels . cpar
    DeclDef aIdent teles exp expWhere -> opar . P.showString "DeclDef" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 teles . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 expWhere . cpar
    DeclHData aIdent teles labels -> opar . P.showString "DeclHData" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 teles . P.showChar ' ' . P.showsPrec 1 labels . cpar
    DeclMutual decls -> opar . P.showString "DeclMutual" . P.showChar ' ' . P.showsPrec 1 decls . cpar
    DeclOpaque aIdent -> opar . P.showString "DeclOpaque" . P.showChar ' ' . P.showsPrec 1 aIdent . cpar
    DeclSplit aIdent teles exp branchs -> opar . P.showString "DeclSplit" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 teles . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 branchs . cpar
    DeclTransparent aIdent -> opar . P.showString "DeclTransparent" . P.showChar ' ' . P.showsPrec 1 aIdent . cpar
    DeclTransparentAll -> P.showString "DeclTransparentAll"
    DeclUndef aIdent teles exp -> opar . P.showString "DeclUndef" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 teles . P.showChar ' ' . P.showsPrec 1 exp . cpar
    NoWhere exp -> opar . P.showString "NoWhere" . P.showChar ' ' . P.showsPrec 1 exp . cpar
    Where exp decls -> opar . P.showString "Where" . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 decls . cpar
    App exp1 exp2 -> opar . P.showString "App" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . cpar
    AppFormula exp formula -> opar . P.showString "AppFormula" . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 formula . cpar
    Comp exp1 exp2 system -> opar . P.showString "Comp" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . P.showChar ' ' . P.showsPrec 1 system . cpar
    Fill exp1 exp2 system -> opar . P.showString "Fill" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . P.showChar ' ' . P.showsPrec 1 system . cpar
    Fst exp -> opar . P.showString "Fst" . P.showChar ' ' . P.showsPrec 1 exp . cpar
    Fun exp1 exp2 -> opar . P.showString "Fun" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . cpar
    Glue exp system -> opar . P.showString "Glue" . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 system . cpar
    GlueElem exp system -> opar . P.showString "GlueElem" . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 system . cpar
    HComp exp1 exp2 system -> opar . P.showString "HComp" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . P.showChar ' ' . P.showsPrec 1 system . cpar
    Hole holeIdent -> opar . P.showString "Hole" . P.showChar ' ' . P.showsPrec 1 holeIdent . cpar
    Id exp1 exp2 exp3 -> opar . P.showString "Id" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . P.showChar ' ' . P.showsPrec 1 exp3 . cpar
    IdJ exp1 exp2 exp3 exp4 exp5 exp6 -> opar . P.showString "IdJ" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . P.showChar ' ' . P.showsPrec 1 exp3 . P.showChar ' ' . P.showsPrec 1 exp4 . P.showChar ' ' . P.showsPrec 1 exp5 . P.showChar ' ' . P.showsPrec 1 exp6 . cpar
    IdPair exp system -> opar . P.showString "IdPair" . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 system . cpar
    Lam pTeles exp -> opar . P.showString "Lam" . P.showChar ' ' . P.showsPrec 1 pTeles . P.showChar ' ' . P.showsPrec 1 exp . cpar
    Let decls exp -> opar . P.showString "Let" . P.showChar ' ' . P.showsPrec 1 decls . P.showChar ' ' . P.showsPrec 1 exp . cpar
    PCon aIdent exp -> opar . P.showString "PCon" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 exp . cpar
    PLam aIdents exp -> opar . P.showString "PLam" . P.showChar ' ' . P.showsPrec 1 aIdents . P.showChar ' ' . P.showsPrec 1 exp . cpar
    Pair exp exps -> opar . P.showString "Pair" . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 exps . cpar
    PathP exp1 exp2 exp3 -> opar . P.showString "PathP" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . P.showChar ' ' . P.showsPrec 1 exp3 . cpar
    Pi pTeles exp -> opar . P.showString "Pi" . P.showChar ' ' . P.showsPrec 1 pTeles . P.showChar ' ' . P.showsPrec 1 exp . cpar
    Sigma pTeles exp -> opar . P.showString "Sigma" . P.showChar ' ' . P.showsPrec 1 pTeles . P.showChar ' ' . P.showsPrec 1 exp . cpar
    Snd exp -> opar . P.showString "Snd" . P.showChar ' ' . P.showsPrec 1 exp . cpar
    Split exp branchs -> opar . P.showString "Split" . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 branchs . cpar
    Trans exp1 exp2 -> opar . P.showString "Trans" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . cpar
    U -> P.showString "U"
    UnGlueElem exp system -> opar . P.showString "UnGlueElem" . P.showChar ' ' . P.showsPrec 1 exp . P.showChar ' ' . P.showsPrec 1 system . cpar
    Var aIdent -> opar . P.showString "Var" . P.showChar ' ' . P.showsPrec 1 aIdent . cpar
    Dir0 -> P.showString "Dir0"
    Dir1 -> P.showString "Dir1"
    System sides -> opar . P.showString "System" . P.showChar ' ' . P.showsPrec 1 sides . cpar
    Face aIdent dir -> opar . P.showString "Face" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 dir . cpar
    Side faces exp -> opar . P.showString "Side" . P.showChar ' ' . P.showsPrec 1 faces . P.showChar ' ' . P.showsPrec 1 exp . cpar
    Atom aIdent -> opar . P.showString "Atom" . P.showChar ' ' . P.showsPrec 1 aIdent . cpar
    Conj formula1 cIdent formula2 -> opar . P.showString "Conj" . P.showChar ' ' . P.showsPrec 1 formula1 . P.showChar ' ' . P.showsPrec 1 cIdent . P.showChar ' ' . P.showsPrec 1 formula2 . cpar
    Dir dir -> opar . P.showString "Dir" . P.showChar ' ' . P.showsPrec 1 dir . cpar
    Disj formula1 formula2 -> opar . P.showString "Disj" . P.showChar ' ' . P.showsPrec 1 formula1 . P.showChar ' ' . P.showsPrec 1 formula2 . cpar
    Neg formula -> opar . P.showString "Neg" . P.showChar ' ' . P.showsPrec 1 formula . cpar
    OBranch aIdent aIdents expWhere -> opar . P.showString "OBranch" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 aIdents . P.showChar ' ' . P.showsPrec 1 expWhere . cpar
    PBranch aIdent aIdents1 aIdents2 expWhere -> opar . P.showString "PBranch" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 aIdents1 . P.showChar ' ' . P.showsPrec 1 aIdents2 . P.showChar ' ' . P.showsPrec 1 expWhere . cpar
    OLabel aIdent teles -> opar . P.showString "OLabel" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 teles . cpar
    PLabel aIdent teles aIdents system -> opar . P.showString "PLabel" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 teles . P.showChar ' ' . P.showsPrec 1 aIdents . P.showChar ' ' . P.showsPrec 1 system . cpar
    Tele aIdent aIdents exp -> opar . P.showString "Tele" . P.showChar ' ' . P.showsPrec 1 aIdent . P.showChar ' ' . P.showsPrec 1 aIdents . P.showChar ' ' . P.showsPrec 1 exp . cpar
    PTele exp1 exp2 -> opar . P.showString "PTele" . P.showChar ' ' . P.showsPrec 1 exp1 . P.showChar ' ' . P.showsPrec 1 exp2 . cpar
    where
    opar = if n > 0 then P.showChar '(' else P.id
    cpar = if n > 0 then P.showChar ')' else P.id

instance P.Eq (Tree c) where (==) = johnMajorEq

instance P.Ord (Tree c) where compare x y = P.compare (index x) (index y) `P.mappend` compareSame x y

index :: Tree c -> P.Int
index (Module _ _ _) = 1
index (Import _) = 2
index (DeclData _ _ _) = 3
index (DeclDef _ _ _ _) = 4
index (DeclHData _ _ _) = 5
index (DeclMutual _) = 6
index (DeclOpaque _) = 7
index (DeclSplit _ _ _ _) = 8
index (DeclTransparent _) = 9
index (DeclTransparentAll ) = 10
index (DeclUndef _ _ _) = 11
index (NoWhere _) = 12
index (Where _ _) = 13
index (App _ _) = 14
index (AppFormula _ _) = 15
index (Comp _ _ _) = 16
index (Fill _ _ _) = 17
index (Fst _) = 18
index (Fun _ _) = 19
index (Glue _ _) = 20
index (GlueElem _ _) = 21
index (HComp _ _ _) = 22
index (Hole _) = 23
index (Id _ _ _) = 24
index (IdJ _ _ _ _ _ _) = 25
index (IdPair _ _) = 26
index (Lam _ _) = 27
index (Let _ _) = 28
index (PCon _ _) = 29
index (PLam _ _) = 30
index (Pair _ _) = 31
index (PathP _ _ _) = 32
index (Pi _ _) = 33
index (Sigma _ _) = 34
index (Snd _) = 35
index (Split _ _) = 36
index (Trans _ _) = 37
index (U ) = 38
index (UnGlueElem _ _) = 39
index (Var _) = 40
index (Dir0 ) = 41
index (Dir1 ) = 42
index (System _) = 43
index (Face _ _) = 44
index (Side _ _) = 45
index (Atom _) = 46
index (Conj _ _ _) = 47
index (Dir _) = 48
index (Disj _ _) = 49
index (Neg _) = 50
index (OBranch _ _ _) = 51
index (PBranch _ _ _ _) = 52
index (OLabel _ _) = 53
index (PLabel _ _ _ _) = 54
index (Tele _ _ _) = 55
index (PTele _ _) = 56
index (AIdent _) = 57
index (CIdent _) = 58
index (HoleIdent _) = 59

johnMajorEq :: Tree a -> Tree b -> P.Bool
johnMajorEq (Module aIdent imps decls) (Module aIdent_ imps_ decls_) = aIdent == aIdent_ && imps == imps_ && decls == decls_
johnMajorEq (Import aIdent) (Import aIdent_) = aIdent == aIdent_
johnMajorEq (DeclData aIdent teles labels) (DeclData aIdent_ teles_ labels_) = aIdent == aIdent_ && teles == teles_ && labels == labels_
johnMajorEq (DeclDef aIdent teles exp expWhere) (DeclDef aIdent_ teles_ exp_ expWhere_) = aIdent == aIdent_ && teles == teles_ && exp == exp_ && expWhere == expWhere_
johnMajorEq (DeclHData aIdent teles labels) (DeclHData aIdent_ teles_ labels_) = aIdent == aIdent_ && teles == teles_ && labels == labels_
johnMajorEq (DeclMutual decls) (DeclMutual decls_) = decls == decls_
johnMajorEq (DeclOpaque aIdent) (DeclOpaque aIdent_) = aIdent == aIdent_
johnMajorEq (DeclSplit aIdent teles exp branchs) (DeclSplit aIdent_ teles_ exp_ branchs_) = aIdent == aIdent_ && teles == teles_ && exp == exp_ && branchs == branchs_
johnMajorEq (DeclTransparent aIdent) (DeclTransparent aIdent_) = aIdent == aIdent_
johnMajorEq DeclTransparentAll DeclTransparentAll = P.True
johnMajorEq (DeclUndef aIdent teles exp) (DeclUndef aIdent_ teles_ exp_) = aIdent == aIdent_ && teles == teles_ && exp == exp_
johnMajorEq (NoWhere exp) (NoWhere exp_) = exp == exp_
johnMajorEq (Where exp decls) (Where exp_ decls_) = exp == exp_ && decls == decls_
johnMajorEq (App exp1 exp2) (App exp1_ exp2_) = exp1 == exp1_ && exp2 == exp2_
johnMajorEq (AppFormula exp formula) (AppFormula exp_ formula_) = exp == exp_ && formula == formula_
johnMajorEq (Comp exp1 exp2 system) (Comp exp1_ exp2_ system_) = exp1 == exp1_ && exp2 == exp2_ && system == system_
johnMajorEq (Fill exp1 exp2 system) (Fill exp1_ exp2_ system_) = exp1 == exp1_ && exp2 == exp2_ && system == system_
johnMajorEq (Fst exp) (Fst exp_) = exp == exp_
johnMajorEq (Fun exp1 exp2) (Fun exp1_ exp2_) = exp1 == exp1_ && exp2 == exp2_
johnMajorEq (Glue exp system) (Glue exp_ system_) = exp == exp_ && system == system_
johnMajorEq (GlueElem exp system) (GlueElem exp_ system_) = exp == exp_ && system == system_
johnMajorEq (HComp exp1 exp2 system) (HComp exp1_ exp2_ system_) = exp1 == exp1_ && exp2 == exp2_ && system == system_
johnMajorEq (Hole holeIdent) (Hole holeIdent_) = holeIdent == holeIdent_
johnMajorEq (Id exp1 exp2 exp3) (Id exp1_ exp2_ exp3_) = exp1 == exp1_ && exp2 == exp2_ && exp3 == exp3_
johnMajorEq (IdJ exp1 exp2 exp3 exp4 exp5 exp6) (IdJ exp1_ exp2_ exp3_ exp4_ exp5_ exp6_) = exp1 == exp1_ && exp2 == exp2_ && exp3 == exp3_ && exp4 == exp4_ && exp5 == exp5_ && exp6 == exp6_
johnMajorEq (IdPair exp system) (IdPair exp_ system_) = exp == exp_ && system == system_
johnMajorEq (Lam pTeles exp) (Lam pTeles_ exp_) = pTeles == pTeles_ && exp == exp_
johnMajorEq (Let decls exp) (Let decls_ exp_) = decls == decls_ && exp == exp_
johnMajorEq (PCon aIdent exp) (PCon aIdent_ exp_) = aIdent == aIdent_ && exp == exp_
johnMajorEq (PLam aIdents exp) (PLam aIdents_ exp_) = aIdents == aIdents_ && exp == exp_
johnMajorEq (Pair exp exps) (Pair exp_ exps_) = exp == exp_ && exps == exps_
johnMajorEq (PathP exp1 exp2 exp3) (PathP exp1_ exp2_ exp3_) = exp1 == exp1_ && exp2 == exp2_ && exp3 == exp3_
johnMajorEq (Pi pTeles exp) (Pi pTeles_ exp_) = pTeles == pTeles_ && exp == exp_
johnMajorEq (Sigma pTeles exp) (Sigma pTeles_ exp_) = pTeles == pTeles_ && exp == exp_
johnMajorEq (Snd exp) (Snd exp_) = exp == exp_
johnMajorEq (Split exp branchs) (Split exp_ branchs_) = exp == exp_ && branchs == branchs_
johnMajorEq (Trans exp1 exp2) (Trans exp1_ exp2_) = exp1 == exp1_ && exp2 == exp2_
johnMajorEq U U = P.True
johnMajorEq (UnGlueElem exp system) (UnGlueElem exp_ system_) = exp == exp_ && system == system_
johnMajorEq (Var aIdent) (Var aIdent_) = aIdent == aIdent_
johnMajorEq Dir0 Dir0 = P.True
johnMajorEq Dir1 Dir1 = P.True
johnMajorEq (System sides) (System sides_) = sides == sides_
johnMajorEq (Face aIdent dir) (Face aIdent_ dir_) = aIdent == aIdent_ && dir == dir_
johnMajorEq (Side faces exp) (Side faces_ exp_) = faces == faces_ && exp == exp_
johnMajorEq (Atom aIdent) (Atom aIdent_) = aIdent == aIdent_
johnMajorEq (Conj formula1 cIdent formula2) (Conj formula1_ cIdent_ formula2_) = formula1 == formula1_ && cIdent == cIdent_ && formula2 == formula2_
johnMajorEq (Dir dir) (Dir dir_) = dir == dir_
johnMajorEq (Disj formula1 formula2) (Disj formula1_ formula2_) = formula1 == formula1_ && formula2 == formula2_
johnMajorEq (Neg formula) (Neg formula_) = formula == formula_
johnMajorEq (OBranch aIdent aIdents expWhere) (OBranch aIdent_ aIdents_ expWhere_) = aIdent == aIdent_ && aIdents == aIdents_ && expWhere == expWhere_
johnMajorEq (PBranch aIdent aIdents1 aIdents2 expWhere) (PBranch aIdent_ aIdents1_ aIdents2_ expWhere_) = aIdent == aIdent_ && aIdents1 == aIdents1_ && aIdents2 == aIdents2_ && expWhere == expWhere_
johnMajorEq (OLabel aIdent teles) (OLabel aIdent_ teles_) = aIdent == aIdent_ && teles == teles_
johnMajorEq (PLabel aIdent teles aIdents system) (PLabel aIdent_ teles_ aIdents_ system_) = aIdent == aIdent_ && teles == teles_ && aIdents == aIdents_ && system == system_
johnMajorEq (Tele aIdent aIdents exp) (Tele aIdent_ aIdents_ exp_) = aIdent == aIdent_ && aIdents == aIdents_ && exp == exp_
johnMajorEq (PTele exp1 exp2) (PTele exp1_ exp2_) = exp1 == exp1_ && exp2 == exp2_
johnMajorEq (AIdent str) (AIdent str_) = str == str_
johnMajorEq (CIdent str) (CIdent str_) = str == str_
johnMajorEq (HoleIdent str) (HoleIdent str_) = str == str_
johnMajorEq _ _ = P.False

compareSame :: Tree c -> Tree c -> P.Ordering
compareSame (Module aIdent imps decls) (Module aIdent_ imps_ decls_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare imps imps_) (P.compare decls decls_))
compareSame (Import aIdent) (Import aIdent_) = P.compare aIdent aIdent_
compareSame (DeclData aIdent teles labels) (DeclData aIdent_ teles_ labels_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare teles teles_) (P.compare labels labels_))
compareSame (DeclDef aIdent teles exp expWhere) (DeclDef aIdent_ teles_ exp_ expWhere_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare teles teles_) (P.mappend (P.compare exp exp_) (P.compare expWhere expWhere_)))
compareSame (DeclHData aIdent teles labels) (DeclHData aIdent_ teles_ labels_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare teles teles_) (P.compare labels labels_))
compareSame (DeclMutual decls) (DeclMutual decls_) = P.compare decls decls_
compareSame (DeclOpaque aIdent) (DeclOpaque aIdent_) = P.compare aIdent aIdent_
compareSame (DeclSplit aIdent teles exp branchs) (DeclSplit aIdent_ teles_ exp_ branchs_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare teles teles_) (P.mappend (P.compare exp exp_) (P.compare branchs branchs_)))
compareSame (DeclTransparent aIdent) (DeclTransparent aIdent_) = P.compare aIdent aIdent_
compareSame DeclTransparentAll DeclTransparentAll = P.EQ
compareSame (DeclUndef aIdent teles exp) (DeclUndef aIdent_ teles_ exp_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare teles teles_) (P.compare exp exp_))
compareSame (NoWhere exp) (NoWhere exp_) = P.compare exp exp_
compareSame (Where exp decls) (Where exp_ decls_) = P.mappend (P.compare exp exp_) (P.compare decls decls_)
compareSame (App exp1 exp2) (App exp1_ exp2_) = P.mappend (P.compare exp1 exp1_) (P.compare exp2 exp2_)
compareSame (AppFormula exp formula) (AppFormula exp_ formula_) = P.mappend (P.compare exp exp_) (P.compare formula formula_)
compareSame (Comp exp1 exp2 system) (Comp exp1_ exp2_ system_) = P.mappend (P.compare exp1 exp1_) (P.mappend (P.compare exp2 exp2_) (P.compare system system_))
compareSame (Fill exp1 exp2 system) (Fill exp1_ exp2_ system_) = P.mappend (P.compare exp1 exp1_) (P.mappend (P.compare exp2 exp2_) (P.compare system system_))
compareSame (Fst exp) (Fst exp_) = P.compare exp exp_
compareSame (Fun exp1 exp2) (Fun exp1_ exp2_) = P.mappend (P.compare exp1 exp1_) (P.compare exp2 exp2_)
compareSame (Glue exp system) (Glue exp_ system_) = P.mappend (P.compare exp exp_) (P.compare system system_)
compareSame (GlueElem exp system) (GlueElem exp_ system_) = P.mappend (P.compare exp exp_) (P.compare system system_)
compareSame (HComp exp1 exp2 system) (HComp exp1_ exp2_ system_) = P.mappend (P.compare exp1 exp1_) (P.mappend (P.compare exp2 exp2_) (P.compare system system_))
compareSame (Hole holeIdent) (Hole holeIdent_) = P.compare holeIdent holeIdent_
compareSame (Id exp1 exp2 exp3) (Id exp1_ exp2_ exp3_) = P.mappend (P.compare exp1 exp1_) (P.mappend (P.compare exp2 exp2_) (P.compare exp3 exp3_))
compareSame (IdJ exp1 exp2 exp3 exp4 exp5 exp6) (IdJ exp1_ exp2_ exp3_ exp4_ exp5_ exp6_) = P.mappend (P.compare exp1 exp1_) (P.mappend (P.compare exp2 exp2_) (P.mappend (P.compare exp3 exp3_) (P.mappend (P.compare exp4 exp4_) (P.mappend (P.compare exp5 exp5_) (P.compare exp6 exp6_)))))
compareSame (IdPair exp system) (IdPair exp_ system_) = P.mappend (P.compare exp exp_) (P.compare system system_)
compareSame (Lam pTeles exp) (Lam pTeles_ exp_) = P.mappend (P.compare pTeles pTeles_) (P.compare exp exp_)
compareSame (Let decls exp) (Let decls_ exp_) = P.mappend (P.compare decls decls_) (P.compare exp exp_)
compareSame (PCon aIdent exp) (PCon aIdent_ exp_) = P.mappend (P.compare aIdent aIdent_) (P.compare exp exp_)
compareSame (PLam aIdents exp) (PLam aIdents_ exp_) = P.mappend (P.compare aIdents aIdents_) (P.compare exp exp_)
compareSame (Pair exp exps) (Pair exp_ exps_) = P.mappend (P.compare exp exp_) (P.compare exps exps_)
compareSame (PathP exp1 exp2 exp3) (PathP exp1_ exp2_ exp3_) = P.mappend (P.compare exp1 exp1_) (P.mappend (P.compare exp2 exp2_) (P.compare exp3 exp3_))
compareSame (Pi pTeles exp) (Pi pTeles_ exp_) = P.mappend (P.compare pTeles pTeles_) (P.compare exp exp_)
compareSame (Sigma pTeles exp) (Sigma pTeles_ exp_) = P.mappend (P.compare pTeles pTeles_) (P.compare exp exp_)
compareSame (Snd exp) (Snd exp_) = P.compare exp exp_
compareSame (Split exp branchs) (Split exp_ branchs_) = P.mappend (P.compare exp exp_) (P.compare branchs branchs_)
compareSame (Trans exp1 exp2) (Trans exp1_ exp2_) = P.mappend (P.compare exp1 exp1_) (P.compare exp2 exp2_)
compareSame U U = P.EQ
compareSame (UnGlueElem exp system) (UnGlueElem exp_ system_) = P.mappend (P.compare exp exp_) (P.compare system system_)
compareSame (Var aIdent) (Var aIdent_) = P.compare aIdent aIdent_
compareSame Dir0 Dir0 = P.EQ
compareSame Dir1 Dir1 = P.EQ
compareSame (System sides) (System sides_) = P.compare sides sides_
compareSame (Face aIdent dir) (Face aIdent_ dir_) = P.mappend (P.compare aIdent aIdent_) (P.compare dir dir_)
compareSame (Side faces exp) (Side faces_ exp_) = P.mappend (P.compare faces faces_) (P.compare exp exp_)
compareSame (Atom aIdent) (Atom aIdent_) = P.compare aIdent aIdent_
compareSame (Conj formula1 cIdent formula2) (Conj formula1_ cIdent_ formula2_) = P.mappend (P.compare formula1 formula1_) (P.mappend (P.compare cIdent cIdent_) (P.compare formula2 formula2_))
compareSame (Dir dir) (Dir dir_) = P.compare dir dir_
compareSame (Disj formula1 formula2) (Disj formula1_ formula2_) = P.mappend (P.compare formula1 formula1_) (P.compare formula2 formula2_)
compareSame (Neg formula) (Neg formula_) = P.compare formula formula_
compareSame (OBranch aIdent aIdents expWhere) (OBranch aIdent_ aIdents_ expWhere_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare aIdents aIdents_) (P.compare expWhere expWhere_))
compareSame (PBranch aIdent aIdents1 aIdents2 expWhere) (PBranch aIdent_ aIdents1_ aIdents2_ expWhere_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare aIdents1 aIdents1_) (P.mappend (P.compare aIdents2 aIdents2_) (P.compare expWhere expWhere_)))
compareSame (OLabel aIdent teles) (OLabel aIdent_ teles_) = P.mappend (P.compare aIdent aIdent_) (P.compare teles teles_)
compareSame (PLabel aIdent teles aIdents system) (PLabel aIdent_ teles_ aIdents_ system_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare teles teles_) (P.mappend (P.compare aIdents aIdents_) (P.compare system system_)))
compareSame (Tele aIdent aIdents exp) (Tele aIdent_ aIdents_ exp_) = P.mappend (P.compare aIdent aIdent_) (P.mappend (P.compare aIdents aIdents_) (P.compare exp exp_))
compareSame (PTele exp1 exp2) (PTele exp1_ exp2_) = P.mappend (P.compare exp1 exp1_) (P.compare exp2 exp2_)
compareSame (AIdent str) (AIdent str_) = P.compare str str_
compareSame (CIdent str) (CIdent str_) = P.compare str str_
compareSame (HoleIdent str) (HoleIdent str_) = P.compare str str_
compareSame _ _ = P.error "BNFC error: compareSame"