{-# 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

-- FIXME: use proper mechanisms for warnings
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
rzkFilePath :: RzkPosition -> Maybe [Char]
rzkLineCol :: RzkPosition -> BNFC'Position
rzkFilePath :: Maybe [Char]
rzkLineCol :: BNFC'Position
..} = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
":" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[[Char]]] -> [[Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [[Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
"<stdin>" Maybe [Char]
rzkFilePath]
  , ((Int, Int) -> [[Char]]) -> BNFC'Position -> [[Char]]
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Int
row, Int
col) -> (Int -> [Char]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Int -> [Char]
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 Show VarIdent where
  show :: VarIdent -> [Char]
show = VarIdent' RzkPosition -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree (VarIdent' RzkPosition -> [Char])
-> (VarIdent -> VarIdent' RzkPosition) -> VarIdent -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarIdent -> VarIdent' RzkPosition
getVarIdent

instance Eq VarIdent where
  == :: VarIdent -> VarIdent -> Bool
(==) = VarIdent' () -> VarIdent' () -> Bool
forall a. Eq a => a -> a -> Bool
(==) (VarIdent' () -> VarIdent' () -> Bool)
-> (VarIdent -> VarIdent' ()) -> VarIdent -> VarIdent -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (VarIdent' RzkPosition -> VarIdent' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (VarIdent' RzkPosition -> VarIdent' ())
-> (VarIdent -> VarIdent' RzkPosition) -> VarIdent -> VarIdent' ()
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 (RzkPosition -> VarIdentToken -> VarIdent' RzkPosition
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent (Maybe [Char] -> BNFC'Position -> RzkPosition
RzkPosition Maybe [Char]
forall a. Maybe a
Nothing BNFC'Position
forall a. Maybe a
Nothing) ([Char] -> VarIdentToken
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)) =
  VarIdent' RzkPosition -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree VarIdent' RzkPosition
var [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" (" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> RzkPosition -> [Char]
ppRzkPosition RzkPosition
pos [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
")"

varIdent :: Rzk.VarIdent -> VarIdent
varIdent :: VarIdent -> VarIdent
varIdent = Maybe [Char] -> VarIdent -> VarIdent
varIdentAt Maybe [Char]
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 (RzkPosition -> VarIdentToken -> VarIdent' RzkPosition
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)) = BNFC'Position -> VarIdentToken -> VarIdent
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
(TermF scope term -> TermF scope term -> Bool)
-> (TermF scope term -> TermF scope term -> Bool)
-> Eq (TermF scope term)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall scope term.
(Eq scope, Eq term) =>
TermF scope term -> TermF scope term -> Bool
$c== :: forall scope term.
(Eq scope, Eq term) =>
TermF scope term -> TermF scope term -> Bool
== :: TermF scope term -> TermF scope term -> Bool
$c/= :: forall scope term.
(Eq scope, Eq term) =>
TermF scope term -> TermF scope term -> Bool
/= :: TermF scope term -> TermF scope term -> Bool
Eq, (forall a b. (a -> b) -> TermF scope a -> TermF scope b)
-> (forall a b. a -> TermF scope b -> TermF scope a)
-> Functor (TermF scope)
forall a b. a -> TermF scope b -> TermF scope a
forall a b. (a -> b) -> TermF scope a -> TermF scope b
forall scope a b. a -> TermF scope b -> TermF scope a
forall scope a b. (a -> b) -> TermF scope a -> TermF scope b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall scope a b. (a -> b) -> TermF scope a -> TermF scope b
fmap :: forall a b. (a -> b) -> TermF scope a -> TermF scope b
$c<$ :: forall scope a b. a -> TermF scope b -> TermF scope a
<$ :: forall a b. a -> TermF scope b -> TermF scope a
Functor, (forall m. Monoid m => TermF scope m -> m)
-> (forall m a. Monoid m => (a -> m) -> TermF scope a -> m)
-> (forall m a. Monoid m => (a -> m) -> TermF scope a -> m)
-> (forall a b. (a -> b -> b) -> b -> TermF scope a -> b)
-> (forall a b. (a -> b -> b) -> b -> TermF scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> TermF scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> TermF scope a -> b)
-> (forall a. (a -> a -> a) -> TermF scope a -> a)
-> (forall a. (a -> a -> a) -> TermF scope a -> a)
-> (forall a. TermF scope a -> [a])
-> (forall a. TermF scope a -> Bool)
-> (forall a. TermF scope a -> Int)
-> (forall a. Eq a => a -> TermF scope a -> Bool)
-> (forall a. Ord a => TermF scope a -> a)
-> (forall a. Ord a => TermF scope a -> a)
-> (forall a. Num a => TermF scope a -> a)
-> (forall a. Num a => TermF scope a -> a)
-> Foldable (TermF scope)
forall a. Eq a => a -> TermF scope a -> Bool
forall a. Num a => TermF scope a -> a
forall a. Ord a => TermF scope a -> a
forall m. Monoid m => TermF scope m -> m
forall a. TermF scope a -> Bool
forall a. TermF scope a -> Int
forall a. TermF scope a -> [a]
forall a. (a -> a -> a) -> TermF scope a -> a
forall scope a. Eq a => a -> TermF scope a -> Bool
forall scope a. Num a => TermF scope a -> a
forall scope a. Ord a => TermF scope a -> a
forall m a. Monoid m => (a -> m) -> TermF scope a -> m
forall scope m. Monoid m => TermF scope m -> m
forall scope a. TermF scope a -> Bool
forall scope a. TermF scope a -> Int
forall scope a. TermF scope a -> [a]
forall b a. (b -> a -> b) -> b -> TermF scope a -> b
forall a b. (a -> b -> b) -> b -> TermF scope a -> b
forall scope a. (a -> a -> a) -> TermF scope a -> a
forall scope m a. Monoid m => (a -> m) -> TermF scope a -> m
forall scope b a. (b -> a -> b) -> b -> TermF scope a -> b
forall scope a b. (a -> b -> b) -> b -> TermF scope 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
$cfold :: forall scope m. Monoid m => TermF scope m -> m
fold :: forall m. Monoid m => TermF scope m -> m
$cfoldMap :: forall scope m a. Monoid m => (a -> m) -> TermF scope a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TermF scope a -> m
$cfoldMap' :: forall scope m a. Monoid m => (a -> m) -> TermF scope a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TermF scope a -> m
$cfoldr :: forall scope a b. (a -> b -> b) -> b -> TermF scope a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TermF scope a -> b
$cfoldr' :: forall scope a b. (a -> b -> b) -> b -> TermF scope a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TermF scope a -> b
$cfoldl :: forall scope b a. (b -> a -> b) -> b -> TermF scope a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TermF scope a -> b
$cfoldl' :: forall scope b a. (b -> a -> b) -> b -> TermF scope a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TermF scope a -> b
$cfoldr1 :: forall scope a. (a -> a -> a) -> TermF scope a -> a
foldr1 :: forall a. (a -> a -> a) -> TermF scope a -> a
$cfoldl1 :: forall scope a. (a -> a -> a) -> TermF scope a -> a
foldl1 :: forall a. (a -> a -> a) -> TermF scope a -> a
$ctoList :: forall scope a. TermF scope a -> [a]
toList :: forall a. TermF scope a -> [a]
$cnull :: forall scope a. TermF scope a -> Bool
null :: forall a. TermF scope a -> Bool
$clength :: forall scope a. TermF scope a -> Int
length :: forall a. TermF scope a -> Int
$celem :: forall scope a. Eq a => a -> TermF scope a -> Bool
elem :: forall a. Eq a => a -> TermF scope a -> Bool
$cmaximum :: forall scope a. Ord a => TermF scope a -> a
maximum :: forall a. Ord a => TermF scope a -> a
$cminimum :: forall scope a. Ord a => TermF scope a -> a
minimum :: forall a. Ord a => TermF scope a -> a
$csum :: forall scope a. Num a => TermF scope a -> a
sum :: forall a. Num a => TermF scope a -> a
$cproduct :: forall scope a. Num a => TermF scope a -> a
product :: forall a. Num a => TermF scope a -> a
Foldable, Functor (TermF scope)
Foldable (TermF scope)
(Functor (TermF scope), Foldable (TermF scope)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TermF scope a -> f (TermF scope b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TermF scope (f a) -> f (TermF scope a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TermF scope a -> m (TermF scope b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TermF scope (m a) -> m (TermF scope a))
-> Traversable (TermF scope)
forall scope. Functor (TermF scope)
forall scope. Foldable (TermF scope)
forall scope (m :: * -> *) a.
Monad m =>
TermF scope (m a) -> m (TermF scope a)
forall scope (f :: * -> *) a.
Applicative f =>
TermF scope (f a) -> f (TermF scope a)
forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermF scope a -> m (TermF scope b)
forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermF scope a -> f (TermF scope b)
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 =>
TermF scope (m a) -> m (TermF scope a)
forall (f :: * -> *) a.
Applicative f =>
TermF scope (f a) -> f (TermF scope a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermF scope a -> m (TermF scope b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermF scope a -> f (TermF scope b)
$ctraverse :: forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermF scope a -> f (TermF scope b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermF scope a -> f (TermF scope b)
$csequenceA :: forall scope (f :: * -> *) a.
Applicative f =>
TermF scope (f a) -> f (TermF scope a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TermF scope (f a) -> f (TermF scope a)
$cmapM :: forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermF scope a -> m (TermF scope b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermF scope a -> m (TermF scope b)
$csequence :: forall scope (m :: * -> *) a.
Monad m =>
TermF scope (m a) -> m (TermF scope a)
sequence :: forall (m :: * -> *) a.
Monad m =>
TermF scope (m a) -> m (TermF scope a)
Traversable)
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
(Type term -> Type term -> Bool)
-> (Type term -> Type term -> Bool) -> Eq (Type term)
forall term. Eq term => Type term -> Type term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Type term -> Type term -> Bool
Eq, (forall a b. (a -> b) -> Type a -> Type b)
-> (forall a b. a -> Type b -> Type a) -> Functor Type
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
$cfmap :: forall a b. (a -> b) -> Type a -> Type b
fmap :: forall a b. (a -> b) -> Type a -> Type b
$c<$ :: forall a b. a -> Type b -> Type a
<$ :: forall a b. a -> Type b -> Type a
Functor, (forall m. Monoid m => Type m -> m)
-> (forall m a. Monoid m => (a -> m) -> Type a -> m)
-> (forall m a. Monoid m => (a -> m) -> Type a -> m)
-> (forall a b. (a -> b -> b) -> b -> Type a -> b)
-> (forall a b. (a -> b -> b) -> b -> Type a -> b)
-> (forall b a. (b -> a -> b) -> b -> Type a -> b)
-> (forall b a. (b -> a -> b) -> b -> Type a -> b)
-> (forall a. (a -> a -> a) -> Type a -> a)
-> (forall a. (a -> a -> a) -> Type a -> a)
-> (forall a. Type a -> [a])
-> (forall a. Type a -> Bool)
-> (forall a. Type a -> Int)
-> (forall a. Eq a => a -> Type a -> Bool)
-> (forall a. Ord a => Type a -> a)
-> (forall a. Ord a => Type a -> a)
-> (forall a. Num a => Type a -> a)
-> (forall a. Num a => Type a -> a)
-> Foldable Type
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
$cfold :: forall m. Monoid m => Type m -> m
fold :: forall m. Monoid m => Type m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Type a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Type a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Type a -> a
foldr1 :: forall a. (a -> a -> a) -> Type a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Type a -> a
foldl1 :: forall a. (a -> a -> a) -> Type a -> a
$ctoList :: forall a. Type a -> [a]
toList :: forall a. Type a -> [a]
$cnull :: forall a. Type a -> Bool
null :: forall a. Type a -> Bool
$clength :: forall a. Type a -> Int
length :: forall a. Type a -> Int
$celem :: forall a. Eq a => a -> Type a -> Bool
elem :: forall a. Eq a => a -> Type a -> Bool
$cmaximum :: forall a. Ord a => Type a -> a
maximum :: forall a. Ord a => Type a -> a
$cminimum :: forall a. Ord a => Type a -> a
minimum :: forall a. Ord a => Type a -> a
$csum :: forall a. Num a => Type a -> a
sum :: forall a. Num a => Type a -> a
$cproduct :: forall a. Num a => Type a -> a
product :: forall a. Num a => Type a -> a
Foldable, Functor Type
Foldable Type
(Functor Type, Foldable Type) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Type a -> f (Type b))
-> (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 (m :: * -> *) a. Monad m => Type (m a) -> m (Type a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
$csequence :: forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a)
sequence :: forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a)
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
(TypeInfo term -> TypeInfo term -> Bool)
-> (TypeInfo term -> TypeInfo term -> Bool) -> Eq (TypeInfo term)
forall term. Eq term => TypeInfo term -> TypeInfo term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: TypeInfo term -> TypeInfo term -> Bool
Eq, (forall a b. (a -> b) -> TypeInfo a -> TypeInfo b)
-> (forall a b. a -> TypeInfo b -> TypeInfo a) -> Functor TypeInfo
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
$cfmap :: forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
fmap :: forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
$c<$ :: forall a b. a -> TypeInfo b -> TypeInfo a
<$ :: forall a b. a -> TypeInfo b -> TypeInfo a
Functor, (forall m. Monoid m => TypeInfo m -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeInfo a -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeInfo a -> m)
-> (forall a b. (a -> b -> b) -> b -> TypeInfo a -> b)
-> (forall a b. (a -> b -> b) -> b -> TypeInfo a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeInfo a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeInfo a -> b)
-> (forall a. (a -> a -> a) -> TypeInfo a -> a)
-> (forall a. (a -> a -> a) -> TypeInfo a -> a)
-> (forall a. TypeInfo a -> [a])
-> (forall a. TypeInfo a -> Bool)
-> (forall a. TypeInfo a -> Int)
-> (forall a. Eq a => a -> TypeInfo a -> Bool)
-> (forall a. Ord a => TypeInfo a -> a)
-> (forall a. Ord a => TypeInfo a -> a)
-> (forall a. Num a => TypeInfo a -> a)
-> (forall a. Num a => TypeInfo a -> a)
-> Foldable TypeInfo
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
$cfold :: forall m. Monoid m => TypeInfo m -> m
fold :: forall m. Monoid m => TypeInfo m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
foldl1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
$ctoList :: forall a. TypeInfo a -> [a]
toList :: forall a. TypeInfo a -> [a]
$cnull :: forall a. TypeInfo a -> Bool
null :: forall a. TypeInfo a -> Bool
$clength :: forall a. TypeInfo a -> Int
length :: forall a. TypeInfo a -> Int
$celem :: forall a. Eq a => a -> TypeInfo a -> Bool
elem :: forall a. Eq a => a -> TypeInfo a -> Bool
$cmaximum :: forall a. Ord a => TypeInfo a -> a
maximum :: forall a. Ord a => TypeInfo a -> a
$cminimum :: forall a. Ord a => TypeInfo a -> a
minimum :: forall a. Ord a => TypeInfo a -> a
$csum :: forall a. Num a => TypeInfo a -> a
sum :: forall a. Num a => TypeInfo a -> a
$cproduct :: forall a. Num a => TypeInfo a -> a
product :: forall a. Num a => TypeInfo a -> a
Foldable, Functor TypeInfo
Foldable TypeInfo
(Functor TypeInfo, Foldable TypeInfo) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TypeInfo a -> f (TypeInfo b))
-> (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 (m :: * -> *) a.
    Monad m =>
    TypeInfo (m a) -> m (TypeInfo a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeInfo a -> f (TypeInfo b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeInfo a -> f (TypeInfo b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeInfo (f a) -> f (TypeInfo a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeInfo (f a) -> f (TypeInfo a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeInfo a -> m (TypeInfo b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeInfo a -> m (TypeInfo b)
$csequence :: forall (m :: * -> *) a. Monad m => TypeInfo (m a) -> m (TypeInfo a)
sequence :: forall (m :: * -> *) a. Monad m => TypeInfo (m a) -> m (TypeInfo a)
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' = AnnF
  TypeInfo TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
-> TermT var
forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free (TypeInfo (TermT var)
-> TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
-> AnnF
     TypeInfo TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF TypeInfo (TermT var)
info { infoWHNF = Just 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' = AnnF
  TypeInfo TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
-> TermT var
forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free (TypeInfo (TermT var)
-> TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
-> AnnF
     TypeInfo TermF (Scope (FS (AnnF TypeInfo TermF)) var) (TermT var)
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF TypeInfo (TermT var)
info { infoWHNF = Just t', infoNF = Just 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 s t. AnnF TypeInfo TermF s t -> AnnF TypeInfo TermF s t)
-> FS (AnnF TypeInfo TermF) var -> FS (AnnF TypeInfo TermF) var
forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS ((forall s t. AnnF TypeInfo TermF s t -> AnnF TypeInfo TermF s t)
 -> FS (AnnF TypeInfo TermF) var -> FS (AnnF TypeInfo TermF) var)
-> (forall s t. AnnF TypeInfo TermF s t -> AnnF TypeInfo TermF s t)
-> FS (AnnF TypeInfo TermF) var
-> FS (AnnF TypeInfo TermF) var
forall a b. (a -> b) -> a -> b
$ \(AnnF TypeInfo t
info TermF s t
f) ->
  TypeInfo t -> TermF s t -> AnnF TypeInfo TermF s t
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF TypeInfo t
info { infoWHNF = Nothing, infoNF = 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 = TermT var -> Scope (FS (AnnF TypeInfo TermF)) var -> TermT var
forall (t :: * -> * -> *) a.
Bifunctor t =>
FS t a -> Scope (FS t) a -> FS t a
substitute TermT var
x (Scope (FS (AnnF TypeInfo TermF)) var -> TermT var)
-> (Scope (FS (AnnF TypeInfo TermF)) var
    -> Scope (FS (AnnF TypeInfo TermF)) var)
-> Scope (FS (AnnF TypeInfo TermF)) var
-> TermT var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope (FS (AnnF TypeInfo TermF)) var
-> Scope (FS (AnnF TypeInfo TermF)) var
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 = (a -> [a]) -> FS TermF a -> [a]
forall m a. Monoid m => (a -> m) -> FS TermF a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> [a]
forall a. a -> [a]
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?)
  (FS (AnnF TypeInfo TermF) a -> [a])
-> [FS (AnnF TypeInfo TermF) a] -> [a]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Term a -> [a]
forall a. Term a -> [a]
freeVars (Term a -> [a])
-> (FS (AnnF TypeInfo TermF) a -> Term a)
-> FS (AnnF TypeInfo TermF) a
-> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FS (AnnF TypeInfo TermF) a -> Term a
forall (ann :: * -> *) (term :: * -> * -> *) a.
(Functor ann, Bifunctor term) =>
FS (AnnF ann term) a -> FS term a
untyped) [FS (AnnF TypeInfo TermF) a
term, TypeInfo (FS (AnnF TypeInfo TermF) a) -> FS (AnnF TypeInfo TermF) a
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 [] (TermT a -> [a]
forall a. TermT a -> [a]
partialFreeVarsT TermT a
t)
  where
    go :: [a] -> [a] -> [a]
go [a]
vars [a]
latest
      | [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
new = [a]
vars
      | Bool
otherwise =
          [a] -> [a] -> [a]
go ([a]
new [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
vars)
             ((a -> [a]) -> [a] -> [a]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TermT a -> [a]
forall a. TermT a -> [a]
partialFreeVarsT (TermT a -> [a]) -> (a -> TermT a) -> a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> TermT a
typeOfVar) [a]
new)
      where
        new :: [a]
new = [a] -> [a]
forall a. Eq a => [a] -> [a]
nub [a]
latest [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
vars

toTerm' :: Rzk.Term -> Term'
toTerm' :: Term -> Term'
toTerm' = (VarIdent -> Term') -> Term -> Term'
forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm VarIdent -> Term'
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 = (VarIdent -> Term (Inc a)) -> Term -> Term (Inc a)
forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm ((VarIdent -> Term (Inc a)) -> Term -> Term (Inc a))
-> (VarIdent -> Term (Inc a)) -> Term -> Term (Inc a)
forall a b. (a -> b) -> a -> b
$ \VarIdent
z -> if VarIdent
x VarIdent -> VarIdent -> Bool
forall a. Eq a => a -> a -> Bool
== VarIdent
z then Inc a -> Term (Inc a)
forall (t :: * -> * -> *) a. a -> FS t a
Pure Inc a
forall var. Inc var
Z else a -> Inc a
forall var. var -> Inc var
S (a -> Inc a) -> Term a -> Term (Inc a)
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 = (VarIdent -> Term (Inc a)) -> Term -> Term (Inc a)
forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm ((VarIdent -> Term (Inc a)) -> Term -> Term (Inc a))
-> (VarIdent -> Term (Inc a)) -> Term -> Term (Inc a)
forall a b. (a -> b) -> a -> b
$ \VarIdent
z ->
  case VarIdent -> [(VarIdent, Term (Inc a))] -> Maybe (Term (Inc a))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VarIdent
z (Pattern -> Term (Inc a) -> [(VarIdent, Term (Inc a))]
forall {a}. Pattern -> FS TermF a -> [(VarIdent, FS TermF a)]
bindings Pattern
pat (Inc a -> Term (Inc a)
forall (t :: * -> * -> *) a. a -> FS t a
Pure Inc a
forall var. Inc var
Z)) of
    Just Term (Inc a)
t  -> Term (Inc a)
t
    Maybe (Term (Inc a))
Nothing -> a -> Inc a
forall var. var -> Inc var
S (a -> Inc a) -> Term a -> Term (Inc a)
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.PatternUnit BNFC'Position
_loc)     FS TermF a
_ = []
    bindings (Rzk.PatternVar BNFC'Position
_loc (Rzk.VarIdent BNFC'Position
_ VarIdentToken
"_")) 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 (FS TermF a -> FS TermF a
forall {a}. FS TermF a -> FS TermF a
First FS TermF a
t) [(VarIdent, FS TermF a)]
-> [(VarIdent, FS TermF a)] -> [(VarIdent, FS TermF a)]
forall a. Semigroup a => a -> a -> a
<> Pattern -> FS TermF a -> [(VarIdent, FS TermF a)]
bindings Pattern
r (FS TermF a -> FS TermF a
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
    deprecated :: Term -> Term -> Term a
deprecated Term
t Term
t' = [Char] -> Term a -> Term a
forall a. [Char] -> a -> a
trace [Char]
msg (Term -> Term a
go Term
t')
      where
        msg :: [Char]
msg = [[Char]] -> [Char]
unlines
          [ [Char]
"[DEPRECATED]:" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> BNFC'Position -> [Char]
forall {a} {a}. (Show a, Show a) => Maybe (a, a) -> [Char]
ppBNFC'Position (Term -> BNFC'Position
forall a. HasPosition a => a -> BNFC'Position
Rzk.hasPosition Term
t)
          , [Char]
"the following notation is deprecated and will be removed from future version of rzk:"
          , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term
t
          , [Char]
"instead consider using the following notation:"
          , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term
t'
          ]

    ppBNFC'Position :: Maybe (a, a) -> [Char]
ppBNFC'Position Maybe (a, a)
Nothing = [Char]
""
    ppBNFC'Position (Just (a
line_, a
col)) = [Char]
" at line " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show a
line_ [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" column " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show a
col

    lint :: a -> a -> a -> a
lint a
orig a
suggestion = [Char] -> a -> a
forall a. [Char] -> a -> a
trace ([Char] -> a -> a) -> [Char] -> a -> a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
      [ [Char]
"[HINT]:" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> BNFC'Position -> [Char]
forall {a} {a}. (Show a, Show a) => Maybe (a, a) -> [Char]
ppBNFC'Position (a -> BNFC'Position
forall a. HasPosition a => a -> BNFC'Position
Rzk.hasPosition a
orig) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" consider replacing"
      , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree a
orig
      , [Char]
"with the following"
      , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree a
suggestion
      ]

    go :: Term -> Term a
go = \case
      -- Depracations
      t :: Term
t@(Rzk.RecOrDeprecated BNFC'Position
loc Term
psi Term
phi Term
a_psi Term
a_phi) -> Term -> Term -> Term a
deprecated Term
t
        (BNFC'Position -> [Restriction' BNFC'Position] -> Term
forall a. a -> [Restriction' a] -> Term' a
Rzk.RecOr BNFC'Position
loc [BNFC'Position -> Term -> Term -> Restriction' BNFC'Position
forall a. a -> Term' a -> Term' a -> Restriction' a
Rzk.Restriction BNFC'Position
loc Term
psi Term
a_psi, BNFC'Position -> Term -> Term -> Restriction' BNFC'Position
forall a. a -> Term' a -> Term' a -> Restriction' a
Rzk.Restriction BNFC'Position
loc Term
phi Term
a_phi])
      t :: Term
t@(Rzk.TypeExtensionDeprecated BNFC'Position
loc ParamDecl' BNFC'Position
shape Term
type_) -> Term -> Term -> Term a
deprecated Term
t
        (BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc ParamDecl' BNFC'Position
shape Term
type_)
      t :: Term
t@(Rzk.TypeFun BNFC'Position
loc (Rzk.ParamTermTypeDeprecated BNFC'Position
loc' Pattern
pat Term
type_) Term
ret) -> Term -> Term -> Term a
deprecated Term
t
        (BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc (BNFC'Position -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
loc' (Pattern -> Term
patternToTerm Pattern
pat) Term
type_) Term
ret)
      t :: Term
t@(Rzk.TypeFun BNFC'Position
loc (Rzk.ParamVarShapeDeprecated BNFC'Position
loc' Pattern
pat Term
cube Term
tope) Term
ret) -> Term -> Term -> Term a
deprecated Term
t
        (BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc (BNFC'Position -> Term -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermShape BNFC'Position
loc' (Pattern -> Term
patternToTerm Pattern
pat) Term
cube Term
tope) Term
ret)
      t :: Term
t@(Rzk.Lambda BNFC'Position
loc ((Rzk.ParamPatternShapeDeprecated BNFC'Position
loc' Pattern
pat Term
cube Term
tope):[Param' BNFC'Position]
params) Term
body) -> Term -> Term -> Term a
deprecated Term
t
        (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc ((BNFC'Position -> [Pattern] -> Term -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternShape BNFC'Position
loc' [Pattern
pat] Term
cube Term
tope)Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
:[Param' BNFC'Position]
params) Term
body)

      -- ASCII versions
      Rzk.ASCII_CubeUnitStar BNFC'Position
loc -> Term -> Term a
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeUnitStar BNFC'Position
loc)
      Rzk.ASCII_Cube2_0 BNFC'Position
loc -> Term -> Term a
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2_0 BNFC'Position
loc)
      Rzk.ASCII_Cube2_1 BNFC'Position
loc -> Term -> Term a
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2_1 BNFC'Position
loc)
      Rzk.ASCII_TopeTop BNFC'Position
loc -> Term -> Term a
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TopeTop BNFC'Position
loc)
      Rzk.ASCII_TopeBottom BNFC'Position
loc -> Term -> Term a
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TopeBottom BNFC'Position
loc)
      Rzk.ASCII_TopeEQ BNFC'Position
loc Term
l Term
r -> Term -> Term a
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeEQ BNFC'Position
loc Term
l Term
r)
      Rzk.ASCII_TopeLEQ BNFC'Position
loc Term
l Term
r -> Term -> Term a
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeLEQ BNFC'Position
loc Term
l Term
r)
      Rzk.ASCII_TopeAnd BNFC'Position
loc Term
l Term
r -> Term -> Term a
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeAnd BNFC'Position
loc Term
l Term
r)
      Rzk.ASCII_TopeOr BNFC'Position
loc Term
l Term
r -> Term -> Term a
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeOr BNFC'Position
loc Term
l Term
r)

      Rzk.ASCII_TypeFun BNFC'Position
loc ParamDecl' BNFC'Position
param Term
ret -> Term -> Term a
go (BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc ParamDecl' BNFC'Position
param Term
ret)
      Rzk.ASCII_TypeSigma BNFC'Position
loc Pattern
pat Term
ty Term
ret -> Term -> Term a
go (BNFC'Position -> Pattern -> Term -> Term -> Term
forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma BNFC'Position
loc Pattern
pat Term
ty Term
ret)
      Rzk.ASCII_Lambda BNFC'Position
loc [Param' BNFC'Position]
pat Term
ret -> Term -> Term a
go (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc [Param' BNFC'Position]
pat Term
ret)
      Rzk.ASCII_TypeExtensionDeprecated BNFC'Position
loc ParamDecl' BNFC'Position
shape Term
type_ -> Term -> Term a
go (BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeExtensionDeprecated BNFC'Position
loc ParamDecl' BNFC'Position
shape Term
type_)
      Rzk.ASCII_First BNFC'Position
loc Term
term -> Term -> Term a
go (BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.First BNFC'Position
loc Term
term)
      Rzk.ASCII_Second BNFC'Position
loc Term
term -> Term -> Term a
go (BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.Second BNFC'Position
loc Term
term)


      Rzk.Var BNFC'Position
_loc VarIdent
x -> VarIdent -> Term a
bvars (VarIdent -> VarIdent
varIdent VarIdent
x)
      Rzk.Universe BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
Universe

      Rzk.UniverseCube BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
UniverseCube
      Rzk.UniverseTope BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
UniverseTope
      Rzk.CubeUnit BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
CubeUnit
      Rzk.CubeUnitStar BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
CubeUnitStar
      Rzk.Cube2 BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
Cube2
      Rzk.Cube2_0 BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
Cube2_0
      Rzk.Cube2_1 BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
Cube2_1
      Rzk.CubeProduct BNFC'Position
_loc Term
l Term
r -> Term a -> Term a -> Term a
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 -> Term a
forall {a}. FS TermF a
TopeTop
      Rzk.TopeBottom BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
TopeBottom
      Rzk.TopeEQ BNFC'Position
_loc Term
l Term
r -> Term a -> Term a -> Term a
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 -> Term a -> Term a -> Term a
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 -> Term a -> Term a -> Term a
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 -> Term a -> Term a -> Term a
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 -> Term a
forall {a}. FS TermF a
RecBottom
      Rzk.RecOr BNFC'Position
_loc [Restriction' BNFC'Position]
rs -> [(Term a, Term a)] -> Term a
forall {a}. [(FS TermF a, FS TermF a)] -> FS TermF a
RecOr ([(Term a, Term a)] -> Term a) -> [(Term a, Term a)] -> Term a
forall a b. (a -> b) -> a -> b
$ ((Restriction' BNFC'Position -> (Term a, Term a))
 -> [Restriction' BNFC'Position] -> [(Term a, Term a)])
-> [Restriction' BNFC'Position]
-> (Restriction' BNFC'Position -> (Term a, Term a))
-> [(Term a, Term a)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Restriction' BNFC'Position -> (Term a, Term a))
-> [Restriction' BNFC'Position] -> [(Term a, Term a)]
forall a b. (a -> b) -> [a] -> [b]
map [Restriction' BNFC'Position]
rs ((Restriction' BNFC'Position -> (Term a, Term a))
 -> [(Term a, Term a)])
-> (Restriction' BNFC'Position -> (Term a, Term a))
-> [(Term a, Term a)]
forall a b. (a -> b) -> a -> b
$ \case
        Rzk.Restriction BNFC'Position
_loc Term
tope Term
term       -> (Term -> Term a
go Term
tope, Term -> Term a
go Term
term)
        Rzk.ASCII_Restriction BNFC'Position
_loc Term
tope Term
term -> (Term -> Term a
go Term
tope, Term -> Term a
go Term
term)
      Rzk.TypeId BNFC'Position
_loc Term
x Term
tA Term
y -> Term a -> Maybe (Term a) -> Term a -> Term a
forall {a}.
FS TermF a -> Maybe (FS TermF a) -> FS TermF a -> FS TermF a
TypeId (Term -> Term a
go Term
x) (Term a -> Maybe (Term a)
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 -> Term a -> Maybe (Term a) -> Term a -> Term a
forall {a}.
FS TermF a -> Maybe (FS TermF a) -> FS TermF a -> FS TermF a
TypeId (Term -> Term a
go Term
x) Maybe (Term a)
forall a. Maybe a
Nothing (Term -> Term a
go Term
y)
      Rzk.TypeUnit BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
TypeUnit
      Rzk.Unit BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
Unit
      Rzk.App BNFC'Position
_loc Term
f Term
x -> Term a -> Term a -> Term a
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 -> Term a -> Term a -> Term a
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 -> Term a -> Term a
forall {a}. FS TermF a -> FS TermF a
First (Term -> Term a
go Term
term)
      Rzk.Second BNFC'Position
_loc Term
term -> Term a -> Term a
forall {a}. FS TermF a -> FS TermF a
Second (Term -> Term a
go Term
term)
      Rzk.Refl BNFC'Position
_loc -> Maybe (Term a, Maybe (Term a)) -> Term a
forall {a}. Maybe (FS TermF a, Maybe (FS TermF a)) -> FS TermF a
Refl Maybe (Term a, Maybe (Term a))
forall a. Maybe a
Nothing
      Rzk.ReflTerm BNFC'Position
_loc Term
term -> Maybe (Term a, Maybe (Term a)) -> Term a
forall {a}. Maybe (FS TermF a, Maybe (FS TermF a)) -> FS TermF a
Refl ((Term a, Maybe (Term a)) -> Maybe (Term a, Maybe (Term a))
forall a. a -> Maybe a
Just (Term -> Term a
go Term
term, Maybe (Term a)
forall a. Maybe a
Nothing))
      Rzk.ReflTermType BNFC'Position
_loc Term
x Term
tA -> Maybe (Term a, Maybe (Term a)) -> Term a
forall {a}. Maybe (FS TermF a, Maybe (FS TermF a)) -> FS TermF a
Refl ((Term a, Maybe (Term a)) -> Maybe (Term a, Maybe (Term a))
forall a. a -> Maybe a
Just (Term -> Term a
go Term
x, Term a -> Maybe (Term a)
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 -> Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Term a
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 -> Term a -> Term a -> Term a
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.ParamTermType BNFC'Position
_ Term
patTerm Term
arg) Term
ret ->
        let pat :: Pattern
pat = Term -> Pattern
unsafeTermToPattern Term
patTerm
         in Maybe VarIdent
-> Term a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> Term a
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) Maybe (Scope (FS TermF) a)
forall a. Maybe a
Nothing (Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars Term
ret)
      t :: Term
t@(Rzk.TypeFun BNFC'Position
loc (Rzk.ParamTermShape BNFC'Position
loc' Term
patTerm Term
cube Term
tope) Term
ret) ->
        let lint' :: a -> a
lint' = case Term
tope of
              Rzk.App BNFC'Position
_loc Term
fun Term
arg | Term -> Term' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term
arg Term' () -> Term' () -> Bool
forall a. Eq a => a -> a -> Bool
== Term -> Term' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term
patTerm ->
                Term -> Term -> a -> a
forall {a} {a} {a}.
(HasPosition a, Print a, Print a) =>
a -> a -> a -> a
lint Term
t (BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc (BNFC'Position -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
loc' Term
patTerm Term
fun) Term
ret)
              Term
_ -> a -> a
forall a. a -> a
id
            pat :: Pattern
pat = Term -> Pattern
unsafeTermToPattern Term
patTerm
         in Term a -> Term a
forall a. a -> a
lint' (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Maybe VarIdent
-> Term a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> Term a
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) (Scope (FS TermF) a -> Maybe (Scope (FS TermF) a)
forall a. a -> Maybe a
Just (Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars Term
tope)) (Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
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.ParamType BNFC'Position
_ Term
arg) Term
ret ->
        Maybe VarIdent
-> Term a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> Term a
forall {a}.
Maybe VarIdent
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun Maybe VarIdent
forall a. Maybe a
Nothing (Term -> Term a
go Term
arg) Maybe (Scope (FS TermF) a)
forall a. Maybe a
Nothing ((VarIdent -> Scope (FS TermF) a) -> Term -> Scope (FS TermF) a
forall a. (VarIdent -> Term a) -> Term -> Term a
toTerm ((a -> Inc a) -> Term a -> Scope (FS TermF) a
forall a b. (a -> b) -> FS TermF a -> FS TermF b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Inc a
forall var. var -> Inc var
S (Term a -> Scope (FS TermF) a)
-> (VarIdent -> Term a) -> VarIdent -> Scope (FS TermF) a
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 ->
        Maybe VarIdent -> Term a -> Scope (FS TermF) a -> Term a
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) (Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
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 ->
        Maybe VarIdent
-> Maybe (Term a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> Term a
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) Maybe (Term a, Maybe (Scope (FS TermF) a))
forall a. Maybe a
Nothing (Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
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 (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
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 ->
        Maybe VarIdent
-> Maybe (Term a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> Term a
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) ((Term a, Maybe (Scope (FS TermF) a))
-> Maybe (Term a, Maybe (Scope (FS TermF) a))
forall a. a -> Maybe a
Just (Term -> Term a
go Term
ty, Maybe (Scope (FS TermF) a)
forall a. Maybe a
Nothing))
          (Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
_loc (BNFC'Position -> [Pattern] -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Param' a
Rzk.ParamPatternType BNFC'Position
_loc [Pattern]
pats Term
ty Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body))
      Rzk.Lambda BNFC'Position
_loc (Rzk.ParamPatternShape BNFC'Position
_ [] Term
_cube Term
_tope : [Param' BNFC'Position]
params) Term
body ->
        Term -> Term a
go (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
_loc [Param' BNFC'Position]
params Term
body)
      t :: Term
t@(Rzk.Lambda BNFC'Position
_loc (Rzk.ParamPatternShape BNFC'Position
_loc' (Pattern
pat:[Pattern]
pats) Term
cube Term
tope : [Param' BNFC'Position]
params) Term
body) ->
        let lint' :: a -> a
lint' = case Term
tope of
              Rzk.App BNFC'Position
_loc Term
fun Term
arg
                | [Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pattern]
pats Bool -> Bool -> Bool
&& Term -> Term' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term
arg Term' () -> Term' () -> Bool
forall a. Eq a => a -> a -> Bool
== Term -> Term' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Pattern -> Term
patternToTerm Pattern
pat) ->
                    Term -> Term -> a -> a
forall {a} {a} {a}.
(HasPosition a, Print a, Print a) =>
a -> a -> a -> a
lint Term
t (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
_loc (BNFC'Position -> [Pattern] -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Param' a
Rzk.ParamPatternType BNFC'Position
_loc' [Pattern
pat] Term
fun Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body)
              Term
_ -> a -> a
forall a. a -> a
id
         in Term a -> Term a
forall a. a -> a
lint' (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Maybe VarIdent
-> Maybe (Term a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> Term a
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) ((Term a, Maybe (Scope (FS TermF) a))
-> Maybe (Term a, Maybe (Scope (FS TermF) a))
forall a. a -> Maybe a
Just (Term -> Term a
go Term
cube, Scope (FS TermF) a -> Maybe (Scope (FS TermF) a)
forall a. a -> Maybe a
Just (Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars Term
tope)))
              (Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
forall a.
Pattern -> (VarIdent -> Term a) -> Term -> Scope (FS TermF) a
toScopePattern Pattern
pat VarIdent -> Term a
bvars (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
_loc (BNFC'Position -> [Pattern] -> Term -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternShape BNFC'Position
_loc' [Pattern]
pats Term
cube Term
tope Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body))

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

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

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

patternToTerm :: Rzk.Pattern -> Rzk.Term
patternToTerm :: Pattern -> Term
patternToTerm = Pattern -> Term
forall {a}. Pattern' a -> Term' a
ptt
  where
    ptt :: Pattern' a -> Term' a
ptt = \case
      Rzk.PatternVar a
loc VarIdent' a
x    -> a -> VarIdent' a -> Term' a
forall a. a -> VarIdent' a -> Term' a
Rzk.Var a
loc VarIdent' a
x
      Rzk.PatternPair a
loc Pattern' a
l Pattern' a
r -> a -> Term' a -> Term' a -> Term' a
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair a
loc (Pattern' a -> Term' a
ptt Pattern' a
l) (Pattern' a -> Term' a
ptt Pattern' a
r)
      Rzk.PatternUnit a
loc     -> a -> Term' a
forall a. a -> Term' a
Rzk.Unit a
loc

unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern
unsafeTermToPattern :: Term -> Pattern
unsafeTermToPattern = Term -> Pattern
forall {a}. Term' a -> Pattern' a
ttp
  where
    ttp :: Term' a -> Pattern' a
ttp = \case
      Rzk.Unit a
loc                        -> a -> Pattern' a
forall a. a -> Pattern' a
Rzk.PatternUnit a
loc
      Rzk.Var a
loc VarIdent' a
x                       -> a -> VarIdent' a -> Pattern' a
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar a
loc VarIdent' a
x
      Rzk.Pair a
loc Term' a
l Term' a
r                    -> a -> Pattern' a -> Pattern' a -> Pattern' a
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair a
loc (Term' a -> Pattern' a
ttp Term' a
l) (Term' a -> Pattern' a
ttp Term' a
r)
      Term' a
term -> [Char] -> Pattern' a
forall a. HasCallStack => [Char] -> a
error ([Char]
"ERROR: expected a pattern but got\n  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term' a -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term' a
term)

fromTerm' :: Term' -> Rzk.Term
fromTerm' :: Term' -> Term
fromTerm' Term'
t = [VarIdent] -> [VarIdent] -> Term' -> Term
fromTermWith' [VarIdent]
vars ([VarIdent]
defaultVarIdents [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [VarIdent]
vars) Term'
t
  where vars :: [VarIdent]
vars = Term' -> [VarIdent]
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 VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
used) [VarIdent]
xs (Term' -> Term)
-> (Scope (FS TermF) VarIdent -> Term')
-> Scope (FS TermF) VarIdent
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Scope (FS TermF) VarIdent -> (Inc VarIdent -> Term') -> Term'
forall a b. FS TermF a -> (a -> FS TermF b) -> FS TermF b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Inc VarIdent -> Term'
forall {t :: * -> * -> *}. Inc VarIdent -> FS t VarIdent
f)
  where
    f :: Inc VarIdent -> FS t VarIdent
f Inc VarIdent
Z     = VarIdent -> FS t VarIdent
forall (t :: * -> * -> *) a. a -> FS t a
Pure VarIdent
x
    f (S VarIdent
z) = VarIdent -> FS t VarIdent
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]
_    -> [Char] -> t
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', (VarIdent -> Bool) -> [VarIdent] -> [VarIdent]
forall a. (a -> Bool) -> [a] -> [a]
filter (VarIdent -> VarIdent -> Bool
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 = Maybe a
forall a. Maybe a
Nothing

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

      Term'
Universe -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Universe BNFC'Position
forall a. Maybe a
loc
      Term'
UniverseCube -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.UniverseCube BNFC'Position
forall a. Maybe a
loc
      Term'
UniverseTope -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.UniverseTope BNFC'Position
forall a. Maybe a
loc
      Term'
CubeUnit -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeUnit BNFC'Position
forall a. Maybe a
loc
      Term'
CubeUnitStar -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeUnitStar BNFC'Position
forall a. Maybe a
loc
      Term'
Cube2 -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2 BNFC'Position
forall a. Maybe a
loc
      Term'
Cube2_0 -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2_0 BNFC'Position
forall a. Maybe a
loc
      Term'
Cube2_1 -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2_1 BNFC'Position
forall a. Maybe a
loc
      CubeProduct Term'
l Term'
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.CubeProduct BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      Term'
TopeTop -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TopeTop BNFC'Position
forall a. Maybe a
loc
      Term'
TopeBottom -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TopeBottom BNFC'Position
forall a. Maybe a
loc
      TopeEQ Term'
l Term'
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeEQ BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      TopeLEQ Term'
l Term'
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeLEQ BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      TopeAnd Term'
l Term'
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeAnd BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      TopeOr Term'
l Term'
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeOr BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      Term'
RecBottom -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.RecBottom BNFC'Position
forall a. Maybe a
loc
      RecOr [(Term', Term')]
rs -> BNFC'Position -> [Restriction' BNFC'Position] -> Term
forall a. a -> [Restriction' a] -> Term' a
Rzk.RecOr BNFC'Position
forall a. Maybe a
loc [ BNFC'Position -> Term -> Term -> Restriction' BNFC'Position
forall a. a -> Term' a -> Term' a -> Restriction' a
Rzk.Restriction BNFC'Position
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 -> Maybe VarIdent -> ((VarIdent, [VarIdent]) -> Term) -> Term
forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z (((VarIdent, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> VarIdent -> Term
forall a. a -> VarIdent' a -> Term' a
Rzk.Var BNFC'Position
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 -> Maybe VarIdent -> ((VarIdent, [VarIdent]) -> Term) -> Term
forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z (((VarIdent, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Term -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermShape BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> VarIdent -> Term
forall a. a -> VarIdent' a -> Term' a
Rzk.Var BNFC'Position
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 -> Maybe VarIdent -> ((VarIdent, [VarIdent]) -> Term) -> Term
forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z (((VarIdent, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        BNFC'Position -> Pattern -> Term -> Term -> Term
forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
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 -> BNFC'Position -> Term -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a -> Term' a
Rzk.TypeId BNFC'Position
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 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeIdSimple BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      App Term'
l Term'
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App BNFC'Position
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 -> Maybe VarIdent -> ((VarIdent, [VarIdent]) -> Term) -> Term
forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z (((VarIdent, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
forall a. Maybe a
loc [BNFC'Position -> Pattern -> Param' BNFC'Position
forall a. a -> Pattern' a -> Param' a
Rzk.ParamPattern BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
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 -> Maybe VarIdent -> ((VarIdent, [VarIdent]) -> Term) -> Term
forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z (((VarIdent, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
forall a. Maybe a
loc [BNFC'Position -> [Pattern] -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Param' a
Rzk.ParamPatternType BNFC'Position
forall a. Maybe a
loc [BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
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 -> Maybe VarIdent -> ((VarIdent, [VarIdent]) -> Term) -> Term
forall {t}. Maybe VarIdent -> ((VarIdent, [VarIdent]) -> t) -> t
withFresh Maybe VarIdent
z (((VarIdent, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, [VarIdent]
xs) ->
        BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
forall a. Maybe a
loc [BNFC'Position -> [Pattern] -> Term -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternShape BNFC'Position
forall a. Maybe a
loc [BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
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 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      First Term'
term -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.First BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
term)
      Second Term'
term -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.Second BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
term)
      Term'
TypeUnit -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TypeUnit BNFC'Position
forall a. Maybe a
loc
      Term'
Unit -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Unit BNFC'Position
forall a. Maybe a
loc
      Refl Maybe (Term', Maybe Term')
Nothing -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Refl BNFC'Position
forall a. Maybe a
loc
      Refl (Just (Term'
t, Maybe Term'
Nothing)) -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.ReflTerm BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
t)
      Refl (Just (Term'
t, Just Term'
ty)) -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.ReflTermType BNFC'Position
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 -> BNFC'Position
-> Term -> Term -> Term -> Term -> Term -> Term -> Term
forall a.
a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
Rzk.IdJ BNFC'Position
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 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeAsc BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
l) (Term' -> Term
go Term'
r)
      TypeRestricted Term'
ty [(Term', Term')]
rs ->
        BNFC'Position -> Term -> [Restriction' BNFC'Position] -> Term
forall a. a -> Term' a -> [Restriction' a] -> Term' a
Rzk.TypeRestricted BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
ty) (((Term', Term') -> Restriction' BNFC'Position)
-> [(Term', Term')] -> [Restriction' BNFC'Position]
forall a b. (a -> b) -> [a] -> [b]
map (\(Term'
tope, Term'
term) -> (BNFC'Position -> Term -> Term -> Restriction' BNFC'Position
forall a. a -> Term' a -> Term' a -> Restriction' a
Rzk.Restriction BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
tope) (Term' -> Term
go Term'
term))) [(Term', Term')]
rs)

defaultVarIdents :: [VarIdent]
defaultVarIdents :: [VarIdent]
defaultVarIdents =
  [ [Char] -> VarIdent
forall a. IsString a => [Char] -> a
fromString [Char]
name
  | Integer
n <- [Integer
1..]
  , let name :: [Char]
name = [Char]
"x" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
digitToSub (Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n) ]
  where
    digitToSub :: Char -> Char
digitToSub Char
c = Int -> Char
chr ((Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') Int -> Int -> Int
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.
--
-- >>> print $ refreshVar ["x", "y", "x₁", "z"] "x"
-- x₂
refreshVar :: [VarIdent] -> VarIdent -> VarIdent
refreshVar :: [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
vars VarIdent
x
  | VarIdent
x VarIdent -> [VarIdent] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 (RzkPosition -> VarIdentToken -> VarIdent' RzkPosition
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent RzkPosition
loc (([Char] -> [Char]) -> VarIdentToken -> VarIdentToken
forall a b. Coercible a b => a -> b
coerce [Char] -> [Char]
incIndex VarIdentToken
token))

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

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

instance IsString Term' where
  fromString :: [Char] -> Term'
fromString = Term -> Term'
toTerm' (Term -> Term') -> ([Char] -> Term) -> [Char] -> Term'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either [Char] Term -> Term
forall {a}. Either [Char] a -> a
fromRight (Either [Char] Term -> Term)
-> ([Char] -> Either [Char] Term) -> [Char] -> Term
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) = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"Parse error: " [Char] -> [Char] -> [Char]
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{} = Term -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree (Term' -> Term
fromTerm' (TermT' -> Term'
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'
infoType :: forall term. TypeInfo term -> term
infoWHNF :: forall term. TypeInfo term -> Maybe term
infoNF :: forall term. TypeInfo term -> Maybe term
infoType :: TermT'
infoWHNF :: Maybe TermT'
infoNF :: Maybe TermT'
..} TermF (Scope (FS (AnnF TypeInfo TermF)) VarIdent) TermT'
_)) = [Char]
termStr [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" : " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
typeStr
    where
      termStr :: [Char]
termStr = Term -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree (Term' -> Term
fromTerm' (TermT' -> Term'
forall (ann :: * -> *) (term :: * -> * -> *) a.
(Functor ann, Bifunctor term) =>
FS (AnnF ann term) a -> FS term a
untyped TermT'
term))
      typeStr :: [Char]
typeStr = Term -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree (Term' -> Term
fromTerm' (TermT' -> Term'
forall (ann :: * -> *) (term :: * -> * -> *) a.
(Functor ann, Bifunctor term) =>
FS (AnnF ann term) a -> FS term a
untyped TermT'
infoType))