Update examples

Author: engboris

README.md

@@ -46,20 +46,11 @@ Finite state machine
   [(-i [1|X]) (+i X)]})
 
 'input words
-(:= e (+i []))
-(:: e binary)
-
-(:= 0 (+i [0]))
-(:: 0 binary)
-
-(:= 000 (+i [0 0 0]))
-(:: 000 binary)
-
-(:= 010 (+i [0 1 0]))
-(:: 010 binary)
-
-(:= 110 (+i [1 1 0]))
-(:: 110 binary)
+(:= e (+i []))        (:: e binary)
+(:= 0 (+i [0]))       (:: 0 binary)
+(:= 000 (+i [0 0 0])) (:: 000 binary)
+(:= 010 (+i [0 1 0])) (:: 010 binary)
+(:= 110 (+i [1 1 0])) (:: 110 binary)
 
 '''
 automaton accepting words ending with 00

examples/automata.sg

@@ -8,20 +8,11 @@
   [(-i [1|X]) (+i X)]})
 
 'input words
-(:= e (+i []))
-(:: e binary)
-
-(:= 0 (+i [0]))
-(:: 0 binary)
-
-(:= 000 (+i [0 0 0]))
-(:: 000 binary)
-
-(:= 010 (+i [0 1 0]))
-(:: 010 binary)
-
-(:= 110 (+i [1 1 0]))
-(:: 110 binary)
+(:= e (+i []))        (:: e binary)
+(:= 0 (+i [0]))       (:: 0 binary)
+(:= 000 (+i [0 0 0])) (:: 000 binary)
+(:= 010 (+i [0 1 0])) (:: 010 binary)
+(:= 110 (+i [1 1 0])) (:: 110 binary)
 
 (:= (initial Q) [(-i W) (+a W Q)])
 (:= (accept Q) [(-a [] Q) accept])

examples/binary4.sg

@@ -7,15 +7,13 @@
 (:= (make_bin Name X1 X2 X3 X4)
   { [(+b Name 1 X1)] [(+b Name 2 X2)] [(+b Name 3 X3)] [(+b Name 4 X4)] })
 
-(:= b1 #(make_bin b1 0 0 0 1))
-(:: b1 u4)
-
-(:= b2 #(make_bin b2 0 0 1 1))
-(:: b2 u4)
+(:= b1 #(make_bin b1 0 0 0 1)) (:: b1 u4)
+(:= b2 #(make_bin b2 0 0 1 1)) (:: b2 u4)
 
 (show #b1)
 (show #b2)
 
+(:= (if A = X then R = Z) [(-b A I X) (+b R I Z)])
 (:= (if A = X and B = Y then R = Z) [(-b A I X) (-b B I Y) (+b R I Z)])
 
 (:= (and A B R) {
@@ -32,10 +30,17 @@
 (show #ror)
 (== #ror #(make_bin r 0 0 1 1))
 
+(:= (not A R) {
+  #(if A = 1 then R = 0)
+  #(if A = 0 then R = 1) })
+(:= rnot (process #b1 #(not b1 r)))
+(show #rnot)
+(== #rnot #(make_bin r 1 1 1 0))
+
+(:= rnand (process #b1 #(and b1 b2 r1) #b2 #(not r1 r2)))
+(show #rnand)
+
 '''
-(:= (xor A B R) {
-  #(if A = X and B = X then R = 0) })
-(:= rxor (process #b1 #(xor b1 b2 r) #b2))
+(:= rxor (process #rnand #(and r2 r r3) #ror))
 (show #rxor)
-(== #rxor #(make_bin r 0 0 1 0))
 '''

examples/nat.sg

@@ -6,14 +6,9 @@
   [(-nat 0) ok]
   [(-nat (s N)) (+nat N)]})
 
-(:= 0 (+nat 0))
-(:: 0 nat)
-
-(:= 1 (+nat (s 0)))
-(:: 1 nat)
-
-(:= 2 <+nat s s 0>)
-(:: 2 nat)
+(:= 0 (+nat 0))     (:: 0 nat)
+(:= 1 (+nat (s 0))) (:: 1 nat)
+(:= 2 <+nat s s 0>) (:: 2 nat)
 
 (:= add1 [(-nat X) (+nat (s X))])
 

examples/npda.sg

@@ -8,17 +8,10 @@
   [(-i [1|X]) (+i X)]})
 
 'input words
-(:= e (+i []))
-(:: e binary)
-
-(:= 0000 (+i [0 0 0 0]))
-(:: 0000 binary)
-
-(:= 0110 (+i [0 1 1 0]))
-(:: 0110 binary)
-
-(:= 1110 (+i [1 1 1 0]))
-(:: 1110 binary)
+(:= e (+i []))           (:: e binary)
+(:= 0000 (+i [0 0 0 0])) (:: 0000 binary)
+(:= 0110 (+i [0 1 1 0])) (:: 0110 binary)
+(:= 1110 (+i [1 1 1 0])) (:: 1110 binary)
 
 (:= (initial Q) [(-i W) (+a W [] Q)])
 (:= (accept Q) [(-a [] [] Q) accept])

examples/sumtypes.sg

@@ -8,15 +8,11 @@
   [-west ok]
   [-east ok]})
 
-(:= n +north)
-(:: n direction)
+(:= n +north) (:: n direction)
 
-(spec result {
-  [(-ok X) ok]
-  [(-error X) ok]})
+(spec result { [(-ok X) ok] [(-error X) ok]})
 
-(:= x (+ok a))
-(:: x result)
+(:= x (+ok a)) (:: x result)
 
 'pattern matching
 (:= get_ok {

src/expr.ml

@@ -28,8 +28,6 @@ type expr =
   | List of expr list
 [@@derive eq]
 
-let pp_err _ = ""
-
 let primitive = String.append "%"
 
 let nil_op = primitive "nil"