{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures -fno-warn-missing-signatures -fno-warn-type-defaults #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeSynonymInstances    #-}
{-# LANGUAGE FlexibleInstances    #-}
module Language.Rzk.Free.Syntax where

import Data.String
import Data.Char (chr, ord)
import Data.Coerce
import Data.List ((\\))
import Data.Bifunctor.TH

import Free.Scoped
import Free.Scoped.TH

import qualified Language.Rzk.Syntax as Rzk

data TermF scope term
    = UniverseF
    | UniverseCubeF
    | UniverseTopeF
    | CubeUnitF
    | CubeUnitStarF
    | Cube2F
    | Cube2_0F
    | Cube2_1F
    | CubeProductF term term
    | TopeTopF
    | TopeBottomF
    | TopeEQF term term
    | TopeLEQF term term
    | TopeAndF term term
    | TopeOrF term term
    | RecBottomF
    | RecOrF [(term, term)]
    | TypeFunF (Maybe Rzk.VarIdent) term (Maybe scope) scope
    | TypeSigmaF (Maybe Rzk.VarIdent) term scope
    | TypeIdF term (Maybe term) term
    | AppF term term
    | LambdaF (Maybe Rzk.VarIdent) (Maybe (term, Maybe scope)) scope
    | PairF term term
    | FirstF term
    | SecondF term
    | ReflF (Maybe (term, Maybe term))
    | IdJF term term term term term term
    | TypeAscF term term
    | TypeRestrictedF term [(term, term)]
    deriving (TermF scope term -> TermF scope term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall scope term.
(Eq term, Eq scope) =>
TermF scope term -> TermF scope term -> Bool
/= :: TermF scope term -> TermF scope term -> Bool
$c/= :: forall scope term.
(Eq term, Eq scope) =>
TermF scope term -> TermF scope term -> Bool
== :: TermF scope term -> TermF scope term -> Bool
$c== :: forall scope term.
(Eq term, Eq scope) =>
TermF scope term -> TermF scope term -> Bool
Eq)
deriveBifunctor ''TermF
deriveBifoldable ''TermF
deriveBitraversable ''TermF
makePatternsAll ''TermF   -- declare all patterns using Template Haskell

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

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

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

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

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

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

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

type Term' = Term Rzk.VarIdent
type TermT' = TermT Rzk.VarIdent

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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