h$MAl      !"#$%&'()*+,-./0123456789:;<=>?@AB C D E F G H I J K L M N O P Q R S T U V W 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 { | } ~                                                                                                                                                None%&'(-/2389>? ONone %&'(-/2389>? Q ectaTried using the BasicHashtable size function to remove need for this IORef ( see  4https://github.com/gregorycollins/hashtables/pull/68 ), but it was slower   None%&'(-/2389>? None%&'(-/2389>?   None %&'(-/2389>? i()()None  %&'(-/2389>? +,-.+,-.None# %&'(-/2389>? 345678345678None %&'(-/2389>? hNone%&'(-/2389>? ?@A?@A None  %&'(-/2389>?p EectaMust be sortedOectaTODO: Should this be redone as a lens-library traversal? | TODO: I am unhappy about this Emptyable design; makes one question whether this should be a typeclass at all. (Terms/ECTAs differ in that there is always an ECTA Node that represents the value at a path)WectaTODO: This pattern (and the caching of the original path list) is a temporary affair until we convert all clients of PathEclass to fully be based on tries`ecta+Read `substSubpath p1 p2 p3` as `[p1/p2]p3`2`substSubpath replacement toReplace target` takes  toReplace8, a prefix of target, and returns a new path in which  toReplace has been replaced by  replacement.0Undefined if toReplace is not a prefix of targetaecta$Precondition: A nonempty cell existsbecta$Precondition: A nonempty cell existsfecta:Precondition: No path in the input is a subpath of anotherkectaExtends the subsumption ordering to a total ordering by using the default lexicographic comparison for incomparable elements. | TODO: Optimization opportunity: Redundant work in the hasSubsumingMember callspectaThe real contradiction condition is a cycle in the subsumption ordering. But, after congruence closure, this will reduce into a self-cycle in the subsumption ordering.TODO; Prove this.5BVCDEFWGHIJNLKMOPQRSTYXUZ[\]^_`abcdefghijklmnopqrstuv9TYXUYXZ[OPQRS\]^_`abcJNLKMdefghFWGHIWijkBVCDEVmlopqrsntuvNone%&'(-/2389>?)$BVFHJLOPQRSTYXZ[\]^cdefghijklnqrstuv'TYXYXZ[OPQRS\]^JLdecfghFHijkBVVlqrsntuv None  %&'(-/2389>?None%&'(-/2389>?! None%&'(-/2389>?ectaThe semantics of this may not be what you expect: Path trie zippers do not support editing currently, only traversing. The value at the cursor (as well as the index) is ignored except when traversing above the root, where it uses those values to extend the path trie upwards.   None! %&'(-/2389>?/ectaRecursive node,The function should be parametric in the Id:  substFree i (Rec j) (f i) == f jSee  for additional discussion.ectaThe  of the node itselfectaAll outgoing edgesecta$Maximum Mu nesting depth in the termectaFree variables in the termecta of the node itselfectaThe body of the ,Recursive occurrences to this node should be Rec (RecNodeId internedMuId)ectaThe body of the , before it was assigned an  Invariant:  substFree internedMuId (Rec (RecUnint (numNestedMu internedMuBody)) internedMuBody == internedMuShapeectaContext-free references to a  node introduced by  intersectBackground: This is a generalization of the idea to be able to refer to the "immediately enclosing binder", and then only deal with graphs with the property that we never need to refer past that enclosing binder. This too would allow us to refer to a  node without knowing its , at the cost of requiring a substitution when we discover that  to return this into a ,. The generalization is that all we need to some way to refer to that  node concretely, without &, but we can: intersection introduces  whenever it encounters a  on the left or the right, /and will then not introduce another  for that same intersection problem (at least, not in the same scope). This means that the  of the left and right operand will indeed uniquely identify the  node to be constructed by  intersect.Furthermore, since we cache the free variables in a term, we have a cheap check to see if we need the  node at all. This means that if the input graphs satisfy the property that there are references past  nodes, the output should too: we will not introduce redundant  nodes.NOTE: Although intersect has three cases in which it introduces  nodes ( in both operands,  in the left, or  in the right), we don't need that distinction here: we just need to know the  of the two operands, so that if we see a call to intersect again with those same two operands (no matter what kind of nodes they are), we can refer to the newly constructed  node.ectaReference to the  of an interned  nodeecta"Reference to an as-yet uninterned  node, for which the  is not yet knownThe 9 argument is used to distinguish between multiple nested  nodes.#NOTE: This is intentionally not an : it does not refer to the  of any interned node.ecta!Placeholder variable that we use only for depth calculations The invariant that this is used only for depth calculations, along with the observation that depth calculation does not depend on the exact choice of variable, justifies subtituting any other variable for  in terms containing  in all contexts.ecta6Refer to Mu-node-to-be-constructed during intersectionTODO: It is obviously not very elegant to have a constructor here specifically for one algorithm. Ideally, we would parameterize  with the type of the identifiers in it. This might be useful also to rule out many other cases (specifically, most of the time we are dealing with fully interned nodes, and so the only constructor we expect is ).ectaPattern only a Mu constructorWhen we go underneath a Mu constructor, we need to bind the corresponding Rec node to something: that's why pattern matching on  yields a function. Code that wants to traverse the term as-is should match on the interned constructors instead (and then deal with the dangling references).An identity function foo (Mu f) = Mu fwill run in O(1) time: foo (Mu f) = Mu f -- { expand view patern } foo node | Just f <- matchMu node = createMu f -- { case for @InternedMu mu@ } foo (InternedMu mu) | Just f <- matchMu (InternedMu m) = createMu f -- { definition of matchMu } foo (InternedMu mu) = let f = \n' -> if | n' == Rec (RecUnint (numNestedMu (internedMuBody mu))) -> internedMuShape mu | n' == Rec RecDepth -> internedMuShape mu | otherwise -> substFree (internedMuId mu) n' (internedMuBody mu) in createMu f -- { definition of createMu } foo (InternedMu mu) = intern $ UninternedMu (f . Rec)At this point,  will call `shape (f . Rec)`, which will call `f . Rec` twice: once with  to compute the depth, and then once again with that depth to substitute a placeholder. Both of these special cases will use ) (and moreover, the depth calculation on  is O(1)).ecta(Maximum number of nested Mus in the term@O(1) provided that there are no unbounded Mu chains in the term.ectaFree variables in the termO(1) in the size of the graph, provided that there are no unbounded Mu chains in the term. O(log n)@ in the number of free variables in the graph, which we expect to be orders of magnitude smaller than the size of the graph (indeed, we don't expect more than a handful).ectaAn optimized Node constructor that avoids the interning/preprocessing of the Node constructor when nothing changesectaConstruct recursive nodeImplementation note:  and / interact in non-trivial ways; see docs of the 1 pattern synonym for performance considerations.ecta Substitution substFree i n! will replace all occurrences of Rec (RecNodeId i) by n. We appeal to the uniqueness of node IDs and assume that all occurrences of i7 must be free (in other words, that any occurrences of  will have a  different identifier.Postcondition: %substFree i (Rec (RecNodeId i)) == id36 None%&'(-/2389>?0Mecta$PRECONDITION: (h x == h y) => x == yNone! %&'(-/2389>?1ectaWarning: Linear in number of paths, exponential in size of graph. Only use for very small graphs.ectaPrecondition: For all i, f (Rec i) is either a Rec node meant to represent the enclosing Mu, or contains no Rec node not beneath another Mu.None  %&'(-/2389>?3 ectaTo visualize an FTA: 1) Call `prettyPrintDot $ toDot fta` from GHCI 2) Copy the output to viz-js.jom or another GraphViz implementationNone" %&'(-/2389>?7XectaInefficient enumerationFor ECTAs with  nodes may produce an infinite list or may loop indefinitely, depending on the ECTAs. For example, for 1createMu $ \r -> Node [Edge "f" [r], Edge "a" []]it will produce [ Term "a" [] , Term "f" [Term "a" []] , Term "f" [Term "f" [Term "a" []]] , ... ]This happens to work currently because non-recursive edges are interned before recursive edges.TODO: It would be much nicer if this did fair enumeration. It would avoid the beforementioned dependency on interning order, and it would give better enumeration for examples such as Node [Edge "h" [ createMu $ \r -> Node [Edge "f" [r], Edge "a" []] , createMu $ \r -> Node [Edge "g" [r], Edge "b" []] ]]This will currently produce [ Term "h" [Term "a" [], Term "b" []] , Term "h" [Term "a" [], Term "g" [Term "b" []]] , Term "h" [Term "a" [], Term "g" [Term "g" [Term "b" []]]] , .. ]where it always unfolds the second argument to h, never the first.++None %&'(-/2389>?8P!None%&'(-/2389>?9None  %&'(-/2389>?9None  %&'(-/2389>?:cNone! %&'(-/2389>?:>>None! %&'(-/2389>?< None  %&'(-/2389>?A0ectaOur construction generalizes to arbitrary NNF formulas, and possibly to arbitrary SAT, but we don't need to bother; just CNF is good enoughecta+Encoding: formula(assnNode, formulaNode)assnNode: * One edge, with one child per literal (2*numVars total) * Each literal has two choices, true or false * Use constraints to force each positive/negative pair of literals to match. * E.g.: x1 node = choice of (0, a) or (1, b). ~x1 node = choice of (0, b) or (1, a) If x1~x1 have indices 091, then the constraint 0.1=1.1 constrains x1~x1 to be either truefalse or false/true6formulaNode: * One edge, having one child per clauseClause nodes: * One edge per literal in the clause, each corresponding to a choice of which variable makes the clause true. * Each edge has 2*numVars children containing a copy of the assnNode, followed by a single child containing "1" * Constrain said final child to be equal to the truth value of the corresponding literal in those 2*numVars children which copy the assnNodeTop level constraints: * Constrain the variable nodes in each clause node to be equal to the global variable assignments. !"#$$%&'()*++,-./0123456789:;<=>?@ABCCDEFGHIJKLMNOPQRSTUVWX Y Y Z [ \ ] ^ _ ` a b c ` d e f g h i i j \ k l m n o p q r s t u v w x y z { | } ~                                                                                                                                                                  5  #ecta-1.0.0.3-GsgcdoZGkFZA4oJqDsbHRSData.HashTable.Extended%Data.Interned.Extended.HashTableBased%Data.Interned.Extended.SingleThreadedData.Persistent.UnionFindData.Text.Extended.PrettyData.Memoization.MetricsData.MemoizationUtility.FixpointData.ECTA.Internal.PathsData.ECTA.Internal.TermData.ECTA.Internal.Paths.ZipperData.ECTA.Internal.ECTA.TypeUtility.HashJoin"Data.ECTA.Internal.ECTA.Operations%Data.ECTA.Internal.ECTA.Visualization#Data.ECTA.Internal.ECTA.EnumerationApplication.TermSearch.TypeApplication.TermSearch.UtilsApplication.TermSearch.Dataset!Application.TermSearch.TermSearch!Application.TermSearch.EvaluationApplication.SAT Paths_ectaData.ECTA.PathsData.ECTA.Term Data.ECTA AnyHashTablegetKeysresetHashTableInterned Description UninterneddescribeidentifycacheCachefreshcontentId freshCache cacheSize resetCacheintern UnionFindUVarUVarGen initUVarGennextUVar uvarToInt intToUVaremptywithInitialValuesunionfind $fEqUnionFind$fOrdUnionFind$fShowUnionFind$fEqUVar $fOrdUVar $fShowUVar $fEqUVarGen $fOrdUVarGen $fShowUVarGenPrettypretty $fPrettya CacheMetrics queryCount missCount$fPrettyCacheMetrics$fEqCacheMetrics$fOrdCacheMetrics$fShowCacheMetrics MemoCacheTagNameTagresetAllCachesmemoIOmemomemo2$fPrettyMemoCacheTag$fHashableMemoCacheTag$fEqMemoCacheTag$fOrdMemoCacheTag$fShowMemoCacheTag$fGenericMemoCacheTagfix fixUnboundedfixMaybe EqConstraintsEqContradiction getEclasses PathEClass PathEClass' getPathTrie getOrigPathsPathTrie EmptyPathTrieTerminalPathTriePathTrieSingleChildPathable EmptyablegetPath getAllAtPath modifyAtPathPathEmptyConstraintsConsPath EmptyPathunPathpathpathHeadUnsafepathTailUnsafe isSubpathisStrictSubpath substSubpathsmallestNonemptylargestNonemptygetMaxNonemptyIndexisEmptyPathTrieisTerminalPathTrie toPathTrie fromPathTriepathTrieDescend unPathEClasshasSubsumingMembercompletedSubsumptionOrderingunsafeGetEclassesrawMkEqConstraintsconstraintsAreContradictoryhasSubsumingMemberListBasedisContradictingmkEqConstraintscombineEqConstraintseqConstraintsDescendconstraintsImplysubsumptionOrderedEclasses unsafeSubsumptionOrderedEclasses $fPrettyPath$fHashablePath $fOrdPathTrie$fHashablePathTrie$fHashablePathEClass$fPrettyPathEClass$fOrdPathEClass$fEqPathEClass$fPrettyEqConstraints$fHashableEqConstraints$fEqEqConstraints$fOrdEqConstraints$fShowEqConstraints$fGenericEqConstraints$fShowPathEClass$fGenericPathEClass $fEqPathTrie$fShowPathTrie$fGenericPathTrie$fEqPath $fOrdPath $fShowPath $fGenericPathTermSymbolSymbol' $fReadSymbol$fIsStringSymbol$fHashableSymbol $fShowSymbol$fPrettySymbol$fPathableTermTerm $fPrettyTerm$fHashableTerm$fEqTerm $fOrdTerm $fReadTerm $fShowTerm $fGenericTerm $fEqSymbol $fOrdSymbolPathTrieZipperInvertedPathTriePathZipperRoot PathTrieAt unionPathTrieemptyPathTrieZipperpathTrieToZipperzipperCurPathTrieunionPathTrieZipperpathTrieZipperDescendpathTrieZipperAscend$fEqPathTrieZipper$fOrdPathTrieZipper$fShowPathTrieZipper$fEqInvertedPathTrie$fOrdInvertedPathTrie$fShowInvertedPathTrieUninternedEdge uEdgeSymbol uEdgeChildrenuEdgeEcsUninternedNodeUninternedEmptyNode UninternedMuNode InternedNode EmptyNode InternedMuRecMkInternedNodeinternedNodeIdinternedNodeEdgesinternedNodeNumNestedMuinternedNodeFree MkInternedMu internedMuIdinternedMuBodyinternedMuShapeEdge InternedEdgeedgeIduninternedEdge IntersectId RecNodeIdRecIntRecUnintRecDepth RecIntersectMu edgeSymbol edgeChildrenedgeEcs numNestedMufreeVars nodeIdentity setChildren emptyEdgemkEdge modifyNodecreateMu substFree$fHashableIntersectId$fHashableRecNodeId$fHashableDescription$fInternedEdge$fHashableUninternedEdge$fHashableDescription0$fHashableNode $fOrdNode $fShowNode$fEqNode$fHashableEdge $fOrdEdge$fEqEdge $fShowEdge$fInternedNode$fHashableUninternedNode$fEqUninternedNode$fEqDescription$fGenericDescription$fEqDescription0$fGenericDescription0$fEqUninternedEdge$fShowUninternedEdge$fGenericUninternedEdge$fShowInternedNode$fShowInternedMu $fEqRecNodeId$fOrdRecNodeId$fShowRecNodeId$fGenericRecNodeId$fEqIntersectId$fOrdIntersectId$fShowIntersectId$fGenericIntersectIdnubByIdnubByIdSinglePasshashClusterIdNub clusterByHashhashJoin pathsMatchingmapNodescrush onNormalNodesunfoldOuterRec nodeEdgesrefold unfoldBounded nodeCount edgeCount maxIndegreenodeRepresentsedgeRepresentsdropRedundantEdges intersectEdge intersect requirePathrequirePathListwithoutRedundantEdgesreducePartiallyreduceEdgeIntersectionreduceEqConstraintsgetSubnodeById$fPathable[]Node$fPathableNodeNode$fHashableIntersectionDom$fShowIntersectionDom$fEqIntersectionDomtoDot$fMonoidPartialGraph$fSemigroupPartialGraph$fEqFglNodeLabel$fOrdFglNodeLabel$fShowFglNodeLabel$fShowPartialGraphEnumerationState _uvarCounter_uvarRepresentative _uvarValues UVarValueUVarUnenumeratedUVarEnumeratedUVarEliminatedcontents constraints termFragmentSuspendedConstraint TermFragmentTermFragmentNodeTermFragmentUVartermFragToTruncatedTerm scGetPathTrie scGetUVar descendScs$fEqEnumerationState$fOrdEnumerationState$fShowEnumerationState $fEqUVarValue$fOrdUVarValue$fShowUVarValue$fEqSuspendedConstraint$fOrdSuspendedConstraint$fShowSuspendedConstraint$fEqTermFragment$fOrdTermFragment$fShowTermFragment EnumerateM uvarCounteruvarRepresentative uvarValuesinitEnumerationState runEnumerateM getUVarValuegetTermFragForUVargetUVarRepresentativeassimilateUvarValmergeNodeIntoUVarVal enumerateNode enumerateEdgefirstExpandableUVarenumerateOutUVarenumerateOutFirstExpandableUVarenumerateFullyexpandTermFrag expandUVargetAllTruncatedTerms getAllTermsnaiveDenotation AblationTypeDefault NoReduction NoEnumeration NoOptimizeModeNormalHKTVLambdaArgument BenchmarkbmNamebmSize bmSolution bmArguments bmGoalType TypeSkeletonTVarTFunTCons$fHashableTypeSkeleton$fEqAblationType$fOrdAblationType$fShowAblationType$fDataAblationType$fGenericAblationType$fEqMode $fOrdMode $fShowMode $fDataMode $fGenericMode $fEqBenchmark$fOrdBenchmark$fShowBenchmark$fReadBenchmark$fEqTypeSkeleton$fOrdTypeSkeleton$fShowTypeSkeleton$fReadTypeSkeleton$fDataTypeSkeleton$fGenericTypeSkeleton typeConst constrType0 constrType1 constrType2 maybeTypelistType theArrowNode arrowTypeappType mkDatatype constFuncconstArgvar1var2var3var4varAccmkGroupsgetRepOf replicatorTau replicatorloop1loop2 typeToFtaspeciallyTreatedFunctionshooglePlusComponentsaugumentedComponentshoogleComponents groupMappingtauallConstructors generalizeapp applyOperator hoogleCompsanyFunc filterTypetermsK relevantTermKrelevantTermsOfSizerelevantTermsUptoK prettyTerm dropTypesgetText fromJustFuncmaybeFunctionslistRepsisListFunction maybeRepsisMaybeFunction anyListFuncanyNonListFunc anyNonNilFuncanyNonNothingFunc reduceFully checkSolutionreduceFullyAndLogf1f2f3f4f5f6f7f8f9f10f11f12f13f14f15f16f17f18f19f20f21f22f23f24f25f26f27f28f29f30 toMappedNameprettyPrintAllTerms substTermparseHoogleComponent runBenchmarkLitPosLitNegLitClauseOrCNFAndVarmkVartoEcta allSolutionsex1ex2ex3 $fIsStringVar $fHashableVar $fPrettyLit $fHashableLit$fHashableClause $fHashableCNF $fFoldAlgLit$fFoldAlgClause $fFoldAlgCNF$fMonoidLitPaths$fSemigroupLitPaths$fEqCNF$fOrdCNF $fShowCNF $fGenericCNF $fEqClause $fOrdClause $fShowClause$fGenericClause$fEqLit$fOrdLit $fShowLit $fGenericLit$fEqVar$fOrdVar $fShowVar $fGenericVarversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileNameshapeghc-prim GHC.TypesIntmatchMu