diff --git a/README.md b/README.md
index 5c2f586..9d15f22 100644
--- a/README.md
+++ b/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/`.
diff --git a/bin/dune b/bin/dune
index d04003a..1d3a4fc 100644
--- a/bin/dune
+++ b/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
diff --git a/bin/lscrun.ml b/bin/lscrun.ml
deleted file mode 100644
index 71d299b..0000000
--- a/bin/lscrun.ml
+++ /dev/null
@@ -1,62 +0,0 @@
-open Base
-open Cmdliner
-open Lsc.Lsc_ast
-open Lsc.Lsc_err
-open Out_channel
-
-let parse_and_eval input_file unfincomp linear showtrace =
-  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 lexer = Sedlexing.with_tokenizer Lsc.Lsc_lexer.read lexbuf in
-  let parser =
-    MenhirLib.Convert.Simplified.traditional2revised
-      Lsc.Lsc_parser.constellation_file
-  in
-  let mcs = parser lexer in
-  let result =
-    match exec ~linear ~showtrace mcs with
-    | Ok result -> result
-    | Error e ->
-      pp_err_effect e |> Out_channel.output_string Out_channel.stderr;
-      Stdlib.exit 1
-  in
-  if not showtrace then
-    result
-    |> (if unfincomp then kill else Fn.id)
-    |> string_of_constellation |> Stdlib.print_endline
-  else output_string stdout "No interaction left.\n"
-
-let input_file_arg =
-  let doc = "Input file to process." in
-  Arg.(required & pos 0 (some string) None & info [] ~docv:"FILENAME" ~doc)
-
-let unfincomp_flag =
-  let doc =
-    "Show stars containing polarities which are left after execution\n\n\
-    \    (they correspond to unfinished computation and are omitted by \
-     default)."
-  in
-  Arg.(value & flag & info [ "unfincomp" ] ~doc)
-
-let showtrace_flag =
-  let doc = "Interactively show steps of selection and unification." in
-  Arg.(value & flag & info [ "showtrace" ] ~doc)
-
-let linear_flag =
-  let doc = "Actions which are used are consummed." in
-  Arg.(value & flag & info [ "linear" ] ~doc)
-
-let term =
-  let open Term in
-  const (fun input_file unfincomp showtrace linear ->
-    try Ok (parse_and_eval input_file unfincomp showtrace linear)
-    with e -> Error (`Msg (Stdlib.Printexc.to_string e)) )
-  $ input_file_arg $ unfincomp_flag $ showtrace_flag $ linear_flag
-  |> term_result
-
-let cmd = Cmd.v (Cmd.info "sgen" ~doc:"Run the Stellogen program.") term
-
-let () = Stdlib.exit (Cmd.eval cmd)
diff --git a/bin/sgen.ml b/bin/sgen.ml
index de6859e..856d342 100644
--- a/bin/sgen.ml
+++ b/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
 
