How to let functions run recursively in k framework?

17 Views Asked by At

I have defined Val as value which needs no more process, and two functions operate recursive_modify.

syntax Val ::= Int | Bool | String
               | array(Type,Map,Int) // my own wrapped array implemented with `Map`
syntax KItem ::= operate(Val)
syntax Val ::= recursive_modify(Val,...) // more arguments are omitted here
syntax KResult ::= Val

rule <k> operate(array(T,M,I)) => /** something here **/ ... </k>

Since the array can be multi-dimensioned, I offer recursive_modify to modify specific element in the array, and I wish the return value of recursive_modify is the new array after modification, so it belongs to the sort Val as well. Here I offer two semantic cases for it:

rule recursive_modify(array(T,M,L),...) => array(T,M[/**some update here**/],L)
requires // arguments indicate the array is now 1-D and can be directly modified
rule recursive_modify(array(T,M,L),...) => 
     array(T,M[/*some index*/ <- recursive_modify(array(T,M,L),...)],L)
requires // arguments indicate the array is multi-D and should be recursively modified

Now I need to do some operation on an array A, using operate(A). But I wanna modify an element in A, and then do the operation, so I tried operate(recursive_modify(A,...)). But the program got stuck like

<k>
operate(recursive_modify(Val,...)) ~> ....
</k>

Cause recursive_modify is also the sort Val.

How to let the recursive_modify continue until it evaluates an array array(_,_,_)?

0

There are 0 best solutions below