{-# LANGUAGE PatternSynonyms #-}

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_,
  mapMember_,
  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.Generation
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_,
  mapMember_,
  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