diff --git a/examples/automata.sg b/examples/automata.sg
index c001932..bced06e 100644
--- a/examples/automata.sg
+++ b/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 }>
diff --git a/examples/binary4.sg b/examples/binary4.sg
index f921b50..ed59e98 100644
--- a/examples/binary4.sg
+++ b/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)>
+  '''
diff --git a/examples/circuits.sg b/examples/circuits.sg
index 0ba4c45..4aac685 100644
--- a/examples/circuits.sg
+++ b/examples/circuits.sg
@@ -1,41 +1,39 @@
 '''
 FIXME
 '''
+(:= semantics {
+  [(+1 1)]
+  [(+0 0)]
+  [(+s X X X)]
+  [(+not 1 0)] [(+not 0 1)]
+  [(+and 1 X X)][(+and 0 X 0)]})
 
-semantics =
-  +1(1);
-  +0(0);
-  +s(X X X);
-  +not(1 0); +not(0 1);
-  +and(1 X X); +and(0 X 0).
-
-show-exec process
+<show exec (process
   'inputs
-    -1(X) +c0(X).
+  [(-1 X) (+c0 X)]
   'layer 1
-    -c0(X) -s(X Y Z) +c1(Y) +c2(Z).
+  [(-c0 X) (-s X Y Z) (+c1 Y) (+c2 Z)]
   'layer 2
-    -c1(X) -not(X R) +c3(R).
+  [(-c1 X) (-not X R) (+c3 R)]
   'layer 3
-    -c2(X) -c3(Y) -and(X Y R) +c4(R).
+  [(-c2 X) (-c3 Y) (-and X Y R) (+c4 R)]
   'output
-    -c4(R) R.
-    #semantics.
-  '&kill.
-end
+  [(-c4 R) R]
+  #semantics)>
 
-show-exec process
+<show exec (process
   'inputs
-    -0(X) +c0(X);
-    -0(X) +c1(X).
+  {
+    [(-0 X) (+c0 X)]
+    [(-0 X) (+c1 X)]}
   'layer 1
-    -c0(X) -not(X R) +c2(R);
-    -c1(X) -not(X R) +c3(R).
+  {
+    [(-c0 X) (-not X R) (+c2 R)]
+    [(-c1 X) (-not X R) (+c3 R)]}
   'layer 2
-    -c2(X) -c3(Y) -and(X Y R) +c4(R).
+  {(-c2 X) (-c3 Y) (-and X Y R) (+c4 R)}
   'output
-    -c4(R) R.
+  [(-c4 R) R]
   'apply semantics
-    #semantics.
-  '&kill.
-end
+    #semantics)>
+  '&kill
diff --git a/examples/lambda.sg b/examples/lambda.sg
index 70f2d4f..c379e9a 100644
--- a/examples/lambda.sg
+++ b/examples/lambda.sg
@@ -1,18 +1,28 @@
-''' id id '''
-id = +id(exp(l:X d)) +id(r:X).
-id_arg = ida(exp(l:X Y)) +arg(exp(l:r:X Y)).
-linker = -id(X) -arg(X); @+arg(r:X) out(X).
-show-exec id id_arg linker.
-
-''' id x '''
-var_x = x(exp(X Y)) +arg(exp(l:X Y)).
-linker = -id(X) -arg(X); @+arg(r:X) out(X).
-show-exec id var_x linker.
-
-''' lproj x '''
-lproj =
-  +lproj(l:X); 'weakening
-  lproj(exp(r:l:X d)) +lproj(r:r:X).
-
-linker = -lproj(X) -arg(X); @+arg(r:X) out(X).
-show-exec lproj var_x linker.
+' id id
+(:= id [(+id (exp [l|X] d)) (+id [r|X])])
+
+(:= id_arg [(ida (exp [l|X] Y)) (+arg (exp [l r|X] Y))])
+
+(:= linker {
+  [(-id X) (-arg X)]
+  @[(+arg [r|X]) (out X)]})
+
+<show exec { #id #id_arg #linker }>
+
+' id x
+(:= var_x [(x (exp X Y)) (+arg (exp [l|X] Y))])
+
+(:= linker {
+  [(-id X) (-arg X)]
+  @[(+arg [r|X]) (out X)]})
+
+<show exec { #id #var_x #linker }>
+
+' lproj x
+(:= lproj {
+  [(+lproj [l|X])] 'weakening
+  [(lproj (exp [r l|X] d)) (+lproj [r r|X])]})
+
+(:= linker {
+  [(-lproj X) (-arg X)]
+  @[(+arg [r|X]) (out X)]})
diff --git a/examples/linear_lambda.sg b/examples/linear_lambda.sg
index f42bf26..7571cfb 100644
--- a/examples/linear_lambda.sg
+++ b/examples/linear_lambda.sg
@@ -1,32 +1,41 @@
-''' identity function (\x -> x) '''
-id = +id(l:X) +id(r:X).
-
-''' id id '''
-id_arg = ida(l:X) +arg(l:r:X).
-linker = -id(X) -arg(X); @+arg(r:X) out(X).
-show-exec #id #id_arg #linker.
-
-''' id x '''
-x_arg = x(X) +arg(l:X).
-linker = -id(X) -arg(X); @+arg(r:X) out(X).
-show-exec #id #x_arg #linker.
-
-''' linear types '''
-spec "a -o a" = galaxy
-  test1 =
-    -x(X) +parxy(X); -y(X);
-    @-parxy(X) ok.
-  test2 =
-    -x(X); -y(X) +parxy(X);
-    @-parxy(X) ok.
-end
-
-adapter = -id(l:X) +x(X); -id(r:X) +y(X).
-
-checker = galaxy
-  interaction = #tested #test.
-  expect = ok.
-end
-
-vehicle :: "a -o a" [checker].
-vehicle = #id #adapter.
+(new-declaration (:: Tested Test)
+  (== @(exec { #Tested #Test }) ok))
+
+' identity function (\x -> x)
+(:= id [(+id [l|X]) (+id [r|X])])
+
+' id id
+(:= id_arg [(ida [l|X]) (+arg [l r|X])])
+
+(:= linker [
+  [(-id X) (-arg X)]
+  @[(+arg [r|X]) (out X)]])
+
+<show exec { #id #id_arg #linker }>
+
+' id x
+(:= x_arg [(x X) (+arg [l X])])
+
+(:= linker [
+  [(-id X) (-arg X)]
+  @[(+arg [r|X]) (out X)]])
+
+<show exec { #id #x_arg #linker }>
+
+' linear types
+(spec (larrow a a) {
+  [+test1 [
+    [(-x X) (+parxy X)]
+    [(-y X)]
+    @[(-parxy X) ok]]]
+  [+test2 [
+    [(-x X)]
+    [(-y X) (+parxy X)]
+    @[(-parxy X) ok]]]})
+
+(:= adapter {
+  [(-id [l|X]) (+x X)]
+  [(-id [r|X]) (+y X)]})
+
+(:= vehicle { #id #adapter })
+'TODO (:: vehicle (larrow a a))
diff --git a/examples/mall.sg b/examples/mall.sg
index 1880fc6..c00dda6 100644
--- a/examples/mall.sg
+++ b/examples/mall.sg
@@ -1,12 +1,14 @@
-left = +5(l:l:X) +5(l:r:X)  | c:a.
-right = +5(r:l:X) +5(r:r:X) | c:b.
-
-with = #left #right.
-plus = +3(l:l:X) c(X); +3(l:r:X) d(X).
-cut = -5(X) -3(X).
-
-show-exec process
-  #with.
-  #plus #cut.
-  &kill.
-end
+(:= left  [(+5 [l l|X]) (+5 [l r|X]) || (slice c a)])
+(:= right [(+5 [r l|X]) (+5 [r r|X]) || (slice c b)])
+
+(:= with { #left #right })
+
+(:= plus {
+  [(+3 [l l|X]) (c X)]
+  [(+3 [l r|X]) (d X)]})
+
+(:= cut [(-5 X) (-3 X)])
+
+<show exec (process
+  #with
+  { #plus #cut })>
diff --git a/examples/mll.sg b/examples/mll.sg
index 3bd6fb4..ef72d90 100644
--- a/examples/mll.sg
+++ b/examples/mll.sg
@@ -1,61 +1,62 @@
-'''test of linear identity'''
-spec "a -o a" = galaxy
-  testrl =
-    -1(X) -2(X) +c5(X);
-    -3(X); -4(X) +c6(X);
-    -c5(X) +7(X); -c6(X);
-    @-7(X) ok.
-  testrr =
-    -1(X) -2(X) +c5(X);
-    -3(X); -4(X) +c6(X);
-    -c5(X); +7(X) -c6(X);
-    @-7(X) ok.
-  testll =
-    -1(X) -2(X) +c5(X);
-    -4(X); -3(X) +c6(X);
-    -c5(X) +7(X); -c6(X);
-    @-7(X) ok.
-  testlr =
-    -1(X) -2(X) +c5(X);
-    -4(X); -3(X) +c6(X);
-    -c5(X); +7(X) -c6(X);
-    @-7(X) ok.
-end
-
-checker = galaxy
-  interaction = #tested #test.
-  expect = ok.
-end
-
-id :: "a -o a" [checker].
-id =
-  -5(l:X) +1(X);
-  -5(r:X) +2(X);
-  -6(l:X) +3(X);
-  -6(r:X) +4(X);
-  +5(l:X) +6(l:X);
-  +5(r:X) +6(r:X).
-
-'''cut-elimination'''
-ps1 = galaxy
-  vehicle = +7(l:X) +7(r:X); 3(X) +8(l:X); @+8(r:X) 6(X).
-  cuts = -7(X) -8(X).
-end
-
-show-exec #ps1->vehicle #ps1->cuts.
-
-spec "a * b" =
-  -1(g:X) -2(g:X) +3(g:X);
-  @-3(g:X) ok.
-
-linear = galaxy
-  interaction = linear-exec #tested #test end.
-  expect = ok.
-end
-
-'does not typecheck
-'vehicle :: "a * a" [linear].
-vehicle =
-  +3(l:X) +3(r:X);
-  -3(l:X) +1(g:X);
-  -3(r:X) +2(g:X).
+(new-declaration (:: Tested Test)
+  (== @(exec { #Tested #Test }) ok))
+
+' test of linear identity
+(spec (larrow a a) {
+  [+testrl [
+    [(-1 X) (-2 X) (+c5 X)]
+    [(-3 X)] [(-4 X) (+c6 X)]
+    [(-c5 X) (+7 X)] [(-c6 X)]
+    @[(-7 X) ok]]]
+  [+testrr [
+    [(-1 X) (-2 X) (+c5 X)]
+    [(-3 X)] [(-4 X) (+c6 X)]
+    [(-c5 X)] [(+7 X) (-c6 X)]
+    @[(-7 X) ok]]]
+  [+testll [
+    [(-1 X) (-2 X) (+c5 X)]
+    [(-4 X)] [(-3 X) (+c6 X)]
+    [(-c5 X) (+7 X)] [(-c6 X)]
+    @[(-7 X) ok]]]
+  [+testlr [
+    [(-1 X) (-2 X) (+c5 X)]
+    [(-4 X)] [(-3 X) (+c6 X)]
+    [(-c5 X)] [(+7 X) (-c6 X)]
+    @[(-7 X) ok]]]})
+
+(:= id {
+  [(-5 [l|X]) (+1 X)]
+  [(-5 [r|X]) (+2 X)]
+  [(-6 [l|X]) (+3 X)]
+  [(-6 [r|X]) (+4 X)]
+  [(+5 [l|X]) (+6 [l|X])]
+  [(+5 [r|X]) (+6 [r|X])]})
+'TODO (:: id (larrow a a))
+
+'cut-elimination
+(:= ps1 {
+  [+vehicle [
+    [(+7 [l|X]) (+7 [r|X])]
+    @[(3 X) (+8 [l|X])]
+    [(+8 [r|X]) (6 X)]]]
+  [+cuts [
+    [(-7 X) (-8 X)]]]})
+
+(:= vehicle <eval exec { #ps1 @[-vehicle] }>)
+(:= cuts    <eval exec { #ps1 @[-cuts] }>)
+
+<show exec { #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))
+
+' does not typecheck
+' (::lin vehicle ((tens a a) linear))
+(:= vehicle {
+  [(+3 [l|X]) (+3 [r|X])]
+  [(-3 [l|X]) (+1 [g|X])]
+  [(-3 [r|X]) (+2 [g|X])]})
diff --git a/examples/nat.sg b/examples/nat.sg
index 470a0c5..bc609b7 100644
--- a/examples/nat.sg
+++ b/examples/nat.sg
@@ -1,35 +1,25 @@
-spec nat = -nat(0) ok; -nat(s(N)) +nat(N).
+(new-declaration (:: Tested Test)
+  (== @(exec { @#Tested #Test }) ok))
 
-checker = galaxy
-  interaction = @#tested #test.
-  expect = ok.
-end
+(spec nat {
+  [(-nat 0) ok]
+  [(-nat (s N)) (+nat N)]})
 
-fchecker = galaxy
-  interaction = @#tested #test.
-  expect = arg out.
-end
+(:= 0 (+nat 0))
+(:: 0 nat)
 
-spec "nat -> nat" =
-  +nat(X) arg;
-  -nat(X) out.
+(:= 1 (+nat (s 0)))
+(:: 1 nat)
 
-0 :: nat [checker].
-0 = +nat(0).
+(:= 2 <+nat s s 0>)
+(:: 2 nat)
 
-1 :: nat [checker].
-1 = +nat(s(0)).
+(:= add1 [(-nat X) (+nat (s X))])
 
-2 :: nat [checker].
-2 = +nat(s(s(0))).
+(:= is_empty {
+  [(-nat 0) (res 1)]
+  [(-nat (s _)) (res 0)]})
 
-add1 :: "nat -> nat" [fchecker].
-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 exec { @#add1 #2 }>
+<show exec { #is_empty @#0 }>
+<show exec { #is_empty @#1 }>
diff --git a/examples/npda.sg b/examples/npda.sg
index e3f90ce..021736e 100644
--- a/examples/npda.sg
+++ b/examples/npda.sg
@@ -1,36 +1,41 @@
-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).
-
-0000 :: binary.
-0000 = +i(0:0:0:0:e).
-
-0110 :: binary.
-0110 = +i(0:1:1:0:e).
-
-1110 :: binary.
-1110 = +i(1:1:1:0:e).
-
-a1 = galaxy
-  initial =
-    -i(W) +a(W e q0).
-  final =
-    -a(e e q0) accept;
-    -a(e e 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).
-end
-
-show process #e.    #a1. &kill. end
-show process #0000. #a1. &kill. end
-show process #0110. #a1. &kill. end
-show process #1110. #a1. &kill. end
+(:= 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])
+(:= (if read C1 on Q1 then Q2 and push C2) [(-a [C1|W] S Q1) (+a W [C2|S] Q2)])
+(:= (if read C1 with C2 on Q1 then Q2) [(-a [C1|W] [C2|S] Q1) (+a W S Q2)])
+(:= (if on Q1 then Q2) [(-a W S Q1) (+a W S Q2)])
+
+(:= a1 {
+  #(initial q0)
+  #(accept q0)
+  #(accept q1)
+  #(if read 0 on q0 then q0 and push 0)
+  #(if read 1 on q0 then q0 and push 1)
+  #(if on q0 then q1)
+  #(if read 0 with 0 on q1 then q1)
+  #(if read 1 with 1 on q1 then q1)})
+
+<show kill exec { @#e #a1 }>
+<show kill exec { @#0000 #a1 }>
+<show kill exec { @#0110 #a1 }>
+<show kill exec { @#1110 #a1 }>
diff --git a/examples/prolog.sg b/examples/prolog.sg
index 57ec01f..220a0a9 100644
--- a/examples/prolog.sg
+++ b/examples/prolog.sg
@@ -1,29 +1,27 @@
 ' unary addition
-add =
-  +add(0 Y Y);
-  -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
-query = -add(s(s(0)) s(s(0)) R) R.
+(:= query [(-add <s s 0> <s s 0> R) R])
 
-show-exec #add @#query.
+<show exec { #add @#query }>
 
-graph =
-  +from(1) +to(2);
-  +from(1) +to(3);
-  +from(3) +to(2);
-  +from(3) +to(4).
-  '+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)]})
 
-composition = -to(X) -from(X).
+(:= composition [(-to X) (-from X)])
 
 ' is there a path between 1 and 4?
-query =
-  @-from(1);
-  -to(4) ok.
+(:= query {
+  @[(-from 1)]
+  [(-to 4) ok]})
 
-show-exec process
-  #query.
-  #graph #composition.
-  &kill.
-end
+<show exec (process
+  #query
+  { #graph #composition })>
diff --git a/examples/stack.sg b/examples/stack.sg
index c68f177..f44d55a 100644
--- a/examples/stack.sg
+++ b/examples/stack.sg
@@ -1,20 +1,18 @@
-show-exec process
-  +stack0(e).
+<show exec (process
+  (+stack0 [])
   'push 1 then 0
-  -stack0(X) +stack1(1:X).
-  -stack1(X) +stack2(0:X).
+  [(-stack0 X) (+stack1 [1|X])]
+  [(-stack1 X) (+stack2 [0|X])]
 
   'pop & save
-  -stack2(C:X) +stack3(X) +save(C).
+  [(-stack2 [C|X]) (+stack3 X) (+save C)]
 
   'conditional duplication
-  -stack3(0:X) +stack4(0:0:X);
-  -stack3(1:X) +stack4(1:1:X).
+  [(-stack3 [0|X]) (+stack4 [0 0|X])]
+  [(-stack3 [1|X]) (+stack4 [1 1|X])]
 
   'freeze information
-  -stack4(X) stack(X).
+  [(-save C) (save C)]
 
-  -save(C) save(C).
-  'kill remaining polarized stars
-  &kill.
-end
+  'clean
+  [(-stack4 _)])>
diff --git a/examples/sumtypes.sg b/examples/sumtypes.sg
index fb2f42a..b8ca74a 100644
--- a/examples/sumtypes.sg
+++ b/examples/sumtypes.sg
@@ -1,27 +1,25 @@
-checker = galaxy
-  interaction = @#tested #test.
-  expect = ok.
-end
+(new-declaration (:: Tested Test)
+  (== @(exec { @#Tested #Test }) ok))
 
-spec direction =
-  -north ok;
-  -south ok;
-  -west ok;
-  -east ok.
+(spec direction {
+  [-north ok]
+  [-south ok]
+  [-west ok]
+  [-east ok]})
 
-n :: direction [checker].
-n = +north.
+(:= n +north)
+(:: n direction)
 
-spec result =
-  -ok(X) ok;
-  -error(X) ok.
+(spec result {
+  [(-ok X) ok]
+  [(-error X) ok]})
 
-x :: result [checker].
-x = +ok(a).
+(:= x (+ok a))
+(:: x result)
 
 'pattern matching
-get_ok =
-  -ok(X) X;
-  -error(X) +error(X).
+(:= get_ok {
+  [(-ok X) X]
+  [(-error X) (+error X)]})
 
-show-exec #get_ok @#x.
+<show exec { #get_ok @#x }>
diff --git a/examples/syntax.sg b/examples/syntax.sg
index 7cec8d2..d36fa2c 100644
--- a/examples/syntax.sg
+++ b/examples/syntax.sg
@@ -1,113 +1,117 @@
-'static definition of constellation
-x = +a; -a b.
-y = #x.
-z = -f(X).
+'define ray
+(:= a (-f X))
 
-'string literals
-w = "hello world".
+'define star
+(:= b [(-f X)])
 
-'cons
-w = +w(0:1:0:1:e).
+'define constellation
+(:= c {
+  @[+a] 'focus
+  [-a b]})
 
 'full focus
-show-exec @#w #w.
+(:= f @{ [a] [b] [c] })
 
-'show (literal) contellations
-show a; b; c.
+'identifier
+(:= x #a)
 
-'print result of execution
-show-exec a; b; c.
-show exec a; b; c end.
+'group
+(:= x { #a #b })
 
-'inequality constraints
-ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.
+'string literals
+(:= s "hello world")
 
-'interactive debugging of execution
-'trace ineq.
+'cons
+' [0 1] == %cons(0 (%cons 1 %nil))
+(:= w (+w [0 1 0 1]))
 
-'dynamic definition of constellation
-c = process
-  +n0(0).           'base constellation
-  -n0(X) +n1(s(X)). 'interacts with previous
-  -n1(X) +n2(s(X)). 'interacts with previous
-end
+'stack
+' <s s 0> == (s (s 0))
+(:= n (+nat <s s 0>))
 
-'galaxy definition
-g = galaxy
-  test1 = +f(a) ok.
-  test2 = +f(b) ok.
-end
-show #g.
+'execution
+(:= x [(+f X) X])
+(:= y (-f a))
+(:= ex (linexec { @#x #y })) 'linear
+(:= ex (exec { @#x #y }))    'non-linear
 
-'reactive effects
-run +&print(X); -&print("hello world\n").
+'show constellation
+(show #ex)
+(show { [a] [b] [c] })
+(show #s)
 
-'access to field of a galaxy
-show #g->test1.
-show #g->test2.
+'complex identifiers
+(:= (f a b) [(function a b)])
+(show #(f a b))
+
+'inequality constraints
+(:= ineq {
+  [(+f a)]
+  [(+f b)]
+  @[(-f X) (-f Y) (r X Y) || (!= X Y)]})
+(show #ineq)
+<show exec #ineq>
+
+'interactive debugging of execution
+'(trace #ineq)
+
+'process
+(:= c (process
+  (+n0 0)                 'base constellation
+  [(-n0 X) (+n1 (s X))]   'interacts with previous
+  [(-n1 X) (+n2 (s X))])) 'interacts with previous
+(show #c)
+
+'constellation with fields
+(:= g {
+  [(+field test1) [(+f a) ok]]
+  [(+field test2) [(+f b) ok]]})
+(show #g)
+
+'field access and evaluation
+(:= (get G X) <eval exec { #G @[(-field X)] }>)
+(show #(get g test1))
+(show #(get g test2))
+
+'nested fields
+(:= g1 [
+  [(+field test1) [
+    [(+field test2) [(+f c) ok]]]]])
+(:= g2 <eval exec { #g1 @[(-field test1)] }>)
+<show eval exec { #g2 @[(-field test2)] }>
 
 'extend rays with a head function symbol
-show-exec (+f(X); f(X))[=>+a].
-show-exec (+f(X); f(X))[=>a].
+'<show exec [[(+f X)] [(f X)]][=>+a]>
+'<show exec [[(+f X)] [(f X)]][=>a]>
 
 'remove head function symbol from a ray
-show-exec (+f(X); f(X))[+f=>].
+'<show-exec [[(+f X)] [(f X)]][+f=>]>
 
 'substitutions
-show-exec (+f(X))[X=>+a(X)].
-show-exec (+f(X))[+f=>+g].
-show-exec (#1 #2)[#1=>+f(X) X][#2=>-f(a)].
-
-'checkers & typechecking
-checker = galaxy
-  interaction = (@#tested) #test.
-  expect = ok.
-end
-
-spec nat = galaxy
-  test =
-    -nat(0) ok;
-    -nat(s(N)) +nat(N).
-end
-
-0 :: nat [checker].
-0 = +nat(0).
-
-1 :: nat [checker].
-1 = +nat(s(0)).
-
-'plural typing
-nat2 = -nat(X) ok.
-2 :: nat.
-2 :: nat2.
-2 = +nat(s(s(0))).
-3 :: nat; nat2.
-3 = +nat(s(s(s(0)))).
-4 :: nat [checker]; nat2 [checker].
-4 = +nat(s(s(s(s(0))))).
-
-'galaxy with type declarations
-show galaxy
-  n1 :: nat.
-  n1 = +nat(0).
-  n2 :: nat.
-  n2 = +nat(s(s(0))).
-end
-
-interface nat_pair
-  n :: nat.
-  m :: nat.
-end
-
-g_pair :: nat_pair.
-g_pair = galaxy
-  n = +nat(0).
-  m = +nat(0).
-end
+'<show exec (+f X)[X=>(+a X)]>
+'<show exec (+f X)[+f=>+g]>
+'<show exec (union #1 #2)
+'  [#1=>[(+f X) X)]]
+'  [#2=>(-f a)]>
+
+'define type
+(spec nat {
+  [(-nat 0) ok]
+  [(-nat (s N)) (+nat N)]})
+
+'expect
+(:= x 0)
+(== #x 0)
+'(== x 1)
+
+'type checking
+(:= 2 <+nat s s 0>)
+(== @(exec { @#2 #nat }) ok)
 
 'import file
-'use examples->automata.
+'(use "examples/automata.sg")
 
-'complex identifiers
-f(a b) = function(a b).
-show #f(a b).
+'declaration definition
+(new-declaration (:: Tested Test)
+  (== @(exec { @#Tested #Test }) ok))
+(:: 2 nat)
diff --git a/examples/turing.sg b/examples/turing.sg
index 26f405f..dcdcadd 100644
--- a/examples/turing.sg
+++ b/examples/turing.sg
@@ -1,42 +1,40 @@
-'''
-Turing machine accepting words with as many 'a' as 'b'
-'''
-mt = galaxy
-  initial =
-    -i(C:W) +m(q0 e:e C W);
-    -i(e) +m(q0 e e e).
-  accept =
-    -m(q0 L e R) +m(qa L e R);
-    -m(qa L e R) accept.
-  initial_skip =
-    -m(q0 L sep C:R) +m(q0 sep:L C R).
-  mark =
-    -m(q0 L a C:R) +m(q2 sep:L C R);
-    -m(q0 L b C:R) +m(q3 sep:L C R).
-  skip =
-    -m(q2 L a C:R)   +m(q2 a:L C R);
-    -m(q2 L sep C:R) +m(q2 sep:L C R);
-    -m(q3 L b C:R)   +m(q3 b:L C R);
-    -m(q3 L sep C:R) +m(q3 sep:L C R).
-  join =
-    -m(q2 C:L b R) +m(q1 L C sep:R);
-    -m(q3 C:L a R) +m(q1 L C sep:R).
-  return =
-    -m(q1 C:L a R)   +m(q1 L C a:R);
-    -m(q1 C:L b R)   +m(q1 L C b:R);
-    -m(q1 C:L sep R) +m(q1 L C sep:R);
-    -m(q1 L e C:R)   +m(q0 e:L C R).
-  reject =
-    -m(q2 L e R) +m(qr L e R);
-    -m(q3 L e R) +m(qr L e R);
-    -m(qr L C R) reject.
-end
+' Turing machine accepting words with as many 'a' as 'b'
+(:= mt {
+  'initial
+  [(-i [C|W]) (+m q0 [e e] C W)]
+  [(-i [])    (+m q0 e e e)]
+  'accept
+  [(-m q0 L e R) (+m qa L e R)]
+  [(-m qa L e R) accept]
+  'initial skip
+  [(-m q0 L sep [C|R]) (+m q0 [sep|L] C R)]
+  'mark
+  [(-m q0 L a [C|R]) (+m q2 [sep|L] C R)]
+  [(-m q0 L b [C|R]) (+m q3 [sep|L] C R)]
+  'skip
+  [(-m q2 L a [C|R])   (+m q2 [a|L] C R)]
+  [(-m q2 L sep [C|R]) (+m q2 [sep|L] C R)]
+  [(-m q3 L b [C|R])   (+m q3 [b|L] C R)]
+  [(-m q3 L sep [C|R]) (+m q3 [sep|L] C R)]
+  'join
+  [(-m q2 [C|L] b R) (+m q1 L C [sep|R])]
+  [(-m q3 [C|L] a R) (+m q1 L C [sep|R])]
+  'return
+  [(-m q1 [C|L] a R)   (+m q1 L C [a|R])]
+  [(-m q1 [C|L] b R)   (+m q1 L C [b|R])]
+  [(-m q1 [C|L] sep R) (+m q1 L C [sep|R])]
+  [(-m q1 L e [C|R])   (+m q0 [e|L] C R)]
+  'reject
+  [(-m q2 L e R) (+m qr L e R)]
+  [(-m q3 L e R) (+m qr L e R)]
+  [(-m qr L C R) reject]})
 
-show process +i(a:e:e).       #mt. &kill. end
-show process +i(b:e:e).       #mt. &kill. end
-show process +i(a:b:b:e:e).   #mt. &kill. end
-show process +i(e:e).         #mt. &kill. end
-show process +i(a:b:e:e).     #mt. &kill. end
-show process +i(a:a:b:b:e:e). #mt. &kill. end
-show process +i(a:b:b:a:e:e). #mt. &kill. end
-show process +i(a:b:a:b:e:e). #mt. &kill. end
+<show kill exec { @(+i [a e e]) #mt}>
+<show kill exec { @(+i [b e e]) #mt}>
+<show kill exec { @(+i [a b b e e]) #mt}>
+
+<show kill exec { @(+i [e e]) #mt}>
+<show kill exec { @(+i [a b e e]) #mt}>
+<show kill exec { @(+i [a a b b e e]) #mt}>
+<show kill exec { @(+i [a b b a e e]) #mt}>
+<show kill exec { @(+i [a b a b e e]) #mt}>
diff --git a/exercises/00-unification.sg b/exercises/00-unification.sg
index 8cd02a8..a01c09c 100644
--- a/exercises/00-unification.sg
+++ b/exercises/00-unification.sg
@@ -1,22 +1,45 @@
 'fill the #your_answer holes with the correct result of execution
 
-x1 :=: #your_answer.
-x1 = @+f(X) X; -f(a).
+(== x1 #your_answer)
+(def x1
+  (const
+    (@star (+f X) X)
+    (star (-f a))))
 
-x2 :=: #your_answer.
-x2 = @+f(X); -f(Y) a.
+(== x2 #your_answer)
+(def x2
+  (const
+    (@star (+f X))
+    (star (-f Y) a)))
 
-x3 :=: #your_answer.
-x3 = @+f(X) X; -f(a); -f(b).
+(== x3 #your_answer)
+(def x3
+  (const
+    (@star (+f X) X)
+    (star (-f a))
+    (star (-f b))))
 
-x4 :=: #your_answer.
-x4 = @+1 -2; -2 +3.
+(== x4 #your_answer)
+(def x4
+  (const
+    (@star +1 -2)
+    (star -2 +3)))
 
-x5 :=: #your_answer.
-x5 = @-1 +2; -2 +1.
+(== x5 #your_answer)
+(def x5
+  (const
+    (@star -1 +2)
+    (star -2 +1)))
 
-x6 :=: #your_answer.
-x6 = @-1 +2; -2 +1.
+(== x6 #your_answer)
+(def x6
+  (const
+    (@star -1 +2)
+    (star -2 +1)))
 
-x7 :=: #your_answer.
-x7 = @-f(X) X; +f(+g(a)); -g(X) X.
+(== x7 #your_answer)
+(def x7
+  (const
+    (@star (-f X) X)
+    (star (+f (+g a)))
+    (star (-g X) X)))
diff --git a/exercises/01-paths.sg b/exercises/01-paths.sg
index 1a24a4b..9733e27 100644
--- a/exercises/01-paths.sg
+++ b/exercises/01-paths.sg
@@ -1,14 +1,32 @@
 'fill the 'your_answer' holes to replace #1 in the constellations
 'below such that the result of execution is { ok }
 
-x :=: { ok }.
+(== x1 (const (star ok)))
+(def x1
+  (union (const (@star -1 ok)) #1)
+  [#1=>#your_answer])
 
-x = ((-1 ok) #1)[#1=>your_answer].
+(== x2 (const (star ok)))
+(def x2
+  (union (const (@star -1) (star +2)) #1)
+  [#1=>#your_answer])
 
-x = ((-1; +2) #1)[#1=>your_answer].
+(== x3 (const (star ok)))
+(def x3
+  (union (const (@star -1 ok) (star -2 +3)) #1)
+  [#1=>#your_answer])
 
-x = ((-1 ok; -2 +3) #1)[#1=>your_answer].
+(== x4 (const (star ok)))
+(def x4
+  (union (const (@star (-f (+g X)) ok)) #1)
+  [#1=>#your_answer])
 
-x = ((-f(+g(X)) ok) #1)[#1=>your_answer].
-
-x = ((+f(a) +f(b); +g(a); @+g(b) ok) #1)[#1=>your_answer].
+(== x5 (const (star ok)))
+(def x5
+  (union
+    (const
+      (star (+f a) (+f b))
+      (star (+g a))
+      (@star (+g b) ok))
+    #1)
+  [#1=>#your_answer])
diff --git a/exercises/02-registers.sg b/exercises/02-registers.sg
index 887a445..17514e7 100644
--- a/exercises/02-registers.sg
+++ b/exercises/02-registers.sg
@@ -1,29 +1,28 @@
-show-exec process
+(show-exec (process
   'represents a register with value 0
-  +r0(0).
+  (const (star (+r0 0)))
 
   'update the value to 1
-  #your_answer.
-  #your_answer.
+  #your_answer
+  #your_answer
 
   'duplicate the register into two registers r1 and r2
-  #your_answer.
+  #your_answer
 
   'update r1 to 0
-  #your_answer.
-  #your_answer.
+  #your_answer
+  #your_answer
 
   'swap the value of r1 and r2
-  #your_answer.
-  #your_answer.
+  #your_answer
+  #your_answer
 
   'duplicate r1 and add a copy identifier as first argument
-  #your_answer.
+  #your_answer
 
   'update the two copies to 5 at once
-  #your_answer.
-  #your_answer.
+  #your_answer
+  #your_answer
 
   'duplicate each copy of r1 again with the same method
-  #your_answer.
-end
+  #your_answer))
diff --git a/exercises/03-boolean.sg b/exercises/03-boolean.sg
new file mode 100644
index 0000000..d4eff41
--- /dev/null
+++ b/exercises/03-boolean.sg
@@ -0,0 +1,84 @@
+'fill the #your_answer hole by following the specifications
+
+(def checker
+  (galaxy
+    (interaction (union #tested #test))
+    (expect (const (star ok)))))
+
+(def not_spec
+  (galaxy
+    (test0 (const (@star (-not 0 1) ok)))
+    (test1 (const (@star (-not 1 0) ok)))))
+
+(:: not (not_spec / checker))
+(def not
+  #your_asnwer)
+
+'how to print the truth table of NOT ?
+(== table_not (const
+  (star (table_not 0 1))
+  (star (table_not 1 0))))
+(def table_not
+  (union
+    #not
+    #your_answer))
+
+(def and_spec
+  (galaxy
+    (test00 (const (@star (-and 0 0 0) ok)))
+    (test01 (const (@star (-and 0 1 0) ok)))
+    (test10 (const (@star (-and 1 0 0) ok)))
+    (test11 (const (@star (-and 1 1 1) ok)))))
+
+(:: and (and_spec / checker))
+(def and
+  #your_answer)
+
+'find a second way to compute AND
+(:: and (and_spec / checker))
+(def and2
+  #your_answer)
+
+(def or_spec
+  (galaxy
+    (test00 (const (@star (-or 0 0 0) ok)))
+    (test01 (const (@star (-or 0 1 1) ok)))
+    (test10 (const (@star (-or 1 0 1) ok)))
+    (test11 (const (@star (-or 1 1 1) ok)))))
+
+(:: or (or_spec / checker))
+(def or
+  #your_asnwer)
+
+'find a second way to compute OR
+(:: or2 (or_spec / checker))
+(def or2
+  #your_answer)
+
+(def impl_spec
+  (galaxy
+    (test00 (const (@star (-impl 0 0 1) ok)))
+    (test01 (const (@star (-impl 0 1 1) ok)))
+    (test10 (const (@star (-impl 1 0 0) ok)))
+    (test11 (const (@star (-impl 1 1 1) ok)))))
+
+(:: impl (impl_spec / checker))
+(def impl
+  (exec (union (union #not #or)
+  #your_answer)))
+
+'find a second way to compute IMPLICATION
+(:: impl2 (impl_spec / checker))
+(def impl2
+  (exec (union (union #not #or)
+  #your_answer)))
+
+'implement the excluded middle X \/ ~X
+(== ex (const (star (+ex 1 1)) (star (+ex 0 1))))
+(def ex
+  (union (union #not #or)
+  #your_answer))
+
+'how to show the values of X, Y and Z for which X /\ ~(Y /\ Z) is true?
+(show-exec
+  #your_answer)
diff --git a/exercises/04-boolean.sg b/exercises/04-boolean.sg
deleted file mode 100644
index 4c648d9..0000000
--- a/exercises/04-boolean.sg
+++ /dev/null
@@ -1,62 +0,0 @@
-'fill the #your_answer hole by following the specifications
-
-not_spec = galaxy
-  test0 = @-not(0 1) ok.
-  test1 = @-not(1 0) ok.
-end
-
-not :: not_spec.
-not = #your_answer.
-
-'how to print the truth table of NOT ?
-table_not :=: { table_not(1 0); table_not(0 1) }.
-table_not = not #your_answer.
-
-and_spec = galaxy
-  test00 = @-and(0 0 0) ok.
-  test01 = @-and(0 1 0) ok.
-  test10 = @-and(1 0 0) ok.
-  test11 = @-and(1 1 1) ok.
-end
-
-and :: and_spec.
-and = #your_answer.
-
-'find a second way to compute AND
-and2 :: and_spec.
-and2 = #your_answer.
-
-or_spec = galaxy
-  test00 = @-or(0 0 0) ok.
-  test01 = @-or(0 1 1) ok.
-  test10 = @-or(1 0 1) ok.
-  test11 = @-or(1 1 1) ok.
-end
-
-or :: or_spec.
-or = #your_answer.
-
-'find a second way to compute OR
-or2 :: or_spec.
-or2 = #your_answer.
-
-impl_spec = galaxy
-  test00 = @-impl(0 0 1) ok.
-  test01 = @-impl(0 1 1) ok.
-  test10 = @-impl(1 0 0) ok.
-  test11 = @-impl(1 1 1) ok.
-end
-
-impl :: impl_spec.
-impl = not or #your_answer.
-
-'find a second way to compute IMPLICATION
-impl2 :: impl_spec.
-impl2 = not or #your_answer.
-
-'implement the excluded middle X \/ ~X
-ex :=: { +ex(1 1); +ex(0 1) }.
-ex = not or #your_answer.
-
-'how to show the values of X, Y and Z for which X /\ ~(Y /\ Z) is true?
-show-exec #your_answer.
diff --git a/exercises/solutions/00-unification.sg b/exercises/solutions/00-unification.sg
index cd7f321..fb02796 100644
--- a/exercises/solutions/00-unification.sg
+++ b/exercises/solutions/00-unification.sg
@@ -1,22 +1,45 @@
 'fill the #your_answer holes with the correct result of execution
 
-x1 :=: a.
-x1 = @+f(X) X; -f(a).
+(== x1 (const (star a)))
+(def x1
+  (const
+    (@star (+f X) X)
+    (star (-f a))))
 
-x2 :=: a.
-x2 = @+f(X); -f(Y) a.
+(== x2 (const (star a)))
+(def x2
+  (const
+    (@star (+f X))
+    (star (-f Y) a)))
 
-x3 :=: b; a.
-x3 = @+f(X) X; -f(a); -f(b).
+(== x3 (const (star b) (star a)))
+(def x3
+  (const
+    (@star (+f X) X)
+    (star (-f a))
+    (star (-f b))))
 
-x4 :=: +1 -2.
-x4 = @+1 -2; -2 +3.
+(== x4 (const (star +1 -2)))
+(def x4
+  (const
+    (@star +1 -2)
+    (star -2 +3)))
 
-x5 :=: -2 +1.
-x5 = @-1 +2; -2 +1.
+(== x5 (const (star -2 +1)))
+(def x5
+  (const
+    (@star -1 +2)
+    (star -2 +1)))
 
-x6 :=: -2 +1.
-x6 = @-1 +2; -2 +1.
+(== x6 (const (star -2 +1)))
+(def x6
+  (const
+    (@star -1 +2)
+    (star -2 +1)))
 
-x7 :=: a.
-x7 = @-f(X) X; +f(+g(a)); -g(X) X.
+(== x7 (const (star a)))
+(def x7
+  (const
+    (@star (-f X) X)
+    (star (+f (+g a)))
+    (star (-g X) X)))
diff --git a/exercises/solutions/01-paths.sg b/exercises/solutions/01-paths.sg
index 84232af..8cd23a4 100644
--- a/exercises/solutions/01-paths.sg
+++ b/exercises/solutions/01-paths.sg
@@ -1,17 +1,32 @@
 'fill the 'your_answer' holes to replace #1 in the constellations
 'below such that the result of execution is { ok }
 
-x1 :=: ok.
-x1 = (@(-1 ok) #1)[#1=>+1].
+(== x1 (const (star ok)))
+(def x1
+  (union (const (@star -1 ok)) #1)
+  [#1=>(const (star +1))])
 
-x2 :=: ok.
-x2 = ((@-1; +2) #1)[#1=>+1 -2 ok].
+(== x2 (const (star ok)))
+(def x2
+  (union (const (@star -1) (star +2)) #1)
+  [#1=>(const (star +1 -2 ok))])
 
-x3 :=: ok.
-x3 = ((@-1 ok; -2 +3) #1)[#1=>+1 +2; -3].
+(== x3 (const (star ok)))
+(def x3
+  (union (const (@star -1 ok) (star -2 +3)) #1)
+  [#1=>(const (star +1 +2) (star -3))])
 
-x4 :=: ok.
-x4 = ((@-f(+g(X)) ok) #1)[#1=>+f(-g(X))].
+(== x4 (const (star ok)))
+(def x4
+  (union (const (@star (-f (+g X)) ok)) #1)
+  [#1=>(const (star (+f (-g X))))])
 
-x5 :=: ok.
-x5 = ((+f(a) +f(b); +g(a); @+g(b) ok) #1)[#1=>-f(a); -f(b) -g(a) -g(b)].
+(== x5 (const (star ok)))
+(def x5
+  (union
+    (const
+      (star (+f a) (+f b))
+      (star (+g a))
+      (@star (+g b) ok))
+    #1)
+  [#1=>(const (star (-f a)) (star (-f b) (-g a) (-g b)))])
diff --git a/exercises/solutions/02-registers.sg b/exercises/solutions/02-registers.sg
index 39c55a5..fbec709 100644
--- a/exercises/solutions/02-registers.sg
+++ b/exercises/solutions/02-registers.sg
@@ -1,32 +1,34 @@
-show-exec process
+(show-exec (process
   'represents a register with value 0
-  +r0(0).
+  (const (star (+r0 0)))
 
   'update the value to 1
-  -r0(X) +tmp0(X).
-  -tmp0(X) +r0(1).
+  (const (star (-r0 X) (+tmp0 X)))
+  (const (star (-tmp0 X) (+r0 1)))
 
   'duplicate the register into two registers r1 and r2
-  -r0(X) +r1(X);
-  -r0(X) +r2(X).
+  (const
+    (star (-r0 X) (+r1 X))
+    (star (-r0 X) (+r2 X)))
 
   'update r1 to 0
-  -r1(X) +tmp0(X).
-  -tmp0(X) +r1(0).
+  (const (star (-r1 X) (+tmp0 X)))
+  (const (star (-tmp0 X) (+r1 0)))
 
   'swap the value of r1 and r2
-  -r1(X) +s1(X); -r2(X) +s2(X).
-  -s1(X) +r2(X); -s2(X) +r1(X).
+  (const (star (-r1 X) (+s1 X)))
+  (const (star (-r2 X) (+s2 X)))
+  (const (star (-s1 X) (+r2 X)))
+  (const (star (-s2 X) (+r1 X)))
 
   'duplicate r1 and add a copy identifier as first argument
-  -r1(X) +r1(l X);
-  -r1(X) +r1(r X).
+  (const (star (-r1 X) (+r1 l X)))
+  (const (star (-r1 X) (+r1 r X)))
 
   'update the two copies to 5 at once
-  -r1(A X) +tmp0(A X).
-  -tmp0(A X) +r1(A 5).
+  (const (star (-r1 A X) (+tmp0 A X)))
+  (const (star (-tmp0 A X) (+r1 A 5)))
 
   'duplicate each copy of r1 again with the same method
-  -r1(A X) +r1(l A X);
-  -r1(A X) +r1(r A X).
-end
+  (const (star (-r1 A X) (+r1 l A X)))
+  (const (star (-r1 A X) (+r1 r A X)))))
diff --git a/exercises/solutions/03-boolean.sg b/exercises/solutions/03-boolean.sg
new file mode 100644
index 0000000..7a5632c
--- /dev/null
+++ b/exercises/solutions/03-boolean.sg
@@ -0,0 +1,95 @@
+'fill the #your_answer hole by following the specifications
+
+(def checker
+  (galaxy
+    (interaction (union #tested #test))
+    (expect (const (star ok)))))
+
+(def not_spec
+  (galaxy
+    (test0 (const (@star (-not 0 1) ok)))
+    (test1 (const (@star (-not 1 0) ok)))))
+
+(:: not (not_spec / checker))
+(def not
+  (const
+    (star (+not 0 1))
+    (star (+not 1 0))))
+
+'how to print the truth table of NOT ?
+(== table_not (const
+  (star (table_not 0 1))
+  (star (table_not 1 0))))
+(def table_not
+  (union
+    #not
+    (const (@star (-not X Y) (table_not X Y)))))
+
+(def and_spec
+  (galaxy
+    (test00 (const (@star (-and 0 0 0) ok)))
+    (test01 (const (@star (-and 0 1 0) ok)))
+    (test10 (const (@star (-and 1 0 0) ok)))
+    (test11 (const (@star (-and 1 1 1) ok)))))
+
+(:: and (and_spec / checker))
+(def and
+  (const
+    (star (+and 0 0 0))
+    (star (+and 0 1 0))
+    (star (+and 1 0 0))
+    (star (+and 1 1 1))))
+
+(:: and (and_spec / checker))
+(def and2
+  (const
+    (star (+and 0 X 0))
+    (star (+and 1 X X))))
+
+(def or_spec
+  (galaxy
+    (test00 (const (@star (-or 0 0 0) ok)))
+    (test01 (const (@star (-or 0 1 1) ok)))
+    (test10 (const (@star (-or 1 0 1) ok)))
+    (test11 (const (@star (-or 1 1 1) ok)))))
+
+(:: or (or_spec / checker))
+(def or
+  (const
+    (star (+or 0 0 0))
+    (star (+or 0 1 1))
+    (star (+or 1 0 1))
+    (star (+or 1 1 1))))
+
+(:: or2 (or_spec / checker))
+(def or2
+  (const
+    (star (+or 0 X X))
+    (star (+or 1 X 1))))
+
+(def impl_spec
+  (galaxy
+    (test00 (const (@star (-impl 0 0 1) ok)))
+    (test01 (const (@star (-impl 0 1 1) ok)))
+    (test10 (const (@star (-impl 1 0 0) ok)))
+    (test11 (const (@star (-impl 1 1 1) ok)))))
+
+(:: impl (impl_spec / checker))
+(def impl
+  (exec (union (union #not #or)
+  (const (@star (-not X Y) (-or Y Z R) (+impl X Z R))))))
+
+(:: impl2 (impl_spec / checker))
+(def impl2
+  (exec (union (union #not #or)
+  (const (@star (-not X Y) (-or Y Z R) (+impl X Z R))))))
+
+(== ex (const (star (+ex 1 1)) (star (+ex 0 1))))
+(def ex
+  (union (union #not #or)
+  (const (@star (-not X R1) (-or R1 X R2) (+ex X R2)))))
+
+'how to show the values of X, Y and Z for which X /\ ~(Y /\ Z) is true?
+(show-exec
+  (union (union (union #or #not) #and)
+  (const (@star (-or Y Z R1) (-not R1 R2) (-and X R2 1) (x X) (y Y) (z Z)))))
diff --git a/exercises/solutions/04-boolean.sg b/exercises/solutions/04-boolean.sg
deleted file mode 100644
index a0ee86d..0000000
--- a/exercises/solutions/04-boolean.sg
+++ /dev/null
@@ -1,63 +0,0 @@
-'fill the #your_answer hole by following the specifications
-
-checker = galaxy
-  interaction = #tested #test.
-  expect = ok.
-end
-
-not_spec = galaxy
-  test0 = @-not(0 1) ok.
-  test1 = @-not(1 0) ok.
-end
-
-not :: not_spec [checker].
-not = +not(0 1); +not(1 0).
-
-'how to print the truth table of NOT ?
-table_not :=: table_not(0 1); table_not(1 0).
-table_not = #not {@-not(X Y) table_not(X Y)}.
-
-and_spec = galaxy
-  test00 = @-and(0 0 0) ok.
-  test01 = @-and(0 1 0) ok.
-  test10 = @-and(1 0 0) ok.
-  test11 = @-and(1 1 1) ok.
-end
-
-and :: and_spec [checker].
-and = +and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1).
-
-and2 :: and_spec [checker].
-and2 = +and(0 X 0); +and(1 X X).
-
-or_spec = galaxy
-  test00 = @-or(0 0 0) ok.
-  test01 = @-or(0 1 1) ok.
-  test10 = @-or(1 0 1) ok.
-  test11 = @-or(1 1 1) ok.
-end
-
-or :: or_spec [checker].
-or = +or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1).
-
-or2 :: or_spec [checker].
-or2 = +or(0 X X); +or(1 X 1).
-
-impl_spec = galaxy
-  test00 = @-impl(0 0 1) ok.
-  test01 = @-impl(0 1 1) ok.
-  test10 = @-impl(1 0 0) ok.
-  test11 = @-impl(1 1 1) ok.
-end
-
-impl :: impl_spec [checker].
-impl = exec #not #or @{-not(X Y) -or(Y Z R) +impl(X Z R)} end.
-
-impl2 :: impl_spec [checker].
-impl2 = exec #not #or @{-not(X Y) -or(Y Z R) +impl(X Z R)} end.
-
-ex :=: +ex(1 1); +ex(0 1).
-ex = #not #or @{-not(X R1) -or(R1 X R2) +ex(X R2)}.
-
-'how to show the values of X, Y and Z for which X /\ ~(Y /\ Z) is true?
-show-exec #or #not #and @{-or(Y Z R1) -not(R1 R2) -and(X R2 1) x(X) y(Y) z(Z)}.
diff --git a/guide/en/src/automata/nfsa.md b/guide/en/src/automata/nfsa.md
deleted file mode 100644
index 8fc4165..0000000
--- a/guide/en/src/automata/nfsa.md
+++ /dev/null
@@ -1 +0,0 @@
-# Automate finis
diff --git a/guide/en/src/automata/pda.md b/guide/en/src/automata/pda.md
deleted file mode 100644
index f6552fa..0000000
--- a/guide/en/src/automata/pda.md
+++ /dev/null
@@ -1 +0,0 @@
-# Automates à pile
diff --git a/guide/en/src/automata/transducers.md b/guide/en/src/automata/transducers.md
deleted file mode 100644
index 34f1efa..0000000
--- a/guide/en/src/automata/transducers.md
+++ /dev/null
@@ -1 +0,0 @@
-# Transducteurs
diff --git a/guide/en/src/automata/turing.md b/guide/en/src/automata/turing.md
deleted file mode 100644
index 8193e64..0000000
--- a/guide/en/src/automata/turing.md
+++ /dev/null
@@ -1 +0,0 @@
-# Machines de Turing (TODO)
diff --git a/guide/en/src/lambda/lintypes.md b/guide/en/src/lambda/lintypes.md
deleted file mode 100644
index 5ca230e..0000000
--- a/guide/en/src/lambda/lintypes.md
+++ /dev/null
@@ -1 +0,0 @@
-# Types linéaires (TODO)
diff --git a/guide/en/src/lambda/stlc.md b/guide/en/src/lambda/stlc.md
deleted file mode 100644
index cff6df6..0000000
--- a/guide/en/src/lambda/stlc.md
+++ /dev/null
@@ -1 +0,0 @@
-# Lambda-calcul simplement typé (TODO)
diff --git a/guide/en/src/lambda/untypedlin.md b/guide/en/src/lambda/untypedlin.md
deleted file mode 100644
index a16604a..0000000
--- a/guide/en/src/lambda/untypedlin.md
+++ /dev/null
@@ -1 +0,0 @@
-# Lambda-calcul linéaire non typé (TODO)
diff --git a/guide/en/src/objects/interfaces.md b/guide/en/src/objects/interfaces.md
deleted file mode 100644
index 2dc9a6d..0000000
--- a/guide/en/src/objects/interfaces.md
+++ /dev/null
@@ -1,17 +0,0 @@
-# Interfaces
-
-It is possible to check whether a galaxy is constructed in a certain way
-with fields of some specific name and type:
-
-```
-interface nat_pair
-  n :: nat.
-  m :: nat.
-end
-
-g_pair :: nat_pair.
-g_pair = galaxy
-  n = +nat(0).
-  m = +nat(0).
-end
-```
diff --git a/guide/en/src/stellogen/effects.md b/guide/en/src/stellogen/effects.md
deleted file mode 100644
index eb4cced..0000000
--- a/guide/en/src/stellogen/effects.md
+++ /dev/null
@@ -1,24 +0,0 @@
-# Reactive effects
-
-Stellogen uses "reactive effects" which are activated during the
-interaction between two rays using special head symbols.
-
-## Print
-
-For printing, an interaction between two rays `%print` is needed.
-The interaction generates a substitution defining the ray to be displayed:
-
-```
-+%print(X); -%print("hello world\n").
-```
-
-This command displays `hello world` then an end of line symbol.
-
-## Running a constellation
-
-When constellations produce an effect, a `run` command is available
-to execute them:
-
-```
-run +%print(X); -%print("hello world\n").
-```
diff --git a/guide/fr/src/automata/nfsa.md b/guide/fr/src/automata/nfsa.md
deleted file mode 100644
index 8fc4165..0000000
--- a/guide/fr/src/automata/nfsa.md
+++ /dev/null
@@ -1 +0,0 @@
-# Automate finis
diff --git a/guide/fr/src/automata/pda.md b/guide/fr/src/automata/pda.md
deleted file mode 100644
index f6552fa..0000000
--- a/guide/fr/src/automata/pda.md
+++ /dev/null
@@ -1 +0,0 @@
-# Automates à pile
diff --git a/guide/fr/src/automata/transducers.md b/guide/fr/src/automata/transducers.md
deleted file mode 100644
index 34f1efa..0000000
--- a/guide/fr/src/automata/transducers.md
+++ /dev/null
@@ -1 +0,0 @@
-# Transducteurs
diff --git a/guide/fr/src/automata/turing.md b/guide/fr/src/automata/turing.md
deleted file mode 100644
index 8193e64..0000000
--- a/guide/fr/src/automata/turing.md
+++ /dev/null
@@ -1 +0,0 @@
-# Machines de Turing (TODO)
diff --git a/guide/fr/src/lambda/lintypes.md b/guide/fr/src/lambda/lintypes.md
deleted file mode 100644
index 5ca230e..0000000
--- a/guide/fr/src/lambda/lintypes.md
+++ /dev/null
@@ -1 +0,0 @@
-# Types linéaires (TODO)
diff --git a/guide/fr/src/lambda/stlc.md b/guide/fr/src/lambda/stlc.md
deleted file mode 100644
index cff6df6..0000000
--- a/guide/fr/src/lambda/stlc.md
+++ /dev/null
@@ -1 +0,0 @@
-# Lambda-calcul simplement typé (TODO)
diff --git a/guide/fr/src/lambda/untypedlin.md b/guide/fr/src/lambda/untypedlin.md
deleted file mode 100644
index a16604a..0000000
--- a/guide/fr/src/lambda/untypedlin.md
+++ /dev/null
@@ -1 +0,0 @@
-# Lambda-calcul linéaire non typé (TODO)
diff --git a/guide/fr/src/objects/interfaces.md b/guide/fr/src/objects/interfaces.md
deleted file mode 100644
index d19fe69..0000000
--- a/guide/fr/src/objects/interfaces.md
+++ /dev/null
@@ -1,17 +0,0 @@
-# Interfaces
-
-Il est possible de vérifier si une galaxie est formé d'une certaine
-manière avec des champs possédant un certain nom et étant d'un certain type :
-
-```
-interface nat_pair
-  n :: nat.
-  m :: nat.
-end
-
-g_pair :: nat_pair.
-g_pair = galaxy
-  n = +nat(0).
-  m = +nat(0).
-end
-```
diff --git a/guide/fr/src/stellogen/effects.md b/guide/fr/src/stellogen/effects.md
deleted file mode 100644
index b78678b..0000000
--- a/guide/fr/src/stellogen/effects.md
+++ /dev/null
@@ -1,24 +0,0 @@
-# Effets réactifs
-
-Stellogen utilise des "effets réactifs" qui sont déclenchés lors de
-l'interaction entre des rayons utilisant des symboles de têtes spéciaux.
-
-## Print
-
-Pour l'affichage, il faut une interaction entre deux rayons `%print`.
-L'interaction génère une substitution définissant le rayon à afficher :
-
-```
-+%print(X); -%print("hello world\n").
-```
-
-La commande ci-dessus affiche `hello world` puis un saut à la ligne.
-
-## Lancement de constellation
-
-Lorsque les constellations produisent des effets, une commande `run`
-est disponible pour les exécuter :
-
-```
-run +%print(X); -%print("hello world\n").
-```
diff --git a/nvim/ftdetect/stellogen.vim b/nvim/ftdetect/stellogen.vim
index 91ef933..89fa3f5 100644
--- a/nvim/ftdetect/stellogen.vim
+++ b/nvim/ftdetect/stellogen.vim
@@ -1 +1,2 @@
 autocmd BufNewFile,BufRead *.sg setfiletype stellogen
+autocmd FileType stellogen setlocal shiftwidth=2 softtabstop=2 expandtab
diff --git a/nvim/syntax/stellogen.vim b/nvim/syntax/stellogen.vim
index 8f7c99f..cc106fa 100644
--- a/nvim/syntax/stellogen.vim
+++ b/nvim/syntax/stellogen.vim
@@ -1,24 +1,21 @@
 syn clear
 
-syn keyword sgKeyword show use exec spec linear trace process end galaxy run interface
+syn keyword sgKeyword define syntax kill clean eval show use exec spec linexec trace process run union
 syn match sgComment "\s*'[^'].*$"
 syn match sgId "#\%(\l\|\d\)\w*"
-syn match sgIdDef "\zs\%(\l\|\d\)\w*\ze\s*="
-syn match sgIdType "\zs\%(\l\|\d\)\w*\ze\s*::"
-syn match sgType "^\w*\s*::\s*\zs\%(\l\|\d\)\w*\ze"
 syn region sgComment start="'''" end="'''" contains=NONE
 syn region sgString start=/\v"/ skip=/\v\\./ end=/\v"/
-syn match sgSeparator "[;\.\{\}\:\[\]|]"
-syn match sgOperator "[=@]"
-syn match sgOperator "=>"
+syn match sgSeparator "[\<\>\{\}\[\]|]"
+syn match sgOperator "@"
+syn match sgOperator "::"
+syn match sgOperator "=="
+syn match sgOperator ":="
 syn match sgOperator "!="
+syn match sgOperator "&"
 
 hi link sgKeyword Keyword
 hi link sgId Identifier
-hi link sgIdDef Identifier
-hi link sgIdType Identifier
 hi link sgComment Comment
 hi link sgOperator Operator
 hi link sgSeparator Special
 hi link sgString String
-hi link sgType Type
diff --git a/src/common/common_parser.mly b/src/common/common_parser.mly
deleted file mode 100644
index f717b5c..0000000
--- a/src/common/common_parser.mly
+++ /dev/null
@@ -1,21 +0,0 @@
-%token PRINT
-%token EOF
-%token AT
-%token DOT
-%token EOL
-%token AMP
-%token LBRACK RBRACK
-%token LBRACE RBRACE
-%token LPAR RPAR
-
-%%
-
-let delimited_opt(l, x, r) :=
-  | ~=x; <>
-  | ~=delimited(l, x, r); <>
-
-%public let pars(x) == ~=delimited(LPAR; EOL*, x, EOL*; RPAR); <>
-%public let bracks(x) == ~=delimited(LBRACK; EOL*, x, EOL*; RBRACK); <>
-%public let braces(x) == ~=delimited(LBRACE; EOL*, x, EOL*; RBRACE); <>
-%public let bracks_opt(x) == ~=delimited_opt(LBRACK; EOL*, x, EOL*; RBRACK); <>
-%public let braces_opt(x) == ~=delimited_opt(LBRACE; EOL*, x, EOL*; RBRACE); <>
diff --git a/src/common/dune b/src/common/dune
deleted file mode 100644
index 30e6468..0000000
--- a/src/common/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(library
- (name common)
- (libraries base))
diff --git a/src/common/format_exn.ml b/src/common/format_exn.ml
deleted file mode 100644
index 7fd3d6a..0000000
--- a/src/common/format_exn.ml
+++ /dev/null
@@ -1 +0,0 @@
-let red text = "\x1b[31m" ^ text ^ "\x1b[0m"
diff --git a/src/dune b/src/dune
new file mode 100644
index 0000000..e15b5f4
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,14 @@
+(library
+ (name stellogen)
+ (libraries base menhirLib)
+ (preprocess
+  (pps sedlex.ppx)))
+
+(env
+ (dev
+  (flags
+   (:standard -warn-error -A))))
+
+(menhir
+ (modules parser)
+ (flags --table --dump --explain))
diff --git a/src/expr.ml b/src/expr.ml
new file mode 100644
index 0000000..32e169d
--- /dev/null
+++ b/src/expr.ml
@@ -0,0 +1,232 @@
+open Base
+open Lsc_ast
+open Sgen_ast
+
+type ident = string
+
+module Raw = struct
+  type t =
+    | Symbol of string
+    | Var of ident
+    | String of string
+    | Focus of t
+    | Call of t
+    | List of t list
+    | Stack of t list
+    | Group of t list
+    | Cons of t list
+    | ConsWithParams of t list * t list
+    | ConsWithBase of t list * t
+end
+
+type expr =
+  | Symbol of string
+  | Var of ident
+  | List of expr list
+
+let primitive = String.append "%"
+
+let nil_op = primitive "nil"
+
+let cons_op = primitive "cons"
+
+let call_op = "#"
+
+let focus_op = "@"
+
+let string_op = primitive "string"
+
+let def_op = ":="
+
+let expect_op = "=="
+
+let params_op = primitive "params"
+
+let ineq_op = "!="
+
+let incomp_op = "slice"
+
+let group_op = "%group"
+
+let string_of_list lmark rmark l =
+  l |> String.concat ~sep:" " |> fun l' ->
+  Printf.sprintf "%s%s%s" lmark l' rmark
+
+let rec to_string : expr -> string = function
+  | Symbol s -> s
+  | Var x -> x
+  | List es -> es |> List.map ~f:to_string |> string_of_list "(" ")"
+
+let rec expand_macro : Raw.t -> expr = function
+  | Raw.Symbol s -> Symbol s
+  | Raw.Var x -> Var x
+  | Raw.String s -> List [ Symbol string_op; Symbol s ]
+  | Raw.Call e' -> List [ Symbol call_op; expand_macro e' ]
+  | Raw.Focus e' -> List [ Symbol focus_op; expand_macro e' ]
+  | Raw.Group es -> List (Symbol group_op :: List.map ~f:expand_macro es)
+  | Raw.List es -> List (List.map ~f:expand_macro es)
+  | Raw.Cons es -> expand_macro (Raw.ConsWithBase (es, Symbol nil_op))
+  | Raw.ConsWithBase (es, base) ->
+    List.fold_left es ~init:(expand_macro base) ~f:(fun acc e ->
+      List [ Symbol cons_op; expand_macro e; acc ] )
+  | Raw.ConsWithParams (es, ps) ->
+    List [ Symbol params_op; expand_macro (Cons es); expand_macro (List ps) ]
+  | Raw.Stack [] -> List []
+  | Raw.Stack (h :: t) ->
+    List.fold_left t ~init:(expand_macro h) ~f:(fun acc e ->
+      List [ expand_macro e; acc ] )
+
+let rec equal_expr x y =
+  match (x, y) with
+  | Var x1, Var x2 | Symbol x1, Symbol x2 -> equal_string x1 x2
+  | List es1, List es2 -> begin
+    try List.for_all2_exn es1 es2 ~f:equal_expr with _ -> false
+  end
+  | _ -> false
+
+let rec replace_id (xfrom : ident) xto e =
+  match e with
+  | Var x when equal_string x xfrom -> xto
+  | Symbol _ | Var _ -> e
+  | List es -> List (List.map ~f:(replace_id xfrom xto) es)
+
+let unfold_decl_def (env : (string * (string list * expr list)) list) es :
+  expr list =
+  List.fold_left es ~init:(env, []) ~f:(fun (env, acc) -> function
+    | List (Symbol "new-declaration" :: List (Symbol k :: args) :: content) ->
+      let var_args =
+        List.map args ~f:(function
+          | Var x -> x
+          | _ -> failwith "error: syntax declaration must contain variables" )
+      in
+      ((k, (var_args, content)) :: env, acc)
+    | List (Symbol k :: args)
+      when List.Assoc.find ~equal:equal_string env k |> Option.is_some ->
+      let syntax_args, content =
+        List.Assoc.find_exn ~equal:equal_string env k
+      in
+      if List.length syntax_args <> List.length args then
+        failwith ("Error: not enough args given in macro call " ^ k)
+      else
+        let replace_ids e =
+          List.fold_left (List.zip_exn syntax_args args) ~init:e
+            ~f:(fun acc (xfrom, xto) -> replace_id xfrom xto acc )
+        in
+        (env, (List.map ~f:replace_ids content |> List.rev) @ acc)
+    | e -> (env, e :: acc) )
+  |> snd |> List.rev
+
+(* ---------------------------------------
+   Constellation of Expr
+   --------------------------------------- *)
+
+let symbol_of_str (s : string) : idfunc =
+  let rest = String.subo s ~pos:1 in
+  match String.get s 0 with
+  | '+' -> (Pos, rest)
+  | '-' -> (Neg, rest)
+  | _ -> (Null, s)
+
+let rec ray_of_expr : expr -> ray = function
+  | Symbol s -> to_func (symbol_of_str s, [])
+  | Var "_" -> to_var ("_" ^ fresh_placeholder ())
+  | Var s -> to_var s
+  | List [] -> failwith "error: ray cannot be empty"
+  | List (Symbol h :: t) -> to_func (symbol_of_str h, List.map ~f:ray_of_expr t)
+  | List (_ :: _) as e ->
+    failwith ("error: ray " ^ to_string e ^ " must start with constant")
+
+let bans_of_expr : expr list -> ban list =
+  let ban_of_expr = function
+    | List [ Symbol k; a; b ] when equal_string k ineq_op ->
+      Ineq (ray_of_expr a, ray_of_expr b)
+    | List [ Symbol k; a; b ] when equal_string k incomp_op ->
+      Incomp (ray_of_expr a, ray_of_expr b)
+    | _ -> failwith "error: invalid ban expression"
+  in
+  List.map ~f:ban_of_expr
+
+let rec raylist_of_expr (e : expr) : ray list =
+  match e with
+  | Symbol k when equal_string k nil_op -> []
+  | Symbol _ | Var _ -> [ ray_of_expr e ]
+  | List [ Symbol s; h; t ] when equal_string s cons_op ->
+    ray_of_expr h :: raylist_of_expr t
+  | e -> failwith ("error: unhandled star " ^ to_string e)
+
+let rec star_of_expr : expr -> marked_star = function
+  | List [ Symbol k; s ] when equal_string k focus_op ->
+    star_of_expr s |> Lsc_ast.remove_mark |> Lsc_ast.mark
+  | List [ Symbol k; s; List ps ] when equal_string k params_op ->
+    Unmarked { content = raylist_of_expr s; bans = bans_of_expr ps }
+  | e -> Unmarked { content = raylist_of_expr e; bans = [] }
+
+let rec constellation_of_expr : expr -> marked_constellation = function
+  | Symbol k when equal_string k nil_op -> []
+  | Symbol s -> [ Unmarked { content = [ var (s, None) ]; bans = [] } ]
+  | Var x -> [ Unmarked { content = [ var (x, None) ]; bans = [] } ]
+  | List [ Symbol s; h; t ] when equal_string s cons_op ->
+    star_of_expr h :: constellation_of_expr t
+  | List g -> [ Unmarked { content = [ ray_of_expr (List g) ]; bans = [] } ]
+
+(* ---------------------------------------
+   Stellogen expr of Expr
+   --------------------------------------- *)
+
+let rec sgen_expr_of_expr (e : expr) : sgen_expr =
+  match e with
+  (* ray *)
+  | Var _ | Symbol _ ->
+    Raw [ Unmarked { content = [ ray_of_expr e ]; bans = [] } ]
+  (* star *)
+  | List (Symbol s :: _) when equal_string s params_op -> Raw [ star_of_expr e ]
+  | List (Symbol s :: _) when equal_string s cons_op -> Raw [ star_of_expr e ]
+  (* id *)
+  | List [ Symbol k; g ] when equal_string k call_op -> Id (ray_of_expr g)
+  (* focus @ *)
+  | List [ Symbol k; g ] when equal_string k focus_op ->
+    Focus (sgen_expr_of_expr g)
+  (* group *)
+  | List (Symbol k :: gs) when equal_string k group_op ->
+    Group (List.map ~f:sgen_expr_of_expr gs)
+  (* process *)
+  | List (Symbol "process" :: gs) -> Process (List.map ~f:sgen_expr_of_expr gs)
+  (* kill *)
+  | List [ Symbol "kill"; g ] -> Kill (sgen_expr_of_expr g)
+  (* clean *)
+  | List [ Symbol "clean"; g ] -> Clean (sgen_expr_of_expr g)
+  (* exec *)
+  | List [ Symbol "exec"; g ] -> Exec (false, sgen_expr_of_expr g)
+  (* linear exec *)
+  | List [ Symbol "linexec"; g ] -> Exec (true, sgen_expr_of_expr g)
+  (* eval *)
+  | List [ Symbol "eval"; g ] -> Eval (sgen_expr_of_expr g)
+  (* KEEP LAST -- raw constellation *)
+  | List g -> Raw (constellation_of_expr (List g))
+
+(* ---------------------------------------
+   Stellogen program of Expr
+   --------------------------------------- *)
+
+let decl_of_expr : expr -> declaration = function
+  (* definition := *)
+  | List [ Symbol k; x; g ] when equal_string k def_op ->
+    Def (ray_of_expr x, sgen_expr_of_expr g)
+  | List [ Symbol "spec"; x; g ] -> Def (ray_of_expr x, sgen_expr_of_expr g)
+  | List [ Symbol "exec"; x; g ] -> Def (ray_of_expr x, sgen_expr_of_expr g)
+  (* show *)
+  | List [ Symbol "show"; g ] -> Show (sgen_expr_of_expr g)
+  (* trace *)
+  | List [ Symbol "trace"; g ] -> Trace (sgen_expr_of_expr g)
+  (* expect *)
+  | List [ Symbol k; g1; g2 ] when equal_string k expect_op ->
+    Expect (sgen_expr_of_expr g1, sgen_expr_of_expr g2, const "default")
+  | List [ Symbol k; g1; g2; m ] when equal_string k expect_op ->
+    Expect (sgen_expr_of_expr g1, sgen_expr_of_expr g2, ray_of_expr m)
+  (* use *)
+  | List [ Symbol k; r ] when equal_string k "use" -> Use (ray_of_expr r)
+  | e -> failwith ("error: invalid declaration " ^ to_string e)
+
+let program_of_expr = List.map ~f:decl_of_expr
+
+let preprocess e = e |> List.map ~f:expand_macro |> unfold_decl_def []
diff --git a/src/lexer.ml b/src/lexer.ml
new file mode 100644
index 0000000..f3edb17
--- /dev/null
+++ b/src/lexer.ml
@@ -0,0 +1,75 @@
+open Sedlexing
+open Parser
+
+exception SyntaxError of string
+
+let space = [%sedlex.regexp? Plus (' ' | '\t')]
+
+let newline = [%sedlex.regexp? '\r' | '\n' | "\r\n"]
+
+let rec comment lexbuf =
+  match%sedlex lexbuf with
+  | newline | eof -> read lexbuf
+  | _ ->
+    ignore (Sedlexing.next lexbuf);
+    comment lexbuf
+
+and comments lexbuf =
+  match%sedlex lexbuf with
+  | "'''" | eof -> read lexbuf
+  | _ ->
+    ignore (Sedlexing.next lexbuf);
+    comments lexbuf
+
+and read lexbuf =
+  match%sedlex lexbuf with
+  | ( Compl (Chars "'\" \t\n\r()<>[]{}|@#")
+    , Star (Compl (Chars " \t\n\r()<>[]{}|")) ) ->
+    let lexeme = Utf8.lexeme lexbuf in
+    begin
+      match lexeme.[0] with '_' | 'A' .. 'Z' -> VAR lexeme | _ -> SYM lexeme
+    end
+  | '(' -> LPAR
+  | ')' -> RPAR
+  | '[' -> LBRACK
+  | ']' -> RBRACK
+  | '{' -> LBRACE
+  | '}' -> RBRACE
+  | '<' -> LANGLE
+  | '>' -> RANGLE
+  | '@' -> AT
+  | '#' -> SHARP
+  | '|' -> BAR
+  | '\'' -> comment lexbuf
+  | "'''" -> comments lexbuf
+  | '"' -> string_literal lexbuf
+  | space | newline -> read lexbuf
+  | eof -> EOF
+  | _ ->
+    raise
+      (SyntaxError
+         ("Unexpected character '" ^ Utf8.lexeme lexbuf ^ "' during lexing") )
+
+and string_literal lexbuf =
+  let buffer = Buffer.create 32 in
+  let rec loop () =
+    match%sedlex lexbuf with
+    | '"' -> STRING (Buffer.contents buffer)
+    | '\\', any ->
+      let escaped =
+        match%sedlex lexbuf with
+        | 'n' -> '\n'
+        | 't' -> '\t'
+        | '\\' -> '\\'
+        | '"' -> '"'
+        | _ -> failwith "Unknown escape sequence"
+      in
+      Buffer.add_char buffer escaped;
+      loop ()
+    | eof -> failwith "Unterminated string literal"
+    | any ->
+      Buffer.add_string buffer (Sedlexing.Utf8.lexeme lexbuf);
+      loop ()
+    | _ -> failwith "Invalid character in string literal"
+  in
+  loop ()
diff --git a/src/lsc/dune b/src/lsc/dune
deleted file mode 100644
index 518d1d4..0000000
--- a/src/lsc/dune
+++ /dev/null
@@ -1,16 +0,0 @@
-(library
- (name lsc)
- (libraries base common menhirLib)
- (preprocess
-  (pps sedlex.ppx))
- (modules lsc_err lsc_ast unification lsc_parser lsc_lexer))
-
-(env
- (dev
-  (flags
-   (:standard -warn-error -A))))
-
-(menhir
- (modules ../common/common_parser lsc_parser)
- (merge_into lsc_parser)
- (flags --table --dump --explain))
diff --git a/src/lsc/lsc_err.ml b/src/lsc/lsc_err.ml
deleted file mode 100644
index 1d1fee0..0000000
--- a/src/lsc/lsc_err.ml
+++ /dev/null
@@ -1,20 +0,0 @@
-open Base
-open Common.Format_exn
-
-type err_effect =
-  | TooFewArgs of string
-  | TooManyArgs of string
-  | UnknownEffect of string
-
-let pp_err_effect = function
-  | TooFewArgs x when equal_string x "print" ->
-    Printf.sprintf "%s: effect '%s' expects 1 arguments.\n"
-      (red "Missing argument") x
-  | TooFewArgs x ->
-    Printf.sprintf "%s: for effect '%s'.\n" (red "Missing argument") x
-  | TooManyArgs x when equal_string x "print" ->
-    Printf.sprintf "%s: effect '%s' expects 1 arguments.\n"
-      (red "Too many arguments") x
-  | TooManyArgs x ->
-    Printf.sprintf "%s: for effect '%s'.\n" (red "Too many arguments") x
-  | UnknownEffect x -> Printf.sprintf "%s '%s'.\n" (red "UnknownEffect") x
diff --git a/src/lsc/lsc_lexer.ml b/src/lsc/lsc_lexer.ml
deleted file mode 100644
index f443bfc..0000000
--- a/src/lsc/lsc_lexer.ml
+++ /dev/null
@@ -1,92 +0,0 @@
-open Sedlexing
-open Lsc_parser
-
-exception SyntaxError of string
-
-let buf = Sedlexing.Utf8.from_channel
-
-let is_func_start = [%sedlex.regexp? 'a' .. 'z' | '0' .. '9']
-
-let is_func_rest =
-  [%sedlex.regexp? 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' | '?']
-
-let is_var_start = [%sedlex.regexp? 'A' .. 'Z']
-
-let is_var_rest =
-  [%sedlex.regexp? 'A' .. 'Z' | 'a' .. 'z' | '0' .. '9' | '_' | '-']
-
-let space = [%sedlex.regexp? Plus (' ' | '\t')]
-
-let newline = [%sedlex.regexp? '\r' | '\n' | "\r\n"]
-
-let rec read_string buf lexbuf =
-  match%sedlex lexbuf with
-  | '"' -> SYM ("\"" ^ Buffer.contents buf ^ "\"")
-  | '\\', '/' ->
-    Buffer.add_char buf '/';
-    read_string buf lexbuf
-  | '\\', '\\' ->
-    Buffer.add_char buf '\\';
-    read_string buf lexbuf
-  | '\\', 'b' ->
-    Buffer.add_char buf '\b';
-    read_string buf lexbuf
-  | '\\', 'f' ->
-    Buffer.add_char buf '\012';
-    read_string buf lexbuf
-  | '\\', 'n' ->
-    Buffer.add_char buf '\n';
-    read_string buf lexbuf
-  | '\\', 'r' ->
-    Buffer.add_char buf '\r';
-    read_string buf lexbuf
-  | '\\', 't' ->
-    Buffer.add_char buf '\t';
-    read_string buf lexbuf
-  | Plus (Compl ('"' | '\\')) ->
-    Buffer.add_string buf (Utf8.lexeme lexbuf);
-    read_string buf lexbuf
-  | eof -> raise (SyntaxError "String is not terminated")
-  | _ -> raise (SyntaxError ("Illegal string character: " ^ Utf8.lexeme lexbuf))
-
-and comment lexbuf =
-  match%sedlex lexbuf with
-  | newline | eof -> read lexbuf
-  | _ ->
-    ignore (Sedlexing.next lexbuf);
-    comment lexbuf
-
-and comments lexbuf =
-  match%sedlex lexbuf with
-  | "'''" -> read lexbuf
-  | _ ->
-    ignore (Sedlexing.next lexbuf);
-    comments lexbuf
-
-and read lexbuf =
-  match%sedlex lexbuf with
-  | is_var_start, Star is_var_rest -> VAR (Utf8.lexeme lexbuf)
-  | is_func_start, Star is_func_rest -> SYM (Utf8.lexeme lexbuf)
-  | '\'' -> comment lexbuf
-  | "'''" -> comments lexbuf
-  | '_' -> PLACEHOLDER
-  | '.' -> DOT
-  | '|' -> BAR
-  | '[' -> LBRACK
-  | ']' -> RBRACK
-  | '(' -> LPAR
-  | ')' -> RPAR
-  | ',' -> COMMA
-  | '@' -> AT
-  | '&' -> AMP
-  | '+' -> PLUS
-  | '-' -> MINUS
-  | ':' -> CONS
-  | ';' -> SEMICOLON
-  | '"' -> read_string (Buffer.create 128) lexbuf
-  | space | newline -> read lexbuf
-  | eof -> EOF
-  | _ ->
-    raise
-      (SyntaxError
-         ("Unexpected character '" ^ Utf8.lexeme lexbuf ^ "' during lexing") )
diff --git a/src/lsc/lsc_parser.mly b/src/lsc/lsc_parser.mly
deleted file mode 100644
index e6b4e93..0000000
--- a/src/lsc/lsc_parser.mly
+++ /dev/null
@@ -1,75 +0,0 @@
-%{
-open Lsc_ast
-%}
-
-%token <string> VAR
-%token <string> SYM
-%token BAR
-%token NEQ
-%token COMMA
-%token PLUS MINUS
-%token CONS
-%token SEMICOLON
-%token PLACEHOLDER
-
-%right CONS
-
-%start <marked_constellation> constellation_file
-%start <marked_constellation> marked_constellation
-
-%%
-
-let constellation_file :=
-  | DOT?; EOL*; EOF;                               { [] }
-  | ~=marked_constellation; EOL*; DOT?; EOL*; EOF; <>
-
-let marked_constellation :=
-  | ~=separated_nonempty_list(pair(SEMICOLON, EOL*), star);
-    EOL*; SEMICOLON?; <>
-
-let star :=
-  | ~=bracks_opt(star_content);           <Unmarked>
-  | ~=bracks_opt(AT; EOL*; star_content); <Marked>
-
-let star_content :=
-  | LBRACK; EOL*; RBRACK;
-    { {content=[]; bans=[]} }
-  | l=separated_nonempty_list(pair(COMMA?, EOL*), ray); bs=bans?;
-    { {content=l; bans=Option.to_list bs |> List.concat } }
-
-%public let bans :=
-  | EOL*; BAR; EOL*; ~=separated_nonempty_list(COMMA?, ban); EOL*; <>
-
-let ban :=
-  | r1=ray; NEQ; r2=ray; EOL*;   { Ineq (r1, r2) }
-  | r1=ray; CONS; r2=ray;  { Incomp (r1, r2) }
-
-%public let symbol :=
-  | p=polarity; AMP; f = SYM; { noisy (p, f) }
-  | p=polarity; AMP; PRINT;   { noisy (p, "print") }
-  | p=polarity; f = SYM;      { muted (p, f) }
-  | f=SYM;                    { muted (Null, f) }
-
-let polarity :=
-  | PLUS;  { Pos }
-  | MINUS; { Neg }
-
-%public let ray :=
-  | PLACEHOLDER;         { to_var ("_"^(fresh_placeholder ())) }
-  | ~=VAR;               <to_var>
-  | pf=symbol; ts=args?; { to_func (pf, Option.to_list ts |> List.concat) }
-
-let ray_internal :=
-  | ~=ray;       <>
-  | ~=cons_expr; <>
-
-let args :=
-  | ~=pars(separated_nonempty_list(COMMA?, ray_internal)); <>
-
-let cons_expr :=
-  | r1=ray_internal; CONS; r2=ray_internal;
-    { to_func (muted (Null, ":"), [r1; r2]) }
-  | LPAR; r1=ray_internal; CONS; r2=ray_internal; RPAR;
-    { to_func (muted (Null, ":"), [r1; r2]) }
-  | e=pars(cons_expr); CONS; r=ray_internal;
-    { to_func (muted (Null, ":"), [e; r]) }
diff --git a/src/lsc/lsc_ast.ml b/src/lsc_ast.ml
similarity index 85%
rename from src/lsc/lsc_ast.ml
rename to src/lsc_ast.ml
index 88d4195..dcb3f06 100644
--- a/src/lsc/lsc_ast.ml
+++ b/src/lsc_ast.ml
@@ -1,8 +1,7 @@
 open Base
-open Common.Pretty
+open Pretty
 open Out_channel
 open In_channel
-open Lsc_err
 
 let ( let* ) x f = Result.bind x ~f
 
@@ -71,7 +70,7 @@ let rec compare_ray r1 r2 =
     String.compare (x ^ i') (y ^ j')
   | Func _, Var _ -> 1
   | Var _, Func _ -> -1
-  | Func ((_, pf1), args1), Func ((_, pf2), args2) -> begin
+  | Func (pf1, args1), Func (pf2, args2) -> begin
     match (pf1, pf2) with
     | pf1, pf2 when StellarSig.equal_idfunc pf1 pf2 ->
       List.compare compare_ray args1 args2
@@ -104,17 +103,13 @@ let neg f = (Neg, f)
 
 let null f = (Null, f)
 
-let muted pf = (Muted, pf)
-
-let noisy pf = (Noisy, pf)
-
 let gfunc c ts = Func (c, ts)
 
-let pfunc f ts = gfunc (muted (pos f)) ts
+let pfunc f ts = gfunc (pos f) ts
 
-let nfunc f ts = gfunc (muted (neg f)) ts
+let nfunc f ts = gfunc (neg f) ts
 
-let func f ts = gfunc (muted (null f)) ts
+let func f ts = gfunc (null f) ts
 
 let var x = Var x
 
@@ -125,7 +120,7 @@ let nconst f = nfunc f []
 let const f = func f []
 
 let is_polarised r : bool =
-  let aux = function _, (Pos, _) | _, (Neg, _) -> true | _ -> false in
+  let aux = function Pos, _ | Neg, _ -> true | _ -> false in
   exists_func aux r
 
 let replace_indices (i : int) : ray -> ray =
@@ -140,10 +135,7 @@ let raymatcher r r' : substitution option =
 
 let string_of_polarity = function Pos -> "+" | Neg -> "-" | Null -> ""
 
-let string_of_polsym (m, (p, f)) =
-  match m with
-  | Noisy -> string_of_polarity p ^ "#" ^ f
-  | Muted -> string_of_polarity p ^ f
+let string_of_polsym (p, f) = string_of_polarity p ^ f
 
 let string_of_var (x, i) =
   match i with None -> x | Some i' -> x ^ Int.to_string i'
@@ -151,9 +143,9 @@ let string_of_var (x, i) =
 let rec string_of_ray = function
   | Var xi -> string_of_var xi
   | Func (pf, []) -> string_of_polsym pf
-  | Func ((_, (Null, ":")), [ Func ((_, (Null, ":")), [ r1; r2 ]); r3 ]) ->
+  | Func ((Null, "%cons"), [ Func ((Null, "%cons"), [ r1; r2 ]); r3 ]) ->
     "(" ^ string_of_ray r1 ^ ":" ^ string_of_ray r2 ^ "):" ^ string_of_ray r3
-  | Func ((_, (Null, ":")), [ r1; r2 ]) ->
+  | Func ((Null, "%cons"), [ r1; r2 ]) ->
     string_of_ray r1 ^ ":" ^ string_of_ray r2
   | Func (pf, ts) ->
     string_of_polsym pf ^ surround "(" ")"
@@ -339,21 +331,6 @@ let fusion repl1 repl2 s1 s2 bans1 bans2 theta : star =
   ; bans = List.map (nbans1 @ nbans2) ~f:(fmap_ban ~f:(subst theta))
   }
 
