Skip to content

Commit 2c20080

Browse files
committed
Remove interfaces and refactor AST
1 parent d8f5756 commit 2c20080

File tree

5 files changed

+59
-170
lines changed

5 files changed

+59
-170
lines changed

examples/syntax.sg

Lines changed: 21 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,10 @@
1818
(:= y (-f a))
1919
<show exec (union @#x #y)>
2020

21+
'complex identifiers
22+
(:= (f a b) [(function a b)])
23+
(show #(f a b))
24+
2125
'show (literal) contellations
2226
(show [ [a] [b] [c] ])
2327

@@ -52,47 +56,33 @@
5256
<show eval exec (union #g @[-test1])>
5357
<show eval exec (union #g @[-test2])>
5458

55-
'''
56-
'reactive effects
57-
(run (const
58-
(star (+&print X))
59-
(star (-&print "hello world\n"))))
60-
61-
'access to field of a galaxy
62-
(show (get g test1))
63-
(show (get g test2))
64-
6559
'extend rays with a head function symbol
66-
(show-exec (const (star (+f X)) (star (f X)))[=>+a])
67-
(show-exec (const (star (+f X)) (star (f X)))[=>a])
60+
'<show exec [[(+f X)] [(f X)]][=>+a]>
61+
'<show exec [[(+f X)] [(f X)]][=>a]>
6862

6963
'remove head function symbol from a ray
70-
(show-exec (const (star (+f X)) (star (f X)))[+f=>])
64+
'<show-exec [[(+f X)] [(f X)]][+f=>]>
7165

7266
'substitutions
73-
(show-exec
74-
(const (star (+f X)))[X=>(+a X)])
75-
(show-exec (const (star (+f X)))[+f=>+g])
76-
(show-exec (union #1 #2)
77-
[#1=>(const (star (+f X) X))]
78-
[#2=>(const (star (-f a)))])
67+
'<show exec (+f X)[X=>(+a X)]>
68+
'<show exec (+f X)[+f=>+g]>
69+
'<show exec (union #1 #2)
70+
' [#1=>[(+f X) X)]]
71+
' [#2=>(-f a)]>
7972

8073
'checkers & typechecking
81-
(def checker (galaxy
82-
(interaction (union @#tested #test))
83-
(expect (const (star ok)))))
74+
(:= checker [
75+
[+interaction (union @#tested #test)]
76+
[+expect ok]])
8477

85-
(spec nat
86-
(galaxy
87-
(test
88-
(const
89-
(star (-nat 0) ok)
90-
(star (-nat (s N)) (+nat N))))))
78+
(spec nat [
79+
[(-nat 0) ok)]
80+
[(-nat (s N)) (+nat N)]])
9181

92-
(:: 0 (nat /checker))
93-
(def 0
94-
(const (star (+nat 0))))
82+
'(:: 0 (nat | checker))
83+
'(:= 0 (+nat 0))
9584

85+
'''
9686
(:: 1 (nat / checker))
9787
(def 1
9888
(const (star (+nat (s 0)))))
@@ -114,29 +104,7 @@
114104
(def 4
115105
(const (star (+nat <s s s s /0>))))
116106

117-
(interface nat_pair
118-
(:: n nat)
119-
(:: m nat))
120-
121-
(:: g_pair nat_pair)
122-
(def g_pair
123-
(galaxy
124-
(n (const (star (+nat 0))))
125-
(m (const (star (+nat 0))))))
126-
127-
'galaxy with type declarations
128-
(show (galaxy
129-
(:: n1 nat)
130-
(n1 (const (star (+nat 0))))
131-
(:: n2 nat)
132-
(n2 (const (star (+nat <s s /0>))))))
133-
134107
'import file
135108
'(use examples automata)
136109

137-
'complex identifiers
138-
(def (f a b)
139-
(const
140-
(star (function a b))))
141-
(show #(f a b))
142110
'''

nvim/syntax/stellogen.vim

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

3-
syn keyword sgKeyword def kill clean const star show use exec spec linear trace process end galaxy run interface union
3+
syn keyword sgKeyword kill clean eval show use exec spec linear trace process run union
44
syn match sgComment "\s*'[^'].*$"
55
syn match sgId "#\%(\l\|\d\)\w*"
66
syn region sgComment start="'''" end="'''" contains=NONE
@@ -9,7 +9,9 @@ syn match sgSeparator "[\<\>\{\}\[\]|]"
99
syn match sgOperator "@"
1010
syn match sgOperator "::"
1111
syn match sgOperator "=="
12+
syn match sgOperator ":="
1213
syn match sgOperator "!="
14+
syn match sgOperator "&"
1315

1416
hi link sgKeyword Keyword
1517
hi link sgId Identifier

src/expr.ml

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ let symbol_of_str (s : string) : idfunc =
8282
let rec ray_of_expr : expr -> ray = function
8383
| Symbol s -> to_func ((Muted, symbol_of_str s), [])
8484
| Var s -> to_var s
85-
| Unquote e -> failwith ("error: cannot unquote ray " ^ to_string e)
85+
| Unquote e -> to_func ((Muted, (Null, "#")), [ ray_of_expr e ])
8686
| List [] -> failwith "error: ray cannot be empty"
8787
| List (Symbol h :: t) ->
8888
to_func ((Muted, symbol_of_str h), List.map ~f:ray_of_expr t)
@@ -179,10 +179,20 @@ let rec galaxy_expr_of_expr (e : expr) : galaxy_expr =
179179
Stellogen program of Expr
180180
--------------------------------------- *)
181181

182+
(* let typedecl_of_expr : expr -> type_declaration = function
183+
| Symbol k when equal_string k nil_op -> []
184+
| List [ Symbol k; h; t ] when equal_string k cons_op ->
185+
*)
186+
182187
let decl_of_expr : expr -> declaration = function
183188
(* definition := *)
184189
| List [ Symbol k; x; g ] when equal_string k def_op ->
185190
Def (ray_of_expr x, galaxy_expr_of_expr g)
191+
| List [ Symbol k; x; g ] when equal_string k "spec" ->
192+
Def (ray_of_expr x, galaxy_expr_of_expr g)
193+
(* type declaration :: *)
194+
(* | List [ Symbol k; x; g ] when equal_string k typedef_op ->
195+
Typedecl (ray_of_expr x, typedecl_of_expr g) *)
186196
(* show *)
187197
| List [ Symbol k; g ] when equal_string k "show" ->
188198
Show (galaxy_expr_of_expr g)
@@ -191,7 +201,7 @@ let decl_of_expr : expr -> declaration = function
191201
Trace (galaxy_expr_of_expr g)
192202
(* expect *)
193203
| List [ Symbol k; x; g ] when equal_string k expect_op ->
194-
TypeDef (TExp (ray_of_expr x, galaxy_expr_of_expr g))
204+
Expect (ray_of_expr x, galaxy_expr_of_expr g)
195205
| _ -> failwith "error: invalid declaration"
196206

197207
let program_of_expr = List.map ~f:decl_of_expr

src/sgen_ast.ml

Lines changed: 4 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -9,18 +9,9 @@ type idfunc = polarity * string
99

1010
type ray_prefix = StellarRays.fmark * idfunc
1111

12-
type type_declaration =
13-
| TDef of ident * (ident * ident option) list
14-
| TExp of ident * galaxy_expr
15-
1612
and galaxy =
1713
| Const of marked_constellation
18-
| Galaxy of galaxy_declaration list
19-
| Interface of type_declaration list
20-
21-
and galaxy_declaration =
22-
| GTypeDef of type_declaration
23-
| GLabelDef of ident * galaxy_expr
14+
| Galaxy of (ident * galaxy_expr) list
2415

2516
and galaxy_expr =
2617
| Raw of galaxy
@@ -54,10 +45,7 @@ type env =
5445

5546
let expect (g : galaxy_expr) : galaxy_expr =
5647
Raw
57-
(Galaxy
58-
[ GLabelDef (const "interaction", Id (const "tested"))
59-
; GLabelDef (const "expect", g)
60-
] )
48+
(Galaxy [ (const "interaction", Id (const "tested")); (const "expect", g) ])
6149

6250
let initial_env =
6351
{ objs = [ (const "^empty", Raw (Const [])) ]
@@ -69,7 +57,8 @@ type declaration =
6957
| Show of galaxy_expr
7058
| Trace of galaxy_expr
7159
| Run of galaxy_expr
72-
| TypeDef of type_declaration
60+
| Typedecl of ident * (ident * ident option) list
61+
| Expect of ident * galaxy_expr
7362
| Use of ident list
7463

7564
type program = declaration list

0 commit comments

Comments
 (0)