{-# 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      (bimap)
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 qualified Data.Text           as T

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

-- | The display name of a hole from its surface token text. The token includes
-- the leading @?@; an anonymous hole (bare @?@) has no name.
holeName :: T.Text -> Maybe VarIdent
holeName :: Text -> Maybe VarIdent
holeName Text
tok =
  case Int -> Text -> Text
T.drop Int
1 Text
tok of
    Text
name | Text -> Bool
T.null Text
name -> Maybe VarIdent
forall a. Maybe a
Nothing
         | Bool
otherwise   -> VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just ([Char] -> VarIdent
forall a. IsString a => [Char] -> a
fromString (Text -> [Char]
T.unpack Text
name))

-- | The surface token text (including the leading @?@) for a hole name.
holeIdentToken :: Maybe VarIdent -> T.Text
holeIdentToken :: Maybe VarIdent -> Text
holeIdentToken Maybe VarIdent
Nothing  = Text
"?"
holeIdentToken (Just VarIdent
x) = Text
"?" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
x)

-- | The name(s) a binder introduces. A binder may name a single (possibly
-- anonymous) variable, or destructure a pair\/tuple via a pattern. The pattern
-- structure is kept around purely so that goals, holes and error messages can
-- show the user's original names (e.g. @t@ and @s@ for @\\ (t , s) -> …@)
-- instead of projections of a fresh variable (e.g. @π₁ x₄@ and @π₂ x₄@).
--
-- Operationally a pair pattern still binds a /single/ variable; the components
-- are projections of it (see 'toScopePattern'). 'Binder' only records the names
-- so they can be restored when rendering.
data Binder
  = BinderVar (Maybe VarIdent)   -- ^ a single variable (@Nothing@ for @_@)
  | BinderPair Binder Binder     -- ^ a pair pattern @(l , r)@
  | BinderUnit                   -- ^ the unit pattern @unit@
  deriving (Binder -> Binder -> Bool
(Binder -> Binder -> Bool)
-> (Binder -> Binder -> Bool) -> Eq Binder
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Binder -> Binder -> Bool
== :: Binder -> Binder -> Bool
$c/= :: Binder -> Binder -> Bool
/= :: Binder -> Binder -> Bool
Eq)

-- | The single name of a binder, if it binds exactly one named variable.
-- A pair\/unit pattern has no single name, so this is 'Nothing' for them.
-- Used wherever the old @Maybe VarIdent@ binder name is still sufficient.
binderName :: Binder -> Maybe VarIdent
binderName :: Binder -> Maybe VarIdent
binderName (BinderVar Maybe VarIdent
mname) = Maybe VarIdent
mname
binderName Binder
_                 = Maybe VarIdent
forall a. Maybe a
Nothing

data TModality = Sharp | Flat | Op | Id deriving (TModality -> TModality -> Bool
(TModality -> TModality -> Bool)
-> (TModality -> TModality -> Bool) -> Eq TModality
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TModality -> TModality -> Bool
== :: TModality -> TModality -> Bool
$c/= :: TModality -> TModality -> Bool
/= :: TModality -> TModality -> Bool
Eq, Int -> TModality -> [Char] -> [Char]
[TModality] -> [Char] -> [Char]
TModality -> [Char]
(Int -> TModality -> [Char] -> [Char])
-> (TModality -> [Char])
-> ([TModality] -> [Char] -> [Char])
-> Show TModality
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> TModality -> [Char] -> [Char]
showsPrec :: Int -> TModality -> [Char] -> [Char]
$cshow :: TModality -> [Char]
show :: TModality -> [Char]
$cshowList :: [TModality] -> [Char] -> [Char]
showList :: [TModality] -> [Char] -> [Char]
Show)

toModality :: Rzk.Modality -> TModality
toModality :: Modality -> TModality
toModality Rzk.Sharp{}       = TModality
Sharp
toModality Rzk.ASCII_Sharp{} = TModality
Sharp
toModality Rzk.Flat{}        = TModality
Flat
toModality Rzk.ASCII_Flat{}  = TModality
Flat
toModality Rzk.Op{}          = TModality
Op
toModality Rzk.ASCII_Op{}    = TModality
Op
toModality Rzk.Id{}          = TModality
Id

modCompToMods :: Rzk.ModComp -> (TModality, TModality)
modCompToMods :: ModComp -> (TModality, TModality)
modCompToMods (Rzk.Single BNFC'Position
_ Modality
m)      = (TModality
Id, Modality -> TModality
toModality Modality
m)
modCompToMods (Rzk.Comp BNFC'Position
_ Modality
ext Modality
inn)  = (Modality -> TModality
toModality Modality
ext, Modality -> TModality
toModality Modality
inn)

fromMod :: TModality -> Rzk.Modality
fromMod :: TModality -> Modality
fromMod TModality
Sharp = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Sharp BNFC'Position
forall a. Maybe a
Nothing
fromMod TModality
Flat  = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Flat BNFC'Position
forall a. Maybe a
Nothing
fromMod TModality
Op    = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Op BNFC'Position
forall a. Maybe a
Nothing
fromMod TModality
Id    = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Id BNFC'Position
forall a. Maybe a
Nothing

modsToModComp :: TModality -> TModality -> Rzk.ModComp
modsToModComp :: TModality -> TModality -> ModComp
modsToModComp TModality
Id TModality
inn  = BNFC'Position -> Modality -> ModComp
forall a. a -> Modality' a -> ModComp' a
Rzk.Single BNFC'Position
forall a. Maybe a
Nothing (TModality -> Modality
fromMod TModality
inn)
modsToModComp TModality
ext TModality
inn = BNFC'Position -> Modality -> Modality -> ModComp
forall a. a -> Modality' a -> Modality' a -> ModComp' a
Rzk.Comp BNFC'Position
forall a. Maybe a
Nothing (TModality -> Modality
fromMod TModality
ext) (TModality -> Modality
fromMod TModality
inn)

