Stream: Coq users

Topic: Typed CPDT stackmachine example


view this post on Zulip Julin S (Dec 31 2021 at 17:24):

I was trying an example from the CPDT book in here (under the 'Typed expressions' section) and made.

Require Import List.
Import ListNotations.
Inductive type : Set := Nat | Bool.

Definition typeDenote (t : type) : Set :=
  match t with
  | Nat => nat
  | Bool => bool
  end.

Definition tstack : Set := list type.

Fixpoint vstack (ts : tstack) : Set :=
  match ts with
  | []%list => unit
  | (x::xs)%list => (typeDenote x * vstack xs)%type
  end.

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TMult : tbinop Nat Nat Nat
| TEq : forall (t : type), tbinop t t Bool
| TLt : tbinop Nat Nat Bool.

Inductive tinstr : tstack -> tstack -> Set :=
| TiNConst : forall (s : tstack), nat -> tinstr s (Nat::s)%list
| TiBConst : forall (s : tstack), bool -> tinstr s (Bool::s)%list
| TiBinop : forall (t1 t2 t : type) (s : tstack),
    tbinop t1 t2 t -> tinstr (t2 :: t1 :: s)%list (t :: s)%list.

Inductive tprog : tstack -> tstack -> Set :=
  | TNil : forall (s : tstack), tprog s s
  | TCons : forall (s1 s2 s3 : tstack),
      tinstr s1 s2 -> tprog s2 s3 -> tprog s1 s3.

Definition eqb (a b : bool) : bool := negb (xorb a b).
Definition tbinopDenote {t1 t2 t : type} (op : tbinop t1 t2 t)
    : (typeDenote t1) -> (typeDenote t2) -> (typeDenote t) :=
  match op with
  | TPlus => plus
  | TMult => mult
  | TEq Nat => Nat.eqb
  | TEq Bool => eqb
  | TLt => Nat.ltb
  end.

Fixpoint tinstrDenote {ts1 ts2 : tstack} (i : tinstr ts1 ts2) :
    vstack ts1 -> vstack ts2 :=
  match i with
  | TiNConst _ n => fun s => (n, s)
  | TiBConst _ b => fun s => (b, s)
  | TiBinop _ _ _ _ op => fun s =>
      let '(arg1, (arg2, s')) := s in
        ((tbinopDenote op) arg1 arg2, s')
  end.

But at tinstrDenote, I got an error that I couldn't figure out:

In environment
tinstrDenote : forall ts1 ts2 : tstack,
               tinstr ts1 ts2 -> vstack ts1 -> vstack ts2
ts1 : tstack
ts2 : tstack
i : tinstr ts1 ts2
t : tstack
n : nat
s : vstack ?t@{t1:=t}
The term "(n, s)" has type "(nat * vstack ?t@{t1:=t})%type"
while it is expected to have type "vstack ?t0@{t2:=Nat :: t}".

The books mentions that an error like this can appear if tinstrDenote was defined like

Fixpoint tinstrDenote {ts1 ts2 : tstack} (i : tinstr ts1 ts2) (vs : vstack ts1) : vstack ts2 :=

But such an error is still showing up.

How can this be fixed?

view this post on Zulip Gaëtan Gilbert (Dec 31 2021 at 17:53):

you need to switch the arg1/arg2 order in (tbinopDenote op) arg1 arg2
not sure if coq could produce a better error here

view this post on Zulip Tomás Díaz (Dec 31 2021 at 20:08):

just in case, in your definition of tinstr the TiBinop constructor has its args swapped:
[...] tinstr (t2 :: t1 :: s) (t :: s) instead of tinstr (t1 :: t2 :: s) (t :: s). If you use the latter, then everything should be ok after (I also swapped the args and was having the same issues as you lol)

view this post on Zulip Gaëtan Gilbert (Dec 31 2021 at 21:26):

also if you make the return clause explicit you get a sane error

Definition tinstrDenote ts1 ts2 (i : tinstr ts1 ts2) : vstack ts1 -> vstack ts2 :=
  match i in tinstr ts1 ts2 return vstack ts1 -> vstack ts2 with
  | TiNConst _ n => fun s => (n, s)
  | TiBConst _ b => fun s => (b, s)
  | TiBinop _ op => fun s =>
                     let '(arg1, (arg2, s')) := s in
                     ((tbinopDenote op) arg1 arg2, s')
  end.
(* The term "arg1" has type "typeDenote t0" while it is expected to have type "typeDenote t". *)

view this post on Zulip Julin S (Jan 01 2022 at 17:31):

Thanks. :smile:


Last updated: Jan 29 2023 at 06:02 UTC