tabling: adapt stack/choice

gares · gares · commit ee2d7862856f · 2024-05-24T10:29:22.000+02:00
diff --git 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,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 =
@@ -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,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
 ;;
 
diff --git 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 =
