Example project for kompile --post-process using pyk

pyk/pyk-tests/Makefile

@@ -10,12 +10,13 @@ CHECK = git --no-pager diff --no-index -R
 
 
 .PHONY: all clean update-results \
-        test test-kpyk test-kpyk-graphviz test-kpyk-minimize-term
+        test test-kpyk test-kpyk-graphviz test-kpyk-minimize-term test-post-process
 
 all: test
 
 clean:
 	rm -rf definitions
+	$(MAKE) -C post-process clean
 
 update-results: CHECK=cp
 update-results: test
@@ -27,7 +28,7 @@ test: test-kpyk
 
 ## kpyk runner tests
 
-test-kpyk: test-kpyk-graphviz test-kpyk-minimize-term
+test-kpyk: test-kpyk-graphviz test-kpyk-minimize-term test-post-process
 
 test-kpyk-graphviz: d.kompiled
 	$(PYK) -v definitions/d graph-imports
@@ -39,6 +40,9 @@ test-kpyk-minimize-term: imp-verification.kompiled
 	    | $(PYK) -v definitions/imp-verification print /dev/stdin > imp-unproveable-spec.k.out
 	$(CHECK) imp-unproveable-spec.k.out imp-unproveable-spec.k.expected
 
+test-post-process:
+	$(MAKE) -C post-process
+
 
 ## definitions to build ahead of time
 

pyk/pyk-tests/post-process/.gitignore

@@ -0,0 +1 @@
+kompiled/

pyk/pyk-tests/post-process/Makefile

@@ -0,0 +1,14 @@
+KOMPILED_DIR := kompiled
+
+.PHONY: clean
+
+
+$(KOMPILED_DIR)/timestamp: assign.k transform.py
+	kompile assign.k                      \
+	  --backend haskell                   \
+	  --output-definition $(KOMPILED_DIR) \
+	  --emit-json                         \
+	  --post-process 'python3 transform.py'
+
+clean:
+	rm -rf $(KOMPILED_DIR)

pyk/pyk-tests/post-process/assign.k

@@ -0,0 +1,41 @@
+module ASSIGN-SYNTAX
+    imports INT-SYNTAX
+    imports ID-SYNTAX
+
+    syntax Expr ::= Int | Id
+
+    syntax Stmt   ::= Decl | Assign
+    syntax Decl   ::= "var" Ids ";"
+    syntax Ids    ::= List{Id, ","}
+    syntax Assign ::= Id "=" Expr ";" [strict(2)]
+
+    syntax Pgm    ::= List{Stmt, ""}
+
+    syntax KResult ::= Int
+endmodule
+
+
+module ASSIGN
+    imports ASSIGN-SYNTAX
+    imports BOOL
+
+    configuration
+        <T>
+            <k> $PGM:Pgm </k>
+            <env> .Map </env>
+        </T>
+
+    rule <k> S:Stmt P:Pgm => S ~> P ... </k>
+    rule <k> .Pgm => . ... </k>
+
+    rule [r1]: <k> X:Id => I ... </k>
+               <env> ... X |-> I ... </env>
+
+    rule [r2]: <k> X = I:Int; => . ... </k>
+               <env> ... X |-> (_ => I) ... </env>
+
+    rule <k> var .Ids ; => . ... </k>
+
+    rule [r3]: <k> var (X, Xs => Xs); ... </k>
+               <env> Rho:Map (.Map => X |-> 0) </env> requires notBool (X in_keys(Rho))
+endmodule

pyk/pyk-tests/post-process/transform.py

@@ -0,0 +1,69 @@
+import json
+from argparse import ArgumentParser
+from sys import stdin
+
+from pyk.kast import KDefinition, KInner, KRule, KSentence, KVariable, top_down
+from pyk.kastManip import if_ktype
+
+
+def main():
+    parser = create_argument_parser()
+    args = parser.parse_args()
+
+    with open(args.compiled_json, 'r') as f:
+        json_data = json.load(f)
+
+    format = json_data['format']
+    version = json_data['version']
+    term = json_data['term']
+
+    input_definition = KDefinition.from_dict(term)
+    output_definition = transform_definition(input_definition)
+
+    print(json.dumps({
+        'format': format,
+        'version': version,
+        'term': output_definition.to_dict(),
+    }))
+
+
+def create_argument_parser() -> ArgumentParser:
+    parser = ArgumentParser(description='Transform rules of a compiled K definition')
+    parser.add_argument('compiled_json', type=str, help='Path to compiled.json')
+    return parser
+
+
+def transform_definition(definition: KDefinition) -> KDefinition:
+    return (
+        definition.let(modules=(
+            module.let(sentences=(
+                transform_sentence(sentence) for sentence in module.sentences
+            )) for module in definition.modules
+        ))
+    )
+
+
+def transform_sentence(sentence: KSentence) -> KSentence:
+    return transform_rule(sentence) if type(sentence) is KRule else sentence
+
+
+def transform_rule(rule: KRule) -> KRule:
+    return rule.let(
+        body=rename_anon_vars(rule.body),
+        requires=rename_anon_vars(rule.requires),
+        ensures=rename_anon_vars(rule.ensures),
+    )
+
+
+def rename_anon_vars(kinner: KInner) -> KInner:
+    return top_down(if_ktype(KVariable, rename_anon), kinner)
+
+
+def rename_anon(var: KVariable) -> KVariable:
+    if var.name.startswith('_Gen'):
+        return var.let(name='_Var' + var.name[4:])
+    return var
+
+
+if __name__ == "__main__":
+   main()