dafny packrat prototype

lazy-grammar.dfy

// This is my attempt to add laziness to the above grammar by wrapping the fields of Derivs with Thunks

include "thunk.dfy"

datatype Result <T> = Parsed(result: T, dvs: Derivs) | NoParse

datatype Derivs = Derivs(
    dvAdditive: Thunk<Result<int>>,
    dvMultitive: Thunk<Result<int>>,
    dvPrimary: Thunk<Result<int>>,
    dvDecimal: Thunk<Result<int>>,
    dvChar: Thunk<Result<char>>)

method pAdditive(d: Derivs) returns (val : Result<int>)
modifies d.dvMultitive
{
    // Additive <- Multitive
    var dvMult := d.dvMultitive.get();
    match dvMult {
        case NoParse => val := NoParse;
        case Parsed(vLeft, d') =>
            ghost var dvCharNotNull := d'.dvChar; // Without this, I get an error that d'.dvChar may be null
            var dvChar := d'.dvChar.get(); // Does not work, violates the modifies clause
            match dvChar
            {
                case NoParse => val := dvMult;

                // Additive <- Multitive '+' Additive
                case Parsed(nextChar, d'') => if nextChar != '+' { val := dvMult; } else {
                    ghost var dvAdditiveNotNull := d''.dvAdditive;
                    var dvAdditive := d''.dvAdditive.get(); // Does not work, violates the modifies clause
                    match dvAdditive {
                        case NoParse => val := dvMult;
                        case Parsed(vRight, d''') =>
                            val := Parsed(vLeft * vRight, d''');
                    }
                }
            }
    }
}

method pMultitive(d: Derivs) returns (result : Result<int>)
modifies d.dvPrimary
{
    // Multitive <- Primary
    var dvPrim := d.dvPrimary.get();
    match dvPrim {
        case NoParse => result := NoParse;
        case Parsed(vLeft, d') =>

            // Multitive <- Primary '*' Multitive
            var dvChar := d'.dvChar.get(); // Does not work; violates the modifies clause
            match dvChar {
                case NoParse => result := dvPrim;
                case Parsed(nextChar, d'') =>
                    if nextChar != '*' { result := dvPrim; } else
                    {
                        var dvMult := d''.dvMultitive.get(); // Does not work; violates the modifies clause
                        match dvMult {
                            case NoParse => { result := dvPrim; }
                            case Parsed(vRight, d''') => { result := Parsed(vLeft * vRight, d'''); }
                        }
                }
          }
    }
}

method pPrimary(d: Derivs) returns (result : Result<int>)
modifies d.dvChar
modifies d.dvDecimal
{
    // Primary <- '(' Additive ')'
    // Primary <- Decimal
    var dvChar := d.dvChar.get();
    var dvDec := d.dvDecimal.get();
    match dvChar {
        case NoParse => { result := dvDec; }
        case Parsed(chr, d') => if chr != '(' { result := dvDec; } else {
            var dvAdd := d'.dvAdditive.get(); // Does not work, violates the modifies clause
            match dvAdd {
                case NoParse => { result := dvDec; }
                case Parsed(val, d'') => 
                    var dvChar' := d''.dvChar.get(); // Does not work, violates the modifies clause
                
                    match dvChar' {
                        case NoParse => { result := dvDec; }
                        case Parsed(chr, d''') => if chr == '}' { result := Parsed(val, d'''); } else { result := dvDec; }
                    }
            }
        }
    }
}

