Documentation

Aesop.Tree.Data

Node IDs #

structure Aesop.GoalId :
Instances For
    Equations
    Equations
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            Equations

            Rule Application IDs #

            structure Aesop.RappId :
            Instances For
              Equations
              Equations
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      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
                                Equations
                                • One or more equations did not get rendered due to their size.
                                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
                                            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
                                                        • 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
                                                                          @[inline, reducible]
                                                                          Equations
                                                                          Instances For
                                                                            @[inline, reducible]
                                                                            Equations
                                                                            Instances For
                                                                              @[inline, reducible]
                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[inline]
                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[inline]
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[inline]
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    Equations
                                                                                                                    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
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]
                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[inline]
                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[inline]
                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[inline]
                                                                                                                                                                      Equations
                                                                                                                                                                      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 #

                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                Equations
                                                                                                                                                                                                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
                                                                                                                                                                                                          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
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  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
                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          Instances For