Zulip Chat Archive

Stream: new members

Topic: Silly Imp problem


view this post on Zulip Kevin Sullivan (Aug 08 2020 at 19:05):

We've implemented a minimal imperative language following Pierce's Imp chapter. On line 28, the definition of cEval, we're getting this error: infer type failed, unknown variable _f_1. We're not familiar enough with Lean's implementation to know why we're seeing this. There is no variable _f_1 in our program.

inductive bvar : Type
| mk (n : )

def bvar_eq : bvar  bvar  bool
| (bvar.mk n1) (bvar.mk n2) := n1=n2

inductive bExpr : Type
| BLit (b: bool)
| BVar (v: bvar)

def benv := bvar  bool

def bEval : bExpr  benv  bool
| (bExpr.BLit b) i := b
| (bExpr.BVar v) i := i v

def init_benv : benv := λ v, ff

def update_benv : benv  bvar  bool  benv
| i v b := λ v2, if (bvar_eq v v2) then b else (i v2)

inductive bCmd : Type
| bAssm (v : bvar) (e : bExpr)
| bSeq (c1 c2 : bCmd)

def cEval : benv  bCmd  benv
| i0 c :=   match c with
            | (bCmd.bAssm v e) := update_benv i0 v (bEval e i0)
            | (bCmd.bSeq c1 c2) :=
                let i1 := (cEval i0 c1) in (cEval i1 c2)
            end

def myFirstProg := bCmd.bAssm (bvar.mk 0) (bExpr.BLit ff)

def newEnv := cEval init_benv myFirstProg

#eval newEnv (bvar.mk 0)

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:17):

The way you have written cEval makes me think you learned this from coq style. In lean you just write a definition with multiple cases

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:18):

def cEval : benv  bCmd  benv
| i0 (bCmd.bAssm v e) := update_benv i0 v (bEval e i0)
| i0 (bCmd.bSeq c1 c2) := cEval (cEval i0 c1) c2

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:19):

@Kevin Sullivan

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:26):

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

view this post on Zulip Kevin Sullivan (Aug 09 2020 at 20:07):

Mario Carneiro said:

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

Thanks, yeah. It is Coq-style but it seemed like a wrong response nonetheless, which is what prompted me to ask. Not sure if I should file an issue?

view this post on Zulip Kevin Sullivan (Aug 10 2020 at 16:18):

Kevin Sullivan said:

Mario Carneiro said:

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

Thanks, yeah. It is Coq-style but it seemed like a wrong response nonetheless, which is what prompted me to ask. Not sure if I should file an issue?

Lean Prover repo has been archived. Doesn't seem I can post an issue. I'm probably missing something, but maybe not. Let me know. Thanks.

view this post on Zulip Yakov Pechersky (Aug 10 2020 at 16:26):

The community version of Lean is at https://github.com/leanprover-community/lean

view this post on Zulip Kevin Sullivan (Aug 10 2020 at 17:25):

Yakov Pechersky said:

The community version of Lean is at https://github.com/leanprover-community/lean

Ah, yes, thanks.


Last updated: May 09 2021 at 19:11 UTC