Skip to content

Commit 8322ec2

Browse files
engborisengboris
committed
Merge branch 'master' of https://github.com/engboris/stellogen into identifiers
2 parents 763625e + 67b707e commit 8322ec2

File tree

9 files changed

+118
-65
lines changed

9 files changed

+118
-65
lines changed

‎bin/sgen.ml‎

Lines changed: 1 addition & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
open Base
22
open Stellogen.Sgen_eval
3-
open Stellogen.Sgen_parser
4-
open Stellogen.Sgen_lexer
53
open Lexing
64

75
let usage_msg = "sgen [--typecheck-only] <filename>"
@@ -21,21 +19,10 @@ let speclist =
2119
; ("--no-typing", Stdlib.Arg.Set notyping, "Perform execution without typing.")
2220
]
2321

24-
let print_position outx lexbuf =
25-
let pos = lexbuf.lex_curr_p in
26-
Stdlib.Printf.fprintf outx "%s:%d:%d" pos.pos_fname pos.pos_lnum
27-
(pos.pos_cnum - pos.pos_bol)
28-
29-
let parse_with_error lexbuf =
30-
try program read lexbuf
31-
with SyntaxError msg ->
32-
Stdlib.Printf.fprintf Stdlib.stderr "%a: %s\n" print_position lexbuf msg;
33-
raise (SyntaxError msg)
34-
3522
let () =
3623
Stdlib.Arg.parse speclist anon_fun usage_msg;
3724
let lexbuf = Lexing.from_channel (Stdlib.open_in !input_file) in
3825
lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = !input_file };
39-
let p = parse_with_error lexbuf in
26+
let p = Stellogen.Sgen_parsing.parse_with_error lexbuf in
4027
let _ = eval_program ~typecheckonly:!typecheckonly ~notyping:!notyping p in
4128
()

‎examples/syntax.sg‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,3 +102,22 @@ g_pair = galaxy
102102
n = +nat(0).
103103
m = +nat(0).
104104
end
105+
106+
'import file
107+
'use examples->automata.
108+
109+
'proof
110+
theorem x : nat =
111+
proof
112+
0.
113+
end
114+
115+
'proof lemma and end proof
116+
lemma y : nat =
117+
proof
118+
0.
119+
end proof
120+
121+
'complex identifiers
122+
f(a b) = function(a b).
123+
show #f(a b).

‎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 linear trace process end galaxy run interface
3+
syn keyword sgKeyword show use 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: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,5 +68,7 @@ type declaration =
6868
| Trace of galaxy_expr
6969
| Run of galaxy_expr
7070
| TypeDef of type_declaration
71+
| Use of ident list
72+
| ProofDef of ident * ident list * ident option * galaxy_expr
7173

7274
type program = declaration list

‎src/stellogen/sgen_eval.ml‎

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -483,16 +483,29 @@ let rec eval_decl ~typecheckonly ~notyping env :
483483
{ objs = add_obj env (const "^expect") (expect mcs)
484484
; types = add_type env x ([ const "^empty" ], Some (const "^expect"))
485485
}
486+
| ProofDef (x, ts, ck, g) ->
487+
eval_decl ~typecheckonly ~notyping
488+
{ objs = add_obj env x g; types = add_type env x (ts, ck) }
489+
(Def (x, g))
490+
| Use path ->
491+
let path = List.map path ~f:string_of_ray in
492+
let formatted_filename = String.concat ~sep:"/" path ^ ".sg" in
493+
let lexbuf = Lexing.from_channel (Stdlib.open_in formatted_filename) in
494+
lexbuf.lex_curr_p <-
495+
{ lexbuf.lex_curr_p with pos_fname = formatted_filename };
496+
let p = Sgen_parsing.parse_with_error lexbuf in
497+
let* env = eval_program ~typecheckonly ~notyping p in
498+
Ok env
486499

487-
let eval_program ~typecheckonly ~notyping p =
500+
and eval_program ~typecheckonly ~notyping p =
488501
match
489502
List.fold_left
490503
~f:(fun acc x ->
491504
let* acc = acc in
492505
eval_decl ~typecheckonly ~notyping acc x )
493506
~init:(Ok initial_env) p
494507
with
495-
| Ok _ -> Ok ()
508+
| Ok env -> Ok env
496509
| Error e ->
497510
let* pp = pp_err ~notyping e in
498511
output_string stderr pp;

‎src/stellogen/sgen_lexer.mll‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,15 @@ rule read = parse
2121
| "interface" { INTERFACE }
2222
| "show" { SHOW }
2323
| "spec" { SPEC }
24+
| "use" { USE }
2425
| "trace" { TRACE }
2526
| "linear-exec" { LINEXEC }
2627
| "show-exec" { SHOWEXEC }
2728
| "galaxy" { GALAXY }
2829
| "process" { PROCESS }
30+
| "proof" { PROOF }
31+
| "theorem" { THEOREM }
32+
| "lemma" { LEMMA }
2933
| "->" { RARROW }
3034
| "=>" { DRARROW }
3135
| "." { DOT }

‎src/stellogen/sgen_parser.mly‎

