{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures -fno-warn-missing-signatures -fno-warn-type-defaults #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeSynonymInstances #-} module Language.Rzk.Free.Syntax where import Data.Bifunctor.TH import Data.Char (chr, ord) import Data.Coerce import Data.List (nub, (\\)) import Data.String import Free.Scoped import Free.Scoped.TH import qualified Language.Rzk.Syntax as Rzk data TermF scope term = UniverseF | UniverseCubeF | UniverseTopeF | CubeUnitF | CubeUnitStarF | Cube2F | Cube2_0F | Cube2_1F | CubeProductF term term | TopeTopF | TopeBottomF | TopeEQF term term | TopeLEQF term term | TopeAndF term term | TopeOrF term term | RecBottomF | RecOrF [(term, term)] | TypeFunF (Maybe Rzk.VarIdent) term (Maybe scope) scope | TypeSigmaF (Maybe Rzk.VarIdent) term scope | TypeIdF term (Maybe term) term | AppF term term | LambdaF (Maybe Rzk.VarIdent) (Maybe (term, Maybe scope)) scope | PairF term term | FirstF term | SecondF term | ReflF (Maybe (term, Maybe term)) | IdJF term term term term term term | TypeAscF term term | TypeRestrictedF term [(term, term)] deriving (TermF scope term -> TermF scope term -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a forall scope term. (Eq term, Eq scope) => TermF scope term -> TermF scope term -> Bool /= :: TermF scope term -> TermF scope term -> Bool $c/= :: forall scope term. (Eq term, Eq scope) => TermF scope term -> TermF scope term -> Bool == :: TermF scope term -> TermF scope term -> Bool $c== :: forall scope term. (Eq term, Eq scope) => TermF scope term -> TermF scope term -> Bool Eq) deriveBifunctor ''TermF deriveBifoldable ''TermF deriveBitraversable ''TermF