Documentation

Aesop.Tree.Data

Node IDs #

structure Aesop.GoalId :
Instances For
    Equations
    Equations
    Instances For
      Equations
      Instances For
        Equations
        • x.succ = match x with | { toNat := n } => { toNat := n + 1 }
        Instances For
          Equations
          Instances For
            Equations
            Equations

            Rule Application IDs #

            structure Aesop.RappId :
            Instances For
              Equations
              Equations
              Instances For
                Equations
                • x.succ = match x with | { toNat := n } => { 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
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • s.isIrrelevant = s.toNodeState.isIrrelevant
                                            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
                                                  • 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

                                                      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
                                                          • One or more equations did not get rendered due to their size.
                                                          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
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    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