Skip to content

Commit

Permalink
tabling: adapt stack/choice
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed May 24, 2024
1 parent 3bf4d04 commit 91dffde
Show file tree
Hide file tree
Showing 2 changed files with 92 additions and 69 deletions.
151 changes: 82 additions & 69 deletions src/runtime.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3014,29 +3014,37 @@ let repack_goal (gid[@trace]) ~depth program goal =
{ depth ; program ; goal ; gid = gid [@trace] }
[@@inline]


(* The activation frames points to the choice point that
cut should backtrack to, i.e. the first one not to be
removed. We call it catto_alts in the code. *)
type frame =
| FNil
| FCons of (*lvl:*)alternative * goal list * frame
and alternative = {
cutto_alts : alternative;
program : prolog_prog;
adepth : int;
agoal_hd : constant;
ogoal_arg : term;
ogoal_args : term list;
agid : UUID.t; [@trace]
goals : goal list;
stack : frame;
trail : T.trail;
state : State.t;
clauses : clause list;
next : alternative;
type goals_crumbles = {
predicate : constant;
fst_arg : term;
other_args : term list;
brothers : goal list;
}
let noalts : alternative = Obj.magic (Sys.opaque_identity 0)

(* The tree *)
type continuation = (* the AND part, what to do next *)
| Done
| ExitSLGRoot of { heap : unit; next : continuation; alts : alternative }
| TableSolution of unit
| SolveGoals of { cutto_alts : alternative; brothers : goal list; next : continuation }
and alternative = (* the OR part, what to do if we fail *)
| Noalts
| UnblockSLGGenerator of slg_generator (* a branch of the tree that could have been cut *)
| ExploreAnotherSLDPath of {
program : prolog_prog;
adepth : int;
path : goals_crumbles;
agid : UUID.t; [@trace]
stack : continuation;
trail : T.trail;
state : State.t;
clauses : clause list;
alts : alternative;
cutto_alts : alternative;
}
and slg_generator =
| Root of { root_goal : term; root_goal_args : int; clauses : clause list; }
| UnexploredBranches of { heap : unit; alts : alternative }

(******************************************************************************
Constraint propagation
Expand Down Expand Up @@ -3719,7 +3727,7 @@ let pp_CHR_resumed_goal { depth; program; goal; gid = gid[@trace] } =
let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x executable -> 'x runtime =
(* Input to be read as the orl (((p,g)::gs)::next)::alts
depth >= 0 is the number of variables in the context. *)
let rec run depth p g (gid[@trace]) gs (next : frame) alts cutto_alts =
let rec run depth p g (gid[@trace]) gs (next : continuation) alts cutto_alts =
[%cur_pred (pred_of g)];
[%trace "run" ~rid begin

Expand Down Expand Up @@ -3804,17 +3812,17 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
let clauses = get_clauses ~depth k g p in
[%spy "user:rule" ~rid ~gid pp_string "backchain"];
[%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses];
[%tcall backchain depth p (k, C.dummy, [], gs) (gid[@trace]) next alts cutto_alts clauses]
[%tcall backchain depth p { predicate = k; fst_arg = C.dummy; other_args = []; brothers = gs} (gid[@trace]) next alts cutto_alts clauses]
| App (k,x,xs) ->
let clauses = get_clauses ~depth k g p in
[%spy "user:rule" ~rid ~gid pp_string "backchain"];
[%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses];
[%tcall backchain depth p (k, x, xs, gs) (gid[@trace]) next alts cutto_alts clauses]
[%tcall backchain depth p { predicate = k; fst_arg = x; other_args = xs; brothers = gs} (gid[@trace]) next alts cutto_alts clauses]
| Builtin(c, args) -> [%spy "user:rule" ~rid ~gid pp_string "builtin"]; [%spy "user:rule:builtin:name" ~rid ~gid pp_string (C.show c)];
let once ~depth g state =
CS.state := state;
let { depth; program; goal; gid = gid [@trace] } = (make_subgoal[@inlined]) (gid[@trace]) ~depth p g in
let _alts = run depth program goal (gid[@trace]) [] FNil noalts noalts in
let _alts = run depth program goal (gid[@trace]) [] Done Noalts Noalts in
!CS.state in
begin match Constraints.exect_builtin_predicate ~once c ~depth p (gid[@trace]) args with
| gs' ->
Expand All @@ -3833,15 +3841,15 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
error "The goal is a flexible term"
end]

(* We pack some arguments into a tuple otherwise we consume too much stack *)
and backchain depth p (k, arg, args_of_g, gs) (gid[@trace]) next alts cutto_alts cp = [%trace "select" ~rid begin
(* We pack some arguments into the goals_crumbles record otherwise we consume too much stack *)
and backchain depth p ({ predicate = k; fst_arg = arg; other_args = args_of_g; brothers = gs} as g_gs) (gid[@trace]) next alts cutto_alts cp = [%trace "select" ~rid begin
match cp with
| [] -> [%spy "user:rule:backchain" ~rid ~gid pp_string "fail"];
[%tcall next_alt alts]
| { depth = c_depth; mode = c_mode; args = c_args; hyps = c_hyps; vars = c_vars; loc } :: cs ->
[%spy "user:rule:backchain:try" ~rid ~gid (pp_option Util.CData.pp) (Util.option_map Ast.cloc.Util.CData.cin loc) (ppclause ~hd:k) { depth = c_depth; mode = c_mode; args = c_args; hyps = c_hyps; vars = c_vars; loc }];
let old_trail = !T.trail in
T.last_call := alts == noalts && cs == [];
T.last_call := alts == Noalts && cs == [];
let env = Array.make c_vars C.dummy in
match
match c_args with
Expand All @@ -3851,23 +3859,22 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
| [] -> unif ~argsdepth:depth ~matching:false (gid[@trace]) depth env c_depth arg x && for_all23 ~argsdepth:depth (unif (gid[@trace])) depth env c_depth args_of_g xs
| arg_mode :: ms -> unif ~argsdepth:depth ~matching:(arg_mode == Input) (gid[@trace]) depth env c_depth arg x && for_all3b3 ~argsdepth:depth (unif (gid[@trace])) depth env c_depth args_of_g xs ms false
with
| false ->
T.undo ~old_trail (); [%tcall backchain depth p (k, arg, args_of_g, gs) (gid[@trace]) next alts cutto_alts cs]
| false -> T.undo old_trail (); [%tcall backchain depth p g_gs (gid[@trace]) next alts cutto_alts cs]
| true ->
let oldalts = alts in
let alts = if cs = [] then alts else
{ program = p; adepth = depth; agoal_hd = k; ogoal_arg = arg; ogoal_args = args_of_g; agid = gid[@trace]; goals = gs; stack = next;
ExploreAnotherSLDPath { program = p; adepth = depth; path = g_gs; agid = gid[@trace]; stack = next;
trail = old_trail;
state = !CS.state;
clauses = cs; cutto_alts = cutto_alts ; next = alts} in
clauses = cs; cutto_alts = cutto_alts ; alts} in
begin match c_hyps with
| [] ->
[%spy "user:rule:backchain" ~rid ~gid pp_string "success"];
begin match gs with
| [] -> [%tcall pop_andl alts next cutto_alts]
| { depth ; program; goal; gid = gid [@trace] } :: gs -> [%tcall run depth program goal (gid[@trace]) gs next alts cutto_alts] end
| h::hs ->
let next = if gs = [] then next else FCons (cutto_alts,gs,next) in
let next = if gs = [] then next else SolveGoals { cutto_alts; brothers = gs; next } in
let h = move ~argsdepth:depth ~from:c_depth ~to_:depth env h in
let gid[@trace] = make_subgoal_id gid ((depth,h)[@trace]) in
let hs =
Expand All @@ -3881,15 +3888,19 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
and cut (gid[@trace]) gs next (alts[@trace]) cutto_alts =
[%spy "user:rule" ~rid ~gid pp_string "cut"];
let ()[@trace] =
let rec prune ({ agid = agid[@trace]; clauses; adepth = depth; agoal_hd = hd } as alts) =
if alts != cutto_alts then begin
List.iter (fun c ->
[%spy "user:rule:cut:branch" ~rid UUID.pp agid (pp_option Util.CData.pp) (Util.option_map Ast.cloc.Util.CData.cin c.loc) (ppclause ~hd) c])
clauses;
prune alts.next
end in
let rec prune alts =
if alts == cutto_alts then () else
match alts with
| ExploreAnotherSLDPath ({ agid = agid[@trace]; clauses; adepth = depth; path = { predicate = hd } } as alts) ->
List.iter (fun c ->
[%spy "user:rule:cut:branch" ~rid UUID.pp agid (pp_option Util.CData.pp) (Util.option_map Ast.cloc.Util.CData.cin c.loc) (ppclause ~hd) c])
clauses;
prune alts.alts
| Noalts -> ()
| UnblockSLGGenerator _ -> ()
in
prune alts in
if cutto_alts == noalts then T.trail := T.empty ();
if cutto_alts == Noalts then T.trail := T.empty ();
match gs with
| [] -> pop_andl cutto_alts next cutto_alts
| { depth; program; goal; gid = gid [@trace] } :: gs -> run depth program goal (gid[@trace]) gs next cutto_alts cutto_alts
Expand Down Expand Up @@ -3921,7 +3932,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
let sol = copy g in
[%spy "findall solution:" ~rid ~gid (ppterm depth [] ~argsdepth:0 empty_env) g];
solutions := sol :: !solutions in
let alternatives = ref noalts in
let alternatives = ref Noalts in
try
alternatives := search ();
add_sol ();
Expand All @@ -3947,18 +3958,20 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut

and pop_andl alts next cutto_alts =
match next with
| FNil ->
| Done ->
(match resume_all () with
None ->
Fmt.fprintf Fmt.std_formatter
"Undo triggered by goal resumption\n%!";
[%tcall next_alt alts]
| Some ({ depth; program; goal; gid = gid [@trace] } :: gs) ->
run depth program goal (gid[@trace]) gs FNil alts cutto_alts
run depth program goal (gid[@trace]) gs Done alts cutto_alts
| Some [] -> alts)
| FCons (_,[],_) -> anomaly "empty stack frame"
| FCons(cutto_alts, { depth; program; goal; gid = gid [@trace] } :: gs, next) ->
| SolveGoals { brothers = []; _ } -> anomaly "empty continuation"
| SolveGoals { cutto_alts; brothers = { depth; program; goal; gid = gid [@trace] } :: gs; next } ->
run depth program goal (gid[@trace]) gs next alts cutto_alts
| ExitSLGRoot _ -> assert false
| TableSolution _ -> assert false

and resume_all () : goal list option =
(* if fm then Some [] else *)
Expand Down Expand Up @@ -4028,20 +4041,20 @@ end;*)
end

and next_alt alts =
if alts == noalts then raise No_clause
else
let { program = p; clauses; agoal_hd = k; ogoal_arg = arg; ogoal_args = args; agid = gid [@trace]; goals = gs; stack = next;
trail = old_trail; state = old_state;
adepth = depth; cutto_alts = cutto_alts; next = alts} = alts in
T.undo ~old_trail ~old_state ();

[%trace "run" ~rid begin
[%cur_pred (Some (C.show k))];
[%spyl "user:curgoal" ~rid ~gid (uppterm depth [] ~argsdepth:0 empty_env) [Const k;App(k,arg,args)]];
[%spy "user:rule" ~rid ~gid pp_string "backchain"];
[%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses];
[%tcall backchain depth p (k, arg, args, gs) (gid[@trace]) next alts cutto_alts clauses]
end]
match alts with
| ExploreAnotherSLDPath { program = p; clauses; path; agid = gid [@trace]; stack = next;
trail = old_trail; state = old_state;
adepth = depth; cutto_alts = cutto_alts; alts} ->
T.undo ~old_trail ~old_state ();
[%trace "run" ~rid begin
[%cur_pred (Some (C.show path.predicate))];
[%spyl "user:curgoal" ~rid ~gid (uppterm depth [] ~argsdepth:0 empty_env) [Const path.predicate;App(path.predicate,path.fst_arg,path.other_args)]];
[%spy "user:rule" ~rid ~gid pp_string "backchain"];
[%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k:(path.predicate)) clauses];
[%tcall backchain depth p path (gid[@trace]) next alts cutto_alts clauses]
end]
| UnblockSLGGenerator _ -> assert false
| Noalts -> raise No_clause
in

(* Finally the runtime *)
Expand Down Expand Up @@ -4077,7 +4090,7 @@ end;*)
let gid[@trace] = UUID.make () in
[%spy "user:newgoal" ~rid ~gid (uppterm initial_depth [] ~argsdepth:0 empty_env) initial_goal];
set T.trail (T.empty ());
run initial_depth !orig_prolog_program initial_goal (gid[@trace]) [] FNil noalts noalts) in
run initial_depth !orig_prolog_program initial_goal (gid[@trace]) [] Done Noalts Noalts) in
let destroy () = () in
let next_solution = exec next_alt in
incr max_runtime_id;
Expand Down Expand Up @@ -4107,8 +4120,8 @@ let mk_outcome search get_cs assignments depth =
} in
Success solution, alts
with
| No_clause (*| Non_linear*) -> Failure, noalts
| No_more_steps -> NoMoreSteps, noalts
| No_clause (*| Non_linear*) -> Failure, Noalts
| No_more_steps -> NoMoreSteps, Noalts

