Safe Haskell	None
Language	Haskell2010

Language.Rzk.Foil.Syntax

Contents

The signature
Annotations
Terms
Equality
Free variables
Holes
Going under a binder, and substituting
Pattern synonyms
- Untyped patterns
Closed constants
Smart constructors
Orphan instances

Description

The core syntax on free-foil.

This is the successor of Language.Rzk.Free.Syntax's TermF / TermT, built on 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 NameBinder, a variable is a Name (an Int), and weakening a term into a larger scope is sink, a coercion rather than a traversal of every node.

Synopsis

data LambdaParam scope term = LambdaParam TModality term (Maybe scope)
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
- | MatchF term (Maybe term) [(VarIdent, term)]
- | 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)
newtype SrcPos term = SrcPos RzkPosition
noSrcPos :: SrcPos term
type Term = AST NameBinder (AnnSig SrcPos TermSig)
type TermT = AST NameBinder (AnnSig TypeInfo TermSig)
type ScopedTermT = ScopedAST NameBinder (AnnSig TypeInfo TermSig)
type ScopedTerm = ScopedAST NameBinder (AnnSig SrcPos TermSig)
atSrcPos :: forall (n :: S). RzkPosition -> Term n -> Term n
positionOfTerm :: forall (n :: S). Term n -> Maybe RzkPosition
typeInfoOf :: forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n))
untyped :: forall (n :: S). TermT n -> Term n
termIsWHNF :: forall (n :: S). TermT n -> TermT n
termIsNF :: forall (n :: S). TermT n -> TermT n
eqT :: forall (n :: S). Distinct n => TermT n -> TermT n -> Bool
alphaEqT :: forall (n :: S). Distinct n => Scope n -> TermT n -> TermT n -> Bool
elemT :: forall (n :: S). Distinct n => TermT n -> [TermT n] -> Bool
notElemT :: forall (n :: S). Distinct n => TermT n -> [TermT n] -> Bool
nubT :: forall (n :: S). Distinct n => [TermT n] -> [TermT n]
freeVarsOfTerm :: forall (n :: S). Term n -> [Name n]
freeVarsOfTermT :: forall (n :: S). TermT n -> [Name n]
containsUniverse :: forall (n :: S). Term n -> Bool
isHoleT :: forall (n :: S). TermT n -> Bool
isHoleHeadedT :: forall (n :: S). TermT n -> Bool
holeNamesOf :: forall (n :: S). Term n -> [Maybe VarIdent]
containsHole :: forall (n :: S). TermT n -> Bool
withScopedT :: forall (sig :: Type -> Type -> Type) (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
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
openWith :: forall (sig :: Type -> Type -> Type) (n :: S) (l :: S). (Bifunctor sig, DExt n l) => Scope l -> Name l -> ScopedAST NameBinder sig n -> AST NameBinder sig l
substituteName :: forall (n :: S). Distinct n => Scope n -> Name n -> TermT n -> TermT n -> TermT n
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
instantiateT :: forall (n :: S). Distinct n => Scope n -> ScopedTermT n -> TermT n -> TermT n
instantiateUntyped :: forall (n :: S). Distinct n => Scope n -> ScopedTerm n -> Term n -> Term n
substituteT :: forall (o :: S) (i :: S). Distinct o => Scope o -> Substitution TermT i o -> TermT i -> TermT o
pattern UniverseT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern UniverseCubeT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern UniverseTopeT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern CubeUnitT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern CubeUnitStarT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern Cube2T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern Cube2_0T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern Cube2_1T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern CubeIT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern CubeI_0T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern CubeI_1T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern CubeProductT :: forall {binder} {ann} {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
pattern CubeFlipT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern CubeUnflipT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern CubeSupT :: forall {binder} {ann} {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
pattern CubeInfT :: forall {binder} {ann} {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
pattern TopeTopT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern TopeBottomT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern TopeEQT :: forall {binder} {ann} {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
pattern TopeLEQT :: forall {binder} {ann} {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
pattern TopeAndT :: forall {binder} {ann} {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
pattern TopeOrT :: forall {binder} {ann} {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
pattern TopeInvT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern TopeUninvT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern RecBottomT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern RecOrT :: forall {binder} {ann} {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
pattern TypeFunT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n
pattern TypeSigmaT :: forall {binder} {ann} {n}. 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
pattern TypeIdT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n
pattern AppT :: forall {binder} {ann} {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
pattern LetT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n
pattern LambdaT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n
pattern PairT :: forall {binder} {ann} {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
pattern FirstT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern SecondT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern ReflT :: forall {binder} {ann} {n}. 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
pattern IdJT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n
pattern MatchT :: forall {binder} {ann} {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)] -> AST binder (AnnSig ann TermSig) n
pattern MatchArmT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> Binder -> ScopedAST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern UnitT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern TypeUnitT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n
pattern TypeAscT :: forall {binder} {ann} {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
pattern TypeRestrictedT :: forall {binder} {ann} {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
pattern TypeModalT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> TModality -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern ModAppT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> TModality -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern ModExtractT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> TModality -> TModality -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n
pattern LetModT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n
pattern HoleT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> Maybe VarIdent -> AST binder (AnnSig ann TermSig) n
pattern UntypedNode :: TermSig (ScopedTerm n) (Term n) -> Term n
pattern Universe :: Term n
pattern UniverseCube :: Term n
pattern UniverseTope :: Term n
pattern CubeUnit :: Term n
pattern CubeUnitStar :: Term n
pattern Cube2 :: Term n
pattern Cube2_0 :: Term n
pattern Cube2_1 :: Term n
pattern CubeI :: Term n
pattern CubeI_0 :: Term n
pattern CubeI_1 :: Term n
pattern CubeProduct :: Term n -> Term n -> Term n
pattern CubeFlip :: Term n -> Term n
pattern CubeUnflip :: Term n -> Term n
pattern CubeSup :: Term n -> Term n -> Term n
pattern CubeInf :: Term n -> Term n -> Term n
pattern TopeTop :: Term n
pattern TopeBottom :: Term n
pattern TopeEQ :: Term n -> Term n -> Term n
pattern TopeLEQ :: Term n -> Term n -> Term n
pattern TopeAnd :: Term n -> Term n -> Term n
pattern TopeOr :: Term n -> Term n -> Term n
pattern TopeInv :: Term n -> Term n
pattern TopeUninv :: Term n -> Term n
pattern RecBottom :: Term n
pattern RecOr :: [(Term n, Term n)] -> Term n
pattern TypeFun :: Binder -> TModality -> Term n -> Maybe (ScopedTerm n) -> ScopedTerm n -> Term n
pattern TypeSigma :: Binder -> TModality -> Term n -> ScopedTerm n -> Term n
pattern TypeId :: Term n -> Maybe (Term n) -> Term n -> Term n
pattern App :: Term n -> Term n -> Term n
pattern Let :: Binder -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n
pattern Lambda :: Binder -> Maybe (LambdaParam (ScopedTerm n) (Term n)) -> ScopedTerm n -> Term n
pattern Pair :: Term n -> Term n -> Term n
pattern First :: Term n -> Term n
pattern Second :: Term n -> Term n
pattern Refl :: Maybe (Term n, Maybe (Term n)) -> Term n
pattern IdJ :: Term n -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
pattern Match :: Term n -> Maybe (Term n) -> [(VarIdent, Term n)] -> Term n
pattern MatchArm :: Binder -> ScopedTerm n -> Term n
pattern Unit :: Term n
pattern TypeUnit :: Term n
pattern TypeAsc :: Term n -> Term n -> Term n
pattern TypeRestricted :: Term n -> [(Term n, Term n)] -> Term n
pattern TypeModal :: TModality -> Term n -> Term n
pattern ModApp :: TModality -> Term n -> Term n
pattern ModExtract :: TModality -> TModality -> Term n -> Term n
pattern LetMod :: Binder -> TModality -> TModality -> Maybe (Term n) -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n
pattern Hole :: Maybe VarIdent -> Term n
universeT :: forall (n :: S). TermT n
cubeT :: forall (n :: S). TermT n
topeT :: forall (n :: S). TermT n
cubeUnitT :: forall (n :: S). TermT n
cubeUnitStarT :: forall (n :: S). TermT n
cube2T :: forall (n :: S). TermT n
cube2_0T :: forall (n :: S). TermT n
cube2_1T :: forall (n :: S). TermT n
cubeIT :: forall (n :: S). TermT n
cubeI_0T :: forall (n :: S). TermT n
cubeI_1T :: forall (n :: S). TermT n
topeTopT :: forall (n :: S). TermT n
topeBottomT :: forall (n :: S). TermT n
typeUnitT :: forall (n :: S). TermT n
unitT :: forall (n :: S). TermT n
recBottomT :: forall (n :: S). TermT n
topeEQT :: forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT :: forall (n :: S). TermT n -> TermT n -> TermT n
topeOrT :: forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT :: forall (n :: S). TermT n -> TermT n -> TermT n
topeInvT :: forall (n :: S). TermT n -> TermT n
topeUninvT :: forall (n :: S). TermT n -> TermT n
topeInfo :: forall (n :: S). TermT n -> TypeInfo (TermT n)
cubeProductT :: forall (n :: S). TermT n -> TermT n -> TermT n
cubeFlipT :: forall (n :: S). TermT n -> TermT n -> TermT n
cubeUnflipT :: forall (n :: S). TermT n -> TermT n -> TermT n
cubeSupT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
cubeInfT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
typeFunT :: forall (n :: S). Binder -> TModality -> TermT n -> Maybe (ScopedTermT n) -> ScopedTermT n -> TermT n
typeSigmaT :: forall (n :: S). Binder -> TModality -> TermT n -> ScopedTermT n -> TermT n
typeIdT :: forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeRestrictedT :: forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n
typeModalT :: forall (n :: S). TermT n -> TModality -> TermT n -> TermT n
typeAscT :: forall (n :: S). TermT n -> TermT n -> TermT n
valueInfo :: forall (n :: S). TermT n -> TermT n -> TypeInfo (TermT n)
lambdaT :: forall (n :: S). TermT n -> Binder -> Maybe (LambdaParam (ScopedTermT n) (TermT n)) -> ScopedTermT n -> TermT n
pairT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
firstT :: forall (n :: S). TermT n -> TermT n -> TermT n
secondT :: forall (n :: S). TermT n -> TermT n -> TermT n
letT :: forall (n :: S). TermT n -> Binder -> 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
reflT :: forall (n :: S). TermT n -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
idJT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n -> TermT n -> TermT n -> TermT n -> TermT n
recOrT :: forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n
modAppT :: forall (n :: S). TermT n -> TModality -> TermT n -> TermT n
modExtractT :: forall (n :: S). TermT n -> TModality -> TModality -> TermT n -> TermT n
holeT :: forall (n :: S). TermT n -> Maybe VarIdent -> TermT n

The signature

data LambdaParam scope term Source #

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.

Constructors

LambdaParam TModality term (Maybe scope)

Instances

Instances details

Bifoldable LambdaParam Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

bifold :: Monoid m => LambdaParam m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> LambdaParam a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> LambdaParam a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> LambdaParam a b -> c #

Bifunctor LambdaParam Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> LambdaParam a c -> LambdaParam b d #

first :: (a -> b) -> LambdaParam a c -> LambdaParam b c #

second :: (b -> c) -> LambdaParam a b -> LambdaParam a c #

Bitraversable LambdaParam Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LambdaParam a b -> f (LambdaParam c d) #

GenericK (LambdaParam scope term :: Type) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Associated Types

type RepK (LambdaParam scope term :: Type)

Instance details

Defined in Language.Rzk.Foil.Syntax

type RepK (LambdaParam scope term :: Type) = D1 ('MetaData "LambdaParam" "Language.Rzk.Foil.Syntax" "rzk-0.11.3-4dSNy7duWaD47zdTR5WJes" 'False) (C1 ('MetaCons "LambdaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon TModality :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon (Maybe scope) :: Atom Type Type)))))

Methods

fromK :: forall (x :: LoT Type). (LambdaParam scope term :@@: x) -> RepK (LambdaParam scope term) x #

toK :: forall (x :: LoT Type). RepK (LambdaParam scope term) x -> LambdaParam scope term :@@: x #

Functor (LambdaParam scope) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

fmap :: (a -> b) -> LambdaParam scope a -> LambdaParam scope b #

(<$) :: a -> LambdaParam scope b -> LambdaParam scope a #

Foldable (LambdaParam scope) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

fold :: Monoid m => LambdaParam scope m -> m #

foldMap :: Monoid m => (a -> m) -> LambdaParam scope a -> m #

foldMap' :: Monoid m => (a -> m) -> LambdaParam scope a -> m #

foldr :: (a -> b -> b) -> b -> LambdaParam scope a -> b #

foldr' :: (a -> b -> b) -> b -> LambdaParam scope a -> b #

foldl :: (b -> a -> b) -> b -> LambdaParam scope a -> b #

foldl' :: (b -> a -> b) -> b -> LambdaParam scope a -> b #

foldr1 :: (a -> a -> a) -> LambdaParam scope a -> a #

foldl1 :: (a -> a -> a) -> LambdaParam scope a -> a #

toList :: LambdaParam scope a -> [a] #

null :: LambdaParam scope a -> Bool #

length :: LambdaParam scope a -> Int #

elem :: Eq a => a -> LambdaParam scope a -> Bool #

maximum :: Ord a => LambdaParam scope a -> a #

minimum :: Ord a => LambdaParam scope a -> a #

sum :: Num a => LambdaParam scope a -> a #

product :: Num a => LambdaParam scope a -> a #

Traversable (LambdaParam scope) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> LambdaParam scope a -> f (LambdaParam scope b) #

sequenceA :: Applicative f => LambdaParam scope (f a) -> f (LambdaParam scope a) #

mapM :: Monad m => (a -> m b) -> LambdaParam scope a -> m (LambdaParam scope b) #

sequence :: Monad m => LambdaParam scope (m a) -> m (LambdaParam scope a) #

Generic (LambdaParam scope term) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Associated Types

type Rep (LambdaParam scope term)

Instance details

Defined in Language.Rzk.Foil.Syntax

type Rep (LambdaParam scope term) = D1 ('MetaData "LambdaParam" "Language.Rzk.Foil.Syntax" "rzk-0.11.3-4dSNy7duWaD47zdTR5WJes" 'False) (C1 ('MetaCons "LambdaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TModality) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe scope)))))

Methods

from :: LambdaParam scope term -> Rep (LambdaParam scope term) x #

to :: Rep (LambdaParam scope term) x -> LambdaParam scope term #

(Eq term, Eq scope) => Eq (LambdaParam scope term) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

(==) :: LambdaParam scope term -> LambdaParam scope term -> Bool #

(/=) :: LambdaParam scope term -> LambdaParam scope term -> Bool #

ZipMatchK LambdaParam Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (LambdaParam :@@: as) -> (LambdaParam :@@: bs) -> Maybe (LambdaParam :@@: cs) #

GenericK LambdaParam Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Associated Types

type RepK LambdaParam

Instance details

Defined in Language.Rzk.Foil.Syntax

type RepK LambdaParam = D1 ('MetaData "LambdaParam" "Language.Rzk.Foil.Syntax" "rzk-0.11.3-4dSNy7duWaD47zdTR5WJes" 'False) (C1 ('MetaCons "LambdaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon TModality :: Atom (Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon Maybe :: Atom (Type -> Type -> Type) (Type -> Type)) ':@: (Var0 :: Atom (Type -> Type -> Type) Type))))))

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type)). (LambdaParam :@@: x) -> RepK LambdaParam x #

toK :: forall (x :: LoT (Type -> Type -> Type)). RepK LambdaParam x -> LambdaParam :@@: x #

GenericK (LambdaParam scope :: Type -> Type) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Associated Types

type RepK (LambdaParam scope :: Type -> Type)

Instance details

Defined in Language.Rzk.Foil.Syntax

type RepK (LambdaParam scope :: Type -> Type) = D1 ('MetaData "LambdaParam" "Language.Rzk.Foil.Syntax" "rzk-0.11.3-4dSNy7duWaD47zdTR5WJes" 'False) (C1 ('MetaCons "LambdaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon TModality :: Atom (Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon (Maybe scope) :: Atom (Type -> Type) Type)))))

Methods

fromK :: forall (x :: LoT (Type -> Type)). (LambdaParam scope :@@: x) -> RepK (LambdaParam scope) x #

toK :: forall (x :: LoT (Type -> Type)). RepK (LambdaParam scope) x -> LambdaParam scope :@@: x #

type RepK (LambdaParam scope term :: Type) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

type RepK (LambdaParam scope term :: Type) = D1 ('MetaData "LambdaParam" "Language.Rzk.Foil.Syntax" "rzk-0.11.3-4dSNy7duWaD47zdTR5WJes" 'False) (C1 ('MetaCons "LambdaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon TModality :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon (Maybe scope) :: Atom Type Type)))))

type Rep (LambdaParam scope term) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

type Rep (LambdaParam scope term) = D1 ('MetaData "LambdaParam" "Language.Rzk.Foil.Syntax" "rzk-0.11.3-4dSNy7duWaD47zdTR5WJes" 'False) (C1 ('MetaCons "LambdaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TModality) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe scope)))))

type RepK LambdaParam Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

type RepK LambdaParam = D1 ('MetaData "LambdaParam" "Language.Rzk.Foil.Syntax" "rzk-0.11.3-4dSNy7duWaD47zdTR5WJes" 'False) (C1 ('MetaCons "LambdaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon TModality :: Atom (Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon Maybe :: Atom (Type -> Type -> Type) (Type -> Type)) ':@: (Var0 :: Atom (Type -> Type -> Type) Type))))))

type RepK (LambdaParam scope :: Type -> Type) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

type RepK (LambdaParam scope :: Type -> Type) = D1 ('MetaData "LambdaParam" "Language.Rzk.Foil.Syntax" "rzk-0.11.3-4dSNy7duWaD47zdTR5WJes" 'False) (C1 ('MetaCons "LambdaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon TModality :: Atom (Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon (Maybe scope) :: Atom (Type -> Type) Type)))))

data TermSig scope term Source #

Constructors

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
MatchF term (Maybe term) [(VarIdent, 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.
MatchArmF Binder scope	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.
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)

Instances

Instances details

Bifoldable TermSig Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

bifold :: Monoid m => TermSig m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> TermSig a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> TermSig a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> TermSig a b -> c #

Bifunctor TermSig Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> TermSig a c -> TermSig b d #

first :: (a -> b) -> TermSig a c -> TermSig b c #

second :: (b -> c) -> TermSig a b -> TermSig a c #

Bitraversable TermSig Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> TermSig a b -> f (TermSig c d) #

GenericK (TermSig scope term :: Type) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Associated Types

type RepK (TermSig scope term :: Type)

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

fromK :: forall (x :: LoT Type). (TermSig scope term :@@: x) -> RepK (TermSig scope term) x #

toK :: forall (x :: LoT Type). RepK (TermSig scope term) x -> TermSig scope term :@@: x #

Functor (TermSig scope) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

fmap :: (a -> b) -> TermSig scope a -> TermSig scope b #

(<$) :: a -> TermSig scope b -> TermSig scope a #

Foldable (TermSig scope) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

fold :: Monoid m => TermSig scope m -> m #

foldMap :: Monoid m => (a -> m) -> TermSig scope a -> m #

foldMap' :: Monoid m => (a -> m) -> TermSig scope a -> m #

foldr :: (a -> b -> b) -> b -> TermSig scope a -> b #

foldr' :: (a -> b -> b) -> b -> TermSig scope a -> b #

foldl :: (b -> a -> b) -> b -> TermSig scope a -> b #

foldl' :: (b -> a -> b) -> b -> TermSig scope a -> b #

foldr1 :: (a -> a -> a) -> TermSig scope a -> a #

foldl1 :: (a -> a -> a) -> TermSig scope a -> a #

toList :: TermSig scope a -> [a] #

null :: TermSig scope a -> Bool #

length :: TermSig scope a -> Int #

elem :: Eq a => a -> TermSig scope a -> Bool #

maximum :: Ord a => TermSig scope a -> a #

minimum :: Ord a => TermSig scope a -> a #

sum :: Num a => TermSig scope a -> a #

product :: Num a => TermSig scope a -> a #

Traversable (TermSig scope) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> TermSig scope a -> f (TermSig scope b) #

sequenceA :: Applicative f => TermSig scope (f a) -> f (TermSig scope a) #

mapM :: Monad m => (a -> m b) -> TermSig scope a -> m (TermSig scope b) #

sequence :: Monad m => TermSig scope (m a) -> m (TermSig scope a) #

Generic (TermSig scope term) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Associated Types

type Rep (TermSig scope term)

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

from :: TermSig scope term -> Rep (TermSig scope term) x #

to :: Rep (TermSig scope term) x -> TermSig scope term #

(Eq term, Eq scope) => Eq (TermSig scope term) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

(==) :: TermSig scope term -> TermSig scope term -> Bool #

(/=) :: TermSig scope term -> TermSig scope term -> Bool #

ZipMatchK TermSig Source #

The node matcher, TH-derived: an explicit instance, so no Generics.Kind view is rebuilt per comparison. It drives alphaEquiv and 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.

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (TermSig :@@: as) -> (TermSig :@@: bs) -> Maybe (TermSig :@@: cs) #

GenericK TermSig Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Associated Types

type RepK TermSig

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type)). (TermSig :@@: x) -> RepK TermSig x #

toK :: forall (x :: LoT (Type -> Type -> Type)). RepK TermSig x -> TermSig :@@: x #

GenericK (TermSig scope :: Type -> Type) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Associated Types

type RepK (TermSig scope :: Type -> Type)

Instance details

Defined in Language.Rzk.Foil.Syntax

Methods

fromK :: forall (x :: LoT (Type -> Type)). (TermSig scope :@@: x) -> RepK (TermSig scope) x #

toK :: forall (x :: LoT (Type -> Type)). RepK (TermSig scope) x -> TermSig scope :@@: x #

type RepK (TermSig scope term :: Type) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

type Rep (TermSig scope term) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

type RepK TermSig Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

type RepK (TermSig scope :: Type -> Type) Source #

Instance details

Defined in Language.Rzk.Foil.Syntax

Annotations

newtype SrcPos term Source #

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.

Constructors

SrcPos RzkPosition

Instances

Instances details

Functor SrcPos Source #
Instance details Defined in Language.Rzk.Foil.Syntax Methods fmap :: (a -> b) -> SrcPos a -> SrcPos b # (<$) :: a -> SrcPos b -> SrcPos a #
Foldable SrcPos Source #
Instance details Defined in Language.Rzk.Foil.Syntax Methods fold :: Monoid m => SrcPos m -> m # foldMap :: Monoid m => (a -> m) -> SrcPos a -> m # foldMap' :: Monoid m => (a -> m) -> SrcPos a -> m # foldr :: (a -> b -> b) -> b -> SrcPos a -> b # foldr' :: (a -> b -> b) -> b -> SrcPos a -> b # foldl :: (b -> a -> b) -> b -> SrcPos a -> b # foldl' :: (b -> a -> b) -> b -> SrcPos a -> b # foldr1 :: (a -> a -> a) -> SrcPos a -> a # foldl1 :: (a -> a -> a) -> SrcPos a -> a # toList :: SrcPos a -> [a] # null :: SrcPos a -> Bool # length :: SrcPos a -> Int # elem :: Eq a => a -> SrcPos a -> Bool # maximum :: Ord a => SrcPos a -> a # minimum :: Ord a => SrcPos a -> a # sum :: Num a => SrcPos a -> a # product :: Num a => SrcPos a -> a #
Traversable SrcPos Source #
Instance details Defined in Language.Rzk.Foil.Syntax Methods traverse :: Applicative f => (a -> f b) -> SrcPos a -> f (SrcPos b) # sequenceA :: Applicative f => SrcPos (f a) -> f (SrcPos a) # mapM :: Monad m => (a -> m b) -> SrcPos a -> m (SrcPos b) # sequence :: Monad m => SrcPos (m a) -> m (SrcPos a) #
ZipMatchK SrcPos Source #	Two terms written in different places are the same term, so a position is ignored in matching, as a node's type is.
Instance details Defined in Language.Rzk.Foil.Syntax Methods zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> (SrcPos :@@: as) -> (SrcPos :@@: bs) -> Maybe (SrcPos :@@: cs) #

noSrcPos :: SrcPos term Source #

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.

Terms

type Term = AST NameBinder (AnnSig SrcPos TermSig) Source #

An untyped term: the surface syntax, elaborated, every node carrying where it was written.

type TermT = AST NameBinder (AnnSig TypeInfo TermSig) Source #

A typed term: every node carries its type. The successor of TermT.

type ScopedTermT = ScopedAST NameBinder (AnnSig TypeInfo TermSig) Source #

A scope: a binder together with the term it binds over.

type ScopedTerm = ScopedAST NameBinder (AnnSig SrcPos TermSig) Source #

A scope of an untyped term.

atSrcPos :: forall (n :: S). RzkPosition -> Term n -> Term n Source #

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.

positionOfTerm :: forall (n :: S). Term n -> Maybe RzkPosition Source #

Where the term was written, when it came from a file.

typeInfoOf :: forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n)) Source #

The annotation of a node: its type, and its memoised normal forms. A variable carries none — its type lives in the context.

untyped :: forall (n :: S). TermT n -> Term n Source #

Drop every annotation, for printing and for the surface-facing API.

termIsWHNF :: forall (n :: S). TermT n -> TermT n Source #

Memoise a node's own weak head normal form (the self-referential knot of the old representation, unchanged).

termIsNF :: forall (n :: S). TermT n -> TermT n Source #

Equality

eqT :: forall (n :: S). Distinct n => TermT n -> TermT n -> Bool Source #

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.

alphaEqT :: forall (n :: S). Distinct n => Scope n -> TermT n -> TermT n -> Bool Source #

α-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.

elemT :: forall (n :: S). Distinct n => TermT n -> [TermT n] -> Bool Source #

notElemT :: forall (n :: S). Distinct n => TermT n -> [TermT n] -> Bool Source #

nubT :: forall (n :: S). Distinct n => [TermT n] -> [TermT n] Source #

Free variables

freeVarsOfTerm :: forall (n :: S). Term n -> [Name n] Source #

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.

freeVarsOfTermT :: forall (n :: S). TermT n -> [Name n] Source #

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).

containsUniverse :: forall (n :: S). Term n -> Bool Source #

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).

Holes

isHoleT :: forall (n :: S). TermT n -> Bool Source #

isHoleHeadedT :: forall (n :: S). TermT n -> Bool Source #

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.

holeNamesOf :: forall (n :: S). Term n -> [Maybe VarIdent] Source #

The name of every hole in a term.

containsHole :: forall (n :: S). TermT n -> Bool Source #

Does the term contain a hole anywhere (including nested, e.g. f ?)?

Going under a binder, and substituting

withScopedT :: forall (sig :: Type -> Type -> Type) (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 Source #

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.

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

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.

openWith :: forall (sig :: Type -> Type -> Type) (n :: S) (l :: S). (Bifunctor sig, DExt n l) => Scope l -> Name l -> ScopedAST NameBinder sig n -> AST NameBinder sig l Source #

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.

substituteName :: forall (n :: S). Distinct n => Scope n -> Name n -> TermT n -> TermT n -> TermT n Source #

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.

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

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.

instantiateT :: forall (n :: S). Distinct n => Scope n -> ScopedTermT n -> TermT n -> TermT n Source #

Instantiate a scoped term with a term: the successor of substituteT x scope.

instantiateUntyped :: forall (n :: S). Distinct n => Scope n -> ScopedTerm n -> Term n -> Term n Source #

Instantiate a scoped untyped term. There are no memoised normal forms to invalidate, so this is free-foil's own substitution.

substituteT :: forall (o :: S) (i :: S). Distinct o => Scope o -> Substitution TermT i o -> TermT i -> TermT o Source #

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.

Pattern synonyms

pattern UniverseT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern UniverseCubeT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern UniverseTopeT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern CubeUnitT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern CubeUnitStarT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern Cube2T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern Cube2_0T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern Cube2_1T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern CubeIT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern CubeI_0T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern CubeI_1T :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern CubeProductT :: forall {binder} {ann} {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 Source #

pattern CubeFlipT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern CubeUnflipT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern CubeSupT :: forall {binder} {ann} {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 Source #

pattern CubeInfT :: forall {binder} {ann} {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 Source #

pattern TopeTopT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern TopeBottomT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern TopeEQT :: forall {binder} {ann} {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 Source #

pattern TopeLEQT :: forall {binder} {ann} {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 Source #

pattern TopeAndT :: forall {binder} {ann} {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 Source #

pattern TopeOrT :: forall {binder} {ann} {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 Source #

pattern TopeInvT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern TopeUninvT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern RecBottomT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern RecOrT :: forall {binder} {ann} {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 Source #

pattern TypeFunT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n Source #

pattern TypeSigmaT :: forall {binder} {ann} {n}. 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 Source #

pattern TypeIdT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n Source #

pattern AppT :: forall {binder} {ann} {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 Source #

pattern LetT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n Source #

pattern LambdaT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n Source #

pattern PairT :: forall {binder} {ann} {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 Source #

pattern FirstT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern SecondT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern ReflT :: forall {binder} {ann} {n}. 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 Source #

pattern IdJT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n Source #

pattern MatchT :: forall {binder} {ann} {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)] -> AST binder (AnnSig ann TermSig) n Source #

pattern MatchArmT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> Binder -> ScopedAST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern UnitT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern TypeUnitT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> AST binder (AnnSig ann TermSig) n Source #

pattern TypeAscT :: forall {binder} {ann} {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 Source #

pattern TypeRestrictedT :: forall {binder} {ann} {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 Source #

pattern TypeModalT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> TModality -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern ModAppT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> TModality -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern ModExtractT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> TModality -> TModality -> AST binder (AnnSig ann TermSig) n -> AST binder (AnnSig ann TermSig) n Source #

pattern LetModT :: forall {binder} {ann} {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 -> AST binder (AnnSig ann TermSig) n Source #

pattern HoleT :: forall {binder} {ann} {n}. ann (AST binder (AnnSig ann TermSig) n) -> Maybe VarIdent -> AST binder (AnnSig ann TermSig) n Source #

Untyped patterns

pattern UntypedNode :: TermSig (ScopedTerm n) (Term n) -> Term n Source #

An untyped node, taken and made without regard for where it was written.

pattern Universe :: Term n Source #

pattern UniverseCube :: Term n Source #

pattern UniverseTope :: Term n Source #

pattern CubeUnit :: Term n Source #

pattern CubeUnitStar :: Term n Source #

pattern Cube2 :: Term n Source #

pattern Cube2_0 :: Term n Source #

pattern Cube2_1 :: Term n Source #

pattern CubeI :: Term n Source #

pattern CubeI_0 :: Term n Source #

pattern CubeI_1 :: Term n Source #

pattern CubeProduct :: Term n -> Term n -> Term n Source #

pattern CubeFlip :: Term n -> Term n Source #

pattern CubeUnflip :: Term n -> Term n Source #

pattern CubeSup :: Term n -> Term n -> Term n Source #

pattern CubeInf :: Term n -> Term n -> Term n Source #

pattern TopeTop :: Term n Source #

pattern TopeBottom :: Term n Source #

pattern TopeEQ :: Term n -> Term n -> Term n Source #

pattern TopeLEQ :: Term n -> Term n -> Term n Source #

pattern TopeAnd :: Term n -> Term n -> Term n Source #

pattern TopeOr :: Term n -> Term n -> Term n Source #

pattern TopeInv :: Term n -> Term n Source #

pattern TopeUninv :: Term n -> Term n Source #

pattern RecBottom :: Term n Source #

pattern RecOr :: [(Term n, Term n)] -> Term n Source #

pattern TypeFun :: Binder -> TModality -> Term n -> Maybe (ScopedTerm n) -> ScopedTerm n -> Term n Source #

pattern TypeSigma :: Binder -> TModality -> Term n -> ScopedTerm n -> Term n Source #

pattern TypeId :: Term n -> Maybe (Term n) -> Term n -> Term n Source #

pattern App :: Term n -> Term n -> Term n Source #

pattern Let :: Binder -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n Source #

pattern Lambda :: Binder -> Maybe (LambdaParam (ScopedTerm n) (Term n)) -> ScopedTerm n -> Term n Source #

pattern Pair :: Term n -> Term n -> Term n Source #

pattern First :: Term n -> Term n Source #

pattern Second :: Term n -> Term n Source #

pattern Refl :: Maybe (Term n, Maybe (Term n)) -> Term n Source #

pattern IdJ :: Term n -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n Source #

pattern Match :: Term n -> Maybe (Term n) -> [(VarIdent, Term n)] -> Term n Source #

pattern MatchArm :: Binder -> ScopedTerm n -> Term n Source #

pattern Unit :: Term n Source #

pattern TypeUnit :: Term n Source #

pattern TypeAsc :: Term n -> Term n -> Term n Source #

pattern TypeRestricted :: Term n -> [(Term n, Term n)] -> Term n Source #

pattern TypeModal :: TModality -> Term n -> Term n Source #

pattern ModApp :: TModality -> Term n -> Term n Source #

pattern ModExtract :: TModality -> TModality -> Term n -> Term n Source #

pattern LetMod :: Binder -> TModality -> TModality -> Maybe (Term n) -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n Source #

pattern Hole :: Maybe VarIdent -> Term n Source #

Closed constants

universeT :: forall (n :: S). TermT n Source #

cubeT :: forall (n :: S). TermT n Source #

topeT :: forall (n :: S). TermT n Source #

cubeUnitT :: forall (n :: S). TermT n Source #

cubeUnitStarT :: forall (n :: S). TermT n Source #

cube2T :: forall (n :: S). TermT n Source #

cube2_0T :: forall (n :: S). TermT n Source #

cube2_1T :: forall (n :: S). TermT n Source #

cubeIT :: forall (n :: S). TermT n Source #

cubeI_0T :: forall (n :: S). TermT n Source #

cubeI_1T :: forall (n :: S). TermT n Source #

topeTopT :: forall (n :: S). TermT n Source #

topeBottomT :: forall (n :: S). TermT n Source #

typeUnitT :: forall (n :: S). TermT n Source #

unitT :: forall (n :: S). TermT n Source #

recBottomT :: forall (n :: S). TermT n Source #

recBOT is its own type: it inhabits every type in a contradictory context.

Smart constructors

The tope layer

topeEQT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

topeLEQT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

topeOrT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

topeAndT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

topeInvT :: forall (n :: S). TermT n -> TermT n Source #

topeUninvT :: forall (n :: S). TermT n -> TermT n Source #

topeInfo :: forall (n :: S). TermT n -> TypeInfo (TermT n) Source #

An unreduced node of the given type.

Cubes

cubeProductT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

cubeFlipT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

cubeUnflipT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

cubeSupT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n Source #

cubeInfT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n Source #

Types

typeFunT :: forall (n :: S). Binder -> TModality -> TermT n -> Maybe (ScopedTermT n) -> ScopedTermT n -> TermT n Source #

typeSigmaT :: forall (n :: S). Binder -> TModality -> TermT n -> ScopedTermT n -> TermT n Source #

typeIdT :: forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n Source #

typeRestrictedT :: forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n Source #

typeModalT :: forall (n :: S). TermT n -> TModality -> TermT n -> TermT n Source #

typeAscT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

valueInfo :: forall (n :: S). TermT n -> TermT n -> TypeInfo (TermT n) Source #

A node that is already a value: it is its own weak head normal form.

Terms

lambdaT :: forall (n :: S). TermT n -> Binder -> Maybe (LambdaParam (ScopedTermT n) (TermT n)) -> ScopedTermT n -> TermT n Source #

pairT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n Source #

appT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n Source #

firstT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

secondT :: forall (n :: S). TermT n -> TermT n -> TermT n Source #

letT :: forall (n :: S). TermT n -> Binder -> Maybe (TermT n) -> TermT n -> ScopedTermT n -> TermT n Source #

letModT :: forall (n :: S). TermT n -> Binder -> TModality -> TModality -> Maybe (TermT n) -> Maybe (TermT n) -> TermT n -> ScopedTermT n -> TermT n Source #

reflT :: forall (n :: S). TermT n -> Maybe (TermT n, Maybe (TermT n)) -> TermT n Source #

refl normalises to a bare refl: its endpoints are recoverable from the type, so they are dropped from the normal form.

idJT :: forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n -> TermT n -> TermT n -> TermT n -> TermT n Source #

recOrT :: forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n Source #

modAppT :: forall (n :: S). TermT n -> TModality -> TermT n -> TermT n Source #

modExtractT :: forall (n :: S). TermT n -> TModality -> TModality -> TermT n -> TermT n Source #

holeT :: forall (n :: S). TermT n -> Maybe VarIdent -> TermT n Source #

Orphan instances

ZipMatchK Binder Source #
Instance details Methods zipMatchWithK :: forall (as :: LoT Type) (bs :: LoT Type) (cs :: LoT Type). Mappings as bs cs -> (Binder :@@: as) -> (Binder :@@: bs) -> Maybe (Binder :@@: cs) #
ZipMatchK TModality Source #	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 details Methods zipMatchWithK :: forall (as :: LoT Type) (bs :: LoT Type) (cs :: LoT Type). Mappings as bs cs -> (TModality :@@: as) -> (TModality :@@: bs) -> Maybe (TModality :@@: cs) #
ZipMatchK VarIdent Source #
Instance details Methods zipMatchWithK :: forall (as :: LoT Type) (bs :: LoT Type) (cs :: LoT Type). Mappings as bs cs -> (VarIdent :@@: as) -> (VarIdent :@@: bs) -> Maybe (VarIdent :@@: cs) #
ZipMatchK (Maybe VarIdent) Source #	A hole's name is a whole field (`HoleF`), so it is matched as a constant rather than through the `Maybe` functor.
Instance details Methods zipMatchWithK :: forall (as :: LoT Type) (bs :: LoT Type) (cs :: LoT Type). Mappings as bs cs -> (Maybe VarIdent :@@: as) -> (Maybe VarIdent :@@: bs) -> Maybe (Maybe VarIdent :@@: cs) #
ZipMatchK TypeInfo Source #	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 `Annotated` haddock.
Instance details Methods zipMatchWithK :: forall (as :: LoT (Type -> Type)) (bs :: LoT (Type -> Type)) (cs :: LoT (Type -> Type)). Mappings as bs cs -> (TypeInfo :@@: as) -> (TypeInfo :@@: bs) -> Maybe (TypeInfo :@@: cs) #