From a48a4ac34125f95fd0056bf7201fc1514676ed40 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 13 Dec 2023 12:37:05 -0600 Subject: [PATCH] Advent of code --- src/Parsers/examples/AdventOfCode1.dfy | 36 ++++++++ src/Parsers/examples/ParserGenerator.dfy | 105 ++++++++++++++++++++++- 2 files changed, 137 insertions(+), 4 deletions(-) create mode 100644 src/Parsers/examples/AdventOfCode1.dfy diff --git a/src/Parsers/examples/AdventOfCode1.dfy b/src/Parsers/examples/AdventOfCode1.dfy new file mode 100644 index 00000000..6ba6c3ed --- /dev/null +++ b/src/Parsers/examples/AdventOfCode1.dfy @@ -0,0 +1,36 @@ +// RUN: %test "%s" + +include "../stringParsersBuilders.dfy" + +// A small regex-like language that can be turned into a straightforward parser +// So first we parse the parser to ParserSpec, we convert it to a parser +// and we parse the string using this parser. +// TODO: Compile this parser and prove it does the same. +module AdventOfCode1 { + import opened StringParsersBuilders + + const nonDigit := + Except("0123456789\r\n").ZeroOrMore() + + const digit := + B(P.DigitNumber()) + + const parseLine := + nonDigit.e_I(digit).Bind((first: nat) => + nonDigit.e_I(digit).??().Rep((first, first), + (pair: (nat, nat), newDigit: nat) => (pair.0, newDigit) + )).I_e(nonDigit) + + const parseInput := + parseLine.I_e(S("\r").?().e_I(S("\n").?())) + .Rep(0, (acc: int, newElem: (nat, nat)) => + acc + newElem.0 * 10 + newElem.1) + + method {:test} TestParser() { + var input := @"1abc2 +pqr3stu8vwx +a1b2c3d4e5f +treb7uchet"; + ParseTest(parseInput, input); + } +} \ No newline at end of file diff --git a/src/Parsers/examples/ParserGenerator.dfy b/src/Parsers/examples/ParserGenerator.dfy index ad47c84c..7c1c5411 100644 --- a/src/Parsers/examples/ParserGenerator.dfy +++ b/src/Parsers/examples/ParserGenerator.dfy @@ -3,9 +3,9 @@ include "../stringParsersBuilders.dfy" // A small regex-like language that can be turned into a straightforward parser -// a compiler from this language to an imperative language -// and a parser that can act -// and a parser that can act as a specification +// So first we parse the parser to ParserSpec, we convert it to a parser +// and we parse the string using this parser. +// TODO: Compile this parser and prove it does the same. module ParserGenerator { import opened StringParsersBuilders @@ -21,12 +21,19 @@ module ParserGenerator { | Or(left: ParserSpec, right: ParserSpec) | Repeat(p: ParserSpec) { + predicate OnlyAndRepeat() { + match this + case Const(s) => true + case And(left, right) => left.OnlyAndRepeat() && right.OnlyAndRepeat() + case Or(left, right) => false + case Repeat(p) => p.OnlyAndRepeat() + } function ToParser(): B { match this case Const(s) => S(s).M(ToBool()) case And(left, right) => left.ToParser().e_I(right.ToParser()).M(ToBool()) case Or(left, right) => O([left.ToParser().??(), right.ToParser()]).M(ToBool()) - case Repeat(x) => x.ToParser().ZeroOrMore().M(ToBool()) + case Repeat(x) => x.ToParser().??().ZeroOrMore().M(ToBool()) } function ToString(): string { match this @@ -66,4 +73,94 @@ module ParserGenerator { program := "abcdeml"; print underlying.apply(program); // Should print true } + + // TODO: Some kind of compilation? +/* + datatype ParserStmt = + Expect(c: char) + | Stmts(first: ParserStmt, next: PArserStmt) + | Repeat(underlying: ParserStmt) + | Break() + { + function ToProgram(indent: string := ""): string { + match this { + case Expect(c) => "if input[i] == '" + [c] + "' { }" + } + } + // (ok, cancelling) + function Run(input: string, index: nat): (bool, nat) { + if |input| <= index then (false, index) else + match this { + case Expect(c) => (input[index] == c, index + 1) + case Stmts(first) => + if s == [] then (true, index) + else + var (r, newIndex) := !s[0].Run(input, index); + if r then Stmts(s[1..]).Run(input, newIndex) + else (false, index) // We completely forget about the failure + case Break() => + case Repeat(stmts) => + stmts + } + } + + method RunImperative(input: string) returns (b: bool) + ensures b == Run(input, 0) + { + var i := + } + } + //datatype +*/ + // A ParserSpec can be compiled to this non-deterministic Automata + // We will prove that the two parsing strategies are equivalent + /*datatype Automata = Automata( + nStates: nat, + startState: nat, + transitions: set<(nat, char, nat)>, + finalState: set + ) + { + static function FromParserSpec(spec: ParserSpec): Automata { + match spec { + case Const("") => + Automata(1, 0, {}, {0}) + case Const(s) => + var a := FromParserSpec(Const(s[1..])); + var newStart := a.nStates; + Automata(a.nStates + 1, newStart, a.transitions + {(newStart, s[0], a.startState)}, a.finalState) + case Or(left, right) => + var l := FromParserSpec(left); + var r := FromParserSpec(right); + var offsetRight := (n: nat) => n + l.nStates; + var newStart := l.nStates + r.nStates + 1; + var rightTransitions := set rt <- r.transitions :: (offsetRight(rt.0), rt.1, offsetRight(rt.2)); + Automata(l.nStates + r.nStates + 1, + newStart, + l.transitions + rightTransitions + + + set firstLeftTransition <- l.transitions | + firstLeftTransition.0 == l.start + ) + case _ => Automata(0, 0, {}, {}) + } + } + + function Run(input: string, states: set, index: nat): set { + if index >= |input| then {} + else set newState: nat, s: nat | + 0 <= newState < nStates && 0 <= s < nStates && + (s, input[index], newState) in transitions + :: newState + } + predicate Accepts(input: string) { + Run(input, {startState}, 0) * finalState != {} + } + + lemma Equivalence(spec: ParserSpec, input: string) + ensures spec.ToParser().apply(input).Success? + <==> FromParserSpec(spec).Accepts(input) + { + + } + }*/ } \ No newline at end of file