Lines changed: 55 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -3,18 +3,19 @@ open Sgen_ast
33
%}
44

55
%token SHOW SHOWEXEC
6-
%token EXEC
76
%token INTERFACE
7+
%token USE
88
%token RUN
99
%token SPEC
1010
%token TRACE
1111
%token SHARP
12-
%token LINEXEC
12+
%token EXEC LINEXEC
1313
%token PROCESS
1414
%token GALAXY
1515
%token RARROW DRARROW
1616
%token EQ
1717
%token END
18+
%token PROOF LEMMA THEOREM
1819

1920
%start <Sgen_ast.program> program
2021

@@ -25,27 +26,31 @@ let program :=
2526
| EOL*; d=declaration; EOL+; p=program; { d::p }
2627
| EOL*; d=declaration; EOF; { [d] }
2728

28-
let ident :=
29-
| ~=ray; <>
29+
let ident := ~=ray; <>
3030

3131
let declaration :=
32-
| SPEC; ~=ident; EOL*; EQ; EOL*;
33-
~=galaxy_expr; <Def>
34-
| ~=ident; EOL*; EQ; EOL*;
35-
~=galaxy_expr; <Def>
36-
| INTERFACE; EOL*; x=ident; EOL*;
37-
i=interface_item*;
38-
END; INTERFACE?; { Def (x, Raw (Interface i)) }
39-
| SHOW; EOL*; ~=galaxy_expr; <Show>
40-
| SHOWEXEC; EOL*; ~=galaxy_expr; <ShowExec>
41-
| TRACE; EOL*; ~=galaxy_expr; <Trace>
42-
| RUN; EOL*; ~=galaxy_expr; <Run>
43-
| ~=type_declaration; <TypeDef>
32+
| SPEC; ~=ident; EOL*; EQ; EOL*; ~=galaxy_expr; <Def>
33+
| ~=ident; EOL*; EQ; EOL*; ~=galaxy_expr; <Def>
34+
| SHOW; EOL*; ~=galaxy_expr; <Show>
35+
| SHOWEXEC; EOL*; ~=galaxy_expr; <ShowExec>
36+
| TRACE; EOL*; ~=galaxy_expr; <Trace>
37+
| RUN; EOL*; ~=galaxy_expr; <Run>
38+
| ~=type_declaration; <TypeDef>
39+
| USE; ~=separated_list(RARROW, ident); DOT; <Use>
40+
| proof_spec; x=ident; CONS; ts=separated_list(COMMA, ident);
41+
EOL*; ck=bracks(ident)?; EOL*; EQ; EOL*; g=galaxy_expr;
42+
{ ProofDef (x, ts, ck, g) }
43+
| INTERFACE; EOL*; x=ident; EOL*; i=interface_item*; END; INTERFACE?;
44+
{ Def (x, Raw (Interface i)) }
45+
46+
let proof_spec :=
47+
| THEOREM; EOL*; <>
48+
| LEMMA; EOL*; <>
4449

4550
let type_declaration :=
4651
| x=ident; CONS; CONS; ts=separated_list(COMMA, ident);
47-
EOL*; ck=bracks(ident)?; EOL*; DOT; { TDef (x, ts, ck) }
48-
| x=ident; CONS; EQ; CONS; EOL*; g=galaxy_expr; { TExp (x, g) }
52+
EOL*; ck=bracks(ident)?; EOL*; DOT; { TDef (x, ts, ck) }
53+
| x=ident; CONS; EQ; CONS; EOL*; g=galaxy_expr; { TExp (x, g) }
4954

5055
let galaxy_expr :=
5156
| ~=galaxy_content; EOL*; DOT; <>
@@ -60,26 +65,30 @@ let undelimited_raw_galaxy :=
6065
| GALAXY; EOL*; ~=galaxy_item*; EOL*; END; GALAXY?; <Galaxy>
6166

6267
let delimited_raw_galaxy :=
63-
| ~=pars(marked_constellation); <Const>
6468
| braces(EOL*); { Const [] }
69+
| ~=pars(marked_constellation); <Const>
6570
| ~=braces(marked_constellation); <Const>
6671

72+
let prefixed_id := SHARP; ~=ident; <Id>
73+
74+
let naked_id := ~=ident; <Id>
75+
6776
let galaxy_content :=
68-
| ~=pars(galaxy_content); <>
69-
| SHARP; ~=ident; <Id>
70-
| ~=delimited_raw_galaxy; <Raw>
71-
| g=galaxy_content; h=galaxy_content; { Union (g, h) }
72-
| ~=galaxy_access; <>
73-
| AT; ~=focussed_galaxy_content; <Focus>
74-
| ~=galaxy_content; ~=bracks(substitution); <Subst>
75-
| ~=galaxy_block; <>
77+
| ~=pars(galaxy_content); <>
78+
| ~=delimited_raw_galaxy; <Raw>
79+
| g=galaxy_content; h=galaxy_content; { Union (g, h) }
80+
| ~=galaxy_access; <>
81+
| AT; ~=focussed_galaxy_content; <Focus>
82+
| ~=galaxy_content; ~=bracks(substitution); <Subst>
83+
| ~=galaxy_block; <>
84+
| ~=prefixed_id; <>
7685

