Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

debugging typeclass resolution in semantics #9

Closed
andres-erbsen opened this issue Jun 15, 2018 · 4 comments
Closed

debugging typeclass resolution in semantics #9

andres-erbsen opened this issue Jun 15, 2018 · 4 comments

Comments

@andres-erbsen
Copy link
Contributor

As a part of an experiment I tried modeling continuations with explicit stacks. In ExprImp.v after defining stmt, the following code

  Inductive cont: Set :=
    | CLoad(x: var)(addr: expr): cont
    | CStore(addr val: expr): cont
    | CSet(x: var)(e: expr): cont
    | CIf(cond: expr)(bThen bElse: cont): cont
    | CWhile(cond: expr)(body: cont): cont
    | CSeq(s1 s2: cont): cont
    | CSkip: cont
    | CCall(binds: list var)(f: func)(args: list expr)
    | CStack(st: state)(c: cont)(binds rets: list var).

  Section WithEnv.
    Context {env} {funcMap: Map env func (list var * list var * stmt)} (e:env).
    Fixpoint eval_cont(f: nat)(st: state)(m: mem)(s: cont): option (state * mem) :=
      match f with
      | 0 => None (* out of fuel *)
      | S f => match s with
        | CLoad x a =>
            a <- eval_expr st a;
            v <- read_mem a m;
            Return (put st x v, m)
        | CStore a v =>
            a <- eval_expr st a;
            v <- eval_expr st v;
            m <- write_mem a v m;
            Return (st, m)
        | CSet x e =>
            v <- eval_expr st e;
            Return (put st x v, m)
        | CIf cond bThen bElse =>
            v <- eval_expr st cond;
            eval_cont f st m (if weq v $0 then bElse else bThen)
        | CWhile cond body =>
            v <- eval_expr st cond;
            if weq v $0 then Return (st, m) else
              p <- eval_cont f st m body;
              let '(st, m) := p in
              eval_cont f st m (CWhile cond body)
        | CSeq s1 s2 =>
            p <- eval_cont f st m s1;
            let '(st, m) := p in
            eval_cont f st m s2
        | CSkip => Return (st, m)
        | CCall binds fname args =>
          fimpl <- get e fname;
          let '(params, rets, fbody) := fimpl in
          argvs <- option_all (map (eval_expr st) args);
          st0 <- putmany params argvs empty;
          st1m' <- eval_cont f st0 m fbody;
          let '(st1, m') := st1m' in
          retvs <- option_all (map (get st1) rets);
          st' <- putmany binds retvs st;
          Return (st', m')
        | CStack stf cf binds rets =>
          stf'm' <- eval_cont f stf m cf;
          let '(stf', m') := stf'm' in
          retvs <- option_all (map (get stf') rets);
          st' <- putmany binds retvs st;
          Some (st', m')
        end
      end.

fails to check with an error

Error: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X170==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args
          |- Map
               ?X167@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args}
               ?X168@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args}
               ?X169@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args}] (parameter Map of
          @get) {?Map}
 ?X185==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets
          |- Monad
               ?X184@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets}] (parameter Monad of
          @Bind) {?Monad}
 ?X193==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs
          |- Monad
               ?X192@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}]
          (parameter Monad of @Bind) {?Monad0}
 ?X199==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs
          |- Map
               ?X196@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}
               ?X197@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}
               ?X198@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}]
          (parameter TMap of @putmany) {?TMap}
 ?X200==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args {fimpl} {p} {fbody} {params} {rets}
          {argvs} |- Type] (parameter K of @putmany) {?K}
 ?X203==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs |- Type]
          (parameter K of @empty) {?K0}
 ?X204==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs |- Type]
          (parameter V of @empty) {?V}
 ?X205==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs
          |- Map
               ?X202@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}
               ?X203@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}
               ?X204@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}]
          (parameter Map of @empty) {?Map0}
 ?X208==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0
          |- Monad
               ?X207@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0}]
          (parameter Monad of @Bind) {?Monad1}
 ?X221==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m'
          |- Monad
               ?X220@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'}] (parameter Monad of @Bind) {?Monad2}
 ?X230==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m'
          |- Map
               ?X227@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'}
               ?X228@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'}
               ?X229@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'}] (parameter Map of @get) {?Map1}
 ?X232==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args {fimpl} {p} {fbody} {params} {rets}
          {argvs} {st0} {st1m'} {st1} {m'} |- Type] (parameter A of map) {?A}
 ?X235==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m' retvs
          |- Monad
               ?X234@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs}]
          (parameter Monad of @Bind) {?Monad3}
 ?X241==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m' retvs
          |- Map
               ?X238@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs}
               ?X239@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs}
               ?X240@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs}] (parameter TMap
          of @putmany) {?TMap0}
 ?X242==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m' {retvs} |- Type] (parameter V of @putmany) {?V0}
 ?X245==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m' retvs st'
          |- Monad
               ?X244@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs; __:=st'}]
          (parameter Monad of @Return) {?Monad4}

even if I replace the new case with _, I get a typelcass resolution error instead of a failed to infer something of type which I normally use to debug mistyped code. There is probably just a typo or something equally stupid in this code, but the typeclass magic puts debugging it beyond my ability -- please help.
@andres-erbsen
Copy link
Contributor Author

Even replacing the new case with None results in an undecipherable typeclass error.

@samuelgruetter
Copy link
Contributor

You have to replace

    Context {env} {funcMap: Map env func (list var * list var * stmt)} (e:env).

with

    Context {env} {funcMap: Map env func (list var * list var * cont)} (e:env).

@samuelgruetter
Copy link
Contributor

This should be a simple "type mismatch" error of the form "expected cont, but found stmt", but due to typeclasses, it becomes quite undecipherable. I've got used to this and I debug it by commenting out all cases and then gradually add more cases until it breaks. I agree that this is unfortunate -- that's the price you pay for not eating bread and lentils every day...

@andres-erbsen
Copy link
Contributor Author

Thanks!

@andres-erbsen andres-erbsen mentioned this issue Jun 22, 2018
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@andres-erbsen @samuelgruetter