| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.Syntax
Contents
Description
This module contains operations and tranformations on Syntax, Term, Pred, etc. 1) Computing Free Variables 2) Substitution 3) Renaming 4) internal helper functions 5) Syntacic only transformations
Synopsis
- mkNamed ∷ String → Q Pat
- mkNamedExpr ∷ String → Q Exp
- var ∷ QuasiQuoter
- 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
- 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
- unBind ∷ a → Binder a → Pred
- data Name where
- fromLits ∷ List Term as → Maybe (List Value as)
- fromLit ∷ Term a → Maybe (Value a)
- isLit ∷ Term a → Bool
- name ∷ String → Term a → Term a
- named ∷ String → Term a → Term a
- mkCase ∷ HasSpec (SumOver as) ⇒ Term (SumOver as) → List (Weighted Binder) as → Pred
- runCaseOn ∷ SumOver as → List Binder as → (∀ a. HasSpec a ⇒ Var a → a → Pred → r) → r
- letSubexpressionElimination ∷ HasSpec Bool ⇒ Pred → Pred
- letFloating ∷ Pred → Pred
- assertExplain ∷ IsPred p ⇒ NonEmpty String → p → Pred
- assert ∷ IsPred p ⇒ p → Pred
- forAll ∷ (Forallable t a, HasSpec t, HasSpec a, IsPred p) ⇒ Term t → (Term a → p) → Pred
- mkForAll ∷ (Forallable t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred
- exists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ ((∀ b. Term b → b) → GE a) → (Term a → p) → Pred
- unsafeExists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ (Term a → p) → Pred
- letBind ∷ (HasSpec a, IsPred p) ⇒ Term a → (Term a → p) → Pred
- reify ∷ (HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → (Term b → p) → Pred
- assertReified ∷ (HasSpec Bool, HasSpec a) ⇒ Term a → (a → Bool) → Pred
- explanation ∷ NonEmpty String → Pred → Pred
- monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred
- reifies ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term a → (a → b) → Pred
- dependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
- lit ∷ HasSpec a ⇒ a → Term a
- genHint ∷ ∀ t. HasGenHint t ⇒ Hint t → Term t → Pred
- envFromPred ∷ Env → Pred → GE Env
- runTermE ∷ ∀ a. Env → Term a → Either (NonEmpty String) a
- runTerm ∷ MonadGenError m ⇒ Env → Term a → m a
- data SolverStage where
- SolverStage ∷ HasSpec a ⇒ {..} → SolverStage
- data SolverPlan = SolverPlan {}
- isTrueSpec ∷ Specification a → Bool
- prettyLinear ∷ [SolverStage] → Doc ann
- regularize ∷ HasVariables t ⇒ Var a → t → Var a
- regularizeBinder ∷ Binder a → Binder a
- regularizeNamesPred ∷ Pred → Pred
- regularizeNames ∷ Specification a → Specification a
Documentation
mkNamedExpr ∷ String → Q Exp Source #
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 (f a) ⇒ HasVariables (Weighted f a) Source # | |
| HasVariables (List Term as) Source # | |
| HasVariables (List (Weighted Binder) as) Source # | |
type Subst = [SubstEntry] Source #
data SubstEntry where Source #
Constructors
| (:=) ∷ HasSpec a ⇒ Var a → Term a → SubstEntry |
fastInequality ∷ Term a → Term b → Bool Source #
Sound but not complete inequality on terms
named ∷ String → Term a → Term a Source #
Give a Term a nameHint, if its a Var, and doesn't already have one, otherwise return the Term unchanged.
letFloating ∷ Pred → Pred Source #
assertReified ∷ (HasSpec Bool, HasSpec a) ⇒ Term a → (a → Bool) → Pred Source #
requires (HasSpec Bool)
explanation ∷ NonEmpty String → Pred → Pred Source #
Wrap an Explain around a Pred, unless there is a simpler form.
monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred Source #
Add QuickCheck monitoring (e.g. collect or counterexample)
to a predicate. To use the monitoring in a property call monitorSpec on the Specification
containing the monitoring and a value generated from the specification.
data SolverStage where Source #
Constructors
| SolverStage | |
Fields
| |
Instances
| Pretty SolverStage Source # | |
Defined in Constrained.Syntax | |
data SolverPlan Source #
Constructors
| SolverPlan | |
Fields | |
Instances
| Pretty SolverPlan Source # | |
Defined in Constrained.Syntax | |
isTrueSpec ∷ Specification a → Bool Source #
prettyLinear ∷ [SolverStage] → Doc ann Source #
regularize ∷ HasVariables t ⇒ Var a → t → Var a Source #
regularizeBinder ∷ Binder a → Binder a Source #
regularizeNames ∷ Specification a → Specification a Source #