plutus-core: sizeOfInteger; succ-integer

runtimeverification · Dec 7, 2018 · 02577e3 · 02577e3
1 parent 0ca81c6
commit 02577e3
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 17 deletions.
diff --git a/lib/build.py b/lib/build.py
@@ -138,6 +138,7 @@ def test_typing(input):
 test('t/sum-list.plc')
 test('t/sum.plc')
 test('t/fact.plc')
+test('t/succ-integer.plc')
 
 # Typing tests
 # ------------

diff --git a/plutus-core.md b/plutus-core.md
@@ -77,6 +77,7 @@ module PLUTUS-CORE-SYNTAX-BASE
 
     syntax BuiltinName   ::= BinaryBuiltin | UnaryBuiltin
     syntax UnaryBuiltin  ::= "sha2_256" | "sha3_256"
+                           | "sizeOfInteger"
     syntax BinaryBuiltin ::= "addInteger"         | "subtractInteger"
                            | "multiplyInteger"    | "divideInteger"
                            | "remainderInteger"

diff --git a/t/succ-integer.plc b/t/succ-integer.plc
@@ -1,20 +1,25 @@
 (program 1.0.0
-  (abs
-    s
-    (size)
-    (lam
-      i
-      [(con integer) s]
-      [
-        [ { (builtin addInteger) s } i ]
-        [
+  [ {
+      (abs
+        s
+        (size)
+        (lam
+          i
+          [(con integer) s]
           [
-            { { (builtin resizeInteger) (con 1) } s }
-            [ { (builtin sizeOfInteger) s } i ]
+            [ { (builtin addInteger) s } i ]
+            [
+              [
+                { { (builtin resizeInteger) (con 1) } s }
+                [ { (builtin sizeOfInteger) s } i ]
+              ]
+              (con 1 ! 1)
+            ]
           ]
-          (con 1 ! 1)
-        ]
-      ]
-    )
-  )
-)
+        )
+      )
+      (con 1)
+    }
+    (con 1 ! 3)
+  ]
+)
diff --git a/t/succ-integer.plc.expected b/t/succ-integer.plc.expected
@@ -0,0 +1,11 @@
+<generatedTop>
+  <k>
+    ( con 1 ! 4 )
+  </k>
+  <env>
+    .Map
+  </env>
+  <store>
+    .Map
+  </store>
+</generatedTop>