Syntax fix and improvement

README.md

@@ -36,29 +36,21 @@ philosophy).
 Finite state machine
 
 ```
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec binary {
   [(-i []) ok]
   [(-i [0|X]) (+i X)]
   [(-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
@@ -77,17 +69,17 @@ automaton accepting words ending with 00
 
 (:= kill (-a _ _))
 
-<show exec { @(exec { @#e #a1 }) #kill }>
-<show exec { @(exec { @#000 #a1 }) #kill }>
-<show exec { @(exec { @#010 #a1 }) #kill }>
-<show exec { @(exec { @#110 #a1 }) #kill }>
+(show (process (interact @#e #a1)   #kill))
+(show (process (interact @#000 #a1) #kill))
+(show (process (interact @#010 #a1) #kill))
+(show (process (interact @#110 #a1) #kill))
 ```
 
 More examples can be found in `examples/`.
 
 ## Learn
 
-This project is still in (chaotic) development, hence the syntax and features
+This project is still in development, hence the syntax and features
 are still changing frequently.
 
 To learn more about the current implementation of stellogen:

bin/sgen.ml

@@ -13,9 +13,19 @@ let parse input_file =
 let run input_file =
   let expr = parse input_file in
   let preprocessed = Expr.preprocess expr in
-  let p = Expr.program_of_expr preprocessed in
-  let _ = Stellogen.Sgen_eval.eval_program p in
-  ()
+  match Expr.program_of_expr preprocessed with
+  | Ok p ->
+    let _ = Stellogen.Sgen_eval.eval_program p in
+    ()
+  | Error e ->
+    let open Stellogen.Sgen_eval in
+    begin
+      match pp_err (ExprError e) with
+      | Ok pp ->
+        Out_channel.output_string Out_channel.stderr pp;
+        ()
+      | Error _ -> ()
+    end
 
 let preprocess_only input_file =
   let expr = parse input_file in

examples/automata.sg

