Skip to content

Commit ad4607a

Browse files
engborisengboris
committed
Add linear exec syntax
1 parent 0d4d910 commit ad4607a

File tree

6 files changed

+72
-49
lines changed

6 files changed

+72
-49
lines changed

‎examples/mll.sg‎

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -39,15 +39,18 @@ end
3939

4040
show-exec #ps1->vehicle #ps1->cuts.
4141

42-
'''
43-
FIXME : MLL incorrectness
42+
spec "a * b" =
43+
-1(g:X) -2(g:X) +3(g:X);
44+
@-3(g:X) ok.
45+
46+
linear = galaxy
47+
interaction = linear-exec #tested #test end
48+
expect = ok.
49+
end
4450

51+
'does not typecheck
52+
'vehicle :: "a * a" [linear].
4553
vehicle =
4654
+3(l:X) +3(r:X);
4755
-3(l:X) +1(g:X);
4856
-3(r:X) +2(g:X).
49-
50-
test =
51-
-1(g:X) -2(g:X) +3(g:X);
52-
@-3(g:X) 3(X).
53-
'''

‎nvim/syntax/stellogen.vim‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
syn clear
22

3-
syn keyword sgKeyword show exec spec trace process end galaxy run interface
3+
syn keyword sgKeyword show exec spec linear trace process end galaxy run interface
44
syn match sgComment "\s*'[^'].*$"
55
syn match sgId "#\%(\l\|\d\)\w*"
66
syn match sgIdDef "\zs\%(\l\|\d\)\w*\ze\s*="

‎src/stellogen/sgen_ast.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ and galaxy_expr =
2727
| Access of galaxy_expr * ident
2828
| Id of ident
2929
| Exec of galaxy_expr
30+
| LinExec of galaxy_expr
3031
| Union of galaxy_expr * galaxy_expr
3132
| Subst of galaxy_expr * substitution
3233
| Focus of galaxy_expr

‎src/stellogen/sgen_eval.ml‎

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,7 @@ let rec map_galaxy env ~f : galaxy -> (galaxy, err) Result.t = function
3131
in
3232
Galaxy g' |> Result.return
3333

