Skip to content

Commit 96ac5c7

Browse files
engborisengboris
committed
Extend identifiers to general rays (non-parametric)
1 parent 7dbd500 commit 96ac5c7

File tree

4 files changed

+88
-84
lines changed

4 files changed

+88
-84
lines changed

‎src/stellogen/sgen_ast.ml‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
open Base
22
open Lsc_ast
33

4-
type ident = string
4+
type ident = StellarRays.term
55

66
type idvar = string * int option
77

@@ -36,13 +36,13 @@ and galaxy_expr =
3636
and substitution =
3737
| Extend of ray_prefix
3838
| Reduce of ray_prefix
39-
| SVar of ident * StellarRays.term
39+
| SVar of string * StellarRays.term
4040
| SFunc of (StellarRays.fmark * idfunc) * (StellarRays.fmark * idfunc)
4141
| SGal of ident * galaxy_expr
4242

43-
let reserved_words = [ "clean"; "kill" ]
43+
let reserved_words = [ const "clean"; const "kill" ]
4444

45-
let is_reserved = List.mem reserved_words ~equal:equal_string
45+
let is_reserved = List.mem reserved_words ~equal:equal_ray
4646

4747
type env =
4848
{ objs : (ident * galaxy_expr) list
@@ -51,11 +51,11 @@ type env =
5151

5252
let expect (g : galaxy_expr) : galaxy_expr =
5353
Raw
54-
(Galaxy [ GLabelDef ("interaction", Id "tested"); GLabelDef ("expect", g) ])
54+
(Galaxy [ GLabelDef (const "interaction", Id (const "tested")); GLabelDef (const "expect", g) ])
5555

5656
let initial_env =
57-
{ objs = [ ("^empty", Raw (Const [])) ]
58-
; types = [ ("^empty", ([ "^empty" ], None)) ]
57+
{ objs = [ (const "^empty", Raw (Const [])) ]
58+
; types = [ (const "^empty", ([ const "^empty" ], None)) ]
5959
}
6060

6161
type declaration =

‎src/stellogen/sgen_err.ml‎

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,11 @@
11
open Base
22
open Sgen_ast
33

4-
type ident = string
5-
64
type err =
75
| IllFormedChecker
86
| ExpectedGalaxy
9-
| ReservedWord of ident
10-
| UnknownField of ident
11-
| UnknownID of ident
12-
| TestFailed of ident * ident * ident * galaxy * galaxy
7+
| ReservedWord of string
8+
| UnknownField of string
9+
| UnknownID of string
10+
| TestFailed of string * string * string * galaxy * galaxy
1311
| LscError of Lsc_err.err_effect

‎src/stellogen/sgen_eval.ml‎

Lines changed: 53 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -9,13 +9,13 @@ open Out_channel
99

1010
let ( let* ) x f = Result.bind x ~f
1111

12-
let add_obj env x e = List.Assoc.add ~equal:equal_string env.objs x e
12+
let add_obj env x e = List.Assoc.add ~equal:equal_ray env.objs x e
1313

14-
let get_obj env x = List.Assoc.find ~equal:equal_string env.objs x
14+
let get_obj env x = List.Assoc.find ~equal:equal_ray env.objs x
1515

16-
let add_type env x e = List.Assoc.add ~equal:equal_string env.types x e
16+
let add_type env x e = List.Assoc.add ~equal:equal_ray env.types x e
1717

18-
let get_type env x = List.Assoc.find ~equal:equal_string env.types x
18+
let get_type env x = List.Assoc.find ~equal:equal_ray env.types x
1919

2020
let rec map_galaxy env ~f : galaxy -> (galaxy, err) Result.t = function
2121
| Const mcs -> Const (f mcs) |> Result.return
@@ -42,7 +42,7 @@ and map_galaxy_expr env ~f : galaxy_expr -> (galaxy_expr, err) Result.t =
4242
| Id x when is_reserved x -> Ok (Id x)
4343
| Id x -> begin
4444
match get_obj env x with
45-
| None -> Error (UnknownID x)
45+
| None -> Error (UnknownID (string_of_ray x))
4646
| Some g -> map_galaxy_expr env ~f g
4747
end
4848
| Exec e ->
@@ -82,7 +82,7 @@ let rec replace_id env (_from : ident) (_to : galaxy_expr) e :
8282
(galaxy_expr, err) Result.t =
8383
match e with
8484
| Id x when is_reserved x -> Ok (Id x)
85-
| Id x when equal_string x _from -> Ok _to
85+
| Id x when equal_ray x _from -> Ok _to
8686
| Access (g, x) ->
8787
let* g' = replace_id env _from _to g in
8888
Access (g', x) |> Result.return
@@ -113,11 +113,10 @@ let subst_vars env _from _to =
113113
let subst_funcs env _from _to =
114114
map_galaxy_expr env ~f:(subst_all_funcs [ (_from, _to) ])
115115

116-
let group_galaxy =
117-
List.fold_left ~init:([], []) ~f:(function types, fields ->
118-
(function
116+
let group_galaxy : galaxy_declaration list -> type_declaration list * (StellarRays.term * galaxy_expr) list =
117+
List.fold_left ~init:([], []) ~f:(function types, fields -> function
119118
| GTypeDef d -> (d :: types, fields)
120-
| GLabelDef (x, g') -> (types, (x, g') :: fields) ) )
119+
| GLabelDef (x, g') -> (types, (x, g') :: fields) )
121120

122121
let rec typecheck_galaxy ~notyping env (g : galaxy_declaration list) :
123122
(unit, err) Result.t =
@@ -126,14 +125,14 @@ let rec typecheck_galaxy ~notyping env (g : galaxy_declaration list) :
126125
| TExp (x, g) ->
127126
let checker = expect g in
128127
let new_env = { types = env.types; objs = fields @ env.objs } in
129-
typecheck ~notyping new_env x "^empty" checker
128+
typecheck ~notyping new_env x (const "^empty") checker
130129
| TDef (x, ts, ck) ->
131130
let* checker =
132131
match ck with
133132
| None -> Ok default_checker
134133
| Some xck -> begin
135134
match get_obj env xck with
136-
| None -> Error (UnknownID xck)
135+
| None -> Error (UnknownID (string_of_ray xck))
137136
| Some g -> Ok g
138137
end
139138
in
@@ -142,7 +141,7 @@ let rec typecheck_galaxy ~notyping env (g : galaxy_declaration list) :
142141
|> Result.all_unit )
143142
|> Result.all_unit
144143

