{-# 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 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
makePatternsAll ''TermF   -- declare all patterns using Template Haskell

newtype Type term = Type { forall term. Type term -> term
getType :: term }
  deriving (Type term -> Type term -> Bool
forall term. Eq term => Type term -> Type term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type term -> Type term -> Bool
$c/= :: forall term. Eq term => Type term -> Type term -> Bool
== :: Type term -> Type term -> Bool
$c== :: forall term. Eq term => Type term -> Type term -> Bool
Eq, forall a b. a -> Type b -> Type a
forall a b. (a -> b) -> Type a -> Type b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Type b -> Type a
$c<$ :: forall a b. a -> Type b -> Type a
fmap :: forall a b. (a -> b) -> Type a -> Type b
$cfmap :: forall a b. (a -> b) -> Type a -> Type b
Functor, forall a. Eq a => a -> Type a -> Bool
forall a. Num a => Type a -> a
forall a. Ord a => Type a -> a
forall m. Monoid m => Type m -> m
forall a. Type a -> Bool
forall a. Type a -> Int
forall a. Type a -> [a]
forall a. (a -> a -> a) -> Type a -> a
forall m a. Monoid m => (a -> m) -> Type a -> m
forall b a. (b -> a -> b) -> b -> Type a -> b
forall a b. (a -> b -> b) -> b -> Type a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Type a -> a
$cproduct :: forall a. Num a => Type a -> a
sum :: forall a. Num a => Type a -> a
$csum :: forall a. Num a => Type a -> a
minimum :: forall a. Ord a => Type a -> a
$cminimum :: forall a. Ord a => Type a -> a
maximum :: forall a. Ord a => Type a -> a
$cmaximum :: forall a. Ord a => Type a -> a
elem :: forall a. Eq a => a -> Type a -> Bool
$celem :: forall a. Eq a => a -> Type a -> Bool
length :: forall a. Type a -> Int
$clength :: forall a. Type a -> Int
null :: forall a. Type a -> Bool
$cnull :: forall a. Type a -> Bool
toList :: forall a. Type a -> [a]
$ctoList :: forall a. Type a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Type a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Type a -> a
foldr1 :: forall a. (a -> a -> a) -> Type a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Type a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Type a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Type a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Type a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Type a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Type a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Type a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Type a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Type a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Type a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Type a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Type a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Type a -> m
fold :: forall m. Monoid m => Type m -> m
$cfold :: forall m. Monoid m => Type m -> m
Foldable, Functor Type
Foldable Type
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a)
forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
sequence :: forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a)
$csequence :: forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
Traversable)

