2, for each subsorting relation, create a proper constructor for it, which has already been done by current implementation of KToIlabelle.
However, we also need to keep a record or two maps in the java code. For each generate constructor, we need to know its direct subsort and its super sort.
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.
2, for each subsorting relation, create a proper constructor for it, which has already been done by current implementation of KToIlabelle. However, we also need to keep a record or two maps in the java code. For each generate constructor, we need to know its direct subsort and its super sort.
For example, if we have the following syntax:
When we are translating it into Isabelle, we need to add two constructors for Int and Id, such as
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:
This map will help to establish the kresult identifying functions we described above.