145-
and pp_err ~notyping e : (ident, err) Result.t =
144+
and pp_err ~notyping e : (string, err) Result.t =
146145
match e with
147146
| IllFormedChecker -> "Ill-formed checker.\n" |> Result.return
148147
| ExpectedGalaxy -> "Expected galaxy.\n" |> Result.return
@@ -178,21 +177,21 @@ and eval_galaxy_expr ~notyping (env : env) :
178177
| Raw (Interface _) -> Ok (Interface [])
179178
| Access (e, x) -> begin
180179
match eval_galaxy_expr ~notyping env e with
181-
| Ok (Const _) -> Error (UnknownField x)
182-
| Ok (Interface _) -> Error (UnknownField x)
180+
| Ok (Const _) -> Error (UnknownField (string_of_ray x))
181+
| Ok (Interface _) -> Error (UnknownField (string_of_ray x))
183182
| Ok (Galaxy g) -> (
184183
let _, fields = group_galaxy g in
185184
try
186185
fields |> fun g ->
187-
List.Assoc.find_exn ~equal:equal_string g x
186+
List.Assoc.find_exn ~equal:equal_ray g x
188187
|> eval_galaxy_expr ~notyping env
189-
with Not_found_s _ -> Error (UnknownField x) )
188+
with Not_found_s _ -> Error (UnknownField (string_of_ray x)) )
190189
| Error e -> Error e
191190
end
192191
| Id x -> begin
193192
begin
194193
match get_obj env x with
195-
| None -> Error (UnknownID x)
194+
| None -> Error (UnknownID (string_of_ray x))
196195
| Some g -> eval_galaxy_expr ~notyping env g
197196
end
198197
end
@@ -231,8 +230,8 @@ and eval_galaxy_expr ~notyping (env : env) :
231230
List.fold_left t ~init:(Ok init) ~f:(fun acc x ->
232231
let* acc = acc in
233232
match x with
234-
| Id "kill" -> acc |> remove_mark_all |> kill |> focus |> Result.return
235-
| Id "clean" ->
233+
| Id (Func ((Muted, (Null, "kill")), [])) -> acc |> remove_mark_all |> kill |> focus |> Result.return
234+
| Id (Func ((Muted, (Null, "clean")), [])) ->
236235
acc |> remove_mark_all |> clean |> focus |> Result.return
237236
| _ ->
238237
let origin = acc |> remove_mark_all |> focus in
@@ -294,93 +293,100 @@ and check_interface ~notyping env x i =
294293
match get_obj env x with
295294
| Some (Raw (Galaxy g)) -> Ok g
296295
| Some _ -> Error ExpectedGalaxy
297-
| None -> Error (UnknownID x)
296+
| None -> Error (UnknownID (string_of_ray x))
298297
in
299298
let type_decls = List.map i ~f:(fun t -> GTypeDef t) in
300299
typecheck_galaxy ~notyping env (type_decls @ g)
301300

302-
and typecheck ~notyping env x t (ck : galaxy_expr) : (unit, err) Result.t =
303-
let* gtests =
301+
and typecheck ~notyping env x (t : StellarRays.term) (ck : galaxy_expr) : (unit, err) Result.t =
302+
let* gtests : (StellarRays.term * galaxy_expr) list =
304303
match get_obj env t with
305-
| Some (Raw (Const mcs)) -> Ok [ ("_", Raw (Const mcs)) ]
304+
| Some (Raw (Const mcs)) -> Ok [ (const "_", Raw (Const mcs)) ]
306305
| Some (Raw (Interface i)) ->
307306
let* _ = check_interface ~notyping env x i in
308307
Ok []
309308
| Some (Raw (Galaxy gtests)) -> group_galaxy gtests |> snd |> Result.return
310309
| Some e ->
311310
let* eval_e = eval_galaxy_expr ~notyping env e in
312311
let* mcs = galaxy_to_constellation ~notyping env eval_e in
313-
[ ("test", Raw (Const mcs)) ] |> Result.return
314-
| None -> Error (UnknownID x)
312+
[ (const "test", Raw (Const mcs)) ] |> Result.return
313+
| None -> Error (UnknownID (string_of_ray x))
315314
in
316315
let testing =
317316
List.map gtests ~f:(fun (idtest, test) ->
318317
match ck with
319318
| Raw (Galaxy gck) ->
320319
let format =
321320
try
322-
List.Assoc.find_exn ~equal:equal_string
321+
List.Assoc.find_exn ~equal:equal_ray
323322
(group_galaxy gck |> snd)
324-
"interaction"
323+
(const "interaction")
325324
with Not_found_s _ -> default_interaction
326325
in
327326
begin
328327
match get_obj env x with
329-
| None -> Error (UnknownID x)
328+
| None -> Error (UnknownID (string_of_ray x))
330329
| Some obj_x ->
331330
Ok
332331
( idtest
333332
, Exec
334333
(Subst
335-
( Subst (format, SGal ("test", test))
336-
, SGal ("tested", obj_x) ) )
334+
( Subst (format, SGal (const "test", test))
335+
, SGal (const "tested", obj_x) ) )
337336
|> eval_galaxy_expr ~notyping env )
338337
end
339338
| _ -> Error IllFormedChecker )
340339
in
341-
let expect = Access (ck, "expect") in
340+
let expect = Access (ck, const "expect") in
342341
let* eval_exp = eval_galaxy_expr ~notyping env expect in
343342
List.map testing ~f:(function
344343
| Ok (idtest, got) ->
345344
let* got = got in
346345
let* eq = equal_galaxy ~notyping env got eval_exp in
347-
if not eq then Error (TestFailed (x, t, idtest, got, eval_exp)) else Ok ()
346+
if not eq then Error (TestFailed (string_of_ray x, string_of_ray t, string_of_ray idtest, got, eval_exp)) else Ok ()
348347
| Error e -> Error e )
349348
|> Result.all_unit
350349