@@ -1,26 +1,18 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec binary {
   [(-i []) ok]
   [(-i [0|X]) (+i X)]
   [(-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])
@@ -39,7 +31,7 @@ automaton accepting words ending with 00
 
 (:= kill (-a _ _))
 
-<show exec { @(exec { @#e #a1 }) #kill }>
-<show exec { @(exec { @#000 #a1 }) #kill }>
-<show exec { @(exec { @#010 #a1 }) #kill }>
-<show exec { @(exec { @#110 #a1 }) #kill }>
+(show (process (interact @#e #a1)   #kill))
+(show (process (interact @#000 #a1) #kill))
+(show (process (interact @#010 #a1) #kill))
+(show (process (interact @#110 #a1) #kill))

examples/binary4.sg

@@ -1,38 +1,46 @@
-(spec u4 [(-b _ 1 _) (-b _ 2 _) (-b _ 3 _) (-b _ 4 _) ok])
-
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec (process #Test #Tested)) ok))
+  (== @(interact (process #Test #Tested)) ok))
+
+(spec u4 [(-b _ 1 _) (-b _ 2 _) (-b _ 3 _) (-b _ 4 _) ok])
 
 (:= (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)])
 
-'''
-'FIXME
-
-(:= (and AA BB RR) {
-  #(if AA = 0 and BB = XX then RR = 0)
-  #(if AA = 1 and BB = XX then RR = XX) })
-(show #(and b1 b2 r1))
-(show (process #b1 #(and b1 b2 r1) #b2))
+(:= (and A B R) {
+  #(if A = 0 and B = _ then R = 0)
+  #(if A = 1 and B = X then R = X) })
+(:= rand (process #b1 #(and b1 b2 r) #b2))
+(show #rand)
+(== #rand #(make_bin r 0 0 0 1))
 
 (:= (or A B R) {
-  [(-b A I 0) (-b B I X) (+b R I X)]
-  [(-b A I 1) (-b B I X) (+b R I 1)]})
-
-(:= (xor A B R) {
-  [(-b A I 1) (-b B I 0) (+b R I 1)]
-  [(-b A I 0) (-b B I 1) (+b R I 1)]
-  [(-b A I 0) (-b B I 0) (+b R I 0)]
-  [(-b A I 1) (-b B I 1) (+b R I 0)]})
+  #(if A = 0 and B = X then R = X)
+  #(if A = 1 and B = Y then R = 1) })
+(:= ror (process #b1 #(or b1 b2 r) #b2))
+(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)
+
+'''
+(:= rxor (process #rnand #(and r2 r r3) #ror))
+(show #rxor)
 '''

examples/circuits.sg

@@ -8,7 +8,7 @@ FIXME
   [(+not 1 0)] [(+not 0 1)]
   [(+and 1 X X)][(+and 0 X 0)]})
 
-<show exec (process
+<show interact (process
   'inputs
   [(-1 X) (+c0 X)]
   'layer 1
@@ -21,7 +21,7 @@ FIXME
   [(-c4 R) R]
   #semantics)>
 
-<show exec (process
+<show interact (process
   'inputs
   {
     [(-0 X) (+c0 X)]

examples/lambda.sg

@@ -7,7 +7,7 @@
   [(-id X) (-arg X)]
   @[(+arg [r|X]) (out X)]})
 
-<show exec { #id #id_arg #linker }>
+(show (interact #id #id_arg #linker))
 
 ' id x
 (:= var_x [(x (exp X Y)) (+arg (exp [l|X] Y))])
@@ -16,7 +16,7 @@
   [(-id X) (-arg X)]
   @[(+arg [r|X]) (out X)]})
 
-<show exec { #id #var_x #linker }>
+(show (interact #id #var_x #linker))
 
 ' lproj x
 (:= lproj {

examples/linear_lambda.sg

@@ -1,5 +1,6 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { #Tested #Test }) ok))
+  (== @(interact #Tested #Test) ok))
 
 ' identity function (\x -> x)
 (:= id [(+id [l|X]) (+id [r|X])])
@@ -11,7 +12,7 @@
   [(-id X) (-arg X)]
   @[(+arg [r|X]) (out X)]])
 
-<show exec { #id #id_arg #linker }>
+(show (interact #id #id_arg #linker))
 
 ' id x
 (:= x_arg [(x X) (+arg [l X])])
@@ -20,7 +21,7 @@
   [(-id X) (-arg X)]
   @[(+arg [r|X]) (out X)]])
 
-<show exec { #id #x_arg #linker }>
+(show (interact #id #x_arg #linker))
 
 ' linear types
 (spec (larrow a a) {

examples/mall.sg

@@ -9,6 +9,6 @@
 
 (:= cut [(-5 X) (-3 X)])
 
-<show exec (process
+<show interact (process
   #with
   { #plus #cut })>

examples/mll.sg

@@ -1,5 +1,6 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { #Tested #Test }) ok))
+  (== @(interact #Tested #Test) ok))
 
 ' test of linear identity
 (spec (larrow a a) {
@@ -42,17 +43,17 @@
   [+cuts [
     [(-7 X) (-8 X)]]]})
 
-(:= vehicle <eval exec { #ps1 @[-vehicle] }>)
-(:= cuts    <eval exec { #ps1 @[-cuts] }>)
+(:= vehicle (eval (interact #ps1 @[-vehicle])))
+(:= cuts    (eval (interact #ps1 @[-cuts])))
 
-<show exec { #vehicle #cuts }>
+(show (interact #vehicle #cuts))
 
 (spec (tens a b) {
   [(-1 [g|X]) (-2 [g|X]) (+3 [g|X])]
   @[(-3 [g|X]) ok]})
 
 (new-declaration (::lin Tested Test)
-  (== @(linexec { #Tested #Test }) ok))
+  (== @(fire #Tested #Test) ok))
 
 ' does not typecheck
 ' (::lin vehicle ((tens a a) linear))

examples/nat.sg

@@ -1,25 +1,21 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec nat {
   [(-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))])
 
 (:= is_empty {
   [(-nat 0) (res 1)]
   [(-nat (s _)) (res 0)]})
 
-<show exec { @#add1 #2 }>
-<show exec { #is_empty @#0 }>
-<show exec { #is_empty @#1 }>
+(show (interact @#add1 #2))
+(show (interact #is_empty @#0))
+(show (interact #is_empty @#1))

examples/npda.sg

@@ -1,23 +1,17 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec binary {
   [(-i []) ok]
   [(-i [0|X]) (+i X)]
   [(-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])
@@ -37,7 +31,7 @@
 
 (:= kill (-a _ _ _))
 
-<show exec { @(exec { @#e #a1 }) #kill }>
-<show exec { @(exec { @#0000 #a1 }) #kill }>
-<show exec { @(exec { @#0110 #a1 }) #kill }>
-<show exec { @(exec { @#1110 #a1 }) #kill }>
+(show (process (interact @#e #a1)    #kill))
+(show (process (interact @#0000 #a1) #kill))
+(show (process (interact @#0110 #a1) #kill))
+(show (process (interact @#1110 #a1) #kill))

examples/prolog.sg

@@ -6,7 +6,7 @@
 ' 2 + 2 = R
 (:= query [(-add <s s 0> <s s 0> R) R])
 
-<show exec { #add @#query }>
+(show (interact #add @#query))
 
 (:= graph {
   [(+from 1) (+to 2)]
@@ -22,6 +22,6 @@
   @[(-from 1)]
   [(-to 4) ok]})
 
-<show exec (process
+<show interact (process
   #query
   { #graph #composition })>

examples/stack.sg

@@ -1,4 +1,4 @@
-<show exec (process
+<show interact (process
   (+stack0 [])
   'push 1 then 0
   [(-stack0 X) (+stack1 [1|X])]