data TermF scope term
    = UniverseF
    | UniverseCubeF 
    | UniverseTopeF
    | CubeUnitF
    | CubeUnitStarF
    | Cube2F
    | Cube2_0F
    | Cube2_1F
    | CubeIF 
    | CubeI_0F 
    | CubeI_1F
    | CubeProductF term term
    | CubeFlipF term
    | CubeUnflipF term
    | TopeTopF
    | TopeBottomF
    | TopeEQF term term
    | TopeLEQF term term
    | TopeAndF term term
    | TopeOrF term term
    | TopeInvF term 
    | TopeUninvF term
    | RecBottomF
    | RecOrF [(term, term)]
    | TypeFunF Binder TModality term (Maybe scope) scope
    | TypeSigmaF Binder TModality term scope
    | TypeIdF term (Maybe term) term
    | AppF term term
    | LetF Binder (Maybe term) term scope
    | LambdaF Binder (Maybe (TModality, 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)]
    | TypeModalF TModality term
    | ModAppF TModality term
    | ModExtractF TModality TModality term
    | LetModF Binder TModality TModality (Maybe term) term scope
    | HoleF (Maybe VarIdent)
    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 term, Eq scope) =>
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
/= :: 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 scope m. Monoid m => TermF scope m -> m
forall m a. Monoid m => (a -> m) -> TermF scope a -> 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)
    bindings (Rzk.PatternTuple BNFC'Position
loc Pattern
p1 Pattern
p2 [Pattern]
ps) FS TermF a
t = Pattern -> FS TermF a -> [(VarIdent, FS TermF a)]
bindings (BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
forall {t}.
t -> [Pattern' t] -> Pattern' t -> Pattern' t -> Pattern' t
desugarTuple BNFC'Position
loc ([Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
ps) Pattern
p2 Pattern
p1) FS TermF a
t

desugarTuple :: t -> [Pattern' t] -> Pattern' t -> Pattern' t -> Pattern' t
desugarTuple t
loc [Pattern' t]
ps Pattern' t
p2 Pattern' t
p1 =
  case [Pattern' t]
ps of
    []          -> t -> Pattern' t -> Pattern' t -> Pattern' t
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair t
loc Pattern' t
p1 Pattern' t
p2
    Pattern' t
pLast : [Pattern' t]
ps' -> t -> Pattern' t -> Pattern' t -> Pattern' t
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair t
loc (t -> [Pattern' t] -> Pattern' t -> Pattern' t -> Pattern' t
desugarTuple t
loc [Pattern' t]
ps' Pattern' t
p2 Pattern' t
p1) Pattern' t
pLast

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_TypeSigmaTuple BNFC'Position
loc SigmaParam' BNFC'Position
p [SigmaParam' BNFC'Position]
ps Term
tN -> Term -> Term a
go (BNFC'Position
-> SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position]
-> Term
-> Term
forall a.
a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
Rzk.TypeSigmaTuple BNFC'Position
loc SigmaParam' BNFC'Position
p [SigmaParam' BNFC'Position]
ps Term
tN)
      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.CubeI BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
CubeI
      Rzk.CubeI_0 BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
CubeI_0
      Rzk.CubeI_1 BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
CubeI_1
      Rzk.ASCII_CubeI BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
CubeI
      Rzk.ASCII_CubeI_0 BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
CubeI_0
      Rzk.ASCII_CubeI_1 BNFC'Position
_loc -> Term a
forall {a}. FS TermF a
CubeI_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.TopeInv BNFC'Position
_loc Term
t -> Term a -> Term a
forall {a}. FS TermF a -> FS TermF a
TopeInv (Term -> Term a
go Term
t)
      Rzk.TopeUninv BNFC'Position
_loc Term
t -> Term a -> Term a
forall {a}. FS TermF a -> FS TermF a
TopeUninv (Term -> Term a
go Term
t)
      Rzk.CubeFlip BNFC'Position
_loc Term
t -> Term a -> Term a
forall {a}. FS TermF a -> FS TermF a
CubeFlip (Term -> Term a
go Term
t)
      Rzk.CubeUnflip BNFC'Position
_loc Term
t -> Term a -> Term a
forall {a}. FS TermF a -> FS TermF a
CubeUnflip (Term -> Term a
go Term
t)
      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.Tuple BNFC'Position
_loc Term
p1 Term
p2 (Term
p:[Term]
ps) -> Term -> Term a
go (BNFC'Position -> Term -> Term -> [Term] -> Term
forall a. a -> Term' a -> Term' a -> [Term' a] -> Term' a
Rzk.Tuple BNFC'Position
_loc (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
_loc Term
p1 Term
p2) Term
p [Term]
ps)
      Rzk.Tuple BNFC'Position
_loc Term
p1 Term
p2 [] -> Term -> Term a
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
_loc Term
p1 Term
p2)
      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)
      -- A binder may name several variables sharing a type, e.g. (x y : A),
      -- which is parsed as the application spine `x y`. Desugar it into nested
      -- one-variable binders ((x : A) → (y : A) → …) before translating, so the
      -- pattern conversion never sees a juxtaposition. (Shape binders are left
      -- alone: their tope refers to the single bound point.)
      Rzk.TypeFun BNFC'Position
loc (Rzk.ParamTermType BNFC'Position
loc' Term
patTerm Term
arg) Term
ret
        | Term
_ : Term
_ : [Term]
_ <- [Term]
vars ->
            Term -> Term a
go ((Term -> Term -> Term) -> Term -> [Term] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Term
v -> 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
v Term
arg)) Term
ret [Term]
vars)
        where vars :: [Term]
vars = Term -> [Term]
flattenBinderApp Term
patTerm
      Rzk.TypeFun BNFC'Position
loc (Rzk.ParamTermModalType BNFC'Position
loc' Term
patTerm ModalColon' BNFC'Position
mc Term
ty) Term
ret
        | Term
_ : Term
_ : [Term]
_ <- [Term]
vars ->
            Term -> Term a
go ((Term -> Term -> Term) -> Term -> [Term] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Term
v -> BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc (BNFC'Position
-> Term
-> ModalColon' BNFC'Position
-> Term
-> ParamDecl' BNFC'Position
forall a. a -> Term' a -> ModalColon' a -> Term' a -> ParamDecl' a
Rzk.ParamTermModalType BNFC'Position
loc' Term
v ModalColon' BNFC'Position
mc Term
ty)) Term
ret [Term]
vars)
        where vars :: [Term]
vars = Term -> [Term]
flattenBinderApp Term
patTerm
      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamTermModalType BNFC'Position
_loc' Term
patTerm ModalColon' BNFC'Position
mc Term
ty) Term
ret ->
        let pat :: Pattern
pat = Term -> Pattern
unsafeTermToPattern Term
patTerm
            md :: TModality
md  = ModalColon' BNFC'Position -> TModality
modalColonToTModality ModalColon' BNFC'Position
mc
        in Binder
-> TModality
-> Term a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> TModality
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun (Pattern -> Binder
toBinder Pattern
pat) TModality
md (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 Term
ret)
      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamTermModalShape BNFC'Position
_loc' Term
patTerm ModalColon' BNFC'Position
mc Term
cube Term
tope) Term
ret ->
        let pat :: Pattern
pat = Term -> Pattern
unsafeTermToPattern Term
patTerm
            md :: TModality
md  = ModalColon' BNFC'Position -> TModality
modalColonToTModality ModalColon' BNFC'Position
mc
        in Binder
-> TModality
-> Term a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> TModality
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun (Pattern -> Binder
toBinder Pattern
pat) TModality
md (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.ParamTermType BNFC'Position
_ Term
patTerm Term
arg) Term
ret ->
        let pat :: Pattern
pat = Term -> Pattern
unsafeTermToPattern Term
patTerm
        in Binder
-> TModality
-> Term a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> TModality
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun (Pattern -> Binder
toBinder Pattern
pat) TModality
Id (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
$ Binder
-> TModality
-> Term a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> TModality
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun (Pattern -> Binder
toBinder Pattern
pat) TModality
Id (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 ->
        Binder
-> TModality
-> Term a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> TModality
-> FS TermF a
-> Maybe (Scope (FS TermF) a)
-> Scope (FS TermF) a
-> FS TermF a
TypeFun (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id (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 ->
        Binder -> TModality -> Term a -> Scope (FS TermF) a -> Term a
forall {a}.
Binder
-> TModality -> FS TermF a -> Scope (FS TermF) a -> FS TermF a
TypeSigma (Pattern -> Binder
toBinder Pattern
pat) TModality
Id (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.TypeSigmaModal BNFC'Position
_loc Pattern
pat ModalColon' BNFC'Position
mc Term
ty Term
body ->
        let md :: TModality
md = ModalColon' BNFC'Position -> TModality
modalColonToTModality ModalColon' BNFC'Position
mc
        in Binder -> TModality -> Term a -> Scope (FS TermF) a -> Term a
forall {a}.
Binder
-> TModality -> FS TermF a -> Scope (FS TermF) a -> FS TermF a
TypeSigma (Pattern -> Binder
toBinder Pattern
pat) TModality
md (Term -> Term a
go Term
ty) (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
body)

      Rzk.TypeSigmaTuple BNFC'Position
_loc (Rzk.SigmaParamModal BNFC'Position
_loc' Pattern
pat ModalColon' BNFC'Position
mc Term
ty) [SigmaParam' BNFC'Position]
rest Term
body ->
        let md :: TModality
md = ModalColon' BNFC'Position -> TModality
modalColonToTModality ModalColon' BNFC'Position
mc
            tailSigma :: Term
tailSigma = case [SigmaParam' BNFC'Position]
rest of
              []       -> Term
body
              [SigmaParam' BNFC'Position
sp]     -> BNFC'Position -> SigmaParam' BNFC'Position -> Term -> Term
sigmaParamToTypeSigma BNFC'Position
_loc SigmaParam' BNFC'Position
sp Term
body
              (SigmaParam' BNFC'Position
sp:[SigmaParam' BNFC'Position]
sps) -> BNFC'Position
-> SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position]
-> Term
-> Term
forall a.
a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
Rzk.TypeSigmaTuple BNFC'Position
_loc SigmaParam' BNFC'Position
sp [SigmaParam' BNFC'Position]
sps Term
body
        in Binder -> TModality -> Term a -> Scope (FS TermF) a -> Term a
forall {a}.
Binder
-> TModality -> FS TermF a -> Scope (FS TermF) a -> FS TermF a
TypeSigma (Pattern -> Binder
toBinder Pattern
pat) TModality
md (Term -> Term a
go Term
ty) (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
tailSigma)
      Rzk.TypeSigmaTuple BNFC'Position
_loc (Rzk.SigmaParam BNFC'Position
_ Pattern
patA Term
tA) (mp :: SigmaParam' BNFC'Position
mp@(Rzk.SigmaParamModal{}) : [SigmaParam' BNFC'Position]
rest) Term
body ->
        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
patA Term
tA (case [SigmaParam' BNFC'Position]
rest of
              []  -> BNFC'Position -> SigmaParam' BNFC'Position -> Term -> Term
sigmaParamToTypeSigma BNFC'Position
_loc SigmaParam' BNFC'Position
mp Term
body
              [SigmaParam' BNFC'Position]
_   -> BNFC'Position
-> SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position]
-> Term
-> Term
forall a.
a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
Rzk.TypeSigmaTuple BNFC'Position
_loc SigmaParam' BNFC'Position
mp [SigmaParam' BNFC'Position]
rest Term
body))
      Rzk.TypeSigmaTuple BNFC'Position
_loc (Rzk.SigmaParam BNFC'Position
_ Pattern
patA Term
tA) ((Rzk.SigmaParam BNFC'Position
_ Pattern
patB Term
tB) : [SigmaParam' BNFC'Position]
ps) Term
tN ->
        Term -> Term a
go (BNFC'Position
-> SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position]
-> Term
-> Term
forall a.
a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
Rzk.TypeSigmaTuple BNFC'Position
_loc (BNFC'Position -> Pattern -> Term -> SigmaParam' BNFC'Position
forall a. a -> Pattern' a -> Term' a -> SigmaParam' a
Rzk.SigmaParam BNFC'Position
_loc Pattern
patX Term
tX) [SigmaParam' BNFC'Position]
ps Term
tN)
        where
          patX :: Pattern
patX = BNFC'Position -> Pattern -> Pattern -> Pattern
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair BNFC'Position
_loc Pattern
patA Pattern
patB
          tX :: Term
tX = BNFC'Position -> Pattern -> Term -> Term -> Term
forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma BNFC'Position
_loc Pattern
patA Term
tA Term
tB
      Rzk.TypeSigmaTuple BNFC'Position
_loc (Rzk.SigmaParam BNFC'Position
_ Pattern
pat Term
tA) [] Term
tB -> 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
tA Term
tB)
      Rzk.Lambda BNFC'Position
_loc (Rzk.ParamPatternModalType BNFC'Position
_ [] ModalColon' BNFC'Position
_mc 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.ParamPatternModalType BNFC'Position
loc' (Pattern
pat:[Pattern]
pats) ModalColon' BNFC'Position
mc Term
ty : [Param' BNFC'Position]
params) Term
body ->
        let md :: TModality
