| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Minimal.Syntax
Contents
Synopsis
- forAll ∷ (Container t a, HasSpec t, HasSpec a) ⇒ Term t → (Term a → Pred) → Pred
- mkForAll ∷ (Container t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred
- exists ∷ ∀ a. HasSpec a ⇒ ((∀ b. Term b → b) → GE a) → (Term a → Pred) → Pred
- unsafeExists ∷ ∀ a. HasSpec a ⇒ (Term a → Pred) → Pred
- notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Spec a
- isErrorLike ∷ ∀ a. Spec a → Bool
- hasError ∷ ∀ a. Spec a → Maybe (NonEmpty String)
- handleErrors ∷ Spec a → Spec b → (Spec a → Spec b → Spec c) → Spec c
- addToErrorSpec ∷ NonEmpty String → Spec a → Spec a
- memberSpecList ∷ [a] → NonEmpty String → Spec a
- satisfies ∷ ∀ a. HasSpec a ⇒ Term a → Spec a → Pred
- runTermE ∷ ∀ a. Env → Term a → Either (NonEmpty String) a
- runTerm ∷ MonadGenError m ⇒ Env → Term a → m a
- conformsToSpec ∷ ∀ a. HasSpec a ⇒ a → Spec a → Bool
- checkPredE ∷ Env → NonEmpty String → Pred → Maybe (NonEmpty String)
- runCaseOn ∷ Either a b → Binder a → Binder b → (∀ x. HasSpec x ⇒ Var x → x → Pred → r) → r
- checkPredsE ∷ NonEmpty String → Env → [Pred] → Maybe (NonEmpty String)
- data Name where
- freeVarNames ∷ ∀ t. HasVariables t ⇒ t → Set Int
- newtype FreeVars = FreeVars {
- unFreeVars ∷ Map Name Int
- restrictedTo ∷ FreeVars → Set Name → FreeVars
- memberOf ∷ Name → FreeVars → Bool
- count ∷ Name → FreeVars → Int
- freeVar ∷ Name → FreeVars
- singleton ∷ Name → Int → FreeVars
- without ∷ Foldable t ⇒ FreeVars → t Name → FreeVars
- class HasVariables a where
- fromLits ∷ List Term as → Maybe (List Value as)
- fromLit ∷ Term a → Maybe (Value a)
- isLit ∷ Term a → Bool
- type Subst = [SubstEntry]
- data SubstEntry where
- (:=) ∷ HasSpec a ⇒ Var a → Term a → SubstEntry
- backwardsSubstitution ∷ ∀ a. HasSpec a ⇒ Subst → Term a → Term a
- fastInequality ∷ Term a → Term b → Bool
- substituteTerm ∷ ∀ a. Subst → Term a → Term a
- substituteTerm' ∷ ∀ a. Subst → Term a → Writer Any (Term a)
- substituteBinder ∷ HasSpec a ⇒ Var a → Term a → Binder b → Binder b
- substitutePred ∷ HasSpec a ⇒ Var a → Term a → Pred → Pred
- substTerm ∷ Env → Term a → Term a
- substBinder ∷ Env → Binder a → Binder a
- substPred ∷ Env → Pred → Pred
- substSpec ∷ Env → Spec a → Spec a
- substSolverStage ∷ Env → SolverStage → SolverStage
- substPlan ∷ Env → SolverPlan → SolverPlan
- unBind ∷ a → Binder a → Pred
- regularize ∷ HasVariables t ⇒ Var a → t → Var a
- regularizeBinder ∷ Binder a → Binder a
- regularizeNamesPred ∷ Pred → Pred
- regularizeNames ∷ Spec a → Spec a
- substituteAndSimplifyTerm ∷ Subst → Term a → Term a
- simplifyTerm ∷ ∀ a. Term a → Term a
- simplifyPred ∷ Pred → Pred
- mkCase ∷ HasSpec (Either a b) ⇒ Term (Either a b) → Binder a → Binder b → Pred
- simplifyPreds ∷ [Pred] → [Pred]
- simplifyBinder ∷ Binder a → Binder a
- toPred ∷ Bool → Pred
- letFloating ∷ Pred → Pred
- letSubexpressionElimination ∷ HasSpec Bool ⇒ Pred → Pred
- data SolverStage where
- SolverStage ∷ HasSpec a ⇒ {..} → SolverStage
- data SolverPlan = SolverPlan {}
- isTrueSpec ∷ Spec a → Bool
- prettyLinear ∷ [SolverStage] → Doc ann
- data EqSym ∷ [Type] → Type → Type where
- equalSpec ∷ a → Spec a
- notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Spec a
- caseBoolSpec ∷ (HasSpec Bool, HasSpec a) ⇒ Spec Bool → (Bool → Spec a) → Spec a
- (==.) ∷ (HasSpec Bool, HasSpec a) ⇒ Term a → Term a → Term Bool
- getWitness ∷ ∀ t t' d r. (AppRequires t d r, Typeable t') ⇒ t d r → Maybe (t' d r)
- pattern Equal ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term a → Term b
- pinnedBy ∷ ∀ a. HasSpec a ⇒ Var a → Pred → Maybe (Term a)
Documentation
isErrorLike ∷ ∀ a. Spec a → Bool Source #
addToErrorSpec ∷ NonEmpty String → Spec a → Spec a Source #
Add the explanations, if it's an ErrorSpec, else drop them
memberSpecList ∷ [a] → NonEmpty String → Spec a Source #
return a MemberSpec or ans ErrorSpec depending on if xs the null list or not
checkPredsE ∷ NonEmpty String → Env → [Pred] → Maybe (NonEmpty String) Source #
Like checkPred, But it takes [Pred] rather than a single Pred, and it builds a much more involved explanation if it fails. Does the Pred evaluate to True under the given Env? If it doesn't, an involved explanation appears in the (Just message) If it does, then it returns Nothing
freeVarNames ∷ ∀ t. HasVariables t ⇒ t → Set Int Source #
Constructors
| FreeVars | |
Fields
| |
class HasVariables a where Source #
Minimal complete definition
Methods
freeVars ∷ a → FreeVars Source #
freeVarSet ∷ a → Set Name Source #
Instances
| HasVariables Pred Source # | |
| HasVariables Name Source # | |
| HasVariables (Binder a) Source # | |
| HasVariables (Term a) Source # | |
| HasVariables a ⇒ HasVariables (Set a) Source # | |
| (Foldable t, HasVariables a) ⇒ HasVariables (t a) Source # | |
| (HasVariables a, HasVariables b) ⇒ HasVariables (a, b) Source # | |
| HasVariables (List Term as) Source # | |
type Subst = [SubstEntry] Source #
data SubstEntry where Source #
Constructors
| (:=) ∷ HasSpec a ⇒ Var a → Term a → SubstEntry |
substPlan ∷ Env → SolverPlan → SolverPlan Source #
regularize ∷ HasVariables t ⇒ Var a → t → Var a Source #
regularizeBinder ∷ Binder a → Binder a Source #
regularizeNames ∷ Spec a → Spec a Source #
substituteAndSimplifyTerm ∷ Subst → Term a → Term a Source #
Apply a substitution and simplify the resulting term if the substitution changed the term.
simplifyTerm ∷ ∀ a. Term a → Term a Source #
Simplify a Term, if the Term is an App, apply the rewrite rules
chosen by the (Semantics t) instance attached to the App
to the function witness f
simplifyPred ∷ Pred → Pred Source #
simplifyPreds ∷ [Pred] → [Pred] Source #
simplifyBinder ∷ Binder a → Binder a Source #
letFloating ∷ Pred → Pred Source #
data SolverStage where Source #
Constructors
| SolverStage | |
Fields
| |
Instances
| Pretty SolverStage Source # | |
Defined in Test.Minimal.Syntax | |
data SolverPlan Source #
Constructors
| SolverPlan | |
Fields | |
Instances
| Pretty SolverPlan Source # | |
Defined in Test.Minimal.Syntax | |
isTrueSpec ∷ Spec a → Bool Source #
prettyLinear ∷ [SolverStage] → Doc ann Source #
data EqSym ∷ [Type] → Type → Type where Source #
Instances
| Logic EqSym Source # | |
Defined in Test.Minimal.Syntax Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqSym as b, HasSpec a) ⇒ EqSym as b → ListCtx as (HOLE a) → TypeSpec b → [b] → Spec a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqSym as b, HasSpec a) ⇒ EqSym as b → ListCtx as (HOLE a) → NonEmpty b → Spec a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqSym as b, HasSpec a) ⇒ EqSym as b → ListCtx as (HOLE a) → Spec b → Spec a Source # | |
| Semantics EqSym Source # | |
| Syntax EqSym Source # | |
| Show (EqSym d r) Source # | |
| Eq (EqSym dom rng) Source # | |
notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Spec a Source #
getWitness ∷ ∀ t t' d r. (AppRequires t d r, Typeable t') ⇒ t d r → Maybe (t' d r) Source #
pinnedBy ∷ ∀ a. HasSpec a ⇒ Var a → Pred → Maybe (Term a) Source #
Is the variable x pinned to some free term in p? (free term meaning that all the variables in the term are free in p).
TODO: complete this with more cases!