CPDT Parser in Lean

Stream: general

[Kevin Buzzard]

My son got interested in parsers and I'm trying to understand them better by implementing the simple parser at the beginning of Certified Programming with Dependent Types. But actually I find making these inductive types quite hard -- in my area of expertise we don't really ever use complicated inductive structures like the ones showing up in these parsers. Here's an example of one I'm struggling with: in Coq it's

[Kevin Buzzard]

Fixpoint progDenote (p : prog) (s : stack) : option stack :=
match p with
| nil ⇒ Some s
| i :: p’ ⇒
match instrDenote i s with
| None ⇒ None
| Some s’ ⇒ progDenote p’ s’
end
end.

[Kevin Buzzard]

http://adam.chlipala.net/cpdt/cpdt.pdf

[Kevin Buzzard]

page 21

[Kevin Buzzard]

I tried writing it by hand with list.rec_on (prog := list instr) but I seemed to end up knowing progDenote p' s rather than progDenote p' s'. Presumably this is the sort of thing the equation compiler can do for me somehow? Or is there some complicated issue which makes this definition problematic? I know very little about this sort of stuff beyond rec.

[Kevin Buzzard]

Oh I see now, I should somehow carry s around as a parameter

[Simon Hudon]

Do you also have the definition of stack?

[Kevin Buzzard]

definition progDenote (p : prog) : stack → option stack :=
list.rec_on p some $
  λ i p' pDp' s,option.rec_on (instrDenote i s) none pDp'

[Kevin Buzzard]

So I can just do it in term mode

[Kevin Buzzard]

I am slightly unnerved by how incomprehensible mine looks compared to Chlipata's

[Kevin Buzzard]

definition stack := list ℕ

[Kevin Buzzard]

you can plough through http://adam.chlipala.net/cpdt/html/Cpdt.StackMachine.html to find these. I see my error now -- I should have been inducting on p before introducing s. These are subtleties I don't usually run into in my area of mathematics, you rarely induct on something other than nat

[Simon Hudon]

You can also write it:

definition progDenote (p : prog) : stack → option stack
 | [] := ...
 | (s :: ss) := ...

[Simon Hudon]

Which I find prettier than Coq

[Simon Hudon]

Sorry, I should write:

definition progDenote : prog  → stack → option stack
 | [] s := some s
 | (p :: ps) s := instrDenote p s >>= progDenote ps

[Kevin Buzzard]

Oh thanks!

[Kevin Buzzard]

I was just working on this myself but I'm not sure I would have hit upon that crazy smiley thing

[Simon Hudon]

is >>= the smiley? :)

[Kevin Buzzard]

I guess he looks pretty sad :-/

[Simon Hudon]

Or angry? I see >> as eyebrows and = as a nose

[Kevin Buzzard]

OK here's my effort:

[Kevin Buzzard]

definition progDenote' : prog → stack → option stack
| ([]) := some
| (i :: p') := λ s, match (instrDenote i s) with
  | none := none
  | some s' := progDenote' p' s'
  end

[Kevin Buzzard]

So you are doing the match with this crazy smiley?

[Kevin Buzzard]

I can see that your progDenote ps is my progDenote p' and then other than that I am sending none to none and s' to s'. You're exploiting this in some way?

[Kevin Buzzard]

PS @Simon Hudon I felt quite bad a week or so ago when I was trying to write some notation and didn't understand binding powers and was in a rush and you tried to explain them and I just said just gimme the number!

[Simon Hudon]

Yes, with option, >>= returns none if either of its parameters does

[Kevin Buzzard]

It was partially because of that incident that I thought it was time to learn about parsers!

[Kevin Buzzard]

Aah I see you're explictly utilising the fact that it's a monad?

[Simon Hudon]

No worries, I got that you were in a rush. And I know I'd always prefer to get deeper into it. But thanks for coming back to it :)

[Simon Hudon]

Exactly!

[Simon Hudon]

In Coq, he'd have to do some work to bring that in but it's just there for us in Lean so it's good to get used to it

[Simon Hudon]

The operators are a bit broken but in Haskell, I'd rather write progDenote ps =<< instrDenote p s. It's a bit like function application with monads (you apply progDenote ps to the result of instrDenote p s)

[Kevin Buzzard]

I have my compiler working now and I'd like to do some unit tests using #eval. This means as far as I can see that I have to go and define a bunch of has_repr instances.

[Kevin Buzzard]

Here's one:

[Kevin Buzzard]

inductive binop
| Plus : binop
| Times : binop

open binop

instance : has_repr binop := ⟨λ b, match b with
    | Plus := "add"
    | Times := "mul"
    end
⟩

[Kevin Buzzard]

I just wanted to write

[Kevin Buzzard]

instance : has_repr binop := ⟨
    | Plus := "add"
    | Times := "mul"
    end
⟩

[Kevin Buzzard]

but that didn't work so I had to put all the match waffle in. Am I missing something?

[Simon Hudon]

No I think that's the way to do it. I was looking to see if it could be generated for you but I haven't found tactics for that