351-
and default_interaction = Union (Focus (Id "tested"), Id "test")
350+
and default_interaction = Union (Focus (Id (const "tested")), Id (const "test"))
352351

353352
and default_expect =
354353
Raw (Const [ Unmarked { content = [ func "ok" [] ]; bans = [] } ])
355354

356355
and default_checker : galaxy_expr =
357356
Raw
358357
(Galaxy
359-
[ GLabelDef ("interaction", default_interaction)
360-
; GLabelDef ("expect", default_expect)
358+
[ GLabelDef (const "interaction", default_interaction)
359+
; GLabelDef (const "expect", default_expect)
361360
] )
362361

363362
and string_of_type_declaration ~notyping env = function
364363
| TDef (x, ts, None) ->
365-
Printf.sprintf " %s :: %s.\n" x (string_of_list Fn.id "," ts)
364+
let str_x = string_of_ray x in
365+
let str_ts = List.map ts ~f:string_of_ray in
366+
Printf.sprintf " %s :: %s.\n" str_x (string_of_list Fn.id "," str_ts)
366367
| TDef (x, ts, Some xck) ->
367-
Printf.sprintf " %s :: %s [%s].\n" x (string_of_list Fn.id "," ts) xck
368+
let str_x = string_of_ray x in
369+
let str_xck = string_of_ray xck in
370+
let str_ts = List.map ts ~f:string_of_ray in
371+
Printf.sprintf " %s :: %s [%s].\n" str_x (string_of_list Fn.id "," str_ts) str_xck
368372
| TExp (x, g) -> (
369373
match eval_galaxy_expr ~notyping env g with
370374
| Error _ -> failwith "Error: string_of_type_declaration"
371375
| Ok eval_g ->
372-
Printf.sprintf "%s :=: %s" x (string_of_galaxy ~notyping env eval_g) )
376+
let str_x = string_of_ray x in
377+
Printf.sprintf "%s :=: %s" str_x (string_of_galaxy ~notyping env eval_g) )
373378