method pDecimal(d: Derivs) returns (result: Result<int>)
modifies d.dvChar
{
    // Decimal = 0 / 1 / 2 / 3 / 4 / 5 / 6 / 7 / 8 / 9
    var dvChar := d.dvChar.get();
    match dvChar {
        case NoParse => { result := NoParse; }
        case Parsed(chr, d') =>
            if chr == '0' { result := Parsed(0, d'); }
            else if chr == '1' { result := Parsed(1, d'); }
            else if chr == '2' { result := Parsed(2, d'); }
            else if chr == '3' { result := Parsed(3, d'); }
            else if chr == '4' { result := Parsed(4, d'); }
            else if chr == '5' { result := Parsed(5, d'); }
            else if chr == '6' { result := Parsed(6, d'); }
            else if chr == '7' { result := Parsed(7, d'); }
            else if chr == '8' { result := Parsed(8, d'); }
            else if chr == '9' { result := Parsed(9, d'); }
            else { result := NoParse; }
    }
}

/*
// This is the top-level method which ties all of the others together by embedding self-
// reference in the Derivs type. This method is one of the cruxes of the problem that
// I've struggled to get to work.

method parse(str : string) returns (d : Derivs) {
  d := Derivs(
      pAdditive(d),
      pMultitive(d),
      pPrimary(d),
      pDecimal(d),
      if |s| == 0 then NoParse else Parsed(s[0], parse(s[0..]))
  );
}
*/

strict-grammar.dfy

// This implements the grammar as though laziness were available. The top-level "parse" function
// is not implemented because it relies on laziness and self-reference which I don't know how to acheive.

// This code is a translation of Haskell code from Bryan Ford's thesis,
// "Packrat Parsing: a Practical Linear-Time Algorithm with Backtracking".

datatype Result <T> = Parsed(result: T, dvs: Derivs) | NoParse

datatype Derivs = Derivs(
    dvAdditive: Result<int>,
    dvMultitive: Result<int>,
    dvPrimary: Result<int>,
    dvDecimal: Result<int>,
    dvChar: Result<char>)

function method pAdditive(d: Derivs) : Result<int>
{
    // Additive <- Multitive
    var dvMult := d.dvMultitive;
    match dvMult {
        case NoParse => NoParse
        case Parsed(vLeft, d') => match d'.dvChar {
            case NoParse => dvMult

            // Additive <- Multitive '+' Additive
            case Parsed(nextChar, d'') => if nextChar != '+' then dvMult else
                match d''.dvAdditive {
                    case NoParse => dvMult
                    case Parsed(vRight, d''') => Parsed(vLeft * vRight, d''')
                }
        }
    }
}

function method pMultitive(d: Derivs) : Result<int>
{
    // Multitive <- Primary
    var dvPrim := d.dvPrimary;
    match dvPrim {
        case NoParse => NoParse
        case Parsed(vLeft, d') =>

          // Multitive <- Primary '*' Multitive
          match d'.dvChar {
              case NoParse => dvPrim
              case Parsed(nextChar, d'') =>
                if nextChar != '*' then dvPrim else match d''.dvMultitive {
                    case NoParse => dvPrim
                    case Parsed(vRight, d''') => Parsed(vLeft * vRight, d''')
                }
          }
    }
}

function method pPrimary(d: Derivs) : Result<int>
{
    // Primary <- '(' Additive ')'
    // Primary <- Decimal
    match d.dvChar {
        case NoParse => d.dvDecimal
        case Parsed(chr, d') => if chr != '(' then d.dvDecimal else match d'.dvAdditive {
            case NoParse => d.dvDecimal
            case Parsed(val, d'') => match d''.dvChar {
                case NoParse => d.dvDecimal
                case Parsed(chr, d''') =>
                    if chr == '}' then Parsed(val, d''') else d.dvDecimal
            }
        }
    }
}

function method pDecimal(d: Derivs) : Result<int>
{
    // Decimal = 0 / 1 / 2 / 3 / 4 / 5 / 6 / 7 / 8 / 9
    match d.dvChar {
        case NoParse => NoParse
        case Parsed(chr, d') =>
            if chr == '0' then Parsed(0, d')
            else if chr == '1' then Parsed(1, d')
            else if chr == '2' then Parsed(2, d')
            else if chr == '3' then Parsed(3, d')
            else if chr == '4' then Parsed(4, d')
            else if chr == '5' then Parsed(5, d')
            else if chr == '6' then Parsed(6, d')
            else if chr == '7' then Parsed(7, d')
            else if chr == '8' then Parsed(8, d')
            else if chr == '9' then Parsed(9, d')
            else NoParse
    }
}

Thunk.dfy

datatype Option<T> = Some(t: T) | None

class Thunk <T> {
    var fn : () -> T, cache : Option<T>;

    constructor (fn: () -> T)
    {
        this.fn := fn;
        this.cache := None;
    }

    // I was unable to prove t == this.fn() without using assume, because I think a proof
    // would relie on induction over invocations of get(), and I can't use get() in clauses
    // which expect functions
    method get() returns (t: T) 
        modifies this
        ensures t == this.fn()
        {
        match this.cache {
            case Some(x) => 
                assume x == this.fn();
                t := x;
            case None =>
                var res := this.fn();
                t := res;
                this.cache := Some(res);
        }
    }
}