7786
let focussed_galaxy_content :=
78-
| ~=pars(galaxy_content); <>
79-
| ~=galaxy_access; <>
80-
| SHARP; ~=ident; <Id>
81-
| ~=delimited_raw_galaxy; <Raw>
82-
| ~=galaxy_block; <>
87+
| ~=pars(galaxy_content); <>
88+
| ~=galaxy_access; <>
89+
| ~=delimited_raw_galaxy; <Raw>
90+
| ~=galaxy_block; <>
91+
| ~=prefixed_id; <>
8392

8493
let galaxy_block :=
8594
| EXEC; EOL*; ~=galaxy_content; EOL*; END; EXEC?;
@@ -105,20 +114,25 @@ let substitution :=
105114
h=marked_constellation; { SGal (x, Raw (Const h)) }
106115

107116
let galaxy_item :=
108-
| ~=ident; EQ; EOL*; ~=galaxy_content; DOT; EOL*; <GLabelDef>
117+
| ~=ident; EQ; EOL*; ~=galaxy_content; DOT; EOL*;
118+
<GLabelDef>
109119
| x=ident; EQ; EOL*; mcs=marked_constellation; EOL*; DOT; EOL*;
110120
{ GLabelDef (x, Raw (Const mcs)) }
111121
| x=ident; EQ; EOL*; g=undelimited_raw_galaxy; EOL*; DOT; EOL*;
112122
{ GLabelDef (x, Raw g) }
113-
| ~=ident; EQ; EOL*; ~=process; EOL*; <GLabelDef>
114-
| ~=type_declaration; EOL*; <GTypeDef>
123+
| ~=ident; EQ; EOL*; ~=process; EOL*; <GLabelDef>
124+
| ~=type_declaration; EOL*; <GTypeDef>
115125

116126
let process :=
117-
| PROCESS; EOL*; END; PROCESS?;
118-
{ Process [] }
119-
| PROCESS; EOL*; ~=process_item+; END; PROCESS?;
120-
<Process>
127+
| PROCESS; EOL*; END; PROCESS?; { Process [] }
128+
| PROOF; EOL*; END; PROOF?; { Process [] }
129+
| PROCESS; EOL*; ~=process_item+; END; PROCESS?; <Process>
130+
| PROOF; EOL*; ~=proof_content+; END; PROOF?; <Process>
121131

122132
let process_item :=
123-
| ~=galaxy_content; DOT; EOL*; <>
124-
| ~=undelimited_raw_galaxy; EOL*; <Raw>
133+
| ~=galaxy_content; DOT; EOL*; <>
134+
| ~=undelimited_raw_galaxy; EOL*; <Raw>
135+
136+
let proof_content :=
137+
| ~=delimited_raw_galaxy; DOT; EOL*; <Raw>
138+
| ~=naked_id; DOT; EOL*; <>

‎src/stellogen/sgen_parsing.ml‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
open Lexing
2+
open Sgen_lexer
3+
open Sgen_parser
4+
5+
let print_position outx lexbuf =
6+
let pos = lexbuf.lex_curr_p in
7+
Stdlib.Printf.fprintf outx "%s:%d:%d" pos.pos_fname pos.pos_lnum
8+
(pos.pos_cnum - pos.pos_bol)
9+
10+
let parse_with_error lexbuf =
11+
try program read lexbuf
12+
with SyntaxError msg ->
13+
Stdlib.Printf.fprintf Stdlib.stderr "%a: %s\n" print_position lexbuf msg;
14+
raise (SyntaxError msg)

‎test/behavior/prolog.sg‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,22 +4,22 @@ add =
44
-add(X Y Z) +add(s(X) Y s(Z)).
55

66
tested :=: 0.
7-
tested = #add (@-add(0 0 R) R).
7+
tested = #add @(-add(0 0 R) R).
88

99
tested :=: s(0).
10-
tested = #add (@-add(s(0) 0 R) R).
10+
tested = #add @(-add(s(0) 0 R) R).
1111

1212
tested :=: s(0).
13-
tested = #add (@-add(0 s(0) R) R).
13+
tested = #add @(-add(0 s(0) R) R).
1414

1515
tested :=: s(s(s(s(0)))).
16-
tested = #add (@-add(s(s(0)) s(s(0)) R) R).
16+
tested = #add @(-add(s(s(0)) s(s(0)) R) R).
1717

1818
tested :=: 0.
19-
tested = #add (@-add(s(s(0)) R s(s(0))) R).
19+
tested = #add @(-add(s(s(0)) R s(s(0))) R).
2020

2121
tested :=: s(0).
22-
tested = #add (@-add(s(s(0)) R s(s(s(0)))) R).
22+
tested = #add @(-add(s(s(0)) R s(s(s(0)))) R).
2323

2424
tested :=: s(s(0)).
25-
tested = #add (@-add(s(s(0)) R s(s(s(s(0))))) R).
25+
tested = #add @(-add(s(s(0)) R s(s(s(s(0))))) R).

0 commit comments

Comments
 (0)