Documentation

Aesop.Tree.Data

Node IDs #

structure Aesop.GoalId :
Instances For
    Equations
    Equations
    Instances For
      Equations
      Instances For
        Equations
        • { toNat := n }.succ = { toNat := n + 1 }
        Instances For
          Equations
          Instances For
            Equations
            Equations

            Rule Application IDs #

            structure Aesop.RappId :
            Instances For
              Equations
              Equations
              Instances For
                Equations
                • { toNat := n }.succ = { toNat := n + 1 }
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Equations

                      Iterations #

                      Equations
                      Instances For

                        The Tree #

                        At each point during the search, every node of the tree (goal, rapp or mvar cluster) is in one of these states:

                        • proven: the node is proven.
                        • unprovable: the node is unprovable, i.e. it will never be proven regardless of any future expansions that might be performed.
                        • unknown: neither of the above.

                        Every node starts in the unknown state and may later become either proven or unprovable. After this, the state does not change any more.

                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Equations
                          Instances For
                            Equations
                            Instances For
                              Equations
                              Instances For

                                A refinement of the NodeState, distinguishing between goals proven during normalisation and goals proven by a child rule application.

                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          • s.isIrrelevant = s.toNodeState.isIrrelevant
                                          Instances For
                                            Equations
                                            Instances For
                                              Equations
                                              Instances For

                                                A goal G can be added to the tree for three reasons:

                                                1. G was produced by its parent rule as a subgoal. This is the most common reason.
                                                2. G was copied because it contains some metavariables which were assigned by its parent rule. In this case, we record goal of which G is a copy. We also record the representative of the equivalence class of goals which are copies of each other. E.g. if goal 1 is copied to goal 2 and goal 2 is copied to goal 3, they are all part of the equivalence class with representative 1.
                                                Instances For
                                                  Equations
                                                  Instances For
                                                    Equations
                                                    Instances For
                                                      structure Aesop.GoalData (Rapp : Type) (MVarCluster : Type) :
                                                      Instances For
                                                        instance Aesop.instNonemptyGoalData :
                                                        ∀ {Rapp MVarCluster : Type} [inst : Nonempty MVarCluster], Nonempty (Aesop.GoalData Rapp MVarCluster)
                                                        Equations
                                                        • =
                                                        structure Aesop.MVarClusterData (Goal : Type) (Rapp : Type) :
                                                        Instances For
                                                          Equations
                                                          • Aesop.instInhabitedMVarClusterData = { default := { parent? := default, goals := default, isIrrelevant := default, state := default } }
                                                          structure Aesop.RappData (Goal : Type) (MVarCluster : Type) :
                                                          Instances For
                                                            instance Aesop.instNonemptyRappData :
                                                            ∀ {Goal : Type} [inst : Nonempty Goal] {MVarCluster : Type}, Nonempty (Aesop.RappData Goal MVarCluster)
                                                            Equations
                                                            • =
                                                            structure Aesop.TreeSpec :
                                                            Instances For
                                                              Instances For
                                                                @[implemented_by Aesop.treeImpl]
                                                                Equations
                                                                Instances For
                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    Instances For
                                                                      @[reducible, inline]
                                                                      Equations
                                                                      Instances For
                                                                        @[reducible, inline]
                                                                        Equations
                                                                        Instances For
                                                                          @[reducible, inline]
                                                                          Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            Equations
                                                                            • c.parent? = c.elim.parent?
                                                                            Instances For
                                                                              @[inline]
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[inline]
                                                                                Equations
                                                                                • c.goals = c.elim.goals
                                                                                Instances For
                                                                                  @[inline]
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    Equations
                                                                                    • c.isIrrelevant = c.elim.isIrrelevant
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        Equations
                                                                                        • c.state = c.elim.state
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            @[inline]
                                                                                            Equations
                                                                                            • g.id = g.elim.id
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              Equations
                                                                                              • g.parent = g.elim.parent
                                                                                              Instances For
                                                                                                @[inline]
                                                                                                Equations
                                                                                                • g.children = g.elim.children
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  Equations
                                                                                                  • g.origin = g.elim.origin
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    Equations
                                                                                                    • g.depth = g.elim.depth
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      Equations
                                                                                                      • g.state = g.elim.state
                                                                                                      Instances For
                                                                                                        @[inline]
                                                                                                        Equations
                                                                                                        • g.isIrrelevant = g.elim.isIrrelevant
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          Equations
                                                                                                          • g.isForcedUnprovable = g.elim.isForcedUnprovable
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            Equations
                                                                                                            • g.preNormGoal = g.elim.preNormGoal
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              Equations
                                                                                                              • g.normalizationState = g.elim.normalizationState
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                Equations
                                                                                                                • g.mvars = g.elim.mvars
                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  Equations
                                                                                                                  • g.successProbability = g.elim.successProbability
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    Equations
                                                                                                                    • g.addedInIteration = g.elim.addedInIteration
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      Equations
                                                                                                                      • g.lastExpandedInIteration = g.elim.lastExpandedInIteration
                                                                                                                      Instances For
                                                                                                                        @[inline]
                                                                                                                        Equations
                                                                                                                        • g.failedRapps = g.elim.failedRapps
                                                                                                                        Instances For
                                                                                                                          @[inline]
                                                                                                                          Equations
                                                                                                                          • g.unsafeRulesSelected = g.elim.unsafeRulesSelected
                                                                                                                          Instances For
                                                                                                                            @[inline]
                                                                                                                            Equations
                                                                                                                            • g.unsafeQueue = g.elim.unsafeQueue
                                                                                                                            Instances For
                                                                                                                              @[inline]
                                                                                                                              Equations
                                                                                                                              • g.unsafeQueue? = if g.unsafeRulesSelected = true then some g.unsafeQueue else none
                                                                                                                              Instances For
                                                                                                                                @[inline]
                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  @[inline]
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    @[inline]
                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      @[inline]
                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For
                                                                                                                                        @[inline]
                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For
                                                                                                                                          @[inline]
                                                                                                                                          Equations
                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                          Instances For
                                                                                                                                            @[inline]
                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            Instances For
                                                                                                                                              @[inline]
                                                                                                                                              Equations
                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                Equations
                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                Instances For
                                                                                                                                                  @[inline]
                                                                                                                                                  Equations
                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                  Instances For
                                                                                                                                                    @[inline]
                                                                                                                                                    Equations
                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        Equations
                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def Aesop.Goal.setUnsafeRulesSelected (unsafeRulesSelected : Bool) (g : Aesop.Goal) :
                                                                                                                                                          Equations
                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]
                                                                                                                                                            Equations
                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                            Instances For
                                                                                                                                                              @[inline]
                                                                                                                                                              Equations
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For
                                                                                                                                                                  Equations
                                                                                                                                                                  @[inline]
                                                                                                                                                                  Equations
                                                                                                                                                                  • r.id = r.elim.id
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    Equations
                                                                                                                                                                    • r.parent = r.elim.parent
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[inline]
                                                                                                                                                                      Equations
                                                                                                                                                                      • r.children = r.elim.children
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]
                                                                                                                                                                        Equations
                                                                                                                                                                        • r.state = r.elim.state
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          Equations
                                                                                                                                                                          • r.isIrrelevant = r.elim.isIrrelevant
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[inline]
                                                                                                                                                                            Equations
                                                                                                                                                                            • r.appliedRule = r.elim.appliedRule
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[inline]
                                                                                                                                                                              Equations
                                                                                                                                                                              • r.scriptSteps? = r.elim.scriptSteps?
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[inline]
                                                                                                                                                                                Equations
                                                                                                                                                                                • r.originalSubgoals = r.elim.originalSubgoals
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[inline]
                                                                                                                                                                                  Equations
                                                                                                                                                                                  • r.successProbability = r.elim.successProbability
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[inline]
                                                                                                                                                                                    Equations
                                                                                                                                                                                    • r.metaState = r.elim.metaState
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[inline]
                                                                                                                                                                                      Equations
                                                                                                                                                                                      • r.introducedMVars = r.elim.introducedMVars
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[inline]
                                                                                                                                                                                        Equations
                                                                                                                                                                                        • r.assignedMVars = r.elim.assignedMVars
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[inline]
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[inline]
                                                                                                                                                                                            Equations
                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[inline]
                                                                                                                                                                                              Equations
                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                Equations
                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  Equations

                                                                                                                                                                                                                  Miscellaneous Queries #

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  • r.isSafe = (r.appliedRule.isSafe && r.assignedMVars.isEmpty)
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        • g.currentGoal = g.postNormGoal?.getD g.preNormGoal
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          • g.parentRapp? = do let __do_liftST.Ref.get g.parent pure __do_lift.parent?
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • g.isExhausted = (pure g.isUnsafeExhausted <||> g.hasSafeRapp)
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        • g.isActive = do let __do_liftpure g.isIrrelevant <||> g.isExhausted pure !__do_lift
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • g.hasMVar = !g.mvars.isEmpty
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  • g.isNormal = g.normalizationState.isNormal
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    • g.originalGoalId = g.origin.originalGoalId?.getD g.id
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                      • g.isRoot = do let __do_liftg.parentRapp? pure __do_lift.isNone
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        • r.introducesMVar = !r.introducedMVars.isEmpty
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          • r.parentPostNormMetaState rootMetaState = do let __do_liftST.Ref.get r.parent __do_lift.parentMetaState rootMetaState
                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                            def Aesop.Rapp.foldSubgoalsM {m : TypeType} {σ : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (init : σ) (f : σAesop.GoalRefm σ) (r : Aesop.Rapp) :
                                                                                                                                                                                                                                                            m σ
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    Instances For