diff --git a/lib/ASTUtils.ml b/lib/ASTUtils.ml index d56962ee8b..33b2a3bc17 100644 --- a/lib/ASTUtils.ml +++ b/lib/ASTUtils.ml @@ -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 + 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 diff --git a/lib/ASTUtils.mli b/lib/ASTUtils.mli index 997a234e41..ba37cdca66 100644 --- a/lib/ASTUtils.mli +++ b/lib/ASTUtils.mli @@ -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 diff --git a/lib/interpreter.ml b/lib/interpreter.ml index ddf2a46afe..797e967566 100644 --- a/lib/interpreter.ml +++ b/lib/interpreter.ml @@ -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 ; @@ -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 = @@ -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 -> @@ -509,6 +525,7 @@ module Make let env_empty = {vals=StringMap.empty; + trans=StringMap.empty; enums=StringMap.empty; tags=StringMap.empty; } @@ -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 @@ -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 @@ -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 *) @@ -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 @@ -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 @@ -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 @@ -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 *) @@ -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 @@ -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 @@ -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