-- The 'ZipMatchK' instances below are orphans: the class is free-foil's and the
-- constant types they cover ('TModality', 'VarIdent', 'Binder') are still the old
-- module's. They come home when the old core goes away.
{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures -fno-warn-orphans #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveFoldable        #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

-- | The core syntax on @free-foil@.
--
-- This is the successor of "Language.Rzk.Free.Syntax"'s @TermF@ \/ @TermT@,
-- built on 'Foil.AST' instead of the vendored @Free.Scoped@. It is compiled but
-- not yet consumed: the checker still runs on the old representation, and the
-- two are swapped over in a later stage.
--
-- Three things carry over unchanged, and are imported rather than duplicated:
-- 'VarIdent' (a surface identifier), 'Binder' (the /names/ a binder introduces,
-- including a pair pattern, which still binds exactly one variable), 'TModality',
-- and 'TypeInfo' (a node's type plus its memoised weak head and normal forms).
--
-- What changes is the variable representation. A binder is a 'Foil.NameBinder',
-- a variable is a 'Foil.Name' (an @Int@), and weakening a term into a larger
-- scope is 'Foil.sink', a coercion rather than a traversal of every node.
module Language.Rzk.Foil.Syntax where

import           Control.Monad.Foil             (NameBinder)
import qualified Control.Monad.Foil             as Foil
import           Control.Monad.Foil.Internal    (Substitution (..),
                                                 unsafeAssertFresh)
import           Control.Monad.Free.Foil        (AST (..), ScopedAST (..),
                                                 alphaEquiv,
                                                 substitute, unsafeEqAST)
import           Data.ZipMatchK                 (Mappings (..),
                                                 ZipMatchK (..),
                                                 zipMatchViaChooseLeft,
                                                 zipMatchViaEq)
import           Control.Monad.Free.Foil.Annotated (AnnSig (..))
import           Data.ZipMatchK.TH              (deriveZipMatchK)
import           Data.Bifoldable                (Bifoldable (..))
import           Data.Bifunctor                 (Bifunctor (..))
import           Data.Bifunctor.TH              (deriveBifoldable,
                                                 deriveBifunctor,
                                                 deriveBitraversable)
import qualified Data.IntMap                    as IntMap
import           Generics.Kind.TH                (deriveGenericK)
import qualified GHC.Generics                   as GHC
import           Unsafe.Coerce                  (unsafeCoerce)

import           Language.Rzk.Foil.Names        (Binder (..), RzkPosition (..),
                                                 TModality (..), TypeInfo (..),
                                                 VarIdent)

-- * The signature
--
-- A transliteration of @TermF@: same constructors, same fields, same order. The
-- @scope@ positions are the ones that bind, and there are eight of them across
-- six constructors ('TypeFunF' and 'LambdaF' each carry a tope scope as well as
-- a body scope, under the same binder).

-- | The optional domain annotation of a λ: its modality, its parameter type,
-- and (for a shape) the tope the parameter is restricted by. It was an anonymous
-- triple in the old signature; the generic machinery needs a named type here, and
-- it reads better anyway.
data LambdaParam scope term = LambdaParam TModality term (Maybe scope)
  deriving (LambdaParam scope term -> LambdaParam scope term -> Bool
(LambdaParam scope term -> LambdaParam scope term -> Bool)
-> (LambdaParam scope term -> LambdaParam scope term -> Bool)
-> Eq (LambdaParam scope term)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall scope term.
(Eq term, Eq scope) =>
LambdaParam scope term -> LambdaParam scope term -> Bool
$c== :: forall scope term.
(Eq term, Eq scope) =>
LambdaParam scope term -> LambdaParam scope term -> Bool
== :: LambdaParam scope term -> LambdaParam scope term -> Bool
$c/= :: forall scope term.
(Eq term, Eq scope) =>
LambdaParam scope term -> LambdaParam scope term -> Bool
/= :: LambdaParam scope term -> LambdaParam scope term -> Bool
Eq, (forall a b.
 (a -> b) -> LambdaParam scope a -> LambdaParam scope b)
-> (forall a b. a -> LambdaParam scope b -> LambdaParam scope a)
-> Functor (LambdaParam scope)
forall a b. a -> LambdaParam scope b -> LambdaParam scope a
forall a b. (a -> b) -> LambdaParam scope a -> LambdaParam scope b
forall scope a b. a -> LambdaParam scope b -> LambdaParam scope a
forall scope a b.
(a -> b) -> LambdaParam scope a -> LambdaParam 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) -> LambdaParam scope a -> LambdaParam scope b
fmap :: forall a b. (a -> b) -> LambdaParam scope a -> LambdaParam scope b
$c<$ :: forall scope a b. a -> LambdaParam scope b -> LambdaParam scope a
<$ :: forall a b. a -> LambdaParam scope b -> LambdaParam scope a
Functor, (forall m. Monoid m => LambdaParam scope m -> m)
-> (forall m a. Monoid m => (a -> m) -> LambdaParam scope a -> m)
-> (forall m a. Monoid m => (a -> m) -> LambdaParam scope a -> m)
-> (forall a b. (a -> b -> b) -> b -> LambdaParam scope a -> b)
-> (forall a b. (a -> b -> b) -> b -> LambdaParam scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> LambdaParam scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> LambdaParam scope a -> b)
-> (forall a. (a -> a -> a) -> LambdaParam scope a -> a)
-> (forall a. (a -> a -> a) -> LambdaParam scope a -> a)
-> (forall a. LambdaParam scope a -> [a])
-> (forall a. LambdaParam scope a -> Bool)
-> (forall a. LambdaParam scope a -> Int)
-> (forall a. Eq a => a -> LambdaParam scope a -> Bool)
-> (forall a. Ord a => LambdaParam scope a -> a)
-> (forall a. Ord a => LambdaParam scope a -> a)
-> (forall a. Num a => LambdaParam scope a -> a)
-> (forall a. Num a => LambdaParam scope a -> a)
-> Foldable (LambdaParam scope)
forall a. Eq a => a -> LambdaParam scope a -> Bool
forall a. Num a => LambdaParam scope a -> a
forall a. Ord a => LambdaParam scope a -> a
forall m. Monoid m => LambdaParam scope m -> m
forall a. LambdaParam scope a -> Bool
forall a. LambdaParam scope a -> Int
forall a. LambdaParam scope a -> [a]
forall a. (a -> a -> a) -> LambdaParam scope a -> a
forall scope a. Eq a => a -> LambdaParam scope a -> Bool
forall scope a. Num a => LambdaParam scope a -> a
forall scope a. Ord a => LambdaParam scope a -> a
forall scope m. Monoid m => LambdaParam scope m -> m
forall m a. Monoid m => (a -> m) -> LambdaParam scope a -> m
forall scope a. LambdaParam scope a -> Bool
forall scope a. LambdaParam scope a -> Int
forall scope a. LambdaParam scope a -> [a]
forall b a. (b -> a -> b) -> b -> LambdaParam scope a -> b
forall a b. (a -> b -> b) -> b -> LambdaParam scope a -> b
forall scope a. (a -> a -> a) -> LambdaParam scope a -> a
forall scope m a. Monoid m => (a -> m) -> LambdaParam scope a -> m
forall scope b a. (b -> a -> b) -> b -> LambdaParam scope a -> b
forall scope a b. (a -> b -> b) -> b -> LambdaParam 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 => LambdaParam scope m -> m
fold :: forall m. Monoid m => LambdaParam scope m -> m
$cfoldMap :: forall scope m a. Monoid m => (a -> m) -> LambdaParam scope a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> LambdaParam scope a -> m
$cfoldMap' :: forall scope m a. Monoid m => (a -> m) -> LambdaParam scope a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> LambdaParam scope a -> m
$cfoldr :: forall scope a b. (a -> b -> b) -> b -> LambdaParam scope a -> b
foldr :: forall a b. (a -> b -> b) -> b -> LambdaParam scope a -> b
$cfoldr' :: forall scope a b. (a -> b -> b) -> b -> LambdaParam scope a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> LambdaParam scope a -> b
$cfoldl :: forall scope b a. (b -> a -> b) -> b -> LambdaParam scope a -> b
foldl :: forall b a. (b -> a -> b) -> b -> LambdaParam scope a -> b
$cfoldl' :: forall scope b a. (b -> a -> b) -> b -> LambdaParam scope a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> LambdaParam scope a -> b
$cfoldr1 :: forall scope a. (a -> a -> a) -> LambdaParam scope a -> a
foldr1 :: forall a. (a -> a -> a) -> LambdaParam scope a -> a
$cfoldl1 :: forall scope a. (a -> a -> a) -> LambdaParam scope a -> a
foldl1 :: forall a. (a -> a -> a) -> LambdaParam scope a -> a
$ctoList :: forall scope a. LambdaParam scope a -> [a]
toList :: forall a. LambdaParam scope a -> [a]
$cnull :: forall scope a. LambdaParam scope a -> Bool
null :: forall a. LambdaParam scope a -> Bool
$clength :: forall scope a. LambdaParam scope a -> Int
length :: forall a. LambdaParam scope a -> Int
$celem :: forall scope a. Eq a => a -> LambdaParam scope a -> Bool
elem :: forall a. Eq a => a -> LambdaParam scope a -> Bool
$cmaximum :: forall scope a. Ord a => LambdaParam scope a -> a
maximum :: forall a. Ord a => LambdaParam scope a -> a
$cminimum :: forall scope a. Ord a => LambdaParam scope a -> a
minimum :: forall a. Ord a => LambdaParam scope a -> a
$csum :: forall scope a. Num a => LambdaParam scope a -> a
sum :: forall a. Num a => LambdaParam scope a -> a
$cproduct :: forall scope a. Num a => LambdaParam scope a -> a
product :: forall a. Num a => LambdaParam scope a -> a
Foldable, Functor (LambdaParam scope)
Foldable (LambdaParam scope)
(Functor (LambdaParam scope), Foldable (LambdaParam scope)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> LambdaParam scope a -> f (LambdaParam scope b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    LambdaParam scope (f a) -> f (LambdaParam scope a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LambdaParam scope a -> m (LambdaParam scope b))
-> (forall (m :: * -> *) a.
    Monad m =>
    LambdaParam scope (m a) -> m (LambdaParam scope a))
-> Traversable (LambdaParam scope)
forall scope. Functor (LambdaParam scope)
forall scope. Foldable (LambdaParam scope)
forall scope (m :: * -> *) a.
Monad m =>
LambdaParam scope (m a) -> m (LambdaParam scope a)
forall scope (f :: * -> *) a.
Applicative f =>
LambdaParam scope (f a) -> f (LambdaParam scope a)
forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LambdaParam scope a -> m (LambdaParam scope b)
forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LambdaParam scope a -> f (LambdaParam 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 =>
LambdaParam scope (m a) -> m (LambdaParam scope a)
forall (f :: * -> *) a.
Applicative f =>
LambdaParam scope (f a) -> f (LambdaParam scope a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LambdaParam scope a -> m (LambdaParam scope b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LambdaParam scope a -> f (LambdaParam scope b)
$ctraverse :: forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LambdaParam scope a -> f (LambdaParam scope b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LambdaParam scope a -> f (LambdaParam scope b)
$csequenceA :: forall scope (f :: * -> *) a.
Applicative f =>
LambdaParam scope (f a) -> f (LambdaParam scope a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
LambdaParam scope (f a) -> f (LambdaParam scope a)
$cmapM :: forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LambdaParam scope a -> m (LambdaParam scope b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LambdaParam scope a -> m (LambdaParam scope b)
$csequence :: forall scope (m :: * -> *) a.
Monad m =>
LambdaParam scope (m a) -> m (LambdaParam scope a)
sequence :: forall (m :: * -> *) a.
Monad m =>
LambdaParam scope (m a) -> m (LambdaParam scope a)
Traversable, (forall x.
 LambdaParam scope term -> Rep (LambdaParam scope term) x)
-> (forall x.
    Rep (LambdaParam scope term) x -> LambdaParam scope term)
-> Generic (LambdaParam scope term)
forall x. Rep (LambdaParam scope term) x -> LambdaParam scope term
forall x. LambdaParam scope term -> Rep (LambdaParam scope term) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall scope term x.
Rep (LambdaParam scope term) x -> LambdaParam scope term
forall scope term x.
LambdaParam scope term -> Rep (LambdaParam scope term) x
$cfrom :: forall scope term x.
LambdaParam scope term -> Rep (LambdaParam scope term) x
from :: forall x. LambdaParam scope term -> Rep (LambdaParam scope term) x
$cto :: forall scope term x.
Rep (LambdaParam scope term) x -> LambdaParam scope term
to :: forall x. Rep (LambdaParam scope term) x -> LambdaParam scope term
GHC.Generic)

data TermSig scope term
    = UniverseF
    | UniverseCubeF
    | UniverseTopeF
    | CubeUnitF
    | CubeUnitStarF
    | Cube2F
    | Cube2_0F
    | Cube2_1F
    | CubeIF
    | CubeI_0F
    | CubeI_1F
    | CubeProductF term term
    | CubeFlipF term
    | CubeUnflipF term
    | CubeSupF term term
    | CubeInfF term 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 (LambdaParam scope term)) scope
    | PairF term term
    | FirstF term
    | SecondF term
    | ReflF (Maybe (term, Maybe term))
    | IdJF term term term term term term
    -- | A match over a @#data@ scrutinee: scrutinee, optional motive, and one
    -- branch per constructor (constructor name, arm chain). The node is
    -- elaborated into the generated eliminator during typechecking, so a
    -- /typed/ match never exists.
    | MatchF term (Maybe term) [(VarIdent, term)]
    -- | One branch binder of a match; the body is the next arm, or the branch
    -- body once the binders run out. Valid only inside a 'MatchF' branch; the
    -- parser cannot produce it anywhere else.
    | MatchArmF Binder scope
    | 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) (Maybe term) term scope
    | HoleF (Maybe VarIdent)
    deriving (TermSig scope term -> TermSig scope term -> Bool
(TermSig scope term -> TermSig scope term -> Bool)
-> (TermSig scope term -> TermSig scope term -> Bool)
-> Eq (TermSig scope term)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall scope term.
(Eq term, Eq scope) =>
TermSig scope term -> TermSig scope term -> Bool
$c== :: forall scope term.
(Eq term, Eq scope) =>
TermSig scope term -> TermSig scope term -> Bool
== :: TermSig scope term -> TermSig scope term -> Bool
$c/= :: forall scope term.
(Eq term, Eq scope) =>
TermSig scope term -> TermSig scope term -> Bool
/= :: TermSig scope term -> TermSig scope term -> Bool
Eq, (forall a b. (a -> b) -> TermSig scope a -> TermSig scope b)
-> (forall a b. a -> TermSig scope b -> TermSig scope a)
-> Functor (TermSig scope)
forall a b. a -> TermSig scope b -> TermSig scope a
forall a b. (a -> b) -> TermSig scope a -> TermSig scope b
forall scope a b. a -> TermSig scope b -> TermSig scope a
forall scope a b. (a -> b) -> TermSig scope a -> TermSig 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) -> TermSig scope a -> TermSig scope b
fmap :: forall a b. (a -> b) -> TermSig scope a -> TermSig scope b
$c<$ :: forall scope a b. a -> TermSig scope b -> TermSig scope a
<$ :: forall a b. a -> TermSig scope b -> TermSig scope a
Functor, (forall m. Monoid m => TermSig scope m -> m)
-> (forall m a. Monoid m => (a -> m) -> TermSig scope a -> m)
-> (forall m a. Monoid m => (a -> m) -> TermSig scope a -> m)
-> (forall a b. (a -> b -> b) -> b -> TermSig scope a -> b)
-> (forall a b. (a -> b -> b) -> b -> TermSig scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> TermSig scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> TermSig scope a -> b)
-> (forall a. (a -> a -> a) -> TermSig scope a -> a)
-> (forall a. (a -> a -> a) -> TermSig scope a -> a)
-> (forall a. TermSig scope a -> [a])
-> (forall a. TermSig scope a -> Bool)
-> (forall a. TermSig scope a -> Int)
-> (forall a. Eq a => a -> TermSig scope a -> Bool)
-> (forall a. Ord a => TermSig scope a -> a)
-> (forall a. Ord a => TermSig scope a -> a)
-> (forall a. Num a => TermSig scope a -> a)
-> (forall a. Num a => TermSig scope a -> a)
-> Foldable (TermSig scope)
forall a. Eq a => a -> TermSig scope a -> Bool
forall a. Num a => TermSig scope a -> a
forall a. Ord a => TermSig scope a -> a
forall m. Monoid m => TermSig scope m -> m
forall a. TermSig scope a -> Bool
forall a. TermSig scope a -> Int
forall a. TermSig scope a -> [a]
forall a. (a -> a -> a) -> TermSig scope a -> a
forall scope a. Eq a => a -> TermSig scope a -> Bool
forall scope a. Num a => TermSig scope a -> a
forall scope a. Ord a => TermSig scope a -> a
forall scope m. Monoid m => TermSig scope m -> m
forall m a. Monoid m => (a -> m) -> TermSig scope a -> m
forall scope a. TermSig scope a -> Bool
forall scope a. TermSig scope a -> Int
forall scope a. TermSig scope a -> [a]
forall b a. (b -> a -> b) -> b -> TermSig scope a -> b
forall a b. (a -> b -> b) -> b -> TermSig scope a -> b
forall scope a. (a -> a -> a) -> TermSig scope a -> a
forall scope m a. Monoid m => (a -> m) -> TermSig scope a -> m
forall scope b a. (b -> a -> b) -> b -> TermSig scope a -> b
forall scope a b. (a -> b -> b) -> b -> TermSig 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 => TermSig scope m -> m
fold :: forall m. Monoid m => TermSig scope m -> m
$cfoldMap :: forall scope m a. Monoid m => (a -> m) -> TermSig scope a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TermSig scope a -> m
$cfoldMap' :: forall scope m a. Monoid m => (a -> m) -> TermSig scope a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TermSig scope a -> m
$cfoldr :: forall scope a b. (a -> b -> b) -> b -> TermSig scope a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TermSig scope a -> b
$cfoldr' :: forall scope a b. (a -> b -> b) -> b -> TermSig scope a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TermSig scope a -> b
$cfoldl :: forall scope b a. (b -> a -> b) -> b -> TermSig scope a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TermSig scope a -> b
$cfoldl' :: forall scope b a. (b -> a -> b) -> b -> TermSig scope a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TermSig scope a -> b
$cfoldr1 :: forall scope a. (a -> a -> a) -> TermSig scope a -> a
foldr1 :: forall a. (a -> a -> a) -> TermSig scope a -> a
$cfoldl1 :: forall scope a. (a -> a -> a) -> TermSig scope a -> a
foldl1 :: forall a. (a -> a -> a) -> TermSig scope a -> a
$ctoList :: forall scope a. TermSig scope a -> [a]
toList :: forall a. TermSig scope a -> [a]
$cnull :: forall scope a. TermSig scope a -> Bool
null :: forall a. TermSig scope a -> Bool
$clength :: forall scope a. TermSig scope a -> Int
length :: forall a. TermSig scope a -> Int
$celem :: forall scope a. Eq a => a -> TermSig scope a -> Bool
elem :: forall a. Eq a => a -> TermSig scope a -> Bool
$cmaximum :: forall scope a. Ord a => TermSig scope a -> a
maximum :: forall a. Ord a => TermSig scope a -> a
$cminimum :: forall scope a. Ord a => TermSig scope a -> a
minimum :: forall a. Ord a => TermSig scope a -> a
$csum :: forall scope a. Num a => TermSig scope a -> a
sum :: forall a. Num a => TermSig scope a -> a
$cproduct :: forall scope a. Num a => TermSig scope a -> a
product :: forall a. Num a => TermSig scope a -> a
Foldable, Functor (TermSig scope)
Foldable (TermSig scope)
(Functor (TermSig scope), Foldable (TermSig scope)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TermSig scope a -> f (TermSig scope b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TermSig scope (f a) -> f (TermSig scope a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TermSig scope a -> m (TermSig scope b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TermSig scope (m a) -> m (TermSig scope a))
-> Traversable (TermSig scope)
forall scope. Functor (TermSig scope)
forall scope. Foldable (TermSig scope)
forall scope (m :: * -> *) a.
Monad m =>
TermSig scope (m a) -> m (TermSig scope a)
forall scope (f :: * -> *) a.
Applicative f =>
TermSig scope (f a) -> f (TermSig scope a)
forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermSig scope a -> m (TermSig scope b)
forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermSig scope a -> f (TermSig 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 =>
TermSig scope (m a) -> m (TermSig scope a)
forall (f :: * -> *) a.
Applicative f =>
TermSig scope (f a) -> f (TermSig scope a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermSig scope a -> m (TermSig scope b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermSig scope a -> f (TermSig scope b)
$ctraverse :: forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermSig scope a -> f (TermSig scope b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermSig scope a -> f (TermSig scope b)
$csequenceA :: forall scope (f :: * -> *) a.
Applicative f =>
TermSig scope (f a) -> f (TermSig scope a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TermSig scope (f a) -> f (TermSig scope a)
$cmapM :: forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermSig scope a -> m (TermSig scope b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermSig scope a -> m (TermSig scope b)
$csequence :: forall scope (m :: * -> *) a.
Monad m =>
TermSig scope (m a) -> m (TermSig scope a)
sequence :: forall (m :: * -> *) a.
Monad m =>
TermSig scope (m a) -> m (TermSig scope a)
Traversable, (forall x. TermSig scope term -> Rep (TermSig scope term) x)
-> (forall x. Rep (TermSig scope term) x -> TermSig scope term)
-> Generic (TermSig scope term)
forall x. Rep (TermSig scope term) x -> TermSig scope term
forall x. TermSig scope term -> Rep (TermSig scope term) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall scope term x.
Rep (TermSig scope term) x -> TermSig scope term
forall scope term x.
TermSig scope term -> Rep (TermSig scope term) x
$cfrom :: forall scope term x.
TermSig scope term -> Rep (TermSig scope term) x
from :: forall x. TermSig scope term -> Rep (TermSig scope term) x
$cto :: forall scope term x.
Rep (TermSig scope term) x -> TermSig scope term
to :: forall x. Rep (TermSig scope term) x -> TermSig scope term
GHC.Generic)

deriveBifunctor ''LambdaParam
deriveBifoldable ''LambdaParam
deriveBitraversable ''LambdaParam
deriveGenericK ''LambdaParam

deriveBifunctor ''TermSig
deriveBifoldable ''TermSig
deriveBitraversable ''TermSig
deriveGenericK ''TermSig

-- | Matching the non-recursive fields of the signature.
--
-- A modality and a hole's name are part of the term: they must agree. A 'Binder'
-- is /not/: it records the names a binder introduces, purely so that goals and
-- error messages can show the user's own names, and two terms that differ only
-- in them are the same term. The old representation compared them (its 'Eq' was
-- derived), so @\ x -> x@ and @\ y -> y@ compared unequal; on the new one they
-- are α-equivalent, as they should be.
instance ZipMatchK TModality where
  zipMatchWithK :: forall (as :: LoT (*)) (bs :: LoT (*)) (cs :: LoT (*)).
Mappings as bs cs
-> (TModality :@@: as)
-> (TModality :@@: bs)
-> Maybe (TModality :@@: cs)
zipMatchWithK = Mappings as bs cs
-> (TModality :@@: as)
-> (TModality :@@: bs)
-> Maybe (TModality :@@: cs)
Mappings as bs cs -> TModality -> TModality -> Maybe TModality
forall {k} a (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
Eq a =>
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq

instance ZipMatchK VarIdent where
  zipMatchWithK :: forall (as :: LoT (*)) (bs :: LoT (*)) (cs :: LoT (*)).
Mappings as bs cs
-> (VarIdent :@@: as)
-> (VarIdent :@@: bs)
-> Maybe (VarIdent :@@: cs)
zipMatchWithK = Mappings as bs cs
-> (VarIdent :@@: as)
-> (VarIdent :@@: bs)
-> Maybe (VarIdent :@@: cs)
Mappings as bs cs -> VarIdent -> VarIdent -> Maybe VarIdent
forall {k} a (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
Eq a =>
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq

instance ZipMatchK Binder where
  zipMatchWithK :: forall (as :: LoT (*)) (bs :: LoT (*)) (cs :: LoT (*)).
Mappings as bs cs
-> (Binder :@@: as) -> (Binder :@@: bs) -> Maybe (Binder :@@: cs)
zipMatchWithK = Mappings as bs cs
-> (Binder :@@: as) -> (Binder :@@: bs) -> Maybe (Binder :@@: cs)
Mappings as bs cs -> Binder -> Binder -> Maybe Binder
forall {k} (as :: LoT k) (bs :: LoT k) (cs :: LoT k) a.
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaChooseLeft

-- | A hole's name is a whole field ('HoleF'), so it is matched as a constant
-- rather than through the 'Maybe' functor.
instance ZipMatchK (Maybe VarIdent) where
  zipMatchWithK :: forall (as :: LoT (*)) (bs :: LoT (*)) (cs :: LoT (*)).
Mappings as bs cs
-> (Maybe VarIdent :@@: as)
-> (Maybe VarIdent :@@: bs)
-> Maybe (Maybe VarIdent :@@: cs)
zipMatchWithK = Mappings as bs cs
-> Maybe VarIdent -> Maybe VarIdent -> Maybe (Maybe VarIdent)
Mappings as bs cs
-> (Maybe VarIdent :@@: as)
-> (Maybe VarIdent :@@: bs)
-> Maybe (Maybe VarIdent :@@: cs)
forall {k} a (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
Eq a =>
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq

instance ZipMatchK LambdaParam

-- | The node matcher, TH-derived: an explicit instance, so no @Generics.Kind@
-- view is rebuilt per comparison. It drives 'Control.Monad.Free.Foil.alphaEquiv'
-- and 'Control.Monad.Free.Foil.unsafeEqAST', run on every comparison of two
-- terms, which in a dependent checker is most of the work. This replaced a
-- hand-written 44-constructor matcher carried on free-foil 0.2.0 (which had no
-- deriver); the deriver is the point of moving to this free-foil.
deriveZipMatchK ''TermSig


-- * Annotations
--
-- 'AnnSig' is @Control.Monad.Free.Foil.Annotated@'s: the annotation is a functor
-- of the signature's /term/ parameter, so a node's type is a term in the node's
-- own scope. free-foil provides it with a /derived/ (explicit) 'ZipMatchK', its
-- 'Bifunctor' (recurses into the annotation, for substitution) and its
-- 'Bifoldable' (does not, so a term's free variables exclude those only in its
-- type). All rzk adds is how its own annotation, 'TypeInfo', matches.

-- | The annotation is ignored in matching, so two terms differing only in their
-- types are α-equivalent. The 'ZipMatchK' API makes an annotation holding terms
-- construct its result through the mapping, so it cannot be dropped from the
-- match — but it is made lazy: 'infoType' below is a thunk never forced, because
-- 'AnnSig's 'Bifoldable' does not visit the annotation. So the 30-deep universe
-- tower inside a type is never walked. The memoised forms are dropped (every
-- consumer of the zipped result discards them). This is the annotation-blind
-- pattern from the 'Control.Monad.Free.Foil.Annotated' haddock.
instance ZipMatchK TypeInfo where
  zipMatchWithK :: forall (as :: LoT (* -> *)) (bs :: LoT (* -> *))
       (cs :: LoT (* -> *)).
Mappings as bs cs
-> (TypeInfo :@@: as)
-> (TypeInfo :@@: bs)
-> Maybe (TypeInfo :@@: cs)
zipMatchWithK (a -> b -> Maybe c
f :^: Mappings as1 bs1 cs1
M0) (TypeInfo a
t1 Maybe a
_ Maybe a
_) (TypeInfo b
t2 Maybe b
_ Maybe b
_) =
    TypeInfo c -> Maybe (TypeInfo c)
forall a. a -> Maybe a
Just (c -> Maybe c -> Maybe c -> TypeInfo c
forall term. term -> Maybe term -> Maybe term -> TypeInfo term
TypeInfo (c -> (c -> c) -> Maybe c -> c
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Char] -> c
forall a. HasCallStack => [Char] -> a
error [Char]
"ZipMatchK TypeInfo: annotation forced") c -> c
forall a. a -> a
id (a -> b -> Maybe c
f a
t1 b
t2)) Maybe c
forall a. Maybe a
Nothing Maybe c
forall a. Maybe a
Nothing)

-- | Where a term was written.
--
-- This is the annotation of an /untyped/ term, so that a diagnostic can point
-- at the sub-term it is about rather than at the declaration around it (issue
-- #81). It is a phantom in the node's term parameter: the annotation machinery
-- wants a functor of the term, and a position holds no terms.
newtype SrcPos term = SrcPos RzkPosition
  deriving ((forall a b. (a -> b) -> SrcPos a -> SrcPos b)
-> (forall a b. a -> SrcPos b -> SrcPos a) -> Functor SrcPos
forall a b. a -> SrcPos b -> SrcPos a
forall a b. (a -> b) -> SrcPos a -> SrcPos 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) -> SrcPos a -> SrcPos b
fmap :: forall a b. (a -> b) -> SrcPos a -> SrcPos b
$c<$ :: forall a b. a -> SrcPos b -> SrcPos a
<$ :: forall a b. a -> SrcPos b -> SrcPos a
Functor, (forall m. Monoid m => SrcPos m -> m)
-> (forall m a. Monoid m => (a -> m) -> SrcPos a -> m)
-> (forall m a. Monoid m => (a -> m) -> SrcPos a -> m)
-> (forall a b. (a -> b -> b) -> b -> SrcPos a -> b)
-> (forall a b. (a -> b -> b) -> b -> SrcPos a -> b)
-> (forall b a. (b -> a -> b) -> b -> SrcPos a -> b)
-> (forall b a. (b -> a -> b) -> b -> SrcPos a -> b)
-> (forall a. (a -> a -> a) -> SrcPos a -> a)
-> (forall a. (a -> a -> a) -> SrcPos a -> a)
-> (forall a. SrcPos a -> [a])
-> (forall a. SrcPos a -> Bool)
-> (forall a. SrcPos a -> Int)
-> (forall a. Eq a => a -> SrcPos a -> Bool)
-> (forall a. Ord a => SrcPos a -> a)
-> (forall a. Ord a => SrcPos a -> a)
-> (forall a. Num a => SrcPos a -> a)
-> (forall a. Num a => SrcPos a -> a)
-> Foldable SrcPos
forall a. Eq a => a -> SrcPos a -> Bool
forall a. Num a => SrcPos a -> a
forall a. Ord a => SrcPos a -> a
forall m. Monoid m => SrcPos m -> m
forall a. SrcPos a -> Bool
forall a. SrcPos a -> Int
forall a. SrcPos a -> [a]
forall a. (a -> a -> a) -> SrcPos a -> a
forall m a. Monoid m => (a -> m) -> SrcPos a -> m
forall b a. (b -> a -> b) -> b -> SrcPos a -> b
forall a b. (a -> b -> b) -> b -> SrcPos 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 => SrcPos m -> m
fold :: forall m. Monoid m => SrcPos m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SrcPos a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SrcPos a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SrcPos a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> SrcPos a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> SrcPos a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SrcPos a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SrcPos a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SrcPos a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SrcPos a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SrcPos a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SrcPos a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> SrcPos a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> SrcPos a -> a
foldr1 :: forall a. (a -> a -> a) -> SrcPos a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SrcPos a -> a
foldl1 :: forall a. (a -> a -> a) -> SrcPos a -> a
$ctoList :: forall a. SrcPos a -> [a]
toList :: forall a. SrcPos a -> [a]
$cnull :: forall a. SrcPos a -> Bool
null :: forall a. SrcPos a -> Bool
$clength :: forall a. SrcPos a -> Int
length :: forall a. SrcPos a -> Int
$celem :: forall a. Eq a => a -> SrcPos a -> Bool
elem :: forall a. Eq a => a -> SrcPos a -> Bool
$cmaximum :: forall a. Ord a => SrcPos a -> a
maximum :: forall a. Ord a => SrcPos a -> a
$cminimum :: forall a. Ord a => SrcPos a -> a
minimum :: forall a. Ord a => SrcPos a -> a
$csum :: forall a. Num a => SrcPos a -> a
sum :: forall a. Num a => SrcPos a -> a
$cproduct :: forall a. Num a => SrcPos a -> a
product :: forall a. Num a => SrcPos a -> a
Foldable, Functor SrcPos
Foldable SrcPos
(Functor SrcPos, Foldable SrcPos) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> SrcPos a -> f (SrcPos b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    SrcPos (f a) -> f (SrcPos a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SrcPos a -> m (SrcPos b))
-> (forall (m :: * -> *) a.
    Monad m =>
    SrcPos (m a) -> m (SrcPos a))
-> Traversable SrcPos
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 => SrcPos (m a) -> m (SrcPos a)
forall (f :: * -> *) a.
Applicative f =>
SrcPos (f a) -> f (SrcPos a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SrcPos a -> m (SrcPos b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SrcPos a -> f (SrcPos b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SrcPos a -> f (SrcPos b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SrcPos a -> f (SrcPos b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SrcPos (f a) -> f (SrcPos a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
SrcPos (f a) -> f (SrcPos a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SrcPos a -> m (SrcPos b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SrcPos a -> m (SrcPos b)
$csequence :: forall (m :: * -> *) a. Monad m => SrcPos (m a) -> m (SrcPos a)
sequence :: forall (m :: * -> *) a. Monad m => SrcPos (m a) -> m (SrcPos a)
Traversable)

-- | Two terms written in different places are the same term, so a position is
-- ignored in matching, as a node's type is.
instance ZipMatchK SrcPos where
  zipMatchWithK :: forall (as :: LoT (* -> *)) (bs :: LoT (* -> *))
       (cs :: LoT (* -> *)).
Mappings as bs cs
-> (SrcPos :@@: as) -> (SrcPos :@@: bs) -> Maybe (SrcPos :@@: cs)
zipMatchWithK Mappings as bs cs
_ (SrcPos RzkPosition
pos) SrcPos :@@: bs
_ = SrcPos (HeadLoT cs) -> Maybe (SrcPos (HeadLoT cs))
forall a. a -> Maybe a
Just (RzkPosition -> SrcPos (HeadLoT cs)
forall term. RzkPosition -> SrcPos term
SrcPos RzkPosition
pos)

-- | No position: what a node the checker builds itself carries, and what a node
-- gets until the conversion from the surface syntax puts the real one on it.
noSrcPos :: SrcPos term
noSrcPos :: forall term. SrcPos term
noSrcPos = RzkPosition -> SrcPos term
forall term. RzkPosition -> SrcPos term
SrcPos (Maybe [Char] -> BNFC'Position -> RzkPosition
RzkPosition Maybe [Char]
forall a. Maybe a
Nothing BNFC'Position
forall a. Maybe a
Nothing)

-- * Terms

-- | An untyped term: the surface syntax, elaborated, every node carrying where
-- it was written.
type Term = AST NameBinder (AnnSig SrcPos TermSig)

-- | A typed term: every node carries its type. The successor of @TermT@.
type TermT = AST NameBinder (AnnSig TypeInfo TermSig)

-- | A scope: a binder together with the term it binds over.
type ScopedTermT = ScopedAST NameBinder (AnnSig TypeInfo TermSig)

-- | A scope of an untyped term.
type ScopedTerm = ScopedAST NameBinder (AnnSig SrcPos TermSig)

-- | Record where a term was written, unless it is already recorded.
--
-- The conversion tags a node after converting what is under it, and desugaring
-- hands surface nodes back to the conversion carrying the position of the node
-- they came from. A node that already knows where it was written therefore
-- learnt it from something more specific, and keeps it: the λ that a
-- definition's parameters are wrapped in reuses the λ's own position as it
-- peels them off, and would otherwise claim every diagnostic in the body.
--
-- A variable carries no node of its own, so it is returned unchanged; where a
-- variable occurrence was written is on its 'VarIdent' instead.
atSrcPos :: RzkPosition -> Term n -> Term n
atSrcPos :: forall (n :: S). RzkPosition -> Term n -> Term n
atSrcPos RzkPosition
pos t :: Term n
t@(Node (AnnSig (SrcPos RzkPosition
old) TermSig (ScopedAST NameBinder (AnnSig SrcPos TermSig) n) (Term n)
sig))
  | BNFC'Position
Nothing <- RzkPosition -> BNFC'Position
rzkLineCol RzkPosition
old = AnnSig
  SrcPos
  TermSig
  (ScopedAST NameBinder (AnnSig SrcPos TermSig) n)
  (Term n)
-> Term n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node (SrcPos (Term n)
-> TermSig
     (ScopedAST NameBinder (AnnSig SrcPos TermSig) n) (Term n)
-> AnnSig
     SrcPos
     TermSig
     (ScopedAST NameBinder (AnnSig SrcPos TermSig) n)
     (Term n)
forall (ann :: * -> *) (sig :: * -> * -> *) scope term.
ann term -> sig scope term -> AnnSig ann sig scope term
AnnSig (RzkPosition -> SrcPos (Term n)
forall term. RzkPosition -> SrcPos term
SrcPos RzkPosition
pos) TermSig (ScopedAST NameBinder (AnnSig SrcPos TermSig) n) (Term n)
sig)
  | Bool
otherwise                 = Term n
t
atSrcPos RzkPosition
_ t :: Term n
t@(Var Name n
_)          = Term n
t

-- | Where the term was written, when it came from a file.
positionOfTerm :: Term n -> Maybe RzkPosition
positionOfTerm :: forall (n :: S). Term n -> Maybe RzkPosition
positionOfTerm (Var Name n
_)                        = Maybe RzkPosition
forall a. Maybe a
Nothing
positionOfTerm (Node (AnnSig (SrcPos RzkPosition
pos) TermSig
  (ScopedAST NameBinder (AnnSig SrcPos TermSig) n)
  (AST NameBinder (AnnSig SrcPos TermSig) n)
_)) =
  case RzkPosition -> BNFC'Position
rzkLineCol RzkPosition
pos of
    BNFC'Position
Nothing -> Maybe RzkPosition
forall a. Maybe a
Nothing
    Just (Int, Int)
_  -> RzkPosition -> Maybe RzkPosition
forall a. a -> Maybe a
Just RzkPosition
pos

-- | The annotation of a node: its type, and its memoised normal forms. A
-- variable carries none — its type lives in the context.
typeInfoOf :: TermT n -> Maybe (TypeInfo (TermT n))
typeInfoOf :: forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n))
typeInfoOf (Var Name n
_)                = Maybe (TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n))
forall a. Maybe a
Nothing
typeInfoOf (Node (AnnSig TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
info TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
  (AST NameBinder (AnnSig TypeInfo TermSig) n)
_)) = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> Maybe (TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n))
forall a. a -> Maybe a
Just TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
info

-- | Drop every annotation, for printing and for the surface-facing API.
untyped :: TermT n -> Term n
untyped :: forall (n :: S). TermT n -> Term n
untyped (Var Name n
name)              = Name n -> AST NameBinder (AnnSig SrcPos TermSig) n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
name
untyped (Node (AnnSig TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
_ann TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
  (AST NameBinder (AnnSig TypeInfo TermSig) n)
sig)) = TermSig (ScopedTerm n) (AST NameBinder (AnnSig SrcPos TermSig) n)
-> AST NameBinder (AnnSig SrcPos TermSig) n
forall (n :: S). TermSig (ScopedTerm n) (Term n) -> Term n
UntypedNode ((ScopedAST NameBinder (AnnSig TypeInfo TermSig) n -> ScopedTerm n)
-> (AST NameBinder (AnnSig TypeInfo TermSig) n
    -> AST NameBinder (AnnSig SrcPos TermSig) n)
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
     (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> TermSig
     (ScopedTerm n) (AST NameBinder (AnnSig SrcPos TermSig) n)
forall a b c d. (a -> b) -> (c -> d) -> TermSig a c -> TermSig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST NameBinder (AnnSig TypeInfo TermSig) n -> ScopedTerm n
forall {n :: S}.
ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> ScopedAST NameBinder (AnnSig SrcPos TermSig) n
untypedScoped AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig SrcPos TermSig) n
forall (n :: S). TermT n -> Term n
untyped TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
  (AST NameBinder (AnnSig TypeInfo TermSig) n)
sig)
  where
    untypedScoped :: ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> ScopedAST NameBinder (AnnSig SrcPos TermSig) n
untypedScoped (ScopedAST NameBinder n l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body) = NameBinder n l
-> AST NameBinder (AnnSig SrcPos TermSig) l
-> ScopedAST NameBinder (AnnSig SrcPos TermSig) n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
binder (AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig SrcPos TermSig) l
forall (n :: S). TermT n -> Term n
untyped AST NameBinder (AnnSig TypeInfo TermSig) l
body)

-- | Memoise a node's own weak head normal form (the self-referential knot of the
-- old representation, unchanged).
termIsWHNF :: TermT n -> TermT n
termIsWHNF :: forall (n :: S). TermT n -> TermT n
termIsWHNF t :: TermT n
t@Var{} = TermT n
t
termIsWHNF (Node (AnnSig TypeInfo (TermT n)
info TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
sig)) = TermT n
t'
  where t' :: TermT n
t' = AnnSig
  TypeInfo
  TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
  (TermT n)
-> TermT n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node (TypeInfo (TermT n)
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
-> AnnSig
     TypeInfo
     TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
     (TermT n)
forall (ann :: * -> *) (sig :: * -> * -> *) scope term.
ann term -> sig scope term -> AnnSig ann sig scope term
AnnSig TypeInfo (TermT n)
info { infoWHNF = Just t' } TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
sig)

termIsNF :: TermT n -> TermT n
termIsNF :: forall (n :: S). TermT n -> TermT n
termIsNF t :: TermT n
t@Var{} = TermT n
t
termIsNF (Node (AnnSig TypeInfo (TermT n)
info TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
sig)) = TermT n
t'
  where t' :: TermT n
t' = AnnSig
  TypeInfo
  TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
  (TermT n)
-> TermT n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node (TypeInfo (TermT n)
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
-> AnnSig
     TypeInfo
     TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
     (TermT n)
forall (ann :: * -> *) (sig :: * -> * -> *) scope term.
ann term -> sig scope term -> AnnSig ann sig scope term
AnnSig TypeInfo (TermT n)
info { infoWHNF = Just t', infoNF = Just t' } TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
sig)

-- * Equality

-- | Syntactic equality of two terms of the same scope.
--
-- Annotation-blind, as the old derived 'Eq' was, but it also requires the two to
-- bind the same names, so it is /conservative/: two α-equivalent terms whose
-- binders differ are not equal. That is what the tope-context scans want — the
-- terms there come from the same context — and it is cheaper than 'alphaEqT',
-- which walks the scope.
eqT :: Foil.Distinct n => TermT n -> TermT n -> Bool
eqT :: forall (n :: S). Distinct n => TermT n -> TermT n -> Bool
eqT = AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (l :: S).
(Bitraversable sig, ZipMatchK sig, UnifiablePattern binder,
 Distinct n, Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
unsafeEqAST

-- | α-equivalence: name-blind and annotation-blind. The old representation's 'Eq'
-- compared binder names, so @\\ x -> x@ and @\\ y -> y@ were unequal; they are the
-- same term, and this says so.
alphaEqT :: Foil.Distinct n => Foil.Scope n -> TermT n -> TermT n -> Bool
alphaEqT :: forall (n :: S).
Distinct n =>
Scope n -> TermT n -> TermT n -> Bool
alphaEqT = Scope n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv

elemT :: Foil.Distinct n => TermT n -> [TermT n] -> Bool
elemT :: forall (n :: S). Distinct n => TermT n -> [TermT n] -> Bool
elemT TermT n
t = (TermT n -> Bool) -> [TermT n] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TermT n -> TermT n -> Bool
forall (n :: S). Distinct n => TermT n -> TermT n -> Bool
eqT TermT n
t)

notElemT :: Foil.Distinct n => TermT n -> [TermT n] -> Bool
notElemT :: forall (n :: S). Distinct n => TermT n -> [TermT n] -> Bool
notElemT TermT n
t = Bool -> Bool
not (Bool -> Bool) -> ([TermT n] -> Bool) -> [TermT n] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> [TermT n] -> Bool
forall (n :: S). Distinct n => TermT n -> [TermT n] -> Bool
elemT TermT n
t

nubT :: Foil.Distinct n => [TermT n] -> [TermT n]
nubT :: forall (n :: S). Distinct n => [TermT n] -> [TermT n]
nubT []       = []
nubT (TermT n
t : [TermT n]
ts) = TermT n
t TermT n -> [TermT n] -> [TermT n]
forall a. a -> [a] -> [a]
: [TermT n] -> [TermT n]
forall (n :: S). Distinct n => [TermT n] -> [TermT n]
nubT ((TermT n -> Bool) -> [TermT n] -> [TermT n]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TermT n -> Bool) -> TermT n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> TermT n -> Bool
forall (n :: S). Distinct n => TermT n -> TermT n -> Bool
eqT TermT n
t) [TermT n]
ts)

-- * Free variables

-- | The free variables of a term.
--
-- free-foil 0.4.0 exports @freeVarsOf@, but it deduplicates and sorts; this one
-- keeps mention order and repeats, as the old representation's did. A name
-- bound on the way down is dropped from the result, which is what makes the
-- coercion back to the outer scope right.
freeVarsOfTerm :: Term n -> [Foil.Name n]
freeVarsOfTerm :: forall (n :: S). Term n -> [Name n]
freeVarsOfTerm (Var Name n
x)    = [Name n
x]
freeVarsOfTerm (UntypedNode TermSig (ScopedTerm n) (AST NameBinder (AnnSig SrcPos TermSig) n)
sig) = (ScopedTerm n -> [Name n])
-> (AST NameBinder (AnnSig SrcPos TermSig) n -> [Name n])
-> TermSig
     (ScopedTerm n) (AST NameBinder (AnnSig SrcPos TermSig) n)
-> [Name n]
forall m a b. Monoid m => (a -> m) -> (b -> m) -> TermSig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap ScopedTerm n -> [Name n]
forall (n' :: S). ScopedTerm n' -> [Name n']
freeVarsOfScoped AST NameBinder (AnnSig SrcPos TermSig) n -> [Name n]
forall (n :: S). Term n -> [Name n]
freeVarsOfTerm TermSig (ScopedTerm n) (AST NameBinder (AnnSig SrcPos TermSig) n)
sig
  where
    freeVarsOfScoped :: ScopedTerm n' -> [Foil.Name n']
    freeVarsOfScoped :: forall (n' :: S). ScopedTerm n' -> [Name n']
freeVarsOfScoped (ScopedAST NameBinder n' l
binder AST NameBinder (AnnSig SrcPos TermSig) l
body) =
      [Name l] -> [Name n']
forall a b. a -> b
unsafeCoerce
        [ Name l
x
        | Name l
x <- AST NameBinder (AnnSig SrcPos TermSig) l -> [Name l]
forall (n :: S). Term n -> [Name n]
freeVarsOfTerm AST NameBinder (AnnSig SrcPos TermSig) l
body
        , Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name l
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId (NameBinder n' l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n' l
binder)
        ]

-- | The free variables of a typed term, not counting those that occur only in the
-- types of its nodes ('Bifoldable' skips the annotation, as it did before).
freeVarsOfTermT :: TermT n -> [Foil.Name n]
freeVarsOfTermT :: forall (n :: S). TermT n -> [Name n]
freeVarsOfTermT = Term n -> [Name n]
forall (n :: S). Term n -> [Name n]
freeVarsOfTerm (Term n -> [Name n]) -> (TermT n -> Term n) -> TermT n -> [Name n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped

-- | Does the term mention the universe @U@ anywhere? A constructor field
-- whose type does is what makes an inductive type /large/ (see the
-- largeness warning in "Rzk.TypeCheck.Decl").
containsUniverse :: Term n -> Bool
containsUniverse :: forall (n :: S). Term n -> Bool
containsUniverse Term n
Universe   = Bool
True
containsUniverse (Var Name n
_)    = Bool
False
containsUniverse (UntypedNode TermSig (ScopedTerm n) (Term n)
sig) =
  (ScopedTerm n -> Bool -> Bool)
-> (Term n -> Bool -> Bool)
-> Bool
-> TermSig (ScopedTerm n) (Term n)
-> Bool
forall a c b.
(a -> c -> c) -> (b -> c -> c) -> c -> TermSig a b -> c
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr (\ScopedTerm n
scoped Bool
acc -> ScopedTerm n -> Bool
forall {n :: S}.
ScopedAST NameBinder (AnnSig SrcPos TermSig) n -> Bool
containsUniverseScoped ScopedTerm n
scoped Bool -> Bool -> Bool
|| Bool
acc)
          (\Term n
t Bool
acc -> Term n -> Bool
forall (n :: S). Term n -> Bool
containsUniverse Term n
t Bool -> Bool -> Bool
|| Bool
acc) Bool
False TermSig (ScopedTerm n) (Term n)
sig
  where
    containsUniverseScoped :: ScopedAST NameBinder (AnnSig SrcPos TermSig) n -> Bool
containsUniverseScoped (ScopedAST NameBinder n l
_ AST NameBinder (AnnSig SrcPos TermSig) l
body) = AST NameBinder (AnnSig SrcPos TermSig) l -> Bool
forall (n :: S). Term n -> Bool
containsUniverse AST NameBinder (AnnSig SrcPos TermSig) l
body

-- * Holes

isHoleT :: TermT n -> Bool
isHoleT :: forall (n :: S). TermT n -> Bool
isHoleT HoleT{} = Bool
True
isHoleT AST NameBinder (AnnSig TypeInfo TermSig) n
_       = Bool
False

-- | Is the term a /flexible/ spine: a hole, or an elimination headed by one
-- (@? a b@, @first ?@, @second (? a)@)?
--
-- Such a term is not yet committed to any shape: filling the head hole can turn
-- it into anything. A type of this form therefore stands for an arbitrary type,
-- which is what lets an eliminator whose result type is a motive application
-- (@ind-path A a C d x p : C x p@) be judged against a concrete goal. Contrast
-- 'containsHole', which is also true of a term whose /shape/ is already fixed
-- and only has holes among its parts (@? = ?@ is an identity type either way).
--
-- A projection counts for the same reason an application does. @first ?@ is
-- whatever the first component of the pair turns out to be, so it has no shape
-- of its own to mismatch with. Without this, a lemma stating a property of
-- projections (@first-path-Σ ... : first s = first t@) is not offered against a
-- goal whose endpoint is a plain variable, because solving @first ?t@ against it
-- would mean inventing the pair.
isHoleHeadedT :: TermT n -> Bool
isHoleHeadedT :: forall (n :: S). TermT n -> Bool
isHoleHeadedT HoleT{}       = Bool
True
isHoleHeadedT (AppT TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
_ AST NameBinder (AnnSig TypeInfo TermSig) n
f AST NameBinder (AnnSig TypeInfo TermSig) n
_)  = AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
forall (n :: S). TermT n -> Bool
isHoleHeadedT AST NameBinder (AnnSig TypeInfo TermSig) n
f
isHoleHeadedT (FirstT TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
_ AST NameBinder (AnnSig TypeInfo TermSig) n
t)  = AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
forall (n :: S). TermT n -> Bool
isHoleHeadedT AST NameBinder (AnnSig TypeInfo TermSig) n
t
isHoleHeadedT (SecondT TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
_ AST NameBinder (AnnSig TypeInfo TermSig) n
t) = AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
forall (n :: S). TermT n -> Bool
isHoleHeadedT AST NameBinder (AnnSig TypeInfo TermSig) n
t
isHoleHeadedT AST NameBinder (AnnSig TypeInfo TermSig) n
_             = Bool
False

-- | The name of every hole in a term.
holeNamesOf :: Term n -> [Maybe VarIdent]
holeNamesOf :: forall (n :: S). Term n -> [Maybe VarIdent]
holeNamesOf (Hole Maybe VarIdent
mname) = [Maybe VarIdent
mname]
holeNamesOf (Var Name n
_)      = []
holeNamesOf (UntypedNode TermSig (ScopedTerm n) (Term n)
sig) = (ScopedTerm n -> [Maybe VarIdent] -> [Maybe VarIdent])
-> (Term n -> [Maybe VarIdent] -> [Maybe VarIdent])
-> [Maybe VarIdent]
-> TermSig (ScopedTerm n) (Term n)
-> [Maybe VarIdent]
forall a c b.
(a -> c -> c) -> (b -> c -> c) -> c -> TermSig a b -> c
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr (\ScopedTerm n
scoped [Maybe VarIdent]
acc -> ScopedTerm n -> [Maybe VarIdent]
forall {n :: S}.
ScopedAST NameBinder (AnnSig SrcPos TermSig) n -> [Maybe VarIdent]
holeNamesOfScoped ScopedTerm n
scoped [Maybe VarIdent] -> [Maybe VarIdent] -> [Maybe VarIdent]
forall a. Semigroup a => a -> a -> a
<> [Maybe VarIdent]
acc)
                                   (\Term n
t [Maybe VarIdent]
acc -> Term n -> [Maybe VarIdent]
forall (n :: S). Term n -> [Maybe VarIdent]
holeNamesOf Term n
t [Maybe VarIdent] -> [Maybe VarIdent] -> [Maybe VarIdent]
forall a. Semigroup a => a -> a -> a
<> [Maybe VarIdent]
acc) [] TermSig (ScopedTerm n) (Term n)
sig
  where
    holeNamesOfScoped :: ScopedAST NameBinder (AnnSig SrcPos TermSig) n -> [Maybe VarIdent]
holeNamesOfScoped (ScopedAST NameBinder n l
_ AST NameBinder (AnnSig SrcPos TermSig) l
body) = AST NameBinder (AnnSig SrcPos TermSig) l -> [Maybe VarIdent]
forall (n :: S). Term n -> [Maybe VarIdent]
holeNamesOf AST NameBinder (AnnSig SrcPos TermSig) l
body

-- | Does the term contain a hole anywhere (including nested, e.g. @f ?@)?
containsHole :: TermT n -> Bool
containsHole :: forall (n :: S). TermT n -> Bool
containsHole HoleT{} = Bool
True
containsHole (Var Name n
_) = Bool
False
containsHole (Node (AnnSig TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
_ TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
  (AST NameBinder (AnnSig TypeInfo TermSig) n)
sig)) =
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n -> Bool -> Bool)
-> (AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool -> Bool)
-> Bool
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
     (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> Bool
forall a c b.
(a -> c -> c) -> (b -> c -> c) -> c -> TermSig a b -> c
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr (\ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
scoped Bool
acc -> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
forall {n :: S}.
ScopedAST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
containsHoleScoped ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
scoped Bool -> Bool -> Bool
|| Bool
acc) (\AST NameBinder (AnnSig TypeInfo TermSig) n
t Bool
acc -> AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
forall (n :: S). TermT n -> Bool
containsHole AST NameBinder (AnnSig TypeInfo TermSig) n
t Bool -> Bool -> Bool
|| Bool
acc) Bool
False TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
  (AST NameBinder (AnnSig TypeInfo TermSig) n)
sig
  where
    containsHoleScoped :: ScopedAST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
containsHoleScoped (ScopedAST NameBinder n l
_ AST NameBinder (AnnSig TypeInfo TermSig) l
body) = AST NameBinder (AnnSig TypeInfo TermSig) l -> Bool
forall (n :: S). TermT n -> Bool
containsHole AST NameBinder (AnnSig TypeInfo TermSig) l
body

-- * Going under a binder, and substituting

-- | Go under the binder of a scoped term.
--
-- The binder is used as it stands when its name is free in the ambient scope,
-- which is the common case and costs nothing. It has to be renamed when the name
-- is taken — sinking a term into a scope that has grown since the term was built
-- can do that — and only then is the body traversed.
withScopedT
  :: (Bifunctor sig, Foil.Distinct n)
  => Foil.Scope n
  -> ScopedAST NameBinder sig n
  -> (forall l. Foil.DExt n l => NameBinder n l -> AST NameBinder sig l -> r)
  -> r
withScopedT :: forall (sig :: * -> * -> *) (n :: S) r.
(Bifunctor sig, Distinct n) =>
Scope n
-> ScopedAST NameBinder sig n
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> AST NameBinder sig l -> r)
-> r
withScopedT Scope n
scope (ScopedAST NameBinder n l
binder AST NameBinder sig l
body) forall (l :: S).
DExt n l =>
NameBinder n l -> AST NameBinder sig l -> r
k
  | Name l -> Scope n -> Bool
forall (l :: S) (n :: S). Name l -> Scope n -> Bool
Foil.member (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder) Scope n
scope =
      Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> r) -> r)
-> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder' ->
        let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder' Scope n
scope
            rename :: Substitution (AST NameBinder sig) l l
rename = Substitution (AST NameBinder sig) n l
-> NameBinder n l
-> Name l
-> Substitution (AST NameBinder sig) l l
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
Foil.addRename (Substitution (AST NameBinder sig) n n
-> Substitution (AST NameBinder sig) n l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST NameBinder sig) n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst) NameBinder n l
binder (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder')
         in NameBinder n l -> AST NameBinder sig l -> r
forall (l :: S).
DExt n l =>
NameBinder n l -> AST NameBinder sig l -> r
k NameBinder n l
binder' (Scope l
-> Substitution (AST NameBinder sig) l l
-> AST NameBinder sig l
-> AST NameBinder sig l
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope l
scope' Substitution (AST NameBinder sig) l l
rename AST NameBinder sig l
body)
  | Bool
otherwise =
      -- The name is fresh here, so the body already /is/ a term of the extended
      -- scope; the coercion says exactly that, and is the same one
      -- 'Foil.withRefreshed' performs on its own fast path.
      NameBinder n l
-> (DExt n (ZonkAny 0) => NameBinder n (ZonkAny 0) -> r) -> r
forall (n :: S) (l :: S) (n' :: S) (l' :: S) r.
NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
unsafeAssertFresh NameBinder n l
binder ((DExt n (ZonkAny 0) => NameBinder n (ZonkAny 0) -> r) -> r)
-> (DExt n (ZonkAny 0) => NameBinder n (ZonkAny 0) -> r) -> r
forall a b. (a -> b) -> a -> b
$ \NameBinder n (ZonkAny 0)
binder' -> NameBinder n (ZonkAny 0) -> AST NameBinder sig (ZonkAny 0) -> r
forall (l :: S).
DExt n l =>
NameBinder n l -> AST NameBinder sig l -> r
k NameBinder n (ZonkAny 0)
binder' (AST NameBinder sig l -> AST NameBinder sig (ZonkAny 0)
forall a b. a -> b
unsafeCoerce AST NameBinder sig l
body)

-- | Go under two scoped terms that stand for /one/ variable.
--
-- A Π-type and a λ over a shape each carry a tope scope beside the body, under
-- what the user wrote as a single binder. On free-foil each 'ScopedAST' has its
-- own 'NameBinder', so the second is instantiated with the first's name: they
-- behave as two abstractions over one argument, as they did before.
withScopedT2
  :: Foil.Distinct n
  => Foil.Scope n
  -> ScopedTermT n
  -> ScopedTermT n
  -> (forall l. Foil.DExt n l => NameBinder n l -> TermT l -> TermT l -> r)
  -> r
withScopedT2 :: forall (n :: S) r.
Distinct n =>
Scope n
-> ScopedTermT n
-> ScopedTermT n
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> TermT l -> TermT l -> r)
-> r
withScopedT2 Scope n
scope ScopedTermT n
scoped1 ScopedTermT n
scoped2 forall (l :: S).
DExt n l =>
NameBinder n l -> TermT l -> TermT l -> r
k =
  Scope n
-> ScopedTermT n
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> AST NameBinder (AnnSig TypeInfo TermSig) l -> r)
-> r
forall (sig :: * -> * -> *) (n :: S) r.
(Bifunctor sig, Distinct n) =>
Scope n
-> ScopedAST NameBinder sig n
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> AST NameBinder sig l -> r)
-> r
withScopedT Scope n
scope ScopedTermT n
scoped1 ((forall (l :: S).
  DExt n l =>
  NameBinder n l -> AST NameBinder (AnnSig TypeInfo TermSig) l -> r)
 -> r)
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> AST NameBinder (AnnSig TypeInfo TermSig) l -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body1 ->
    NameBinder n l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> r
forall (l :: S).
DExt n l =>
NameBinder n l -> TermT l -> TermT l -> r
k NameBinder n l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body1 (Scope l
-> Name l
-> ScopedTermT n
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
Scope l
-> Name l -> ScopedAST NameBinder sig n -> AST NameBinder sig l
openWith (NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope) (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder) ScopedTermT n
scoped2)

-- | Open a scoped term with a name that is already in scope.
--
-- Generic in the signature, so that a λ's (untyped) body and the codomain of the
-- Π it is checked against can be opened under one and the same binder.
openWith
  :: (Bifunctor sig, Foil.DExt n l)
  => Foil.Scope l -> Foil.Name l -> ScopedAST NameBinder sig n -> AST NameBinder sig l
openWith :: forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
Scope l
-> Name l -> ScopedAST NameBinder sig n -> AST NameBinder sig l
openWith Scope l
scope Name l
name (ScopedAST NameBinder n l
binder AST NameBinder sig l
body) =
  Scope l
-> Substitution (AST NameBinder sig) l l
-> AST NameBinder sig l
-> AST NameBinder sig l
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope l
scope (Substitution (AST NameBinder sig) n l
-> NameBinder n l
-> Name l
-> Substitution (AST NameBinder sig) l l
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
Foil.addRename (Substitution (AST NameBinder sig) n n
-> Substitution (AST NameBinder sig) n l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST NameBinder sig) n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst) NameBinder n l
binder Name l
name) AST NameBinder sig l
body

-- | Replace a /free/ name by a term.
--
-- A section's assumption is a free name at the top level, and closing the section
-- abstracts it out of the definitions that use it; this is how those definitions
-- are rewritten. free-foil's substitutions are keyed by a binder, so the map is
-- built directly.
substituteName
  :: Foil.Distinct n
  => Foil.Scope n -> Foil.Name n -> TermT n -> TermT n -> TermT n
substituteName :: forall (n :: S).
Distinct n =>
Scope n -> Name n -> TermT n -> TermT n -> TermT n
substituteName Scope n
scope Name n
name TermT n
value =
  Scope n -> Substitution TermT n n -> TermT n -> TermT n
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution TermT i o -> TermT i -> TermT o
substituteT Scope n
scope (IntMap (TermT n) -> Substitution TermT n n
forall (e :: S -> *) (i :: S) (o :: S).
IntMap (e o) -> Substitution e i o
UnsafeSubstitution (Int -> TermT n -> IntMap (TermT n)
forall a. Int -> a -> IntMap a
IntMap.singleton (Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
name) TermT n
value))

-- | Abstract a free name out of a term: the binder the continuation receives binds
-- what the name stood for.
--
-- The name stays in the scope index (a scope only ever grows), but the term no
-- longer mentions it, which is what makes the resulting Π or λ closed over it.
abstractName
  :: Foil.Distinct n
  => Foil.Scope n
  -> Foil.Name n
  -> TermT n
  -> (forall l. Foil.DExt n l => NameBinder n l -> TermT l -> r)
  -> r
abstractName :: forall (n :: S) r.
Distinct n =>
Scope n
-> Name n
-> TermT n
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT l -> r)
-> r
abstractName Scope n
scope Name n
name TermT n
term forall (l :: S). DExt n l => NameBinder n l -> TermT l -> r
k =
  Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> r) -> r)
-> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
    let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
        term' :: TermT l
term' = Scope l -> Name l -> TermT l -> TermT l -> TermT l
forall (n :: S).
Distinct n =>
Scope n -> Name n -> TermT n -> TermT n -> TermT n
substituteName Scope l
scope' (Name n -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Name n
name) (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))
                  (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
term)
     in NameBinder n l -> TermT l -> r
forall (l :: S). DExt n l => NameBinder n l -> TermT l -> r
k NameBinder n l
binder TermT l
term'

-- | Instantiate a scoped term with a term: the successor of @substituteT x scope@.
instantiateT :: Foil.Distinct n => Foil.Scope n -> ScopedTermT n -> TermT n -> TermT n
instantiateT :: forall (n :: S).
Distinct n =>
Scope n -> ScopedTermT n -> TermT n -> TermT n
instantiateT Scope n
scope (ScopedAST NameBinder n l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body) TermT n
arg =
  Scope n
-> Substitution TermT l n
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> TermT n
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution TermT i o -> TermT i -> TermT o
substituteT Scope n
scope (Substitution TermT n n
-> NameBinder n l -> TermT n -> Substitution TermT l n
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
Foil.addSubst Substitution TermT n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst NameBinder n l
binder TermT n
arg) AST NameBinder (AnnSig TypeInfo TermSig) l
body

-- | Instantiate a scoped /untyped/ term. There are no memoised normal forms to
-- invalidate, so this is free-foil's own substitution.
instantiateUntyped :: Foil.Distinct n => Foil.Scope n -> ScopedTerm n -> Term n -> Term n
instantiateUntyped :: forall (n :: S).
Distinct n =>
Scope n -> ScopedTerm n -> Term n -> Term n
instantiateUntyped Scope n
scope (ScopedAST NameBinder n l
binder AST NameBinder (AnnSig SrcPos TermSig) l
body) Term n
arg =
  Scope n
-> Substitution (AST NameBinder (AnnSig SrcPos TermSig)) l n
-> AST NameBinder (AnnSig SrcPos TermSig) l
-> Term n
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope n
scope (Substitution (AST NameBinder (AnnSig SrcPos TermSig)) n n
-> NameBinder n l
-> Term n
-> Substitution (AST NameBinder (AnnSig SrcPos TermSig)) l n
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
Foil.addSubst Substitution (AST NameBinder (AnnSig SrcPos TermSig)) n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst NameBinder n l
binder Term n
arg) AST NameBinder (AnnSig SrcPos TermSig) l
body

-- | Substitution that invalidates the memoised normal forms of every node it
-- rebuilds, and substitutes into each node's type.
--
-- A renaming ('substitute') keeps the memo, since a renamed term reduces exactly
-- as the original does. A real substitution does not: a variable is in weak head
-- normal form, and what replaces it need not be. This is one traversal, as
-- substituting and invalidating separately was two.
substituteT
  :: Foil.Distinct o
  => Foil.Scope o
  -> Foil.Substitution TermT i o
  -> TermT i
  -> TermT o
substituteT :: forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution TermT i o -> TermT i -> TermT o
substituteT Scope o
scope Substitution TermT i o
subst TermT i
term = Scope o -> Substitution TermT i o -> TermT i -> TermT o
forall (i' :: S) (o' :: S).
Distinct o' =>
Scope o' -> Substitution TermT i' o' -> TermT i' -> TermT o'
go Scope o
scope Substitution TermT i o
subst TermT i
term
  where
    go
      :: forall i' o'. Foil.Distinct o'
      => Foil.Scope o' -> Foil.Substitution TermT i' o' -> TermT i' -> TermT o'
    go :: forall (i' :: S) (o' :: S).
Distinct o' =>
Scope o' -> Substitution TermT i' o' -> TermT i' -> TermT o'
go Scope o'
_ Substitution TermT i' o'
subst' (Var Name i'
name) = Substitution TermT i' o'
-> Name i' -> AST NameBinder (AnnSig TypeInfo TermSig) o'
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
Foil.lookupSubst Substitution TermT i' o'
subst' Name i'
name
    go Scope o'
scope' Substitution TermT i' o'
subst' (Node (AnnSig TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) i')
info TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) i')
  (AST NameBinder (AnnSig TypeInfo TermSig) i')
sig)) = AnnSig
  TypeInfo
  TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
  (AST NameBinder (AnnSig TypeInfo TermSig) o')
-> AST NameBinder (AnnSig TypeInfo TermSig) o'
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node (TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) o')
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
     (AST NameBinder (AnnSig TypeInfo TermSig) o')
-> AnnSig
     TypeInfo
     TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
     (AST NameBinder (AnnSig TypeInfo TermSig) o')
forall (ann :: * -> *) (sig :: * -> * -> *) scope term.
ann term -> sig scope term -> AnnSig ann sig scope term
AnnSig TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) o')
info' TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
  (AST NameBinder (AnnSig TypeInfo TermSig) o')
sig')
      where
        info' :: TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) o')
info' = TypeInfo
          { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) o'
infoType = Scope o'
-> Substitution TermT i' o'
-> AST NameBinder (AnnSig TypeInfo TermSig) i'
-> AST NameBinder (AnnSig TypeInfo TermSig) o'
forall (i' :: S) (o' :: S).
Distinct o' =>
Scope o' -> Substitution TermT i' o' -> TermT i' -> TermT o'
go Scope o'
scope' Substitution TermT i' o'
subst' (TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) i')
-> AST NameBinder (AnnSig TypeInfo TermSig) i'
forall term. TypeInfo term -> term
infoType TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) i')
info)
          , infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) o')
infoWHNF = Maybe (AST NameBinder (AnnSig TypeInfo TermSig) o')
forall a. Maybe a
Nothing
          , infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) o')
infoNF   = Maybe (AST NameBinder (AnnSig TypeInfo TermSig) o')
forall a. Maybe a
Nothing
          }
        sig' :: TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
  (AST NameBinder (AnnSig TypeInfo TermSig) o')
sig' = (ScopedAST NameBinder (AnnSig TypeInfo TermSig) i'
 -> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
-> (AST NameBinder (AnnSig TypeInfo TermSig) i'
    -> AST NameBinder (AnnSig TypeInfo TermSig) o')
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) i')
     (AST NameBinder (AnnSig TypeInfo TermSig) i')
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
     (AST NameBinder (AnnSig TypeInfo TermSig) o')
forall a b c d. (a -> b) -> (c -> d) -> TermSig a c -> TermSig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST NameBinder (AnnSig TypeInfo TermSig) i'
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o'
goScoped (Scope o'
-> Substitution TermT i' o'
-> AST NameBinder (AnnSig TypeInfo TermSig) i'
-> AST NameBinder (AnnSig TypeInfo TermSig) o'
forall (i' :: S) (o' :: S).
Distinct o' =>
Scope o' -> Substitution TermT i' o' -> TermT i' -> TermT o'
go Scope o'
scope' Substitution TermT i' o'
subst') TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) i')
  (AST NameBinder (AnnSig TypeInfo TermSig) i')
sig

        goScoped :: ScopedAST NameBinder (AnnSig TypeInfo TermSig) i'
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o'
goScoped (ScopedAST NameBinder i' l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body) =
          Scope o'
-> Name l
-> (forall (o' :: S).
    DExt o' o' =>
    NameBinder o' o'
    -> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o'
forall (o :: S) (i :: S) r.
Distinct o =>
Scope o
-> Name i
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)
-> r
Foil.withRefreshed Scope o'
scope' (NameBinder i' l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder i' l
binder) ((forall (o' :: S).
  DExt o' o' =>
  NameBinder o' o'
  -> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
 -> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
-> (forall (o' :: S).
    DExt o' o' =>
    NameBinder o' o'
    -> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o')
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o'
forall a b. (a -> b) -> a -> b
$ \NameBinder o' o'
binder' ->
            let scope'' :: Scope o'
scope'' = NameBinder o' o' -> Scope o' -> Scope o'
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder o' o'
binder' Scope o'
scope'
                subst'' :: Substitution TermT l o'
subst'' = Substitution TermT i' o'
-> NameBinder i' l -> Name o' -> Substitution TermT l o'
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
Foil.addRename (Substitution TermT i' o' -> Substitution TermT i' o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution TermT i' o'
subst') NameBinder i' l
binder (NameBinder o' o' -> Name o'
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder o' o'
binder')
             in NameBinder o' o'
-> AST NameBinder (AnnSig TypeInfo TermSig) o'
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) o'
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder o' o'
binder' (Scope o'
-> Substitution TermT l o'
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) o'
forall (i' :: S) (o' :: S).
Distinct o' =>
Scope o' -> Substitution TermT i' o' -> TermT i' -> TermT o'
go Scope o'
scope'' Substitution TermT l o'
subst'' AST NameBinder (AnnSig TypeInfo TermSig) l
body)

-- * Pattern synonyms
--
-- One per constructor, as @makePatternsAll@ generated before. A @scope@ field is
-- a 'ScopedTermT', so going under a binder means matching on 'ScopedAST', which
-- is where the existential scope index appears.

pattern $mUniverseT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bUniverseT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
UniverseT info = Node (AnnSig info UniverseF)
pattern $mUniverseCubeT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bUniverseCubeT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
UniverseCubeT info = Node (AnnSig info UniverseCubeF)
pattern $mUniverseTopeT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bUniverseTopeT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
UniverseTopeT info = Node (AnnSig info UniverseTopeF)
pattern $mCubeUnitT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bCubeUnitT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeUnitT info = Node (AnnSig info CubeUnitF)
pattern $mCubeUnitStarT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bCubeUnitStarT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeUnitStarT info = Node (AnnSig info CubeUnitStarF)
pattern $mCube2T :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bCube2T :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
Cube2T info = Node (AnnSig info Cube2F)
pattern $mCube2_0T :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bCube2_0T :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
Cube2_0T info = Node (AnnSig info Cube2_0F)
pattern $mCube2_1T :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bCube2_1T :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
Cube2_1T info = Node (AnnSig info Cube2_1F)
pattern $mCubeIT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bCubeIT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeIT info = Node (AnnSig info CubeIF)
pattern $mCubeI_0T :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bCubeI_0T :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeI_0T info = Node (AnnSig info CubeI_0F)
pattern $mCubeI_1T :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bCubeI_1T :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeI_1T info = Node (AnnSig info CubeI_1F)
pattern $mCubeProductT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bCubeProductT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeProductT info l r = Node (AnnSig info (CubeProductF l r))
pattern $mCubeFlipT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bCubeFlipT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeFlipT info t = Node (AnnSig info (CubeFlipF t))
pattern $mCubeUnflipT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bCubeUnflipT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeUnflipT info t = Node (AnnSig info (CubeUnflipF t))
pattern $mCubeSupT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bCubeSupT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeSupT info l r = Node (AnnSig info (CubeSupF l r))
pattern $mCubeInfT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bCubeInfT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeInfT info l r = Node (AnnSig info (CubeInfF l r))
pattern $mTopeTopT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bTopeTopT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
TopeTopT info = Node (AnnSig info TopeTopF)
pattern $mTopeBottomT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bTopeBottomT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
TopeBottomT info = Node (AnnSig info TopeBottomF)
pattern $mTopeEQT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bTopeEQT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeEQT info l r = Node (AnnSig info (TopeEQF l r))
pattern $mTopeLEQT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bTopeLEQT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeLEQT info l r = Node (AnnSig info (TopeLEQF l r))
pattern $mTopeAndT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bTopeAndT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeAndT info l r = Node (AnnSig info (TopeAndF l r))
pattern $mTopeOrT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bTopeOrT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeOrT info l r = Node (AnnSig info (TopeOrF l r))
pattern $mTopeInvT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bTopeInvT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeInvT info t = Node (AnnSig info (TopeInvF t))
pattern $mTopeUninvT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bTopeUninvT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeUninvT info t = Node (AnnSig info (TopeUninvF t))
pattern $mRecBottomT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bRecBottomT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
RecBottomT info = Node (AnnSig info RecBottomF)
pattern $mRecOrT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> [(AST binder (AnnSig ann TermSig) n,
         AST binder (AnnSig ann TermSig) n)]
    -> r)
-> ((# #) -> r)
-> r
$bRecOrT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> [(AST binder (AnnSig ann TermSig) n,
     AST binder (AnnSig ann TermSig) n)]
-> AST binder (AnnSig ann TermSig) n
RecOrT info rs = Node (AnnSig info (RecOrF rs))
pattern $mTypeFunT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> Binder
    -> TModality
    -> AST binder (AnnSig ann TermSig) n
    -> Maybe (ScopedAST binder (AnnSig ann TermSig) n)
    -> ScopedAST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bTypeFunT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> Maybe (ScopedAST binder (AnnSig ann TermSig) n)
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeFunT info orig md param mtope ret = Node (AnnSig info (TypeFunF orig md param mtope ret))
pattern $mTypeSigmaT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> Binder
    -> TModality
    -> AST binder (AnnSig ann TermSig) n
    -> ScopedAST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bTypeSigmaT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeSigmaT info orig md a b = Node (AnnSig info (TypeSigmaF orig md a b))
pattern $mTypeIdT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> Maybe (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bTypeIdT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeIdT info a mtA b = Node (AnnSig info (TypeIdF a mtA b))
pattern $mAppT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bAppT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
AppT info f x = Node (AnnSig info (AppF f x))
pattern $mLetT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> Binder
    -> Maybe (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> ScopedAST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bLetT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
LetT info orig mparam val body = Node (AnnSig info (LetF orig mparam val body))
pattern $mLambdaT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> Binder
    -> Maybe
         (LambdaParam
            (ScopedAST binder (AnnSig ann TermSig) n)
            (AST binder (AnnSig ann TermSig) n))
    -> ScopedAST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bLambdaT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> Maybe
     (LambdaParam
        (ScopedAST binder (AnnSig ann TermSig) n)
        (AST binder (AnnSig ann TermSig) n))
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
LambdaT info orig mparam body = Node (AnnSig info (LambdaF orig mparam body))
pattern $mPairT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bPairT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
PairT info l r = Node (AnnSig info (PairF l r))
pattern $mFirstT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bFirstT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
FirstT info t = Node (AnnSig info (FirstF t))
pattern $mSecondT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bSecondT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
SecondT info t = Node (AnnSig info (SecondF t))
pattern $mReflT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> Maybe
         (AST binder (AnnSig ann TermSig) n,
          Maybe (AST binder (AnnSig ann TermSig) n))
    -> r)
-> ((# #) -> r)
-> r
$bReflT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Maybe
     (AST binder (AnnSig ann TermSig) n,
      Maybe (AST binder (AnnSig ann TermSig) n))
-> AST binder (AnnSig ann TermSig) n
ReflT info mx = Node (AnnSig info (ReflF mx))
pattern $mIdJT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bIdJT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
IdJT info a b c d e f = Node (AnnSig info (IdJF a b c d e f))
pattern $mMatchT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> Maybe (AST binder (AnnSig ann TermSig) n)
    -> [(VarIdent, AST binder (AnnSig ann TermSig) n)]
    -> r)
-> ((# #) -> r)
-> r
$bMatchT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> [(VarIdent, AST binder (AnnSig ann TermSig) n)]
-> AST binder (AnnSig ann TermSig) n
MatchT info scrut mmotive branches = Node (AnnSig info (MatchF scrut mmotive branches))
pattern $mMatchArmT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> Binder -> ScopedAST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bMatchArmT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
MatchArmT info orig arm = Node (AnnSig info (MatchArmF orig arm))
pattern $mUnitT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bUnitT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
UnitT info = Node (AnnSig info UnitF)
pattern $mTypeUnitT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> r)
-> ((# #) -> r)
-> r
$bTypeUnitT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
TypeUnitT info = Node (AnnSig info TypeUnitF)
pattern $mTypeAscT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bTypeAscT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeAscT info term ty = Node (AnnSig info (TypeAscF term ty))
pattern $mTypeRestrictedT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> [(AST binder (AnnSig ann TermSig) n,
         AST binder (AnnSig ann TermSig) n)]
    -> r)
-> ((# #) -> r)
-> r
$bTypeRestrictedT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> [(AST binder (AnnSig ann TermSig) n,
     AST binder (AnnSig ann TermSig) n)]
-> AST binder (AnnSig ann TermSig) n
TypeRestrictedT info ty rs = Node (AnnSig info (TypeRestrictedF ty rs))
pattern $mTypeModalT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> TModality -> AST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bTypeModalT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeModalT info md ty = Node (AnnSig info (TypeModalF md ty))
pattern $mModAppT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> TModality -> AST binder (AnnSig ann TermSig) n -> r)
-> ((# #) -> r)
-> r
$bModAppT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
ModAppT info md t = Node (AnnSig info (ModAppF md t))
pattern $mModExtractT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> TModality
    -> TModality
    -> AST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bModExtractT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> TModality
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
ModExtractT info app inn t = Node (AnnSig info (ModExtractF app inn t))
pattern $mLetModT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n)
    -> Binder
    -> TModality
    -> TModality
    -> Maybe (AST binder (AnnSig ann TermSig) n)
    -> Maybe (AST binder (AnnSig ann TermSig) n)
    -> AST binder (AnnSig ann TermSig) n
    -> ScopedAST binder (AnnSig ann TermSig) n
    -> r)
-> ((# #) -> r)
-> r
$bLetModT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> TModality
-> TModality
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
LetModT info orig app inn mparam mmotive val body = Node (AnnSig info (LetModF orig app inn mparam mmotive val body))
pattern $mHoleT :: forall {r} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n
-> (ann (AST binder (AnnSig ann TermSig) n) -> Maybe VarIdent -> r)
-> ((# #) -> r)
-> r
$bHoleT :: forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Maybe VarIdent -> AST binder (AnnSig ann TermSig) n
HoleT info mname = Node (AnnSig info (HoleF mname))

{-# COMPLETE Var, UniverseT, UniverseCubeT, UniverseTopeT, CubeUnitT,
  CubeUnitStarT, Cube2T, Cube2_0T, Cube2_1T, CubeIT, CubeI_0T, CubeI_1T,
  CubeProductT, CubeFlipT, CubeUnflipT, CubeSupT, CubeInfT, TopeTopT, TopeBottomT,
  TopeEQT, TopeLEQT, TopeAndT, TopeOrT, TopeInvT, TopeUninvT, RecBottomT, RecOrT,
  TypeFunT, TypeSigmaT, TypeIdT, AppT, LetT, LambdaT, PairT, FirstT, SecondT,
  ReflT, IdJT, MatchT, MatchArmT, UnitT, TypeUnitT, TypeAscT, TypeRestrictedT,
  TypeModalT, ModAppT, ModExtractT, LetModT, HoleT #-}

-- ** Untyped patterns
--
-- The same constructors on 'Term', for the surface conversions and the printer.
--
-- Each goes through 'UntypedNode', which ignores a node's position on the way in
-- and leaves it unset on the way out. So the checker builds and matches untyped
-- terms exactly as it did before terms carried a position, and the conversion
-- from the surface syntax ('atSrcPos') is the only place that puts a real one on.

-- | An untyped node, taken and made without regard for where it was written.
pattern UntypedNode :: TermSig (ScopedTerm n) (Term n) -> Term n
pattern $mUntypedNode :: forall {r} {n :: S}.
Term n
-> (TermSig (ScopedTerm n) (Term n) -> r) -> ((# #) -> r) -> r
$bUntypedNode :: forall (n :: S). TermSig (ScopedTerm n) (Term n) -> Term n
UntypedNode sig <- Node (AnnSig _ sig) where
  UntypedNode TermSig (ScopedTerm n) (Term n)
sig = AnnSig SrcPos TermSig (ScopedTerm n) (Term n) -> Term n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node (SrcPos (Term n)
-> TermSig (ScopedTerm n) (Term n)
-> AnnSig SrcPos TermSig (ScopedTerm n) (Term n)
forall (ann :: * -> *) (sig :: * -> * -> *) scope term.
ann term -> sig scope term -> AnnSig ann sig scope term
AnnSig SrcPos (Term n)
forall term. SrcPos term
noSrcPos TermSig (ScopedTerm n) (Term n)
sig)

{-# COMPLETE Var, UntypedNode #-}

pattern $mUniverse :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bUniverse :: forall {n :: S}. Term n
Universe = UntypedNode UniverseF
pattern $mUniverseCube :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bUniverseCube :: forall {n :: S}. Term n
UniverseCube = UntypedNode UniverseCubeF
pattern $mUniverseTope :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bUniverseTope :: forall {n :: S}. Term n
UniverseTope = UntypedNode UniverseTopeF
pattern $mCubeUnit :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bCubeUnit :: forall {n :: S}. Term n
CubeUnit = UntypedNode CubeUnitF
pattern $mCubeUnitStar :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bCubeUnitStar :: forall {n :: S}. Term n
CubeUnitStar = UntypedNode CubeUnitStarF
pattern $mCube2 :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bCube2 :: forall {n :: S}. Term n
Cube2 = UntypedNode Cube2F
pattern $mCube2_0 :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bCube2_0 :: forall {n :: S}. Term n
Cube2_0 = UntypedNode Cube2_0F
pattern $mCube2_1 :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bCube2_1 :: forall {n :: S}. Term n
Cube2_1 = UntypedNode Cube2_1F
pattern $mCubeI :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bCubeI :: forall {n :: S}. Term n
CubeI = UntypedNode CubeIF
pattern $mCubeI_0 :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bCubeI_0 :: forall {n :: S}. Term n
CubeI_0 = UntypedNode CubeI_0F
pattern $mCubeI_1 :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bCubeI_1 :: forall {n :: S}. Term n
CubeI_1 = UntypedNode CubeI_1F
pattern $mCubeProduct :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bCubeProduct :: forall {n :: S}. Term n -> Term n -> Term n
CubeProduct l r = UntypedNode (CubeProductF l r)
pattern $mCubeFlip :: forall {r} {n :: S}. Term n -> (Term n -> r) -> ((# #) -> r) -> r
$bCubeFlip :: forall {n :: S}. Term n -> Term n
CubeFlip t = UntypedNode (CubeFlipF t)
pattern $mCubeUnflip :: forall {r} {n :: S}. Term n -> (Term n -> r) -> ((# #) -> r) -> r
$bCubeUnflip :: forall {n :: S}. Term n -> Term n
CubeUnflip t = UntypedNode (CubeUnflipF t)
pattern $mCubeSup :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bCubeSup :: forall {n :: S}. Term n -> Term n -> Term n
CubeSup l r = UntypedNode (CubeSupF l r)
pattern $mCubeInf :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bCubeInf :: forall {n :: S}. Term n -> Term n -> Term n
CubeInf l r = UntypedNode (CubeInfF l r)
pattern $mTopeTop :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bTopeTop :: forall {n :: S}. Term n
TopeTop = UntypedNode TopeTopF
pattern $mTopeBottom :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bTopeBottom :: forall {n :: S}. Term n
TopeBottom = UntypedNode TopeBottomF
pattern $mTopeEQ :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bTopeEQ :: forall {n :: S}. Term n -> Term n -> Term n
TopeEQ l r = UntypedNode (TopeEQF l r)
pattern $mTopeLEQ :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bTopeLEQ :: forall {n :: S}. Term n -> Term n -> Term n
TopeLEQ l r = UntypedNode (TopeLEQF l r)
pattern $mTopeAnd :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bTopeAnd :: forall {n :: S}. Term n -> Term n -> Term n
TopeAnd l r = UntypedNode (TopeAndF l r)
pattern $mTopeOr :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bTopeOr :: forall {n :: S}. Term n -> Term n -> Term n
TopeOr l r = UntypedNode (TopeOrF l r)
pattern $mTopeInv :: forall {r} {n :: S}. Term n -> (Term n -> r) -> ((# #) -> r) -> r
$bTopeInv :: forall {n :: S}. Term n -> Term n
TopeInv t = UntypedNode (TopeInvF t)
pattern $mTopeUninv :: forall {r} {n :: S}. Term n -> (Term n -> r) -> ((# #) -> r) -> r
$bTopeUninv :: forall {n :: S}. Term n -> Term n
TopeUninv t = UntypedNode (TopeUninvF t)
pattern $mRecBottom :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bRecBottom :: forall {n :: S}. Term n
RecBottom = UntypedNode RecBottomF
pattern $mRecOr :: forall {r} {n :: S}.
Term n -> ([(Term n, Term n)] -> r) -> ((# #) -> r) -> r
$bRecOr :: forall {n :: S}. [(Term n, Term n)] -> Term n
RecOr rs = UntypedNode (RecOrF rs)
pattern $mTypeFun :: forall {r} {n :: S}.
Term n
-> (Binder
    -> TModality
    -> Term n
    -> Maybe (ScopedTerm n)
    -> ScopedTerm n
    -> r)
-> ((# #) -> r)
-> r
$bTypeFun :: forall {n :: S}.
Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
TypeFun orig md param mtope ret = UntypedNode (TypeFunF orig md param mtope ret)
pattern $mTypeSigma :: forall {r} {n :: S}.
Term n
-> (Binder -> TModality -> Term n -> ScopedTerm n -> r)
-> ((# #) -> r)
-> r
$bTypeSigma :: forall {n :: S}.
Binder -> TModality -> Term n -> ScopedTerm n -> Term n
TypeSigma orig md a b = UntypedNode (TypeSigmaF orig md a b)
pattern $mTypeId :: forall {r} {n :: S}.
Term n
-> (Term n -> Maybe (Term n) -> Term n -> r) -> ((# #) -> r) -> r
$bTypeId :: forall {n :: S}. Term n -> Maybe (Term n) -> Term n -> Term n
TypeId a mtA b = UntypedNode (TypeIdF a mtA b)
pattern $mApp :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bApp :: forall {n :: S}. Term n -> Term n -> Term n
App f x = UntypedNode (AppF f x)
pattern $mLet :: forall {r} {n :: S}.
Term n
-> (Binder -> Maybe (Term n) -> Term n -> ScopedTerm n -> r)
-> ((# #) -> r)
-> r
$bLet :: forall {n :: S}.
Binder -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n
Let orig mparam val body = UntypedNode (LetF orig mparam val body)
pattern $mLambda :: forall {r} {n :: S}.
Term n
-> (Binder
    -> Maybe (LambdaParam (ScopedTerm n) (Term n))
    -> ScopedTerm n
    -> r)
-> ((# #) -> r)
-> r
$bLambda :: forall {n :: S}.
Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
Lambda orig mparam body = UntypedNode (LambdaF orig mparam body)
pattern $mPair :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bPair :: forall {n :: S}. Term n -> Term n -> Term n
Pair l r = UntypedNode (PairF l r)
pattern $mFirst :: forall {r} {n :: S}. Term n -> (Term n -> r) -> ((# #) -> r) -> r
$bFirst :: forall {n :: S}. Term n -> Term n
First t = UntypedNode (FirstF t)
pattern $mSecond :: forall {r} {n :: S}. Term n -> (Term n -> r) -> ((# #) -> r) -> r
$bSecond :: forall {n :: S}. Term n -> Term n
Second t = UntypedNode (SecondF t)
pattern $mRefl :: forall {r} {n :: S}.
Term n
-> (Maybe (Term n, Maybe (Term n)) -> r) -> ((# #) -> r) -> r
$bRefl :: forall {n :: S}. Maybe (Term n, Maybe (Term n)) -> Term n
Refl mx = UntypedNode (ReflF mx)
pattern $mIdJ :: forall {r} {n :: S}.
Term n
-> (Term n -> Term n -> Term n -> Term n -> Term n -> Term n -> r)
-> ((# #) -> r)
-> r
$bIdJ :: forall {n :: S}.
Term n -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
IdJ a b c d e f = UntypedNode (IdJF a b c d e f)
pattern $mMatch :: forall {r} {n :: S}.
Term n
-> (Term n -> Maybe (Term n) -> [(VarIdent, Term n)] -> r)
-> ((# #) -> r)
-> r
$bMatch :: forall {n :: S}.
Term n -> Maybe (Term n) -> [(VarIdent, Term n)] -> Term n
Match scrut mmotive branches = UntypedNode (MatchF scrut mmotive branches)
pattern $mMatchArm :: forall {r} {n :: S}.
Term n -> (Binder -> ScopedTerm n -> r) -> ((# #) -> r) -> r
$bMatchArm :: forall {n :: S}. Binder -> ScopedTerm n -> Term n
MatchArm orig arm = UntypedNode (MatchArmF orig arm)
pattern $mUnit :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bUnit :: forall {n :: S}. Term n
Unit = UntypedNode UnitF
pattern $mTypeUnit :: forall {r} {n :: S}. Term n -> ((# #) -> r) -> ((# #) -> r) -> r
$bTypeUnit :: forall {n :: S}. Term n
TypeUnit = UntypedNode TypeUnitF
pattern $mTypeAsc :: forall {r} {n :: S}.
Term n -> (Term n -> Term n -> r) -> ((# #) -> r) -> r
$bTypeAsc :: forall {n :: S}. Term n -> Term n -> Term n
TypeAsc term ty = UntypedNode (TypeAscF term ty)
pattern $mTypeRestricted :: forall {r} {n :: S}.
Term n -> (Term n -> [(Term n, Term n)] -> r) -> ((# #) -> r) -> r
$bTypeRestricted :: forall {n :: S}. Term n -> [(Term n, Term n)] -> Term n
TypeRestricted ty rs = UntypedNode (TypeRestrictedF ty rs)
pattern $mTypeModal :: forall {r} {n :: S}.
Term n -> (TModality -> Term n -> r) -> ((# #) -> r) -> r
$bTypeModal :: forall {n :: S}. TModality -> Term n -> Term n
TypeModal md ty = UntypedNode (TypeModalF md ty)
pattern $mModApp :: forall {r} {n :: S}.
Term n -> (TModality -> Term n -> r) -> ((# #) -> r) -> r
$bModApp :: forall {n :: S}. TModality -> Term n -> Term n
ModApp md t = UntypedNode (ModAppF md t)
pattern $mModExtract :: forall {r} {n :: S}.
Term n
-> (TModality -> TModality -> Term n -> r) -> ((# #) -> r) -> r
$bModExtract :: forall {n :: S}. TModality -> TModality -> Term n -> Term n
ModExtract app inn t = UntypedNode (ModExtractF app inn t)
pattern $mLetMod :: forall {r} {n :: S}.
Term n
-> (Binder
    -> TModality
    -> TModality
    -> Maybe (Term n)
    -> Maybe (Term n)
    -> Term n
    -> ScopedTerm n
    -> r)
-> ((# #) -> r)
-> r
$bLetMod :: forall {n :: S}.
Binder
-> TModality
-> TModality
-> Maybe (Term n)
-> Maybe (Term n)
-> Term n
-> ScopedTerm n
-> Term n
LetMod orig app inn mparam mmotive val body = UntypedNode (LetModF orig app inn mparam mmotive val body)
pattern $mHole :: forall {r} {n :: S}.
Term n -> (Maybe VarIdent -> r) -> ((# #) -> r) -> r
$bHole :: forall {n :: S}. Maybe VarIdent -> Term n
Hole mname = UntypedNode (HoleF mname)

{-# COMPLETE Var, Universe, UniverseCube, UniverseTope, CubeUnit, CubeUnitStar,
  Cube2, Cube2_0, Cube2_1, CubeI, CubeI_0, CubeI_1, CubeProduct, CubeFlip,
  CubeUnflip, CubeSup, CubeInf, TopeTop, TopeBottom, TopeEQ, TopeLEQ, TopeAnd,
  TopeOr, TopeInv, TopeUninv, RecBottom, RecOr, TypeFun, TypeSigma, TypeId, App,
  Let, Lambda, Pair, First, Second, Refl, IdJ, Match, MatchArm, Unit, TypeUnit,
  TypeAsc, TypeRestricted, TypeModal, ModApp, ModExtract, LetMod, Hole #-}

-- * Closed constants
--
-- They are closed, so they generalise over the scope index: no shifting, no
-- per-scope construction. (The universe is still the 30-deep chain of the old
-- representation, ending in a bottom; making it a real level-polymorphic
-- universe is a separate FIXME.)

universeT :: TermT n
universeT :: forall (n :: S). TermT n
universeT = (TermT n -> TermT n) -> TermT n -> [TermT n]
forall a. (a -> a) -> a -> [a]
iterate TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
f ([Char] -> TermT n
forall a. HasCallStack => [Char] -> a
error [Char]
"going too high up the universe levels") [TermT n] -> Int -> TermT n
forall a. HasCallStack => [a] -> Int -> a
!! Int
30
  where
    f :: TermT n -> TermT n
f TermT n
t = TypeInfo (TermT n) -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
UniverseT TypeInfo { infoType :: TermT n
infoType = TermT n
t, infoWHNF :: Maybe (TermT n)
infoWHNF = TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
forall (n :: S). TermT n
universeT, infoNF :: Maybe (TermT n)
infoNF = TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
forall (n :: S). TermT n
universeT }

cubeT :: TermT n
cubeT :: forall (n :: S). TermT n
cubeT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
UniverseCubeT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
universeT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeT }

topeT :: TermT n
topeT :: forall (n :: S). TermT n
topeT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
UniverseTopeT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
universeT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeT }

cubeUnitT :: TermT n
cubeUnitT :: forall (n :: S). TermT n
cubeUnitT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeUnitT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeUnitT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeUnitT }

cubeUnitStarT :: TermT n
cubeUnitStarT :: forall (n :: S). TermT n
cubeUnitStarT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeUnitStarT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeUnitT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeUnitStarT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeUnitStarT }

cube2T :: TermT n
cube2T :: forall (n :: S). TermT n
cube2T = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
Cube2T TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2T, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2T }

cube2_0T :: TermT n
cube2_0T :: forall (n :: S). TermT n
cube2_0T = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
Cube2_0T TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2T, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2_0T, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2_0T }

cube2_1T :: TermT n
cube2_1T :: forall (n :: S). TermT n
cube2_1T = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
Cube2_1T TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2T, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2_1T, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2_1T }

cubeIT :: TermT n
cubeIT :: forall (n :: S). TermT n
cubeIT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeIT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeIT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeIT }

cubeI_0T :: TermT n
cubeI_0T :: forall (n :: S). TermT n
cubeI_0T = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeI_0T TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeIT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeI_0T, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeI_0T }

cubeI_1T :: TermT n
cubeI_1T :: forall (n :: S). TermT n
cubeI_1T = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
CubeI_1T TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeIT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeI_1T, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cubeI_1T }

topeTopT :: TermT n
topeTopT :: forall (n :: S). TermT n
topeTopT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
TopeTopT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeTopT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeTopT }

topeBottomT :: TermT n
topeBottomT :: forall (n :: S). TermT n
topeBottomT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
TopeBottomT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeBottomT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeBottomT }

typeUnitT :: TermT n
typeUnitT :: forall (n :: S). TermT n
typeUnitT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
TypeUnitT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
universeT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
typeUnitT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
typeUnitT }

unitT :: TermT n
unitT :: forall (n :: S). TermT n
unitT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
UnitT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
typeUnitT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
unitT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
unitT }

-- | @recBOT@ is its own type: it inhabits every type in a contradictory context.
recBottomT :: TermT n
recBottomT :: forall (n :: S). TermT n
recBottomT = TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
RecBottomT TypeInfo
  { infoType :: AST NameBinder (AnnSig TypeInfo TermSig) n
infoType = AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
recBottomT, infoWHNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoWHNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
recBottomT, infoNF :: Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
infoNF = AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
recBottomT }

-- * Smart constructors
--
-- Each builds the 'TypeInfo' of the node it makes, so the checker never writes a
-- raw @FooT@. A node whose head is already a value ('lambdaT', 'pairT', the type
-- formers) memoises itself as its own WHNF.

-- ** The tope layer

topeEQT :: TermT n -> TermT n -> TermT n
topeEQT :: forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
l TermT n
r = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeEQT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
forall (n :: S). TermT n
topeT) TermT n
l TermT n
r

topeLEQT :: TermT n -> TermT n -> TermT n
topeLEQT :: forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
l TermT n
r = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeLEQT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
forall (n :: S). TermT n
topeT) TermT n
l TermT n
r

topeOrT :: TermT n -> TermT n -> TermT n
topeOrT :: forall (n :: S). TermT n -> TermT n -> TermT n
topeOrT TermT n
l TermT n
r = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeOrT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
forall (n :: S). TermT n
topeT) TermT n
l TermT n
r

topeAndT :: TermT n -> TermT n -> TermT n
topeAndT :: forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT TermT n
l TermT n
r = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeAndT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
forall (n :: S). TermT n
topeT) TermT n
l TermT n
r

topeInvT :: TermT n -> TermT n
topeInvT :: forall (n :: S). TermT n -> TermT n
topeInvT TermT n
t = TypeInfo (TermT n) -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeInvT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo (TermT n -> TModality -> TermT n -> TermT n
forall (n :: S). TermT n -> TModality -> TermT n -> TermT n
typeModalT TermT n
forall (n :: S). TermT n
universeT TModality
Op TermT n
forall (n :: S). TermT n
topeT)) TermT n
t

topeUninvT :: TermT n -> TermT n
topeUninvT :: forall (n :: S). TermT n -> TermT n
topeUninvT TermT n
t = TypeInfo (TermT n) -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TopeUninvT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
forall (n :: S). TermT n
topeT) TermT n
t

-- | An unreduced node of the given type.
topeInfo :: TermT n -> TypeInfo (TermT n)
topeInfo :: forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty = TypeInfo { infoType :: TermT n
infoType = TermT n
ty, infoWHNF :: Maybe (TermT n)
infoWHNF = Maybe (TermT n)
forall a. Maybe a
Nothing, infoNF :: Maybe (TermT n)
infoNF = Maybe (TermT n)
forall a. Maybe a
Nothing }

-- ** Cubes

cubeProductT :: TermT n -> TermT n -> TermT n
cubeProductT :: forall (n :: S). TermT n -> TermT n -> TermT n
cubeProductT TermT n
l TermT n
r = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeProductT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
forall (n :: S). TermT n
cubeT) TermT n
l TermT n
r

cubeFlipT :: TermT n -> TermT n -> TermT n
cubeFlipT :: forall (n :: S). TermT n -> TermT n -> TermT n
cubeFlipT TermT n
cubeTy TermT n
t = TypeInfo (TermT n) -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeFlipT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo (TermT n -> TModality -> TermT n -> TermT n
forall (n :: S). TermT n -> TModality -> TermT n -> TermT n
typeModalT TermT n
forall (n :: S). TermT n
cubeT TModality
Op TermT n
cubeTy)) TermT n
t

cubeUnflipT :: TermT n -> TermT n -> TermT n
cubeUnflipT :: forall (n :: S). TermT n -> TermT n -> TermT n
cubeUnflipT TermT n
cubeTy TermT n
t = TypeInfo (TermT n) -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeUnflipT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
cubeTy) TermT n
t

cubeSupT :: TermT n -> TermT n -> TermT n -> TermT n
cubeSupT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
cubeSupT TermT n
cubeTy TermT n
l TermT n
r = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeSupT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
cubeTy) TermT n
l TermT n
r

cubeInfT :: TermT n -> TermT n -> TermT n -> TermT n
cubeInfT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
cubeInfT TermT n
cubeTy TermT n
l TermT n
r = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
CubeInfT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
cubeTy) TermT n
l TermT n
r

-- ** Types

typeFunT
  :: Binder -> TModality -> TermT n -> Maybe (ScopedTermT n) -> ScopedTermT n
  -> TermT n
typeFunT :: forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT Binder
orig TModality
md TermT n
cube Maybe (ScopedTermT n)
mtope ScopedTermT n
ret = TermT n
t
  where t :: TermT n
t = TypeInfo (TermT n)
-> Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> Maybe (ScopedAST binder (AnnSig ann TermSig) n)
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeFunT (TermT n -> TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TermT n -> TypeInfo (TermT n)
valueInfo TermT n
t TermT n
forall (n :: S). TermT n
universeT) Binder
orig TModality
md TermT n
cube Maybe (ScopedTermT n)
mtope ScopedTermT n
ret

typeSigmaT :: Binder -> TModality -> TermT n -> ScopedTermT n -> TermT n
typeSigmaT :: forall (n :: S).
Binder -> TModality -> TermT n -> ScopedTermT n -> TermT n
typeSigmaT Binder
orig TModality
md TermT n
a ScopedTermT n
b = TermT n
t
  where t :: TermT n
t = TypeInfo (TermT n)
-> Binder -> TModality -> TermT n -> ScopedTermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeSigmaT (TermT n -> TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TermT n -> TypeInfo (TermT n)
valueInfo TermT n
t TermT n
forall (n :: S). TermT n
universeT) Binder
orig TModality
md TermT n
a ScopedTermT n
b

typeIdT :: TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT :: forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT TermT n
x Maybe (TermT n)
tA TermT n
y = TermT n
t
  where t :: TermT n
t = TypeInfo (TermT n)
-> TermT n -> Maybe (TermT n) -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeIdT (TermT n -> TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TermT n -> TypeInfo (TermT n)
valueInfo TermT n
t TermT n
forall (n :: S). TermT n
universeT) TermT n
x Maybe (TermT n)
tA TermT n
y

typeRestrictedT :: TermT n -> [(TermT n, TermT n)] -> TermT n
typeRestrictedT :: forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n
typeRestrictedT TermT n
ty [(TermT n, TermT n)]
rs = TypeInfo (TermT n) -> TermT n -> [(TermT n, TermT n)] -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> [(AST binder (AnnSig ann TermSig) n,
     AST binder (AnnSig ann TermSig) n)]
-> AST binder (AnnSig ann TermSig) n
TypeRestrictedT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
forall (n :: S). TermT n
universeT) TermT n
ty [(TermT n, TermT n)]
rs

typeModalT :: TermT n -> TModality -> TermT n -> TermT n
typeModalT :: forall (n :: S). TermT n -> TModality -> TermT n -> TermT n
typeModalT TermT n
ty TModality
md TermT n
te = TypeInfo (TermT n) -> TModality -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeModalT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) TModality
md TermT n
te

typeAscT :: TermT n -> TermT n -> TermT n
typeAscT :: forall (n :: S). TermT n -> TermT n -> TermT n
typeAscT TermT n
x TermT n
ty = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
TypeAscT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) TermT n
x TermT n
ty

-- | A node that is already a value: it is its own weak head normal form.
valueInfo :: TermT n -> TermT n -> TypeInfo (TermT n)
valueInfo :: forall (n :: S). TermT n -> TermT n -> TypeInfo (TermT n)
valueInfo TermT n
t TermT n
ty = TypeInfo { infoType :: TermT n
infoType = TermT n
ty, infoWHNF :: Maybe (TermT n)
infoWHNF = TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
t, infoNF :: Maybe (TermT n)
infoNF = Maybe (TermT n)
forall a. Maybe a
Nothing }

-- ** Terms

lambdaT
  :: TermT n -> Binder -> Maybe (LambdaParam (ScopedTermT n) (TermT n))
  -> ScopedTermT n -> TermT n
lambdaT :: forall (n :: S).
TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
lambdaT TermT n
ty Binder
orig Maybe (LambdaParam (ScopedTermT n) (TermT n))
mparam ScopedTermT n
body = TermT n
t
  where t :: TermT n
t = TypeInfo (TermT n)
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> Maybe
     (LambdaParam
        (ScopedAST binder (AnnSig ann TermSig) n)
        (AST binder (AnnSig ann TermSig) n))
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
LambdaT (TermT n -> TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TermT n -> TypeInfo (TermT n)
valueInfo TermT n
t TermT n
ty) Binder
orig Maybe (LambdaParam (ScopedTermT n) (TermT n))
mparam ScopedTermT n
body

pairT :: TermT n -> TermT n -> TermT n -> TermT n
pairT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
pairT TermT n
ty TermT n
l TermT n
r = TermT n
t
  where t :: TermT n
t = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
PairT (TermT n -> TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TermT n -> TypeInfo (TermT n)
valueInfo TermT n
t TermT n
ty) TermT n
l TermT n
r

appT :: TermT n -> TermT n -> TermT n -> TermT n
appT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT n
ty TermT n
f TermT n
x = TypeInfo (TermT n) -> TermT n -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
AppT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) TermT n
f TermT n
x

firstT :: TermT n -> TermT n -> TermT n
firstT :: forall (n :: S). TermT n -> TermT n -> TermT n
firstT TermT n
ty TermT n
arg = TypeInfo (TermT n) -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
FirstT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) TermT n
arg

secondT :: TermT n -> TermT n -> TermT n
secondT :: forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
ty TermT n
arg = TypeInfo (TermT n) -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
SecondT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) TermT n
arg

letT :: TermT n -> Binder -> Maybe (TermT n) -> TermT n -> ScopedTermT n -> TermT n
letT :: forall (n :: S).
TermT n
-> Binder -> Maybe (TermT n) -> TermT n -> ScopedTermT n -> TermT n
letT TermT n
ty Binder
orig Maybe (TermT n)
mparam TermT n
val ScopedTermT n
body = TypeInfo (TermT n)
-> Binder -> Maybe (TermT n) -> TermT n -> ScopedTermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
LetT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) Binder
orig Maybe (TermT n)
mparam TermT n
val ScopedTermT n
body

letModT
  :: TermT n -> Binder -> TModality -> TModality -> Maybe (TermT n)
  -> Maybe (TermT n) -> TermT n -> ScopedTermT n -> TermT n
letModT :: forall (n :: S).
TermT n
-> Binder
-> TModality
-> TModality
-> Maybe (TermT n)
-> Maybe (TermT n)
-> TermT n
-> ScopedTermT n
-> TermT n
letModT TermT n
ty Binder
orig TModality
app TModality
inn Maybe (TermT n)
mparam Maybe (TermT n)
mmotive TermT n
val ScopedTermT n
body =
  TypeInfo (TermT n)
-> Binder
-> TModality
-> TModality
-> Maybe (TermT n)
-> Maybe (TermT n)
-> TermT n
-> ScopedTermT n
-> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> TModality
-> TModality
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
LetModT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) Binder
orig TModality
app TModality
inn Maybe (TermT n)
mparam Maybe (TermT n)
mmotive TermT n
val ScopedTermT n
body

-- | @refl@ normalises to a bare @refl@: its endpoints are recoverable from the
-- type, so they are dropped from the normal form.
reflT :: TermT n -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
reflT :: forall (n :: S).
TermT n -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
reflT TermT n
ty Maybe (TermT n, Maybe (TermT n))
mx = TypeInfo (TermT n) -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Maybe
     (AST binder (AnnSig ann TermSig) n,
      Maybe (AST binder (AnnSig ann TermSig) n))
-> AST binder (AnnSig ann TermSig) n
ReflT TypeInfo (TermT n)
info Maybe (TermT n, Maybe (TermT n))
mx
  where
    info :: TypeInfo (TermT n)
info = TypeInfo
      { infoType :: TermT n
infoType = TermT n
ty
      , infoWHNF :: Maybe (TermT n)
infoWHNF = TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just (TypeInfo (TermT n) -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Maybe
     (AST binder (AnnSig ann TermSig) n,
      Maybe (AST binder (AnnSig ann TermSig) n))
-> AST binder (AnnSig ann TermSig) n
ReflT TypeInfo (TermT n)
info Maybe (TermT n, Maybe (TermT n))
forall a. Maybe a
Nothing)
      , infoNF :: Maybe (TermT n)
infoNF   = TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just (TypeInfo (TermT n) -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Maybe
     (AST binder (AnnSig ann TermSig) n,
      Maybe (AST binder (AnnSig ann TermSig) n))
-> AST binder (AnnSig ann TermSig) n
ReflT TypeInfo (TermT n)
info Maybe (TermT n, Maybe (TermT n))
forall a. Maybe a
Nothing)
      }

idJT
  :: TermT n -> TermT n -> TermT n -> TermT n -> TermT n -> TermT n -> TermT n
  -> TermT n
idJT :: forall (n :: S).
TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
idJT TermT n
ty TermT n
tA TermT n
a TermT n
tC TermT n
d TermT n
x TermT n
p = TypeInfo (TermT n)
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
IdJT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) TermT n
tA TermT n
a TermT n
tC TermT n
d TermT n
x TermT n
p

recOrT :: TermT n -> [(TermT n, TermT n)] -> TermT n
recOrT :: forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n
recOrT TermT n
ty [(TermT n, TermT n)]
rs = TypeInfo (TermT n) -> [(TermT n, TermT n)] -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> [(AST binder (AnnSig ann TermSig) n,
     AST binder (AnnSig ann TermSig) n)]
-> AST binder (AnnSig ann TermSig) n
RecOrT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) [(TermT n, TermT n)]
rs

modAppT :: TermT n -> TModality -> TermT n -> TermT n
modAppT :: forall (n :: S). TermT n -> TModality -> TermT n -> TermT n
modAppT TermT n
ty TModality
md TermT n
term = TypeInfo (TermT n) -> TModality -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
ModAppT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) TModality
md TermT n
term

modExtractT :: TermT n -> TModality -> TModality -> TermT n -> TermT n
modExtractT :: forall (n :: S).
TermT n -> TModality -> TModality -> TermT n -> TermT n
modExtractT TermT n
ty TModality
app TModality
inn TermT n
term = TypeInfo (TermT n) -> TModality -> TModality -> TermT n -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> TModality
-> TModality
-> AST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
ModExtractT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) TModality
app TModality
inn TermT n
term

holeT :: TermT n -> Maybe VarIdent -> TermT n
holeT :: forall (n :: S). TermT n -> Maybe VarIdent -> TermT n
holeT TermT n
ty Maybe VarIdent
mname = TypeInfo (TermT n) -> Maybe VarIdent -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Maybe VarIdent -> AST binder (AnnSig ann TermSig) n
HoleT (TermT n -> TypeInfo (TermT n)
forall (n :: S). TermT n -> TypeInfo (TermT n)
topeInfo TermT n
ty) Maybe VarIdent
mname