data TypeInfo term = TypeInfo
  { forall term. TypeInfo term -> term
infoType :: term
  , forall term. TypeInfo term -> Maybe term
infoWHNF :: Maybe term
  , forall term. TypeInfo term -> Maybe term
infoNF   :: Maybe term
  } deriving (TypeInfo term -> TypeInfo term -> Bool
forall term. Eq term => TypeInfo term -> TypeInfo term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeInfo term -> TypeInfo term -> Bool
$c/= :: forall term. Eq term => TypeInfo term -> TypeInfo term -> Bool
== :: TypeInfo term -> TypeInfo term -> Bool
$c== :: forall term. Eq term => TypeInfo term -> TypeInfo term -> Bool
Eq, forall a b. a -> TypeInfo b -> TypeInfo a
forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TypeInfo b -> TypeInfo a
$c<$ :: forall a b. a -> TypeInfo b -> TypeInfo a
fmap :: forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
$cfmap :: forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
Functor, forall a. Eq a => a -> TypeInfo a -> Bool
forall a. Num a => TypeInfo a -> a
forall a. Ord a => TypeInfo a -> a
forall m. Monoid m => TypeInfo m -> m
forall a. TypeInfo a -> Bool
forall a. TypeInfo a -> Int
forall a. TypeInfo a -> [a]
forall a. (a -> a -> a) -> TypeInfo a -> a
forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => TypeInfo a -> a
$cproduct :: forall a. Num a => TypeInfo a -> a
sum :: forall a. Num a => TypeInfo a -> a
$csum :: forall a. Num a => TypeInfo a -> a
minimum :: forall a. Ord a => TypeInfo a -> a
$cminimum :: forall a. Ord a => TypeInfo a -> a
maximum :: forall a. Ord a => TypeInfo a -> a
$cmaximum :: forall a. Ord a => TypeInfo a -> a
elem :: forall a. Eq a => a -> TypeInfo a -> Bool
$celem :: forall a. Eq a => a -> TypeInfo a -> Bool
length :: forall a. TypeInfo a -> Int
$clength :: forall a. TypeInfo a -> Int
null :: forall a. TypeInfo a -> Bool
$cnull :: forall a. TypeInfo a -> Bool
toList :: forall a. TypeInfo a -> [a]
$ctoList :: forall a. TypeInfo a -> [a]
foldl1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
fold :: forall m. Monoid m => TypeInfo m -> m
$cfold :: forall m. Monoid m => TypeInfo m -> m
Foldable, Functor TypeInfo
Foldable TypeInfo
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => TypeInfo (m a) -> m (TypeInfo a)
forall (f :: * -> *) a.
Applicative f =>
TypeInfo (f a) -> f (TypeInfo a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeInfo a -> m (TypeInfo b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeInfo a -> f (TypeInfo b)
sequence :: forall (m :: * -> *) a. Monad m => TypeInfo (m a) -> m (TypeInfo a)
$csequence :: forall (m :: * -> *) a. Monad m => TypeInfo (m a) -> m (TypeInfo a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeInfo a -> m (TypeInfo b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeInfo a -> m (TypeInfo b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeInfo (f a) -> f (TypeInfo a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeInfo (f a) -> f (TypeInfo a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeInfo a -> f (TypeInfo b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeInfo a -> f (TypeInfo b)
Traversable)

type Term = FS TermF
type TermT = FS (AnnF TypeInfo TermF)

termIsWHNF :: TermT var -> TermT var
termIsWHNF :: forall var. TermT var -> TermT var
termIsWHNF t :: TermT var
t@Pure{} = TermT var
t
termIsWHNF (Free (AnnF TypeInfo (TermT var)
info TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
f)) = TermT var
t'
  where
    t' :: TermT var
t' = forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free (forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF TypeInfo (TermT var)
info { infoWHNF :: Maybe (TermT var)
infoWHNF = forall a. a -> Maybe a
Just TermT var
t' } TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
f)

termIsNF :: TermT var -> TermT var
termIsNF :: forall var. TermT var -> TermT var
termIsNF t :: TermT var
t@Pure{} = TermT var
t
termIsNF (Free (AnnF TypeInfo (TermT var)
info TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
f)) = TermT var
t'
  where
    t' :: TermT var
t' = forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free (forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF TypeInfo (TermT var)
info { infoWHNF :: Maybe (TermT var)
infoWHNF = forall a. a -> Maybe a
Just TermT var
t', infoNF :: Maybe (TermT var)
infoNF = forall a. a -> Maybe a
Just TermT var
t' } TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
f)

invalidateWHNF :: TermT var -> TermT var
invalidateWHNF :: forall var. TermT var -> TermT var
invalidateWHNF = forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS forall a b. (a -> b) -> a -> b
$ \(AnnF TypeInfo t
info TermF s t
f) ->
  forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF TypeInfo t
info { infoWHNF :: Maybe t
infoWHNF = forall a. Maybe a
Nothing, infoNF :: Maybe t
infoNF = forall a. Maybe a
Nothing } TermF s t
f

substituteT :: TermT var -> Scope TermT var -> TermT var
substituteT :: forall var.
TermT var -> Scope (FS (AnnF TypeInfo TermF)) var -> TermT var
substituteT TermT var
x = forall (t :: * -> * -> *) a.
Bifunctor t =>
FS t a -> Scope (FS t) a -> FS t a
substitute TermT var
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall var. TermT var -> TermT var
invalidateWHNF

type Term' = Term VarIdent
type TermT' = TermT VarIdent

freeVars :: Term a -> [a]
freeVars :: forall a. Term a -> [a]
freeVars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- FIXME: should be cached in TypeInfo?
partialFreeVarsT :: TermT a -> [a]
partialFreeVarsT :: forall a. TermT a -> [a]
partialFreeVarsT (Pure a
x)             = [a
x]
partialFreeVarsT UniverseT{}          = []
partialFreeVarsT term :: FS (AnnF TypeInfo TermF) a
term@(Free (AnnF TypeInfo (FS (AnnF TypeInfo TermF) a)
info TermF
  (Scope (FS (AnnF TypeInfo TermF)) a) (FS (AnnF TypeInfo TermF) a)
_)) =
  -- FIXME: check correctness (is it ok to use untyped here?)
  forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. Term a -> [a]
freeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ann :: * -> *) (term :: * -> * -> *) a.
(Functor ann, Bifunctor term) =>
FS (AnnF ann term) a -> FS term a
untyped) [FS (AnnF TypeInfo TermF) a
term, forall term. TypeInfo term -> term
infoType TypeInfo (FS (AnnF TypeInfo TermF) a)
info]

-- FIXME: should be cached in TypeInfo?
freeVarsT :: Eq a => (a -> TermT a) -> TermT a -> [a]
freeVarsT :: forall a. Eq a => (a -> TermT a) -> TermT a -> [a]
freeVarsT a -> TermT a
typeOfVar TermT a
t = [a] -> [a] -> [a]
go [] (forall a. TermT a -> [a]
partialFreeVarsT TermT a
t)
  where
    go :: [a] -> [a] -> [a]
go [a]
vars [a]
latest
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
new = [a]
vars
      | Bool
otherwise =
          [a] -> [a] -> [a]
go ([a]
new forall a. Semigroup a => a -> a -> a
<> [a]
vars)
             (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. TermT a -> [a]
partialFreeVarsT forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> TermT a
typeOfVar) [a]
new)
      where
        new :: [a]
new = forall a. Eq a => [a] -> [a]
nub [a]
latest forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
vars

toTerm' :: Rzk.Term -> Term'
toTerm' :: Term -> Term'
toTerm' = forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm forall (t :: * -> * -> *) a. a -> FS t a
Pure

toScope :: VarIdent -> (VarIdent -> Term a) -> Rzk.Term -> Scope Term a
toScope :: forall a.
VarIdent -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScope VarIdent
x VarIdent -> Term a
bvars = forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm forall a b. (a -> b) -> a -> b
$ \VarIdent
z -> if VarIdent
x forall a. Eq a => a -> a -> Bool
== VarIdent
z then forall (t :: * -> * -> *) a. a -> FS t a
Pure forall var. Inc var
Z else forall var. var -> Inc var
S forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarIdent -> Term a
bvars VarIdent
z

toScopePattern :: Rzk.Pattern -> (VarIdent -> Term a) -> Rzk.Term -> Scope Term a
toScopePattern :: forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars = forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm forall a b. (a -> b) -> a -> b
$ \VarIdent
z ->
  case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VarIdent
z (forall {a}. Pattern -> FS TermF a -> [(VarIdent, FS TermF a)]
bindings Pattern
pat (forall (t :: * -> * -> *) a. a -> FS t a
Pure forall var. Inc var
Z)) of
    Just Term (Inc a)
t  -> Term (Inc a)
t
    Maybe (Term (Inc a))
Nothing -> forall var. var -> Inc var
S forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarIdent -> Term a
bvars VarIdent
z
  where
    bindings :: Pattern -> FS TermF a -> [(VarIdent, FS TermF a)]
bindings (Rzk.PatternWildcard BNFC'Position
_loc) FS TermF a
_ = []
    bindings (Rzk.PatternUnit BNFC'Position
_loc)     FS TermF a
_ = []
    bindings (Rzk.PatternVar BNFC'Position
_loc VarIdent
x)    FS TermF a
t = [(VarIdent -> VarIdent
varIdent VarIdent
x, FS TermF a
t)]
    bindings (Rzk.PatternPair BNFC'Position
_loc Pattern
l Pattern
r) FS TermF a
t = Pattern -> FS TermF a -> [(VarIdent, FS TermF a)]
bindings Pattern
l (forall {a}. FS TermF a -> FS TermF a
First FS TermF a
t) forall a. Semigroup a => a -> a -> a
<> Pattern -> FS TermF a -> [(VarIdent, FS TermF a)]
bindings Pattern
r (forall {a}. FS TermF a -> FS TermF a
Second FS TermF a
t)

toTerm :: (VarIdent -> Term a) -> Rzk.Term -> Term a
toTerm :: forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm VarIdent -> Term a
bvars = Term -> Term a
go
  where
    go :: Term -> Term a
go = \case
      Rzk.Var BNFC'Position
_loc VarIdent
x -> VarIdent -> Term a
bvars (VarIdent -> VarIdent
varIdent VarIdent
x)
      Rzk.Universe BNFC'Position
_loc -> forall {a}. FS TermF a
Universe

      Rzk.UniverseCube BNFC'Position
_loc -> forall {a}. FS TermF a
UniverseCube
      Rzk.UniverseTope BNFC'Position
_loc -> forall {a}. FS TermF a
UniverseTope
      Rzk.CubeUnit BNFC'Position
_loc -> forall {a}. FS TermF a
CubeUnit
      Rzk.CubeUnitStar BNFC'Position
_loc -> forall {a}. FS TermF a
CubeUnitStar
      Rzk.Cube2 BNFC'Position
_loc -> forall {a}. FS TermF a
Cube2
      Rzk.Cube2_0 BNFC'Position
_loc -> forall {a}. FS TermF a
Cube2_0
      Rzk.Cube2_1 BNFC'Position
_loc -> forall {a}. FS TermF a
Cube2_1
      Rzk.CubeProduct BNFC'Position
_loc Term
l Term
r -> forall {a}. FS TermF a -> FS TermF a -> FS TermF a
CubeProduct (Term -> Term a
go Term
l) (Term -> Term a
go Term
r)
      Rzk.TopeTop BNFC'Position
_loc -> forall {a}. FS TermF a
TopeTop
      Rzk.TopeBottom BNFC'Position
_loc -> forall {a}. FS TermF a
TopeBottom
      Rzk.TopeEQ BNFC'Position
_loc Term
l Term
r -> forall {a}. FS TermF a -> FS TermF a -> FS TermF a
TopeEQ (Term -> Term a
go Term
l) (Term -> Term a
go Term
r)
      Rzk.TopeLEQ BNFC'Position
_loc Term
l Term
r -> forall {a}. FS TermF a -> FS TermF a -> FS TermF a
TopeLEQ (Term -> Term a
go Term
l) (Term -> Term a
go Term
r)
      Rzk.TopeAnd BNFC'Position
_loc Term
l Term
r -> forall {a}. FS TermF a -> FS TermF a -> FS TermF a
TopeAnd (Term -> Term a
go Term
l) (Term -> Term a
go Term
r)
      Rzk.TopeOr BNFC'Position
_loc Term
l Term
r -> forall {a}. FS TermF a -> FS TermF a -> FS TermF a
TopeOr (Term -> Term a
go Term
l) (Term -> Term a
go Term
r)
      Rzk.RecBottom BNFC'Position
_loc -> forall {a}. FS TermF a
RecBottom
      Rzk.RecOr BNFC'Position
_loc [Restriction' BNFC'Position]
rs -> forall {a}. [(FS TermF a, FS TermF a)] -> FS TermF a
RecOr [ (Term -> Term a
go Term
tope, Term -> Term a
go Term
term) | Rzk.Restriction BNFC'Position
_loc Term
tope Term
term <- [Restriction' BNFC'Position]
rs ]
      Rzk.TypeId BNFC'Position
_loc Term
x Term
tA Term
y -> forall {a}.
FS TermF a -> Maybe (FS TermF a) -> FS TermF a -> FS TermF a
TypeId (Term -> Term a
go Term
x) (forall a. a -> Maybe a
Just (Term -> Term a
go Term
tA)) (Term -> Term a
go Term
y)
      Rzk.TypeIdSimple BNFC'Position
_loc Term
x Term
y -> forall {a}.
FS TermF a -> Maybe (FS TermF a) -> FS TermF a -> FS TermF a
TypeId (Term -> Term a
go Term
x) forall a. Maybe a
Nothing (Term -> Term a
go Term
y)
      Rzk.TypeUnit BNFC'Position
_loc -> forall {a}. FS TermF a
TypeUnit
      Rzk.Unit BNFC'Position
_loc -> forall {a}. FS TermF a
Unit
      Rzk.App BNFC'Position
_loc Term
f Term
x -> forall {a}. FS TermF a -> FS TermF a -> FS TermF a
App (Term -> Term a
go Term
f) (Term -> Term a
go Term
x)
      Rzk.Pair BNFC'Position
_loc Term
l Term
r -> forall {a}. FS TermF a -> FS TermF a -> FS TermF a
Pair (Term -> Term a
go Term
l) (Term -> Term a
go Term
r)
      Rzk.First BNFC'Position
_loc Term
term -> forall {a}. FS TermF a -> FS TermF a
First (Term -> Term a
go Term
term)
      Rzk.Second BNFC'Position
_loc Term
term -> forall {a}. FS TermF a -> FS TermF a
Second (Term -> Term a
go Term
term)
      Rzk.Refl BNFC'Position
_loc -> forall {a}. Maybe (FS TermF a, Maybe (FS TermF a)) -> FS TermF a
Refl forall a. Maybe a
Nothing
      Rzk.ReflTerm BNFC'Position
_loc Term
term -> forall {a}. Maybe (FS TermF a, Maybe (FS TermF a)) -> FS TermF a
Refl (forall a. a -> Maybe a
Just (Term -> Term a
go Term
term, forall a. Maybe a
Nothing))
      Rzk.ReflTermType BNFC'Position
_loc Term
x Term
tA -> forall {a}. Maybe (FS TermF a, Maybe (FS TermF a)) -> FS TermF a
Refl (forall a. a -> Maybe a
Just (Term -> Term a
go Term
x, forall a. a -> Maybe a
Just (Term -> Term a
go Term
tA)))
      Rzk.IdJ BNFC'Position
_loc Term
a Term
b Term
c Term
d Term
e Term
f -> forall {a}.
FS TermF a
-> FS TermF a
-> FS TermF a
-> FS TermF a
-> FS TermF a
-> FS TermF a
-> FS TermF a
IdJ (Term -> Term a
go Term
a) (Term -> Term a
go Term
b) (Term -> Term a
go Term
c) (Term -> Term a
go Term
d) (Term -> Term a
go Term
e) (Term -> Term a
go Term
f)
      Rzk.TypeAsc BNFC'Position
_loc Term
x Term
t -> forall {a}. FS TermF a -> FS TermF a -> FS TermF a
TypeAsc (Term -> Term a
go Term
x) (Term -> Term a
go Term
t)

      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamVarType BNFC'Position
_ Pattern
pat Term
arg) Term
ret ->
        forall {a}.
Maybe VarIdent
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun (Pattern -> Maybe VarIdent
patternVar Pattern
pat) (Term -> Term a
go Term
arg) forall a. Maybe a
Nothing (forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars Term
ret)
      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamVarShape BNFC'Position
_ Pattern
pat Term
cube Term
tope) Term
ret ->
        forall {a}.
Maybe VarIdent
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun (Pattern -> Maybe VarIdent
patternVar Pattern
pat) (Term -> Term a
go Term
cube) (forall a. a -> Maybe a
Just (forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars Term
tope)) (forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars Term
ret)
      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamWildcardType BNFC'Position
_ Term
arg) Term
ret ->
        forall {a}.
Maybe VarIdent
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun forall a. Maybe a
Nothing (Term -> Term a
go Term
arg) forall a. Maybe a
Nothing (forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall var. var -> Inc var
S forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarIdent -> Term a
bvars) Term
ret)
      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamType BNFC'Position
_ Term
arg) Term
ret ->
        forall {a}.
