Use S-expressions

README.md

@@ -9,15 +9,15 @@ It has been designed from concepts of Girard's transcendental syntax.
 
 ## Key characteristics
 
-- dynamically/statically **typed** but without primitive types nor type systems,
-by using very flexible assert-like expressions defining *sets of tests* to pass;
-- everything is based on **term unification**.
+- **typable** but without primitive types nor type systems
+- both computation and typing are based on basic **term unification** between
+blocks of terms.
 
 It is multi-paradigm:
-- _logic programs_ called "constellations" are the elementary bricks of
-computation and typing;
-- _functional programs_ correspond to logic programs enforcing an order of
-interaction;
+- _logic programs_ called "constellations" are the elementary blocks of
+programming;
+- _functional programs_ correspond to layered constellations enforcing an order
+of interaction;
 - _imperative programs_ are iterative recipes constructing constellations;
 - _objects_ are ways to structure constellations.
 
@@ -28,7 +28,6 @@ It draws (or try to draw) inspiration from:
 - Smalltalk (for message-passing, object-oriented paradigm and minimalism);
 - Coq (for proof-as-program paradigm and iterative programming with tactics);
 - Scheme/Racket (for minimalism and metaprogramming);
-- Haskell/Ruby/Lua (for syntax);
 - Shen (for its optional type systems and its "power and responsibility"
 philosophy).
 
@@ -37,39 +36,49 @@ philosophy).
 Finite state machine
 
 ```
-spec binary =
-  -i(e) ok;
-  -i(0:X) +i(X);
-  -i(1:X) +i(X).
+(new-declaration (:: Tested Test)
+  (== @(exec { @#Tested #Test }) ok))
 
-e :: binary.
-e = +i(e).
+(spec binary {
+  [(-i []) ok]
+  [(-i [0|X]) (+i X)]
+  [(-i [1|X]) (+i X)]})
 
-000 :: binary.
-000 = +i(0:0:0:e).
+'input words
+(:= e (+i []))
+(:: e binary)
 
-010 :: binary.
-010 = +i(0:1:0:e).
+(:= 0 (+i [0]))
+(:: 0 binary)
 
-110 :: binary.
-110 = +i(1:1:0:e).
+(:= 000 (+i [0 0 0]))
+(:: 000 binary)
 
-a1 = galaxy
-  initial =
-    -i(W) +a(W q0).
-  final =
-    -a(e q2) accept.
-  transitions =
-    -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).
-end
+(:= 010 (+i [0 1 0]))
+(:: 010 binary)
 
-show process #e.   #a1. &kill. end
-show process #000. #a1. &kill. end
-show process #010. #a1. &kill. end
-show process #110. #a1. &kill. end
+(:= 110 (+i [1 1 0]))
+(:: 110 binary)
+
+'''
+automaton accepting words ending with 00
+'''
+(:= (initial Q) [(-i W) (+a W Q)])
+(:= (accept Q) [(-a [] Q) accept])
+(:= (if read C1 on Q1 then Q2) [(-a [C1|W] Q1) (+a W Q2)])
+
+(:= a1 {
+  #(initial q0)
+  #(accept q2)
+  #(if read 0 on q0 then q0)
+  #(if read 0 on q0 then q1)
+  #(if read 1 on q0 then q0)
+  #(if read 0 on q1 then q2)})
+
+<show kill exec { @#e #a1 }>
+<show kill exec { @#000 #a1 }>
+<show kill exec { @#010 #a1 }>
+<show kill exec { @#110 #a1 }>
 ```
 
 More examples can be found in `examples/`.

bin/dune

