{-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} module Constrained.API ( PredD (..), TermD (..), SpecificationD (..), GenericallyInstantiated, Logic (..), Semantics (..), Syntax (..), Foldy (..), NumSpec (..), MaybeBounded (..), NonEmpty ((:|)), Specification, pattern TypeSpec, Term, Fun (..), name, named, Pred, HasSpec (..), HasSimpleRep (..), OrdLike (..), conformsToSpecE, conformsToSpec, satisfies, genFromSpecT, genFromSpec, debugSpec, genFromSpecWithSeed, simplifySpec, cardinality, ifElse, whenTrue, simplifyTerm, constrained, assertExplain, assert, forAll, exists, unsafeExists, letBind, reify, assertReified, explanation, monitor, reifies, dependsOn, lit, genHint, giveHint, (<.), (<=.), (>=.), (>.), (==.), (/=.), not_, or_, (||.), toGeneric_, fromGeneric_, (+.), (-.), negate_, addFn, negateFn, Numeric, pair_, fst_, snd_, prodSnd_, prodFst_, prod_, IsNormalType, injLeft_, injRight_, left_, right_, cJust_, cNothing_, caseOn, branch, branchW, forAll', constrained', reify', con, onCon, isCon, sel, match, onJust, isJust, chooseSpec, equalSpec, notEqualSpec, notMemberSpec, id_, flip_, compose_, foldMap_, sum_, elem_, singletonList_, append_, (++.), sizeOf, sizeOf_, null_, hasSize, rangeSize, length_, genFromSizeSpec, between, maxSpec, SetW (..), SetSpec (..), singleton_, member_, union_, subset_, disjoint_, fromList_, pattern Elem, pattern ToGeneric, pattern FromGeneric, pattern Unary, pattern (:<:), pattern (:>:), printPlan, NumLike, PairSpec (..), MapSpec (..), dom_, rng_, lookup_, fstSpec, sndSpec, var, Prod (..), ) where import Constrained.AbstractSyntax import Constrained.Base ( Fun (..), GenericallyInstantiated, HasSpec (..), Logic (..), Pred, Specification, Term, constrained, equalSpec, fromGeneric_, giveHint, name, named, notEqualSpec, notMemberSpec, toGeneric_, pattern FromGeneric, pattern ToGeneric, pattern TypeSpec, pattern Unary, pattern (:<:), pattern (:>:), ) import Constrained.Conformance ( conformsToSpec, conformsToSpecE, satisfies, ) import Constrained.Core (NonEmpty ((:|))) import Constrained.FunctionSymbol import Constrained.Generic (HasSimpleRep (..), Prod (..)) import Constrained.NumOrd ( MaybeBounded (..), NumLike, NumSpec (..), Numeric, OrdLike (..), addFn, cardinality, negateFn, negate_, (+.), (-.), (<.), (<=.), (>.), (>=.), ) import Constrained.Spec.Map ( MapSpec (..), dom_, fstSpec, lookup_, rng_, sndSpec, ) import Constrained.Spec.Set ( SetSpec (..), SetW (..), disjoint_, fromList_, member_, singleton_, subset_, union_, ) import Constrained.Spec.SumProd import Constrained.Syntax ( assert, assertExplain, assertReified, dependsOn, exists, explanation, forAll, genHint, letBind, lit, monitor, reifies, reify, unsafeExists, var, ) import Constrained.TheKnot infix 4 /=. (/=.) :: HasSpec a => Term a -> Term a -> Term Bool Term a a /=. :: forall a. HasSpec a => Term a -> Term a -> Term Bool /=. Term a b = Term Bool -> Term Bool not_ (Term a a Term a -> Term a -> Term Bool forall a. HasSpec a => Term a -> Term a -> Term Bool ==. Term a b) length_ :: HasSpec a => Term [a] -> Term Integer length_ :: forall a. HasSpec a => Term [a] -> Term Integer length_ = Term [a] -> Term Integer forall a. (HasSpec a, Sized a) => Term a -> Term Integer sizeOf_ infixr 2 ||. (||.) :: Term Bool -> Term Bool -> Term Bool ||. :: Term Bool -> Term Bool -> Term Bool (||.) = Term Bool -> Term Bool -> Term Bool or_ infixr 5 ++. (++.) :: HasSpec a => Term [a] -> Term [a] -> Term [a] ++. :: forall a. HasSpec a => Term [a] -> Term [a] -> Term [a] (++.) = Term [a] -> Term [a] -> Term [a] forall a. (Sized [a], HasSpec a) => Term [a] -> Term [a] -> Term [a] append_ null_ :: (HasSpec a, Sized a) => Term a -> Term Bool null_ :: forall a. (HasSpec a, Sized a) => Term a -> Term Bool null_ Term a xs = Term a -> Term Integer forall a. (HasSpec a, Sized a) => Term a -> Term Integer sizeOf_ Term a xs Term Integer -> Term Integer -> Term Bool forall a. HasSpec a => Term a -> Term a -> Term Bool ==. Term Integer 0