C generation with Mathematica

khp.md

@@ -85,7 +85,7 @@ Main symbolic execution semantics
 ```{.k}
 module KHP
     imports KHP-SYNTAX
-    imports MAP
+    imports COLLECTIONS
     imports WOLFRAMLANGUAGE
     imports K-IO
 
@@ -95,15 +95,12 @@ module KHP
     syntax KItem ::= "#processMode" "(" Mode ")"
                    | "#synthesizeConstraints"
 
-    syntax Ids ::= ".Ids"
-                 | Id
-                 | Ids "," Ids  [right]
-
     configuration <k> #processMode($MODE) ~> $PGM:Pgm </k>
                   <pgmVars> .Ids </pgmVars>
                   <state> .Map </state>
                   <evolutionConditions> .Set </evolutionConditions>
                   <counter> 0 </counter>
+                  <constraintVars> SetItem(String2Id("t_post")) </constraintVars>
 
     rule #processMode(#regular) ~> P:Pgm => P
     rule #processMode(#constraintSynthesis) ~> P:Pgm => P ~> #synthesizeConstraints
@@ -129,6 +126,7 @@ For each variable, the state is bound to a logical Variable of sort `Real`.
             (.Set => SetItem(#appendStrToPgmVar(X, "_i") == #VarReal(#prependStrToPgmVar("VAR_", X))))
             ...
          </evolutionConditions>
+         <constraintVars> ... .Set => (SetItem(#prependStrToPgmVar("VAR_", X)) SetItem(#appendStrToPgmVar(X, "_i"))) ... </constraintVars>
 
     rule vars .VarDecls ; S:Stmts => S
     syntax FullFormExpression ::= "#toWolframExpression" "(" BExp ")" [function]
@@ -383,10 +381,17 @@ Mechanism to handle storing evolution conditions
 
     syntax KItem ::= "#wolfram.quantifierElimination" "(" FullFormExpression ")"    [function]
 
-    rule #wolfram.quantifierElimination( WLFRAMEXPR )
+    syntax Ids ::= "List2Ids" "(" List ")" [function]
+    rule List2Ids(.List) => .Ids
+    rule List2Ids(ListItem(I:Id) L:List) => I , List2Ids(L)
+
+    rule <k> #wolfram.quantifierElimination( WLFRAMEXPR )
       => #system("wolframscript -c" +String "\""
+                //+String #toWolframExpressionString(Compile[ { List2Ids(Set2List(Vars)) } , WLFRAMEXPR ])
                 +String #toWolframExpressionString(Resolve[ WLFRAMEXPR, Reals ])
-                +String "\"")
+                +String "\"") <k>
+         //<constraintVars> Vars </constraintVars>
+
 
     rule <k> #processFinalStateConstraints ~> #constraints(WLFRAMEXPR)
           => #wolfram.quantifierElimination(WLFRAMEXPR) </k>

wolframlanguage.md

@@ -8,11 +8,18 @@ module WOLFRAMLANGUAGE-SYNTAX
     imports ID
     imports STRING
 
+    syntax Ids ::= ".Ids"
+                 | Id
+                 | Ids "," Ids  [right]
+
+    syntax VariableExpressions ::= "{" Ids "}"
+
     syntax FullFormExpression ::= Id
                                 | Real
                                 | "True"    [token]
                                 | "Reals"   [token]
                                 | Operator "[" FullFormExpressions "]"
+                                | Operator "[" VariableExpressions "," FullFormExpressions "]"
 
     syntax FullFormExpressions ::= List{FullFormExpression, ","}
 
@@ -30,9 +37,12 @@ module WOLFRAMLANGUAGE-SYNTAX
                       | "Implies"      [token]
                       | "ForAll"       [token]
                       | "Resolve"      [token]
+                      | "Export"       [token]
+                      | "Compile"      [token]
 
     syntax String ::= "Operator2String" "(" Operator ")"                            [function, hook(STRING.token2string)]
                     | "#toWolframExpressionString"    "(" FullFormExpression ")"    [function]
+                    | "#toWolframExpressionString"    "(" VariableExpressions ")"   [function]
                     | "#toWolframExpressionStringAux" "(" FullFormExpressions ")"   [function]
 
 endmodule
@@ -44,6 +54,8 @@ module WOLFRAMLANGUAGE
     rule #toWolframExpressionString(REAL:Real) => Real2String(REAL)
     rule #toWolframExpressionString(True) => "True"
     rule #toWolframExpressionString(Reals) => "Reals"
+    //rule #toWolframExpressionString({ E:FullFormExpressions }) => "{" +String #toWolframExpressionStringAux(E) +String "}"
+    rule #toWolframExpressionString({ I:Id , Rest:Ids }) => "{" +String Id2String(I) +String #toWolframExpressionString(Rest) +String "}"
 
     rule #toWolframExpressionStringAux(E1:FullFormExpression , E2:FullFormExpressions)
       => #toWolframExpressionString(E1) +String ", " +String #toWolframExpressionStringAux(E2)
@@ -55,6 +67,10 @@ module WOLFRAMLANGUAGE
       => Operator2String(OP)
          +String "[" +String #toWolframExpressionStringAux(EXPRS) +String "]"
 
+    rule #toWolframExpressionString(OP:Operator [ VARS:VariableExpressions , EXPRS:FullFormExpressions ])
+      => Operator2String(OP)
+         +String "[" +String #toWolframExpressionString(VARS) +String #toWolframExpressionStringAux(EXPRS) +String "]"
+
 endmodule
 
 ```