Skip to Content.
Sympa Menu

k-user - Re: [K-user] a question about strictness annotation

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] a question about strictness annotation


Chronological Thread 
  • From: Andrei Arusoaie <andrei.arusoaie AT gmail.com>
  • To: Ömer Sinan Ağacan <omeragacan AT gmail.com>
  • Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
  • Subject: Re: [K-user] a question about strictness annotation
  • Date: Mon, 16 Sep 2013 17:07:30 +0300
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
  • List-id: <k-user.cs.uiuc.edu>

Hi Omer,

You have a typo.. use KResult instead of KReuslt.

Andrei A.



2013/9/16 Ömer Sinan Ağacan <omeragacan AT gmail.com>
Hi Andrei, thanks for your response.

What I don't understand is;

    > rule somePredicate(V1:Val, V2:Val) => something else

To me this rule should give an error at compilation, because in the
syntax definition arguments of somePredicate is specified as Exp, but
here arguments is not Exp but Val.

I also tried that and it worked like I expected:


    ➜  test git:(master) ✗ cat test.k
    module TEST

      syntax Exp ::= "nilExp" | return(Exp) [strict]

      syntax Val ::= "nil"

      syntax KReuslt ::=  Val

      rule <k> nilExp => nil ... </k>

    endmodule
    ➜  test git:(master) ✗ cat test
    return(nilExp)
    ➜  test git:(master) ✗ krun test
    <k>
        nil ~> return ( HOLE )
    </k>
    ➜  test git:(master) ✗


Cooling rule can't apply here because return's parameter type is Exp,
not Val or some super-sort(if such a thing exists) of Val.

Am I missing something?

---
Ömer Sinan Ağacan
http://osa1.net




Archive powered by MHonArc 2.6.16.

Top of Page