Z/      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVW X Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~                                   ! " # $ % & ' ( ) * + , - . (C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalSafe+,D/: for indexed type constructors (most importantly functors)(C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalSafe+,DOT7Type constructors (usually functors) that can be folded(C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalSafe+,DOTKType constructors (usually functors) that produce types that can be equated!Indexed types that can be equated(C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone+,DOT A functor in indexed category +A fixpoint of a functor in indexed categoryIndexed catamorphism       (C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone+,DOT:Type constructors (usually functors) that can be traversed1Maps a monadic action over a traversable functor.(C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone +,9;<=DOQRT+Inclusion relation for indexed sum functorsSum of two indexed functorsInject a component into a sum.%Try to unpack a sum into a component. !"#$%  !"#$%8(C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone%&+,9DOQRT &A universe of recognized sorts'booleans (true, false)(integers (..., -1, 0, 1, ...))arrays indexed by * sort, containing elements of + sort5@An expression of some sort (obtained for example during parsing)7/Some sort (obtained for example during parsing)9Tries to convert some sort (7) to a requested sort.: Tries to convert an expression (5L) of some sort to an expression of requested sort. Performs no conversions.;-Parser that accepts sort definitions such as bool, int,  array int int, array int (array ...).+&'()*+0123456789:;<=>?@ABCDE5678FG9:;<=>?@AHIJKLMNOPQ@ABRCD&'()*+56789:;&'()*+7856;9:&'()*+0123456789:;<=>?E@ABCD5678FG9:;<=>?@A(C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone+,9;<=DQRTBExpressions that can be parsedD:Context-sensitive parser that remembers sorts of variablesE2Parsing context assigning sorts to known variablesFiTries to parse the entire input text and produce an expression in desired language and with desired sort.GLike FD but allows adding initial assumption about sorts of some variables.HMatches a given character.IMatches first of many choices.JMatches a given decimal number.KMatches a given digit.LMatches any character.MMatches one or more times.N<Matches one or more times, separated by specified separator.OMatches a signed number.PMatches space.QMatches a given string.R-Matches identifier that starts with [a-zA-Z'_#] and is followed by [a-zA-Z'_#0-9].SLabels parser.T?Asserts what sort is assigned to a variable in current context.U/Variable assumes sort based on current context.BCDEFGHIJKLMNOPQRSTUVBCDEFGHIJKLMNOPQRSTUEDBCFGHIJKLMNOPQRSTUBCDEFGHIJKLMNOPQRSTUV (C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone%&+,9:;<=DOQRTWUA functor representing an equality predicate between two expressions of matching sortY-A smart constructor for an equality predicate WXYZ[\]^_WXYWXYWXYZ[\]^_Y7 (C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone%&+,9:;<=DOQRT`.A functor representing array-theoretic terms (c and d" also known as "read" and "write")cA smart constructor for selectdA smart constructor for store `abcdefghij`bacd`abcd `abcdefghij (C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone%&+,9:;<=DOQRT k=A functor representing linear integer arithmetic: constants (q ), addition (t or r), multiplication (u or s), divisibility predicate (v) and ordering (w, x, y, z).q)A smart constructor for integer constantsr'A smart constructor for binary additions/A smart constructor for a binary multiplicationt+A smart constructor for a variadic additionu1A smart constructor for a variadic multiplicationv0A smart constructor for a divisibility predicatewA smart constructor for <xA smart constructor for >yA smart constructor for <=zA smart constructor for >=klmnopqSrTstuvwxyz{|}~klmnopqrstuvwxyzklmnopqtursvwxyzklmnopqSrTstuvwxyz{|}~r8s9 v7w7x7y7z7 (C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE)*Jakub Daniel <jakub.daniel@protonmail.com> experimentalNone%&+,9:;<=DOQRT/jA functor representing a mono-sorted existential quantifier binding a number of variables within a formulahA functor representing a mono-sorted universal quantifier binding a number of variables within a formula8A functor representing a logical connective for negation;A functor representing a logical connective for disjunction;A functor representing a logical connective for conjunctiontSubstitution that given an expression produces replacement if the expression is to be replaced or nothing otherwise.ZA functor representing a sorted variable, each variable is identified by its name and sort#Type of names assigned to variables4Bounded lattices that support complementing elementscomplement . complement = id#A language obtained as fixpoint of #A language obtained as fixpoint of #A language obtained as fixpoint of #A language obtained as fixpoint of #A language obtained as fixpoint of A language consisting solely of variables (useful for listing variables outside of any particular context, such as bound variables of quantified formula)A functor much like , with quantifiers over booleans and integersA functor representing the language of quantifier-free linear integer arithmetic and array theories in first order logic (much like " with additional array variables, c, and d)A functor much like , with quantifiers over booleans and integersA functor representing the language of quantifier-free linear integer arithmetic theory in first order logic (integer constants, integer variables, addition, multiplication, divisibility, ordering)A functor representing propositional logic embedded in first order logic (quantifier-free, boolean variables aka propositions, logical connectives , , , equality of propositions)A smart constructor for variables of any sort in any language Takes the variable name and infers the target language and sort from context. var "a" :: Lia 'IntegralSort LCollects a list of all variables occurring in an expression (bound or free).ZA simple constructor of substitutions that replaces the latter expression with the former.Executes a substitution. decomposes a boolean combination (formed with conjunctions and disjunctions, preferably in negation normal form) into its constituents.) decomposes a conjunction into conjuncts.) decomposes a disjunction into disjuncts.*A smart constructor for binary conjunction*A smart constructor for binary disjunction9A smart constructor for implication (an abbreviation for  not a .|. b)BA smart constructor for reversed implication (an abbreviation for  a .|. not b)1A smart constructor for if-and-only-if connective#A smart constructor for disequalityLogical tautologyLogical contradiction,A smart constructor for variadic conjunction,A smart constructor for variadic disjunction A smart constructor for negation1Test whether an expression contains a quantifier.6Tests whether an expression is free of any quantifier.ACollects a list of all free variables occurring in an expression.7A smart constructor for universally quantified formulae9A smart constructor for existentially quantified formulaeXPropagates negation toward boolean atoms (across conjunction, disjunction, quantifiers).VPuts an expression into prenex form (quantifier prefix and a quantifier-free formula).UReplaces non-variable and non-constant arguments to uninterpreted functions (such as c and d`) with a fresh bound (universally or existentially) variable that is bound to the original term. Replaces d( with an instance of its axiomatization.UVWXYZ[\]^_`abcdefghij      !"#$%&'()*+,-.HIJKLMNOPQ@ABRCD &'()+56789:;BCDEFGHIJKLMNOPQRSTUWXY`bacdklmnopqrstuvwxyz=UVWXYZ[\]^_`abcdefghij      !"#$%&'()*+,-.654437k  !"#$%&'()*+,-./0123456789:;<=>?@ABBCCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~                                                                   ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 789:;<=>?@ABCDEFGHIJKLMNOPQR ST SU SV SW SX SY SZ S[ S\ ] ^ _ ` a b  c d e f g h i j k l m n o p q r s t uv(expressions-0.1.2-BlTZgeUUNn0ESPo4JQDKysData.Expression.Sort"Data.Expression.Utils.Indexed.Show&Data.Expression.Utils.Indexed.Foldable Data.Expression.Utils.Indexed.Eq%Data.Expression.Utils.Indexed.Functor)Data.Expression.Utils.Indexed.Traversable!Data.Expression.Utils.Indexed.SumData.Expression.ParserData.Expression.EqualityData.Expression.ArrayData.Expression.ArithmeticData.Expression%singletons-2.2-6Xhmhx7QYPTLwUVmYMqwoMData.SingletonsSingIShowishow IFoldableifoldIEq1ieq1IEqieqIFunctorimapindexIFixunIFixicata $fShowIFix$fEqIFix $fIEqiIFix ITraversable itraverseimapM:<:injprj:+:InLInRinjectmatch $fIShowkk:+:$fITraversablei:+:$fIFoldablei:+: $fIEq1i:+: $f:<:kf:+: $f:<:kf:+:0$f:<:iff$fIFunctori:+:Sort BooleanSort IntegralSort ArraySortelement$fEqSort$fSingISortArraySort$fSingISortIntegralSort$fSingISortBooleanSort$fSingKindSort)$fSuppressUnusedWarnings(->)ArraySortSym0)$fSuppressUnusedWarnings(->)ArraySortSym1%$fSuppressUnusedWarnings(->)IndexSym0'$fSuppressUnusedWarnings(->)ElementSym0DynamicallySorted DynamicSort toStaticSorttoStaticallySorted parseSort$fShowDynamicallySorted$fEqDynamicallySorted$fEqDynamicSort $fShowSing $fShowSort $fSDecideSort ParseableparserParserContextparse parseWithcharchoicedecimaldigitlettermany1sepBy1signedspacestring identifier assertSort assumeSort$fParseable(->):+:h EqualityFEquals.=.$fParseable(->)EqualityFf$fIShowSortkEqualityF$fITraversableSortEqualityF$fIFoldableSortEqualityF$fIFunctorSortEqualityF$fIEq1SortEqualityFArrayFSelectStoreselectstore$fParseable(->)ArrayFf$fIShowSortSortArrayF$fITraversableSortArrayF$fIFoldableSortArrayF$fIFunctorSortArrayF$fIEq1SortArrayF ArithmeticFConstAddMulDividesLessThancnst.+..*.addmul.\..<..>..<=..>=.$fParseable(->)ArithmeticFf$fIShowSortSortArithmeticF$fITraversableSortArithmeticF$fIFoldableSortArithmeticF$fIFunctorSortArithmeticF$fIEq1SortArithmeticFUnstoreFlattenPrenexNNFMaybeQuantified ExistentialFExists UniversalFForall NegationFNot DisjunctionFOr ConjunctionFAnd SubstitutionrunSubstitutionVarFVar VariableNameComplementedLattice complementALiaQFALiaLiaQFLiaQFLogicALiaFQFALiaFLiaFQFLiaFQFLogicFvarvarsfor substituteliterals conjuncts disjuncts.&..|..->..<-..<->../=.truefalseandornot isQuantifiedisQuantifierFreefreevarsforallexistsnnfprenexflattenunstore $fUnstoref$fAxiomatizedfg$fAxiomatized:+:h$fAxiomatizedArrayFg $fForallkfg$fForall(->):+:h$fForall(->)UniversalFg $fFlattenf$fMaybeQuantified''fg$fMaybeQuantified'':+:h $fMaybeQuantified''ExistentialFg$fMaybeQuantified''UniversalFg$fMaybeQuantified''ArrayFg $fBind'fg $fBind':+:h$fBind'DisjunctionFg$fBind'ConjunctionFg$fBind'ArithmeticFg $fBind'VarFg $fBindkfg$fBind(->):+:h$fBind(->)ExistentialFg$fBind(->)UniversalFg $fPrenexf$fMaybeQuantified'fg$fMaybeQuantified':+:h$fMaybeQuantified'ExistentialFg$fMaybeQuantified'UniversalFg$fNNFf $fHasDualfg $fHasDual:+:h$fHasDualExistentialFg$fHasDualUniversalFg$fHasDualDisjunctionFg$fHasDualConjunctionFg$fHasDualNegationFg$fMaybeQuantifiedkf$fMaybeQuantifiedk:+:!$fMaybeQuantifiedSortExistentialF$fMaybeQuantifiedSortUniversalF$fMaybeQuantifiedSortVarF$fParseable(->)ExistentialFf$fParseable(->)UniversalFf$fIShowSortSortExistentialF$fIShowSortSortUniversalF$fITraversableSortExistentialF$fITraversableSortUniversalF$fIFoldableSortExistentialF$fIFoldableSortUniversalF$fIFunctorSortExistentialF$fIFunctorSortUniversalF$fIEq1SortExistentialF$fIEq1SortUniversalF$fParseable(->)NegationFf$fParseable(->)DisjunctionFf$fParseable(->)ConjunctionFf$fIShowSortSortNegationF$fIShowSortSortDisjunctionF$fIShowSortSortConjunctionF$fITraversableSortNegationF$fITraversableSortDisjunctionF$fITraversableSortConjunctionF$fIFoldableSortNegationF$fIFoldableSortDisjunctionF$fIFoldableSortConjunctionF$fIFunctorSortNegationF$fIFunctorSortDisjunctionF$fIFunctorSortConjunctionF$fIEq1SortNegationF$fIEq1SortDisjunctionF$fIEq1SortConjunctionF$fMonoidSubstitution$fParseable(->)VarFf$fIShowSortkVarF$fITraversableSortVarF$fIFoldableSortVarF$fIFunctorSortVarF$fIEq1SortVarF$fComplementedLatticeIFix$fComplementedLatticeIFix0$fComplementedLatticeIFix1$fComplementedLatticeIFix2$fComplementedLatticeIFix3$fBoundedLatticeIFix$fBoundedLatticeIFix0$fBoundedLatticeIFix1$fBoundedLatticeIFix2$fBoundedLatticeIFix3$fBoundedMeetSemiLatticeIFix$fBoundedMeetSemiLatticeIFix0$fBoundedMeetSemiLatticeIFix1$fBoundedMeetSemiLatticeIFix2$fBoundedMeetSemiLatticeIFix3$fBoundedJoinSemiLatticeIFix$fBoundedJoinSemiLatticeIFix0$fBoundedJoinSemiLatticeIFix1$fBoundedJoinSemiLatticeIFix2$fBoundedJoinSemiLatticeIFix3 $fLatticeIFix$fLatticeIFix0$fLatticeIFix1$fLatticeIFix2$fLatticeIFix3$fMeetSemiLatticeIFix$fMeetSemiLatticeIFix0$fMeetSemiLatticeIFix1$fMeetSemiLatticeIFix2$fMeetSemiLatticeIFix3$fJoinSemiLatticeIFix$fJoinSemiLatticeIFix0$fJoinSemiLatticeIFix1$fJoinSemiLatticeIFix2$fJoinSemiLatticeIFix3baseGHC.ShowShowSSort ArraySortSym0ArraySortSym0KindInference ArraySortSym1ArraySortSym1KindInference ArraySortSym2IntegralSortSym0BooleanSortSym0IndexElement IndexSym0IndexSym0KindInference IndexSym1 ElementSym0ElementSym0KindInference ElementSym1 SBooleanSort SIntegralSort SArraySortsIndexsElementD:R:DemoteRepSortshow' ssortToSort!Data.Singletons.Prelude.InstancesSTrueSFalseSTuple0STuple7STuple6STuple5STuple4STuple3STuple2SLambda applySing mergeConstAdd mergeConstMul Axiomatized instantiatequantifyMaybeQuantified''flatten'Bind'bind'BindbindMaybeQuantified'pushQuantifierHasDualdual isQuantified' freevars' conjuncts' disjuncts'freename freenamespushQuantifier'bind''