A small example use of SynthCL grammar.

jamestiotio · Feb 28, 2016 · da2f985 · da2f985
1 parent 9efb1ff
commit da2f985
Showing 1 changed file with 20 additions and 0 deletions.
diff --git a/sdsl/synthcl/test/grammar.rkt b/sdsl/synthcl/test/grammar.rkt
@@ -0,0 +1,20 @@
+#lang s-exp "../lang/main.rkt"
+
+
+(grammar int (expr [int x] [int y] [int depth])
+  #:base (choose x y)
+  #:else (locally-scoped
+          (: int left right)
+          (= left  (expr x y (- depth 1)))
+          (= right (expr x y (- depth 1)))
+          (+ left right)))
+
+(procedure int (h0 [int x] [int y])
+  (expr x y 1))
+
+(procedure int (s0 [int x] [int y])
+  (+ x y))
+
+(synth #:forall [(: int x) (: int y)]
+       #:ensure (assert (== (h0 x y) (s0 x y))))
+