K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

It seems like it is not recognizing BQ as a list.

If I replace size(BQ) with size(.List), it rewrites size(.List) to 0.

  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(.List) ... </k>

Daniel

On 5 Jan 2018, at 14:13, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(BQ) ... </k>

the result is simply: size(BQ)

More specifically, the result is:

<k> size ( ListItem ( ListItem ( 42 ) ListItem ( .Map ) ListItem ( .Set ) ) ) </k>

On 5 Jan 2018, at 14:07, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

Seems like size(BQ) is not being evaluated.

If I replace:

  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(BQ) >=Int 1 ... </k>

by:

  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(BQ) ... </k>

the result is simply: size(BQ)

But if I replace it by

  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => 0 >=Int 1 ... </k>

the result is “false” as expected.

Daniel

On 5 Jan 2018, at 11:39, Markus Knecht <markus.knecht85 AT gmail.com> wrote:

It seems that 
size ( ListItem ( ListItem ( 42 ) ListItem ( .Map ) ListItem ( .Set ) ) )
cannot be evaluated and thus >=Int is stuck, the question is why, I do not see it, especially as you have the same _expression_ size(BQ) in the requires where it seems to work.
It may have something to do that Int >=Int Int is already a Bool even in its unevaluated form, but that is unlikely as Int >=Int Int is defined as a function and should match anywhere anyways.
If you use:

rule <k> R:Bool ~> selFindEnBs(BTail, L) => selFindEnBs(BTail, L ListItem(R)) </k>
Instead of the true/false version, does the unevaluated Term end up in the ListItem of selFindEnBs ? atleast the rewriting would continue but will be stuck later, so no solution but maybe it helps pinpoint the problem.

Daniel Schnetzer Fava <danielsf AT ifi.uio.no> schrieb am Fr., 5. Jan. 2018 um 11:13 Uhr:

Hi Markus,

Thanks for the reply.

What error do you get?

Does the evaluation get Stuck at   aBoolean  ~> selFindEnBs(...) , or does IsSelBranchEnabled(BHead) fails to evaluate to a boolean? or did it not kompile at all? 

IsSelBranchEnabled(BHead) fails to evaluate to a boolean.

It does get evaluated to a certain degree, but it stops here, and does not evaluate the >=Int

size ( ListItem ( ListItem ( 42 ) ListItem ( .Map ) ListItem ( .Set ) ) ) >=Int 1

Here is the rule for IsSelBranchEnabled:

  syntax Bool ::= "IsSelBranchEnabled" "(" GChan ")"

  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(BQ) >=Int 1 ... </k>

      <chan>

        <ref> Ref </ref>

        <type> _ </type>

       <forward> FQ </forward>

       <backward> BQ </backward>

     </chan>

      requires (EotInFQ(FQ) ==Bool false) // channel is open  

               andBool

               (size(FQ) +Int size(BQ) >Int 0) // channel is async

   is Bool declared as KResult [do you have syntax KResult ::= Bool somwhere]

Bool is declared as KResult.

Thanks again,

Daniel

PS.

Independent tips:
  I don't think the brackets before => are necessary

  instead of true/false ~> ... you could capture both in one statement with Res:Bool ~> …

Great!  I appreciate the comments.  Often, even though I manage to accomplish what I need/want, I get the feeling that there is a better way of doing it.

On 4 Jan 2018, at 16:55, Markus Knecht <markus.knecht85 AT gmail.com> wrote:

What error do you get?

Does the evaluation get Stuck at   aBoolean  ~> selFindEnBs(...) , or does IsSelBranchEnabled(BHead) fails to evaluate to a boolean? or did it not kompile at all? 

Some things to check: 

   if something follows selFindEnBs you need to add ... before  </k>. 

   is Bool declared as KResult [do you have syntax KResult ::= Bool somwhere]

Independent tips:
  I don't think the brackets before => are necessary
  instead of true/false ~> ... you could capture both in one statement with Res:Bool ~> ...

Daniel Schnetzer Fava <danielsf AT ifi.uio.no> schrieb am Do., 4. Jan. 2018 um 16:25 Uhr:

Hi,

I am trying to write a rule that first evaluates another, then evaluates itself.

I think I ought to be using ~> but I am not sure exactly how.

Here is some attempt that does not seem to work:

rule <k> selFindEnBs({ BHead } BTail, L:List) =>

            IsSelBranchEnabled(BHead) ~> selFindEnBs(BTail, L) </k>

rule <k> (true ~> selFindEnBs(BTail, L)) => 

              selFindEnBs(BTail, L ListItem(true)) </k>

rule <k> (false ~> selFindEnBs(BTail, L)) => 

              selFindEnBs(BTail, L ListItem(false)) </k>

The goal is to have the result of “IsSelBranchEnabled(BHead)” appended to the list L

and then continue evaluating selFindEnBs on BTail.

Any help is highly appreciated!

Thanks,

Daniel