34-
and map_galaxy_expr env ~f e : (galaxy_expr, err) Result.t =
35-
match e with
34+
and map_galaxy_expr env ~f : galaxy_expr -> (galaxy_expr, err) Result.t = function
3635
| Raw g ->
3736
let* map_g = map_galaxy env ~f g in
3837
Raw map_g |> Result.return
@@ -48,6 +47,9 @@ and map_galaxy_expr env ~f e : (galaxy_expr, err) Result.t =
4847
| Exec e ->
4948
let* map_e = map_galaxy_expr env ~f e in
5049
Exec map_e |> Result.return
50+
| LinExec e ->
51+
let* map_e = map_galaxy_expr env ~f e in
52+
LinExec map_e |> Result.return
5153
| Union (e, e') ->
5254
let* map_e = map_galaxy_expr env ~f e in
5355
let* map_e' = map_galaxy_expr env ~f e' in
@@ -86,6 +88,9 @@ let rec replace_id env (_from : ident) (_to : galaxy_expr) e :
8688
| Exec e ->
8789
let* g = replace_id env _from _to e in
8890
Exec g |> Result.return
91+
| LinExec e ->
92+
let* g = replace_id env _from _to e in
93+
LinExec g |> Result.return
8994
| Union (e1, e2) ->
9095
let* g1 = replace_id env _from _to e1 in
9196
let* g2 = replace_id env _from _to e2 in
@@ -200,7 +205,15 @@ and eval_galaxy_expr ~notyping (env : env) :
200205
let* eval_e = eval_galaxy_expr ~notyping env e in
201206
let* mcs = galaxy_to_constellation ~notyping env eval_e in
202207
begin
203-
match exec ~showtrace:false mcs with
208+
match exec ~linear:false ~showtrace:false mcs with
209+
| Ok mcs -> Ok (Const (unmark_all mcs))
210+
| Error e -> Error (LscError e)
211+
end
212+
| LinExec e ->
213+
let* eval_e = eval_galaxy_expr ~notyping env e in
214+
let* mcs = galaxy_to_constellation ~notyping env eval_e in
215+
begin
216+
match exec ~linear:true ~showtrace:false mcs with
204217
| Ok mcs -> Ok (Const (unmark_all mcs))
205218
| Error e -> Error (LscError e)
206219
end

‎src/stellogen/sgen_lexer.mll‎

Lines changed: 39 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -13,46 +13,47 @@ let newline = '\r' | '\n' | "\r\n"
1313

1414
rule read = parse
1515
(* Stellogen *)
16-
| '{' { LBRACE }
17-
| '}' { RBRACE }
18-
| "end" { END }
19-
| "exec" { EXEC }
20-
| "run" { RUN }
21-
| "interface" { INTERFACE }
22-
| "show" { SHOW }
23-
| "spec" { SPEC }
24-
| "trace" { TRACE }
25-
| "show-exec" { SHOWEXEC }
26-
| "galaxy" { GALAXY }
27-
| "process" { PROCESS }
28-
| "->" { RARROW }
29-
| "=>" { DRARROW }
30-
| "." { DOT }
31-
| "#" { SHARP }
32-
| "%" { PERCENT }
33-
| '"' { read_string (Buffer.create 255) lexbuf }
16+
| '{' { LBRACE }
17+
| '}' { RBRACE }
18+
| "end" { END }
19+
| "exec" { EXEC }
20+
| "run" { RUN }
21+
| "interface" { INTERFACE }
22+
| "show" { SHOW }
23+
| "spec" { SPEC }
24+
| "trace" { TRACE }
25+
| "linear-exec" { LINEXEC }
26+
| "show-exec" { SHOWEXEC }
27+
| "galaxy" { GALAXY }
28+
| "process" { PROCESS }
29+
| "->" { RARROW }
30+
| "=>" { DRARROW }
31+
| "." { DOT }
32+
| "#" { SHARP }
33+
| "%" { PERCENT }
34+
| '"' { read_string (Buffer.create 255) lexbuf }
3435
(* Stellar resolution *)
35-
| '|' { BAR }
36-
| "!=" { NEQ }
37-
| '_' { PLACEHOLDER }
38-
| '[' { LBRACK }
39-
| ']' { RBRACK }
40-
| '(' { LPAR }
41-
| ')' { RPAR }
42-
| ',' { COMMA }
43-
| '@' { AT }
44-
| '+' { PLUS }
45-
| '-' { MINUS }
46-
| '=' { EQ }
47-
| ':' { CONS }
48-
| ';' { SEMICOLON }
49-
| var_id { VAR (Lexing.lexeme lexbuf) }
50-
| ident { SYM (Lexing.lexeme lexbuf) }
36+
| '|' { BAR }
37+
| "!=" { NEQ }
38+
| '_' { PLACEHOLDER }
39+
| '[' { LBRACK }
40+
| ']' { RBRACK }
41+
| '(' { LPAR }
42+
| ')' { RPAR }
43+
| ',' { COMMA }
44+
| '@' { AT }
45+
| '+' { PLUS }
46+
| '-' { MINUS }
47+
| '=' { EQ }
48+
| ':' { CONS }
49+
| ';' { SEMICOLON }
50+
| var_id { VAR (Lexing.lexeme lexbuf) }
51+
| ident { SYM (Lexing.lexeme lexbuf) }
5152
(* Common *)
52-
| '\'' { comment lexbuf }
53-
| "'''" { comments lexbuf }
54-
| space { read lexbuf }
55-
| newline {
53+
| '\'' { comment lexbuf }
54+
| "'''" { comments lexbuf }
55+
| space { read lexbuf }
56+
| newline {
5657
let pos = lexbuf.lex_curr_p in
5758
lexbuf.lex_curr_p <- {
5859
lexbuf.lex_curr_p with

‎src/stellogen/sgen_parser.mly‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ open Sgen_ast
99
%token SPEC
1010
%token TRACE
1111
%token SHARP
12+
%token LINEXEC
1213
%token PROCESS
1314
%token GALAXY
1415
%token RARROW DRARROW
@@ -95,6 +96,10 @@ let galaxy_block :=
9596
<Exec>
9697
| EXEC; EOL*; mcs=marked_constellation; END; EXEC?;
9798
{ Exec (Raw (Const mcs)) }
99+
| LINEXEC; EOL*; ~=galaxy_content; END; LINEXEC?;
100+
<LinExec>
101+
| LINEXEC; EOL*; mcs=marked_constellation; END; LINEXEC?;
102+
{ LinExec (Raw (Const mcs)) }
98103

99104
let process_item :=
100105
| ~=galaxy_content; DOT; EOL*; <>

0 commit comments

Comments
 (0)