Implement placeholder variable and fix examples

Author: engboris

README.md

@@ -36,31 +36,41 @@ philosophy).
 Finite state machine
 
 ```
+(new-declaration (:: tested test)
+  (:= test @(exec (union @#tested #test)))
+  (== test ok))
+
 (spec binary [
-  [(-i e) ok]
-  [(-i [0 X]) (+i X)]
-  [(-i [1 X]) (+i X)]])
+  [(-i []) ok]
+  [(-i [0|X]) (+i X)]
+  [(-i [1|X]) (+i X)]])
 
 'input words
+(:= e (+i []))
 (:: e binary)
-(:= e (+i e))
 
+(:= 0 (+i [0]))
+(:: 0 binary)
+
+(:= 000 (+i [0 0 0]))
 (:: 000 binary)
-(:= 000 (+i [0 0 0 e]))
 
+(:= 010 (+i [0 1 0]))
 (:: 010 binary)
-(:= 010 (+i [0 1 0 e]))
 
+(:= 110 (+i [1 1 0]))
 (:: 110 binary)
-(:= 110 (+i [1 1 0 e]))
 
+'''
+automaton accepting words ending with 00
+'''
 (:= a1 [
   [(-i W) (+a W q0)]
-  [(-a e q2) accept]
-  [(-a [0 W] q0) (+a W q0)]
-  [(-a [0 W] q0) (+a W q1)]
-  [(-a [1 W] q0) (+a W q0)]
-  [(-a [0 W] q1) (+a W q2)]])
+  [(-a [] q2) accept]
+  [(-a [0|W] q0) (+a W q0)]
+  [(-a [0|W] q0) (+a W q1)]
+  [(-a [1|W] q0) (+a W q0)]
+  [(-a [0|W] q1) (+a W q2)]])
 
 <show kill exec (union @#e #a1)>
 <show kill exec (union @#000 #a1)>

examples/binary4.sg

@@ -1,8 +1,10 @@
-(spec u4
-  (const
-    (star (-b 1 _) (-b 2 _) (-b 3 _) (-b 4 _) ok)))
+(spec u4 [(-b 1 _) (-b 2 _) (-b 3 _) (-b 4 _) ok])
+
+(new-declaration (:: tested test)
+  (:= test @(exec (process #test #test)))
+  (== test ok))
 
-(def checker
+(:= checker
   (galaxy
     (interaction
       (process

examples/nat.sg

@@ -1,42 +1,35 @@
-(spec nat
-  (const
-    (star (-nat 0) ok)
-    (star (-nat (s N)) (+nat N))))
+(spec nat [
+  [(-nat 0) ok]
+  [(-nat (s N)) (+nat N)]])
 
-(def fchecker
-  (galaxy
-    (interaction (union @#tested #test))
-    (expect (const (star arg out)))))
+(new-declaration (:: tested test)
+  (:= test @(exec (union @#tested #test)))
+  (== test ok))
 
-(spec (arrow nat nat)
-  (const
-    (star (+nat X) arg)
-    (star (-nat X) out)))
+(new-declaration (:: tested test fchecker)
+  (:= test @(exec (union @#tested #test)))
+  (== test [arg out]))
 
+(spec (arrow nat nat) [
+  [(+nat X) arg]
+  [(-nat X) out]])
+
+(:= 0 (+nat 0))
 (:: 0 nat)
-(def 0
-  (const (star (+nat 0))))
 
+(:= 1 (+nat (s 0)))
 (:: 1 nat)
-(def 1
-  (const
-    (star (+nat (s 0)))))
 
+(:= 2 <+nat s s 0>)
 (:: 2 nat)
-(def 2
-  (const
-    (star <+nat s s /0>)))
-
-(:: add1 ((arrow nat nat) / fchecker))
-(def add1
-  (const
-    (star (-nat X) (+nat (s X)))))
-
-(def is_empty
-  (const
-    (star (-nat 0) (res 1))
-    (star (-nat (s _)) (res 0))))
-
-(show-exec (union @#add1 #2))
-(show-exec (union #is_empty @#0))
-(show-exec (union #is_empty @#1))
+
+(:= add1 [(-nat X) (+nat (s X))])
+(:: add1 (arrow nat nat) fchecker)
+
+(:= is_empty [
+  [(-nat 0) (res 1)]
+  [(-nat (s _)) (res 0)]])
+
+<show exec (union @#add1 #2)>
+<show exec (union #is_empty @#0)>
+<show exec (union #is_empty @#1)>

examples/npda.sg

@@ -1,48 +1,39 @@
-(spec binary
-  (const
-    (star (-i e) ok)
-    (star (-i [0 X]) (+i X))
-    (star (-i [1 X]) (+i X))))
+(new-declaration (:: tested test)
+  (:= test @(exec (union @#tested #test)))
+  (== test ok))
+
+(spec binary [
+  [(-i []) ok]
+  [(-i [0|X]) (+i X)]
+  [(-i [1|X]) (+i X)]])
 
 'input words
+(:= e (+i []))
 (:: e binary)
-(def e
-  (const (star (+i e))))
 
+(:= 0000 (+i [0 0 0 0]))
 (:: 0000 binary)
-(def 0000
-  (const (star (+i [0 0 0 0 e]))))
 
+(:= 0110 (+i [0 1 1 0]))
 (:: 0110 binary)
-(def 0110
-  (const (star (+i [0 1 1 0 e]))))
 
+(:= 1110 (+i [1 1 1 0]))
 (:: 1110 binary)
-(def 1110
-  (const (star (+i [1 1 1 0 e]))))
 
-(def a1
-  (galaxy
-    (initial
-      (const
-        (star (-i W) (+a W e q0))))
-    (final
-      (const
-        (star (-a e e q0) accept)
-        (star (-a e e q1) accept)))
-    (transitions
-      (const
-        (star (-a [0 W] S q0) (+a W [0 S] q0))
-        (star (-a [1 W] S q0) (+a W [1 S] q0))
-        (star (-a W S q0) (+a W S q1))
-        (star (-a [0 W] [0 S] q1) (+a W S q1))
-        (star (-a [1 W] [1 S] q1) (+a W S q1))))))
+(:= a1 [
+  'initial
+  [(-i W) (+a W [] q0)]
+  'final
+  [(-a [] [] q0) accept]
+  [(-a [] [] q1) accept]
+  'transitions
+  [(-a [0|W] S q0) (+a W [0|S] q0)]
+  [(-a [1|W] S q0) (+a W [1|S] q0)]
+  [(-a W S q0) (+a W S q1)]
+  [(-a [0|W] [0|S] q1) (+a W S q1)]
+  [(-a [1|W] [1|S] q1) (+a W S q1)]])
 
-(show (kill (exec
-      (union @#e #a1))))
-(show (kill (exec
-      (union @#0000 #a1))))
-(show (kill (exec
-      (union @#0110 #a1))))
-(show (kill (exec
-      (union @#1110 #a1))))
+<show kill exec (union @#e #a1)>
+<show kill exec (union @#0000 #a1)>
+<show kill exec (union @#0110 #a1)>
+<show kill exec (union @#1110 #a1)>

examples/prolog.sg

@@ -1,35 +1,27 @@
 ' unary addition
-(def add
-  (const
-    (star (+add 0 Y Y))
-    (star (-add X Y Z) (+add (s X) Y (s Z)))))
+(:= add [
+  [(+add 0 Y Y)]
+  [(-add X Y Z) (+add (s X) Y (s Z))]])
 
 ' 2 + 2 = R
-(def query
-  (const
-    (star (-add <s s /0> <s s /0> R) R)))
+(:= query [(-add <s s 0> <s s 0> R) R])
 
-(show-exec (union #add @#query))
+<show exec (union #add @#query)>
 
-(def graph
-  (const
-    (star (+from 1) (+to 2))
-    (star (+from 1) (+to 3))
-    (star (+from 3) (+to 2))
-    (star (+from 3) (+to 4))))
-    '(star (+from 4) (+to 3))
+(:= graph [
+  [(+from 1) (+to 2)]
+  [(+from 1) (+to 3)]
+  [(+from 3) (+to 2)]
+  '[(+from 4) (+to 3)]
+  [(+from 3) (+to 4)]])
 
-(def composition
-  (const
-    (star (-to X) (-from X))))
+(:= composition [(-to X) (-from X)])
 
 ' is there a path between 1 and 4?
-(def query
-  (const
-    (@star (-from 1))
-    (star (-to 4) ok)))
+(:= query [
+  @[(-from 1)]
+  [(-to 4) ok]])
 
-(show-exec (process
+<show exec (process
   #query
-  (union #graph #composition)
-  &kill))
+  (union #graph #composition))>

examples/stack.sg

@@ -1,21 +1,18 @@
-(show-exec (process
-  (const (star (+stack0 e)))
+<show exec (process
+  (+stack0 [])
   'push 1 then 0
-  (const
-    (star (-stack0 X) (+stack1 [1 X]))
-    (star (-stack1 X) (+stack2 [0 X])))
+  [(-stack0 X) (+stack1 [1|X])]
+  [(-stack1 X) (+stack2 [0|X])]
 
   'pop & save
-  (const (star (-stack2 [C X]) (+stack3 X) (+save C)))
+  [(-stack2 [C|X]) (+stack3 X) (+save C)]
 
   'conditional duplication
-  (const
-    (star (-stack3 [0 X]) (+stack4 [0 0 X]))
-    (star (-stack3 [1 X]) (+stack4 [1 1 X])))
+  [(-stack3 [0|X]) (+stack4 [0 0|X])]
+  [(-stack3 [1|X]) (+stack4 [1 1|X])]
 
   'freeze information
-  (const (star (-stack4 X) (stack X)))
+  [(-save C) (save C)]
 
-  (const (star (-save C) (save C)))
-  'kill remaining polarized stars
-  &kill))
+  'clean
+  [(-stack4 _)])>

examples/sumtypes.sg

@@ -1,32 +1,26 @@
-(def checker
-  (galaxy
-    (interaction (union @#tested #test))
-    (expect (const (star ok)))))
+(new-declaration (:: tested test)
+  (:= test @(exec (union @#tested #test)))
+  (== test ok))
 
-(spec direction
-  (const
-    (star -north ok)
-    (star -south ok)
-    (star -west ok)
-    (star -east ok)))
+(spec direction [
+  [-north ok]
+  [-south ok]
+  [-west ok]
+  [-east ok]])
 
-(:: n (direction / checker))
-(def n
-  (const (star +north)))
+(:= n +north)
+(:: n direction)
 
-(spec result
-  (const
-    (star (-ok X) ok)
-    (star (-error X) ok)))
+(spec result [
+  [(-ok X) ok]
+  [(-error X) ok]])
 
-(:: x (result / checker))
-(def x
-  (const (star (+ok a))))
+(:= x (+ok a))
+(:: x result)
 
 'pattern matching
-(def get_ok
-  (const
-    (star (-ok X) X)
-    (star (-error X) (+error X))))
+(:= get_ok [
+  [(-ok X) X]
+  [(-error X) (+error X)]])
 
-(show-exec (union #get_ok @#x))
+<show exec (union #get_ok @#x)>