-let apply_effect r theta : (unit, err_effect) Result.t =
-  match (r, theta) with
-  | Func ((Noisy, (_, "print")), _), [] -> Error (TooFewArgs "print")
-  | Func ((Noisy, (_, "print")), _), _ :: _ :: _ -> Error (TooManyArgs "print")
-  | Func ((Noisy, (_, "print")), _), [ (_, Func ((_, (Null, arg)), [])) ] ->
-    String.strip ~drop:(fun x -> equal_char x '\"') arg |> output_string stdout;
-    flush stdout;
-    Ok ()
-  | Func ((Noisy, (_, "print")), _), [ (_, arg) ] ->
-    output_string stdout (string_of_ray arg);
-    flush stdout;
-    Ok ()
-  | Func ((Noisy, (_, s)), _), _ -> Error (UnknownEffect s)
-  | _ -> Ok ()
-
 let pause () =
   flush stdout;
   let _ = input_line stdin in
@@ -383,10 +360,10 @@ let coherent_bans bans =
 
 (* interaction between one selected ray and one selected action *)
 let rec interaction ~showtrace ~queue repl1 repl2
-  (selected_action, other_actions) (selected_ray, other_rays, bans) :
-  (star list, err_effect) Result.t =
+  (selected_action, other_actions) (selected_ray, other_rays, bans) : star list
+    =
   match selected_action.content with