374379
and string_of_galaxy_declaration ~notyping env = function
375380
| GLabelDef (k, v) -> begin
376381
match eval_galaxy_expr ~notyping env v with
377382
| Error _ -> failwith "Error: string_of_galaxy_declaration"
378383
| Ok eval_v ->
379-
Printf.sprintf " %s = %s\n" k (string_of_galaxy ~notyping env eval_v)
384+
let str_k = string_of_ray k in
385+
Printf.sprintf " %s = %s\n" str_k (string_of_galaxy ~notyping env eval_v)
380386
end
381387
| GTypeDef decl -> string_of_type_declaration ~notyping env decl
382388

383-
and string_of_galaxy ~notyping env : galaxy -> ident = function
389+
and string_of_galaxy ~notyping env : galaxy -> string = function
384390
| Const mcs -> mcs |> remove_mark_all |> string_of_constellation
385391
| Interface i ->
386392
let content =
@@ -393,13 +399,13 @@ and string_of_galaxy ~notyping env : galaxy -> ident = function
393399

394400
let rec eval_decl ~typecheckonly ~notyping env :
395401
declaration -> (env, err) Result.t = function
396-
| Def (x, _) when is_reserved x -> Error (ReservedWord x)
402+
| Def (x, _) when is_reserved x -> Error (ReservedWord (string_of_ray x))
397403
| Def (x, e) ->
398404
let env = { objs = add_obj env x e; types = env.types } in
399405
let* _ =
400406
if notyping then Ok ()
401407
else
402-
List.filter env.types ~f:(fun (y, _) -> equal_string x y)
408+
List.filter env.types ~f:(fun (y, _) -> equal_ray x y)
403409
|> List.map ~f:(fun (_, (ts, ck)) ->
404410
match ck with
405411
| None ->
@@ -408,7 +414,7 @@ let rec eval_decl ~typecheckonly ~notyping env :
408414
|> Result.all_unit
409415
| Some xck -> begin
410416
match get_obj env xck with
411-
| None -> Error (UnknownID xck)
417+
| None -> Error (UnknownID (string_of_ray xck))
412418
| Some obj_xck ->
413419
List.map ts ~f:(fun t -> typecheck ~notyping env x t obj_xck)
414420
|> Result.all_unit
@@ -419,7 +425,7 @@ let rec eval_decl ~typecheckonly ~notyping env :
419425
| Show _ when typecheckonly -> Ok env
420426
| Show (Id x) -> begin
421427
match get_obj env x with
422-
| None -> Error (UnknownID x)
428+
| None -> Error (UnknownID (string_of_ray x))
423429
| Some e -> eval_decl ~typecheckonly ~notyping env (Show e)
424430
end
425431
| Show (Raw (Galaxy g)) ->
@@ -459,8 +465,8 @@ let rec eval_decl ~typecheckonly ~notyping env :
459465
Ok { objs = env.objs; types = add_type env x (ts, ck) }
460466
| TypeDef (TExp (x, mcs)) ->
461467
Ok
462-
{ objs = add_obj env "^expect" (expect mcs)
463-
; types = add_type env x ([ "^empty" ], Some "^expect")
468+
{ objs = add_obj env (const "^expect") (expect mcs)
469+
; types = add_type env x ([ const "^empty" ], Some (const "^expect"))
464470
}
465471

466472
let eval_program ~typecheckonly ~notyping p =

0 commit comments

Comments
 (0)