md = ModalColon' BNFC'Position -> TModality
modalColonToTModality ModalColon' BNFC'Position
mc
        in Binder
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> Maybe (TModality, FS TermF a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> FS TermF a
Lambda (Pattern -> Binder
toBinder Pattern
pat) ((TModality, Term a, Maybe (Scope (FS TermF) a))
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
forall a. a -> Maybe a
Just (TModality
md, 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 (if [Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pattern]
pats then [Param' BNFC'Position]
params else BNFC'Position
-> [Pattern]
-> ModalColon' BNFC'Position
-> Term
-> Param' BNFC'Position
forall a. a -> [Pattern' a] -> ModalColon' a -> Term' a -> Param' a
Rzk.ParamPatternModalType BNFC'Position
loc' [Pattern]
pats ModalColon' BNFC'Position
mc 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.ParamPatternModalShape BNFC'Position
_ [] ModalColon' BNFC'Position
_mc 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)
      Rzk.Lambda BNFC'Position
_loc (Rzk.ParamPatternModalShape BNFC'Position
loc' (Pattern
pat:[Pattern]
pats) ModalColon' BNFC'Position
mc Term
cube Term
tope : [Param' BNFC'Position]
params) Term
body ->
        let md :: TModality
md = ModalColon' BNFC'Position -> TModality
modalColonToTModality ModalColon' BNFC'Position
mc
        in Binder
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> Maybe (TModality, FS TermF a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> FS TermF a
Lambda (Pattern -> Binder
toBinder Pattern
pat) ((TModality, Term a, Maybe (Scope (FS TermF) a))
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
forall a. a -> Maybe a
Just (TModality
md, 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 (if [Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pattern]
pats then [Param' BNFC'Position]
params else BNFC'Position
-> [Pattern]
-> ModalColon' BNFC'Position
-> Term
-> Term
-> Param' BNFC'Position
forall a.
a
-> [Pattern' a] -> ModalColon' a -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternModalShape BNFC'Position
loc' [Pattern]
pats ModalColon' BNFC'Position
mc 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.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 ->
        Binder
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> Maybe (TModality, FS TermF a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> FS TermF a
Lambda (Pattern -> Binder
toBinder Pattern
pat) Maybe (TModality, 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 ->
        Binder
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> Maybe (TModality, FS TermF a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> FS TermF a
Lambda (Pattern -> Binder
toBinder Pattern
pat) ((TModality, Term a, Maybe (Scope (FS TermF) a))
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
forall a. a -> Maybe a
Just (TModality
Id, 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
$ Binder
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> Maybe (TModality, FS TermF a, Maybe (Scope (FS TermF) a))
-> Scope (FS TermF) a
-> FS TermF a
Lambda (Pattern -> Binder
toBinder Pattern
pat) ((TModality, Term a, Maybe (Scope (FS TermF) a))
-> Maybe (TModality, Term a, Maybe (Scope (FS TermF) a))
forall a. a -> Maybe a
Just (TModality
Id, 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.Let BNFC'Position
_loc (Rzk.BindPattern BNFC'Position
_ Pattern
pat) Term
val Term
expr ->
        Binder -> Maybe (Term a) -> Term a -> Scope (FS TermF) a -> Term a
forall {a}.
Binder
-> Maybe (FS TermF a)
-> FS TermF a
-> Scope (FS TermF) a
-> FS TermF a
Let (Pattern -> Binder
toBinder Pattern
pat) Maybe (Term a)
forall a. Maybe a
Nothing (Term -> Term a
go Term
val) (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
expr)
      Rzk.Let BNFC'Position
_loc (Rzk.BindPatternType BNFC'Position
_ Pattern
pat Term
ty) Term
val Term
expr -> 
        Binder -> Maybe (Term a) -> Term a -> Scope (FS TermF) a -> Term a
forall {a}.
Binder
-> Maybe (FS TermF a)
-> FS TermF a
-> Scope (FS TermF) a
-> FS TermF a
Let (Pattern -> Binder
toBinder Pattern
pat) (Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term -> Term a
go Term
ty)) (Term -> Term a
go Term
val) (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
expr)
      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 (Rzk.HoleIdent BNFC'Position
_ (Rzk.HoleIdentToken Text
tok)) ->
        Maybe VarIdent -> Term a
forall {a}. Maybe VarIdent -> FS TermF a
Hole (Text -> Maybe VarIdent
holeName Text
tok)
      Rzk.ModApp BNFC'Position
_loc Modality
md Term
body -> TModality -> Term a -> Term a
forall {a}. TModality -> FS TermF a -> FS TermF a
ModApp (Modality -> TModality
toModality Modality
md) (Term -> Term a
go Term
body)
      Rzk.ModType BNFC'Position
_loc Modality
md Term
ty -> TModality -> Term a -> Term a
forall {a}. TModality -> FS TermF a -> FS TermF a
TypeModal (Modality -> TModality
toModality Modality
md) (Term -> Term a
go Term
ty)
      Rzk.ModExtract{} -> [Char] -> Term a
forall a. HasCallStack => [Char] -> a
error [Char]
"$extract$ is an internal term and cannot appear in source"
      Rzk.LetMod BNFC'Position
_loc ModComp
comp (Rzk.BindPattern BNFC'Position
_ Pattern
pat) Term
val Term
body ->
        let (TModality
ext, TModality
inn) = ModComp -> (TModality, TModality)
modCompToMods ModComp
comp
        in Binder
-> TModality
-> TModality
-> Maybe (Term a)
-> Term a
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> TModality
-> TModality
-> Maybe (FS TermF a)
-> FS TermF a
-> Scope (FS TermF) a
-> FS TermF a
LetMod (Pattern -> Binder
toBinder Pattern
pat) TModality
ext TModality
inn Maybe (Term a)
forall a. Maybe a
Nothing (Term -> Term a
go Term
val) (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
body)
      Rzk.LetMod BNFC'Position
_loc ModComp
comp (Rzk.BindPatternType BNFC'Position
_ Pattern
pat Term
ty) Term
val Term
body ->
        let (TModality
ext, TModality
inn) = ModComp -> (TModality, TModality)
modCompToMods ModComp
comp
        in Binder
-> TModality
-> TModality
-> Maybe (Term a)
-> Term a
-> Scope (FS TermF) a
-> Term a
forall {a}.
Binder
-> TModality
-> TModality
-> Maybe (FS TermF a)
-> FS TermF a
-> Scope (FS TermF) a
-> FS TermF a
LetMod (Pattern -> Binder
toBinder Pattern
pat) TModality
ext TModality
inn (Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term -> Term a
go Term
ty)) (Term -> Term a
go Term
val) (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
body)

    -- Translate a surface pattern into a 'Binder', keeping the pair\/tuple
    -- structure so the component names can be restored when rendering.
    toBinder :: Pattern -> Binder
toBinder (Rzk.PatternVar BNFC'Position
_loc (Rzk.VarIdent BNFC'Position
_ VarIdentToken
"_")) = Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing
    toBinder (Rzk.PatternVar BNFC'Position
_loc VarIdent
x)                    = Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (VarIdent -> VarIdent
varIdent VarIdent
x))
    toBinder (Rzk.PatternUnit BNFC'Position
_loc)                     = Binder
BinderUnit
    toBinder (Rzk.PatternPair BNFC'Position
_loc Pattern
l Pattern
r)                 = Binder -> Binder -> Binder
BinderPair (Pattern -> Binder
toBinder Pattern
l) (Pattern -> Binder
toBinder Pattern
r)
    toBinder (Rzk.PatternTuple BNFC'Position
loc Pattern
p1 Pattern
p2 [Pattern]
ps)            = Pattern -> Binder
toBinder (BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
forall {t}.
t -> [Pattern' t] -> Pattern' t -> Pattern' t -> Pattern' t
desugarTuple BNFC'Position
loc ([Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
ps) Pattern
p2 Pattern
p1)

patternToTerm :: Rzk.Pattern -> Rzk.Term
patternToTerm :: Pattern -> Term
patternToTerm = Pattern -> Term
ptt
  where
    ptt :: Pattern -> Term
ptt = \case
      Rzk.PatternVar BNFC'Position
loc VarIdent
x    -> BNFC'Position -> VarIdent -> Term
forall a. a -> VarIdent' a -> Term' a
Rzk.Var BNFC'Position
loc VarIdent
x
      Rzk.PatternPair BNFC'Position
loc Pattern
l Pattern
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
loc (Pattern -> Term
ptt Pattern
l) (Pattern -> Term
ptt Pattern
r)
      Rzk.PatternUnit BNFC'Position
loc     -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Unit BNFC'Position
loc
      Rzk.PatternTuple BNFC'Position
loc Pattern
p1 Pattern
p2 [Pattern]
ps -> Pattern -> Term
patternToTerm (BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
forall {t}.
t -> [Pattern' t] -> Pattern' t -> Pattern' t -> Pattern' t
desugarTuple BNFC'Position
loc ([Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
ps) Pattern
p2 Pattern
p1)


modalColonModality :: Rzk.ModalColon -> Rzk.Modality
modalColonModality :: ModalColon' BNFC'Position -> Modality
modalColonModality = \case
  Rzk.ModalColonFlat BNFC'Position
loc        -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Flat BNFC'Position
loc
  Rzk.ModalColonSharp BNFC'Position
loc       -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Sharp BNFC'Position
loc
  Rzk.ModalColonOp BNFC'Position
loc          -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Op BNFC'Position
loc
  Rzk.ModalColonId BNFC'Position
loc          -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Id BNFC'Position
loc
  Rzk.ASCII_ModalColonFlat BNFC'Position
loc  -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Flat BNFC'Position
loc
  Rzk.ASCII_ModalColonSharp BNFC'Position
loc -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Sharp BNFC'Position
loc
  Rzk.ASCII_ModalColonOp BNFC'Position
loc    -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Op BNFC'Position
loc

modalColonToTModality :: Rzk.ModalColon -> TModality
modalColonToTModality :: ModalColon' BNFC'Position -> TModality
modalColonToTModality = Modality -> TModality
toModality (Modality -> TModality)
-> (ModalColon' BNFC'Position -> Modality)
-> ModalColon' BNFC'Position
-> TModality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModalColon' BNFC'Position -> Modality
modalColonModality

fromTModalityToModalColon :: TModality -> Rzk.ModalColon
fromTModalityToModalColon :: TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon = \case
  TModality
Sharp -> BNFC'Position -> ModalColon' BNFC'Position
forall a. a -> ModalColon' a
Rzk.ModalColonSharp BNFC'Position
forall a. Maybe a
Nothing
  TModality
Flat  -> BNFC'Position -> ModalColon' BNFC'Position
forall a. a -> ModalColon' a
Rzk.ModalColonFlat BNFC'Position
forall a. Maybe a
Nothing
  TModality
Op    -> BNFC'Position -> ModalColon' BNFC'Position
forall a. a -> ModalColon' a
Rzk.ModalColonOp BNFC'Position
forall a. Maybe a
Nothing
  TModality
Id    -> BNFC'Position -> ModalColon' BNFC'Position
forall a. a -> ModalColon' a
Rzk.ModalColonId BNFC'Position
forall a. Maybe a
Nothing

-- | Split a binder term into the individual variables it names. A multi-variable
-- binder like @(x y : A)@ is parsed as the application spine @x y@; this returns
-- @[x, y]@ so each can become its own nested binder. A single binder term (a
-- variable, a pair pattern, …) is returned unchanged as a singleton.
flattenBinderApp :: Rzk.Term -> [Rzk.Term]
flattenBinderApp :: Term -> [Term]
flattenBinderApp = \case
  Rzk.App BNFC'Position
_loc Term
f Term
x -> Term -> [Term]
flattenBinderApp Term
f [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
x]
  Term
t                -> [Term
t]

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)
      Rzk.Tuple a
loc Term' a
t1 Term' a
t2 [Term' a]
ts              -> a -> Pattern' a -> Pattern' a -> [Pattern' a] -> Pattern' a
forall a.
a -> Pattern' a -> Pattern' a -> [Pattern' a] -> Pattern' a
Rzk.PatternTuple a
loc (Term' a -> Pattern' a
ttp Term' a
t1) (Term' a -> Pattern' a
ttp Term' a
t2) ((Term' a -> Pattern' a) -> [Term' a] -> [Pattern' a]
forall a b. (a -> b) -> [a] -> [b]
map Term' a -> Pattern' a
ttp [Term' a]
ts)
      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)

sigmaParamToTypeSigma :: Rzk.BNFC'Position -> Rzk.SigmaParam -> Rzk.Term -> Rzk.Term
sigmaParamToTypeSigma :: BNFC'Position -> SigmaParam' BNFC'Position -> Term -> Term
sigmaParamToTypeSigma BNFC'Position
loc SigmaParam' BNFC'Position
sp Term
body = case SigmaParam' BNFC'Position
sp of
  Rzk.SigmaParam      BNFC'Position
_ Pattern
pat Term
ty      -> 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
body
  Rzk.SigmaParamModal BNFC'Position
_ Pattern
pat ModalColon' BNFC'Position
mc Term
ty  -> BNFC'Position
-> Pattern -> ModalColon' BNFC'Position -> Term -> Term -> Term
forall a.
a -> Pattern' a -> ModalColon' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigmaModal BNFC'Position
loc Pattern
pat ModalColon' BNFC'Position
mc Term
ty Term
body

-- | A projection step: first (@π₁@) or second (@π₂@) component.
data Proj = PFst | PSnd
  deriving (Proj -> Proj -> Bool
(Proj -> Proj -> Bool) -> (Proj -> Proj -> Bool) -> Eq Proj
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Proj -> Proj -> Bool
== :: Proj -> Proj -> Bool
$c/= :: Proj -> Proj -> Bool
/= :: Proj -> Proj -> Bool
Eq)

-- | Render a 'Binder' as a surface pattern (used to display the binder itself,
-- e.g. @(t , s)@). Anonymous variables become @_@.
binderToPattern :: Binder -> Rzk.Pattern
binderToPattern :: Binder -> Pattern
binderToPattern (BinderVar Maybe VarIdent
Nothing)  = BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
forall a. Maybe a
Nothing (VarIdent -> VarIdent
fromVarIdent VarIdent
"_")
binderToPattern (BinderVar (Just VarIdent
x)) = BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
forall a. Maybe a
Nothing (VarIdent -> VarIdent
fromVarIdent VarIdent
x)
binderToPattern (BinderPair Binder
l Binder
r)     = BNFC'Position -> Pattern -> Pattern -> Pattern
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair BNFC'Position
forall a. Maybe a
Nothing (Binder -> Pattern
binderToPattern Binder
l) (Binder -> Pattern
binderToPattern Binder
r)
binderToPattern Binder
BinderUnit           = BNFC'Position -> Pattern
forall a. a -> Pattern' a
Rzk.PatternUnit BNFC'Position
forall a. Maybe a
Nothing

-- | A term that prints as the binder's surface pattern, e.g. the point
-- @(t , s)@. Used to render a /bare/ occurrence of a pattern binder's variable
-- (one not under a projection, e.g. the point in a shape tope @Δ² (t , s)@) as
-- the pattern itself rather than the underlying single variable. A
-- single-variable binder yields that variable.
binderToTerm :: Binder -> Term VarIdent
binderToTerm :: Binder -> Term'
binderToTerm (BinderVar Maybe VarIdent
Nothing)  = VarIdent -> Term'
forall (t :: * -> * -> *) a. a -> FS t a
Pure ([Char] -> VarIdent
forall a. IsString a => [Char] -> a
fromString [Char]
"_")
binderToTerm (BinderVar (Just VarIdent
x)) = VarIdent -> Term'
forall (t :: * -> * -> *) a. a -> FS t a
Pure VarIdent
x
binderToTerm (BinderPair Binder
l Binder
r)     = Term' -> Term' -> Term'
forall {a}. FS TermF a -> FS TermF a -> FS TermF a
Pair (Binder -> Term'
binderToTerm Binder
l) (Binder -> Term'
binderToTerm Binder
r)
binderToTerm Binder
BinderUnit           = Term'
forall {a}. FS TermF a
Unit

-- | A 'VarIdent' that prints as the binder's surface pattern, e.g. @(t , s)@.
-- Used to display a pattern binder in a hole's local context as the pattern
-- itself rather than as the underlying single variable.
binderDisplayName :: Binder -> VarIdent
binderDisplayName :: Binder -> VarIdent
binderDisplayName = [Char] -> VarIdent
forall a. IsString a => [Char] -> a
fromString ([Char] -> VarIdent) -> (Binder -> [Char]) -> Binder -> VarIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree (Pattern -> [Char]) -> (Binder -> Pattern) -> Binder -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> Pattern
binderToPattern

-- | The named leaves of a binder, each paired with the projection path that
-- reaches it from the bound variable. For example @(t , (a , b))@ yields
-- @[([PFst], t), ([PSnd, PFst], a), ([PSnd, PSnd], b)]@.
binderPaths :: Binder -> [([Proj], VarIdent)]
binderPaths :: Binder -> [([Proj], VarIdent)]
binderPaths (BinderVar (Just VarIdent
x)) = [([], VarIdent
x)]
binderPaths (BinderVar Maybe VarIdent
Nothing)  = []
binderPaths Binder
BinderUnit           = []
binderPaths (BinderPair Binder
l Binder
r)     =
  [ (Proj
PFst Proj -> [Proj] -> [Proj]
forall a. a -> [a] -> [a]
: [Proj]
p, VarIdent
n) | ([Proj]
p, VarIdent
n) <- Binder -> [([Proj], VarIdent)]
binderPaths Binder
l ] [([Proj], VarIdent)]
-> [([Proj], VarIdent)] -> [([Proj], VarIdent)]
forall a. [a] -> [a] -> [a]
++
  [ (Proj
PSnd Proj -> [Proj] -> [Proj]
forall a. a -> [a] -> [a]
: [Proj]
p, VarIdent
n) | ([Proj]
p, VarIdent
n) <- Binder -> [([Proj], VarIdent)]
binderPaths Binder
r ]

-- | The names appearing in a binder.
binderLeaves :: Binder -> [VarIdent]
binderLeaves :: Binder -> [VarIdent]
binderLeaves = (([Proj], VarIdent) -> VarIdent)
-> [([Proj], VarIdent)] -> [VarIdent]
forall a b. (a -> b) -> [a] -> [b]
map ([Proj], VarIdent) -> VarIdent
forall a b. (a, b) -> b
snd ([([Proj], VarIdent)] -> [VarIdent])
-> (Binder -> [([Proj], VarIdent)]) -> Binder -> [VarIdent]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> [([Proj], VarIdent)]
binderPaths

-- | Does this binder destructure a pair\/tuple (as opposed to naming a single
-- variable or @_@)?
binderIsCompound :: Binder -> Bool
binderIsCompound :: Binder -> Bool
binderIsCompound BinderVar{} = Bool
False
binderIsCompound Binder
_           = Bool
True

-- | Refresh the named leaves of a binder so they avoid the given names (and one
-- another). Anonymous leaves and the unit pattern are left unchanged.
freshenBinderLeaves :: [VarIdent] -> Binder -> Binder
freshenBinderLeaves :: [VarIdent] -> Binder -> Binder
freshenBinderLeaves [VarIdent]
used = ([VarIdent], Binder) -> Binder
forall a b. (a, b) -> b
snd (([VarIdent], Binder) -> Binder)
-> (Binder -> ([VarIdent], Binder)) -> Binder -> Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VarIdent] -> Binder -> ([VarIdent], Binder)
go [VarIdent]
used
  where
    go :: [VarIdent] -> Binder -> ([VarIdent], Binder)
go [VarIdent]
u (BinderVar (Just VarIdent
x)) = let x' :: VarIdent
x' = [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
u VarIdent
x in (VarIdent
x' VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
u, Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x'))
    go [VarIdent]
u b :: Binder
b@(BinderVar Maybe VarIdent
Nothing) = ([VarIdent]
u, Binder
b)
    go [VarIdent]
u Binder
BinderUnit            = ([VarIdent]
u, Binder
BinderUnit)
    go [VarIdent]
u (BinderPair Binder
l Binder
r)      =
      let ([VarIdent]
u1, Binder
l') = [VarIdent] -> Binder -> ([VarIdent], Binder)
go [VarIdent]
u Binder
l
          ([VarIdent]
u2, Binder
r') = [VarIdent] -> Binder -> ([VarIdent], Binder)
go [VarIdent]
u1 Binder
r
      in ([VarIdent]
u2, Binder -> Binder -> Binder
BinderPair Binder
l' Binder
r')

-- | Decompose a chain of projections applied to a variable into the projection
-- path /from the variable outwards/, matching 'binderPaths'. The outermost
-- projection is applied last, so it goes at the /end/ of the path: e.g.
-- @π₂ (π₁ x)@ (select @π₁@ first, then @π₂@) becomes @Just ([PFst, PSnd], x)@.
projChain :: Term a -> Maybe ([Proj], a)
projChain :: forall a. Term a -> Maybe ([Proj], a)
projChain (First FS TermF a
t)  = (\([Proj]
ps, a
r) -> ([Proj]
ps [Proj] -> [Proj] -> [Proj]
forall a. [a] -> [a] -> [a]
++ [Proj
PFst], a
r)) (([Proj], a) -> ([Proj], a))
-> Maybe ([Proj], a) -> Maybe ([Proj], a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FS TermF a -> Maybe ([Proj], a)
forall a. Term a -> Maybe ([Proj], a)
projChain FS TermF a
t
projChain (Second FS TermF a
t) = (\([Proj]
ps, a
r) -> ([Proj]
ps [Proj] -> [Proj] -> [Proj]
forall a. [a] -> [a] -> [a]
++ [Proj
PSnd], a
r)) (([Proj], a) -> ([Proj], a))
-> Maybe ([Proj], a) -> Maybe ([Proj], a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FS TermF a -> Maybe ([Proj], a)
forall a. Term a -> Maybe ([Proj], a)
projChain FS TermF a
t
projChain (Pure a
x)   = ([Proj], a) -> Maybe ([Proj], a)
forall a. a -> Maybe a
Just ([], a
x)
projChain FS TermF a
_          = Maybe ([Proj], a)
forall a. Maybe a
Nothing

-- | Replace projection chains rooted at a pattern binder with the binder's
-- component name. Given a map from a (bound) variable to the named leaves of
-- its binder, every @π₁/π₂@ chain that reaches a named leaf is rewritten to
-- that name. Ordinary projections (of variables not bound by a pattern, or
-- chains that do not reach a named leaf) are left untouched.
foldBinderProjections :: Eq a => [(a, [([Proj], a)])] -> Term a -> Term a
foldBinderProjections :: forall a. Eq a => [(a, [([Proj], a)])] -> Term a -> Term a
foldBinderProjections [(a, [([Proj], a)])]
m = FS TermF a -> FS TermF a
go
  where
    go :: FS TermF a -> FS TermF a
go FS TermF a
t
      | Just ([Proj]
ps, a
root) <- FS TermF a -> Maybe ([Proj], a)
forall a. Term a -> Maybe ([Proj], a)
projChain FS TermF a
t
      , Bool -> Bool
not ([Proj] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Proj]
ps)
      , Just [([Proj], a)]
leaves <- a -> [(a, [([Proj], a)])] -> Maybe [([Proj], a)]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
root [(a, [([Proj], a)])]
m
      , Just a
nm <- [Proj] -> [([Proj], a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Proj]
ps [([Proj], a)]
leaves
      = a -> FS TermF a
forall (t :: * -> * -> *) a. a -> FS t a
Pure a
nm
    go (Free TermF (Scope (FS TermF) a) (FS TermF a)
f) = TermF (Scope (FS TermF) a) (FS TermF a) -> FS TermF a
forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free ((Scope (FS TermF) a -> Scope (FS TermF) a)
-> (FS TermF a -> FS TermF a)
-> TermF (Scope (FS TermF) a) (FS TermF a)
-> TermF (Scope (FS TermF) a) (FS TermF a)
forall a b c d. (a -> b) -> (c -> d) -> TermF a c -> TermF b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Scope (FS TermF) a -> Scope (FS TermF) a
goScope FS TermF a -> FS TermF a
go TermF (Scope (FS TermF) a) (FS TermF a)
f)
    go (Pure a
x) = a -> FS TermF a
forall (t :: * -> * -> *) a. a -> FS t a
Pure a
x
    goScope :: Scope (FS TermF) a -> Scope (FS TermF) a
goScope = [(Inc a, [([Proj], Inc a)])]
-> Scope (FS TermF) a -> Scope (FS TermF) a
forall a. Eq a => [(a, [([Proj], a)])] -> Term a -> Term a
foldBinderProjections (((a, [([Proj], a)]) -> (Inc a, [([Proj], Inc a)]))
-> [(a, [([Proj], a)])] -> [(Inc a, [([Proj], Inc a)])]
forall a b. (a -> b) -> [a] -> [b]
map (a, [([Proj], a)]) -> (Inc a, [([Proj], Inc a)])
forall {f :: * -> *} {var} {a}.
Functor f =>
(var, [f a]) -> (Inc var, [f (Inc a)])
liftEntry [(a, [([Proj], a)])]
m)
    liftEntry :: (var, [f a]) -> (Inc var, [f (Inc a)])
liftEntry (var
k, [f a]
leaves) = (var -> Inc var
forall var. var -> Inc var
S var
k, (f a -> f (Inc a)) -> [f a] -> [f (Inc a)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Inc a) -> f a -> f (Inc a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Inc a
forall var. var -> Inc var
S) [f a]
leaves)

-- | Replace bare uses of a pattern binder's variable with the pattern term
-- (e.g. a whole point @(t , s)@ rather than the underlying single variable, in
-- a tope @Δ² (t , s)@). Given a map from each (already display-named) variable
-- to its binder, every free occurrence of a /compound/ binder's variable is
-- expanded to its pattern. Complements 'foldBinderProjections', which folds
-- /projections/ of such a variable; run this /after/ folding, so projections
-- have already become component names and only bare uses remain.
restorePatternVars :: [(VarIdent, Binder)] -> Term VarIdent -> Term VarIdent
restorePatternVars :: [(VarIdent, Binder)] -> Term' -> Term'
restorePatternVars [(VarIdent, Binder)]
binders = (Term' -> (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
>>= VarIdent -> Term'
expand)
  where
    expand :: VarIdent -> Term'
expand VarIdent
v = case VarIdent -> [(VarIdent, Binder)] -> Maybe Binder
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VarIdent
v [(VarIdent, Binder)]
binders of
      Just Binder
b | Binder -> Bool
binderIsCompound Binder
b -> Binder -> Term'
binderToTerm Binder
b
      Maybe Binder
_                           -> VarIdent -> Term'
forall (t :: * -> * -> *) a. a -> FS t a
Pure VarIdent
v

-- | Like 'projChain', but for type-annotated terms.
projChainT :: TermT a -> Maybe ([Proj], a)
projChainT :: forall a. TermT a -> Maybe ([Proj], a)
projChainT (FirstT TypeInfo (FS (AnnF TypeInfo TermF) a)
_ FS (AnnF TypeInfo TermF) a
t)  = (\([Proj]
ps, a
r) -> ([Proj]
ps [Proj] -> [Proj] -> [Proj]
forall a. [a] -> [a] -> [a]
++ [Proj
PFst], a
r)) (([Proj], a) -> ([Proj], a))
-> Maybe ([Proj], a) -> Maybe ([Proj], a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FS (AnnF TypeInfo TermF) a -> Maybe ([Proj], a)
forall a. TermT a -> Maybe ([Proj], a)
projChainT FS (AnnF TypeInfo TermF) a
t
projChainT (SecondT TypeInfo (FS (AnnF TypeInfo TermF) a)
_ FS (AnnF TypeInfo TermF) a
t) = (\([Proj]
ps, a
r) -> ([Proj]
ps [Proj] -> [Proj] -> [Proj]
forall a. [a] -> [a] -> [a]
++ [Proj
PSnd], a
r)) (([Proj], a) -> ([Proj], a))
-> Maybe ([Proj], a) -> Maybe ([Proj], a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FS (AnnF TypeInfo TermF) a -> Maybe ([Proj], a)
forall a. TermT a -> Maybe ([Proj], a)
projChainT FS (AnnF TypeInfo TermF) a
t
projChainT (Pure a
x)      = ([Proj], a) -> Maybe ([Proj], a)
forall a. a -> Maybe a
Just ([], a
x)
projChainT FS (AnnF TypeInfo TermF) a
_             = Maybe ([Proj], a)
forall a. Maybe a
Nothing

-- | Like 'foldBinderProjections', but for type-annotated terms (e.g. those
-- embedded in type errors). The annotation of a folded leaf is dropped, which
-- is harmless: the result is only rendered, and a bare variable needs none.
foldBinderProjectionsT :: Eq a => [(a, [([Proj], a)])] -> TermT a -> TermT a
foldBinderProjectionsT :: forall a. Eq a => [(a, [([Proj], a)])] -> TermT a -> TermT a
foldBinderProjectionsT [(a, [([Proj], a)])]
m = FS (AnnF TypeInfo TermF) a -> FS (AnnF TypeInfo TermF) a
go
  where
    go :: FS (AnnF TypeInfo TermF) a -> FS (AnnF TypeInfo TermF) a
go FS (AnnF TypeInfo TermF) a
t
      | Just ([Proj]
ps, a
root) <- FS (AnnF TypeInfo TermF) a -> Maybe ([Proj], a)
forall a. TermT a -> Maybe ([Proj], a)
projChainT FS (AnnF TypeInfo TermF) a
t
      , Bool -> Bool
not ([Proj] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Proj]
ps)
      , Just [([Proj], a)]
leaves <- a -> [(a, [([Proj], a)])] -> Maybe [([Proj], a)]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
root [(a, [([Proj], a)])]
m
      , Just a
nm <- [Proj] -> [([Proj], a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Proj]
ps [([Proj], a)]
leaves
      = a -> FS (AnnF TypeInfo TermF) a
forall (t :: * -> * -> *) a. a -> FS t a
Pure a
nm
    go (Free (AnnF TypeInfo (FS (AnnF TypeInfo TermF) a)
info TermF
  (Scope (FS (AnnF TypeInfo TermF)) a) (FS (AnnF TypeInfo TermF) a)
f)) = AnnF
  TypeInfo
  TermF
  (Scope (FS (AnnF TypeInfo TermF)) a)
  (FS (AnnF TypeInfo TermF) a)
-> FS (AnnF TypeInfo TermF) a
forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free (TypeInfo (FS (AnnF TypeInfo TermF) a)
-> TermF
     (Scope (FS (AnnF TypeInfo TermF)) a) (FS (AnnF TypeInfo TermF) a)
-> AnnF
     TypeInfo
     TermF
     (Scope (FS (AnnF TypeInfo TermF)) a)
     (FS (AnnF TypeInfo TermF) a)
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF ((FS (AnnF TypeInfo TermF) a -> FS (AnnF TypeInfo TermF) a)
-> TypeInfo (FS (AnnF TypeInfo TermF) a)
-> TypeInfo (FS (AnnF TypeInfo TermF) a)
forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FS (AnnF TypeInfo TermF) a -> FS (AnnF TypeInfo TermF) a
go TypeInfo (FS (AnnF TypeInfo TermF) a)
info) ((Scope (FS (AnnF TypeInfo TermF)) a
 -> Scope (FS (AnnF TypeInfo TermF)) a)
-> (FS (AnnF TypeInfo TermF) a -> FS (AnnF TypeInfo TermF) a)
-> TermF
     (Scope (FS (AnnF TypeInfo TermF)) a) (FS (AnnF TypeInfo TermF) a)
-> TermF
     (Scope (FS (AnnF TypeInfo TermF)) a) (FS (AnnF TypeInfo TermF) a)
forall a b c d. (a -> b) -> (c -> d) -> TermF a c -> TermF b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Scope (FS (AnnF TypeInfo TermF)) a
-> Scope (FS (AnnF TypeInfo TermF)) a
goScope FS (AnnF TypeInfo TermF) a -> FS (AnnF TypeInfo TermF) a
go TermF
  (Scope (FS (AnnF TypeInfo TermF)) a) (FS (AnnF TypeInfo TermF) a)
f))
    go (Pure a
x) = a -> FS (AnnF TypeInfo TermF) a
forall (t :: * -> * -> *) a. a -> FS t a
Pure a
x
    goScope :: Scope (FS (AnnF TypeInfo TermF)) a
-> Scope (FS (AnnF TypeInfo TermF)) a
goScope = [(Inc a, [([Proj], Inc a)])]
-> Scope (FS (AnnF TypeInfo TermF)) a
-> Scope (FS (AnnF TypeInfo TermF)) a
forall a. Eq a => [(a, [([Proj], a)])] -> TermT a -> TermT a
foldBinderProjectionsT (((a, [([Proj], a)]) -> (Inc a, [([Proj], Inc a)]))
-> [(a, [([Proj], a)])] -> [(Inc a, [([Proj], Inc a)])]
forall a b. (a -> b) -> [a] -> [b]
map (a, [([Proj], a)]) -> (Inc a, [([Proj], Inc a)])
forall {f :: * -> *} {var} {a}.
Functor f =>
(var, [f a]) -> (Inc var, [f (Inc a)])
liftEntry [(a, [([Proj], a)])]
m)
    liftEntry :: (var, [f a]) -> (Inc var, [f (Inc a)])
liftEntry (var
k, [f a]
leaves) = (var -> Inc var
forall var. var -> Inc var
S var
k, (f a -> f (Inc a)) -> [f a] -> [f (Inc a)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Inc a) -> f a -> f (Inc a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Inc a
forall var. var -> Inc var
S) [f a]
leaves)

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

-- | Like 'fromScope'', but additionally restores pattern-binder component names
-- inside the scope: projections of the bound variable @x@ are folded back to
-- the names recorded in @binder@ (e.g. @π₁ x@ becomes @t@). For a binder that
-- names a single variable this is exactly 'fromScope''.
fromScopeBinder' :: Binder -> VarIdent -> [VarIdent] -> [VarIdent] -> Scope Term VarIdent -> Rzk.Term
fromScopeBinder' :: Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
binder VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope =
  [VarIdent] -> [VarIdent] -> Term' -> Term
fromTermWith' (VarIdent
x VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
used) [VarIdent]
xs
    (Term' -> Term'
restorePattern ([(VarIdent, [([Proj], VarIdent)])] -> Term' -> Term'
forall a. Eq a => [(a, [([Proj], a)])] -> Term a -> Term a
foldBinderProjections [(VarIdent
x, Binder -> [([Proj], VarIdent)]
binderPaths Binder
binder)] (Scope (FS TermF) VarIdent
scope 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
    -- After projection chains have been folded to their component names, a bare
    -- use of a pattern binder's variable (the whole point, e.g. in a shape tope
    -- @Δ² (t , s)@) still reads as the placeholder; show it as the pattern.
    restorePattern :: Term' -> Term'
restorePattern
      | Binder -> Bool
binderIsCompound Binder
binder = (Term' -> (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
>>= \VarIdent
v -> if VarIdent
v VarIdent -> VarIdent -> Bool
forall a. Eq a => a -> a -> Bool
== VarIdent
x then Binder -> Term'
binderToTerm Binder
binder else VarIdent -> Term'
forall (t :: * -> * -> *) a. a -> FS t a
Pure VarIdent
v)
      | Bool
otherwise               = Term' -> Term'
forall a. a -> a
id

fromTermWith' :: [VarIdent] -> [VarIdent] -> Term' -> Rzk.Term
fromTermWith' :: [VarIdent] -> [VarIdent] -> Term' -> Term
fromTermWith' [VarIdent]
used [VarIdent]
vars = Term' -> Term
go
  where
    -- Refresh a binder's named leaves against the names already in use and draw
    -- fresh names for anonymous leaves from the remaining supply.
    freshenBinder :: [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder [VarIdent]
_    [VarIdent]
stream (BinderVar Maybe VarIdent
Nothing) =
      case [VarIdent]
stream of
        VarIdent
x:[VarIdent]
xs -> (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x), [VarIdent]
xs)
        [VarIdent]
_    -> [Char] -> (Binder, [VarIdent])
forall a. HasCallStack => [Char] -> a
error [Char]
"not enough fresh variables!"
    freshenBinder [VarIdent]
used' [VarIdent]
stream (BinderVar (Just VarIdent
z)) =
      (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just 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]
stream)
      where z' :: VarIdent
z' = [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
used' VarIdent
z
    freshenBinder [VarIdent]
_    [VarIdent]
stream Binder
BinderUnit = (Binder
BinderUnit, [VarIdent]
stream)
    freshenBinder [VarIdent]
used' [VarIdent]
stream (BinderPair Binder
l Binder
r) =
      let (Binder
l', [VarIdent]
s1) = [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder [VarIdent]
used' [VarIdent]
stream Binder
l
          (Binder
r', [VarIdent]
s2) = [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder ([VarIdent]
used' [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. [a] -> [a] -> [a]
++ Binder -> [VarIdent]
binderLeaves Binder
l') [VarIdent]
s1 Binder
r
      in (Binder -> Binder -> Binder
BinderPair Binder
l' Binder
r', [VarIdent]
s2)

    -- Pick fresh names for a binder. Yields the bound variable's display name
    -- (used as the De Bruijn placeholder), the freshened binder (for the
    -- displayed pattern and for projection folding), and the remaining supply.
    withFreshBinder :: Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (VarIdent, Binder, [VarIdent]) -> t
f =
      case Binder
binder' of
        BinderVar (Just VarIdent
x) -> (VarIdent, Binder, [VarIdent]) -> t
f (VarIdent
x, Binder
binder', [VarIdent]
stream)
        Binder
_ -> case [VarIdent]
stream of
               VarIdent
x:[VarIdent]
xs -> (VarIdent, Binder, [VarIdent]) -> t
f (VarIdent
x, Binder
binder', [VarIdent]
xs)
               [VarIdent]
_    -> [Char] -> t
forall a. HasCallStack => [Char] -> a
error [Char]
"not enough fresh variables!"
      where
        (Binder
binder', [VarIdent]
stream) = [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder [VarIdent]
used [VarIdent]
vars Binder
z

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

    goMod :: TModality -> Rzk.Modality  
    goMod :: TModality -> Modality
goMod TModality
Sharp = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Sharp BNFC'Position
forall a. Maybe a
loc
    goMod TModality
Flat = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Flat BNFC'Position
forall a. Maybe a
loc 
    goMod TModality
Op = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Op BNFC'Position
forall a. Maybe a
loc
    goMod TModality
Id = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Id BNFC'Position
forall a. Maybe a
loc 


    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
      Term'
CubeI -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI BNFC'Position
forall a. Maybe a
loc
      Term'
CubeI_0 -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI_0 BNFC'Position
forall a. Maybe a
loc
      Term'
CubeI_1 -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI_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)
      TopeInv Term'
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.TopeInv BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
t)
      TopeUninv Term'
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.TopeUninv BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
t)
      CubeFlip Term'
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.CubeFlip BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
t)
      CubeUnflip Term'
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.CubeUnflip BNFC'Position
forall a. Maybe a
loc (Term' -> Term
go Term'
t)
      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 ]

      Hole Maybe VarIdent
mname -> BNFC'Position -> HoleIdent' BNFC'Position -> Term
forall a. a -> HoleIdent' a -> Term' a
Rzk.Hole BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> HoleIdentToken -> HoleIdent' BNFC'Position
forall a. a -> HoleIdentToken -> HoleIdent' a
Rzk.HoleIdent BNFC'Position
forall a. Maybe a
loc (Text -> HoleIdentToken
Rzk.HoleIdentToken (Maybe VarIdent -> Text
holeIdentToken Maybe VarIdent
mname)))

      TypeFun Binder
z TModality
Id Term'
arg Maybe (Scope (FS TermF) VarIdent)
Nothing Scope (FS TermF) VarIdent
ret -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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 (Pattern -> Term
patternToTerm (Binder -> Pattern
binderToPattern Binder
z')) (Term' -> Term
go Term'
arg)) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
ret)
      TypeFun Binder
z TModality
Id Term'
arg (Just Scope (FS TermF) VarIdent
tope) Scope (FS TermF) VarIdent
ret -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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 (Pattern -> Term
patternToTerm (Binder -> Pattern
binderToPattern Binder
z')) (Term' -> Term
go Term'
arg) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
tope)) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
ret)
      TypeFun Binder
z TModality
md Term'
arg Maybe (Scope (FS TermF) VarIdent)
Nothing Scope (FS TermF) VarIdent
ret -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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
-> ModalColon' BNFC'Position
-> Term
-> ParamDecl' BNFC'Position
forall a. a -> Term' a -> ModalColon' a -> Term' a -> ParamDecl' a
Rzk.ParamTermModalType BNFC'Position
forall a. Maybe a
loc (Pattern -> Term
patternToTerm (Binder -> Pattern
binderToPattern Binder
z')) (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term' -> Term
go Term'
arg)) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
ret)
      TypeFun Binder
z TModality
md Term'
arg (Just Scope (FS TermF) VarIdent
tope) Scope (FS TermF) VarIdent
ret -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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
-> ModalColon' BNFC'Position
-> Term
-> Term
-> ParamDecl' BNFC'Position
forall a.
a -> Term' a -> ModalColon' a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermModalShape BNFC'Position
forall a. Maybe a
loc (Pattern -> Term
patternToTerm (Binder -> Pattern
binderToPattern Binder
z')) (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term' -> Term
go Term'
arg) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
tope)) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
ret)

      TypeSigma Binder
z TModality
Id Term'
a Scope (FS TermF) VarIdent
b -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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 (Binder -> Pattern
binderToPattern Binder
z') (Term' -> Term
go Term'
a) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
b)
      TypeSigma Binder
z TModality
md Term'
a Scope (FS TermF) VarIdent
b -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [VarIdent]
xs) ->
        BNFC'Position
-> Pattern -> ModalColon' BNFC'Position -> Term -> Term -> Term
forall a.
a -> Pattern' a -> ModalColon' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigmaModal BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z') (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term' -> Term
go Term'
a) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' 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 Binder
z Maybe (TModality, Term', Maybe (Scope (FS TermF) VarIdent))
Nothing Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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 (Binder -> Pattern
binderToPattern Binder
z')] (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      Lambda Binder
z (Just (TModality
Id, Term'
ty, Maybe (Scope (FS TermF) VarIdent)
Nothing)) Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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 [Binder -> Pattern
binderToPattern Binder
z'] (Term' -> Term
go Term'
ty)] (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      Lambda Binder
z (Just (TModality
Id, Term'
cube, Just Scope (FS TermF) VarIdent
tope)) Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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 [Binder -> Pattern
binderToPattern Binder
z'] (Term' -> Term
go Term'
cube) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
tope)] (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      Lambda Binder
z (Just (TModality
md, Term'
ty, Maybe (Scope (FS TermF) VarIdent)
Nothing)) Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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]
-> ModalColon' BNFC'Position
-> Term
-> Param' BNFC'Position
forall a. a -> [Pattern' a] -> ModalColon' a -> Term' a -> Param' a
Rzk.ParamPatternModalType BNFC'Position
forall a. Maybe a
loc [Binder -> Pattern
binderToPattern Binder
z'] (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term' -> Term
go Term'
ty)] (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      Lambda Binder
z (Just (TModality
md, Term'
cube, Just Scope (FS TermF) VarIdent
tope)) Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [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]
-> ModalColon' BNFC'Position
-> Term
-> Term
-> Param' BNFC'Position
forall a.
a
-> [Pattern' a] -> ModalColon' a -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternModalShape BNFC'Position
forall a. Maybe a
loc [Binder -> Pattern
binderToPattern Binder
z'] (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term' -> Term
go Term'
cube) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
tope)] (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' 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
      Let Binder
z Maybe Term'
Nothing Term'
val Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [VarIdent]
xs) ->
        BNFC'Position -> Bind' BNFC'Position -> Term -> Term -> Term
forall a. a -> Bind' a -> Term' a -> Term' a -> Term' a
Rzk.Let BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Pattern -> Bind' BNFC'Position
forall a. a -> Pattern' a -> Bind' a
Rzk.BindPattern BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z')) (Term' -> Term
go Term'
val) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      Let Binder
z (Just Term'
ty) Term'
val Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [VarIdent]
xs) ->
        BNFC'Position -> Bind' BNFC'Position -> Term -> Term -> Term
forall a. a -> Bind' a -> Term' a -> Term' a -> Term' a
Rzk.Let BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Pattern -> Term -> Bind' BNFC'Position
forall a. a -> Pattern' a -> Term' a -> Bind' a
Rzk.BindPatternType BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z') (Term' -> Term
go Term'
ty)) (Term' -> Term
go Term'
val) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
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)
      TypeModal TModality
m Term'
ty -> BNFC'Position -> Modality -> Term -> Term
forall a. a -> Modality' a -> Term' a -> Term' a
Rzk.ModType BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
m) (Term' -> Term
go Term'
ty)
      ModApp TModality
m Term'
ty -> BNFC'Position -> Modality -> Term -> Term
forall a. a -> Modality' a -> Term' a -> Term' a
Rzk.ModApp BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
m) (Term' -> Term
go Term'
ty)
      ModExtract TModality
ma TModality
mb Term'
t -> BNFC'Position -> ModComp -> Term -> Term
forall a. a -> ModComp' a -> Term' a -> Term' a
Rzk.ModExtract BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Modality -> Modality -> ModComp
forall a. a -> Modality' a -> Modality' a -> ModComp' a
Rzk.Comp BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
ma) (TModality -> Modality
goMod TModality
mb)) (Term' -> Term
go Term'
t)
      LetMod Binder
z TModality
ext TModality
inn Maybe Term'
Nothing Term'
val Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [VarIdent]
xs) ->
        BNFC'Position
-> ModComp -> Bind' BNFC'Position -> Term -> Term -> Term
forall a.
a -> ModComp' a -> Bind' a -> Term' a -> Term' a -> Term' a
Rzk.LetMod BNFC'Position
forall a. Maybe a
loc (TModality -> TModality -> ModComp
modsToModComp TModality
ext TModality
inn)
          (BNFC'Position -> Pattern -> Bind' BNFC'Position
forall a. a -> Pattern' a -> Bind' a
Rzk.BindPattern BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z'))
          (Term' -> Term
go Term'
val) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)
      LetMod Binder
z TModality
ext TModality
inn (Just Term'
ty) Term'
val Scope (FS TermF) VarIdent
scope -> Binder -> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall {t}. Binder -> ((VarIdent, Binder, [VarIdent]) -> t) -> t
withFreshBinder Binder
z (((VarIdent, Binder, [VarIdent]) -> Term) -> Term)
-> ((VarIdent, Binder, [VarIdent]) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(VarIdent
x, Binder
z', [VarIdent]
xs) ->
        BNFC'Position
-> ModComp -> Bind' BNFC'Position -> Term -> Term -> Term
forall a.
a -> ModComp' a -> Bind' a -> Term' a -> Term' a -> Term' a
Rzk.LetMod BNFC'Position
forall a. Maybe a
loc (TModality -> TModality -> ModComp
modsToModComp TModality
ext TModality
inn)
          (BNFC'Position -> Pattern -> Term -> Bind' BNFC'Position
forall a. a -> Pattern' a -> Term' a -> Bind' a
Rzk.BindPatternType BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z') (Term' -> Term
go Term'
ty))
          (Term' -> Term
go Term'
val) (Binder
-> VarIdent
-> [VarIdent]
-> [VarIdent]
-> Scope (FS TermF) VarIdent
-> Term
fromScopeBinder' Binder
z' VarIdent
x [VarIdent]
used [VarIdent]
xs Scope (FS TermF) VarIdent
scope)


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
'₀')

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> import qualified Data.Text as T

-- | 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 ((Text -> Text) -> VarIdentToken -> VarIdentToken
forall a b. Coercible a b => a -> b
coerce Text -> Text
incIndex VarIdentToken
token))

-- | Increment the subscript number at the end of the indentifier.
--
-- >>> putStrLn $ T.unpack $ incIndex "x"
-- x₁
-- >>> putStrLn $ T.unpack $ incIndex "x₁₉"
-- x₂₀
incIndex :: T.Text -> T.Text
incIndex :: Text -> Text
incIndex Text
s = [Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [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 (Text -> [Char]
T.unpack Text
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 Text Term -> Term
forall {a}. Either Text a -> a
fromRight (Either Text Term -> Term)
-> ([Char] -> Either Text Term) -> [Char] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either Text Term
Rzk.parseTerm (Text -> Either Text Term)
-> ([Char] -> Text) -> [Char] -> Either Text Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Text
T.pack
    where
      fromRight :: Either Text a -> a
fromRight (Left Text
err) = [Char] -> a
forall a. HasCallStack => [Char] -> a
error (Text -> [Char]
T.unpack (Text -> [Char]) -> Text -> [Char]
forall a b. (a -> b) -> a -> b
$ Text
"Parse error: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
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))