| 26 Jul 2021 |
 Mike Stay | What's the current syntax for bags? (Or are they supported?) | 18:29:38 |
| Mike Stay | Can we declare an operator to be associative and commutative? | 18:31:04 |
 nishantjr | Ah, the attribute may be a tag for the now depricated --transition parameter to kompile:
--transition
[DEPRECATED: java backend only] string is a whitespace-separated list
of tags designating rules to become transitions.
Default: [transition] | 18:32:03 |
 cbwilliams | I think I remember seeing that we can add the tag [associative] to an operator, but I don't know where I saw this. | 18:33:26 |
| nishantjr | I'm not sure if that was in a really old version on K based on maude, but that's no longer supported unfortunately. I think in this situation, you move to create a rule to move each subterm to its own cell within a cell marked multiplicity="*" type="Set", as in the thread cell here : https://github.com/kframework/k/blob/master/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md#configuration | 18:39:21 |
| nishantjr | You'd need a rule similar to https://github.com/kframework/k/blob/master/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md#spawn | 18:40:06 |
| nishantjr | Another way of getting commutativity is to use the builtin SET module (though I don't think its appropriate in this case). https://github.com/kframework/k/blob/master/k-distribution/include/kframework/builtin/domains.md#sets | 18:41:06 |
| cbwilliams | okay, thanks, this seems to be working so far. | 18:49:28 |
| cbwilliams | Redacted or Malformed Event | 18:49:36 |
| cbwilliams | Redacted or Malformed Event | 18:49:46 |
| cbwilliams | Redacted or Malformed Event | 18:50:03 |
| cbwilliams | Redacted or Malformed Event | 18:50:13 |
| cbwilliams | Redacted or Malformed Event | 18:50:24 |
| cbwilliams | Redacted or Malformed Event | 18:50:49 |
| cbwilliams | Redacted or Malformed Event | 18:50:53 |
| cbwilliams | Redacted or Malformed Event | 18:51:17 |
| Mike Stay | Redacted or Malformed Event | 18:54:32 |
| Mike Stay | Redacted or Malformed Event | 18:55:53 |
| Mike Stay | * If we just have an in(...), we see it in the <in> cell. Ditto for out(...). But if we put both in, they react with each other using the final rule but we don't see the result in the <k> cell. | 18:56:15 |
| cbwilliams | *
module RHO-SYNTAX
imports DOMAINS-SYNTAX
imports KVAR-SYNTAX
syntax N ::= "&" Terms
| KVar
syntax Zero ::= "Z"
syntax In ::= "in" "(" KVar "<-" N "." Terms ")" [binder]
syntax Out ::= "out" "(" N "," Terms ")"
syntax Term ::= Zero
| In
| Out
syntax Terms ::= List{Term, "|"}
endmodule
module RHO
imports RHO-SYNTAX
imports SUBSTITUTION
syntax KResult ::= Terms
configuration <T>
<ins>
<in multiplicity="*" type="Set"> . </in>
</ins>
<outs>
<out multiplicity="*" type="Set"> . </out>
</outs>
<k> $PGM:Terms </k>
</T>
rule
<k> _:Zero | Ts:Terms => Ts </k>
rule
<k> I:In | Ts:Terms => Ts </k>
<ins> (Is) => (Is <in> I </in>) </ins>
rule
<k> O:Out | Ts:Terms => Ts </k>
<outs> (Os) => (Os <out> O </out>) </outs>
rule
<in> in (Y <- X . Ts:Terms ) => . </in>
<out> out(X , P:Terms) => . </out>
<k> .Terms => Ts[&P / Y] </k>
endmodule```
| 19:01:14 |
| Mike Stay | Is there a way to concatenate lists? | 19:12:24 |
| Mike Stay | For example, suppose we have a list of Xs separated by "|", where an X is either a Y or a list of Ys.
Something like rule <k> (ys:Ys) | xs:Xs => ys ++ xs </k> | 19:15:14 |
| nishantjr | Unfortunately you'd need to write a function, like "++DeclList" here https://github.com/kframework/boogie-semantics/blob/master/helpers.md . | 19:22:26 |
| nishantjr | Try using the --depth flag to krun to see what the state looks like at each step. | 19:23:11 |
| Mike Stay | OK, thanks. When there are multiple rules that can apply to a configuration, how do we see all the possible outcomes? | 19:31:37 |
| Mike Stay | BTW, why would we need to write concatenation for a built-in data structure? syntax Xs ::= List{X, "|"} | 19:33:23 |
| nishantjr | Use --search for the LLVM (default) backend. For haskell it is the default behaviour. | 19:41:52 |
| nishantjr | I'm not sure why exactly we dont have this yet. Currently this production desugars into ordinary rules, but no functions are generated. I think the plan is to replace these with parametric data types eventually. I think functions over parametric datatypes is on the TODO list though I'm not sure what the priority is exactly. | 19:44:23 |
| cbwilliams | sorry, I don't understand. how do we write a term and display its graph of all future behaviors? | 21:25:02 |
| cbwilliams | surely there is a way to do this; I believe that reasoning about these graphs is one of the main purposes of Matching Logic. | 21:26:59 |
