Open liyili2 opened 9 years ago
4, in order to separate one inductive rules into several different sorts of inductive rules, we need to separate the rules based on the type of the first element of K cell.
In order to do so, we need to have a mechanism in Java to collect the sort of the first element of K cell.
I think the collection will happen in the rule level of a visitor pattern in Java.
Liyi Li
Instead of printing out the following:
datatype ('a,'context) step_conf =
Direct "'a
we should print out the:
datatype ('a,'context) step_conf =
Singleton "'a" "'a" (* rule a1
Second step is to print out the type of collection of threeTuples. To have three functions where:
by giving two arguments, the functions will return the other feild in the threeTuples.
The next step is to divide the inductive impRule into several categories according to the sort in the K cell. For example:
if we have the following rule in K:
rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0
The sort in the K cell is AExp, so that when we print out the rule, we should print it out in the
inductive aexpRule category.
Hence, If we want to print out the imp.k file, we should print it out as these several categories:
Inductive AExpRule
inductive BExpRule
inductive StmtRule
inductive BlockRule
inductive PgmRule
inductive KRule
The next step is to deal with KResult sort in a rule
If we have the following rule:
rule I1:Int / I2:Int => I1 /Int I2 when I2 =/=Int 0
Since I1 and I2 are kresult in Imp.k, and / is a experssion in AExp sort, when we are print out the rule, we will need to use the function is_akresult to do something like:
is_akresult I1 ==> is_akresult I2 ==> AExpRule (I1 / I2) (I1 div I2) (a)
What I mean is that, originally, we have the printing function as:
AExpRule ((I1::int) / (I2::Int)) ((I1::int) div (I2:int)) when we print it out to Isabelle.
Now, instead of printing out the above result, we should print out the rule as we shown in (a).
1, printing out of the syntax doesn't need that much treatment. There are several small fixed
For example, if we have the following sort:
syntax AExp ::= Int | Id | "AexpPlus" AExp AExp [strict]
and the KResult is like:
syntax KResult ::= Int | Bool
We can print out the kresult function for AExp as: fun is_akresult where "is_akresult (AexpInt i) = True" | "isakresult = False"
Since the intersection of KResult sort and the AExp are only share common sort of Int. We need to print out the kresult determining function for every sort of a definition.
2, for each subsorting relation, create a proper constructor for it, which has already been done by current implementation of KToIlabelle.
For example, if we have the following syntax:
syntax AExp ::= Int | Id | "AexpPlus" AExp AExp [strict]
When we are translating it into Isabelle, we need to add two constructors for Int and Id, such as
syntax AExp ::= aexpInt Int | aexpId Id
In the Java code, we need to maintain a map as (aexpInt |-> (AExp, Int); aexpId |-> (AExp, Id)), etc.
It will be convenient to maintain a map from (AExp, Int) |-> aexpInt also.
In addition, it is better to have a map to collect all the kresult sort constructor.
For example, The Int sort is the kresult sort of AExp, so that we need to have a kresult map like:
(AExp, Int) |-> aexpInt.
This map will help to establish the kresult identifying functions we described above.
3, we need to print out the datatype for the inductive rules in Isabelle as:
datatype ('a,'context) stepconf = Direct "'a 'context" "kitem 'context" (* rule a1 a2 ... state1 state2 )
| Final "'a 'context" "kresult 'context"
| Heating "'a" "kitem 'a" ( rule a1 k a2[] )
| Cooling "kresultvalue 'a" "'a" ( rule k a1[] a2[] *)
I think we can do better than that, since I think the datatype of the transition rules have nothing to do with Heating/cooling/Direct or Final rules. We don't need to divide the category of these rules. Instead, we need to have a smart way in Isabelle to represent the configurations, especially the AC matching properties of these configurations.