Skip to content

[herd] More implicit transitive relations in the Cat interpreter #1719

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
maranget wants to merge 4 commits into
base: master
Choose a base branch
from
Open

[herd] More implicit transitive relations in the Cat interpreter #1719

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
fe7e1ca
[herd,cat] Identify recursive definitions that reduce to transitive c…
maranget Feb 12, 2026
70f0e5a
[herd] Special handling of union transitive closure in the Cat interp…
maranget Feb 17, 2026
d9f45c1
[herd] Use left-to-right scan for union arguments
maranget Feb 19, 2026
15a920b
[herd] Extend special transitive handline to let bindings
maranget Feb 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 32 additions & 0 deletions lib/ASTUtils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -202,3 +202,35 @@ let free_body xs e =
(fun r p0 -> remove_pat0 p0 r)
(free e)
xs


let rec as_plus_args saw_seq x = function
| [] -> [],saw_seq
| e::es ->
if StringSet.mem x (free e) then
match e with
| Op (_,Seq,[Var (_,x1);Var (_,x2)]) ->
if String.equal x1 x && String.equal x2 x then
as_plus_args true x es
else raise Exit
| _ -> raise Exit
else
let es,saw_seq = as_plus_args saw_seq x es in
e::es,saw_seq

let as_plus = function
| [_,Pvar (Some x),Op (_,Union,es)] ->
begin
try
let es,saw_seq = as_plus_args false x es in
if saw_seq then Some (x,es) else None
Copy link
Copy Markdown
Collaborator

@HadrienRenaud HadrienRenaud Feb 18, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we have a warning that the rec flag is useless in that case?

Copy link
Copy Markdown
Member Author

@maranget maranget Feb 19, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd rather leave this to another PR.

with Exit -> None
end
| _ -> None

let rec check_accept_implicit = function
| Var _|Op1 (_,(Plus|Star|Opt|Inv),_) -> true
| Bind (_,_,e)|BindRec (_,_,e) -> check_accept_implicit e
| If (_,_,e1,e2) ->
check_accept_implicit e1 || check_accept_implicit e2
| _ -> false
10 changes: 10 additions & 0 deletions lib/ASTUtils.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,3 +30,13 @@ val flatten : AST.exp -> AST.exp

(* Get free variables *)
val free_body : AST.var option list -> AST.exp -> AST.varset

(* Is a recursive binding equivalent to transitive closure? *)
val as_plus : AST.binding list -> (AST.var * AST.exp list) option

(* Is it possible that the evaluaton of this expression returns
* and implicit transitive relation?
* Notice that this function is used for optimisation purposes
* and this need not to be complete, nor even correct...
*)
val check_accept_implicit : AST.exp -> bool
191 changes: 129 additions & 62 deletions lib/interpreter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -288,9 +288,11 @@ module Make
| Tuple of v list

