Add information about clauses to implication cards

CHANGES.md

@@ -1,3 +1,8 @@
+# UNRELEASED
+
+- Trace:
+  - Add information about added clauses to Implication cards
+
 # v3.7.2 (July 2026)
 
 Requires Menhir 20211230 and OCaml 4.14 or above on Linux, Windows and

src/elpi_trace_elaborator.ml

@@ -71,7 +71,7 @@ module Elaborate : sig
     type chr_attempt = { loc : location; code: string; events : event list; timestamp : timestamp; removed : goal_id list; resumed : goal_id list;  }
 
     type action =
-      | Builtin of { name : builtin_name; outcome : step_outcode; events : event list }
+      | Builtin of { name : builtin_rule; outcome : step_outcode; events : event list }
       | Backchain of { trylist : attempt list; outcome : step_outcode }
 
     type step =
@@ -117,7 +117,7 @@ end = struct
     type chr_attempt = { loc : location; code: string; events : event list; timestamp : timestamp; removed : goal_id list; resumed : goal_id list;  }
 
     type action =
-      | Builtin of { name : builtin_name; outcome : step_outcode; events : event list }
+      | Builtin of { name : builtin_rule; outcome : step_outcode; events : event list }
       | Backchain of { trylist : attempt list; outcome : step_outcode }
 
     type step =
@@ -288,18 +288,29 @@ let decode_cut = function
   | { payload = [g;r;t] }, _ -> int_of_string g, decode_loc r, t
   | _ -> assert false
 
-let get_builtin_name l : builtin_name =
+let get_builtin_name l : builtin_rule =
   match has "user:rule:builtin:name" l with
   | None -> assert false
-  | Some x -> `FFI (decode_string x)
+  | Some x -> { kind = `FFI; name = decode_string x; payload = [] }
 
 let gstacks : frame list GoalMap.t ref = ref GoalMap.empty (* goal_id -> stack *)
 let fstacks : frame list StepMap.t ref = ref StepMap.empty (* step_id -> stack *)
 
 let push_stack (step,rid) goal_id rule siblings =
-  let this_stack = try GoalMap.find goal_id !gstacks with Not_found -> [] in
+  (* If a step pushes multiple frames, such as an implication with
+     multiple clauses on the LHS, then a stack for this step already
+     exists; we need to make sure to properly push to it, instead of
+     overriding *)
+  let this_stack =
+    try StepMap.find (step,rid) !fstacks
+    with Not_found ->
+      try GoalMap.find goal_id !gstacks
+      with Not_found -> [] in
   let stack = { rule; step_id = step; runtime_id = rid } :: this_stack in
   fstacks := StepMap.add (step,rid) stack !fstacks;
+  (* We assume that a step pushes all its frames before we start
+     processing siblings, so we can safely override the siblings'
+     stacks *)
   List.iter (fun g -> gstacks := GoalMap.add g stack !gstacks) siblings
 
 let update_stack (step,rid) goal_id rule =
