Documentation

Validator.Certificate.Parser

Parser for Certificates #

This file contains a parser for parsing certificates for the proof system.

source
instance Certificate.instCoeResultParserSubtype {α : Type} {p : α → Prop} :
Coe (Validator.Result α p) (Validator.Parser { a : α // p a })
Equations
source
def Certificate.parseActionSetExpr (idx : ℕ) :
Validator.Parser Validator.ActionSetExpr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Certificate.parserTODO {α : outParam Type} :
    Validator.Parser α
    Equations
    Instances For
      source
      def Certificate.parseConstStateSetExpr {n : ℕ} (pt : Validator.STRIPS n) :
      Validator.Parser (Validator.StateSetExpr pt)
      Equations
      Instances For
        source
        def Certificate.parseBdd {n : ℕ} (pt : Validator.STRIPS n) :
        Validator.Parser (Validator.StateSetExpr pt)
        Equations
        Instances For
          source
          def Certificate.parseStateSetExpr {n : ℕ} (pt : Validator.STRIPS n) (idx : ℕ) :
          Validator.Parser (Validator.StateSetExpr pt)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Certificate.parseDeadKnowledge :
            Validator.Parser Validator.Knowledge
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Certificate.parseUnsolvableKnowledge :
              Validator.Parser Validator.Knowledge
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Certificate.parseSubsetKnowledge :
                Validator.Parser Validator.Knowledge
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Certificate.parseKnowledge (idx : ℕ) :
                  Validator.Parser Validator.Knowledge
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    partial def Certificate.parseCertificate {n : ℕ} (pt : Validator.STRIPS n) (C : Validator.Certificate pt := { actions := #[], states := #[], knowledge := #[] }) :
                    Validator.Parser (Validator.Certificate pt)
                    source
                    def Certificate.parse {n : ℕ} (pt : Validator.STRIPS n) (path : System.FilePath) :
                    IO (Validator.Certificate pt)

                    Try to read the file at the given path, and try to parse it into a certificate for the planing task pt. Each line of the certificate is expected to either be an action set expression, a state set expression, a piece of knowledge or a comment (starting with #).

                    Action set expressions have the following formats, where <AID> stands for action set ID. The action set ID after a is the ID of the action set itself, it should start at 0 and increase by one for each action set expression.

                    a <AID> b <amount of actions> <list of action IDs>         (list of actions)
a <AID> u <AID left> <AID right>                           (union of actions)
a <AID> a                                                  (set of all actions)

                    State set expressions have the following formats, where <SID> stands for state set ID. The state set ID after e is the ID of the state set itself, it should start at 0 and increase by one for each state set expression.

                    e <SID> c e                                                 (constant empty set)
e <SID> c i                                                 (constant initial state set)
e <SID> c g                                                 (constant goal set)
e <SID> b <bdd_filename> <bdd_index>                        (bdd set)
e <SID> t <discription in DIMACS>                           (horn set)
e <SID> e <TODO>                                            (MODS set)
e <SID> n <ID of negated state set>                         (negation)
e <SID> i <SID left> <SID right>                            (intersection)
e <SID> u <SID left> <SID right>                            (union)
e <SID> p <SID> <AID>                                       (progression)
e <SID> r <SID> <AID>                                       (regression)

                    Knowledge expressions have the following formats, where <KID> stands for knowledge ID. The knowledge ID after k is the ID of the knowledge itself, it should start at 0 and increase by one for each piece of knowledge. For dead knowledge, the ID after d is the ID of state set that is dead, and for subset knowledge the IDs after s are the IDs corresponding to the left and right state set. The knowledge IDs after the rule are the IDs of the premises.

                    k <KID> d <SID> ed                                          (empty set dead)
k <KID> d <SID> ud <KID> <KID>                              (union dead)
k <KID> d <SID> sd <KID> <KID>                              (subset dead)
k <KID> d <SID> pg <KID> <KID> <KID>                        (progression goal)
k <KID> d <SID> pi <KID> <KID> <KID>                        (progression initial)
k <KID> d <SID> sd <KID> <KID> <KID>                        (regression goal)
k <KID> d <SID> pg <KID> <KID> <KID>                        (regression initial)
k <KID> u ci <KID>                                          (conclusion initial)
k <KID> u cg <KID>                                          (conclusion goal)
k <KID> s <SID> <SID> urs                                   (union right state)
k <KID> s <AID> <AID> ura                                   (union right action)
k <KID> s <SID> <SID> uls                                   (union left state)
k <KID> s <AID> <AID> ula                                   (union left action)
k <KID> s <SID> <SID> irs                                   (intersection right state)
k <KID> s <SID> <SID> ils                                   (intersection left state)
k <KID> s <SID> <SID> dis                                   (distributivity state)
k <KID> s <SID> <SID> sus <KID> <KID>                       (subset union state)
k <KID> s <AID> <AID> sua <KID> <KID>                       (subset union action)
k <KID> s <SID> <SID> sis <KID> <KID>                       (subset intersection state)
k <KID> s <SID> <SID> sts <KID> <KID>                       (subset transitivity state)
k <KID> s <AID> <AID> sta <KID> <KID>                       (subset transitivity action)
k <KID> s <SID> <SID> at <KID> <KID>                        (action transitivity)
k <KID> s <SID> <SID> au <KID> <KID>                        (action union)
k <KID> s <SID> <SID> pt <KID> <KID>                        (progression transitivity)
k <KID> s <SID> <SID> pu <KID> <KID>                        (progression union)
k <KID> s <SID> <SID> pr <KID>                              (progression regression)
k <KID> s <SID> <SID> rp <KID>                              (regression progression)
k <KID> s <SID> <SID> b1                                    (basic statement 1)
k <KID> s <SID> <SID> b2                                    (basic statement 2)
k <KID> s <SID> <SID> b3                                    (basic statement 3)
k <KID> s <SID> <SID> b4                                    (basic statement 4)
k <KID> s <AID> <AID> b5                                    (basic statement 5)
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For