let execute_once ?max_steps ?delay_outside_fragment exec =
let { search; get } = make_runtime ?max_steps ?delay_outside_fragment exec in
Expand All @@ -4124,20 +4137,20 @@ let execute_once ?max_steps ?delay_outside_fragment exec =

let execute_loop ?delay_outside_fragment exec ~more ~pp =
let { search; next_solution; get; destroy } = make_runtime ?delay_outside_fragment exec in
let k = ref noalts in
let k = ref Noalts in
let do_with_infos f =
let time0 = Unix.gettimeofday() in
let o, alts = mk_outcome f (fun () -> get CS.Ugly.delayed, (exec.initial_depth,get CS.state), get CS.state |> State.end_execution, exec.query_arguments, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments exec.initial_depth in
let time1 = Unix.gettimeofday() in
k := alts;
pp (time1 -. time0) o in
do_with_infos search;
while !k != noalts do
if not(more()) then k := noalts else
while !k != Noalts do
if not(more()) then k := Noalts else
try do_with_infos (fun () -> next_solution !k)
with
| No_clause -> pp 0.0 Failure; k := noalts; [%end_trace "execute_loop" ~rid]
| e -> pp 0.0 Failure; k := noalts; [%end_trace "execute_loop" ~rid]; raise e
| No_clause -> pp 0.0 Failure; k := Noalts; [%end_trace "execute_loop" ~rid]
| e -> pp 0.0 Failure; k := Noalts; [%end_trace "execute_loop" ~rid]; raise e
done
;;

Expand Down
10 changes: 10 additions & 0 deletions trace/ppx/trace_ppx.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,16 @@ let map_trace = object(self)
let lbls = lbls |> List.filter (fun { pld_attributes = l; _ } ->
not (has_iftrace_attribute l)) in
{ tyd with ptype_kind = Ptype_record lbls }
| Ptype_variant l ->
let aux ({ pcd_args; _ } as pcd) =
match pcd_args with
| Pcstr_record lbls when not !enabled ->
let lbls = lbls |> List.filter (fun { pld_attributes = l; _ } ->
not (has_iftrace_attribute l)) in
{pcd with pcd_args = Pcstr_record lbls }
| _ -> pcd in
let l = List.map aux l in
{ tyd with ptype_kind = Ptype_variant l }
| _ -> tyd

method! expression e =
Expand Down

0 comments on commit 91dffde

Please sign in to comment.