and env =
{ vals : v Lazy.t StringMap.t;
enums : string list StringMap.t;
tags : string StringMap.t; }
{ vals : v Lazy.t StringMap.t; (* Standard bindings *)
(* Optionnal bindigs for (implicit) transitive relations *)
trans : v Lazy.t StringMap.t;
enums : string list StringMap.t;
tags : string StringMap.t; }
and closure =
{ clo_args : AST.pat ;
mutable clo_env : env ;
Expand Down Expand Up @@ -322,7 +324,8 @@ module Make
| Tuple of v list

and env =
{ vals : v Lazy.t StringMap.t;
{ vals : v Lazy.t StringMap.t;
trans : v Lazy.t StringMap.t;
enums : string list StringMap.t;
tags : string StringMap.t; }
and closure =
Expand Down Expand Up @@ -488,6 +491,19 @@ module Make
| None -> env
| Some k -> do_add_val k v env

let add_trans_val _loc x v env =
let trans = StringMap.add x v env.trans
and vals =
let w =
lazy begin
match Lazy.force v with
| TransRel r ->
Rel (E.EventRel.transitive_closure r)
| v -> v
end in
StringMap.add x w env.vals in
{ env with vals; trans; }

let add_pat_val silent loc pat v env = match pat with
| Pvar k -> add_val k v env
| Ptuple ks ->
Expand All @@ -509,6 +525,7 @@ module Make

let env_empty =
{vals=StringMap.empty;
trans=StringMap.empty;
enums=StringMap.empty;
tags=StringMap.empty; }

Expand Down Expand Up @@ -690,9 +707,16 @@ module Make
end

let find_env_loc loc env k =
try find_env env.EV.env k
try find_env env.EV.env k
with Misc.UserError msg -> error env.EV.silent loc "%s" msg

let find_env_loc_trans loc env k =
let e = env.EV.env in
try Lazy.force @@ StringMap.find k e.trans
with Not_found ->
try find_env e k
with Misc.UserError msg -> error env.EV.silent loc "%s" msg

(* find without forcing lazy's *)
let just_find_env fail loc env k =
try StringMap.find k env.EV.env.vals
Expand Down Expand Up @@ -811,7 +835,8 @@ module Make
(* Tests are polymorphic, acting on relations, class relations and sets *)
let test2pred env t e v = match t,v with
| (Acyclic,(Rel r|TransRel r))
| (Irreflexive,TransRel r) -> E.EventRel.is_acyclic r
| (Irreflexive,TransRel r) ->
E.EventRel.is_acyclic r
| Acyclic,ClassRel r -> ClassRel.is_acyclic r
| Irreflexive,Rel r -> E.EventRel.is_irreflexive r
| Irreflexive,ClassRel r -> ClassRel.is_irreflexive r
Expand Down Expand Up @@ -861,13 +886,13 @@ module Make

(* Union is polymorphic *)
let union_args =
let rec u_rec = function
| [] -> []
| (_,V.Empty)::xs -> u_rec xs
| (_,Unv)::_ -> raise Exit
| (loc,v)::xs ->
(loc,tag2set v)::u_rec xs in
u_rec
List.fold_left
(fun k p ->
match p with
| (_,V.Empty) -> k
| (_,Unv) -> raise Exit
| (loc,v) -> (loc,tag2set v)::k)
[]

(* Definition of primitives *)

Expand Down Expand Up @@ -1290,10 +1315,20 @@ module Make
error env.EV.silent loc "tag '%s is undefined" s
end
| Var (loc,k) ->
find_env_loc loc env k
if accept_implicit then
find_env_loc_trans loc env k
else
find_env_loc loc env k
| Fun (loc,xs,body,name,fvs) ->
Clo (eval_fun false env loc xs body name fvs)
(* Unary operators *)
| Op1 (_,Plus,Op (_,Union,es)) ->
begin
match eval_union_plus env es with
| TransRel r when not accept_implicit ->
Rel (E.EventRel.transitive_closure r)
| v -> v
end
| Op1 (_,Plus,e) ->
begin match eval true env e with
| V.Empty -> V.Empty
Expand Down Expand Up @@ -1394,7 +1429,7 @@ module Make
V.Tuple (List.map (eval accept_implicit env) es)
(* N-ary operators, those associative binary operators are optimized *)
| Op (loc,Union,es) ->
let vs = List.map (eval_loc false env) es in
let vs = List.rev_map (eval_loc false env) es in
begin try
let vs = union_args vs in
match vs with
Expand Down Expand Up @@ -1703,6 +1738,29 @@ module Make
if eval_cond loc env cond then eval accept_implicit env ifso
else eval accept_implicit env ifnot

(*
* Evaluation of `(e1|..|en)+`
* Hence, `e1`, ...,`en` must be relations.
*)
and eval_union_plus env es =
try
let rs =
(* Union being commutative, the order of `rs` is irrelevant *)
List.fold_left
(fun k e ->
match eval true env e with
| TransRel r (* `(..|ei+|...)+` = `(...|ei|...)+` *)
| Rel r -> r::k
| V.Empty -> k
| V.Unv -> raise Exit
| v ->
error_rel env.EV.silent (get_loc e) v)
[] es in
match rs with
| [] -> V.Empty
| _ -> TransRel (E.EventRel.unions rs)
with Exit -> Unv

and eval_diff env loc e1 e2 =
let loc1,v1 = eval_ord_loc env e1
and loc2,v2 = eval_ord_loc env e2 in
Expand Down Expand Up @@ -1919,19 +1977,20 @@ module Make

(* For let *)
and eval_bds env_bd =
let rec do_rec bds = match bds with
| [] -> env_bd.EV.env
| (loc,p,e)::bds ->
(*
begin match v with
| Rel r -> printf "Defining relation %s = {%a}.\n" k debug_rel r
| Set s -> printf "Defining set %s = %a.\n" k debug_set s
| Clo _ -> printf "Defining function %s.\n" k
end;
*)
add_pat_val env_bd.EV.silent loc
p (lazy (eval_ord env_bd e)) (do_rec bds) in
do_rec
let rec do_rec env_r bds = match bds with
| [] -> env_r
| (_,Pvar None,_)::bds -> do_rec env_r bds
| (loc,Pvar (Some x),e)::bds
when ASTUtils.check_accept_implicit e ->
let v = lazy (eval true env_bd e) in
do_rec (add_trans_val loc x v env_r) bds
| (loc,p,e)::bds ->
do_rec
(add_pat_val env_bd.EV.silent loc
p (lazy (eval_ord env_bd e))
env_r)
bds in
do_rec env_bd.EV.env

(* For let rec *)

Expand Down Expand Up @@ -2013,7 +2072,7 @@ module Make
end ;
let env,ws = fix_step env_bd env bds in
let env = env_rec_funs { env_bd with EV.env=env;} loc funs in
let check_ok = check { env_bd with EV.env=env; } in
let check_ok = check { env_bd with EV.env=env; } in
if not check_ok then begin
if O.debug then warn loc "Fix point interrupted" ;
CheckFailed env
Expand Down Expand Up @@ -2214,7 +2273,7 @@ module Make
let eval_test check env t e =
let accept_implicit =
match t with
| Yes Acyclic|No Acyclic -> true
| Yes (Acyclic|Irreflexive)|No (Acyclic|Irreflexive) -> true
| _ -> false in
check (test2pred env t e (eval_rel_set accept_implicit env e)) in

Expand Down Expand Up @@ -2337,44 +2396,52 @@ module Make
let st = check_bell_order bds st in
kont st res
| Rec (loc,bds,testo) ->
let env =
match
env_rec
(make_eval_test testo) (from_st st)
loc (fun pp -> pp@show_to_vbpp st) bds
with
| CheckOk env -> Some env
| CheckFailed env ->
if O.debug then begin
begin
match testo,ASTUtils.as_plus bds with
| None,Some (x,es) ->
let env = from_st st in
let v = lazy (eval_union_plus env es) in
let env = add_trans_val loc x v env.EV.env in
kont { st with env; } res
| _,_ ->
let env =
match
env_rec
(make_eval_test testo) (from_st st)
loc (fun pp -> pp@show_to_vbpp st) bds
with
| CheckOk env -> Some env
| CheckFailed env ->
if O.debug then begin
let st = { st with env; } in
let st = doshow bds st in
pp_check_failure st (Misc.as_some testo)
end ;
None in
begin match env with
| None -> kfail res
| Some env ->
let st = { st with env; } in
let st = doshow bds st in

(* Check again for strictskip *)
let st = match testo with
| None -> st
| Some (_,_,t,e,name) ->
if
O.strictskip &&
skip_this_check name &&
not (eval_test Misc.identity (from_st st) t e)
then begin
{ st with
skipped =
StringSet.add (Misc.as_some name) st.skipped;}
None in
begin match env with
| None -> kfail res
| Some env ->
let st = { st with env; } in
let st = doshow bds st in
(* Check again for strictskip *)
let st = match testo with
| None -> st
| Some (_,_,t,e,name) ->
if
O.strictskip &&
skip_this_check name &&
not (eval_test Misc.identity (from_st st) t e)
then begin
{ st with
skipped =
StringSet.add
(Misc.as_some name) st.skipped;}
end else st in
(* Check bell definitions *)
let st = check_bell_order bds st in
kont st res
(* Check bell definitions *)
let st = check_bell_order bds st in
kont st res
end
end

| InsMatch (loc,e,cls,d) ->
let v = eval_st st e in
begin match v with
Expand Down