@@ -1,7 +1,7 @@
 (executables
- (public_names lsc sgen isgen)
- (names lscrun sgen isgen)
- (libraries lsc stellogen base cmdliner))
+ (public_names sgen)
+ (names sgen)
+ (libraries stellogen base cmdliner))
 
 (env
  (dev

bin/sgen.ml

@@ -1,35 +1,35 @@
 open Base
 open Cmdliner
-open Stellogen.Sgen_eval
+open Stellogen
 
-let parse_and_eval input_file typecheckonly notyping =
+let parse_and_eval input_file =
   let lexbuf = Sedlexing.Utf8.from_channel (Stdlib.open_in input_file) in
   let start_pos filename =
     { Lexing.pos_fname = filename; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 }
   in
   Sedlexing.set_position lexbuf (start_pos input_file);
-  let p = Stellogen.Sgen_parsing.parse_with_error lexbuf in
-  let _ = eval_program ~typecheckonly ~notyping p in
+  let expr = Sgen_parsing.parse_with_error lexbuf in
+  let preprocessed = Expr.preprocess expr in
+  Stdlib.print_string
+    (List.map ~f:Expr.to_string preprocessed |> String.concat ~sep:"\n");
+  Stdlib.print_newline ();
+  Stdlib.print_string "----------------";
+  Stdlib.flush Stdlib.stdout;
+  let p = Expr.program_of_expr preprocessed in
+  Stdlib.print_string "\n";
+  let _ = Stellogen.Sgen_eval.eval_program p in
   ()
 
 let input_file_arg =
   let doc = "Input file to process." in
   Arg.(required & pos 0 (some string) None & info [] ~docv:"FILENAME" ~doc)
 
-let typecheckonly_flag =
-  let doc = "Only perform typechecking." in
-  Arg.(value & flag & info [ "typecheck-only" ] ~doc)
-
-let notyping_flag =
-  let doc = "Perform execution without typing." in
-  Arg.(value & flag & info [ "no-typing" ] ~doc)
-
 let term =
   let open Term in
-  const (fun input_file typecheckonly notyping ->
-    try Ok (parse_and_eval input_file typecheckonly notyping)
+  const (fun input_file ->
+    try Ok (parse_and_eval input_file)
     with e -> Error (`Msg (Stdlib.Printexc.to_string e)) )
-  $ input_file_arg $ typecheckonly_flag $ notyping_flag |> term_result
+  $ input_file_arg |> term_result
 
 let cmd = Cmd.v (Cmd.info "sgen" ~doc:"Run the Stellogen program.") term
 

examples/automata.sg

@@ -1,37 +1,43 @@
-spec binary =
-  -i(e) ok;
-  -i(0:X) +i(X);
-  -i(1:X) +i(X).
+(new-declaration (:: Tested Test)
+  (== @(exec { @#Tested #Test }) ok))
+
+(spec binary {
+  [(-i []) ok]
+  [(-i [0|X]) (+i X)]
+  [(-i [1|X]) (+i X)]})
 
 'input words
-e :: binary.
-e = +i(e).
+(:= e (+i []))
+(:: e binary)
+
+(:= 0 (+i [0]))
+(:: 0 binary)
 
-000 :: binary.
-000 = +i(0:0:0:e).
+(:= 000 (+i [0 0 0]))
+(:: 000 binary)
 
-010 :: binary.
-010 = +i(0:1:0:e).
+(:= 010 (+i [0 1 0]))
+(:: 010 binary)
 
-110 :: binary.
-110 = +i(1:1:0:e).
+(:= 110 (+i [1 1 0]))
+(:: 110 binary)
 
 '''
 automaton accepting words ending with 00
 '''
-a1 = galaxy
-  initial =
-    -i(W) +a(W q0).
-  final =
-    -a(e q2) accept.
-  transitions =
-    -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).
-end
-
-show process #e.   #a1. &kill. end
-show process #000. #a1. &kill. end
-show process #010. #a1. &kill. end
-show process #110. #a1. &kill. end
+(:= (initial Q) [(-i W) (+a W Q)])
+(:= (accept Q) [(-a [] Q) accept])
+(:= (if read C1 on Q1 then Q2) [(-a [C1|W] Q1) (+a W Q2)])
+
+(:= a1 {
+  #(initial q0)
+  #(accept q2)
+  #(if read 0 on q0 then q0)
+  #(if read 0 on q0 then q1)
+  #(if read 1 on q0 then q0)
+  #(if read 0 on q1 then q2)})
+
+<show kill exec { @#e #a1 }>
+<show kill exec { @#000 #a1 }>
+<show kill exec { @#010 #a1 }>
+<show kill exec { @#110 #a1 }>

examples/binary4.sg

@@ -1,54 +1,48 @@
-spec u4 = -b(1 _) -b(2 _) -b(3 _) -b(4 _) ok.
+'''
+(spec u4 [(-b 1 _) (-b 2 _) (-b 3 _) (-b 4 _) ok])
 
-checker = galaxy
-  interaction =
-    process
-      #test.
-      #tested[b=>+b].
-    end
-  expect = ok.
-end
+(new-declaration (:: tested test)
+  (:= test @(exec (process #test #test{b=>+b})))
+  (== test ok))
 
-b1 :: u4 [checker].
-b1 = b(1 1); b(2 0); b(3 0); b(4 1).
+(:= b1 [ [(b 1 1)] [(b 2 0)] [(b 3 0)] [(b 4 1)]])
+(:: b1 u4)
 
-b1 :: u4 [checker].
-b2 = b(1 0); b(2 0); b(3 1); b(4 1).
+(:= b2 [ [(b 1 0)] [(b 2 0)] [(b 3 1)] [(b 4 1)]])
+(:: b1 u4)
 
-and =
-  -b1(arg 0) -b2(arg X) b(arg 0);
-  -b1(arg 1) -b2(arg X) b(arg X).
+(:= and [
+  [(-b1 arg 0) (-b2 arg X) (b arg 0)]
+  [(-b1 arg 1) (-b2 arg X) (b arg X)]])
 
-or =
-  -b1(arg 0) -b2(arg X) b(arg X);
-  -b1(arg 1) -b2(arg X) b(arg 1).
+(:= or [
+  [(-b1 arg 0) (-b2 arg X) (b arg X)]
+  [(-b1 arg 1) (-b2 arg X) (b arg 1)]])
 
-xor =
-  -b1(arg 1) -b2(arg 0) b(arg 1);
-  -b1(arg 0) -b2(arg 1) b(arg 1);
-  -b1(arg 0) -b2(arg 0) b(arg 0);
-  -b1(arg 1) -b2(arg 1) b(arg 0).
+(:= xor [
+  [(-b1 arg 1) (-b2 arg 0) (b arg 1)]
+  [(-b1 arg 0) (-b2 arg 1) (b arg 1)]
+  [(-b1 arg 0) (-b2 arg 0) (b arg 0)]
+  [(-b1 arg 1) (-b2 arg 1) (b arg 0)]])
 
 'logical AND
-show-exec process
-  #b1[b=>+b1].
-  #and[arg=>1]. #and[arg=>2]. #and[arg=>3]. #and[arg=>4].
-  #b2[b=>+b2].
-  &kill.
-end
+<show exec (process
+  #b1{b=>+b1}
+  #and{arg=>1} #and{arg=>2} #and{arg=>3} #and{arg=>4}
+  #b2{b=>+b2}
+  kill)>
 
 'logical OR
-show-exec process
-  #b1[b=>+b1].
-  #or[arg=>1]. #or[arg=>2]. #or[arg=>3]. #or[arg=>4].
-  #b2[b=>+b2].
-  &kill.
-end
+<show exec (process
+  #b1{b=>+b1}
+  #or{arg=>1} #or{arg=>2} #or{arg=>3} #or{arg=>4}
+  #b2{b=>+b2}
+  kill)>
 
 'logical XOR
-show-exec process
-  #b1[b=>+b1].
-  #xor[arg=>1]. #xor[arg=>2]. #xor[arg=>3]. #xor[arg=>4].
-  #b2[b=>+b2].
-  &kill.
-end
+<show exec (process
+  #b1{b=>+b1}
+  #xor{arg=>1} #xor{arg=>2} #xor{arg=>3} #xor{arg=>4}
+  #b2{b=>+b2}
+  kill)>
+  '''