Zulip Chat Archive

Stream: general

Topic: CPDT Parser in Lean


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 14:47):

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

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 14:47):

page 21

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 14:51):

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

view this post on Zulip Simon Hudon (Jun 09 2018 at 14:52):

Do you also have the definition of stack?

view this post on Zulip 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'

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 14:59):

So I can just do it in term mode

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:00):

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

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:00):

definition stack := list ℕ

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jun 09 2018 at 15:03):

You can also write it:

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

view this post on Zulip Simon Hudon (Jun 09 2018 at 15:03):

Which I find prettier than Coq

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:07):

Oh thanks!

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jun 09 2018 at 15:07):

is >>= the smiley? :)

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:09):

I guess he looks pretty sad :-/

view this post on Zulip Simon Hudon (Jun 09 2018 at 15:10):

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

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:12):

OK here's my effort:

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:13):

So you are doing the match with this crazy smiley?

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Simon Hudon (Jun 09 2018 at 15:15):

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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:16):

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

view this post on Zulip 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 :)

view this post on Zulip Simon Hudon (Jun 09 2018 at 15:16):

Exactly!

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:34):

Here's one:

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:35):

inductive binop
| Plus : binop
| Times : binop

open binop

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

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:35):

I just wanted to write

view this post on Zulip Kevin Buzzard (Jun 09 2018 at 15:35):

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

view this post on Zulip 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?

view this post on Zulip 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