Maybe VarIdent
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun forall a. Maybe a
Nothing (Term -> Term a
go Term
arg) forall a. Maybe a
Nothing (forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall var. var -> Inc var
S forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarIdent -> Term a
bvars) Term
ret)

      Rzk.TypeSigma BNFC'Position
_loc Pattern
pat Term
tA Term
tB ->
        forall {a}.
Maybe VarIdent -> FS TermF a -> Scope (FS TermF) a -> FS TermF a
TypeSigma (Pattern -> Maybe VarIdent
patternVar Pattern
pat) (Term -> Term a
go Term
tA) (forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars Term
tB)

      Rzk.Lambda BNFC'Position
_loc [] Term
body -> Term -> Term a
go Term
body
      Rzk.Lambda BNFC'Position
_loc (Rzk.ParamPattern BNFC'Position
_ Pattern
pat : [Param' BNFC'Position]
params) Term
body ->
        forall {a}.
Maybe VarIdent
-> Maybe (FS TermF a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> FS TermF a
Lambda (Pattern -> Maybe VarIdent
patternVar Pattern
pat) forall a. Maybe a
Nothing (forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars (forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
_loc [Param' BNFC'Position]
params Term
body))
      Rzk.Lambda BNFC'Position
_loc (Rzk.ParamPatternType BNFC'Position
_ [] Term
_ty : [Param' BNFC'Position]
params) Term
body ->
        Term -> Term a
go (forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
_loc [Param' BNFC'Position]
params Term
body)
      Rzk.Lambda BNFC'Position
_loc (Rzk.ParamPatternType BNFC'Position
_ (Pattern
pat:[Pattern]
pats) Term
ty : [Param' BNFC'Position]
params) Term
body ->
        forall {a}.
Maybe VarIdent
-> Maybe (FS TermF a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> FS TermF a
Lambda (Pattern -> Maybe VarIdent
patternVar Pattern
pat) (forall a. a -> Maybe a
Just (Term -> Term a
go Term
ty, forall a. Maybe a
Nothing))
          (forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars (forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
_loc (forall a. a -> [Pattern' a] -> Term' a -> Param' a
Rzk.ParamPatternType BNFC'Position
_loc [Pattern]
pats Term
ty forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body))
      Rzk.Lambda BNFC'Position
_loc (Rzk.ParamPatternShape BNFC'Position
_ Pattern
pat Term
cube Term
tope : [Param' BNFC'Position]
params) Term
body ->
        forall {a}.
Maybe VarIdent
-> Maybe (FS TermF a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> FS TermF a
Lambda (Pattern -> Maybe VarIdent
patternVar Pattern
pat) (forall a. a -> Maybe a
Just (Term -> Term a
go Term
cube, forall a. a -> Maybe a
Just (forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars Term
tope)))
          (forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars (forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
_loc [Param' BNFC'Position]
params Term
body))

      Rzk.TypeRestricted BNFC'Position
_loc Term
ty [Restriction' BNFC'Position]
rs ->
        forall {a}. FS TermF a -> [(FS TermF a, FS TermF a)] -> FS TermF a
TypeRestricted (Term -> Term a
go Term
ty) (forall a b. (a -> b) -> [a] -> [b]
map (\(Rzk.Restriction BNFC'Position
_loc Term
tope Term
term) -> (Term -> Term a
go Term
tope, Term -> Term a
go Term
term)) [Restriction' BNFC'Position]
rs)

      Rzk.Hole BNFC'Position
_loc HoleIdent' BNFC'Position
_ident -> forall a. HasCallStack => [Char] -> a
error [Char]
"holes are not supported"


    patternVar :: Pattern -> Maybe VarIdent
patternVar (Rzk.PatternVar BNFC'Position
_loc VarIdent
x) = forall a. a -> Maybe a
Just (VarIdent -> VarIdent
varIdent VarIdent
x)
    patternVar Pattern
_                       = forall a. Maybe a
Nothing

fromTerm' :: Term' -> Rzk.Term
fromTerm' :: Term' -> Term
fromTerm' Term'
t = [VarIdent] -> [VarIdent] -> Term' -> Term
fromTermWith' [VarIdent]
vars ([VarIdent]
defaultVarIdents forall a. Eq a => [a] -> [a] -> [a]
\\ [VarIdent]
vars) Term'
t
  where vars :: [VarIdent]
vars = forall a. Term a -> [a]
freeVars Term'
t

fromScope' :: VarIdent -> [VarIdent] -> [VarIdent] -> Scope Term VarIdent -> Rzk.Term
fromScope' :: VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs = [VarIdent] -> [VarIdent] -> Term' -> Term
fromTermWith' (VarIdent
x forall a. a -> [a] -> [a]
: [VarIdent]
used) [VarIdent]
xs forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {t :: * -> * -> *}. Inc VarIdent -> FS t VarIdent
f)
  where
    f :: Inc VarIdent -> FS t VarIdent
f Inc VarIdent
Z     = forall (t :: * -> * -> *) a. a -> FS t a
Pure VarIdent
x
    f (S VarIdent
z) = forall (t :: * -> * -> *) a. a -> FS t a
Pure VarIdent
z

fromTermWith' :: [VarIdent] -> [VarIdent] -> Term' -> Rzk.Term
fromTermWith' :: [VarIdent] -> [VarIdent] -> Term' -> Term
fromTermWith' [VarIdent]
used [VarIdent]
vars = Term' -> Term
go
  where
    withFresh :: Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
Nothing (VarIdent, [VarIdent]) -> t
f =
      case [VarIdent]
vars of
        VarIdent
x:[VarIdent]
xs -> (VarIdent, [VarIdent]) -> t
f (VarIdent
x, [VarIdent]
xs)
        [VarIdent]
_    -> forall a. HasCallStack => [Char] -> a
error [Char]
"not enough fresh variables!"
    withFresh (Just VarIdent
z) (VarIdent, [VarIdent]) -> t
f = (VarIdent, [VarIdent]) -> t
f (VarIdent
z', forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= VarIdent
z') [VarIdent]
vars)    -- FIXME: very inefficient filter
      where
        z' :: VarIdent
z' = [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
used VarIdent
z

    loc :: Maybe a
loc = forall a. Maybe a
Nothing

    go :: Term' -> Rzk.Term
    go :: Term' -> Term
go = \case
      Pure VarIdent
z -> forall a. a -> VarIdent' a -> Term' a
Rzk.Var forall a. Maybe a
loc (VarIdent -> VarIdent
fromVarIdent VarIdent
z)

      Term'
Universe -> forall a. a -> Term' a
Rzk.Universe forall a. Maybe a
loc
      Term'
UniverseCube -> forall a. a -> Term' a
Rzk.UniverseCube forall a. Maybe a
loc
      Term'
UniverseTope -> forall a. a -> Term' a
Rzk.UniverseTope forall a. Maybe a
loc
      Term'
CubeUnit -> forall a. a -> Term' a
Rzk.CubeUnit forall a. Maybe a
loc
      Term'
CubeUnitStar -> forall a. a -> Term' a
Rzk.CubeUnitStar forall a. Maybe a
loc
      Term'
Cube2 -> forall a. a -> Term' a
Rzk.Cube2 forall a. Maybe a
loc
      Term'
Cube2_0 -> forall a. a -> Term' a
Rzk.Cube2_0 forall a. Maybe a
loc
      Term'
Cube2_1 -> forall a. a -> Term' a
Rzk.Cube2_1 forall a. Maybe a
loc
      CubeProduct Term'
l Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.CubeProduct forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      Term'
TopeTop -> forall a. a -> Term' a
Rzk.TopeTop forall a. Maybe a
loc
      Term'
TopeBottom -> forall a. a -> Term' a
Rzk.TopeBottom forall a. Maybe a
loc
      TopeEQ Term'
l Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeEQ forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      TopeLEQ Term'
l Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeLEQ forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      TopeAnd Term'
l Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeAnd forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      TopeOr Term'
l Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeOr forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      Term'
RecBottom -> forall a. a -> Term' a
Rzk.RecBottom forall a. Maybe a
loc
      RecOr [(Term', Term')]
rs -> forall a. a -> [Restriction' a] -> Term' a
Rzk.RecOr forall a. Maybe a
loc [ forall a. a -> Term' a -> Term' a -> Restriction' a
Rzk.Restriction forall a. Maybe a
loc (Term' -> Term
go Term'
tope) (Term' -> Term
go Term'
term) | (Term'
tope, Term'
term) <- [(Term', Term')]
rs ]

      TypeFun Maybe VarIdent
z Term'
arg Maybe (Scope (FS TermF) VarIdent)
Nothing Scope (FS TermF) VarIdent
ret -> forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun forall a. Maybe a
loc (forall a. a -> Pattern' a -> Term' a -> ParamDecl' a
Rzk.ParamVarType forall a. Maybe a
loc (forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar forall a. Maybe a
loc (VarIdent -> VarIdent
fromVarIdent VarIdent
x)) (Term' -> Term
go Term'
arg)) (VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
ret)
      TypeFun Maybe VarIdent
z Term'
arg (Just Scope (FS TermF) VarIdent
tope) Scope (FS TermF) VarIdent
ret -> forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun forall a. Maybe a
loc (forall a. a -> Pattern' a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamVarShape forall a. Maybe a
loc (forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar forall a. Maybe a
loc (VarIdent -> VarIdent
fromVarIdent VarIdent
x)) (Term' -> Term
go Term'
arg) (VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
tope)) (VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
ret)

      TypeSigma Maybe VarIdent
z Term'
a Scope (FS TermF) VarIdent
b -> forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma forall a. Maybe a
loc (forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar forall a. Maybe a
loc (VarIdent -> VarIdent
fromVarIdent VarIdent
x)) (Term' -> Term
go Term'
a) (VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
b)
      TypeId Term'
l (Just Term'
tA) Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a -> Term' a
Rzk.TypeId forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
tA) (Term' -> Term
go Term'
r)
      TypeId Term'
l Maybe Term'
Nothing Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeIdSimple forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      App Term'
l Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)

      Lambda Maybe VarIdent
z Maybe (Term', Maybe (Scope (FS TermF) VarIdent))
Nothing Scope (FS TermF) VarIdent
scope -> forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda forall a. Maybe a
loc [forall a. a -> Pattern' a -> Param' a
Rzk.ParamPattern forall a. Maybe a
loc (forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar forall a. Maybe a
loc (VarIdent -> VarIdent
fromVarIdent VarIdent
x))] (VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      Lambda Maybe VarIdent
z (Just (Term'
ty, Maybe (Scope (FS TermF) VarIdent)
Nothing)) Scope (FS TermF) VarIdent
scope -> forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda forall a. Maybe a
loc [forall a. a -> [Pattern' a] -> Term' a -> Param' a
Rzk.ParamPatternType forall a. Maybe a
loc [forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar forall a. Maybe a
loc (VarIdent -> VarIdent
fromVarIdent VarIdent
x)] (Term' -> Term
go Term'
ty)] (VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      Lambda Maybe VarIdent
z (Just (Term'
cube, Just Scope (FS TermF) VarIdent
tope)) Scope (FS TermF) VarIdent
scope -> forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda forall a. Maybe a
loc [forall a. a -> Pattern' a -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternShape forall a. Maybe a
loc (forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar forall a. Maybe a
loc (VarIdent -> VarIdent
fromVarIdent VarIdent
x)) (Term' -> Term
go Term'
cube) (VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
tope)] (VarIdent
-> [VarIdent] -> [VarIdent] -> Scope (FS TermF) VarIdent -> Term
fromScope' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      -- Lambda (Maybe (term, Maybe scope)) scope -> Rzk.Lambda loc (Maybe (term, Maybe scope)) scope

      Pair Term'
l Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      First Term'
term -> forall a. a -> Term' a -> Term' a
Rzk.First forall a. Maybe a
loc (Term' -> Term
go Term'
term)
      Second Term'
term -> forall a. a -> Term' a -> Term' a
Rzk.Second forall a. Maybe a
loc (Term' -> Term
go Term'
term)
      Term'
TypeUnit -> forall a. a -> Term' a
Rzk.TypeUnit forall a. Maybe a
loc
      Term'
Unit -> forall a. a -> Term' a
Rzk.Unit forall a. Maybe a
loc
      Refl Maybe (Term', Maybe Term')
Nothing -> forall a. a -> Term' a
Rzk.Refl forall a. Maybe a
loc
      Refl (Just (Term'
t, Maybe Term'
Nothing)) -> forall a. a -> Term' a -> Term' a
Rzk.ReflTerm forall a. Maybe a
loc (Term' -> Term
go Term'
t)
      Refl (Just (Term'
t, Just Term'
ty)) -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.ReflTermType forall a. Maybe a
loc (Term' -> Term
go Term'
t) (Term' -> Term
go Term'
ty)
      IdJ Term'
a Term'
b Term'
c Term'
d Term'
e Term'
f -> forall a.
a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
Rzk.IdJ forall a. Maybe a
loc (Term' -> Term
go Term'
a) (Term' -> Term
go Term'
b) (Term' -> Term
go Term'
c) (Term' -> Term
go Term'
d) (Term' -> Term
go Term'
e) (Term' -> Term
go Term'
f)
      TypeAsc Term'
l Term'
r -> forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeAsc forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      TypeRestricted Term'
ty [(Term', Term')]
rs ->
        forall a. a -> Term' a -> [Restriction' a] -> Term' a
Rzk.TypeRestricted forall a. Maybe a
loc (Term' -> Term
go Term'
ty) (forall a b. (a -> b) -> [a] -> [b]
map (\(Term'
tope, Term'
term) -> (forall a. a -> Term' a -> Term' a -> Restriction' a
Rzk.Restriction forall a. Maybe a
loc (Term' -> Term
go Term'
tope) (Term' -> Term
go Term'
term))) [(Term', Term')]
rs)

defaultVarIdents :: [VarIdent]
defaultVarIdents :: [VarIdent]
defaultVarIdents =
  [ forall a. IsString a => [Char] -> a
fromString [Char]
name
  | Integer
n <- [Integer
1..]
  , let name :: [Char]
name = [Char]
"x" forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
digitToSub (forall a. Show a => a -> [Char]
show Integer
n) ]
  where
    digitToSub :: Char -> Char
digitToSub Char
c = Int -> Char
chr ((Char -> Int
ord Char
c forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') forall a. Num a => a -> a -> a
+ Char -> Int
ord Char
'₀')

-- | Given a list of used variable names in the current context,
-- generate a unique fresh name based on a given one.
--
-- >>> refreshVar ["x", "y", "x₁", "z"] "x"
-- x₂
refreshVar :: [VarIdent] -> VarIdent -> VarIdent
refreshVar :: [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
vars VarIdent
x
  | VarIdent
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VarIdent]
vars = [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
vars (VarIdent -> VarIdent
incVarIdentIndex VarIdent
x)
  | Bool
otherwise     = VarIdent
x

incVarIdentIndex :: VarIdent -> VarIdent
incVarIdentIndex :: VarIdent -> VarIdent
incVarIdentIndex (VarIdent (Rzk.VarIdent RzkPosition
loc VarIdentToken
token)) =
  VarIdent' RzkPosition -> VarIdent
VarIdent (forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent RzkPosition
loc (coerce :: forall a b. Coercible a b => a -> b
coerce [Char] -> [Char]
incIndex VarIdentToken
token))

-- | Increment the subscript number at the end of the indentifier.
--
-- >>> incIndex "x"
-- x₁
-- >>> incIndex "x₁₉"
-- x₂₀
incIndex :: String -> String
incIndex :: [Char] -> [Char]
incIndex [Char]
s = [Char]
name forall a. Semigroup a => a -> a -> a
<> [Char]
newIndex
  where
    digitsSub :: [Char]
digitsSub = [Char]
"₀₁₂₃₄₅₆₇₈₉" :: String
    isDigitSub :: Char -> Bool
isDigitSub = (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char]
digitsSub)
    digitFromSub :: Char -> Char
digitFromSub Char
c = Int -> Char
chr ((Char -> Int
ord Char
c forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'₀') forall a. Num a => a -> a -> a
+ Char -> Int
ord Char
'0')
    digitToSub :: Char -> Char
digitToSub Char
c = Int -> Char
chr ((Char -> Int
ord Char
c forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') forall a. Num a => a -> a -> a
+ Char -> Int
ord Char
'₀')
    ([Char]
name, [Char]
index) = forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isDigitSub [Char]
s
    oldIndexN :: Integer
oldIndexN = forall a. Read a => [Char] -> a
read (Char
'0' forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
digitFromSub [Char]
index) -- FIXME: read
    newIndex :: [Char]
newIndex = forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
digitToSub (forall a. Show a => a -> [Char]
show (Integer
oldIndexN forall a. Num a => a -> a -> a
+ Integer
1))

instance Show Term' where
  show :: Term' -> [Char]
show = forall a. Print a => a -> [Char]
Rzk.printTree forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term' -> Term
fromTerm'

instance IsString Term' where
  fromString :: [Char] -> Term'
fromString = Term -> Term'
toTerm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Either [Char] a -> a
fromRight forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Either [Char] Term
Rzk.parseTerm
    where
      fromRight :: Either [Char] a -> a
fromRight (Left [Char]
err) = forall a. HasCallStack => [Char] -> a
error ([Char]
"Parse error: " forall a. Semigroup a => a -> a -> a
<> [Char]
err)
      fromRight (Right a
t)  = a
t

instance Show TermT' where
  show :: TermT' -> [Char]
show var :: TermT'
var@Pure{} = forall a. Print a => a -> [Char]
Rzk.printTree (Term' -> Term
fromTerm' (forall (ann :: * -> *) (term :: * -> * -> *) a.
(Functor ann, Bifunctor term) =>
FS (AnnF ann term) a -> FS term a
untyped TermT'
var))
  show term :: TermT'
term@(Free (AnnF TypeInfo{Maybe TermT'
TermT'
infoNF :: Maybe TermT'
infoWHNF :: Maybe TermT'
infoType :: TermT'
infoNF :: forall term. TypeInfo term -> Maybe term
infoWHNF :: forall term. TypeInfo term -> Maybe term
infoType :: forall term. TypeInfo term -> term
..} TermF (Scope (FS (AnnF TypeInfo TermF)) VarIdent) TermT'
_)) = [Char]
termStr forall a. Semigroup a => a -> a -> a
<> [Char]
" : " forall a. Semigroup a => a -> a -> a
<> [Char]
typeStr
    where
      termStr :: [Char]
termStr = forall a. Print a => a -> [Char]
Rzk.printTree (Term' -> Term
fromTerm' (forall (ann :: * -> *) (term :: * -> * -> *) a.
(Functor ann, Bifunctor term) =>
FS (AnnF ann term) a -> FS term a
untyped TermT'
term))
      typeStr :: [Char]
typeStr = forall a. Print a => a -> [Char]
Rzk.printTree (Term' -> Term
fromTerm' (forall (ann :: * -> *) (term :: * -> * -> *) a.
(Functor ann, Bifunctor term) =>
FS (AnnF ann term) a -> FS term a
untyped TermT'
infoType))