Merge pull request #105 from engboris/fix-exec

Remove sources of unpredictability in behaviour of execution

Author: engboris

examples/linear_lambda.sg

@@ -23,5 +23,10 @@ end
 
 adapter = -id(l:X) +x(X); -id(r:X) +y(X).
 
-vehicle :: "a -o a".
+checker = galaxy
+  interaction = #tested #test.
+  expect = ok.
+end
+
+vehicle :: "a -o a" [checker].
 vehicle = #id #adapter.

examples/mll.sg

@@ -22,7 +22,12 @@ spec "a -o a" = galaxy
     @-7(X) ok.
 end
 
-id :: "a -o a".
+checker = galaxy
+  interaction = #tested #test.
+  expect = ok.
+end
+
+id :: "a -o a" [checker].
 id =
   -5(l:X) +1(X);
   -5(r:X) +2(X);

examples/syntax.sg

@@ -60,7 +60,7 @@ show-exec (#1 #2)[#1=>+f(X) X][#2=>-f(a)].
 
 'checkers & typechecking
 checker = galaxy
-  interaction = #tested #test.
+  interaction = (@#tested) #test.
   expect = ok.
 end
 

exercises/solutions/01-paths.sg

@@ -1,14 +1,17 @@
 'fill the 'your_answer' holes to replace #1 in the constellations
 'below such that the result of execution is { ok }
 
-x :=: ok.
+x1 :=: ok.
+x1 = (@(-1 ok) #1)[#1=>+1].
 
-x = ((-1 ok) #1)[#1=>+1].
+x2 :=: ok.
+x2 = ((@-1; +2) #1)[#1=>+1 -2 ok].
 
-x = ((-1; +2) #1)[#1=>+1 -2 ok].
+x3 :=: ok.
+x3 = ((@-1 ok; -2 +3) #1)[#1=>+1 +2; -3].
 
-x = ((-1 ok; -2 +3) #1)[#1=>+1 +2; -3].
+x4 :=: ok.
+x4 = ((@-f(+g(X)) ok) #1)[#1=>+f(-g(X))].
 
-x = ((-f(+g(X)) ok) #1)[#1=>+f(-g(X))].
-
-x = ((+f(a) +f(b); +g(a); @+g(b) ok) #1)[#1=>-f(a); -f(b) -g(a) -g(b)].
+x5 :=: ok.
+x5 = ((+f(a) +f(b); +g(a); @+g(b) ok) #1)[#1=>-f(a); -f(b) -g(a) -g(b)].

exercises/solutions/04-boolean.sg

@@ -1,11 +1,16 @@
 '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.
+not :: not_spec [checker].
 not = +not(0 1); +not(1 0).
 
 'how to print the truth table of NOT ?
@@ -19,10 +24,10 @@ and_spec = galaxy
   test11 = @-and(1 1 1) ok.
 end
 
-and :: and_spec.
+and :: and_spec [checker].
 and = +and(0 0 0); +and(0 1 0); +and(1 0 0); +and(1 1 1).
 
-and2 :: and_spec.
+and2 :: and_spec [checker].
 and2 = +and(0 X 0); +and(1 X X).
 
 or_spec = galaxy
@@ -32,10 +37,10 @@ or_spec = galaxy
   test11 = @-or(1 1 1) ok.
 end
 
-or :: or_spec.
+or :: or_spec [checker].
 or = +or(0 0 0); +or(0 1 1); +or(1 0 1); +or(1 1 1).
 
-or2 :: or_spec.
+or2 :: or_spec [checker].
 or2 = +or(0 X X); +or(1 X 1).
 
 impl_spec = galaxy
@@ -45,11 +50,11 @@ impl_spec = galaxy
   test11 = @-impl(1 1 1) ok.
 end
 
-impl :: impl_spec.
-impl = #not #or @{-not(X Y) -or(Y Z R) +impl(X Z R)}.
+impl :: impl_spec [checker].
+impl = exec #not #or @{-not(X Y) -or(Y Z R) +impl(X Z R)} end.
 
-impl2 :: impl_spec.
-impl2 = #not #or @{-not(X Y) -or(Y Z R) +impl(X Z R)}.
+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)}.

src/lsc/lsc_ast.ml

@@ -294,22 +294,19 @@ let cc_representatives from cs =
   in
   selection [] from cs
 
-let extract_intspace (mcs : marked_constellation) =
-  let rec sort (cs, space) = function
+let classify =
+  let rec aux (cs, space) = function
     | [] -> (List.rev cs, List.rev space)
-    | Marked s :: t -> sort (cs, s :: space) t
-    | Unmarked s :: t -> sort (s :: cs, space) t
+    | Marked s :: t -> aux (cs, s :: space) t
+    | Unmarked s :: t -> aux (s :: cs, space) t
   in
-  match sort ([], []) mcs with
-  (* marks are selected for you in each connected component *)
-  | unmarked, [] ->
-    let cs, marked = cc_representatives [] unmarked in
-    ident_counter := 0;
-    (cs, marked)
-  (* user selects marks *)
-  | unmarked, marked ->
-    ident_counter := 0;
-    (unmarked, marked)
+  aux ([], [])
+
+let extract_intspace (mcs : marked_constellation) =
+  (* auto-selection *)
+  (* let cs, marked = cc_representatives [] unmarked in *)
+  ident_counter := 0;
+  classify mcs
 
 (* ---------------------------------------
    Execution

src/stellogen/sgen_ast.ml

@@ -50,7 +50,8 @@ type env =
   }
 
 let expect (g : galaxy_expr) : galaxy_expr =
-  Raw (Galaxy [ GLabelDef ("expect", g) ])
+  Raw
+    (Galaxy [ GLabelDef ("interaction", Id "tested"); GLabelDef ("expect", g) ])
 
 let initial_env =
   { objs = [ ("^empty", Raw (Const [])) ]

src/stellogen/sgen_eval.ml

@@ -207,7 +207,7 @@ and eval_galaxy_expr ~notyping (env : env) :
     let* mcs = galaxy_to_constellation ~notyping env eval_e in
     begin
       match exec ~linear:false ~showtrace:false mcs with
-      | Ok mcs -> Ok (Const (unmark_all mcs))
+      | Ok res -> Ok (Const (unmark_all res))
       | Error e -> Error (LscError e)
     end
   | LinExec e ->
@@ -237,7 +237,8 @@ and eval_galaxy_expr ~notyping (env : env) :
         | _ ->
           let origin = acc |> remove_mark_all |> focus in
           let* ev =
-            eval_galaxy_expr ~notyping env (Exec (Union (x, Raw (Const origin))))
+            eval_galaxy_expr ~notyping env
+              (Focus (Exec (Union (x, Raw (Const origin)))))
           in
           galaxy_to_constellation ~notyping env ev )
     in
@@ -332,7 +333,7 @@ and typecheck ~notyping env x t (ck : galaxy_expr) : (unit, err) Result.t =
               , Exec
                   (Subst
                      ( Subst (format, SGal ("test", test))
-                     , SGal ("tested", Exec obj_x) ) )
+                     , SGal ("tested", obj_x) ) )
                 |> eval_galaxy_expr ~notyping env )
         end
       | _ -> Error IllFormedChecker )
@@ -347,7 +348,7 @@ and typecheck ~notyping env x t (ck : galaxy_expr) : (unit, err) Result.t =
     | Error e -> Error e )
   |> Result.all_unit
 
-and default_interaction = Union (Id "tested", Id "test")
+and default_interaction = Union (Focus (Id "tested"), Id "test")
 
 and default_expect =
   Raw (Const [ Unmarked { content = [ func "ok" [] ]; bans = [] } ])

src/stellogen/sgen_parser.mly

@@ -16,6 +16,9 @@ open Sgen_ast
 %token EQ
 %token END
 
+%left RARROW
+%nonassoc AT
+
 %start <Sgen_ast.program> program
 
 %%
@@ -62,21 +65,36 @@ let delimited_raw_galaxy :=
   | ~=braces(marked_constellation); <Const>
 
 let galaxy_content :=
-  | ~=pars(galaxy_content);             <>
-  | SHARP; ~=SYM;                       <Id>
-  | ~=delimited_raw_galaxy;             <Raw>
-  | g=galaxy_content; h=galaxy_content; { Union (g, h) }
-  | ~=galaxy_content; RARROW; ~=SYM;    <Access>
-  | AT; SHARP; x=SYM;                   { Focus (Id x) }
-  | AT; g=delimited_raw_galaxy;         { Focus (Raw g) }
-  | ~=galaxy_content; ~=bracks(substitution);             <Subst>
-  | EXEC; EOL*; ~=galaxy_content; EOL*; END; EXEC?;       <Exec>
-  | LINEXEC; EOL*; ~=galaxy_content; EOL*; END; LINEXEC?; <LinExec>
+  | ~=pars(galaxy_content);                   <>
+  | SHARP; ~=SYM;                             <Id>
+  | ~=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;                           <>
+
+let focussed_galaxy_content :=
+  | ~=pars(galaxy_content); <>
+  | ~=galaxy_access;        <>
+  | SHARP; ~=SYM;           <Id>
+  | ~=delimited_raw_galaxy; <Raw>
+  | ~=galaxy_block;         <>
+
+let galaxy_block :=
+  | EXEC; EOL*; ~=galaxy_content; EOL*; END; EXEC?;
+    <Exec>
+  | LINEXEC; EOL*; ~=galaxy_content; EOL*; END; LINEXEC?;
+    <LinExec>
   | EXEC; EOL*; mcs=marked_constellation; EOL*; END; EXEC?;
     { Exec (Raw (Const mcs)) }
   | LINEXEC; EOL*; mcs=marked_constellation; EOL*; END; LINEXEC?;
     { LinExec (Raw (Const mcs)) }
 
+let galaxy_access :=
+  | SHARP; x=SYM; RARROW; y=SYM;    { Access (Id x, y) }
+  | ~=galaxy_access; RARROW; y=SYM; <Access>
+
 let substitution :=
   | DRARROW; ~=symbol;                    <Extend>
   | ~=symbol; DRARROW;                    <Reduce>

test/behavior/galaxy.sg

@@ -9,10 +9,10 @@ g = galaxy
 end
 
 x :=: 1.
-x = #g->test1.
+x = @#g->test1.
 
 x :=: 2.
-x = #g->test2->test21.
+x = @#g->test2->test21.
 
 x :=: 3.
-x = #g->test2->test22->test3.
+x = @#g->test2->test22->test3.