Skip to content

Commit 8702000

Browse files
marangetmaranget
committed
[herd] Special handling of union transitive closure in the Cat interpreter
We notice that `(...|r+|...)+` is `(...|r|...)+` and thus also that irrefexivity of `(...|r+|...)+` is equivalent to acyclicity of `(...|r|...)`. The process may be interesting because we also identify some of the recursive definitions that are equivalent to a transitive closure and represent them as (implicit) transitive closure, thereby saving some transitive closure operations. In practice, improvements are barely noticeable.
1 parent 19e460a commit 8702000

File tree

1 file changed

+104
-41
lines changed

1 file changed

+104
-41
lines changed

‎lib/interpreter.ml‎

Lines changed: 104 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -288,9 +288,11 @@ module Make
288288
| Tuple of v list
289289

290290
and env =
291-
{ vals : v Lazy.t StringMap.t;
292-
enums : string list StringMap.t;
293-
tags : string StringMap.t; }
291+
{ vals : v Lazy.t StringMap.t; (* Standard bindings *)
292+
(* Optionnal bindigs for (implicit) transitive relations *)
293+
trans : v Lazy.t StringMap.t;
294+
enums : string list StringMap.t;
295+
tags : string StringMap.t; }
294296
and closure =
295297
{ clo_args : AST.pat ;
296298
mutable clo_env : env ;
@@ -322,7 +324,8 @@ module Make
322324
| Tuple of v list
323325

324326
and env =
325-
{ vals : v Lazy.t StringMap.t;
327+
{ vals : v Lazy.t StringMap.t;
328+
trans : v Lazy.t StringMap.t;
326329
enums : string list StringMap.t;
327330
tags : string StringMap.t; }
328331
and closure =
@@ -509,6 +512,7 @@ module Make
509512

510513
let env_empty =
511514
{vals=StringMap.empty;
515+
trans=StringMap.empty;
512516
enums=StringMap.empty;
513517
tags=StringMap.empty; }
514518

@@ -690,9 +694,16 @@ module Make
690694
end
691695

692696
let find_env_loc loc env k =
693-
try find_env env.EV.env k
697+
try find_env env.EV.env k
694698
with Misc.UserError msg -> error env.EV.silent loc "%s" msg
695699

700+
let find_env_loc_trans loc env k =
701+
let e = env.EV.env in
702+
try Lazy.force @@ StringMap.find k e.trans
703+
with Not_found ->
704+
try find_env e k
705+
with Misc.UserError msg -> error env.EV.silent loc "%s" msg
706+
696707
(* find without forcing lazy's *)
697708
let just_find_env fail loc env k =
698709
try StringMap.find k env.EV.env.vals
@@ -811,7 +822,8 @@ module Make
811822
(* Tests are polymorphic, acting on relations, class relations and sets *)
812823
let test2pred env t e v = match t,v with
813824
| (Acyclic,(Rel r|TransRel r))
814-
| (Irreflexive,TransRel r) -> E.EventRel.is_acyclic r
825+
| (Irreflexive,TransRel r) ->
826+
E.EventRel.is_acyclic r
815827
| Acyclic,ClassRel r -> ClassRel.is_acyclic r
816828
| Irreflexive,Rel r -> E.EventRel.is_irreflexive r
817829
| Irreflexive,ClassRel r -> ClassRel.is_irreflexive r
@@ -1290,10 +1302,20 @@ module Make
12901302
error env.EV.silent loc "tag '%s is undefined" s
12911303
end
12921304
| Var (loc,k) ->
1293-
find_env_loc loc env k
1305+
if accept_implicit then
1306+
find_env_loc_trans loc env k
1307+
else
1308+
find_env_loc loc env k
12941309
| Fun (loc,xs,body,name,fvs) ->
12951310
Clo (eval_fun false env loc xs body name fvs)
12961311
(* Unary operators *)
1312+
| Op1 (_,Plus,Op (_,Union,es)) ->
1313+
begin
1314+
match eval_union_plus env es with
1315+
| TransRel r when not accept_implicit ->
1316+
Rel (E.EventRel.transitive_closure r)
1317+
| v -> v
1318+
end
12971319
| Op1 (_,Plus,e) ->
12981320
begin match eval true env e with
12991321
| V.Empty -> V.Empty
@@ -1703,6 +1725,28 @@ module Make
17031725
if eval_cond loc env cond then eval accept_implicit env ifso
17041726
else eval accept_implicit env ifnot
17051727

1728+
(*
1729+
* Evaluation of `(e1|..|en)+`
1730+
* Hence, `e1`, ...,`en` must be relations.
1731+
*)
1732+
and eval_union_plus env es =
1733+
try
1734+
let rs =
1735+
List.fold_right
1736+
(fun e k ->
1737+
match eval true env e with
1738+
| TransRel r (* `(..|ei+|...)+` = `(...|ei|...)+` *)
1739+
| Rel r -> r::k
1740+
| V.Empty -> k
1741+
| V.Unv -> raise Exit
1742+
| v ->
1743+
error_rel env.EV.silent (get_loc e) v)
1744+
es [] in
1745+
match rs with
1746+
| [] -> V.Empty
1747+
| _ -> TransRel (E.EventRel.unions rs)
1748+
with Exit -> Unv
1749+
17061750
and eval_diff env loc e1 e2 =
17071751
let loc1,v1 = eval_ord_loc env e1
17081752
and loc2,v2 = eval_ord_loc env e2 in
@@ -2013,7 +2057,7 @@ module Make
20132057
end ;
20142058
let env,ws = fix_step env_bd env bds in
20152059
let env = env_rec_funs { env_bd with EV.env=env;} loc funs in
2016-
let check_ok = check { env_bd with EV.env=env; } in
2060+
let check_ok = check { env_bd with EV.env=env; } in
20172061
if not check_ok then begin
20182062
if O.debug then warn loc "Fix point interrupted" ;
20192063
CheckFailed env
@@ -2214,7 +2258,7 @@ module Make
22142258
let eval_test check env t e =
22152259
let accept_implicit =
22162260
match t with
2217-
| Yes Acyclic|No Acyclic -> true
2261+
| Yes (Acyclic|Irreflexive)|No (Acyclic|Irreflexive) -> true
22182262
| _ -> false in
22192263
check (test2pred env t e (eval_rel_set accept_implicit env e)) in
22202264

@@ -2337,44 +2381,63 @@ module Make
23372381
let st = check_bell_order bds st in
23382382
kont st res
23392383
| Rec (loc,bds,testo) ->
2340-
let env =
2341-
match
2342-
env_rec
2343-
(make_eval_test testo) (from_st st)
2344-
loc (fun pp -> pp@show_to_vbpp st) bds
2345-
with
2346-
| CheckOk env -> Some env
2347-
| CheckFailed env ->
2348-
if O.debug then begin
2384+
begin
2385+
match testo,ASTUtils.as_plus bds with
2386+
| None,Some (x,es) ->
2387+
let env = from_st st in
2388+
let v = lazy (eval_union_plus env es) in
2389+
let env = env.EV.env in
2390+
let trans = StringMap.add x v env.trans
2391+
and vals =
2392+
let w =
2393+
lazy begin
2394+
match Lazy.force v with
2395+
| TransRel r ->
2396+
Rel (E.EventRel.transitive_closure r)
2397+
| v -> v
2398+
end in
2399+
StringMap.add x w env.vals in
2400+
let env = { env with vals; trans; } in
2401+
kont { st with env; } res
2402+
| _,_ ->
2403+
let env =
2404+
match
2405+
env_rec
2406+
(make_eval_test testo) (from_st st)
2407+
loc (fun pp -> pp@show_to_vbpp st) bds
2408+
with
2409+
| CheckOk env -> Some env
2410+
| CheckFailed env ->
2411+
if O.debug then begin
23492412
let st = { st with env; } in
23502413
let st = doshow bds st in
23512414
pp_check_failure st (Misc.as_some testo)
23522415
end ;
2353-
None in
2354-
begin match env with
2355-
| None -> kfail res
2356-
| Some env ->
2357-
let st = { st with env; } in
2358-
let st = doshow bds st in
2359-
2360-
(* Check again for strictskip *)
2361-
let st = match testo with
2362-
| None -> st
2363-
| Some (_,_,t,e,name) ->
2364-
if
2365-
O.strictskip &&
2366-
skip_this_check name &&
2367-
not (eval_test Misc.identity (from_st st) t e)
2368-
then begin
2369-
{ st with
2370-
skipped =
2371-
StringSet.add (Misc.as_some name) st.skipped;}
2416+
None in
2417+
begin match env with
2418+
| None -> kfail res
2419+
| Some env ->
2420+
let st = { st with env; } in
2421+
let st = doshow bds st in
2422+
(* Check again for strictskip *)
2423+
let st = match testo with
2424+
| None -> st
2425+
| Some (_,_,t,e,name) ->
2426+
if
2427+
O.strictskip &&
2428+
skip_this_check name &&
2429+
not (eval_test Misc.identity (from_st st) t e)
2430+
then begin
2431+
{ st with
2432+
skipped =
2433+
StringSet.add
2434+
(Misc.as_some name) st.skipped;}
23722435
end else st in
2373-
(* Check bell definitions *)
2374-
let st = check_bell_order bds st in
2375-
kont st res
2436+
(* Check bell definitions *)
2437+
let st = check_bell_order bds st in
2438+
kont st res
2439+
end
23762440
end
2377-
23782441
| InsMatch (loc,e,cls,d) ->
23792442
let v = eval_st st e in
23802443
begin match v with

0 commit comments

Comments
 (0)