Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data TyInst
- = InstApp (Type TyName DefaultUni ())
- | InstArg (Type TyName DefaultUni ())
- findInstantiation ∷ HasCallStack ⇒ TypeCtx → Int → Type TyName DefaultUni () → Type TyName DefaultUni () → Either String [TyInst]
- genConstant ∷ SomeTypeIn DefaultUni → GenTm (Term TyName Name DefaultUni DefaultFun ())
- inhabitType ∷ Type TyName DefaultUni () → GenTm (Term TyName Name DefaultUni DefaultFun ())
- typeArity ∷ Num a ⇒ Type tyname uni ann → a
- genAtomicTerm ∷ Type TyName DefaultUni () → GenTm (Term TyName Name DefaultUni DefaultFun ())
- genTermOfType ∷ Type TyName DefaultUni () → GenTm (Term TyName Name DefaultUni DefaultFun ())
- genTerm ∷ Maybe (Type TyName DefaultUni ()) → GenTm (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
- scaledListOf ∷ GenTm a → GenTm [a]
- genDatatypeLet ∷ Bool → (Datatype TyName Name DefaultUni () → GenTm a) → GenTm a
- genDatatypeLets ∷ ([Datatype TyName Name DefaultUni ()] → GenTm a) → GenTm a
- genTypeAndTerm_ ∷ Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
- genTypeAndTermDebug_ ∷ Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
- genFullyApplied ∷ Type TyName DefaultUni () → Term TyName Name DefaultUni DefaultFun () → Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
- genTermInContext_ ∷ TypeCtx → Map Name (Type TyName DefaultUni ()) → Type TyName DefaultUni () → Gen (Term TyName Name DefaultUni DefaultFun ())
Documentation
This type keeps track of what kind of argument, term argument (InstArg
) or
type argument (InstApp
) is required for a function. This type is used primarily
with findInstantiation
below where we do unification to figure out if we can
use a variable to construct a term of a target type.
InstApp (Type TyName DefaultUni ()) | |
InstArg (Type TyName DefaultUni ()) |
findInstantiation ∷ HasCallStack ⇒ TypeCtx → Int → Type TyName DefaultUni () → Type TyName DefaultUni () → Either String [TyInst] Source #
inhabitType ∷ Type TyName DefaultUni () → GenTm (Term TyName Name DefaultUni DefaultFun ()) Source #
Try to inhabit a given type in as simple a way as possible,
prefers to not default to error
genAtomicTerm ∷ Type TyName DefaultUni () → GenTm (Term TyName Name DefaultUni DefaultFun ()) Source #
Generate as small a term as possible to match a given type.
genTermOfType ∷ Type TyName DefaultUni () → GenTm (Term TyName Name DefaultUni DefaultFun ()) Source #
Generate a term of a given type.
Requires the type to be of kind *.
genTerm ∷ Maybe (Type TyName DefaultUni ()) → GenTm (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) Source #
Generate a term, if the first argument is Nothing then we get something of any type
and if the first argument is `Just ty` we get something of type ty
.
Requires the type to be of kind *.
scaledListOf ∷ GenTm a → GenTm [a] Source #
Like listOf
except each of the elements is generated with a proportionally smaller size.
genDatatypeLet ∷ Bool → (Datatype TyName Name DefaultUni () → GenTm a) → GenTm a Source #
genDatatypeLets ∷ ([Datatype TyName Name DefaultUni ()] → GenTm a) → GenTm a Source #
Generate up to 5 datatypes and bind them in a generator.
NOTE: despite its name this function does in fact not generate the Let
binding
for the datatypes.
genTypeAndTerm_ ∷ Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) Source #
genTypeAndTermDebug_ ∷ Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) Source #
genFullyApplied ∷ Type TyName DefaultUni () → Term TyName Name DefaultUni DefaultFun () → Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) Source #
Take a term of a specified type and generate a fully applied term. Useful for generating terms that you want to stick directly in an interpreter. Prefers to generate small arguments. NOTE: The logic of this generating small arguments is that the inner term should already have plenty of complicated arguments to functions to begin with and now we just want to fill out the arguments so that we get something that hopefully evaluates for a non-trivial number of steps.
genTermInContext_ ∷ TypeCtx → Map Name (Type TyName DefaultUni ()) → Type TyName DefaultUni () → Gen (Term TyName Name DefaultUni DefaultFun ()) Source #
Generate a term of a specific type given a type and term context