From 3bf4d0476524d998c810c8c07f5e7fbb0709fc37 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 2 Nov 2021 16:29:02 +0100 Subject: [PATCH 1/3] tabling: adapt trail --- src/runtime.ml | 98 +++++++++++++++++++++++++++++++------------------- 1 file changed, 62 insertions(+), 36 deletions(-) diff --git a/src/runtime.ml b/src/runtime.ml index 8e165063b..b382a9eff 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -384,11 +384,9 @@ module ConstraintStoreAndTrail : sig type trail - val empty : trail + val empty : unit -> trail - val initial_trail : trail Fork.local_ref val trail : trail Fork.local_ref - val cut_trail : unit -> unit [@@inline] (* If true, no need to trail an imperative action. Not part of trial_this * because you can save allocations and a function call by testing locally *) @@ -430,20 +428,19 @@ end = struct (* {{{ *) type trail_item = -| Assignement of uvar_body -| StuckGoalAddition of stuck_goal -| StuckGoalRemoval of stuck_goal + | Assignement of uvar_body * trail + | Restore of uvar_body * term * trail + | StuckGoalAddition of stuck_goal * trail + | StuckGoalRemoval of stuck_goal * trail + | Top +and trail = trail_item ref [@@deriving show] -type trail = trail_item list -[@@deriving show] -let empty = [] +let empty () = ref Top -let trail = Fork.new_local [] -let initial_trail = Fork.new_local [] +let trail = Fork.new_local (empty ()) let last_call = Fork.new_local false;; -let cut_trail () = trail := !initial_trail [@@inline];; let blockers_map = Fork.new_local (IntMap.empty : stuck_goal list IntMap.t) let blocked_by r = IntMap.find (uvar_id r) !blockers_map @@ -460,18 +457,31 @@ let contents ?overlapping () = | _ -> None) !delayed let trail_assignment x = - [%spy "dev:trail:assign" ~rid Fmt.pp_print_bool !last_call pp_trail_item (Assignement x)]; - if not !last_call then trail := Assignement x :: !trail + assert(! (!trail) = Top); + if not !last_call then begin + let new_top = ref Top in + [%spy "dev:trail:assign" ~rid Fmt.pp_print_bool !last_call pp_trail_item (Assignement(x,new_top))]; + !trail := Assignement(x ,new_top); + trail := new_top; + end; [@@inline] ;; let trail_stuck_goal_addition x = - [%spy "dev:trail:add-constraint" ~rid Fmt.pp_print_bool !last_call pp_trail_item (StuckGoalAddition x)]; - if not !last_call then trail := StuckGoalAddition x :: !trail + if not !last_call then begin + let new_top = ref Top in + [%spy "dev:trail:add-constraint" ~rid Fmt.pp_print_bool !last_call pp_trail_item (StuckGoalAddition(x,new_top))]; + !trail := StuckGoalAddition(x,new_top); + trail := new_top; + end; [@@inline] ;; let trail_stuck_goal_removal x = - [%spy "dev:trail:remove-constraint" ~rid Fmt.pp_print_bool !last_call pp_trail_item (StuckGoalRemoval x)]; - if not !last_call then trail := StuckGoalRemoval x :: !trail + if not !last_call then begin + let new_top = ref Top in + [%spy "dev:trail:remove-constraint" ~rid Fmt.pp_print_bool !last_call pp_trail_item (StuckGoalRemoval(x,new_top))]; + !trail := StuckGoalRemoval(x,new_top); + trail := new_top; + end; [@@inline] ;; @@ -560,15 +570,34 @@ let undo ~old_trail ?old_state () = rules. *) to_resume := []; new_delayed := []; [%spy "dev:trail:undo" ~rid pp_trail !trail pp_string "->" pp_trail old_trail]; - while !trail != old_trail do - match !trail with - | Assignement r :: rest -> - r.contents <- C.dummy; - trail := rest - | StuckGoalAddition sg :: rest -> remove sg; trail := rest - | StuckGoalRemoval sg :: rest -> add sg; trail := rest - | [] -> anomaly "undo to unknown trail" - done; + let rec aux h k = + match !h with + | Top -> k () + | Assignement(r,h') -> + aux h' (fun () -> + h' := Restore(r,r.contents, h); + r.contents <- C.dummy; + k ()) + | Restore(r,v,h') -> + aux h' (fun () -> + h' := Assignement(r,h); + r.contents <- v; + k ()) + | StuckGoalAddition(sg,h') -> + aux h' (fun () -> + h := StuckGoalRemoval(sg,h); + remove sg; + k ()) + | StuckGoalRemoval(sg,h') -> + aux h' (fun () -> + h := StuckGoalAddition(sg,h); + add sg; + k ()) + in + aux old_trail (fun () -> + trail := old_trail; + old_trail := Top); + assert(!(!trail) = Top); match old_state with | Some old_state -> state := old_state | None -> () @@ -3858,11 +3887,9 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut [%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 - prune alts in - if cutto_alts == noalts then (T.cut_trail[@inlined]) (); - [%spy "user:rule:cut" ~rid ~gid pp_string "success"]; + end in + prune alts in + 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 @@ -4031,8 +4058,7 @@ end;*) let { Fork.exec = exec ; get = get ; set = set } = Fork.fork () in set orig_prolog_program compiled_program; set Constraints.chrules chr; - set T.initial_trail T.empty; - set T.trail T.empty; + set T.trail (T.empty ()); set T.last_call false; set CS.new_delayed []; set CS.to_resume []; @@ -4050,9 +4076,9 @@ end;*) [%spy "dev:trail:init" ~rid (fun fmt () -> T.print_trail fmt) ()]; let gid[@trace] = UUID.make () in [%spy "user:newgoal" ~rid ~gid (uppterm initial_depth [] ~argsdepth:0 empty_env) initial_goal]; - T.initial_trail := !T.trail; + set T.trail (T.empty ()); run initial_depth !orig_prolog_program initial_goal (gid[@trace]) [] FNil noalts noalts) in - let destroy () = exec (fun () -> T.undo ~old_trail:T.empty ()) () in + let destroy () = () in let next_solution = exec next_alt in incr max_runtime_id; { search; next_solution; destroy; exec; get } From 91dffde509f6c09ff2697be7664fea8f12922c6e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 2 Nov 2021 13:26:19 +0100 Subject: [PATCH 2/3] 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 = From 46645733ef475bc237742f1f484cc4e58023edf7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 24 May 2024 10:40:05 +0200 Subject: [PATCH 3/3] fix trace --- src/runtime.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/runtime.ml b/src/runtime.ml index 061f04648..506963d7e 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -3901,6 +3901,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut in prune alts in if cutto_alts == Noalts then T.trail := T.empty (); + [%spy "user:rule:cut" ~rid ~gid pp_string "success"]; 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