Stream: general

Topic: CPDT Parser in Lean

Kevin Buzzard (Jun 09 2018 at 14:46):

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 (Jun 09 2018 at 14:46):

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.


page 21

Kevin Buzzard (Jun 09 2018 at 14:51):

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 (Jun 09 2018 at 14:51):

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

Simon Hudon (Jun 09 2018 at 14:52):

Do you also have the definition of stack?

Kevin Buzzard (Jun 09 2018 at 14:59):

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 (Jun 09 2018 at 14:59):

So I can just do it in term mode

Kevin Buzzard (Jun 09 2018 at 15:00):

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

Kevin Buzzard (Jun 09 2018 at 15:00):

definition stack := list ℕ

Kevin Buzzard (Jun 09 2018 at 15:02):

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 (Jun 09 2018 at 15:03):

You can also write it:

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


Simon Hudon (Jun 09 2018 at 15:03):

Which I find prettier than Coq

Simon Hudon (Jun 09 2018 at 15:07):

Sorry, I should write:

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


Oh thanks!

Kevin Buzzard (Jun 09 2018 at 15:07):

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

Simon Hudon (Jun 09 2018 at 15:07):

is >>= the smiley? :)

Kevin Buzzard (Jun 09 2018 at 15:09):

I guess he looks pretty sad :-/

Simon Hudon (Jun 09 2018 at 15:10):

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

Kevin Buzzard (Jun 09 2018 at 15:12):

OK here's my effort:

Kevin Buzzard (Jun 09 2018 at 15:12):

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 (Jun 09 2018 at 15:13):

So you are doing the match with this crazy smiley?

Kevin Buzzard (Jun 09 2018 at 15:14):

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 (Jun 09 2018 at 15:15):

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 (Jun 09 2018 at 15:15):

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

Kevin Buzzard (Jun 09 2018 at 15:15):

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

Kevin Buzzard (Jun 09 2018 at 15:16):

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

Simon Hudon (Jun 09 2018 at 15:16):

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 :)

Exactly!

Simon Hudon (Jun 09 2018 at 15:18):

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 (Jun 09 2018 at 15:30):

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 (Jun 09 2018 at 15:34):

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.

Here's one:

Kevin Buzzard (Jun 09 2018 at 15:35):

inductive binop
| Plus : binop
| Times : binop

open binop

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


Kevin Buzzard (Jun 09 2018 at 15:35):

I just wanted to write

Kevin Buzzard (Jun 09 2018 at 15:35):

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


Kevin Buzzard (Jun 09 2018 at 15:35):

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

Simon Hudon (Jun 09 2018 at 15:37):

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

Last updated: May 14 2021 at 04:22 UTC