@@ -325,7 +336,7 @@ try
   timestamp,match decode_step items with
   | `Findall (({ goal_id; payload = [pred;goal] },_),start) ->
       let result = all "user:assign" decode_string items in
-      let () = push_stack (step,rid) goal_id (`BuiltinRule (`FFI "findall")) [] in
+      let () = push_stack (step,rid) goal_id (`BuiltinRule ({ kind = `FFI; name = "findall"; payload = [] })) [] in
       let stop =
         match has "user:assign" items with
         | None -> assert false
@@ -334,15 +345,15 @@ try
   | `Suspend ({ goal_id; payload = [pred;goal] },_) ->
        let sibling = all "user:subgoal" decode_int items in
        assert(List.length sibling = 1);
-       let () = push_stack (step,rid) goal_id (`BuiltinRule (`Logic "suspend")) sibling in
+       let () = push_stack (step,rid) goal_id (`BuiltinRule ({ kind = `Logic; name = "suspend"; payload = [] })) sibling in
        Suspend {goal_id;goal;sibling = List.hd sibling} 
   | `Cut ({ goal_id; payload = [pred;goal] },_) ->
-      let () = push_stack (step,rid) goal_id (`BuiltinRule (`FFI "!")) [] in
+      let () = push_stack (step,rid) goal_id (`BuiltinRule ({ kind = `FFI; name = "!"; payload = []})) [] in
       let cutted = all "user:rule:cut:branch" decode_cut items in
       Cut (goal_id,cutted)
   | `Resumption l ->
       let resumed = List.map (fun ({ goal_id; payload },_ as x) ->
-        let () = update_stack (step,rid) goal_id (`BuiltinRule (`Logic "resume")) in
+        let () = update_stack (step,rid) goal_id (`BuiltinRule ({ kind = `Logic; name = "resume"; payload = [] })) in
         goal_id, decode_string x) l in
       Resume resumed
   | `CHR(chr_store_before,chr_store_after) ->
@@ -382,8 +393,22 @@ try
           assert(List.length events = 1);
           let _, events = List.hd events in
           Builtin { name; outcome; events = List.map decode_infer_event events  }
+        else if name = "implication" then
+          let new_hyps = match has "user:new-hyps" items with
+            | Some ({ payload = hyps },_) -> hyps
+            (* Backwards compatibility: treat a missing new-hyps item
+               as empty, which renders as before *)
+            | _ -> [] in
+          let () =
+            push_stack (step,rid) goal_id (`BuiltinRule ({ kind = `Logic; name = name; payload = new_hyps })) siblings
+          in
+          let name = { kind = `Logic; name = name; payload = [] } in
+          (* Every step needs to push a stack, even a degenerate ([] => P) *)
+          if new_hyps = [] then
+            push_stack (step,rid) goal_id (`BuiltinRule name) siblings;
+          Builtin { name; outcome; events = [] }
         else
-          let name = `Logic name in
+          let name = { kind = `Logic; name = name; payload = [] } in
           let () = push_stack (step,rid) goal_id (`BuiltinRule name) siblings in
           let events = all_infer_event_chains "user:rule:builtin:name" items in (* ??? *)
           let events =

src/runtime/runtime.ml

@@ -4109,6 +4109,8 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> executabl
        let clauses, pdiff, lcs = clausify ~tail_cut:(ik = ImplBang) ~loc p ~depth g1 in
        let g2 = hmove ~from:depth ~to_:(depth+lcs) g2 in
        let gid[@trace] = make_subgoal_id gid ((depth,g2)[@trace]) in
+       (* clausify returns the clauses right-to-left, but we want to report them left-to-right *)
+       [%spyl "user:new-hyps" ~rid ~gid (fun f (hd,c) -> ppclause f ~hd c) (List.rev clauses)];
        [%spy "user:rule:implication" ~rid ~gid pp_string "success"];
        [%tcall run (depth+lcs) (add_clauses ~depth clauses pdiff p) g2 (gid[@trace]) gs next alts cutto_alts]
     | Builtin(Pi, [arg]) -> [%spy "user:rule" ~rid ~gid pp_string "pi"];

src/trace.atd

@@ -64,9 +64,10 @@ type attempt = {
   rule : rule;
   events : event list;
 }
-type rule = [ BuiltinRule of builtin_name | UserRule of user_rule ]
+type rule = [ BuiltinRule of builtin_rule | UserRule of user_rule ]
 type user_rule = { rule_text : rule_text; rule_loc : location }
-type builtin_name = [ Logic of string | FFI of string ]
+type builtin_kind = [ Logic | FFI ]
+type builtin_rule = { name : string; kind : builtin_kind; payload : string list }
 type location = [ File of file_location | Context of step_id ]
 type file_location = { filename : string; line : int; column : int; character : int }
 type event = [ Assign of string | Fail of string | ResumeGoal of goal_id list]

src/trace_atd.ts

@@ -77,17 +77,23 @@ export type Attempt = {
 }
 
 export type Rule =
-| { kind: 'BuiltinRule'; value: BuiltinName }
+| { kind: 'BuiltinRule'; value: BuiltinRule }
 | { kind: 'UserRule'; value: UserRule }
 
 export type UserRule = {
   rule_text: RuleText;
   rule_loc: Location;
 }
 
-export type BuiltinName =
-| { kind: 'Logic'; value: string }
-| { kind: 'FFI'; value: string }
+export type BuiltinKind =
+| { kind: 'Logic' }
+| { kind: 'FFI' }
+
+export type BuiltinRule = {
+  name: string;
+  kind: BuiltinKind;
+  payload: string[];
+}
 
 export type Location =
 | { kind: 'File'; value: FileLocation }
@@ -411,7 +417,7 @@ export function readAttempt(x: any, context: any = x): Attempt {
 export function writeRule(x: Rule, context: any = x): any {
   switch (x.kind) {
     case 'BuiltinRule':
-      return ['BuiltinRule', writeBuiltinName(x.value, x)]
+      return ['BuiltinRule', writeBuiltinRule(x.value, x)]
     case 'UserRule':
       return ['UserRule', writeUserRule(x.value, x)]
   }
@@ -421,7 +427,7 @@ export function readRule(x: any, context: any = x): Rule {
   _atd_check_json_tuple(2, x, context)
   switch (x[0]) {
     case 'BuiltinRule':
-      return { kind: 'BuiltinRule', value: readBuiltinName(x[1], x) }
+      return { kind: 'BuiltinRule', value: readBuiltinRule(x[1], x) }
     case 'UserRule':
       return { kind: 'UserRule', value: readUserRule(x[1], x) }
     default:
@@ -444,28 +450,43 @@ export function readUserRule(x: any, context: any = x): UserRule {
   };
 }
 
-export function writeBuiltinName(x: BuiltinName, context: any = x): any {
+export function writeBuiltinKind(x: BuiltinKind, context: any = x): any {
   switch (x.kind) {
     case 'Logic':
-      return ['Logic', _atd_write_string(x.value, x)]
+      return 'Logic'
     case 'FFI':
-      return ['FFI', _atd_write_string(x.value, x)]
+      return 'FFI'
   }
 }
 
-export function readBuiltinName(x: any, context: any = x): BuiltinName {
-  _atd_check_json_tuple(2, x, context)
-  switch (x[0]) {
+export function readBuiltinKind(x: any, context: any = x): BuiltinKind {
+  switch (x) {
     case 'Logic':
-      return { kind: 'Logic', value: _atd_read_string(x[1], x) }
+      return { kind: 'Logic' }
     case 'FFI':
-      return { kind: 'FFI', value: _atd_read_string(x[1], x) }
+      return { kind: 'FFI' }
     default:
-      _atd_bad_json('BuiltinName', x, context)
+      _atd_bad_json('BuiltinKind', x, context)
       throw new Error('impossible')
   }
 }
 
+export function writeBuiltinRule(x: BuiltinRule, context: any = x): any {
+  return {
+    'name': _atd_write_required_field('BuiltinRule', 'name', _atd_write_string, x.name, x),
+    'kind': _atd_write_required_field('BuiltinRule', 'kind', writeBuiltinKind, x.kind, x),
+    'payload': _atd_write_required_field('BuiltinRule', 'payload', _atd_write_array(_atd_write_string), x.payload, x),
+  };
+}
+
+export function readBuiltinRule(x: any, context: any = x): BuiltinRule {
+  return {
+    name: _atd_read_required_field('BuiltinRule', 'name', _atd_read_string, x['name'], x),
+    kind: _atd_read_required_field('BuiltinRule', 'kind', readBuiltinKind, x['kind'], x),
+    payload: _atd_read_required_field('BuiltinRule', 'payload', _atd_read_array(_atd_read_string), x['payload'], x),
+  };
+}
+
 export function writeLocation(x: Location, context: any = x): any {
   switch (x.kind) {
     case 'File':