Parsers

A theory assigns its own parses to the sentences of a dataset in two ways. By a rule, it parses a sentence from its parse in a fragment that the theories share, so that it parses alike every sentence of the same shared parse, including sentences no dataset holds yet. By a table, it stipulates the parse of a single sentence. A parser has both, and the table overrides the rule on the sentences it lists (Eval.Parser). A verdict that rests on a listed sentence rests on a stipulation, so the listed sentences are what a parser costs beyond its rule (Parser.stipulations). A rule that reproduces every stipulated parse replaces the table without changing a parse (Parser.parse_ofRule_eq).

structure Eval.Parser (S : Type u_1) (F : Type u_2) (P : Type u_3) : Type (max (max u_1 u_2) u_3)

How a theory parses the sentences S of a dataset into its parses P: by a rule on the parse of a sentence in a shared fragment F, defined on the shared parses the theory covers, and by a table of parses stipulated for single sentences, which overrides the rule.

• rule : F → Option P

  The theory's parse of the sentences of each shared parse it covers.

• table : Finmap fun (x : S) => P

  The parses stipulated for single sentences.

def Eval.Parser.stipulations {S : Type u_1} {F : Type u_2} {P : Type u_3} (π : Parser S F P) : Finset S

The sentences whose parses are stipulated.

Equations

• π.stipulations = π.table.keys

def Eval.Parser.ofRule {S : Type u_1} {F : Type u_2} {P : Type u_3} (r : F → Option P) : Parser S F P

The parser of a rule alone.

Equations

• Eval.Parser.ofRule r = { rule := r, table := ∅ }

@[simp]

theorem Eval.Parser.stipulations_ofRule {S : Type u_1} {F : Type u_2} {P : Type u_3} (r : F → Option P) : (ofRule r).stipulations = ∅

def Eval.Parser.parse {S : Type u_1} {F : Type u_2} {P : Type u_3} (π : Parser S F P) [DecidableEq S] (shared : S → F) (s : S) : Option P

The parse of a sentence, given its shared parse: the stipulated one if the table lists the sentence, and the rule's otherwise.

Equations

• π.parse shared s = (Finmap.lookup s π.table).or (π.rule (shared s))

@[simp]

theorem Eval.Parser.parse_ofRule {S : Type u_1} {F : Type u_2} {P : Type u_3} [DecidableEq S] (shared : S → F) (r : F → Option P) (s : S) : (ofRule r).parse shared s = r (shared s)

theorem Eval.Parser.parse_of_notMem {S : Type u_1} {F : Type u_2} {P : Type u_3} (π : Parser S F P) [DecidableEq S] (shared : S → F) {s : S} (hs : s ∉ π.stipulations) : π.parse shared s = π.rule (shared s)

theorem Eval.Parser.parse_ofRule_eq {S : Type u_1} {F : Type u_2} {P : Type u_3} (π : Parser S F P) [DecidableEq S] (shared : S → F) {r : F → Option P} (hstip : ∀ (s : S) (p : P), Finmap.lookup s π.table = some p → r (shared s) = some p) (hrule : ∀ s ∉ π.stipulations, r (shared s) = π.rule (shared s)) : (ofRule r).parse shared = π.parse shared

A rule that reproduces every stipulated parse, and agrees with the parser's rule on the other sentences, parses every sentence as the parser does.