{-# 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 OverloadedStrings #-}
{-# 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.Function (on)
import Data.Functor (void)
import Data.List (intercalate, nub, (\\))
import Data.Maybe (fromMaybe)
import Data.String
import Free.Scoped
import Free.Scoped.TH
import Debug.Trace
import qualified Language.Rzk.Syntax as Rzk
data RzkPosition = RzkPosition
{ RzkPosition -> Maybe [Char]
rzkFilePath :: Maybe FilePath
, RzkPosition -> BNFC'Position
rzkLineCol :: Rzk.BNFC'Position
}
ppRzkPosition :: RzkPosition -> String
ppRzkPosition :: RzkPosition -> [Char]
ppRzkPosition RzkPosition{Maybe [Char]
BNFC'Position
rzkLineCol :: BNFC'Position
rzkFilePath :: Maybe [Char]
rzkLineCol :: RzkPosition -> BNFC'Position
rzkFilePath :: RzkPosition -> Maybe [Char]
..} = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
":" forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [forall a. a -> Maybe a -> a
fromMaybe [Char]
"<stdin>" Maybe [Char]
rzkFilePath]
, forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Int
row, Int
col) -> forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Int
row, Int
col]) BNFC'Position
rzkLineCol]
newtype VarIdent = VarIdent { VarIdent -> VarIdent' RzkPosition
getVarIdent :: Rzk.VarIdent' RzkPosition }
instance Eq VarIdent where
== :: VarIdent -> VarIdent -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarIdent -> VarIdent' RzkPosition
getVarIdent)
instance IsString VarIdent where
fromString :: [Char] -> VarIdent
fromString [Char]
s = VarIdent' RzkPosition -> VarIdent
VarIdent (forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent (Maybe [Char] -> BNFC'Position -> RzkPosition
RzkPosition forall a. Maybe a
Nothing forall a. Maybe a
Nothing) (forall a. IsString a => [Char] -> a
fromString [Char]
s))
ppVarIdentWithLocation :: VarIdent -> String
ppVarIdentWithLocation :: VarIdent -> [Char]
ppVarIdentWithLocation (VarIdent var :: VarIdent' RzkPosition
var@(Rzk.VarIdent RzkPosition
pos VarIdentToken
_ident)) =
forall a. Print a => a -> [Char]
Rzk.printTree VarIdent' RzkPosition
var forall a. Semigroup a => a -> a -> a
<> [Char]
" (" forall a. Semigroup a => a -> a -> a
<> RzkPosition -> [Char]
ppRzkPosition RzkPosition
pos forall a. Semigroup a => a -> a -> a
<> [Char]
")"
varIdent :: Rzk.VarIdent -> VarIdent
varIdent :: VarIdent -> VarIdent
varIdent = Maybe [Char] -> VarIdent -> VarIdent
varIdentAt forall a. Maybe a
Nothing
varIdentAt :: Maybe FilePath -> Rzk.VarIdent -> VarIdent
varIdentAt :: Maybe [Char] -> VarIdent -> VarIdent
varIdentAt Maybe [Char]
path (Rzk.VarIdent BNFC'Position
pos VarIdentToken
ident) = VarIdent' RzkPosition -> VarIdent
VarIdent (forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent (Maybe [Char] -> BNFC'Position -> RzkPosition
RzkPosition Maybe [Char]
path BNFC'Position
pos) VarIdentToken
ident)
fromVarIdent :: VarIdent -> Rzk.VarIdent
fromVarIdent :: VarIdent -> VarIdent
fromVarIdent (VarIdent (Rzk.VarIdent (RzkPosition Maybe [Char]
_file BNFC'Position
pos) VarIdentToken
ident)) = forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent BNFC'Position
pos VarIdentToken
ident
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 VarIdent) term (Maybe scope) scope
| TypeSigmaF (Maybe VarIdent) term scope
| TypeIdF term (Maybe term) term
| AppF term term
| LambdaF (Maybe 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
| UnitF
| TypeUnitF
| 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