-  | [] -> Ok []
+  | [] -> []
   | r' :: s' when not (is_polarised r') ->
     interaction ~showtrace ~queue:(r' :: queue) repl1 repl2
       ({ content = s'; bans }, other_actions)
@@ -405,7 +382,6 @@ let rec interaction ~showtrace ~queue repl1 repl2
         (selected_ray, other_rays, bans)
     (* if there is an actual connection between rays *)
     | Some theta ->
-      let* _ = apply_effect selected_ray theta in
       begin
         if showtrace then
           output_string stdout
@@ -413,7 +389,7 @@ let rec interaction ~showtrace ~queue repl1 repl2
         if showtrace then pause ()
       end;
       (* action is consumed when execution is linear *)
-      let* next =
+      let next =
         interaction ~showtrace ~queue:(r' :: queue) repl1 repl2
           ({ content = s'; bans }, other_actions)
           (selected_ray, other_rays, bans)
@@ -423,29 +399,29 @@ let rec interaction ~showtrace ~queue repl1 repl2
         fusion repl1 repl2 other_rays other_rays' bans selected_action.bans
           theta
       in
-      let* res =
+      let res =
         if coherent_bans after_fusion.bans then begin
           let _ =
             if showtrace then
               output_string stdout
               @@ Printf.sprintf "  add star %s." (string_of_star after_fusion)
           in
-          Ok (after_fusion :: next)
+          after_fusion :: next
         end
         else begin
           if showtrace then
             output_string stdout
             @@ Printf.sprintf "  result filtered out by constraint.";
-          Ok next
+          next
         end
       in
       if showtrace then pause ();
       ident_counter := !ident_counter + 2;
-      Ok res )
+      res )
 
 (* search partner for a selected ray within a set of available actions *)
 let search_partners ~linear ~showtrace (selected_ray, other_rays, bans) actions
-  : (star list * star list, err_effect) Result.t =
+  : star list * star list =
   if showtrace then begin
     let str_ray = string_of_ray selected_ray in
     let str_rays = string_of_raylist other_rays in
@@ -455,29 +431,29 @@ let search_partners ~linear ~showtrace (selected_ray, other_rays, bans) actions
   end;
   let repl1 = replace_indices !ident_counter in
   let rec try_actions acc = function
-    | [] -> Ok ([], acc)
+    | [] -> ([], acc)
     | selected_action :: other_actions ->
       let repl2 = replace_indices (!ident_counter + 1) in
-      let* res =
+      let res =
         interaction ~showtrace ~queue:[] repl1 repl2
           (selected_action, other_actions)
           (selected_ray, other_rays, bans)
       in
       if (not @@ List.is_empty res) && linear then
-        let* next, new_actions = try_actions acc other_actions in
-        Ok (res @ next, new_actions)
+        let next, new_actions = try_actions acc other_actions in
+        (res @ next, new_actions)
       else
-        let* next, new_actions =
+        let next, new_actions =
           try_actions (selected_action :: acc) other_actions
         in
-        Ok (res @ next, new_actions)
+        (res @ next, new_actions)
   in
   try_actions [] actions
 
 let rec select_ray ~linear ~showtrace ~queue actions other_states
-  (selected_state, bans) : (star list option * star list, err_effect) Result.t =
+  (selected_state, bans) : star list option * star list =
   match selected_state with
-  | [] -> Ok (None, actions)
+  | [] -> (None, actions)
   (* if unpolarized, no need to try, try other stars *)
   | r :: rs when not (is_polarised r) ->
     select_ray ~linear ~showtrace ~queue:(r :: queue) actions other_states
@@ -490,16 +466,15 @@ let rec select_ray ~linear ~showtrace ~queue actions other_states
         actions
     with
     (* interaction did nothing (no partner), try other rays *)
-    | Ok ([], new_actions) ->
+    | [], new_actions ->
       select_ray ~linear ~showtrace ~queue:(selected_ray :: queue) new_actions
         other_states (other_rays, bans)
     (* interaction returns a result, keep it for the next round *)
-    | Ok (new_stars, new_actions) -> Ok (Some new_stars, new_actions)
-    | Error e -> Error e )
+    | new_stars, new_actions -> (Some new_stars, new_actions) )
 
 let rec select_star ~linear ~showtrace ~queue actions :
-  star list -> (star list option * star list, err_effect) Result.t = function
-  | [] -> Ok (None, actions)
+  star list -> star list option * star list = function
+  | [] -> (None, actions)
   (* select a state star and try finding a partner for each ray *)
   | selected_state :: other_states -> (
     match
@@ -507,21 +482,19 @@ let rec select_star ~linear ~showtrace ~queue actions :
         (selected_state.content, selected_state.bans)
     with
     (* no success with this star, try other stars *)
-    | Ok (None, new_actions) ->
+    | None, new_actions ->
       select_star ~linear ~showtrace new_actions
         ~queue:(selected_state :: queue) other_states
     (* got new stars to add, construct the result for the next round *)
-    | Ok (Some new_stars, new_actions) ->
-      Ok (Some (List.rev queue @ other_states @ new_stars), new_actions)
-    | Error e -> Error e )
+    | Some new_stars, new_actions ->
+      (Some (List.rev queue @ other_states @ new_stars), new_actions) )
 
 let string_of_cfg (actions, states) : string =
   Printf.sprintf ">> actions: %s\n>> states: %s\n"
     (string_of_constellation actions)
     (string_of_constellation states)
 
-let exec ?(showtrace = false) ?(linear = false) mcs :
-  (constellation, err_effect) Result.t =
+let exec ?(showtrace = false) ?(linear = false) mcs : constellation =
   (* do a sequence of rounds with a single interaction on state per round *)
   let rec loop ((actions, states) as cfg) =
     if showtrace then begin
@@ -529,9 +502,8 @@ let exec ?(showtrace = false) ?(linear = false) mcs :
       pause ()
     end;
     match select_star ~linear ~showtrace ~queue:[] actions states with
-    | Ok (None, _) -> Ok states (* no more possible interaction *)
-    | Ok (Some res, new_actions) -> loop (new_actions, res)
-    | Error e -> Error e
+    | None, _ -> states (* no more possible interaction *)
+    | Some res, new_actions -> loop (new_actions, res)
   in
   let cfg = extract_intspace mcs in
   if showtrace then
diff --git a/src/parser.mly b/src/parser.mly
new file mode 100644
index 0000000..3825941
--- /dev/null
+++ b/src/parser.mly
@@ -0,0 +1,51 @@
+%{
+open Expr.Raw
+%}
+
+%token <string> VAR
+%token <string> SYM
+%token <string> STRING
+%token AT
+%token BAR
+%token LPAR RPAR
+%token LBRACK RBRACK
+%token LBRACE RBRACE
+%token LANGLE RANGLE
+%token SHARP
+%token EOF
+
+%start <Expr.Raw.t list> expr_file
+
+%%
+
+let delimited_opt(l, x, r) :=
+  | ~=x; <>
+  | ~=delimited(l, x, r); <>
+
+let revlist(x) :=
+  | { [] }
+  | t=revlist(x); h=x; { h::t }
+
+let pars(x) == ~=delimited(LPAR, x, RPAR); <>
+let bracks(x) == ~=delimited(LBRACK, x, RBRACK); <>
+let bracks_opt(x) == ~=delimited_opt(LBRACK, x, RBRACK); <>
+
+let expr_file :=
+  | EOF; { [] }
+  | es=expr+; EOF; { es }
+
+let params :=
+  | BAR; BAR; ~=expr+; <>
+
+let expr :=
+  | ~=SYM; <Symbol>
+  | ~=VAR; <Var>
+  | ~=STRING; <String>
+  | SHARP; ~=expr; <Call>
+  | AT; ~=expr; <Focus>
+  | ~=pars(expr+); <List>
+  | LANGLE; es=revlist(expr); RANGLE; <Stack>
+  | LBRACK; es=revlist(expr); RBRACK; <Cons>
+  | LBRACE; es=revlist(expr); RBRACE; <Group>
+  | LBRACK; ~=revlist(expr); ~=params; RBRACK; <ConsWithParams>
+  | LBRACK; ~=revlist(expr); BAR; ~=expr; RBRACK; <ConsWithBase>
diff --git a/src/common/pretty.ml b/src/pretty.ml
similarity index 100%
rename from src/common/pretty.ml
rename to src/pretty.ml
diff --git a/src/sgen_ast.ml b/src/sgen_ast.ml
new file mode 100644
index 0000000..1c365cb
--- /dev/null
+++ b/src/sgen_ast.ml
@@ -0,0 +1,45 @@
+open Base
+open Lsc_ast
+
+type ident = StellarRays.term
+
+type idvar = string * int option
+
+type idfunc = polarity * string
+
+type sgen_expr =
+  | Raw of marked_constellation
+  | Id of ident
+  | Exec of bool * sgen_expr
+  | Group of sgen_expr list
+  | Subst of sgen_expr * substitution
+  | Focus of sgen_expr
+  | Clean of sgen_expr
+  | Kill of sgen_expr
+  | Process of sgen_expr list
+  | Eval of sgen_expr
+
+and substitution =
+  | Extend of idfunc
+  | Reduce of idfunc
+  | SVar of string * StellarRays.term
+  | SFunc of idfunc * idfunc
+  | SGal of ident * sgen_expr
+
+type err =
+  | ExpectError of marked_constellation * marked_constellation * ident
+  | UnknownID of string
+
+type env = { objs : (ident * sgen_expr) list }
+
+let initial_env = { objs = [] }
+
+type declaration =
+  | Def of ident * sgen_expr
+  | Show of sgen_expr
+  | Trace of sgen_expr
+  | Run of sgen_expr
+  | Expect of sgen_expr * sgen_expr * ident
+  | Use of ident
+
+type program = declaration list
diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml
new file mode 100644
index 0000000..1e466b2
--- /dev/null
+++ b/src/sgen_eval.ml
@@ -0,0 +1,269 @@
+open Base
+open Lsc_ast
+open Sgen_ast
+open Out_channel
+
+let ( let* ) x f = Result.bind x ~f
+
+let unifiable r r' = StellarRays.solution [ (r, r') ] |> Option.is_some
+
+let find_with_solution env x =
+  let rec aux = function
+    | [] -> None
+    | (key, value) :: rest -> (
+      match StellarRays.solution [ (key, x) ] with
+      | Some subst -> Some (value, subst)
+      | None -> aux rest )
+  in
+  aux env.objs
+
+let add_obj env x e = List.Assoc.add ~equal:unifiable env.objs x e
+
+let get_obj env x = find_with_solution env x
+
+let rec replace_id (xfrom : ident) (xto : sgen_expr) e :
+  (sgen_expr, err) Result.t =
+  match e with
+  | Id x when equal_ray x xfrom -> Ok xto
+  | Exec (b, e) ->
+    let* g = replace_id xfrom xto e in
+    Exec (b, g) |> Result.return
+  | Kill e ->
+    let* g = replace_id xfrom xto e in
+    Kill g |> Result.return
+  | Clean e ->
+    let* g = replace_id xfrom xto e in
+    Clean g |> Result.return
+  | Group es ->
+    let* gs = List.map ~f:(replace_id xfrom xto) es |> Result.all in
+    Group gs |> Result.return
+  | Focus e ->
+    let* g = replace_id xfrom xto e in
+    Focus g |> Result.return
+  | Subst (e, subst) ->
+    let* g = replace_id xfrom xto e in
+    Subst (g, subst) |> Result.return
+  | Process gs ->
+    let* procs = List.map ~f:(replace_id xfrom xto) gs |> Result.all in
+    Process procs |> Result.return
+  | Eval e ->
+    let* g = replace_id xfrom xto e in
+    Eval g |> Result.return
+  | Raw _ | Id _ -> e |> Result.return
+
+let rec map_sgen_expr env ~f : sgen_expr -> (sgen_expr, err) Result.t = function
+  | Raw g -> Raw (f g) |> Result.return
+  | Id x -> Id x |> Result.return
+  | Exec (b, e) ->
+    let* map_e = map_sgen_expr env ~f e in
+    Exec (b, map_e) |> Result.return
+  | Kill e ->
+    let* map_e = map_sgen_expr env ~f e in
+    Kill map_e |> Result.return
+  | Clean e ->
+    let* map_e = map_sgen_expr env ~f e in
+    Clean map_e |> Result.return
+  | Group es ->
+    let* map_es = List.map ~f:(map_sgen_expr env ~f) es |> Result.all in
+    Group map_es |> Result.return
+  | Subst (e, Extend pf) ->
+    let* map_e = map_sgen_expr env ~f e in
+    Subst (map_e, Extend pf) |> Result.return
+  | Subst (e, Reduce pf) ->
+    let* map_e = map_sgen_expr env ~f e in
+    Subst (map_e, Reduce pf) |> Result.return
+  | Focus e ->
+    let* map_e = map_sgen_expr env ~f e in
+    Focus map_e |> Result.return
+  | Subst (e, SVar (x, r)) ->
+    let* map_e = map_sgen_expr env ~f e in
+    Subst (map_e, SVar (x, r)) |> Result.return
+  | Subst (e, SFunc (pf, pf')) ->
+    let* map_e = map_sgen_expr env ~f e in
+    Subst (map_e, SFunc (pf, pf')) |> Result.return
+  | Subst (e', SGal (x, e)) ->
+    let* map_e = map_sgen_expr env ~f e in
+    let* map_e' = map_sgen_expr env ~f e' in
+    Subst (map_e', SGal (x, map_e)) |> Result.return
+  | Process gs ->
+    let* procs = List.map ~f:(map_sgen_expr env ~f) gs |> Result.all in
+    Process procs |> Result.return
+  | Eval e ->
+    let* map_e = map_sgen_expr env ~f e in
+    Eval map_e |> Result.return
+
+let subst_vars env _from _to =
+  map_sgen_expr env ~f:(subst_all_vars [ (_from, _to) ])
+
+let subst_funcs env _from _to =
+  map_sgen_expr env ~f:(subst_all_funcs [ (_from, _to) ])
+
+let pp_err e : (string, err) Result.t =
+  let red text = "\x1b[31m" ^ text ^ "\x1b[0m" in
+  let open Lsc_ast.StellarRays in
+  let open Printf in
+  match e with
+  | ExpectError (x, e, Func ((Null, f), [])) when equal_string f "default" ->
+    sprintf "%s:\n* expected: %s\n* got: %s\n" (red "Expect Error")
+      (e |> remove_mark_all |> string_of_constellation)
+      (x |> remove_mark_all |> string_of_constellation)
+    |> Result.return
+  | ExpectError (_x, _e, Func ((Null, f), [ t ])) when equal_string f "error" ->
+    sprintf "%s: %s\n" (red "Expect Error") (string_of_ray t) |> Result.return
+  | ExpectError (_x, _e, message) ->
+    sprintf "%s\n" (string_of_ray message) |> Result.return
+  | UnknownID x ->
+    sprintf "%s: identifier '%s' not found.\n" (red "UnknownID Error") x
+    |> Result.return
+
+let rec eval_sgen_expr (env : env) :
+  sgen_expr -> (marked_constellation, err) Result.t = function
+  | Raw mcs -> Ok mcs
+  | Id x -> begin
+    match get_obj env x with
+    | None -> Error (UnknownID (string_of_ray x))
+    | Some (g, subst) ->
+      let result =
+        List.fold_result subst ~init:g ~f:(fun g_acc (xfrom, xto) ->
+          subst_vars env xfrom xto g_acc )
+      in
+      Result.bind result ~f:(eval_sgen_expr env)
+  end
+  | Group es ->
+    let* eval_es = List.map ~f:(eval_sgen_expr env) es |> Result.all in
+    let* mcs = Ok eval_es in
+    Ok (List.concat mcs)
+  | Exec (b, e) ->
+    let* eval_e = eval_sgen_expr env e in
+    Ok (exec ~linear:b ~showtrace:false eval_e |> unmark_all)
+  | Focus e ->
+    let* eval_e = eval_sgen_expr env e in
+    eval_e |> remove_mark_all |> focus |> Result.return
+  | Kill e ->
+    let* eval_e = eval_sgen_expr env e in
+    eval_e |> remove_mark_all |> kill |> focus |> Result.return
+  | Clean e ->
+    let* eval_e = eval_sgen_expr env e in
+    eval_e |> remove_mark_all |> clean |> focus |> Result.return
+  | Process [] -> Ok []
+  | Process (h :: t) ->
+    let* eval_e = eval_sgen_expr env h in
+    let init = eval_e |> remove_mark_all |> focus in
+    let* res =
+      List.fold_left t ~init:(Ok init) ~f:(fun acc x ->
+        let* acc = acc in
+        match x with
+        | Id (Func ((Null, "&kill"), [])) ->
+          acc |> remove_mark_all |> kill |> focus |> Result.return
+        | Id (Func ((Null, "&clean"), [])) ->
+          acc |> remove_mark_all |> clean |> focus |> Result.return
+        | _ ->
+          let origin = acc |> remove_mark_all |> focus in
+          eval_sgen_expr env (Focus (Exec (false, Group [ x; Raw origin ]))) )
+    in
+    res |> Result.return
+  | Subst (e, Extend pf) ->
+    let* eval_e = eval_sgen_expr env e in
+    List.map eval_e ~f:(map_mstar ~f:(fun r -> gfunc pf [ r ])) |> Result.return
+  | Subst (e, Reduce pf) ->
+    let* eval_e = eval_sgen_expr env e in
+    List.map eval_e
+      ~f:
+        (map_mstar ~f:(fun r ->
+           match r with
+           | StellarRays.Func (pf', ts)
+             when StellarSig.equal_idfunc pf pf' && List.length ts = 1 ->
+             List.hd_exn ts
+           | _ -> r ) )
+    |> Result.return
+  | Subst (e, SVar (x, r)) ->
+    let* subst = subst_vars env (x, None) r e in
+    eval_sgen_expr env subst
+  | Subst (e, SFunc (pf1, pf2)) ->
+    let* subst = subst_funcs env pf1 pf2 e in
+    eval_sgen_expr env subst
+  | Subst (e, SGal (x, _to)) ->
+    let* fill = replace_id x _to e in
+    eval_sgen_expr env fill
+  | Eval e -> (
+    let* eval_e = eval_sgen_expr env e in
+    match eval_e with
+    | [ Marked { content = [ r ]; bans = _ } ]
+    | [ Unmarked { content = [ r ]; bans = _ } ] ->
+      r |> expr_of_ray |> Expr.sgen_expr_of_expr |> eval_sgen_expr env
+    | e ->
+      failwith
+        ( "eval error: "
+        ^ string_of_constellation (remove_mark_all e)
+        ^ " is not a ray." ) )
+
+and expr_of_ray = function
+  | Var (x, None) -> Expr.Var x
+  | Var (x, Some i) -> Expr.Var (x ^ Int.to_string i)
+  | Func (pf, []) -> Symbol (Lsc_ast.string_of_polsym pf)
+  | Func (pf, args) ->
+    Expr.List
+      (Symbol (Lsc_ast.string_of_polsym pf) :: List.map ~f:expr_of_ray args)
+
+let rec eval_decl env : declaration -> (env, err) Result.t = function
+  | Def (x, e) ->
+    let env = { objs = add_obj env x e } in
+    Ok env
+  | Show (Raw mcs) ->
+    mcs |> remove_mark_all |> string_of_constellation |> Stdlib.print_string;
+    Stdlib.print_newline ();
+    Stdlib.flush Stdlib.stdout;
+    Ok env
+  | Show e ->
+    let* eval_e = eval_sgen_expr env e in
+    List.map eval_e ~f:remove_mark
+    |> string_of_constellation |> Stdlib.print_string;
+    Stdlib.print_newline ();
+    Ok env
+  | Trace e ->
+    let* eval_e = eval_sgen_expr env e in
+    let _ = exec ~showtrace:true eval_e in
+    Ok env
+  | Run e ->
+    let _ = eval_sgen_expr env (Exec (false, e)) in
+    Ok env
+  | Expect (e1, e2, message) ->
+    let* eval_e1 = eval_sgen_expr env e1 in
+    let* eval_e2 = eval_sgen_expr env e2 in
+    let normalize x = x |> remove_mark_all |> unmark_all in
+    if not @@ equal_mconstellation (normalize eval_e1) (normalize eval_e2) then
+      Error (ExpectError (eval_e1, eval_e2, message))
+    else Ok env
+  | Use path ->
+    let open Lsc_ast.StellarRays in
+    let formatted_filename : string =
+      match path with
+      | Func ((Null, f), [ s ]) when equal_string f "%string" -> string_of_ray s
+      | path -> string_of_ray path ^ ".sg"
+    in
+    let lexbuf =
+      Sedlexing.Utf8.from_channel (Stdlib.open_in formatted_filename)
+    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 formatted_filename);
+    let expr = Sgen_parsing.parse_with_error lexbuf in
+    let preprocessed = Expr.preprocess expr in
+    let p = Expr.program_of_expr preprocessed in
+    let* env = eval_program p in
+    Ok env
+
+and eval_program (p : program) =
+  match
+    List.fold_left
+      ~f:(fun acc x ->
+        let* acc = acc in
+        eval_decl acc x )
+      ~init:(Ok initial_env) p
+  with
+  | Ok env -> Ok env
+  | Error e ->
+    let* pp = pp_err e in
+    output_string stderr pp;
+    Error e
diff --git a/src/stellogen/sgen_parsing.ml b/src/sgen_parsing.ml
similarity index 92%
rename from src/stellogen/sgen_parsing.ml
rename to src/sgen_parsing.ml
index 95006e4..a3bffec 100644
--- a/src/stellogen/sgen_parsing.ml
+++ b/src/sgen_parsing.ml
@@ -1,6 +1,6 @@
 open Lexing
-open Sgen_lexer
-open Sgen_parser
+open Lexer
+open Parser
 
 let print_position fmt (pos : Lexing.position) =
   Format.fprintf fmt "%s:%d:%d" pos.pos_fname pos.pos_lnum
@@ -8,7 +8,7 @@ let print_position fmt (pos : Lexing.position) =
 
 let parse_with_error lexbuf =
   let lexer = Sedlexing.with_tokenizer read lexbuf in
-  let parser = MenhirLib.Convert.Simplified.traditional2revised program in
+  let parser = MenhirLib.Convert.Simplified.traditional2revised expr_file in
   try parser lexer
   with SyntaxError msg ->
     let _start_pos, end_pos = Sedlexing.lexing_positions lexbuf in
diff --git a/src/stellogen/dune b/src/stellogen/dune
deleted file mode 100644
index 82edf30..0000000
--- a/src/stellogen/dune
+++ /dev/null
@@ -1,15 +0,0 @@
-(library
- (name stellogen)
- (libraries base common menhirLib)
- (preprocess
-  (pps sedlex.ppx)))
-
-(env
- (dev
-  (flags
-   (:standard -warn-error -A))))
-
-(menhir
- (modules ../common/common_parser lsc_parser sgen_parser)
- (merge_into sgen_parser)
- (flags --table --explain --dump))
diff --git a/src/stellogen/lsc_ast.ml b/src/stellogen/lsc_ast.ml
deleted file mode 120000
index 6c30619..0000000
--- a/src/stellogen/lsc_ast.ml
+++ /dev/null
@@ -1 +0,0 @@
-../lsc/lsc_ast.ml
\ No newline at end of file
diff --git a/src/stellogen/lsc_err.ml b/src/stellogen/lsc_err.ml
deleted file mode 120000
index 47e4f3c..0000000
--- a/src/stellogen/lsc_err.ml
+++ /dev/null
@@ -1 +0,0 @@
-../lsc/lsc_err.ml
\ No newline at end of file
diff --git a/src/stellogen/lsc_parser.mly b/src/stellogen/lsc_parser.mly
deleted file mode 120000
index ea060e8..0000000
--- a/src/stellogen/lsc_parser.mly
+++ /dev/null
@@ -1 +0,0 @@
-../lsc/lsc_parser.mly
\ No newline at end of file
diff --git a/src/stellogen/sgen_ast.ml b/src/stellogen/sgen_ast.ml
deleted file mode 100644
index 461053e..0000000
--- a/src/stellogen/sgen_ast.ml
+++ /dev/null
@@ -1,75 +0,0 @@
-open Base
-open Lsc_ast
-
-type ident = StellarRays.term
-
-type idvar = string * int option
-
-type idfunc = polarity * string
-
-type ray_prefix = StellarRays.fmark * idfunc
-
-type type_declaration =
-  | TDef of ident * (ident * ident option) list
-  | TExp of ident * galaxy_expr
-
-and galaxy =
-  | Const of marked_constellation
-  | Galaxy of galaxy_declaration list
-  | Interface of type_declaration list
-
-and galaxy_declaration =
-  | GTypeDef of type_declaration
-  | GLabelDef of ident * galaxy_expr
-
-and galaxy_expr =
-  | Raw of galaxy
-  | Access of galaxy_expr * ident
-  | Id of ident
-  | Exec of galaxy_expr
-  | LinExec of galaxy_expr
-  | Union of galaxy_expr * galaxy_expr
-  | Subst of galaxy_expr * substitution
-  | Focus of galaxy_expr
-  | Clean of galaxy_expr
-  | Kill of galaxy_expr
-  | Process of galaxy_expr list
-
-and substitution =
-  | Extend of ray_prefix
-  | Reduce of ray_prefix
-  | SVar of string * StellarRays.term
-  | SFunc of (StellarRays.fmark * idfunc) * (StellarRays.fmark * idfunc)
-  | SGal of ident * galaxy_expr
-
-let reserved_words = [ const "clean"; const "kill" ]
-
-let is_reserved = List.mem reserved_words ~equal:equal_ray
-
-type env =
-  { objs : (ident * galaxy_expr) list
-  ; types : (ident * (ident * ident option) list) list
-  }
-
-let expect (g : galaxy_expr) : galaxy_expr =
-  Raw
-    (Galaxy
-       [ GLabelDef (const "interaction", Id (const "tested"))
-       ; GLabelDef (const "expect", g)
-       ] )
-
-let initial_env =
-  { objs = [ (const "^empty", Raw (Const [])) ]
-  ; types = [ (const "^empty", [ (const "^empty", None) ]) ]
-  }
-
-type declaration =
-  | Def of ident * galaxy_expr
-  | Show of galaxy_expr
-  | ShowExec of galaxy_expr
-  | Trace of galaxy_expr
-  | Run of galaxy_expr
-  | TypeDef of type_declaration
-  | Use of ident list
-
-type program = declaration list
diff --git a/src/stellogen/sgen_err.ml b/src/stellogen/sgen_err.ml
deleted file mode 100644
index 4b956c5..0000000
--- a/src/stellogen/sgen_err.ml
+++ /dev/null
@@ -1,11 +0,0 @@
-open Base
-open Sgen_ast
-
-type err =
-  | IllFormedChecker
-  | ExpectedGalaxy
-  | ReservedWord of string
-  | UnknownField of string
-  | UnknownID of string
-  | TestFailed of string * string * string * galaxy * galaxy
-  | LscError of Lsc_err.err_effect
diff --git a/src/stellogen/sgen_eval.ml b/src/stellogen/sgen_eval.ml
deleted file mode 100644
index 490f2a2..0000000
--- a/src/stellogen/sgen_eval.ml
+++ /dev/null
@@ -1,526 +0,0 @@
-open Base
-open Lsc_ast
-open Lsc_err
-open Sgen_ast
-open Sgen_err
-open Common.Format_exn
-open Common.Pretty
-open Out_channel
-
-let ( let* ) x f = Result.bind x ~f
-
-let add_obj env x e = List.Assoc.add ~equal:equal_ray env.objs x e
-
-let get_obj env x = List.Assoc.find ~equal:equal_ray env.objs x
-
-let add_type env x e = List.Assoc.add ~equal:equal_ray env.types x e
-
-let get_type env x = List.Assoc.find ~equal:equal_ray env.types x
-
-let rec map_galaxy env ~f : galaxy -> (galaxy, err) Result.t = function
-  | Const mcs -> Const (f mcs) |> Result.return
-  | Interface i -> Interface i |> Result.return
-  | Galaxy g ->
-    let* g' =
-      List.map g ~f:(function
-        | GTypeDef tdef -> GTypeDef tdef |> Result.return
-        | GLabelDef (k, v) ->
-          let* map_v = map_galaxy_expr env ~f v in
-          GLabelDef (k, map_v) |> Result.return )
-      |> Result.all
-    in
-    Galaxy g' |> Result.return
-
-and map_galaxy_expr env ~f : galaxy_expr -> (galaxy_expr, err) Result.t =
-  function
-  | Raw g ->
-    let* map_g = map_galaxy env ~f g in
-    Raw map_g |> Result.return
-  | Access (e, x) ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Access (map_e, x) |> Result.return
-  | Id x when is_reserved x -> Ok (Id x)
-  | Id x -> begin
-    match get_obj env x with
-    | None -> Error (UnknownID (string_of_ray x))
-    | Some g -> map_galaxy_expr env ~f g
-  end
-  | Exec e ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Exec map_e |> Result.return
-  | Kill e ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Kill map_e |> Result.return
-  | Clean e ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Clean map_e |> Result.return
-  | LinExec e ->
-    let* map_e = map_galaxy_expr env ~f e in
-    LinExec map_e |> Result.return
-  | Union (e, e') ->
-    let* map_e = map_galaxy_expr env ~f e in
-    let* map_e' = map_galaxy_expr env ~f e' in
-    Union (map_e, map_e') |> Result.return
-  | Subst (e, Extend pf) ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Subst (map_e, Extend pf) |> Result.return
-  | Subst (e, Reduce pf) ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Subst (map_e, Reduce pf) |> Result.return
-  | Focus e ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Focus map_e |> Result.return
-  | Subst (e, SVar (x, r)) ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Subst (map_e, SVar (x, r)) |> Result.return
-  | Subst (e, SFunc (pf, pf')) ->
-    let* map_e = map_galaxy_expr env ~f e in
-    Subst (map_e, SFunc (pf, pf')) |> Result.return
-  | Subst (e', SGal (x, e)) ->
-    let* map_e = map_galaxy_expr env ~f e in
-    let* map_e' = map_galaxy_expr env ~f e' in
-    Subst (map_e', SGal (x, map_e)) |> Result.return
-  | Process gs ->
-    let* procs = List.map ~f:(map_galaxy_expr env ~f) gs |> Result.all in
-    Process procs |> Result.return
-
-let rec replace_id env (_from : ident) (_to : galaxy_expr) e :
-  (galaxy_expr, err) Result.t =
-  match e with
-  | Id x when is_reserved x -> Ok (Id x)
-  | Id x when equal_ray x _from -> Ok _to
-  | Access (g, x) ->
-    let* g' = replace_id env _from _to g in
-    Access (g', x) |> Result.return
-  | Exec e ->
-    let* g = replace_id env _from _to e in
-    Exec g |> Result.return
-  | Kill e ->
-    let* g = replace_id env _from _to e in
-    Kill g |> Result.return
-  | Clean e ->
-    let* g = replace_id env _from _to e in
-    Clean g |> Result.return
-  | LinExec e ->
-    let* g = replace_id env _from _to e in
-    LinExec g |> Result.return
-  | Union (e1, e2) ->
-    let* g1 = replace_id env _from _to e1 in
-    let* g2 = replace_id env _from _to e2 in
-    Union (g1, g2) |> Result.return
-  | Focus e ->
-    let* g = replace_id env _from _to e in
-    Focus g |> Result.return
-  | Subst (e, subst) ->
-    let* g = replace_id env _from _to e in
-    Subst (g, subst) |> Result.return
-  | Process gs ->
-    let* procs = List.map ~f:(replace_id env _from _to) gs |> Result.all in
-    Process procs |> Result.return
-  | Raw _ | Id _ -> e |> Result.return
-
-let subst_vars env _from _to =
-  map_galaxy_expr env ~f:(subst_all_vars [ (_from, _to) ])
-
-let subst_funcs env _from _to =
-  map_galaxy_expr env ~f:(subst_all_funcs [ (_from, _to) ])
-
-let group_galaxy :
-     galaxy_declaration list
-  -> type_declaration list * (StellarRays.term * galaxy_expr) list =
-  List.fold_left ~init:([], []) ~f:(function types, fields ->
-    (function
-    | GTypeDef d -> (d :: types, fields)
-    | GLabelDef (x, g') -> (types, (x, g') :: fields) ) )
-
-let rec typecheck_galaxy ~notyping env (g : galaxy_declaration list) :
-  (unit, err) Result.t =
-  let types, fields = group_galaxy g in
-  List.map types ~f:(function
-    | TExp (x, g) ->
-      let checker = expect g in
-      let new_env = { types = env.types; objs = fields @ env.objs } in
-      typecheck ~notyping new_env x (const "^empty") checker
-    | TDef (x, ts) ->
-      List.map ts ~f:(fun (t, ck) ->
-        let* checker =
-          match ck with
-          | None -> Ok default_checker
-          | Some xck -> begin
-            match get_obj env xck with
-            | None -> Error (UnknownID (string_of_ray xck))
-            | Some g -> Ok g
-          end
-        in
-        let new_env = { types = env.types; objs = fields @ env.objs } in
-        typecheck ~notyping new_env x t checker )
-      |> Result.all_unit )
-  |> Result.all_unit
-
-and pp_err ~notyping e : (string, err) Result.t =
-  match e with
-  | IllFormedChecker -> "Ill-formed checker.\n" |> Result.return
-  | ExpectedGalaxy -> "Expected galaxy.\n" |> Result.return
-  | ReservedWord x ->
-    Printf.sprintf "%s: identifier '%s' is reserved.\n"
-      (red "ReservedWord Error") x
-    |> Result.return
-  | UnknownField x ->
-    Printf.sprintf "%s: field '%s' not found.\n" (red "UnknownField Error") x
-    |> Result.return
-  | UnknownID x ->
-    Printf.sprintf "%s: identifier '%s' not found.\n" (red "UnknownID Error") x
-    |> Result.return
-  | TestFailed (x, t, id, got, expected) ->
-    let* eval_got = galaxy_to_constellation ~notyping initial_env got in
-    let* eval_exp = galaxy_to_constellation ~notyping initial_env expected in
-    Printf.sprintf "%s: %s.\nChecking %s :: %s\n* got: %s\n* expected: %s\n"
-      (red "TestFailed Error")
-      ( if equal_string id "_" then "unique test of '" ^ t ^ "' failed"
-        else "test '" ^ id ^ "' failed" )
-      x t
-      (eval_got |> List.map ~f:remove_mark |> string_of_constellation)
-      (eval_exp |> List.map ~f:remove_mark |> string_of_constellation)
-    |> Result.return
-  | LscError e -> pp_err_effect e |> Result.return
-
-and eval_galaxy_expr ~notyping (env : env) :
-  galaxy_expr -> (galaxy, err) Result.t = function
-  | Raw (Galaxy g) ->
-    let* _ = if notyping then Ok () else typecheck_galaxy ~notyping env g in
-    Ok (Galaxy g)
-  | Raw (Const mcs) -> Ok (Const mcs)
-  | Raw (Interface _) -> Ok (Interface [])
-  | Access (e, x) -> begin
-    match eval_galaxy_expr ~notyping env e with
-    | Ok (Const _) -> Error (UnknownField (string_of_ray x))
-    | Ok (Interface _) -> Error (UnknownField (string_of_ray x))
-    | Ok (Galaxy g) -> (
-      let _, fields = group_galaxy g in
-      try
-        fields |> fun g ->
-        List.Assoc.find_exn ~equal:equal_ray g x
-        |> eval_galaxy_expr ~notyping env
-      with Not_found_s _ -> Error (UnknownField (string_of_ray x)) )
-    | Error e -> Error e
-  end
-  | Id x -> begin
-    begin
-      match get_obj env x with
-      | None -> Error (UnknownID (string_of_ray x))
-      | Some g -> eval_galaxy_expr ~notyping env g
-    end
-  end
-  | Union (e, e') ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* eval_e' = eval_galaxy_expr ~notyping env e' in
-    let* mcs1 = eval_e |> galaxy_to_constellation ~notyping env in
-    let* mcs2 = eval_e' |> galaxy_to_constellation ~notyping env in
-    Ok (Const (mcs1 @ mcs2))
-  | Exec e ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    begin
-      match exec ~linear:false ~showtrace:false mcs with
-      | Ok res -> Ok (Const (unmark_all res))
-      | Error e -> Error (LscError e)
-    end
-  | LinExec e ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    begin
-      match exec ~linear:true ~showtrace:false mcs with
-      | Ok mcs -> Ok (Const (unmark_all mcs))
-      | Error e -> Error (LscError e)
-    end
-  | Focus e ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    Const (mcs |> remove_mark_all |> focus) |> Result.return
-  | Kill e ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    Const (mcs |> remove_mark_all |> kill |> focus) |> Result.return
-  | Clean e ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    Const (mcs |> remove_mark_all |> clean |> focus) |> Result.return
-  | Process [] -> Ok (Const [])
-  | Process (h :: t) ->
-    let* eval_e = eval_galaxy_expr ~notyping env h in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    let init = mcs |> remove_mark_all |> focus in
-    let* res =
-      List.fold_left t ~init:(Ok init) ~f:(fun acc x ->
-        let* acc = acc in
-        match x with
-        | Id (Func ((Muted, (Null, "kill")), [])) ->
-          acc |> remove_mark_all |> kill |> focus |> Result.return
-        | Id (Func ((Muted, (Null, "clean")), [])) ->
-          acc |> remove_mark_all |> clean |> focus |> Result.return
-        | _ ->
-          let origin = acc |> remove_mark_all |> focus in
-          let* ev =
-            eval_galaxy_expr ~notyping env
-              (Focus (Exec (Union (x, Raw (Const origin)))))
-          in
-          galaxy_to_constellation ~notyping env ev )
-    in
-    Const res |> Result.return
-  | Subst (e, Extend pf) ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    Const (List.map mcs ~f:(map_mstar ~f:(fun r -> gfunc pf [ r ])))
-    |> Result.return
-  | Subst (e, Reduce pf) ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    Const
-      (List.map mcs
-         ~f:
-           (map_mstar ~f:(fun r ->
-              match r with
-              | StellarRays.Func (pf', ts)
-                when StellarSig.equal_idfunc (snd pf) (snd pf')
-                     && List.length ts = 1 ->
-                List.hd_exn ts
-              | _ -> r ) ) )
-    |> Result.return
-  | Subst (e, SVar (x, r)) ->
-    let* subst = subst_vars env (x, None) r e in
-    eval_galaxy_expr ~notyping env subst
-  | Subst (e, SFunc (pf1, pf2)) ->
-    let* subst = subst_funcs env pf1 pf2 e in
-    eval_galaxy_expr ~notyping env subst
-  | Subst (e, SGal (x, _to)) ->
-    let* fill = replace_id env x _to e in
-    eval_galaxy_expr ~notyping env fill
-
-and galaxy_to_constellation ~notyping env :
-  galaxy -> (marked_constellation, err) Result.t = function
-  | Const mcs -> Ok mcs
-  | Interface _ -> Ok []
-  | Galaxy g ->
-    let _, fields = group_galaxy g in
-    List.fold_left fields ~init:(Ok []) ~f:(fun acc (_, v) ->
-      let* acc = acc in
-      let* eval_v = eval_galaxy_expr ~notyping env v in
-      let* mcs = galaxy_to_constellation ~notyping env eval_v in
-      Ok (mcs @ acc) )
-
-and equal_galaxy ~notyping env g g' =
-  let* mcs = galaxy_to_constellation ~notyping env g in
-  let* mcs' = galaxy_to_constellation ~notyping env g' in
-  equal_mconstellation mcs mcs' |> Result.return
-
-and check_interface ~notyping env x i =
-  let* g =
-    match get_obj env x with
-    | Some (Raw (Galaxy g)) -> Ok g
-    | Some _ -> Error ExpectedGalaxy
-    | None -> Error (UnknownID (string_of_ray x))
-  in
-  let type_decls = List.map i ~f:(fun t -> GTypeDef t) in
-  typecheck_galaxy ~notyping env (type_decls @ g)
-
-and typecheck ~notyping env x (t : StellarRays.term) (ck : galaxy_expr) :
-  (unit, err) Result.t =
-  let* gtests : (StellarRays.term * galaxy_expr) list =
-    match get_obj env t with
-    | Some (Raw (Const mcs)) -> Ok [ (const "_", Raw (Const mcs)) ]
-    | Some (Raw (Interface i)) ->
-      let* _ = check_interface ~notyping env x i in
-      Ok []
-    | Some (Raw (Galaxy gtests)) -> group_galaxy gtests |> snd |> Result.return
-    | Some e ->
-      let* eval_e = eval_galaxy_expr ~notyping env e in
-      let* mcs = galaxy_to_constellation ~notyping env eval_e in
-      [ (const "test", Raw (Const mcs)) ] |> Result.return
-    | None -> Error (UnknownID (string_of_ray t))
-  in
-  let testing =
-    List.map gtests ~f:(fun (idtest, test) ->
-      match ck with
-      | Raw (Galaxy gck) ->
-        let format =
-          try
-            List.Assoc.find_exn ~equal:equal_ray
-              (group_galaxy gck |> snd)
-              (const "interaction")
-          with Not_found_s _ -> default_interaction
-        in
-        begin
-          match get_obj env x with
-          | None -> Error (UnknownID (string_of_ray x))
-          | Some obj_x ->
-            Ok
-              ( idtest
-              , Exec
-                  (Subst
-                     ( Subst (format, SGal (const "test", test))
-                     , SGal (const "tested", obj_x) ) )
-                |> eval_galaxy_expr ~notyping env )
-        end
-      | _ -> Error IllFormedChecker )
-  in
-  let expect = Access (ck, const "expect") in
-  let* eval_exp = eval_galaxy_expr ~notyping env expect in
-  List.map testing ~f:(function
-    | Ok (idtest, got) ->
-      let* got = got in
-      let* eq = equal_galaxy ~notyping env got eval_exp in
-      if not eq then
-        Error
-          (TestFailed
-             ( string_of_ray x
-             , string_of_ray t
-             , string_of_ray idtest
-             , got
-             , eval_exp ) )
-      else Ok ()
-    | Error e -> Error e )
-  |> Result.all_unit
-
-and default_interaction = Union (Focus (Id (const "tested")), Id (const "test"))
-
-and default_expect =
-  Raw (Const [ Unmarked { content = [ func "ok" [] ]; bans = [] } ])
-
-and default_checker : galaxy_expr =
-  Raw
-    (Galaxy
-       [ GLabelDef (const "interaction", default_interaction)
-       ; GLabelDef (const "expect", default_expect)
-       ] )
-
-and string_of_type_expr (t, ck) =
-  match ck with
-  | None -> Printf.sprintf "%s" (string_of_ray t)
-  | Some xck -> Printf.sprintf "%s [%s]" (string_of_ray t) (string_of_ray xck)
-
-and string_of_type_declaration ~notyping env = function
-  | TDef (x, ts) ->
-    let str_x = string_of_ray x in
-    let str_ts = List.map ts ~f:string_of_type_expr in
-    Printf.sprintf "  %s :: %s.\n" str_x (string_of_list Fn.id ";" str_ts)
-  | TExp (x, g) -> (
-    match eval_galaxy_expr ~notyping env g with
-    | Error _ -> failwith "Error: string_of_type_declaration"
-    | Ok eval_g ->
-      let str_x = string_of_ray x in
-      Printf.sprintf "%s :=: %s" str_x (string_of_galaxy ~notyping env eval_g) )
-
-and string_of_galaxy_declaration ~notyping env = function
-  | GLabelDef (k, v) -> begin
-    match eval_galaxy_expr ~notyping env v with
-    | Error _ -> failwith "Error: string_of_galaxy_declaration"
-    | Ok eval_v ->
-      let str_k = string_of_ray k in
-      Printf.sprintf "  %s = %s\n" str_k (string_of_galaxy ~notyping env eval_v)
-  end
-  | GTypeDef decl -> string_of_type_declaration ~notyping env decl
-
-and string_of_galaxy ~notyping env : galaxy -> string = function
-  | Const mcs -> mcs |> remove_mark_all |> string_of_constellation
-  | Interface i ->
-    let content =
-      string_of_list (string_of_type_declaration ~notyping env) "" i
-    in
-    Printf.sprintf "interface\n%send" content
-  | Galaxy g ->
-    Printf.sprintf "galaxy\n%send"
-      (string_of_list (string_of_galaxy_declaration ~notyping env) "" g)
-
-let rec eval_decl ~typecheckonly ~notyping env :
-  declaration -> (env, err) Result.t = function
-  | Def (x, _) when is_reserved x -> Error (ReservedWord (string_of_ray x))
-  | Def (x, e) ->
-    let env = { objs = add_obj env x e; types = env.types } in
-    let* _ =
-      if notyping then Ok ()
-      else
-        List.filter env.types ~f:(fun (y, _) -> equal_ray x y)
-        |> List.map ~f:(fun (_, ts) ->
-             List.map ts ~f:(fun (t, ck) ->
-               match ck with
-               | None -> typecheck ~notyping env x t default_checker
-               | Some xck -> begin
-                 match get_obj env xck with
-                 | None -> Error (UnknownID (string_of_ray xck))
-                 | Some obj_xck -> typecheck ~notyping env x t obj_xck
-               end ) )
-        |> List.concat |> Result.all_unit
-    in
-    Ok env
-  | Show _ when typecheckonly -> Ok env
-  | Show (Id x) -> begin
-    match get_obj env x with
-    | None -> Error (UnknownID (string_of_ray x))
-    | Some e -> eval_decl ~typecheckonly ~notyping env (Show e)
-  end
-  | Show (Raw (Galaxy g)) ->
-    Galaxy g |> string_of_galaxy ~notyping env |> Stdlib.print_string;
-    Stdlib.print_newline ();
-    Stdlib.flush Stdlib.stdout;
-    Ok env
-  | Show (Raw (Interface i)) ->
-    Interface i |> string_of_galaxy ~notyping env |> Stdlib.print_string;
-    Stdlib.print_newline ();
-    Stdlib.flush Stdlib.stdout;
-    Ok env
-  | Show e ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    List.map mcs ~f:remove_mark
-    |> string_of_constellation |> Stdlib.print_string;
-    Stdlib.print_newline ();
-    Ok env
-  | ShowExec _ when typecheckonly -> Ok env
-  | ShowExec e -> eval_decl ~typecheckonly ~notyping env (Show (Exec e))
-  | Trace _ when typecheckonly -> Ok env
-  | Trace e ->
-    let* eval_e = eval_galaxy_expr ~notyping env e in
-    let* mcs = galaxy_to_constellation ~notyping env eval_e in
-    begin
-      match exec ~showtrace:true mcs with
-      | Ok _ -> Ok env
-      | Error e -> Error (LscError e)
-    end
-  | Run _ when typecheckonly -> Ok env
-  | Run e ->
-    let _ = eval_galaxy_expr ~notyping env (Exec e) in
-    Ok env
-  | TypeDef _ when notyping -> Ok env
-  | TypeDef (TDef (x, ts)) -> Ok { objs = env.objs; types = add_type env x ts }
-  | TypeDef (TExp (x, mcs)) ->
-    Ok
-      { objs = add_obj env (const "^expect") (expect mcs)
-      ; types = add_type env x [ (const "^empty", Some (const "^expect")) ]
-      }
-  | Use path ->
-    let path = List.map path ~f:string_of_ray in
-    let formatted_filename = String.concat ~sep:"/" path ^ ".sg" in
-    let lexbuf =
-      Sedlexing.Utf8.from_channel (Stdlib.open_in formatted_filename)
-    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 formatted_filename);
-    let p = Sgen_parsing.parse_with_error lexbuf in
-    let* env = eval_program ~typecheckonly ~notyping p in
-    Ok env
-
-and eval_program ~typecheckonly ~notyping p =
-  match
-    List.fold_left
-      ~f:(fun acc x ->
-        let* acc = acc in
-        eval_decl ~typecheckonly ~notyping acc x )
-      ~init:(Ok initial_env) p
-  with
-  | Ok env -> Ok env
-  | Error e ->
-    let* pp = pp_err ~notyping e in
-    output_string stderr pp;
-    Error e
diff --git a/src/stellogen/sgen_lexer.ml b/src/stellogen/sgen_lexer.ml
deleted file mode 100644
index cc5a794..0000000
--- a/src/stellogen/sgen_lexer.ml
+++ /dev/null
@@ -1,110 +0,0 @@
-open Sgen_parser
-
-exception SyntaxError of string
-
-let update_pos_newline lexbuf =
-  Sedlexing.new_line lexbuf;
-  EOL
-
-let rec read lexbuf =
-  match%sedlex lexbuf with
-  (* Stellogen *)
-  | '{' -> LBRACE
-  | '}' -> RBRACE
-  | "end" -> END
-  | "exec" -> EXEC
-  | "run" -> RUN
-  | "interface" -> INTERFACE
-  | "show" -> SHOW
-  | "spec" -> SPEC
-  | "kill" -> KILL
-  | "clean" -> CLEAN
-  | "use" -> USE
-  | "trace" -> TRACE
-  | "linear-exec" -> LINEXEC
-  | "show-exec" -> SHOWEXEC
-  | "galaxy" -> GALAXY
-  | "process" -> PROCESS
-  | "->" -> RARROW
-  | "=>" -> DRARROW
-  | "." -> DOT
-  | "#" -> SHARP
-  | "&" -> AMP
-  | '"' -> read_string (Buffer.create 255) lexbuf
-  (* Stellar resolution *)
-  | '|' -> BAR
-  | "!=" -> NEQ
-  | '_' -> PLACEHOLDER
-  | '[' -> LBRACK
-  | ']' -> RBRACK
-  | '(' -> LPAR
-  | ')' -> RPAR
-  | ',' -> COMMA
-  | '@' -> AT
-  | '+' -> PLUS
-  | '-' -> MINUS
-  | '=' -> EQ
-  | ':' -> CONS
-  | ';' -> SEMICOLON
-  (* Identifiers *)
-  | Plus 'A' .. 'Z', Star ('a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' | '-') ->
-    VAR (Sedlexing.Utf8.lexeme lexbuf)
-  | ( ('a' .. 'z' | '0' .. '9')
-    , Star ('a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' | '?') ) ->
-    SYM (Sedlexing.Utf8.lexeme lexbuf)
-  (* Whitespace *)
-  | Plus (' ' | '\t') -> read lexbuf
-  | '\r' | '\n' | "\r\n" -> update_pos_newline lexbuf
-  (* Comments *)
-  | '\'' -> comment lexbuf
-  | "'''" -> comments lexbuf
-  | eof -> EOF
-  | _ ->
-    raise (SyntaxError ("Unexpected character: " ^ Sedlexing.Utf8.lexeme lexbuf))
-
-and read_string buf lexbuf =
-  match%sedlex lexbuf with
-  | '"' -> SYM ("\"" ^ Buffer.contents buf ^ "\"")
-  | '\\', '/' ->
-    Buffer.add_char buf '/';
-    read_string buf lexbuf
-  | '\\', '\\' ->
-    Buffer.add_char buf '\\';
-    read_string buf lexbuf
-  | '\\', 'b' ->
-    Buffer.add_char buf '\b';
-    read_string buf lexbuf
-  | '\\', 'f' ->
-    Buffer.add_char buf '\012';
-    read_string buf lexbuf
-  | '\\', 'n' ->
-    Buffer.add_char buf '\n';
-    read_string buf lexbuf
-  | '\\', 'r' ->
-    Buffer.add_char buf '\r';
-    read_string buf lexbuf
-  | '\\', 't' ->
-    Buffer.add_char buf '\t';
-    read_string buf lexbuf
-  | Plus (Compl ('"' | '\\')) ->
-    Buffer.add_string buf (Sedlexing.Utf8.lexeme lexbuf);
-    read_string buf lexbuf
-  | eof -> raise (SyntaxError "String is not terminated")
-  | _ ->
-    raise
-      (SyntaxError ("Illegal string character: " ^ Sedlexing.Utf8.lexeme lexbuf))
-
-and comment lexbuf =
-  match%sedlex lexbuf with
-  | '\r' | '\n' | "\r\n" -> EOL
-  | eof -> EOF
-  | _ ->
-    ignore (Sedlexing.next lexbuf);
-    comment lexbuf
-
-and comments lexbuf =
-  match%sedlex lexbuf with
-  | "'''" -> read lexbuf
-  | _ ->
-    ignore (Sedlexing.next lexbuf);
-    comments lexbuf
diff --git a/src/stellogen/sgen_parser.mly b/src/stellogen/sgen_parser.mly
deleted file mode 100644
index c3a1430..0000000
--- a/src/stellogen/sgen_parser.mly
+++ /dev/null
@@ -1,136 +0,0 @@
-%{
-open Sgen_ast
-%}
-
-%token SHOW SHOWEXEC
-%token INTERFACE
-%token USE
-%token RUN
-%token SPEC
-%token TRACE
-%token SHARP
-%token KILL CLEAN
-%token EXEC LINEXEC
-%token PROCESS
-%token GALAXY
-%token RARROW DRARROW
-%token EQ
-%token END
-
-%start <Sgen_ast.program> program
-%start <Sgen_ast.declaration> declaration
-
-%%
-
-let program :=
-  | EOL*; EOF;                            { [] }
-  | EOL*; d=declaration; EOL+; p=program; { d::p }
-  | EOL*; d=declaration; EOF;             { [d] }
-
-let ident := ~=ray; <>
-
-let declaration :=
-  | SPEC; ~=ident; EOL*; EQ; EOL*; ~=galaxy_expr; <Def>
-  | ~=ident; EOL*; EQ; EOL*; ~=galaxy_expr;       <Def>
-  | SHOW; EOL*; ~=galaxy_expr;                    <Show>
-  | SHOWEXEC; EOL*; ~=galaxy_expr;                <ShowExec>
-  | TRACE; EOL*; ~=galaxy_expr;                   <Trace>
-  | RUN; EOL*; ~=galaxy_expr;                     <Run>
-  | ~=type_declaration;                           <TypeDef>
-  | USE; ~=separated_list(RARROW, ident); DOT;    <Use>
-  | INTERFACE; EOL*; x=ident; EOL*; i=interface_item*; END; INTERFACE?;
-    { Def (x, Raw (Interface i)) }
-
-let type_declaration :=
-  | x=ident; CONS; CONS; ts=separated_list(SEMICOLON, type_expr); EOL*; DOT;
-    { TDef (x, ts) }
-  | x=ident; CONS; EQ; CONS; EOL*; g=galaxy_expr;
-    { TExp (x, g) }
-
-let type_expr := ~=ident; ~=bracks(ident)?; EOL*; <>
-
-let galaxy_expr :=
-  | ~=galaxy_content; EOL*; DOT; <>
-  | ~=process;                   <>
-  | ~=undelimited_raw_galaxy;    <Raw>
-
-let interface_item := ~=type_declaration; EOL*; <>
-
-let undelimited_raw_galaxy :=
-  | ~=marked_constellation; EOL*; DOT;                <Const>
-  | GALAXY; EOL*; ~=galaxy_item*; EOL*; END; GALAXY?; <Galaxy>
-
-let delimited_raw_galaxy :=
-  | braces(EOL*);                   { Const [] }
-  | ~=pars(marked_constellation);   <Const>
-  | ~=braces(marked_constellation); <Const>
-
-let prefixed_id := SHARP; ~=ident; <Id>
-
-let galaxy_content :=
-  | ~=pars(galaxy_content);                    <>
-  | ~=delimited_raw_galaxy;                    <Raw>
-  | g=galaxy_content; h=galaxy_content;        { Union (g, h) }
-  | ~=galaxy_access;                           <>
-  | AT; ~=focussed_galaxy_content;             <Focus>
-  | ~=galaxy_content; ~=bracks(substitution);  <Subst>
-  | ~=galaxy_block;                            <>
-  | ~=prefixed_id;                             <>
-
-let focussed_galaxy_content :=
-  | ~=pars(galaxy_content);  <>
-  | ~=galaxy_access;         <>
-  | ~=delimited_raw_galaxy;  <Raw>
-  | ~=galaxy_block;          <>
-  | ~=prefixed_id;           <>
-
-let galaxy_block :=
-  | EXEC; EOL*; ~=galaxy_content; EOL*; END; EXEC?;
-    <Exec>
-  | LINEXEC; EOL*; ~=galaxy_content; EOL*; END; LINEXEC?;
-    <LinExec>
-  | KILL; EOL*; ~=galaxy_content; EOL*; END; KILL?;
-    <Kill>
-  | CLEAN; EOL*; ~=galaxy_content; EOL*; END; CLEAN?;
-    <Clean>
-  | EXEC; EOL*; mcs=marked_constellation; EOL*; END; EXEC?;
-    { Exec (Raw (Const mcs)) }
-  | LINEXEC; EOL*; mcs=marked_constellation; EOL*; END; LINEXEC?;
-    { LinExec (Raw (Const mcs)) }
-  | KILL; EOL*; mcs=marked_constellation; EOL*; END; KILL?;
-    { Kill (Raw (Const mcs)) }
-  | CLEAN; EOL*; mcs=marked_constellation; EOL*; END; CLEAN?;
-    { Clean (Raw (Const mcs)) }
-
-let galaxy_access :=
-  | SHARP; x=ident; RARROW; y=ident;  { Access (Id x, y) }
-  | ~=galaxy_access; RARROW; y=ident; <Access>
-
-let substitution :=
-  | DRARROW; ~=symbol;                      <Extend>
-  | ~=symbol; DRARROW;                      <Reduce>
-  | ~=VAR; DRARROW; ~=ray;                  <SVar>
-  | f=symbol; DRARROW; g=symbol;            { SFunc (f, g) }
-  | SHARP; ~=ident; DRARROW; ~=galaxy_expr; <SGal>
-  | SHARP; x=ident; DRARROW;
-    h=marked_constellation;                 { SGal (x, Raw (Const h)) }
-
-let galaxy_item :=
-  | ~=ident; EQ; EOL*; ~=galaxy_content; DOT; EOL*;
-    <GLabelDef>
-  | x=ident; EQ; EOL*; mcs=marked_constellation; EOL*; DOT; EOL*;
-    { GLabelDef (x, Raw (Const mcs)) }
-  | x=ident; EQ; EOL*; g=undelimited_raw_galaxy; EOL*; DOT; EOL*;
-    { GLabelDef (x, Raw g) }
-  | ~=ident; EQ; EOL*; ~=process; EOL*;  <GLabelDef>
-  | ~=type_declaration; EOL*;            <GTypeDef>
-
-let process :=
-  | PROCESS; EOL*; END; PROCESS?;                   { Process [] }
-  | PROCESS; EOL*; ~=process_item+; END; PROCESS?;  <Process>
-
-let process_item :=
-  | ~=galaxy_content; DOT; EOL*;     <>
-  | ~=undelimited_raw_galaxy; EOL*;  <Raw>
-  | AMP; KILL; DOT; EOL*;            { Id (const "kill") }
-  | AMP; CLEAN; DOT; EOL*;           { Id (const "clean") }
diff --git a/src/stellogen/unification.ml b/src/stellogen/unification.ml
deleted file mode 120000
index 1d705c1..0000000
--- a/src/stellogen/unification.ml
+++ /dev/null
@@ -1 +0,0 @@
-../lsc/unification.ml
\ No newline at end of file
diff --git a/src/lsc/unification.ml b/src/unification.ml
similarity index 72%
rename from src/lsc/unification.ml
rename to src/unification.ml
index 1f4b1c7..9b1a834 100644
--- a/src/lsc/unification.ml
+++ b/src/unification.ml
@@ -17,26 +17,19 @@ end
    --------------------------------------- *)
 
 module Make (Sig : Signature) = struct
-  type fmark =
-    | Noisy
-    | Muted
-
   type term =
     | Var of Sig.idvar
-    | Func of (fmark * Sig.idfunc) * term list
-
-  let equal_mark m m' =
-    match (m, m') with Noisy, Noisy | Muted, Muted -> true | _ -> false
-
-  let equal_func (m, f) (m', f') = equal_mark m m' && Sig.equal_idfunc f f'
+    | Func of Sig.idfunc * term list
 
   let rec equal_term t u =
     match (t, u) with
     | Var x, Var y -> Sig.equal_idvar x y
-    | Func ((Muted, f), ts), Func ((Muted, g), us)
-    | Func ((Noisy, f), ts), Func ((Noisy, g), us) ->
-      Sig.equal_idfunc f g
-      && List.for_all2_exn ~f:(fun t u -> equal_term t u) ts us
+    | Func (f, ts), Func (g, us) -> begin
+      try
+        Sig.equal_idfunc f g
+        && List.for_all2_exn ~f:(fun t u -> equal_term t u) ts us
+      with _ -> false
+    end
     | _ -> false
 
   type substitution = (Sig.idvar * term) list
@@ -77,7 +70,9 @@ module Make (Sig : Signature) = struct
   let subst sub = map Fn.id (apply sub)
 
   let replace_func from_pf to_pf =
-    map (fun pf -> if equal_func pf from_pf then to_pf else pf) (fun x -> Var x)
+    map
+      (fun pf -> if Sig.equal_idfunc pf from_pf then to_pf else pf)
+      (fun x -> Var x)
 
   let replace_funcs fsub t =
     List.fold_left fsub ~init:t ~f:(fun acc (from_pf, to_pf) ->
@@ -103,13 +98,6 @@ module Make (Sig : Signature) = struct
       ~init:[] ts
     |> List.rev
 
-  let signals = ref []
-
-  (* FIXME: doesn't work as expected *)
-  let emit_signals sub =
-    let new_signals = List.map ~f:(fun (_, t) -> t) sub in
-    signals := new_signals @ !signals
-
   let rec solve sub : problem -> substitution option = function
     | [] -> Some sub
     (* Clear *)
@@ -117,18 +105,9 @@ module Make (Sig : Signature) = struct
     (* Orient + Replace *)
     | (Var x, t) :: pbs | (t, Var x) :: pbs -> elim x t pbs sub
     (* Open *)
-    | (Func ((m, f), ts), Func ((m', g), us)) :: pbs
-      when equal_mark m m' && Sig.compatible f g
-           && List.length ts = List.length us -> begin
-      match solve sub (List.zip_exn ts us @ pbs) with
-      | None -> None
-      | Some s -> begin
-        match m with
-        | Noisy ->
-          emit_signals s;
-          Some s
-        | _ -> Some s
-      end
+    | (Func (f, ts), Func (g, us)) :: pbs
+      when Sig.compatible f g && List.length ts = List.length us -> begin
+      solve sub (List.zip_exn ts us @ pbs)
     end
     | _ -> None
 
diff --git a/test/behavior/automata.sg b/test/behavior/automata.sg
deleted file mode 100644
index c6eaa80..0000000
--- a/test/behavior/automata.sg
+++ /dev/null
@@ -1,45 +0,0 @@
-binary =
-  -i(e) ok;
-  -i(0:X) +i(X);
-  -i(1:X) +i(X).
-
-e :: binary.
-e = +i(e).
-
-0 :: binary.
-0 = +i(0:e).
-
-1 :: binary.
-1 = +i(1:e).
-
-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
-
-empty = {}.
-
-tested :=: {}.
-tested = process #e. #a1. &kill. end
-
-tested :=: {}.
-tested = process #0. #a1. &kill. end
-
-tested :=: {}.
-tested = process #1. #a1. &kill. end
-
-tested :=: accept.
-tested = process +i(0:0:0:e). #a1. &kill. end
-
-tested :=: {}.
-tested = process +i(0:1:0:e). #a1. &kill. end
-
-tested :=: {}.
-tested = process +i(1:1:0:e). #a1. &kill. end
diff --git a/test/behavior/galaxy.sg b/test/behavior/galaxy.sg
deleted file mode 100644
index 54d1603..0000000
--- a/test/behavior/galaxy.sg
+++ /dev/null
@@ -1,18 +0,0 @@
-g = galaxy
-  test1 = 1.
-  test2 = galaxy
-    test21 = 2.
-    test22 = galaxy
-      test3 = 3.
-    end.
-  end.
-end
-
-x :=: 1.
-x = @#g->test1.
-
-x :=: 2.
-x = @#g->test2->test21.
-
-x :=: 3.
-x = @#g->test2->test22->test3.
diff --git a/test/behavior/linear.sg b/test/behavior/linear.sg
deleted file mode 100644
index 1d410f4..0000000
--- a/test/behavior/linear.sg
+++ /dev/null
@@ -1,14 +0,0 @@
-1 = +nat(s(0)).
-2 = +nat(s(s(0))).
-3 = +nat(s(s(s(0)))).
-
-nat = -nat(s(X)) +nat(X).
-
-tested :=: +nat(0).
-tested = @linear-exec (@#1) #nat end.
-
-tested :=: +nat(s(0)).
-tested = @linear-exec (@#2) #nat end.
-
-tested :=: +nat(s(s(0))).
-tested = @linear-exec (@#3) #nat end.
diff --git a/test/behavior/prolog.sg b/test/behavior/prolog.sg
deleted file mode 100644
index c7b3dd5..0000000
--- a/test/behavior/prolog.sg
+++ /dev/null
@@ -1,25 +0,0 @@
-'''unary addition'''
-add =
-  +add(0 Y Y);
-  -add(X Y Z) +add(s(X) Y s(Z)).
-
-tested :=: 0.
-tested = #add @(-add(0 0 R) R).
-
-tested :=: s(0).
-tested = #add @(-add(s(0) 0 R) R).
-
-tested :=: s(0).
-tested = #add @(-add(0 s(0) R) R).
-
-tested :=: s(s(s(s(0)))).
-tested = #add @(-add(s(s(0)) s(s(0)) R) R).
-
-tested :=: 0.
-tested = #add @(-add(s(s(0)) R s(s(0))) R).
-
-tested :=: s(0).
-tested = #add @(-add(s(s(0)) R s(s(s(0)))) R).
-
-tested :=: s(s(0)).
-tested = #add @(-add(s(s(0)) R s(s(s(s(0))))) R).
diff --git a/test/dune b/test/dune
index b55a4a3..723e018 100644
--- a/test/dune
+++ b/test/dune
@@ -2,12 +2,10 @@
  (name test)
  (modules test)
  (deps
-  (glob_files ./lsc/*.stellar)
-  (glob_files ./syntax/*.sg)
-  (glob_files ./behavior/*.sg)
+  (glob_files ./subjects/*.sg)
   (glob_files ../examples/*.sg)
   (glob_files ../exercises/solutions/*.sg))
- (libraries alcotest base stellogen lsc))
+ (libraries alcotest base stellogen))
 
 (env
  (dev
diff --git a/test/lsc/basic.stellar b/test/lsc/basic.stellar
deleted file mode 100644
index 281fa6d..0000000
--- a/test/lsc/basic.stellar
+++ /dev/null
@@ -1 +0,0 @@
--f(a); @+f(X) X.
diff --git a/test/lsc/empty.stellar b/test/lsc/empty.stellar
deleted file mode 100644
index e69de29..0000000
diff --git a/test/lsc/prolog.stellar b/test/lsc/prolog.stellar
deleted file mode 100644
index 64af300..0000000
--- a/test/lsc/prolog.stellar
+++ /dev/null
@@ -1,3 +0,0 @@
-[+add(0 Y Y)];
-[-add(X Y Z) +add(s(X) Y s(Z))];
-[@-add(s(s(0)) s(s(0)) R) R].
diff --git a/test/subjects/linear.sg b/test/subjects/linear.sg
new file mode 100644
index 0000000..e44ea9b
--- /dev/null
+++ b/test/subjects/linear.sg
@@ -0,0 +1,14 @@
+(:= 1 (+nat (s 0)))
+(:= 2 (+nat <s s 0>))
+(:= 3 (+nat <s s s 0>))
+
+(spec nat [(-nat (s X)) (+nat X)])
+
+(:= tested @(linexec { @#1 #nat }))
+(== #tested (+nat 0))
+
+(:= tested @(linexec { @#2 #nat }))
+(== #tested (+nat (s 0)))
+
+(:= tested @(linexec { @#3 #nat }))
+(== #tested (+nat <s s 0>))
diff --git a/test/subjects/prolog.sg b/test/subjects/prolog.sg
new file mode 100644
index 0000000..e767c8a
--- /dev/null
+++ b/test/subjects/prolog.sg
@@ -0,0 +1,24 @@
+(:= add {
+  [(+add 0 Y Y)]
+  [(-add X Y Z) (+add (s X) Y (s Z))]})
+
+(:= tested (exec { #add @[(-add 0 0 R) R] }))
+(== #tested 0)
+
+(:= tested (exec { #add @[(-add (s 0) 0 R) R] }))
+(== #tested (s 0))
+
+(:= tested (exec { #add @[(-add 0 (s 0) R) R] }))
+(== #tested (s 0))
+
+(:= tested (exec { #add @[(-add <s s 0> <s s 0> R) R] }))
+(== #tested <s s s s 0>)
+
+(:= tested (exec { #add @[(-add <s s 0> R <s s 0>) R] }))
+(== #tested 0)
+
+(:= tested (exec { #add @[(-add <s s 0> R <s s s 0>) R] }))
+(== #tested <s 0>)
+
+(:= tested (exec { #add @[(-add <s s 0> R <s s s s 0>) R] }))
+(== #tested <s s 0>)
diff --git a/test/subjects/records.sg b/test/subjects/records.sg
new file mode 100644
index 0000000..0afe23a
--- /dev/null
+++ b/test/subjects/records.sg
@@ -0,0 +1,18 @@
+(:= g {
+  [+test1 1]
+  [+test2 {
+    [+test21 2]
+    [+test22 {
+      [+test3 3]}]}]})
+
+(:= x <eval exec { #g @[-test1] }>)
+(== #x 1)
+
+(:= x <eval exec { #g @[-test2] }>)
+(:= y <eval exec { #x @[-test21] }>)
+(== #y 2)
+
+(:= x <eval exec { #g @[-test2] }>)
+(:= y <eval exec { #x @[-test22] }>)
+(:= z <eval exec { #y @[-test3] }>)
+(== #z 3)
diff --git a/test/syntax/blocks.sg b/test/syntax/blocks.sg
deleted file mode 100644
index 57090c3..0000000
--- a/test/syntax/blocks.sg
+++ /dev/null
@@ -1,8 +0,0 @@
-x = exec 0 end.
-x = linear-exec 0 end.
-x = exec exec 0 end end.
-x = linear-exec linear-exec 0 end end.
-x = exec linear-exec 0 end end.
-x = linear-exec exec 0 end end.
-x = exec linear-exec 0 end linear-exec end exec.
-x = linear-exec exec 0 end exec end linear-exec.
diff --git a/test/syntax/definitions.sg b/test/syntax/definitions.sg
deleted file mode 100644
index 7731aaf..0000000
--- a/test/syntax/definitions.sg
+++ /dev/null
@@ -1,99 +0,0 @@
-'normal
-x = +a.
-x = -a.
-x = +a b; -c d.
-x = { a }.
-x = { [a] }.
-x = { +a }.
-x = { -a }.
-x = { [-a] }.
-x = { +a b; -c d }.
-x = { [+a b]; -c d }.
-x = { +a b; [-c d] }.
-x = { a b }.
-x = { a b; -c d }.
-
-'cons
-x = +w(0:1:0:1:e).
-x = +w((0:(1:(0:(1:e))))).
-x = +w((((0:1):0):1):e).
-x = +w((0:1):(0:1):e).
-x = +w(0:(1:0):(1:e)).
-x = +w((0:1):0:(1:e)).
-
-'trailing end of star
-'FIXME: it should work
-'x = { a; }.
-
-'focussed
-x = [@+a].
-x = [@+a b]; -c d.
-x = +a b; [@-c d].
-x = [@+a b]; [@-c d].
-x = { [@a] }.
-x = { @+a }.
-x = { [@-a] }.
-x = { [@+a b]; -c d }.
-x = { [+a b]; @-c d }.
-x = { @+a b; [-c d] }.
-x = { +a b; [@-c d] }.
-x = { @+a b; [@-c d] }.
-x = { @a b }.
-x = { @a b; -c d }.
-x = { a b; @-c d }.
-x = { @a b; @-c d }.
-
-'ineq
-x = +f(X); +f(Y) | X!=Y Y!=X X!=g(Y) g(X)!=Y.
-x = +f(X) | X!=Y Y!=X X!=g(Y) g(X)!=Y; +f(Y).
-x = +f(X) | X!=Y Y!=X X!=g(Y) g(X)!=Y.
-x = +f(X) | X!=Y Y!=X X!=g(Y) g(X)!=Y.
-x = +f(X) | X != Y Y != X X != g(Y) g(X) != Y.
-x = +f(X) |
-  X!=Y Y!=X X!=g(Y) g(X)!=Y.
-x = +f(X) |
-  X!=Y
-  Y!=X
-  X!=g(Y)
-  g(X)!=Y.
-x = +f(X) |
-  X!=Y Y!=X
-  X!=g(Y) g(X)!=Y.
-'''FIXME
-  x = +f(X)
-  | X!=Y Y!=X X!=g(Y) g(X)!=Y.
-'''
-
-'incomp
-x = +f(X) | a:b; +f(Y) | a:c.
-x = +f(X) | X!=Y a:b X!=Y; +f(Y) | X!=Y a:c X!=Y.
-x = +f(X) | a:b a:b a:b; +f(Y) | a:c a:c a:c.
-
-'with EOL
-'''FIX ME
-x
-=
-+a
-.
-
-x
-=
-@
-+a
-.
-
-x
-=
-{+a}
-.
-
-x
-=
-{@+a}
-.
-
-x
-=
-{[a]}
-.
-'''
diff --git a/test/syntax/empty.sg b/test/syntax/empty.sg
deleted file mode 100644
index e69de29..0000000
diff --git a/test/syntax/galaxy.sg b/test/syntax/galaxy.sg
deleted file mode 100644
index 66f96b5..0000000
--- a/test/syntax/galaxy.sg
+++ /dev/null
@@ -1,37 +0,0 @@
-g = galaxy end
-g = galaxy end galaxy
-
-g = galaxy
-end
-
-g = galaxy
-  test1 = 1.
-  test2 = 2.
-end
-
-g = galaxy
-  test1 = 1.
-  test2 = 2.
-end galaxy
-
-g = galaxy
-  test1 = galaxy
-    test2 = galaxy
-    end.
-  end.
-end
-
-g = galaxy
-  test1 = galaxy
-    test11 = 11.
-    test12 = 12.
-  end.
-  test2 = galaxy
-    test21 = 21.
-    test22 = 22.
-  end.
-end
-
-x = #g->test1.
-x = #g->test1->test11.
-x = #g->test1->test11->test111.
diff --git a/test/test.ml b/test/test.ml
index 2b09ffe..8fca86c 100644
--- a/test/test.ml
+++ b/test/test.ml
@@ -1,27 +1,11 @@
 open Base
 
-let lsc filename () =
-  let lexbuf = Sedlexing.Utf8.from_channel (Stdlib.open_in filename) in
-  let lexer = Sedlexing.with_tokenizer Lsc.Lsc_lexer.read lexbuf in
-  let parser =
-    MenhirLib.Convert.Simplified.traditional2revised
-      Lsc.Lsc_parser.constellation_file
-  in
-  let mcs = parser lexer in
-  match Lsc.Lsc_ast.exec ~showtrace:false mcs with
-  | Error e -> Lsc.Lsc_err.pp_err_effect e
-  | Ok res -> Lsc.Lsc_ast.string_of_constellation res
-
 let sgen filename () =
   let lexbuf = Sedlexing.Utf8.from_channel (Stdlib.open_in filename) in
-  let p = Stellogen.Sgen_parsing.parse_with_error lexbuf in
-  Stellogen.Sgen_eval.eval_program ~typecheckonly:false ~notyping:false p
-
-let make_expect_test name path f expected =
-  let test got expected () =
-    Alcotest.(check string) "same string" got expected
-  in
-  (name, `Quick, test (f (path ^ name) ()) expected)
+  let expr = Stellogen.Sgen_parsing.parse_with_error lexbuf in
+  let preprocessed = Stellogen.Expr.preprocess expr in
+  let p = Stellogen.Expr.program_of_expr preprocessed in
+  Stellogen.Sgen_eval.eval_program p
 
 let make_ok_test name path f =
   let test got () =
@@ -36,18 +20,10 @@ let run_dir test_f directory =
        not @@ Stdlib.Sys.is_directory (Stdlib.Filename.concat directory f) )
   |> List.map ~f:(fun x -> make_ok_test x directory test_f)
 
-let lsc_test_suite () =
-  let path = "./lsc/" in
-  [ make_expect_test "empty.stellar" path lsc "{}"
-  ; make_expect_test "basic.stellar" path lsc "a."
-  ; make_expect_test "prolog.stellar" path lsc "s(s(s(s(0))))."
-  ]
-
 let () =
   Alcotest.run "Stellogen Test Suite"
-    [ ("LSC test suite", lsc_test_suite ())
-    ; ("Stellogen examples", run_dir sgen "../examples/")
-    ; ("Stellogen exercises solutions", run_dir sgen "../exercises/solutions/")
-    ; ("Stellogen syntax", run_dir sgen "./syntax/")
-    ; ("Stellogen behavior", run_dir sgen "./behavior/")
+    [ ("Stellogen examples", run_dir sgen "../examples/")
+    ; (* ; ("Stellogen exercises solutions", run_dir sgen "../exercises/solutions/")
+    ; *)
+      ("Stellogen syntax", run_dir sgen "./subjects/")
     ]