From 91dffde509f6c09ff2697be7664fea8f12922c6e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 2 Nov 2021 13:26:19 +0100 Subject: [PATCH] tabling: adapt stack/choice --- src/runtime.ml | 151 ++++++++++++++++++++++------------------- trace/ppx/trace_ppx.ml | 10 +++ 2 files changed, 92 insertions(+), 69 deletions(-) diff --git a/src/runtime.ml b/src/runtime.ml index b382a9eff..061f04648 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -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 @@ -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 @@ -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' -> @@ -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 @@ -3851,15 +3859,14 @@ 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"]; @@ -3867,7 +3874,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut | [] -> [%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 = @@ -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 @@ -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 (); @@ -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 *) @@ -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 *) @@ -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; @@ -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 @@ -4124,7 +4137,7 @@ 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 @@ -4132,12 +4145,12 @@ let execute_loop ?delay_outside_fragment exec ~more ~pp = 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 ;; diff --git a/trace/ppx/trace_ppx.ml b/trace/ppx/trace_ppx.ml index 5727b37ae..844b5423b 100644 --- a/trace/ppx/trace_ppx.ml +++ b/trace/ppx/trace_ppx.ml @@ -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 =