diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 8752da04a..eaa2826bc 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -20,7 +20,7 @@ jobs: - 4.13.1 - 4.11.2 - 4.09.1 - - 4.07.1 + - 4.08.1 profile: - dev parser: diff --git a/Makefile b/Makefile index 1792da07e..fdb249d6c 100644 --- a/Makefile +++ b/Makefile @@ -28,6 +28,7 @@ PWD=$(shell pwd) RUNNERS=\ dune \ $(PWD)/$(INSTALL)/bin/elpi \ + $(PWD)/$(INSTALL)/bin/elpi-trace-elaborator \ $(addprefix $(PWD)/,$(wildcard _build/git/*/$(INSTALL)/bin/elpi.git.*)) \ $(shell if type tjsim >/dev/null 2>&1; then type -P tjsim; else echo; fi) TIME=--time $(shell if type -P gtime >/dev/null 2>&1; then type -P gtime; else echo /usr/bin/time; fi) diff --git a/dune b/dune index c5091d875..bfdb21e97 100644 --- a/dune +++ b/dune @@ -6,6 +6,27 @@ (package elpi) ) +(executable + (name elpi_trace_elaborator) + (public_name elpi-trace-elaborator) + (libraries yojson atdgen re) + (modules elpi_trace_elaborator trace_atd) + (package elpi) +) + +(rule + (targets trace_atd.ml trace_atd.mli) + (action (run atdgen -o trace_atd -j-std %{dep:trace.atd}))) + +(rule + (targets trace_atd.ts) + (mode promote) + (action (copy %{dep:trace.ts} trace_atd.ts))) + +(rule + (targets trace.ts) + (action (run atdts %{dep:trace.atd}))) + (env (dev (flags (:standard -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A))) diff --git a/elpi.opam b/elpi.opam index 1e3320535..32faf30dd 100644 --- a/elpi.opam +++ b/elpi.opam @@ -25,6 +25,8 @@ depends: [ "cmdliner" {with-test} "dune" {>= "2.8.0"} "conf-time" {with-test} + "atdgen" {>= "2.5.0"} + "atdts" {>= "2.5.0"} ] depopts: [ "elpi-option-legacy-parser" diff --git a/elpi_trace_elaborator.ml b/elpi_trace_elaborator.ml new file mode 100644 index 000000000..c98621220 --- /dev/null +++ b/elpi_trace_elaborator.ml @@ -0,0 +1,637 @@ +(* elpi: embedded lambda prolog interpreter *) +(* license: GNU Lesser General Public License Version 2.1 or later *) +(* ------------------------------------------------------------------------- *) + +(* This file elaborates a traec as spit by the runtime into a list of + cards to be displayed by the trace browser. + + Trace items are first aggregated into steps. + Then some data is aggregated into steps (like the success of an inference + based on the success of all siblings, or the text of subgoals when only + the ID is part of the trace). A stack of rules is also recomputed from the + father/son link of goals and attached to each card. + + Time stamps are used to preserve the linear time line, that in turn is + used to nest card traces (e.g. the trace of a CHR guard, or the trace + of a findall). + +*) + +open Trace_atd +module Str = Re.Str + +module Int = struct type t = int let compare x y = x - y end +module Int2 = struct type t = int * int let compare (s1,r1) (s2,r2) = let x = r1 - r2 in if x = 0 then s1 - s2 else x end +module StepMap : Map.S with type key = step_id * runtime_id = Map.Make(Int2) +module GoalMap : Map.S with type key = goal_id = Map.Make(Int) + +type time = int +type timestamp = { start : time; stop : time } + +(* Reads the raw trace and associates to each item a timestamp *) +module Raw : sig + + val read_stdin : unit -> (timestamp * (item * time) list) StepMap.t + +end = struct + +(* raw steps *) +let steps : (timestamp * (item * time) list) StepMap.t ref = ref StepMap.empty + +let tt = ref 0 +let load_item i = + incr tt; + if i.kind = [`Info] then + let { start },items = try StepMap.find (i.step,i.runtime_id) !steps with Not_found -> { start = !tt; stop = !tt },[] in + steps := StepMap.add (i.step,i.runtime_id) ({ start; stop = !tt }, (i,!tt) :: items) !steps +;; + +let read_stdin () = + let lexer_state = Yojson.Safe.init_lexer () in + let lexbuf = Lexing.from_channel stdin in + begin try while true do + let i = read_item lexer_state lexbuf in + load_item i + done + with Yojson.Json_error _ -> () end; + !steps + +end + +(* Elaborated steps, similar to cards but not complete *) +module Elaborate : sig + + module Elaborated_step : sig + + type step_outcode = + | Success of { siblings : goal_id list} + | Fail + + type attempt = { loc : location; code : string; events : event list } + 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 } + | Backchain of { trylist : attempt list; outcome : step_outcode } + + type step = + | Inference of { pred : string; goal : string; goal_id : goal_id; action : action; rid : int } + | Findall of { goal : string; goal_id : goal_id; timestamp : timestamp; result : string list } + | Cut of (goal_id * location) list + | Suspend of { goal : string; goal_id : goal_id; sibling : goal_id } + | Resume of goal_id list + | CHR of { failed_attempts : chr_attempt list; successful_attempts : chr_attempt list; chr_store_before : (goal_id * goal_text) list; chr_store_after : (goal_id * goal_text) list;} + | Init of goal_id + + type t = timestamp * step + + end + + type elaboration = { + steps : Elaborated_step.t StepMap.t; + stack_frames : frame list StepMap.t; + goal_text : string GoalMap.t + } + + val elaborate : (timestamp * (item * time) list) StepMap.t -> elaboration + + type analysis = { + aggregated_goal_success : bool GoalMap.t; + goal_attempts : (step_id * runtime_id) list GoalMap.t + } + + val success_analysis : Elaborated_step.t StepMap.t -> analysis + +end = struct + module Elaborated_step = struct + + type step_outcode = + | Success of { siblings : goal_id list} + | Fail + + type attempt = { loc : location; code : string; events : event list } + 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 } + | Backchain of { trylist : attempt list; outcome : step_outcode } + + type step = + | Inference of { pred : string; goal : string; goal_id : goal_id; action : action; rid : int } + | Findall of { goal : string; goal_id : goal_id; timestamp : timestamp; result : string list } + | Cut of (goal_id * location) list + | Suspend of { goal : string; goal_id : goal_id; sibling : goal_id } + | Resume of goal_id list + | CHR of { failed_attempts : chr_attempt list; successful_attempts : chr_attempt list; chr_store_before : (goal_id * goal_text) list; chr_store_after : (goal_id * goal_text) list;} + | Init of goal_id + + type t = timestamp * step + end + open Elaborated_step + + type elaboration = { + steps : Elaborated_step.t StepMap.t; + stack_frames : frame list StepMap.t; + goal_text : string GoalMap.t + } + + type analysis = { + aggregated_goal_success : bool GoalMap.t; + goal_attempts : (step_id * runtime_id) list GoalMap.t + } + +let elaborated_steps : Elaborated_step.t StepMap.t ref = ref StepMap.empty + +(* elaboration *) +let rec filter_map f = function + | [] -> [] + | x :: xs -> + match f x with + | None -> filter_map f xs + | Some y -> y :: filter_map f xs + +let has f l = List.find_opt (fun (i,_) -> i.name = f) l +let all f p l = filter_map (fun (i,_ as it) -> if i.name = f then Some (p it) else None) l +let rec split_on p current = function + | [] -> (match current with None -> [] | Some x -> [List.rev x]) + | i :: is when p i -> + (match current with None -> split_on p (Some [i]) is | Some x -> List.rev x :: split_on p (Some [i]) is) + | i :: is -> + split_on p (match current with None -> None | Some x -> Some (i::x)) is +let split_on p l = split_on p None l + +let starts_with sl ({ name },_) = + List.exists (fun s -> Str.(string_match (regexp ("^"^s^".*")) name 0)) sl + +let decode_int = function + | { payload = [ s ] },_ -> int_of_string s + | _ -> assert false + +let decode_string = function + | { payload }, _ -> String.concat "" payload +let decode_chr_store_entry = function + | { payload = [ gid; gtext ]}, _ -> int_of_string gid, gtext + | _ -> assert false + +let get s l = + try (fst @@ List.find (fun ({ name },_) -> name = s) l).payload + with Not_found -> assert false + +type decoded_step = + [ `Focus of item * time + | `CHR of (goal_id * goal_text) list * (goal_id * goal_text) list + | `Resumption of (item * time) list + | `Init of goal_id + | `Suspend of item * time + | `Findall of (item * time) * time + | `Cut of item * time + ] + +let decode_step l : decoded_step = + let curgoal, rule = has "user:curgoal" l, has "user:rule" l in + let builtin = has "user:rule:builtin:name" l in + let chr = has "user:CHR:try" l in + let newg = has "user:newgoal" l in + match curgoal, Option.map decode_string rule, Option.map decode_string builtin, chr, newg with + | Some g, _, Some "declare_constraint", None, _ -> `Suspend g + | Some g, Some "findall", _, None, _ -> `Findall (g,snd @@ Option.get rule) + | Some g, Some "cut", _, None, _ -> `Cut g + | None, Some "resume", _, None, _ -> `Resumption (List.filter (fun ({ name },_) -> name = "user:rule:resume:resumed") l) + | None, _, _, Some c, _ -> `CHR (all "user:CHR:store:before" decode_chr_store_entry l, all "user:CHR:store:after" decode_chr_store_entry l) + | None, _, _, None, Some (x,_) -> `Init (x.goal_id) + | Some g, _, _, None, _ -> `Focus g + | _ -> assert false + +let decode_attempt = function + | { payload = [ loc; code ] },_ -> loc, code + | _ -> assert false + +let all_chains f fs l = + let chains = split_on (fun (i,_) -> i.name = f) l in + List.map (fun l -> + List.hd l, + List.filter (starts_with fs) (List.tl l)) chains + +let all_infer_event_chains f = + all_chains f ["user:assign";"user:backchain:fail-to"] + +let all_chr_event_chains f = + all_chains f ["user:assign";"user:CHR:rule-failed";"user:CHR:rule-fired";"user:CHR:rule-remove-constraints";"user:subgoal";"user:rule:resume:resumed"] + +let int_of_string s = + try int_of_string s + with Failure _ -> raise (Failure (Printf.sprintf "int_of_string %S" s)) + +let decode_loc s = + if Str.(string_match (regexp "File .(context step_id:\\([0-9]+\\))") s 0) then + `Context (int_of_string (Str.matched_group 1 s)) + else if Str.(string_match (regexp "File .\\([^,]+\\)., line \\([0-9]+\\), column \\([0-9]+\\), character \\([0-9]+\\)") s 0) then + `File { + filename = Str.matched_group 1 s; + line = Str.matched_group 2 s |> int_of_string; + column = Str.matched_group 3 s |> int_of_string; + character = Str.matched_group 4 s |> int_of_string; + } + else + (Printf.eprintf "error decoding loc: %s\n" s; exit 1) + +let decode_infer_event ({ name; payload },_ as x) : event = + match name, payload with + | "user:assign:resume", [s] -> `ResumeGoal (List.map int_of_string (String.split_on_char ' 's)) + | "user:backchain:fail-to", [s] -> `Fail s + | _ -> `Assign (decode_string x) + +let decode_infer_try (attempt,events) : attempt = + let loc, code = decode_attempt attempt in + let events = List.map decode_infer_event events in + { loc = decode_loc loc; code; events } + +let decode_chr_event ( { name; payload; goal_id}, time as x) = + match name with + | "user:rule:resume:resumed" -> Some (`CreateGoal goal_id) + | "user:CHR:rule-remove-constraints" -> Some (`RemoveConstraint (List.map int_of_string payload)) + | "user:assign" -> Some (`Assign (decode_string x)) + | _ -> None + +type chr_attempt2 = { loc : location; code : string; events : event list; success : bool; removed: goal_id list; resumed : goal_id list; timestamp : timestamp } +let a2 { loc ; code; events ; success = _; timestamp; removed; resumed} : chr_attempt = + { loc ; code; events ; timestamp; removed; resumed } + +let decode_chr_try ((_,start as attempt),events) : chr_attempt2 = + let loc, code = decode_attempt attempt in + let success = has "user:CHR:rule-fired" events <> None in + let _, stop = List.(hd (rev events)) in + let events = List.filter_map decode_chr_event events in + let events, resumed, removed = + let rec aux a1 a2 a3 = function + | [] -> List.(rev a1, rev a2, flatten (rev a3)) + | `Assign s :: rest -> aux (`Assign s :: a1) a2 a3 rest + | `CreateGoal g :: rest -> aux a1 (g :: a2) a3 rest + | `RemoveConstraint c :: rest -> aux a1 a2 (c :: a3) rest in + aux [] [] [] events in + { loc = decode_loc loc; code; events; success; removed; resumed; timestamp = { start; stop } } + +let decode_chr_try_list l = + let l = List.map decode_chr_try l in + let successful_attempts, failed_attempts = List.partition (fun x -> x.success) l in + assert(List.length successful_attempts > 0); + let failed_attempts = List.map a2 failed_attempts in + let successful_attempts = List.map a2 successful_attempts in + failed_attempts, successful_attempts + + +let get_builtin_name l : builtin_name = + match has "user:rule:builtin:name" l with + | None -> assert false + | Some x -> `FFI (decode_string x) + +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 + let stack = { rule; step_id = step; runtime_id = rid } :: this_stack in + fstacks := StepMap.add (step,rid) stack !fstacks; + List.iter (fun g -> gstacks := GoalMap.add g stack !gstacks) siblings + +let update_stack (step,rid) goal_id rule = + let old_stack = try GoalMap.find goal_id !gstacks with Not_found -> [] in + let stack = { rule; step_id = step ; runtime_id = rid} :: old_stack in + gstacks := GoalMap.add goal_id stack !gstacks + + +let push_end_stack step goal_id siblings = + let this_stack = try GoalMap.find goal_id !gstacks with Not_found -> [] in + let stack = this_stack in + fstacks := StepMap.add step stack !fstacks; + assert(siblings=[]) + +let elaborate_step (step,rid) (timestamp,(items : (item * time) list)) : t = +try + let items = List.rev items in + let rids = List.map (fun (x,_) -> x.runtime_id) items in + let rid = List.hd rids in + assert(List.for_all (fun x -> x = rid) rids); + 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 stop = + match has "user:assign" items with + | None -> assert false + | Some (_,time) -> time in + Findall {goal_id;goal;result;timestamp = { start; stop}} + | `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 + Suspend {goal_id;goal;sibling = List.hd sibling} + | `Cut ({ goal_id; payload = [pred;goal] },_) -> + let () = push_stack (step,rid) goal_id (`BuiltinRule (`FFI "!")) [] in + (* Cut *) assert false + | `Resumption l -> + let resumed = List.map (fun ({ goal_id; payload },_) -> + let () = update_stack (step,rid) goal_id (`BuiltinRule (`Logic "resume")) in + goal_id) l in + Resume resumed + | `CHR(chr_store_before,chr_store_after) -> + let trylist = all_chr_event_chains "user:CHR:try" items in + let failed_attempts, successful_attempts = decode_chr_try_list trylist in + CHR { failed_attempts; successful_attempts; chr_store_before; chr_store_after } + | `Init g -> Init g + | `Focus ({ goal_id; payload = [pred;goal] },_) -> + let action = + match has "user:rule" items with + | None | Some ({ payload = [] },_) | Some ({ payload = _ :: _ :: _ },_) -> assert false (* bug in instrumentaion *) + | Some ({ payload = [ name ] },_) -> + let siblings = all "user:subgoal" decode_int items in + let outcome = + match has ("user:rule:"^name) items with + | Some ({ payload = [ "success" ] },_) -> Success { siblings } + | Some ({ payload = [ "fail" ] },_) -> + (*assert(siblings = []);*) + Fail + | _ -> assert false (* bug *) in + if name = "backchain" then + let trylist = all_infer_event_chains "user:rule:backchain:try" items in + let trylist = List.map decode_infer_try trylist in + if trylist <> [] then begin (* can be empty if the goal is, say, fail *) + let { loc; code } : attempt = List.hd trylist in + let () = push_stack (step,rid) goal_id (`UserRule { rule_loc = loc; rule_text = code }) siblings in + () + end else begin + let () = push_end_stack (step,rid) goal_id siblings in + () + end; + Backchain { trylist; outcome } + else if name = "builtin" then + let name = get_builtin_name items in + let () = push_stack (step,rid) goal_id (`BuiltinRule name) siblings in + let events = all_infer_event_chains "user:rule:builtin:name" items in (* ??? *) + assert(List.length events = 1); + let _, events = List.hd events in + Builtin { name; outcome; events = List.map decode_infer_event events } + else + let name = `Logic name 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 = + if events <> [] then snd @@ List.hd events + else [] in + Builtin { name; outcome; events = List.map decode_infer_event events } + in + Inference { rid; pred; goal; goal_id; action } + + | _ -> assert false +with e -> + let e = Printexc.to_string e in + raise (Failure (Printf.sprintf "elaborating step %d: %s" step e)) + +let elaborate (steps : (timestamp * (item * time) list) StepMap.t) = + let goal_text = + let goals : string GoalMap.t ref = ref GoalMap.empty in (* goal_id -> goal *) + StepMap.iter (fun _ (_,is) -> List.iter (fun i -> + match has "user:newgoal" [i] with + | None -> () + | Some ({ goal_id },_) -> goals := GoalMap.add goal_id (decode_string i) !goals) is) steps; + !goals in + let steps : Elaborated_step.t StepMap.t = StepMap.mapi elaborate_step steps in + { steps; stack_frames = !fstacks; goal_text } + +let success_analysis (elaborated_steps : Elaborated_step.t StepMap.t) = + + let aggregated_goal_success = + let gsuccess : bool GoalMap.t ref = ref GoalMap.empty in (* goal_id -> true = success *) + let set_success goal_id b = + gsuccess := GoalMap.add goal_id ((try GoalMap.find goal_id !gsuccess with Not_found -> false) || b) !gsuccess in + let aggregate_success l = + List.fold_left (&&) true (List.map (fun x -> + try GoalMap.find x !gsuccess + with Not_found -> false) l) in + StepMap.bindings elaborated_steps |> List.rev |> List.iter (function + | _, (_,Resume _) -> () + | _, (_,Suspend _) -> () + | _, (_,Cut _) -> () + | _, (_,CHR _) -> () + | _, (_,Init _) -> () + | _, (_,Findall { goal_id }) -> set_success goal_id true + | _, (_,Inference { goal_id; action = Builtin { outcome = Fail }}) -> set_success goal_id false + | _, (_,Inference { goal_id; action = Builtin { outcome = Success { siblings } }}) -> set_success goal_id (aggregate_success siblings) + | _, (_,Inference { goal_id; action = Backchain { outcome = Fail }}) -> set_success goal_id false + | _, (_,Inference { goal_id; action = Backchain { outcome = Success { siblings } }}) -> set_success goal_id (aggregate_success siblings) + ); + !gsuccess in + + let goal_attempts = + let gattempts : (step_id * runtime_id) list GoalMap.t ref = ref GoalMap.empty in (* goal_id -> true = success *) + let add_more_success goal_id step_id = + try + let l = GoalMap.find goal_id !gattempts in + gattempts := GoalMap.add goal_id (step_id :: l) !gattempts + with Not_found -> + gattempts := GoalMap.add goal_id [step_id] !gattempts + in + StepMap.bindings elaborated_steps |> List.iter (function + | _, (_,Resume _) -> () + | _, (_,Suspend _) -> () + | _, (_,Findall _) -> () + | _, (_,Cut _) -> () + | _, (_,CHR _) -> () + | _, (_,Init _) -> () + | _, (_,Inference { action = Builtin _}) -> () + | _, (_,Inference { action = Backchain { outcome = Fail }}) -> () + | step_id, (_,Inference { goal_id; action = Backchain { outcome = Success _ }}) -> + add_more_success goal_id step_id + ); + !gattempts in + + { aggregated_goal_success; goal_attempts } + +end + +(* Aggrgates some data computed by Elaborate and structures sub-traces *) +module Trace : sig + + val cards : + Elaborate.Elaborated_step.t StepMap.t -> + stack_frames:frame list StepMap.t -> + aggregated_goal_success:bool GoalMap.t -> + goal_text:string GoalMap.t -> + goal_attempts:(step_id * runtime_id) list GoalMap.t -> + trace + +end = struct + + open Elaborate.Elaborated_step + + let find_success goal_success x = + try GoalMap.find x goal_success + with Not_found -> false + + let find_goal_text goal_goal_text x = + try GoalMap.find x goal_goal_text + with Not_found -> raise (Failure (Printf.sprintf "find_goal_text %d not found" x)) + + + let cards elaborated_steps ~stack_frames ~aggregated_goal_success ~goal_text ~goal_attempts : trace = + let find_success = find_success aggregated_goal_success in + let find_goal_text = find_goal_text goal_text in + let pre_cards = + StepMap.bindings elaborated_steps |> List.map (fun ((step_id,runtime_id),(timestamp,step)) -> + let step = + match step with + | Inference { rid; goal; pred; goal_id; action } -> + let stack = + try StepMap.find (step_id,runtime_id) stack_frames + with Not_found -> assert false in + let failed_attempts, successful_attempts = + match action with + | Builtin { name; outcome = Fail; events } -> + [{ rule = `BuiltinRule name ; events}],[] + | Builtin { name; outcome = Success { siblings }; events } -> + let siblings_aggregated_outcome = + if List.fold_left (&&) true (List.map find_success siblings) then `Success else `Fail in + let siblings = List.map (fun goal_id -> { goal_id; goal_text = find_goal_text goal_id }) siblings in + [],[{ attempt = { rule = `BuiltinRule name; events}; siblings; siblings_aggregated_outcome }] + | Backchain { trylist ; outcome = Fail } -> + List.map (fun ({ loc; code; events } : attempt) -> { rule = `UserRule { rule_text = code; rule_loc = loc } ; events } ) trylist,[] + | Backchain { trylist ; outcome = Success { siblings } } -> + let faillist = List.tl trylist in + let { loc; code; events } : attempt = List.hd trylist in + List.map (fun ({ loc; code; events } : attempt) -> { rule = `UserRule { rule_text = code; rule_loc = loc } ; events } ) faillist, + let siblings_aggregated_outcome = + if List.fold_left (&&) true (List.map find_success siblings) then `Success else `Fail in + let siblings = List.map (fun goal_id -> { goal_id; goal_text = find_goal_text goal_id }) siblings in + [{attempt = { rule = `UserRule { rule_loc = loc; rule_text = code }; events}; siblings; siblings_aggregated_outcome}] + in + let more_successful_attempts = + try + GoalMap.find goal_id goal_attempts |> + List.filter (fun (s,r) -> r = runtime_id && s > step_id) |> + List.map fst |> + List.sort Stdlib.compare + with + Not_found -> [] in + let inference = { + current_goal_id = goal_id; + current_goal_text = goal; + current_goal_predicate = pred; + failed_attempts; + successful_attempts; + more_successful_attempts; + stack; + } in + assert(runtime_id = rid); + `Inference inference + | Resume l -> + `Resume (List.map (fun goal_id -> { goal_id; goal_text = find_goal_text goal_id }) l) + | Suspend { goal; goal_id; sibling } -> + let stack = + try StepMap.find (step_id,runtime_id) stack_frames + with Not_found -> assert false in + `Suspend { + suspend_goal_id = goal_id; + suspend_goal_text = goal; + suspend_sibling = { goal_id = sibling; goal_text = find_goal_text sibling }; + suspend_stack = stack; + } + | Cut l -> assert false + | Findall { goal; goal_id; timestamp; result } -> + `Findall_TODO ( goal, goal_id, timestamp, result) + | CHR { failed_attempts; successful_attempts; chr_store_before; chr_store_after } -> + let chr_store_before = chr_store_before |> List.map (fun (goal_id,goal_text) -> { goal_id; goal_text }) in + let chr_store_after = chr_store_after |> List.map (fun (goal_id,goal_text) -> { goal_id; goal_text }) in + `CHR_TODO (failed_attempts,successful_attempts,chr_store_before, chr_store_after) + | Init goal_id -> `Init { goal_id; goal_text = find_goal_text goal_id } + in + timestamp,(step,step_id,runtime_id)) in + (* bad complexity *) + let in_time_stamp { start; stop } { start = start1; stop = stop1 } = start1 >= start && stop1 <= stop in + let rec to_chr_attempt ( x : chr_attempt) : Trace_atd.chr_attempt = + let chr_loc = match x.loc with `File x -> x | `Context _ -> assert false in + let chr_text = x.code in + let chr_condition_cards : card list = + pre_cards |> List.filter (fun (time,_) -> in_time_stamp x.timestamp time) + |> List.map pre_card2card in + assert( + let rid = (List.hd chr_condition_cards).runtime_id in + List.for_all (fun ({ runtime_id } : card) -> runtime_id = rid) chr_condition_cards); + { Trace_atd.chr_loc; chr_text; chr_condition_cards } + + and to_successful_chr_attempt ( x : chr_attempt) : successful_chr_attempt = + let chr_loc = match x.loc with `File x -> x | `Context _ -> assert false in + let chr_text = x.code in + let chr_condition_cards : card list = + pre_cards |> List.filter (fun (time,_) -> in_time_stamp x.timestamp time) + |> List.map pre_card2card in + assert( + let rid = (List.hd chr_condition_cards).runtime_id in + List.for_all (fun ({ runtime_id } : card) -> runtime_id = rid) chr_condition_cards); + let chr_new_goals = List.map (fun goal_id -> { goal_id; goal_text = find_goal_text goal_id }) x.resumed in + { chr_attempt = { chr_loc; chr_text; chr_condition_cards }; chr_new_goals; chr_removed_goals = x.removed } + + and inference_color rid { successful_attempts; more_successful_attempts } = + match successful_attempts, List.rev more_successful_attempts with + | [], [] -> `Red + | [], _ :: _ -> assert false + | [ { siblings_aggregated_outcome = `Success }], [] -> `Green + | [ { siblings_aggregated_outcome = `Success }], _ :: _ -> `YellowGreen + | [ { siblings_aggregated_outcome = `Fail }], [] -> `Red + | [ { siblings_aggregated_outcome = `Fail }], last :: _ -> + let (_,(step,_,_)) = List.find (fun (_,(_,step_id,runtime_id)) -> runtime_id = rid && step_id = last) pre_cards in + begin match step with + | `Inference x -> + begin match inference_color rid x with + | `Green -> `YellowGreen + | `Red -> `YellowRed + | x -> x + end + | _ -> assert false + end + | _ -> assert false + + and pre_card2card (_,(step,step_id,runtime_id)) = + match step with + | `Init g -> { step_id; step = `Init g; runtime_id; color = `Grey } + | `Resume x -> { step_id; step = `Resume x; runtime_id; color = `Grey } + | `Inference x -> { step_id; step = `Inference x; runtime_id; color = inference_color runtime_id x } + | `CHR_TODO (failed_attempts,successful_attempts,chr_store_before, chr_store_after) -> + let chr_failed_attempts = List.map to_chr_attempt failed_attempts in + let chr_successful_attempts = List.map to_successful_chr_attempt successful_attempts in + let step = `CHR { chr_failed_attempts; chr_successful_attempts; chr_store_before; chr_store_after} in + { step_id; step; runtime_id; color = `Grey } + | `Findall_TODO ( goal, goal_id, timestamp, result) -> + let findall_cards = + pre_cards |> List.filter (fun (time,_) -> in_time_stamp timestamp time) in + let findall_cards = findall_cards |> List.map pre_card2card in + assert( + let rid = (List.hd findall_cards).runtime_id in + List.for_all (fun ({ runtime_id } : card) -> runtime_id = rid) findall_cards); + let stack = + try StepMap.find (step_id,runtime_id) stack_frames + with Not_found -> assert false in + let findall = { + findall_goal_id = goal_id; + findall_goal_text = goal; + findall_cards; + findall_solution_text = result; + findall_stack = stack } in + { step_id; step = `Findall findall; runtime_id; color = `Green } + | `Suspend x -> { step_id; step = `Suspend x; runtime_id; color = `Grey } + | `Cut x -> { step_id; step = `Cut x; runtime_id; color = `Grey } + in + pre_cards |> List.filter (fun (_,(_,_,rid)) -> rid = 0) |> List.map pre_card2card + +end + +let main = + let raw_steps = Raw.read_stdin () in + + let { Elaborate.steps; stack_frames; goal_text } = Elaborate.elaborate raw_steps in + let { Elaborate.aggregated_goal_success; goal_attempts } = Elaborate.success_analysis steps in + + let cards = Trace.cards steps ~stack_frames ~aggregated_goal_success ~goal_text ~goal_attempts in + + let ob = Bi_outbuf.create_channel_writer stdout in + write_trace ob cards; + Bi_outbuf.flush_channel_writer ob diff --git a/src/builtin.ml b/src/builtin.ml index c2ac13c35..aa1dedb2b 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -1420,7 +1420,7 @@ let ocaml_runtime = let open BuiltIn in let open BuiltInData in [ In (string,"Name", Out(int, "Value", Easy "reads the Value of a trace point Name")), - (fun s _ ~depth:_ -> !:(Trace_ppx_runtime.Runtime.get_cur_step s))), + (fun s _ ~depth:_ -> !:(Trace_ppx_runtime.Runtime.get_cur_step ~runtime_id:0 s))), DocAbove); MLCode(Pred("gc.get", diff --git a/src/runtime.ml b/src/runtime.ml index 0e754d7d4..b35615f36 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -373,6 +373,8 @@ module ConstraintStoreAndTrail : sig val contents : ?overlapping:uvar_body list -> unit -> (constraint_def * blockers) list val print : ?pp_ctx:pp_ctx -> Fmt.formatter -> (constraint_def * blockers) list -> unit + val print1 : ?pp_ctx:pp_ctx -> Fmt.formatter -> constraint_def * blockers -> unit + val print_gid: Fmt.formatter -> constraint_def * blockers -> unit val pp_stuck_goal : ?pp_ctx:pp_ctx -> Fmt.formatter -> stuck_goal -> unit val state : State.t Fork.local_ref @@ -568,7 +570,7 @@ let undo ~old_trail ?old_state () = | None -> () ;; -let print ?pp_ctx fmt x = +let print1 ?pp_ctx fmt x = let pp_depth fmt d = if d > 0 then Fmt.fprintf fmt "{%a} :@ " @@ -579,14 +581,21 @@ let print ?pp_ctx fmt x = (pplist (fun fmt { hdepth = d; hsrc = t } -> uppterm ?pp_ctx d [] ~argsdepth:0 empty_env fmt t) ", ") ctx in let pp_goal depth = uppterm ?pp_ctx depth [] ~argsdepth:0 empty_env in - pplist (fun fmt ({ cdepth=depth;context=pdiff; conclusion=g }, blockers) -> - Fmt.fprintf fmt " @[@[%a%a%a@]@ /* suspended on %a */@]" - pp_depth depth - pp_hyps pdiff - (pp_goal depth) g - (pplist (uppterm ?pp_ctx 0 [] ~argsdepth:0 empty_env) ", ") - (List.map (fun r -> UVar(r,0,0)) blockers) - ) " " fmt x + let { cdepth=depth;context=pdiff; conclusion=g }, blockers = x in + Fmt.fprintf fmt " @[@[%a%a%a@]@ /* suspended on %a */@]" + pp_depth depth + pp_hyps pdiff + (pp_goal depth) g + (pplist (uppterm ?pp_ctx 0 [] ~argsdepth:0 empty_env) ", ") + (List.map (fun r -> UVar(r,0,0)) blockers) + +let print_gid fmt x = + let { cgid = gid [@trace]; cdepth = _ }, _ = x in + let () [@trace] = Fmt.fprintf fmt "%a" UUID.pp gid in + () + +let print ?pp_ctx fmt x = + pplist (print1 ?pp_ctx) " " fmt x let pp_stuck_goal ?pp_ctx fmt { kind; blockers } = match kind with | Unification { adepth = ad; env = e; bdepth = bd; a; b } -> @@ -608,7 +617,7 @@ let (@:=) r v = (T.trail_assignment[@inlined]) r; if uvar_is_a_blocker r then begin let blocked = CS.blocked_by r in - [%spy "user:assign(resume)" ~rid (fun fmt l -> + [%spy "user:assign:resume" ~rid (fun fmt l -> let l = map_filter (function | { kind = Constraint { cgid; _ } ; _ } -> Some cgid | _ -> None) l in @@ -983,7 +992,7 @@ let rec move ~argsdepth e ?avoid ~from ~to_ t = else let t, assignment = expand_uv ~depth:(from+depth) r ~lvl:vardepth ~ano:argsno in option_iter (fun (r,_,assignment) -> - [%spy "user:assign(expand)" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a" + [%spy "user:assign:expand" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a" (uppterm (from+depth) [] ~argsdepth e) x (uppterm vardepth [] ~argsdepth e) assignment) ()]; r @:= assignment) assignment; @@ -1025,7 +1034,7 @@ let rec move ~argsdepth e ?avoid ~from ~to_ t = let r' = oref C.dummy in let newvar = mkAppUVar r' vardepth' !filteredargs_vardepth in let assignment = mknLam orig_argsno newvar in - [%spy "user:assign(restrict)" ~rid (fun fmt () -> Fmt.fprintf fmt "%d %a := %a" vardepth + [%spy "user:assign:restrict" ~rid (fun fmt () -> Fmt.fprintf fmt "%d %a := %a" vardepth (ppterm (from+depth) [] ~argsdepth e) x (ppterm (vardepth) [] ~argsdepth e) assignment) ()]; r @:= assignment; @@ -1483,7 +1492,7 @@ let bind ~argsdepth r gamma l a d delta b left t e = end] in try let v = mknLam new_lams (bind b delta 0 t) in - [%spy "user:assign(HO)" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a" + [%spy "user:assign:HO" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a" (uppterm gamma [] ~argsdepth e) (UVar(r,gamma,0)) (uppterm gamma [] ~argsdepth e) v) ()]; r @:= v; @@ -1756,14 +1765,14 @@ let rec unif argsdepth matching depth adepth a bdepth b e = | _, UVar (r,origdepth,args) when args > 0 && match a with UVar(r1,_,_) | AppUVar(r1,_,_) -> r != r1 | _ -> true -> let v = fst (make_lambdas origdepth args) in - [%spy "user:assign(simplify)" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a" + [%spy "user:assign:simplify" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a" (uppterm depth [] ~argsdepth e) (UVar(r,origdepth,0)) (uppterm depth [] ~argsdepth e) v) ()]; r @:= v; unif argsdepth matching depth adepth a bdepth b e | UVar (r,origdepth,args), _ when args > 0 && match b with UVar(r1,_,_) | AppUVar(r1,_,_) -> r != r1 | _ -> true -> let v = fst (make_lambdas origdepth args) in - [%spy "user:assign(simplify)" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a" + [%spy "user:assign:simplify" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a" (uppterm depth [] ~argsdepth e) (UVar(r,origdepth,0)) (uppterm depth [] ~argsdepth e) v) ()]; r @:= v; @@ -1882,11 +1891,11 @@ and eta_contract_stack_or_expand_heap argsdepth matching depth adepth a c args b let unif ~argsdepth ~matching (gid[@trace]) adepth e bdepth a b = let res = unif argsdepth matching 0 adepth a bdepth b e in [%spy "dev:unif:out" ~rid Fmt.pp_print_bool res]; - [%spy "user:select" ~rid ~gid ~cond:(not res) (fun fmt () -> + [%spy "user:backchain:fail-to" ~rid ~gid ~cond:(not res) (fun fmt () -> let op = if matching then "match" else "unify" in - Fmt.fprintf fmt "@[fail to %s: %a@ with %a@]" op - (ppterm (adepth) [] ~argsdepth:bdepth empty_env) a - (ppterm (bdepth) [] ~argsdepth:bdepth e) b) ()]; + Fmt.fprintf fmt "@[%s@ %a@ with@ %a@]" op + (uppterm (adepth) [] ~argsdepth:bdepth empty_env) a + (uppterm (bdepth) [] ~argsdepth:bdepth e) b) ()]; res ;; @@ -2273,8 +2282,8 @@ module Indexing = struct (* {{{ *) let mustbevariablec = min_int (* uvar or uvar t or uvar l t *) let ppclause f ~depth ~hd { args = args; hyps = hyps } = - Fmt.fprintf f "@[%s %a :- %a.@]" (C.show hd) - (pplist (uppterm ~min_prec:(Elpi_parser.Parser_config.appl_precedence+1) depth [] ~argsdepth:0 empty_env) " ") args + Fmt.fprintf f "@[%a :- %a.@]" + (uppterm ~min_prec:(Elpi_parser.Parser_config.appl_precedence+1) depth [] ~argsdepth:0 empty_env) (C.mkAppL hd args) (pplist (uppterm ~min_prec:(Elpi_parser.Parser_config.appl_precedence+1) depth [] ~argsdepth:0 empty_env) ", ") hyps let tail_opt = function @@ -2554,7 +2563,7 @@ let get_clauses ~depth predicate goal { index = m } = List.(map fst (sort (fun (_,cl1) (_,cl2) -> cl2 - cl1) cl)) with Not_found -> [] in - [%log "get_clauses" (C.show predicate) (List.length rc)]; + [%log "get_clauses" ~rid (C.show predicate) (List.length rc)]; rc (* flatten_snd = List.flatten o (List.map ~~snd~~) *) @@ -2616,7 +2625,7 @@ let orig_prolog_program = Fork.new_local (make_index ~depth:0 ~indexing:C.Map.em module Clausify : sig - val clausify : prolog_prog -> depth:int -> term -> (constant*clause) list * clause_src list * int + val clausify : loc:Loc.t option -> prolog_prog -> depth:int -> term -> (constant*clause) list * clause_src list * int val clausify1 : loc:Loc.t -> mode C.Map.t -> nargs:int -> depth:int -> term -> (constant*clause) * clause_src * int @@ -2692,16 +2701,16 @@ r :- (pi X\ pi Y\ q X Y :- pi c\ pi d\ q (Z c d) (X c d) (Y c)) => ... *) * - the argument lives in (depth+lts) * - the clause will live in (depth+lcs) *) -let rec claux1 ?loc get_mode vars depth hyps ts lts lcs t = +let rec claux1 loc get_mode vars depth hyps ts lts lcs t = [%trace "clausify" ~rid ("%a %d %d %d %d\n%!" (ppterm (depth+lts) [] ~argsdepth:0 empty_env) t depth lts lcs (List.length ts)) begin match t with | Discard -> error ?loc "ill-formed hypothetical clause: discard in head position" | App(c, g2, [g1]) when c == Global_symbols.rimplc -> - claux1 ?loc get_mode vars depth ((ts,g1)::hyps) ts lts lcs g2 + claux1 loc get_mode vars depth ((ts,g1)::hyps) ts lts lcs g2 | App(c, _, _) when c == Global_symbols.rimplc -> error ?loc "ill-formed hypothetical clause" | App(c, g1, [g2]) when c == Global_symbols.implc -> - claux1 ?loc get_mode vars depth ((ts,g1)::hyps) ts lts lcs g2 + claux1 loc get_mode vars depth ((ts,g1)::hyps) ts lts lcs g2 | App(c, _, _) when c == Global_symbols.implc -> error ?loc "ill-formed hypothetical clause" | App(c, arg, []) when c == Global_symbols.sigmac -> let b = get_lambda_body ~depth:(depth+lts) arg in @@ -2711,10 +2720,10 @@ let rec claux1 ?loc get_mode vars depth hyps ts lts lcs t = match args with [] -> Const (depth+lcs) | hd::rest -> App (depth+lcs,hd,rest) in - claux1 ?loc get_mode vars depth hyps (cst::ts) (lts+1) (lcs+1) b + claux1 loc get_mode vars depth hyps (cst::ts) (lts+1) (lcs+1) b | App(c, arg, []) when c == Global_symbols.pic -> let b = get_lambda_body ~depth:(depth+lts) arg in - claux1 ?loc get_mode (vars+1) depth hyps (Arg(vars,0)::ts) (lts+1) lcs b + claux1 loc get_mode (vars+1) depth hyps (Arg(vars,0)::ts) (lts+1) lcs b | App(c, _, _) when c == Global_symbols.andc -> error ?loc "Conjunction in the head of a clause is not supported" | Const _ @@ -2750,10 +2759,10 @@ let rec claux1 ?loc get_mode vars depth hyps ts lts lcs t = [%spy "dev:claudify:extra-clause" ~rid (ppclause ~depth:(depth+lcs) ~hd) c]; (hd,c), { hdepth = depth; hsrc = g }, lcs | UVar ({ contents=g },from,args) when g != C.dummy -> - claux1 ?loc get_mode vars depth hyps ts lts lcs + claux1 loc get_mode vars depth hyps ts lts lcs (deref_uv ~from ~to_:(depth+lts) args g) | AppUVar ({contents=g},from,args) when g != C.dummy -> - claux1 ?loc get_mode vars depth hyps ts lts lcs + claux1 loc get_mode vars depth hyps ts lts lcs (deref_appuv ~from ~to_:(depth+lts) args g) | Arg _ | AppArg _ -> error ?loc "The head of a clause cannot be flexible" @@ -2764,7 +2773,7 @@ let rec claux1 ?loc get_mode vars depth hyps ts lts lcs t = | Nil | Cons _ -> error ?loc "ill-formed hypothetical clause" end] -let clausify { index } ~depth t = +let clausify ~loc { index } ~depth t = let get_mode x = match Ptmap.find x index with | TwoLevelIndex { mode } -> mode @@ -2774,7 +2783,7 @@ let clausify { index } ~depth t = let clauses, program, lcs = List.fold_left (fun (clauses, programs, lcs) t -> let clause, program, lcs = - try claux1 get_mode 0 depth [] [] 0 lcs t + try claux1 loc get_mode 0 depth [] [] 0 lcs t with CannotDeclareClauseForBuiltin(loc,c) -> error ?loc ("Declaring a clause for built in predicate " ^ C.show c) in @@ -2783,7 +2792,7 @@ let clausify { index } ~depth t = ;; let clausify1 ~loc m ~nargs ~depth t = - claux1 ~loc (fun x -> try C.Map.find x m with Not_found -> []) + claux1 (Some loc) (fun x -> try C.Map.find x m with Not_found -> []) nargs depth [] [] 0 0 t end (* }}} *) @@ -3107,7 +3116,7 @@ let make_constraint_def ~rid ~gid:(gid[@trace]) depth prog pdiff conclusion = let delay_goal ?(filter_ctx=fun _ -> true) ~depth prog ~goal:g (gid[@trace]) ~on:keys = let pdiff = local_prog prog in let pdiff = List.filter filter_ctx pdiff in - [%spy "user:suspend" ~rid ~gid (uppterm depth [] ~argsdepth:0 empty_env) g]; + let gid[@trace] = make_subgoal_id gid (depth,g) in let kind = Constraint (make_constraint_def ~rid ~gid:(gid[@trace]) depth prog pdiff g) in CS.declare_new { kind ; blockers = keys } ;; @@ -3186,6 +3195,33 @@ let match_head { conclusion = x; cdepth } p = | _ -> false ;; +let pp_opt start f fmt = function + | None -> () + | Some x -> Fmt.fprintf fmt "%s%a" start f x + +let pp_optl start f fmt = function + | [] -> () + | x -> Fmt.fprintf fmt "%s%a" start (pplist f " ") x + +let pp_optterm stop fmt x = + match deref_head ~depth:0 x with + | Discard -> () + | _ -> Fmt.fprintf fmt "%a%s" (uppterm 0 [] ~argsdepth:0 empty_env) x stop + +let pp_sequent fmt { CHR.eigen; context; conclusion } = + Fmt.fprintf fmt "@[(%a%a%a)@]" + (pp_optterm " : ") eigen + (pp_optterm " ?- ") context + (uppterm 0 [] ~argsdepth:0 empty_env) conclusion + +let pp_urule fmt { CHR. to_match; to_remove; new_goal; guard } = + Fmt.fprintf fmt "@[%a@ %a@ %a@ %a@]" + (pplist pp_sequent " ") to_match + (pp_optl "\\ " pp_sequent) to_remove + (pp_opt "| " (uppterm ~min_prec:Elpi_parser.Parser_config.inf_precedence 0 [] ~argsdepth:0 empty_env)) guard + (pp_opt "<=> " pp_sequent) new_goal + + let try_fire_rule (gid[@trace]) rule (constraints as orig_constraints) = let { CHR. @@ -3325,7 +3361,6 @@ let try_fire_rule (gid[@trace]) rule (constraints as orig_constraints) = let resumption to_be_resumed_rev = List.map (fun { cdepth = d; prog; conclusion = g; cgid = gid [@trace] } -> - [%spy "user:resume" ~rid ~gid (uppterm d [] ~argsdepth:0 empty_env) g]; (repack_goal[@inlined]) ~depth:d (gid[@trace]) prog g) (List.rev to_be_resumed_rev) @@ -3356,6 +3391,8 @@ let propagation () = let to_be_resumed_rev = ref [] in let removed = ref [] in let outdated cs = List.exists (fun x -> List.memq x !removed) cs in + let some_rule_fired[@trace] = ref false in + let orig_store_contents[@trace] = CS.contents () in while !CS.new_delayed <> [] do match !CS.new_delayed with | [] -> anomaly "Empty list" @@ -3384,11 +3421,12 @@ let propagation () = (* a constraint just removed may occur in a permutation (that * was generated before the removal *) if outdated constraints then () - else begin - [%spy "user:CHR:try-rule" ~rid ~gid:active.cgid Loc.pp rule.rule_loc]; + else begin + [%spy "user:CHR:try" ~rid ~gid:active.cgid Loc.pp rule.rule_loc pp_urule rule]; match try_fire_rule (active.cgid[@trace]) rule constraints with | None -> [%spy "user:CHR:rule-failed" ~rid ] | Some (rule_name, to_be_removed, to_be_added, assignments) -> + let ()[@trace] = some_rule_fired := true in [%spy "user:CHR:rule-fired" ~rid ~gid: (active.cgid[@trace]) pp_string rule_name]; [%spyl "user:CHR:rule-remove-constraints" ~rid ~gid: (active.cgid[@trace]) (fun fmt { cgid } -> UUID.pp fmt cgid) to_be_removed]; removed := to_be_removed @ !removed; @@ -3400,6 +3438,16 @@ let propagation () = end) done); done; + let ()[@trace] = + if !some_rule_fired then begin + orig_store_contents |> List.iter (fun it -> + [%spy "user:CHR:store:before" ~rid CS.print_gid it CS.print1 it] + ); + CS.contents () |> List.iter (fun it -> + [%spy "user:CHR:store:after" ~rid CS.print_gid it CS.print1 it] + ); + end + in !to_be_resumed_rev end (* }}} *) @@ -3429,6 +3477,16 @@ let pp_candidate ~depth ~k fmt ({ loc } as cl) = | Some x -> Util.CData.pp fmt (Ast.cloc.Util.CData.cin x) | None -> Fmt.fprintf fmt "hypothetical clause: %a" (ppclause ~depth ~hd:k) cl +let hd_c_of = function + | Const _ as x -> x + | App(x,_,_) -> C.mkConst x + | Builtin(x,_) -> C.mkConst x + | _ -> C.dummy + +let pp_resumed_goal { depth; program; goal; gid = gid[@trace] } = + [%spy "user:rule:resume:resumed" ~rid ~gid (uppterm depth [] ~argsdepth:0 empty_env) goal] +;; + (* The block of recursive functions spares the allocation of a Some/None * at each iteration in order to know if one needs to backtrack or continue *) let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x executable -> 'x runtime = @@ -3446,48 +3504,62 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut match resume_all () with | None -> - [%spy "user:rule" ~rid ~gid pp_string "fail-resume"]; + [%spy "user:rule" ~rid pp_string "constraint-failure"]; [%tcall next_alt alts] - | Some ({ depth = ndepth; program; goal; gid = ngid [@trace] } :: goals) -> - [%spy "user:rule" ~rid ~gid pp_string "resume"]; + | Some ({ depth = ndepth; program; goal; gid = ngid [@trace] } :: goals as all) -> + [%spy "user:rule" ~rid pp_string "resume"]; + (List.iter pp_resumed_goal all)[@trace]; + [%spy "user:rule:resume" ~rid pp_string "success"]; [%tcall run ndepth program goal (ngid[@trace]) (goals @ (repack_goal[@inlined]) (gid[@trace]) ~depth p g :: gs) next alts cutto_alts] | Some [] -> - [%spy "user:curgoal" ~rid ~gid (uppterm depth [] ~argsdepth:0 empty_env) g]; + [%spyl "user:curgoal" ~rid ~gid (uppterm depth [] ~argsdepth:0 empty_env) [hd_c_of g;g]]; match g with - | Builtin(c,[]) when c == Global_symbols.cutc -> [%spy "user:rule" ~rid ~gid pp_string "cut"]; + | Builtin(c,[]) when c == Global_symbols.cutc -> [%tcall cut (gid[@trace]) gs next (alts[@trace]) cutto_alts] - | Builtin(c,[q;sol]) when c == Global_symbols.findall_solutionsc -> [%spy "user:rule" ~rid ~gid pp_string "findall"]; + | Builtin(c,[q;sol]) when c == Global_symbols.findall_solutionsc -> [%tcall findall depth p q sol (gid[@trace]) gs next alts cutto_alts] | App(c, g, gs') when c == Global_symbols.andc -> [%spy "user:rule" ~rid ~gid pp_string "and"]; let gs' = List.map (fun x -> (make_subgoal[@inlined]) ~depth (gid[@trace]) p x) gs' in let gid[@trace] = make_subgoal_id gid ((depth,g)[@trace]) in + [%spy "user:rule:and" ~rid ~gid pp_string "success"]; [%tcall run depth p g (gid[@trace]) (gs' @ gs) next alts cutto_alts] | Cons (g,gs') -> [%spy "user:rule" ~rid ~gid pp_string "and"]; let gs' = (make_subgoal[@inlined]) ~depth (gid[@trace]) p gs' in let gid[@trace] = make_subgoal_id gid ((depth,g)[@trace]) in + [%spy "user:rule:and" ~rid ~gid pp_string "success"]; [%tcall run depth p g (gid[@trace]) (gs' :: gs) next alts cutto_alts] - | Nil -> [%spy "user:rule" ~rid ~gid pp_string "true"]; + | Nil -> [%spy "user:rule" ~rid ~gid pp_string "true"]; [%spy "user:rule:true" ~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 - | Builtin(c,[l;r]) when c == Global_symbols.eqc -> [%spy "user:rule" ~rid ~gid pp_string "eq"]; - if unif ~argsdepth:depth ~matching:false (gid[@trace]) depth empty_env depth l r then - 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] - else [%tcall next_alt alts] + | Builtin(c,[l;r]) when c == Global_symbols.eqc -> [%spy "user:rule" ~rid ~gid pp_string "eq"]; [%spy "user:rule:builtin:name" ~rid ~gid pp_string (C.show c)]; + if unif ~argsdepth:depth ~matching:false (gid[@trace]) depth empty_env depth l r then begin + [%spy "user:rule:eq" ~rid ~gid pp_string "success"]; + 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 else begin + [%spy "user:rule:eq" ~rid ~gid pp_string "fail"]; + [%tcall next_alt alts] + end | App(c, g2, [g1]) when c == Global_symbols.rimplc -> [%spy "user:rule" ~rid ~gid pp_string "implication"]; - let clauses, pdiff, lcs = clausify p ~depth g1 in + let [@warning "-26"]loc = None in + let loc[@trace] = Some (Loc.initial ("(context step_id:" ^ string_of_int (Trace_ppx_runtime.Runtime.get_cur_step ~runtime_id:!rid "run") ^")")) in + let clauses, pdiff, lcs = clausify ~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 + [%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] | App(c, g1, [g2]) when c == Global_symbols.implc -> [%spy "user:rule" ~rid ~gid pp_string "implication"]; - let clauses, pdiff, lcs = clausify p ~depth g1 in + let [@warning "-26"]loc = None in + let loc[@trace] = Some (Loc.initial ("(context step_id:" ^ string_of_int (Trace_ppx_runtime.Runtime.get_cur_step ~runtime_id:!rid "run") ^")")) in + let clauses, pdiff, lcs = clausify ~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 + [%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] | App(c, arg, []) when c == Global_symbols.pic -> [%spy "user:rule" ~rid ~gid pp_string "pi"]; let f = get_lambda_body ~depth arg in @@ -3498,28 +3570,31 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut let v = UVar(oref C.dummy, depth, 0) in let fv = subst depth [v] f in let gid[@trace] = make_subgoal_id gid ((depth,fv)[@trace]) in + [%spy "user:rule:pi" ~rid ~gid pp_string "success"]; [%tcall run depth p fv (gid[@trace]) gs next alts cutto_alts] - | UVar ({ contents = g }, from, args) when g != C.dummy -> [%spy "user:rule" ~rid ~gid pp_string "deref"]; + | UVar ({ contents = g }, from, args) when g != C.dummy -> [%spy "user:rule" ~rid ~gid pp_string "deref"]; [%spy "user:rule:deref" ~rid ~gid pp_string "success"]; [%tcall run depth p (deref_uv ~from ~to_:depth args g) (gid[@trace]) gs next alts cutto_alts] - | AppUVar ({contents = t}, from, args) when t != C.dummy -> [%spy "user:rule" ~rid ~gid pp_string "deref"]; + | AppUVar ({contents = t}, from, args) when t != C.dummy -> [%spy "user:rule" ~rid ~gid pp_string "deref"]; [%spy "user:rule:deref" ~rid ~gid pp_string "success"]; [%tcall run depth p (deref_appuv ~from ~to_:depth args t) (gid[@trace]) gs next alts cutto_alts] - | Const k -> [%spy "user:rule" ~rid ~gid pp_string "backchain"]; + | Const k -> let clauses = get_clauses depth k g p in - [%spyl "user:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses]; + [%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] - | App (k,x,xs) -> [%spy "user:rule" ~rid ~gid pp_string "backchain"]; + | App (k,x,xs) -> let clauses = get_clauses depth k g p in - [%spyl "user:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses]; + [%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] - | Builtin(c, args) -> [%spy "user:rule" ~rid ~gid pp_string "builtin"]; + | Builtin(c, args) -> [%spy "user:rule" ~rid ~gid pp_string "builtin"]; [%spy "user:rule:builtin:name" ~rid ~gid pp_string (C.show c)]; begin match Constraints.exect_builtin_predicate c ~depth p (gid[@trace]) args with | gs' -> - [%spy "user:builtin" ~rid ~gid pp_string "success"]; + [%spy "user:rule:builtin" ~rid ~gid pp_string "success"]; (match List.map (fun g -> (make_subgoal[@inlined]) (gid[@trace]) ~depth p g) gs' @ 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]) | exception No_clause -> - [%spy "user:builtin" ~rid ~gid pp_string "fail"]; + [%spy "user:rule:builtin" ~rid ~gid pp_string "fail"]; [%tcall next_alt alts] end | Arg _ | AppArg _ -> anomaly "The goal is not a heap term" @@ -3532,10 +3607,10 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut (* 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 match cp with - | [] -> [%spy "user:select" ~rid ~gid pp_string "fail"]; + | [] -> [%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:select" ~rid ~gid (pp_option Util.CData.pp) (Util.option_map Ast.cloc.Util.CData.cin loc) (ppclause ~depth ~hd:k) { depth = c_depth; mode = c_mode; args = c_args; hyps = c_hyps; vars = c_vars; loc }]; + [%spy "user:rule:backchain:try" ~rid ~gid (pp_option Util.CData.pp) (Util.option_map Ast.cloc.Util.CData.cin loc) (ppclause ~depth ~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 == []; let env = Array.make c_vars C.dummy in @@ -3547,7 +3622,8 @@ 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 | matching :: ms -> unif ~argsdepth:depth ~matching (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 (k, arg, args_of_g, gs) (gid[@trace]) next alts cutto_alts cs] | true -> let oldalts = alts in let alts = if cs = [] then alts else @@ -3557,35 +3633,42 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut clauses = cs; cutto_alts = cutto_alts ; next = 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 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 = List.map (fun x-> (make_subgoal[@inlined]) (gid[@trace]) ~depth p (move ~argsdepth:depth ~from:c_depth ~to_:depth env x)) hs in - let gid[@trace] = make_subgoal_id gid ((depth,h)[@trace]) in + [%spy "user:rule:backchain" ~rid ~gid pp_string "success"]; [%tcall run depth p h (gid[@trace]) hs next alts oldalts] end end] and cut (gid[@trace]) gs next (alts[@trace]) cutto_alts = - [%spy "user:cut" ~rid ~gid (fun fmt 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 - Format.fprintf fmt "%a" (pplist (ppclause ~depth ~hd) " | ") clauses; + List.iter (fun c -> + [%spy "user:rule:cut" ~rid UUID.pp gid (pp_candidate ~depth ~k:hd) c]) + clauses; prune alts.next - end in - prune alts - ) alts]; + end + in + prune alts in if cutto_alts == noalts then (T.cut_trail[@inlined]) (); + [%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 and findall depth p g s (gid[@trace]) gs next alts cutto_alts = + [%spy "user:rule" ~rid ~gid pp_string "findall"]; let avoid = oref C.dummy in (* to force a copy *) let copy = move ~argsdepth:depth ~from:depth ~to_:depth empty_env ~avoid in let g = copy g in (* so that Discard becomes a variable *) @@ -3625,8 +3708,11 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut let solutions = list_to_lp_list (List.rev !solutions) in [%spy "findall solutions:" ~rid ~gid (ppterm depth [] ~argsdepth:0 empty_env) solutions]; match unif ~argsdepth:depth ~matching:false (gid[@trace]) depth empty_env depth s solutions with - | false -> [%tcall next_alt alts] + | false -> + [%spy "user:rule:findall" ~rid ~gid pp_string "fail"]; + [%tcall next_alt alts] | true -> + [%spy "user:rule:findall" ~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 @@ -3691,7 +3777,14 @@ end;*) trail = old_trail; state = old_state; adepth = depth; cutto_alts = cutto_alts; next = alts} = alts in T.undo ~old_trail ~old_state (); - backchain depth p (k, arg, args, gs) (gid[@trace]) next alts cutto_alts clauses + + [%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] in (* Finally the runtime *) @@ -3724,8 +3817,10 @@ end;*) set rid !max_runtime_id; let search = exec (fun () -> [%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; - run initial_depth !orig_prolog_program initial_goal ((UUID.make ())[@trace]) [] FNil noalts noalts) in + 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 next_solution = exec next_alt in incr max_runtime_id; diff --git a/tests/sources/trace.elab.json b/tests/sources/trace.elab.json new file mode 100644 index 000000000..6e9487539 --- /dev/null +++ b/tests/sources/trace.elab.json @@ -0,0 +1,1124 @@ +[ + { + "step_id": 0, + "runtime_id": 0, + "step": [ "Init", { "goal_text": "main", "goal_id": 4 } ], + "color": "Grey" + }, + { + "step_id": 1, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 4, + "current_goal_text": "main", + "current_goal_predicate": "main", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "events": [] + }, + "siblings": [ { "goal_text": "p 1 X0 ; p 2 X1", "goal_id": 5 } ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 2, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 5, + "current_goal_text": "p 1 X0 ; p 2 X1", + "current_goal_predicate": ";", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "events": [ [ "Assign", "A0 := p 1 X0" ] ] + }, + "siblings": [ { "goal_text": "p 1 X0", "goal_id": 6 } ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [ 11 ], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "YellowGreen" + }, + { + "step_id": 3, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 6, + "current_goal_text": "p 1 X0", + "current_goal_predicate": "p", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 1) :- (1 is 2 + 3).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 2, + "column": 0, + "character": 1 + } + ] + } + ], + "events": [ [ "Assign", "X0 := 1" ] ] + }, + "siblings": [ { "goal_text": "1 is 2 + 3", "goal_id": 7 } ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [ 7 ], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 1) :- (1 is 2 + 3).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 2, + "column": 0, + "character": 1 + } + ] + } + ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "YellowRed" + }, + { + "step_id": 4, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 7, + "current_goal_text": "1 is 2 + 3", + "current_goal_predicate": "is", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(A0 is A1) :- (calc A1 A0).", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 77, + "column": 0, + "character": 1165 + } + ] + } + ], + "events": [ + [ "Assign", "A0 := 1" ], + [ "Assign", "A1 := 2 + 3" ] + ] + }, + "siblings": [ { "goal_text": "calc (2 + 3) 1", "goal_id": 8 } ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 is A1) :- (calc A1 A0).", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 77, + "column": 0, + "character": 1165 + } + ] + } + ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 1) :- (1 is 2 + 3).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 2, + "column": 0, + "character": 1 + } + ] + } + ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 5, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 8, + "current_goal_text": "calc (2 + 3) 1", + "current_goal_predicate": "calc", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "FFI", "calc" ] ], + "events": [] + }, + "siblings": [ { "goal_text": "1 = 5", "goal_id": 9 } ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "FFI", "calc" ] ], + "step_id": 5, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 is A1) :- (calc A1 A0).", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 77, + "column": 0, + "character": 1165 + } + ] + } + ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 1) :- (1 is 2 + 3).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 2, + "column": 0, + "character": 1 + } + ] + } + ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 6, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 9, + "current_goal_text": "1 = 5", + "current_goal_predicate": "=", + "failed_attempts": [ + { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "events": [ [ "Fail", "unify 1 with 5" ] ] + } + ], + "successful_attempts": [], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "step_id": 6, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "FFI", "calc" ] ], + "step_id": 5, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 is A1) :- (calc A1 A0).", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 77, + "column": 0, + "character": 1165 + } + ] + } + ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 1) :- (1 is 2 + 3).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 2, + "column": 0, + "character": 1 + } + ] + } + ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 7, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 6, + "current_goal_text": "p 1 X0", + "current_goal_predicate": "p", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 2) :- (A0 = 1), (A1 = 2), (A0 = A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 3, + "column": 0, + "character": 22 + } + ] + } + ], + "events": [ [ "Assign", "X0 := 2" ] ] + }, + "siblings": [ + { "goal_text": "X2 = 1", "goal_id": 10 }, + { "goal_text": "X3 = 2", "goal_id": 11 }, + { "goal_text": "X2 = X3", "goal_id": 12 } + ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 2) :- (A0 = 1), (A1 = 2), (A0 = A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 3, + "column": 0, + "character": 22 + } + ] + } + ], + "step_id": 7, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 8, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 10, + "current_goal_text": "X2 = 1", + "current_goal_predicate": "=", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "events": [ [ "Assign", "X2 := 1" ] ] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "step_id": 8, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 2) :- (A0 = 1), (A1 = 2), (A0 = A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 3, + "column": 0, + "character": 22 + } + ] + } + ], + "step_id": 7, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 9, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 11, + "current_goal_text": "X3 = 2", + "current_goal_predicate": "=", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "events": [ [ "Assign", "X3 := 2" ] ] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "step_id": 9, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 2) :- (A0 = 1), (A1 = 2), (A0 = A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 3, + "column": 0, + "character": 22 + } + ] + } + ], + "step_id": 7, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 10, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 12, + "current_goal_text": "1 = 2", + "current_goal_predicate": "=", + "failed_attempts": [ + { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "events": [ [ "Fail", "unify 1 with 2" ] ] + } + ], + "successful_attempts": [], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "step_id": 10, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1 2) :- (A0 = 1), (A1 = 2), (A0 = A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 3, + "column": 0, + "character": 22 + } + ] + } + ], + "step_id": 7, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(A0 ; _) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 28, + "column": 0, + "character": 296 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 11, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 5, + "current_goal_text": "p 1 X0 ; p 2 X1", + "current_goal_predicate": ";", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(_ ; A0) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 30, + "column": 0, + "character": 311 + } + ] + } + ], + "events": [ [ "Assign", "A0 := p 2 X1" ] ] + }, + "siblings": [ { "goal_text": "p 2 X1", "goal_id": 13 } ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(_ ; A0) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 30, + "column": 0, + "character": 311 + } + ] + } + ], + "step_id": 11, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 12, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 13, + "current_goal_text": "p 2 X1", + "current_goal_predicate": "p", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(p 2 3) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 4, + "column": 0, + "character": 52 + } + ] + } + ], + "events": [ [ "Assign", "X1 := 3" ] ] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(p 2 3) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 4, + "column": 0, + "character": 52 + } + ] + } + ], + "step_id": 12, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(_ ; A0) :- A0.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 30, + "column": 0, + "character": 311 + } + ] + } + ], + "step_id": 11, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (p 1 A0 ; p 2 A1).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace.elpi", + "line": 6, + "column": 0, + "character": 60 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + } +] diff --git a/tests/sources/trace.elpi b/tests/sources/trace.elpi new file mode 100644 index 000000000..3474ca357 --- /dev/null +++ b/tests/sources/trace.elpi @@ -0,0 +1,7 @@ + +p 1 1 :- 1 is 2 + 3. +p 1 2 :- X = 1, Y = 2, X = Y. +p 2 3. + +main :- + p 1 X ; p 2 Y. \ No newline at end of file diff --git a/tests/sources/trace.json b/tests/sources/trace.json new file mode 100644 index 000000000..b74e2245c --- /dev/null +++ b/tests/sources/trace.json @@ -0,0 +1,85 @@ +{"step" : 0,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["main"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["main","main"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace.elpi\", line 6, column 0, character 60:"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace.elpi\", line 6, column 0, character 60:","main :- (p 1 A0 ; p 2 A1)."]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["5"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["p 1 X0 ; p 2 X1"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : [";","p 1 X0 ; p 2 X1"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 28, column 0, character 296:","File \"builtin.elpi\", line 30, column 0, character 311:"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 28, column 0, character 296:","(A0 ; _) :- A0."]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := p 1 X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["6"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["p 1 X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["p","p 1 X0"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace.elpi\", line 2, column 0, character 1:","File \"tests/sources/trace.elpi\", line 3, column 0, character 22:"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace.elpi\", line 2, column 0, character 1:","(p 1 1) :- (1 is 2 + 3)."]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X0 := 1"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["7"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["1 is 2 + 3"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["is","1 is 2 + 3"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 77, column 0, character 1165:"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 77, column 0, character 1165:","(A0 is A1) :- (calc A1 A0)."]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := 1"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A1 := 2 + 3"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["8"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["calc (2 + 3) 1"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["calc","calc (2 + 3) 1"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule","payload" : ["builtin"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["calc"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["9"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["1 = 5"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=","1 = 5"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule","payload" : ["eq"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["="]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:backchain:fail-to","payload" : ["unify 1 with 5"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:eq","payload" : ["fail"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["p","p 1 X0"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace.elpi\", line 3, column 0, character 22:"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace.elpi\", line 3, column 0, character 22:","(p 1 2) :- (A0 = 1), (A1 = 2), (A0 = A1)."]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X0 := 2"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["10"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["X2 = 1"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["11"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["X3 = 2"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["12"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["X2 = X3"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=","X2 = 1"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:rule","payload" : ["eq"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["="]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X2 := 1"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:rule:eq","payload" : ["success"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=","X3 = 2"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:rule","payload" : ["eq"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["="]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X3 := 2"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:rule:eq","payload" : ["success"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=","1 = 2"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:rule","payload" : ["eq"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["="]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:backchain:fail-to","payload" : ["unify 1 with 2"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:rule:eq","payload" : ["fail"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : [";","p 1 X0 ; p 2 X1"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 30, column 0, character 311:"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 30, column 0, character 311:","(_ ; A0) :- A0."]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := p 2 X1"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["13"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["p 2 X1"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["p","p 2 X1"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace.elpi\", line 4, column 0, character 52:"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace.elpi\", line 4, column 0, character 52:","(p 2 3) :- ."]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X1 := 3"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} diff --git a/tests/sources/trace2.elab.json b/tests/sources/trace2.elab.json new file mode 100644 index 000000000..9ce65c2ed --- /dev/null +++ b/tests/sources/trace2.elab.json @@ -0,0 +1,388 @@ +[ + { + "step_id": 0, + "runtime_id": 0, + "step": [ "Init", { "goal_text": "main", "goal_id": 4 } ], + "color": "Grey" + }, + { + "step_id": 1, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 4, + "current_goal_text": "main", + "current_goal_predicate": "main", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "main :- (print 1), (fail => (true , fail)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace2.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "events": [] + }, + "siblings": [ + { "goal_text": "print 1", "goal_id": 5 }, + { "goal_text": "fail => (true , fail)", "goal_id": 6 } + ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (print 1), (fail => (true , fail)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace2.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 2, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 5, + "current_goal_text": "print 1", + "current_goal_predicate": "print", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "FFI", "print" ] ], + "events": [] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "FFI", "print" ] ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (print 1), (fail => (true , fail)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace2.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 3, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 6, + "current_goal_text": "fail => (true , fail)", + "current_goal_predicate": "=>", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "Logic", "implication" ] ], + "events": [] + }, + "siblings": [ { "goal_text": "true , fail", "goal_id": 7 } ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "implication" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (print 1), (fail => (true , fail)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace2.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 4, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 7, + "current_goal_text": "true , fail", + "current_goal_predicate": ",", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "Logic", "and" ] ], + "events": [] + }, + "siblings": [ + { "goal_text": "fail", "goal_id": 8 }, + { "goal_text": "true", "goal_id": 9 } + ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "and" ] ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "implication" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (print 1), (fail => (true , fail)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace2.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 5, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 9, + "current_goal_text": "true", + "current_goal_predicate": "true", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "true :- .", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 9, + "column": 0, + "character": 89 + } + ] + } + ], + "events": [] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "true :- .", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 9, + "column": 0, + "character": 89 + } + ] + } + ], + "step_id": 5, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "and" ] ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "implication" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (print 1), (fail => (true , fail)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace2.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 6, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 8, + "current_goal_text": "fail", + "current_goal_predicate": "fail", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { "rule_text": "fail :- .", "rule_loc": [ "Context", 3 ] } + ], + "events": [] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { "rule_text": "fail :- .", "rule_loc": [ "Context", 3 ] } + ], + "step_id": 6, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "and" ] ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "implication" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (print 1), (fail => (true , fail)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace2.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + } +] diff --git a/tests/sources/trace2.elpi b/tests/sources/trace2.elpi new file mode 100644 index 000000000..8058a319f --- /dev/null +++ b/tests/sources/trace2.elpi @@ -0,0 +1,2 @@ +main :- + print 1, (fail => (true, fail)). \ No newline at end of file diff --git a/tests/sources/trace2.json b/tests/sources/trace2.json new file mode 100644 index 000000000..e8e402852 --- /dev/null +++ b/tests/sources/trace2.json @@ -0,0 +1,36 @@ +{"step" : 0,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["main"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["main","main"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace2.elpi\", line 1, column 0, character 0:"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace2.elpi\", line 1, column 0, character 0:","main :- (print 1), (fail => (true , fail))."]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["5"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["print 1"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["6"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["fail => (true , fail)"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["print","print 1"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["builtin"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["print"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=>","fail => (true , fail)"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule","payload" : ["implication"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["7"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["true , fail"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:implication","payload" : ["success"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:curgoal","payload" : [",","true , fail"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule","payload" : ["and"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["8"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["fail"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["9"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["true"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:and","payload" : ["success"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["true","true"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 9, column 0, character 89:"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 9, column 0, character 89:","true :- ."]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["fail","fail"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"(context step_id:3)\", line 1, column 0, character 0:"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"(context step_id:3)\", line 1, column 0, character 0:","fail :- ."]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} diff --git a/tests/sources/trace_chr.elab.json b/tests/sources/trace_chr.elab.json new file mode 100644 index 000000000..cbb543d81 --- /dev/null +++ b/tests/sources/trace_chr.elab.json @@ -0,0 +1,1398 @@ +[ + { + "step_id": 0, + "runtime_id": 0, + "step": [ "Init", { "goal_text": "main", "goal_id": 4 } ], + "color": "Grey" + }, + { + "step_id": 1, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 4, + "current_goal_text": "main", + "current_goal_predicate": "main", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "events": [] + }, + "siblings": [ + { "goal_text": "even X0", "goal_id": 5 }, + { "goal_text": "declare_constraint true X0", "goal_id": 6 }, + { "goal_text": "X0 = s X1", "goal_id": 7 }, + { "goal_text": "not (even X1)", "goal_id": 8 } + ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 2, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 5, + "current_goal_text": "even X0", + "current_goal_predicate": "even", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "events": [ [ "Assign", "A0 := X0" ] ] + }, + "siblings": [ + { + "goal_text": "declare_constraint (even X0) X0", + "goal_id": 9 + } + ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 3, + "runtime_id": 0, + "step": [ + "Suspend", + { + "suspend_goal_id": 9, + "suspend_goal_text": "declare_constraint (even X0) X0", + "suspend_sibling": { "goal_text": "even X0", "goal_id": 10 }, + "suspend_stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "suspend" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Grey" + }, + { + "step_id": 4, + "runtime_id": 0, + "step": [ + "Suspend", + { + "suspend_goal_id": 6, + "suspend_goal_text": "declare_constraint true X0", + "suspend_sibling": { "goal_text": "true", "goal_id": 11 }, + "suspend_stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "suspend" ] ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Grey" + }, + { + "step_id": 5, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 7, + "current_goal_text": "X0 = s X1", + "current_goal_predicate": "=", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "events": [ + [ "Assign", "X0 := s X1" ], + [ "ResumeGoal", [ 11, 10 ] ] + ] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], + "step_id": 5, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 6, + "runtime_id": 0, + "step": [ + "Resume", + [ + { "goal_text": "true", "goal_id": 11 }, + { "goal_text": "even X0", "goal_id": 10 } + ] + ], + "color": "Grey" + }, + { + "step_id": 7, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 11, + "current_goal_text": "true", + "current_goal_predicate": "true", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "true :- .", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 9, + "column": 0, + "character": 89 + } + ] + } + ], + "events": [] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "true :- .", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 9, + "column": 0, + "character": 89 + } + ] + } + ], + "step_id": 7, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "resume" ] ], + "step_id": 6, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "suspend" ] ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 8, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 10, + "current_goal_text": "even (s X1)", + "current_goal_predicate": "even", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(even (s A0)) :- (odd A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 14, + "column": 0, + "character": 230 + } + ] + } + ], + "events": [ [ "Assign", "A0 := X1" ] ] + }, + "siblings": [ { "goal_text": "odd X1", "goal_id": 12 } ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(even (s A0)) :- (odd A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 14, + "column": 0, + "character": 230 + } + ] + } + ], + "step_id": 8, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "resume" ] ], + "step_id": 6, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "suspend" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 9, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 12, + "current_goal_text": "odd X1", + "current_goal_predicate": "odd", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": + "(odd (as uvar A0)) :- (declare_constraint (odd A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 17, + "column": 0, + "character": 303 + } + ] + } + ], + "events": [ [ "Assign", "A0 := X1" ] ] + }, + "siblings": [ + { + "goal_text": "declare_constraint (odd X1) X1", + "goal_id": 13 + } + ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": + "(odd (as uvar A0)) :- (declare_constraint (odd A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 17, + "column": 0, + "character": 303 + } + ] + } + ], + "step_id": 9, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(even (s A0)) :- (odd A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 14, + "column": 0, + "character": 230 + } + ] + } + ], + "step_id": 8, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "resume" ] ], + "step_id": 6, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "suspend" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 10, + "runtime_id": 0, + "step": [ + "Suspend", + { + "suspend_goal_id": 13, + "suspend_goal_text": "declare_constraint (odd X1) X1", + "suspend_sibling": { "goal_text": "odd X1", "goal_id": 14 }, + "suspend_stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "suspend" ] ], + "step_id": 10, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "(odd (as uvar A0)) :- (declare_constraint (odd A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 17, + "column": 0, + "character": 303 + } + ] + } + ], + "step_id": 9, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(even (s A0)) :- (odd A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 14, + "column": 0, + "character": 230 + } + ] + } + ], + "step_id": 8, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "resume" ] ], + "step_id": 6, + "runtime_id": 0 + }, + { + "rule": [ "BuiltinRule", [ "Logic", "suspend" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Grey" + }, + { + "step_id": 11, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 8, + "current_goal_text": "not (even X1)", + "current_goal_predicate": "not", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(not A0) :- A0, (!), fail.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 52, + "column": 0, + "character": 609 + } + ] + } + ], + "events": [ [ "Assign", "A0 := even X1" ] ] + }, + "siblings": [ + { "goal_text": "even X1", "goal_id": 15 }, + { "goal_text": "!", "goal_id": 16 }, + { "goal_text": "fail", "goal_id": 17 } + ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [ 17 ], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(not A0) :- A0, (!), fail.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 52, + "column": 0, + "character": 609 + } + ] + } + ], + "step_id": 11, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "YellowGreen" + }, + { + "step_id": 12, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 15, + "current_goal_text": "even X1", + "current_goal_predicate": "even", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "events": [ [ "Assign", "A0 := X1" ] ] + }, + "siblings": [ + { + "goal_text": "declare_constraint (even X1) X1", + "goal_id": 18 + } + ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "step_id": 12, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(not A0) :- A0, (!), fail.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 52, + "column": 0, + "character": 609 + } + ] + } + ], + "step_id": 11, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 13, + "runtime_id": 0, + "step": [ + "Suspend", + { + "suspend_goal_id": 18, + "suspend_goal_text": "declare_constraint (even X1) X1", + "suspend_sibling": { "goal_text": "even X1", "goal_id": 19 }, + "suspend_stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "suspend" ] ], + "step_id": 13, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "(even (as uvar A0)) :- (declare_constraint (even A0) A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 16, + "column": 0, + "character": 252 + } + ] + } + ], + "step_id": 12, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(not A0) :- A0, (!), fail.", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 52, + "column": 0, + "character": 609 + } + ] + } + ], + "step_id": 11, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Grey" + }, + { + "step_id": 14, + "runtime_id": 0, + "step": [ + "CHR", + { + "chr_failed_attempts": [ + { + "chr_text": " \\ (even A0) (odd A0) | (odd z) <=> (true)", + "chr_loc": { + "filename": "tests/sources/trace_chr.elpi", + "line": 2, + "column": 3, + "character": 25 + }, + "chr_condition_cards": [ + { + "step_id": 0, + "runtime_id": 1, + "step": [ "Init", { "goal_text": "odd z", "goal_id": 21 } ], + "color": "Grey" + }, + { + "step_id": 1, + "runtime_id": 1, + "step": [ + "Inference", + { + "current_goal_id": 21, + "current_goal_text": "odd z", + "current_goal_predicate": "odd", + "failed_attempts": [], + "successful_attempts": [], + "more_successful_attempts": [], + "stack": [] + } + ], + "color": "Red" + } + ] + } + ], + "chr_successful_attempts": [ + { + "chr_attempt": { + "chr_text": " \\ (even A0) (odd A0) | (odd (s z)) <=> (fail)", + "chr_loc": { + "filename": "tests/sources/trace_chr.elpi", + "line": 3, + "column": 3, + "character": 71 + }, + "chr_condition_cards": [ + { + "step_id": 0, + "runtime_id": 2, + "step": [ + "Init", + { "goal_text": "odd (s z)", "goal_id": 23 } + ], + "color": "Grey" + }, + { + "step_id": 1, + "runtime_id": 2, + "step": [ + "Inference", + { + "current_goal_id": 23, + "current_goal_text": "odd (s z)", + "current_goal_predicate": "odd", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(odd (s A0)) :- (even A0).", + "rule_loc": [ + "File", + { + "filename": + "tests/sources/trace_chr.elpi", + "line": 13, + "column": 0, + "character": 209 + } + ] + } + ], + "events": [ [ "Assign", "A0 := z" ] ] + }, + "siblings": [ + { "goal_text": "even z", "goal_id": 24 } + ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(odd (s A0)) :- (even A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 13, + "column": 0, + "character": 209 + } + ] + } + ], + "step_id": 1, + "runtime_id": 2 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 2, + "runtime_id": 2, + "step": [ + "Inference", + { + "current_goal_id": 24, + "current_goal_text": "even z", + "current_goal_predicate": "even", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(even z) :- .", + "rule_loc": [ + "File", + { + "filename": + "tests/sources/trace_chr.elpi", + "line": 11, + "column": 0, + "character": 200 + } + ] + } + ], + "events": [] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(even z) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 11, + "column": 0, + "character": 200 + } + ] + } + ], + "step_id": 2, + "runtime_id": 2 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(odd (s A0)) :- (even A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 13, + "column": 0, + "character": 209 + } + ] + } + ], + "step_id": 1, + "runtime_id": 2 + } + ] + } + ], + "color": "Green" + } + ] + }, + "chr_removed_goals": [ 19, 14 ], + "chr_new_goals": [ { "goal_text": "_ => fail", "goal_id": 25 } ] + } + ], + "chr_store_before": [ + { "goal_text": " even X1 /* suspended on X1 */", "goal_id": 19 }, + { "goal_text": " odd X1 /* suspended on X1 */", "goal_id": 14 } + ], + "chr_store_after": [] + } + ], + "color": "Grey" + }, + { + "step_id": 15, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 25, + "current_goal_text": "_ => fail", + "current_goal_predicate": "=>", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "Logic", "implication" ] ], + "events": [] + }, + "siblings": [ { "goal_text": "fail", "goal_id": 26 } ], + "siblings_aggregated_outcome": "Fail" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "implication" ] ], + "step_id": 15, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 16, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 26, + "current_goal_text": "fail", + "current_goal_predicate": "fail", + "failed_attempts": [], + "successful_attempts": [], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "Logic", "implication" ] ], + "step_id": 15, + "runtime_id": 0 + } + ] + } + ], + "color": "Red" + }, + { + "step_id": 17, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 8, + "current_goal_text": "not (even X1)", + "current_goal_predicate": "not", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(not _) :- .", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 54, + "column": 0, + "character": 631 + } + ] + } + ], + "events": [] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(not _) :- .", + "rule_loc": [ + "File", + { + "filename": "builtin.elpi", + "line": 54, + "column": 0, + "character": 631 + } + ] + } + ], + "step_id": 17, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1)).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_chr.elpi", + "line": 19, + "column": 0, + "character": 353 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + } +] diff --git a/tests/sources/trace_chr.elpi b/tests/sources/trace_chr.elpi new file mode 100644 index 000000000..a712a3411 --- /dev/null +++ b/tests/sources/trace_chr.elpi @@ -0,0 +1,24 @@ +constraint even odd { + rule \ (even X) (odd X) | (odd z) <=> true. + rule \ (even X) (odd X) | (odd (s z)) <=> fail. +} +kind nat type. +type s nat -> nat. +type z nat. + +pred even i:nat. +pred odd i:nat. +even z. + +odd (s X) :- even X. +even (s X) :- odd X. + +even (uvar as X) :- declare_constraint (even X) X. +odd (uvar as X) :- declare_constraint (odd X) X. + +main :- + even Z, + declare_constraint true Z, + Z = s W, + not(even W). + diff --git a/tests/sources/trace_chr.json b/tests/sources/trace_chr.json new file mode 100644 index 000000000..a9099306a --- /dev/null +++ b/tests/sources/trace_chr.json @@ -0,0 +1,144 @@ +{"step" : 0,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["main"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["main","main"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 19, column 0, character 353:"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 19, column 0, character 353:","main :- (even A0), (declare_constraint true A0), (A0 = s A1), \n (not (even A1))."]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["5"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["even X0"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["6"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["declare_constraint true X0"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["7"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["X0 = s X1"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["8"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["not (even X1)"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["even","even X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 16, column 0, character 252:"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 16, column 0, character 252:","(even (as uvar A0)) :- (declare_constraint (even A0) A0)."]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["9"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["declare_constraint (even X0) X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["declare_constraint","declare_constraint (even X0) X0"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule","payload" : ["builtin"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["declare_constraint"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["10"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["even X0"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["declare_constraint","declare_constraint true X0"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule","payload" : ["builtin"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["declare_constraint"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["11"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["true"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=","X0 = s X1"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule","payload" : ["eq"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["="]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X0 := s X1"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign:resume","payload" : ["11 10"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:eq","payload" : ["success"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:rule","payload" : ["resume"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:rule:resume:resumed","payload" : ["true"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:rule:resume:resumed","payload" : ["even (s X1)"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:rule:resume","payload" : ["success"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["true","true"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 9, column 0, character 89:"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 9, column 0, character 89:","true :- ."]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 11,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["even","even (s X1)"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 14, column 0, character 230:"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 14, column 0, character 230:","(even (s A0)) :- (odd A0)."]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := X1"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["12"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["odd X1"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["odd","odd X1"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 17, column 0, character 303:"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 17, column 0, character 303:","(odd (as uvar A0)) :- (declare_constraint (odd A0) A0)."]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := X1"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["13"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["declare_constraint (odd X1) X1"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["declare_constraint","declare_constraint (odd X1) X1"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule","payload" : ["builtin"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["declare_constraint"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["14"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 14,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["odd X1"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["not","not (even X1)"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 52, column 0, character 609:","File \"builtin.elpi\", line 54, column 0, character 631:"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 52, column 0, character 609:","(not A0) :- A0, (!), fail."]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := even X1"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["15"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["even X1"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["16"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 16,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["!"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["17"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 17,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["fail"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["even","even X1"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 16, column 0, character 252:"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 16, column 0, character 252:","(even (as uvar A0)) :- (declare_constraint (even A0) A0)."]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := X1"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 15,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["18"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["declare_constraint (even X1) X1"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["declare_constraint","declare_constraint (even X1) X1"]} +{"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:rule","payload" : ["builtin"]} +{"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["declare_constraint"]} +{"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["19"]} +{"step" : 13,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["even X1"]} +{"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 2, column 3, character 25:"," \\ (even A0) (odd A0) | (odd z) <=> (true)"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--479 []"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["odd z"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["odd","odd z"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : []} +{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["fail"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:rule-failed","payload" : []} +{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 3, column 3, character 71:"," \\ (even A0) (odd A0) | (odd (s z)) <=> (fail)"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--480 []"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["odd (s z)"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["odd","odd (s z)"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 13, column 0, character 209:"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 13, column 0, character 209:","(odd (s A0)) :- (even A0)."]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := z"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:subgoal","payload" : ["24"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["even z"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["even","even z"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_chr.elpi\", line 11, column 0, character 200:"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 11, column 0, character 200:","(even z) :- ."]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 24,"runtime_id" : 2,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["25"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["_ => fail"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:rule-fired","payload" : ["File \"tests/sources/trace_chr.elpi\", line 3, column 3, character 71:"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:rule-remove-constraints","payload" : ["19","14"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:store:before","payload" : ["19"," even X1 /* suspended on X1 */"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:store:before","payload" : ["14"," odd X1 /* suspended on X1 */"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:rule","payload" : ["resume"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:rule:resume:resumed","payload" : ["_ => fail"]} +{"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:rule:resume","payload" : ["success"]} +{"step" : 15,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=>","_ => fail"]} +{"step" : 15,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:rule","payload" : ["implication"]} +{"step" : 15,"kind" : ["Info"],"goal_id" : 25,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["26"]} +{"step" : 15,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["fail"]} +{"step" : 15,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:rule:implication","payload" : ["success"]} +{"step" : 16,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["fail","fail"]} +{"step" : 16,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 16,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : []} +{"step" : 16,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["fail"]} +{"step" : 17,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["not","not (even X1)"]} +{"step" : 17,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 17,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 54, column 0, character 631:"]} +{"step" : 17,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 54, column 0, character 631:","(not _) :- ."]} +{"step" : 17,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} diff --git a/tests/sources/trace_findall.elab.json b/tests/sources/trace_findall.elab.json new file mode 100644 index 000000000..f96f0bd6b --- /dev/null +++ b/tests/sources/trace_findall.elab.json @@ -0,0 +1,534 @@ +[ + { + "step_id": 0, + "runtime_id": 0, + "step": [ "Init", { "goal_text": "main", "goal_id": 4 } ], + "color": "Grey" + }, + { + "step_id": 1, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 4, + "current_goal_text": "main", + "current_goal_predicate": "main", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "main :- (std.findall (p _) A0), (print A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 5, + "column": 0, + "character": 23 + } + ] + } + ], + "events": [] + }, + "siblings": [ + { "goal_text": "std.findall (p _) X0", "goal_id": 5 }, + { "goal_text": "print X0", "goal_id": 6 } + ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (std.findall (p _) A0), (print A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 5, + "column": 0, + "character": 23 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 2, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 5, + "current_goal_text": "std.findall (p _) X0", + "current_goal_predicate": "std.findall", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": + "(std.findall A0 A1) :- (findall_solutions A0 A1).", + "rule_loc": [ + "File", + { + "filename": "builtin_stdlib.elpi", + "line": 283, + "column": 0, + "character": 9378 + } + ] + } + ], + "events": [ + [ "Assign", "A0 := p _" ], + [ "Assign", "A1 := X0" ] + ] + }, + "siblings": [ + { "goal_text": "findall_solutions (p _) X0", "goal_id": 7 } + ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": + "(std.findall A0 A1) :- (findall_solutions A0 A1).", + "rule_loc": [ + "File", + { + "filename": "builtin_stdlib.elpi", + "line": 283, + "column": 0, + "character": 9378 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (std.findall (p _) A0), (print A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 5, + "column": 0, + "character": 23 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 3, + "runtime_id": 0, + "step": [ + "Findall", + { + "findall_goal_id": 7, + "findall_goal_text": "findall_solutions (p _) X0", + "findall_cards": [ + { + "step_id": 0, + "runtime_id": 1, + "step": [ "Init", { "goal_text": "p X0", "goal_id": 9 } ], + "color": "Grey" + }, + { + "step_id": 1, + "runtime_id": 1, + "step": [ + "Inference", + { + "current_goal_id": 9, + "current_goal_text": "p X0", + "current_goal_predicate": "p", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(p 1) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "events": [ [ "Assign", "X0 := 1" ] ] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [ 2, 3 ], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(p 1) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 1, + "column": 0, + "character": 0 + } + ] + } + ], + "step_id": 1, + "runtime_id": 1 + } + ] + } + ], + "color": "YellowGreen" + }, + { + "step_id": 2, + "runtime_id": 1, + "step": [ + "Inference", + { + "current_goal_id": 9, + "current_goal_text": "p X0", + "current_goal_predicate": "p", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(p 2) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 2, + "column": 0, + "character": 5 + } + ] + } + ], + "events": [ [ "Assign", "X0 := 2" ] ] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [ 3 ], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(p 2) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 2, + "column": 0, + "character": 5 + } + ] + } + ], + "step_id": 2, + "runtime_id": 1 + } + ] + } + ], + "color": "YellowGreen" + }, + { + "step_id": 3, + "runtime_id": 1, + "step": [ + "Inference", + { + "current_goal_id": 9, + "current_goal_text": "p X0", + "current_goal_predicate": "p", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(p 3) :- (p 2).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 3, + "column": 0, + "character": 10 + } + ] + } + ], + "events": [ [ "Assign", "X0 := 3" ] ] + }, + "siblings": [ { "goal_text": "p 2", "goal_id": 10 } ], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(p 3) :- (p 2).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 3, + "column": 0, + "character": 10 + } + ] + } + ], + "step_id": 3, + "runtime_id": 1 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 4, + "runtime_id": 1, + "step": [ + "Inference", + { + "current_goal_id": 10, + "current_goal_text": "p 2", + "current_goal_predicate": "p", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ + "UserRule", + { + "rule_text": "(p 2) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 2, + "column": 0, + "character": 5 + } + ] + } + ], + "events": [] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ + "UserRule", + { + "rule_text": "(p 2) :- .", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 2, + "column": 0, + "character": 5 + } + ] + } + ], + "step_id": 4, + "runtime_id": 1 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "(p 3) :- (p 2).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 3, + "column": 0, + "character": 10 + } + ] + } + ], + "step_id": 3, + "runtime_id": 1 + } + ] + } + ], + "color": "Green" + } + ], + "findall_solution_text": [ "X0 := [p 1, p 2, p 3]" ], + "findall_stack": [ + { + "rule": [ "BuiltinRule", [ "FFI", "findall" ] ], + "step_id": 3, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": + "(std.findall A0 A1) :- (findall_solutions A0 A1).", + "rule_loc": [ + "File", + { + "filename": "builtin_stdlib.elpi", + "line": 283, + "column": 0, + "character": 9378 + } + ] + } + ], + "step_id": 2, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (std.findall (p _) A0), (print A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 5, + "column": 0, + "character": 23 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + }, + { + "step_id": 4, + "runtime_id": 0, + "step": [ + "Inference", + { + "current_goal_id": 6, + "current_goal_text": "print [p 1, p 2, p 3]", + "current_goal_predicate": "print", + "failed_attempts": [], + "successful_attempts": [ + { + "attempt": { + "rule": [ "BuiltinRule", [ "FFI", "print" ] ], + "events": [] + }, + "siblings": [], + "siblings_aggregated_outcome": "Success" + } + ], + "more_successful_attempts": [], + "stack": [ + { + "rule": [ "BuiltinRule", [ "FFI", "print" ] ], + "step_id": 4, + "runtime_id": 0 + }, + { + "rule": [ + "UserRule", + { + "rule_text": "main :- (std.findall (p _) A0), (print A0).", + "rule_loc": [ + "File", + { + "filename": "tests/sources/trace_findall.elpi", + "line": 5, + "column": 0, + "character": 23 + } + ] + } + ], + "step_id": 1, + "runtime_id": 0 + } + ] + } + ], + "color": "Green" + } +] diff --git a/tests/sources/trace_findall.elpi b/tests/sources/trace_findall.elpi new file mode 100644 index 000000000..5761c0edc --- /dev/null +++ b/tests/sources/trace_findall.elpi @@ -0,0 +1,6 @@ +p 1. +p 2. +p 3 :- p 2. + +main :- + std.findall (p _) L, print L. \ No newline at end of file diff --git a/tests/sources/trace_findall.json b/tests/sources/trace_findall.json new file mode 100644 index 000000000..329055aba --- /dev/null +++ b/tests/sources/trace_findall.json @@ -0,0 +1,53 @@ +{"step" : 0,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["main"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["main","main"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 5, column 0, character 23:"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 5, column 0, character 23:","main :- (std.findall (p _) A0), (print A0)."]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["5"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["std.findall (p _) X0"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["6"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["print X0"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["std.findall","std.findall (p _) X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin_stdlib.elpi\", line 283, column 0, character 9378:"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin_stdlib.elpi\", line 283, column 0, character 9378:","(std.findall A0 A1) :- (findall_solutions A0 A1)."]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := p _"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A1 := X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["7"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["findall_solutions (p _) X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["findall_solutions","findall_solutions (p _) X0"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule","payload" : ["findall"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["p X0"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 1, column 0, character 0:","File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 1, column 0, character 0:","(p 1) :- ."]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X0 := 1"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","(p 2) :- ."]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X0 := 2"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p X0"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 3, column 0, character 10:","(p 3) :- (p 2)."]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X0 := 3"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 9,"runtime_id" : 1,"name" : "user:subgoal","payload" : ["10"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["p 2"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["p","p 2"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace_findall.elpi\", line 2, column 0, character 5:","(p 2) :- ."]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 10,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["success"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X0 := [p 1, p 2, p 3]"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:findall","payload" : ["success"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["print","print [p 1, p 2, p 3]"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule","payload" : ["builtin"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["print"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]} diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml index b9105aeb2..ff28a01df 100644 --- a/tests/suite/elpi_specific.ml +++ b/tests/suite/elpi_specific.ml @@ -289,3 +289,61 @@ let () = declare "IO_COLON" ~description:"IO_COLON token" ~typecheck:true () + +let () = declare "trace-browser" + ~source_elpi:"trace.elpi" + ~description:"trace generation" + ~typecheck:false + ~trace:(On["json";"/tmp/trace.json.new";"-trace-at";"0";"99";"-trace-only";"user"]) + ~expectation:(SuccessOutputFile { sample = "/tmp/trace.json.new"; adjust = Util.strip_cwd; reference = "trace.json" }) + () + +let () = declare "trace-browser-elab" + ~source_json:"trace.json" + ~description:"trace elaboration" + ~expectation:(SuccessOutputFile { sample = "/tmp/trace.elab.json.new"; adjust = Util.strip_cwd; reference = "trace.elab.json" }) + () + + + +let () = declare "trace-browser2" + ~source_elpi:"trace2.elpi" + ~description:"trace generation" + ~typecheck:false + ~trace:(On["json";"/tmp/trace2.json.new";"-trace-at";"0";"99";"-trace-only";"user"]) + ~expectation:(SuccessOutputFile { sample = "/tmp/trace2.json.new"; adjust = Util.strip_cwd; reference = "trace2.json" }) + () + + let () = declare "trace-browser2-elab" + ~source_json:"trace2.json" + ~description:"trace elaboration" + ~expectation:(SuccessOutputFile { sample = "/tmp/trace.elab.json.new"; adjust = Util.strip_cwd; reference = "trace2.elab.json" }) + () + +let () = declare "trace-browser-chr" + ~source_elpi:"trace_chr.elpi" + ~description:"trace generation" + ~typecheck:false + ~trace:(On["json";"/tmp/trace_chr.json.new";"-trace-at";"0";"99";"-trace-only";"user"]) + ~expectation:(SuccessOutputFile { sample = "/tmp/trace_chr.json.new"; adjust = Util.strip_cwd; reference = "trace_chr.json" }) + () + +let () = declare "trace-browser-elab-chr" + ~source_json:"trace_chr.json" + ~description:"trace elaboration" + ~expectation:(SuccessOutputFile { sample = "/tmp/trace_chr.elab.json.new"; adjust = Util.strip_cwd; reference = "trace_chr.elab.json" }) + () + +let () = declare "trace-browser-findall" + ~source_elpi:"trace_findall.elpi" + ~description:"trace generation" + ~typecheck:false + ~trace:(On["json";"/tmp/trace_findall.json.new";"-trace-at";"0";"99";"-trace-only";"user"]) + ~expectation:(SuccessOutputFile { sample = "/tmp/trace_findall.json.new"; adjust = Util.strip_cwd; reference = "trace_findall.json" }) + () + +let () = declare "trace-browser-elab-findall" + ~source_json:"trace_findall.json" + ~description:"trace elaboration" + ~expectation:(SuccessOutputFile { sample = "/tmp/trace_findall.elab.json.new"; adjust = Util.strip_cwd; reference = "trace_findall.elab.json" }) + () diff --git a/tests/suite/suite.ml b/tests/suite/suite.ml index 2bcda753e..a7c70d1f0 100644 --- a/tests/suite/suite.ml +++ b/tests/suite/suite.ml @@ -10,6 +10,7 @@ type expectation = | Failure | SuccessOutput of Str.regexp | FailureOutput of Str.regexp + | SuccessOutputFile of { sample : string; adjust : string -> string; reference : string } type trace = Off | On of string list @@ -21,6 +22,7 @@ type t = { source_teyjus : fname option; deps_teyjus : fname list; source_dune : fname option; + source_json : fname option; after: string list; typecheck : bool; input: fname option; @@ -33,7 +35,7 @@ type t = { let tests = ref [] let declare - name ~description ?source_elpi ?source_teyjus ?(deps_teyjus=[]) ?source_dune + name ~description ?source_elpi ?source_teyjus ?(deps_teyjus=[]) ?source_dune ?source_json ?after ?(typecheck=true) ?input ?(expectation=Success) ?(outside_llam=false) @@ -44,8 +46,8 @@ let declare = if List.exists (fun { name = x; _ } -> x = name) !tests then failwith ("a test named " ^ name ^ " already exists"); - begin match source_elpi, source_teyjus, source_dune with - | None, None, None -> failwith ("test "^name^" has no sources"); + begin match source_elpi, source_teyjus, source_dune, source_json with + | None, None, None, None-> failwith ("test "^name^" has no sources"); | _ -> () end; tests := { @@ -55,6 +57,7 @@ let declare source_teyjus; deps_teyjus; source_dune; + source_json; after = (match after with None -> [] | Some x -> [x]); typecheck; input; @@ -162,11 +165,14 @@ let open_log ~executable { Test.name; _ } = let name = logdir^"/"^Filename.basename executable^"+"^name^".log" in open_file_w name, name +let close_log (fd,_) = Unix.close fd + let open_dummy_log () = let name = Filename.temp_file "elpi" "txt" in open_file_w name, name -let write (fd,_) s = ignore(Unix.write_substring fd s 0 (String.length s)) +let write (fd,f) s = + ignore(Unix.write_substring fd s 0 (String.length s)) let open_input name = Unix.openfile name [Unix.O_RDONLY] 0 @@ -216,20 +222,20 @@ let wait pid timeout timelog = !rc -let fork_wait_win ~close_output exe argv env input output timefile timeout = +let fork_wait_win ~close_output exe argv env input output error timefile timeout = ignore close_output; let pid = Unix.create_process_env - exe (Array.of_list argv) env input output output in + exe (Array.of_list argv) env input output error in wait pid timeout timefile -let fork_wait_unix ~close_output exe argv env input output timefile timeout = +let fork_wait_unix ~close_output exe argv env input output error timefile timeout = let pid = Unix.fork () in if pid = 0 then begin let _ = Unix.setsid () in let runner = Unix.create_process_env - exe (Array.of_list argv) env input output output in + exe (Array.of_list argv) env input output error in let _, rc = Unix.waitpid [] runner in match rc with | Unix.WEXITED n -> exit n @@ -244,7 +250,7 @@ let fork_wait_unix ~close_output exe argv env input output timefile timeout = let null = if Sys.win32 then "NUL:" else "/dev/null" -let exec ~timeout ?timetool ~env ~log:(output,oname) ?(input=null) ~executable ~args ?(close_output=true) () = +let exec ~timeout ?timetool ~env ~log:(output,oname) ?(input=null) ?(error=output,oname) ~executable ~args ?(close_output=true) () = Sys.catch_break true; let exe, argv, timefile = match timetool with @@ -255,8 +261,8 @@ let exec ~timeout ?timetool ~env ~log:(output,oname) ?(input=null) ~executable ~ executable :: args), timefile in Unix.handle_unix_error (fun () -> let input = open_input input in - if Sys.win32 then fork_wait_win ~close_output exe argv env input output timefile timeout - else fork_wait_unix ~close_output exe argv env input output timefile timeout) + if Sys.win32 then fork_wait_win ~close_output exe argv env input output (fst error) timefile timeout + else fork_wait_unix ~close_output exe argv env input output (fst error) timefile timeout) () let with_log (_,log) f = @@ -269,13 +275,45 @@ let with_log (_,log) f = let option_map f = function None -> None | Some x -> Some (f x) +let strip_cwd file = + let name = Filename.temp_file "elpi" "txt" in + let oc = open_out name in + let ic = open_in file in + let rex = Str.regexp_string (Sys.getcwd () ^ "/") in + try + while true do + let l = input_line ic in + let l = Str.global_replace rex "" l in + output_string oc (l ^ "\n") + done; + name + with End_of_file -> + close_in ic; + close_out oc; + name + end +let match_file ~log file adjust reference = + let file = adjust file in + Util.write log (Printf.sprintf "Diffing %s against %s\n" file reference); + match + Util.exec ~timeout:5.0 ~env:(Unix.environment ()) + ~log ~close_output:false + ~executable:"diff" ~args:["-u";reference;file] () + with + | Util.Exit(0,_,_) -> true + | Util.Exit(n,_,_) -> + Util.write log (Printf.sprintf "Exit code: %d\n" n); + Util.write log (Printf.sprintf "Promotion: cp %s %s\n" file reference); + false + | _ -> false + module Elpi = struct let is_elpi = - let rex = Str.regexp "elpi.*" in + let rex = Str.regexp "\\(elpi\\|elpi\\.git\\..*\\)$" in fun s -> Str.string_match rex (Filename.basename s) 0 let read_time input_line = @@ -353,41 +391,77 @@ let () = Runner.declare Util.write log (Printf.sprintf "args: %s\n" (String.concat " " args)); let rc = - match expectation, Util.exec ~timeout ~timetool ?input ~executable ~env ~log ~args () with - | Test.Success, Util.Exit(0,walltime,mem) -> - Runner.Success { walltime; typechecking = Util.with_log log read_tctime; execution = Util.with_log log read_time; mem } - | Test.Failure, Util.Exit(0,walltime,mem) -> - Runner.Failure { walltime; typechecking = Util.with_log log read_tctime; execution = Util.with_log log read_time; mem } - | Test.Success, Util.Exit(_,walltime,mem) -> - Runner.Failure { walltime; typechecking = Util.with_log log read_tctime; execution = walltime; mem } - | Test.Failure, Util.Exit(_,walltime,mem) -> - Runner.Success { walltime; typechecking = Util.with_log log read_tctime; execution = Util.with_log log read_time; mem } - | Test.Success, Util.Timeout -> - Runner.Timeout timeout - | Test.Failure, Util.Timeout -> - Runner.Timeout timeout - | Test.FailureOutput _, Util.Exit(0,walltime,mem) -> - Runner.Failure { walltime; typechecking = Util.with_log log read_tctime; execution = walltime; mem } - | Test.SuccessOutput rex, Util.Exit(0,walltime,mem) -> - if Util.with_log log (match_rex rex) then - Runner.Success { walltime; typechecking = Util.with_log log read_tctime; execution = Util.with_log log read_time; mem } - else - Runner.Failure { walltime; typechecking = Util.with_log log read_tctime; execution = walltime; mem } - | Test.SuccessOutput _, Util.Exit(_,walltime,mem) -> - Runner.Failure { walltime; typechecking = Util.with_log log read_tctime; execution = walltime; mem } - | Test.FailureOutput rex, Util.Exit(_,walltime,mem) -> - if Util.with_log log (match_rex rex) then - Runner.Success { walltime; typechecking = Util.with_log log read_tctime; execution = Util.with_log log read_time; mem } - else - Runner.Failure { walltime; typechecking = Util.with_log log read_tctime; execution = walltime; mem } - | (Test.FailureOutput _ | Test.SuccessOutput _), Util.Timeout -> - Runner.Timeout timeout + let outcome = Util.exec ~timeout ~timetool ~close_output:false ?input ~executable ~env ~log ~args () in + let typechecking = Util.with_log log read_tctime in + let execution = Util.with_log log read_time in + + match outcome with + | Util.Exit(0,walltime,mem) -> + begin match expectation with + | Test.Success -> Runner.Success { walltime; typechecking; execution; mem } + | Test.SuccessOutput rex when Util.with_log log (match_rex rex) -> Runner.Success { walltime; typechecking; execution; mem } + | Test.SuccessOutputFile { sample; adjust; reference } when match_file ~log sample adjust (sources^"/"^reference) -> Runner.Success { walltime; typechecking; execution; mem } + | _ -> Runner.Failure { walltime; typechecking; execution; mem } + end + + | Util.Exit(_,walltime,mem) -> + begin match expectation with + | Test.Failure -> Runner.Success { walltime; typechecking; execution; mem } + | Test.FailureOutput rex when Util.with_log log (match_rex rex) -> Runner.Success { walltime; typechecking; execution; mem } + | _ -> Runner.Failure { walltime; typechecking; execution; mem } + end + + | Util.Timeout -> Runner.Timeout timeout + in + Util.close_log log; Runner.(Done { Runner.rc; executable; test; log = snd log }) end end +module ElpiTraceElab = struct + let is_elpi_elab = + let rex = Str.regexp "elpi-trace-elaborator" in + fun s -> Str.string_match rex (Filename.basename s) 0 + + let () = Runner.declare + ~applicable:(fun ~executable { Test.source_json; } -> + if is_elpi_elab executable && source_json <> None then + Runner.Can_run_it + else Runner.Not_for_me) + ~run:(fun ~executable ~timetool ~timeout ~env ~sources test -> + if not (Sys.file_exists executable) then Runner.Skipped + else + let log = Util.open_log ~executable test in + Util.write log (Printf.sprintf "executable: %s\n" executable); + let source = + match test.Test.source_json with Some x -> x | _ -> assert false in + let input = sources ^ source in + Util.write log (Printf.sprintf "input: %s\n" input); + let output_file = + match test.Test.expectation with + | Test.SuccessOutputFile { sample } -> Util.open_file_w sample, sample + | _ -> Printf.eprintf "ElpiTraceElab only supoprts SuccessOutputFile tests"; exit 1 in + let output_file_tmp = Util.open_dummy_log () in + Util.write log (Printf.sprintf "output: %s\n" (snd output_file)); + let log = Util.open_log ~executable test in + let outcome = Util.exec ~timeout ~timetool ~input ~executable ~env ~error:log ~log:output_file_tmp ~args:[] () in + let outcomey = Util.exec ~timeout ~timetool ~input:(snd output_file_tmp) ~executable:"ydump" ~env ~log:output_file ~args:[] () in + let typechecking = 0.0 in + let execution = 0.0 in + let rc = + match outcome, outcomey, test.Test.expectation with + | Util.Exit(0,walltime,mem), Util.Exit(0,_,_), Test.SuccessOutputFile { sample; adjust; reference } when match_file ~log sample adjust (sources^"/"^reference) -> + Runner.Success { walltime; typechecking; execution; mem } + | _ -> Runner.Failure { walltime = 0.0; typechecking; execution = 0.0; mem = 0 } + in + Util.close_log log; + Runner.(Done { Runner.rc; executable; test; log = snd log }) + ) + +end + module Teyjus = struct let assert_ok = function @@ -439,25 +513,25 @@ let is_tjsim = let args = ["-m";"1";"-b";"-s";"main.";"-p";dir^"/";modname] in Util.write log (Printf.sprintf "%s %s\n" executable (String.concat " " args)); - let rc = Util.exec ~timeout ~timetool ~executable ?input ~env ~log ~args ~close_output:false () in + let outcome = Util.exec ~timeout ~timetool ~executable ?input ~env ~log ~args ~close_output:false () in + let typechecking = 0.0 in let rc = - match expectation, rc with - | Test.Success, Util.Exit(0,walltime,mem) -> - Runner.Success { walltime; typechecking = 0.0; execution = walltime; mem } - | Test.Failure, Util.Exit(0,walltime,mem) -> - Runner.Failure { walltime; typechecking = 0.0; execution = walltime; mem } - | Test.Success, Util.Exit(_,walltime,mem) -> - Runner.Failure { walltime; typechecking = 0.0; execution = walltime; mem } - | Test.Failure, Util.Exit(_,walltime,mem) -> - Runner.Success { walltime; typechecking = 0.0; execution = walltime; mem } - | Test.Success, Util.Timeout -> - Runner.Timeout timeout - | Test.Failure, Util.Timeout -> - Runner.Timeout timeout - | (Test.SuccessOutput _ | Test.FailureOutput _), Util.Exit(_,walltime,mem) -> - Runner.Success { walltime; typechecking = 0.0; execution = walltime; mem } - | (Test.SuccessOutput _ | Test.FailureOutput _), Util.Timeout -> - Runner.Timeout timeout + + match outcome with + | Util.Exit(0,walltime,mem) -> let execution = walltime in + begin match expectation with + | Test.Success -> Runner.Success { walltime; typechecking; execution; mem } + | _ -> Runner.Failure { walltime; typechecking; execution; mem } + end + + | Util.Exit(_,walltime,mem) -> let execution = walltime in + begin match expectation with + | Test.Failure -> Runner.Success { walltime; typechecking; execution; mem } + | _ -> Runner.Failure { walltime; typechecking; execution; mem } + end + + | Util.Timeout -> Runner.Timeout timeout + in Runner.Done { Runner.rc; executable; test; log = snd log } end @@ -501,31 +575,25 @@ let () = Runner.declare let args = ["exec"; sources ^ "/" ^ source; "--"; "-I"; "src/"] in Util.write log (Printf.sprintf "args: %s\n" (String.concat " " args)); let rc = - match expectation, Util.exec ~timeout ~timetool ?input ~executable ~env ~log ~args () with - | Test.Success, Util.Exit(0,walltime,mem) -> - Runner.Success { walltime; typechecking = 0.0; execution = 0.0; mem } - | Test.Success, Util.Exit(_,walltime,mem)-> - Runner.Failure { walltime; typechecking = 0.0; execution = 0.0; mem } - | Test.Failure, Util.Exit(0,walltime,mem) -> - Runner.Failure { walltime; typechecking = 0.0; execution = 0.0; mem } - | Test.Failure, Util.Exit(_,walltime,mem)-> - Runner.Success { walltime; typechecking = 0.0; execution = 0.0; mem } - | Test.SuccessOutput rex, Util.Exit(0,walltime,mem) -> - if Util.with_log log (match_rex rex) then - Runner.Success { walltime; typechecking = 0.0; execution = 0.0; mem } - else - Runner.Failure { walltime; typechecking = 0.0; execution = walltime; mem } - | Test.FailureOutput _, Util.Exit(0,walltime,mem) -> - Runner.Failure { walltime; typechecking = 0.0; execution = walltime; mem } - | Test.SuccessOutput _, Util.Exit(_,walltime,mem) -> - Runner.Failure { walltime; typechecking = 0.0; execution = walltime; mem } - | Test.FailureOutput rex, Util.Exit(_,walltime,mem) -> - if Util.with_log log (match_rex rex) then - Runner.Success { walltime; typechecking = 0.0; execution = 0.0; mem } - else - Runner.Failure { walltime; typechecking = 0.0; execution = walltime; mem } - | _, Util.Timeout -> - Runner.Timeout timeout + let outcome = Util.exec ~timeout ~timetool ?input ~executable ~env ~log ~args () in + let typechecking = 0.0 in + match outcome with + | Util.Exit(0,walltime,mem) -> let execution = walltime in + begin match expectation with + | Test.Success -> Runner.Success { walltime; typechecking; execution; mem } + | Test.SuccessOutput rex when Util.with_log log (match_rex rex) -> Runner.Success { walltime; typechecking; execution; mem } + | _ -> Runner.Failure { walltime; typechecking; execution; mem } + end + + | Util.Exit(_,walltime,mem) -> let execution = walltime in + begin match expectation with + | Test.Failure -> Runner.Success { walltime; typechecking; execution; mem } + | Test.FailureOutput rex when Util.with_log log (match_rex rex) -> Runner.Success { walltime; typechecking; execution; mem } + | _ -> Runner.Failure { walltime; typechecking; execution; mem } + end + + | Util.Timeout -> Runner.Timeout timeout + in Runner.(Done { Runner.rc; executable; test; log = snd log }) diff --git a/tests/suite/suite.mli b/tests/suite/suite.mli index 62724e0c4..ecd3b4cf0 100644 --- a/tests/suite/suite.mli +++ b/tests/suite/suite.mli @@ -1,4 +1,10 @@ +module Util : sig + + val strip_cwd : string -> string + +end + module Test : sig type fname = string @@ -8,6 +14,7 @@ type expectation = | Failure | SuccessOutput of Str.regexp | FailureOutput of Str.regexp + | SuccessOutputFile of { sample : string; adjust : string -> string; reference : string } type trace = Off | On of string list @@ -18,6 +25,7 @@ val declare : ?source_teyjus:fname -> ?deps_teyjus:fname list -> ?source_dune:fname -> + ?source_json:fname -> ?after:string -> ?typecheck:bool -> ?input:fname -> @@ -36,6 +44,7 @@ type t = { source_teyjus : fname option; deps_teyjus : fname list; source_dune : fname option; + source_json : fname option; after : string list; typecheck : bool; input : fname option; diff --git a/tests/test.real.ml b/tests/test.real.ml index 2636e26e2..0b9c582bd 100644 --- a/tests/test.real.ml +++ b/tests/test.real.ml @@ -70,6 +70,8 @@ let print_log ~fname = printf [red] "------------------------------------------------------------------\n"; print_file fname; printf [red] "------------------------------------------------------------------\n"; + printf [blue] "End log of the first failure: "; printf [] "%s\n" fname; + printf [red] "------------------------------------------------------------------\n"; end diff --git a/trace.atd b/trace.atd new file mode 100644 index 000000000..59f262250 --- /dev/null +++ b/trace.atd @@ -0,0 +1,138 @@ +(* This file describes the format of the trace generated by elpi + and the format of the elaborate trace generated by elpi-trace-elaborator + + home: https://github.com/ahrefs/atd + doc: https://atd.readthedocs.io/en/latest/index.html + + +*) + +(* input: raw events *) + +type item = { + kind : kind list; + goal_id : int; + runtime_id : int; + step : int; + name : string; + payload : string list; +} +type kind = [ Start | Info | Stop of stop ] +type stop = { cause : string; time : float } +type raw_trace = item list + +(* **** output: cards to be displayed ************************************** *) + +type trace = card list + +(* Note: step_id + runtime_id form a unique identified for the card *) +type card = { + step_id : step_id; (* sequential, but local to the runtime *) + runtime_id : runtime_id; (* each runtime has an id, 0 for the main one *) + step : step; (* the computation step *) + color : color; +} + +type color = [ Red | Green | Grey | YellowGreen | YellowRed ] + +type step = + [ Inference of inference (* The goal is solved by a rule, most common case *) + | Findall of findall (* A sub runtime computes all solutions to a goal *) + | Cut of cut (* Some alternatives are dropped *) + | Suspend of suspend (* A new constraint is generated *) + | Resume of resume (* A constraint is resumed *) + | CHR of chr (* Some constraint handling rules fires *) + | Init of goal (* The initial goal is set *) + ] + +(* Inference step operates on a goal with a bunch of rules: first a bunch of + rules which fail, and then some which succeed. If no rule succeeds, then + the inference fails. If a rule succeeds, but some sibling fails, then + there may be more rules to be attempted later *) +type inference = { + current_goal_id : goal_id; + current_goal_text : goal_text; + current_goal_predicate : string; (* string to search/filter steps *) + failed_attempts : attempt list; + successful_attempts : successful_attempt list; + more_successful_attempts : step_id list; + stack : stack; +} + +type attempt = { + rule : rule; + events : event list; +} +type rule = [ BuiltinRule of builtin_name | UserRule of user_rule ] +type user_rule = { rule_text : rule_text; rule_loc : location } +type builtin_name = [ Logic of string | FFI of string ] +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] +type rule_text = string (* Todo: use a formattable data, e.g. box language *) + +type successful_attempt = { + attempt : attempt; + siblings : goal list; + siblings_aggregated_outcome : outcome; +} +type goal = { goal_text : string; goal_id : goal_id } +type outcome = [ Fail | Success ] + +type stack = frame list +type frame = { rule : rule; step_id : step_id; runtime_id : runtime_id } + +type goal_id = int +type step_id = int +type runtime_id = int +type goal_text = string (* Todo: use a formattable data, e.g. box language *) + + +(* Findall step *) +type findall = { + findall_goal_id : goal_id; + findall_goal_text : goal_text; + findall_cards : trace; (* The sub trace computing all solutions to the goal *) + findall_solution_text : solution_text; + findall_stack : stack; +} +type solution_text = string list (* Todo: use a formattable data, e.g. box language *) + +(* This goal generates a suspended sibling *) +type suspend = { + suspend_goal_id : goal_id; + suspend_goal_text : goal_text; + suspend_sibling : goal; + suspend_stack : stack; +} + +(* The ! operator eliminates some rules (for some goal) *) +type cut = cutted list +type cutted = { + cut_branch_for_goal : goal; + cut_branch : user_rule +} + +(* Resumption activaes suspended goals *) +type resume = goal list + +(* A CHR step is like an inference step, it is made of some failed and some + successful attempts. It acts on the store. *) +type chr = { + chr_failed_attempts : chr_attempt list; + chr_successful_attempts : successful_chr_attempt list; + chr_store_before : goal list; + chr_store_after : goal list; +} +type chr_attempt = { + chr_text : chr_text; (* the rule text *) + chr_loc : file_location; (* the rule loc *) + chr_condition_cards : trace; (* the rule has a condition, which is an elpi + program running in a dedicated runtime *) +} +type successful_chr_attempt = { + chr_attempt : chr_attempt; + chr_removed_goals : goal_id list; + chr_new_goals : goal list; +} +type chr_text = string (* Todo: use a formattable data, e.g. box language *) diff --git a/trace/ppx/trace_ppx.ml b/trace/ppx/trace_ppx.ml index 36b45a278..4633429c5 100644 --- a/trace/ppx/trace_ppx.ml +++ b/trace/ppx/trace_ppx.ml @@ -14,7 +14,7 @@ let z = f x in [%spy "z" ~rid ~gid ~cond (fun fmt z -> .. z ..) z]; [%spyl "z" ~rid ~gid ~cond (fun fmt z -> .. z ..) zs]; - [%log "K2" "whatever" 37]; + [%log "K2" ~rid "whatever" 37]; let x[@trace] = ... in e let w = { a; b = b[@trace ] } in match w with @@ -91,8 +91,8 @@ let spyl ~loc err ?(cond=[%expr true]) ~rid ?gid name pp = | None -> [%expr if [%e cond] then Trace_ppx_runtime.Runtime.info ~runtime_id:![%e rid] [%e name] [%e ppl]] | Some gid -> [%expr if [%e cond] then Trace_ppx_runtime.Runtime.info ~runtime_id:![%e rid] ~goal_id:(Util.UUID.hash [%e gid]) [%e name] [%e ppl]] -let log ~loc name key data = - [%expr Trace_ppx_runtime.Runtime.log [%e name] [%e key] [%e data]] +let log ~loc name ~rid key data = + [%expr Trace_ppx_runtime.Runtime.log ~runtime_id:![%e rid] [%e name] [%e key] [%e data]] let cur_pred ~loc name = [%expr Trace_ppx_runtime.Runtime.set_cur_pred [%e name]] @@ -312,10 +312,14 @@ let cur_pred_rule = Context_free.Rule.extension cur_pred_extension (* ----------------------------------------------------------------- *) let log_expand_function ~loc ~path:_ = function - | [%expr ([%e? name] [%e? key] [%e? code]) ] -> - if !enabled then log ~loc name key code - else [%expr ()] - | _ -> err ~loc "use: [%log id data]" + | { pexp_desc = Pexp_apply (name,args); _ } when !enabled -> + let rid, args = pull is_rid args in + begin match rid, args with + | Some rid, [_,key;_,code] -> log ~loc ~rid name key code + | _ -> err ~loc "use: [%log id ~rid data]" + end + | { pexp_desc = Pexp_apply _; _ } -> [%expr ()] + | _ -> err ~loc "use: [%log id ~rid data]" let log_extension = Extension.declare diff --git a/trace/runtime/runtime.ml b/trace/runtime/runtime.ml index bbd3fbb44..06f258b95 100644 --- a/trace/runtime/runtime.ml +++ b/trace/runtime/runtime.ml @@ -5,12 +5,13 @@ module F = Format +module IntMap = Map.Make(struct type t = int let compare x y = x - y end) module StrMap = Map.Make(String) module Str = Re.Str let debug = ref false let where_loc = ref ("",0,max_int) -let cur_step = ref StrMap.empty +let cur_step = ref IntMap.empty let filter = ref [] let fonly = ref [] let ponly = ref [] @@ -102,22 +103,26 @@ end module Trace = struct -let get_cur_step k = - try StrMap.find k !cur_step - with Not_found -> - try StrMap.find "run" !cur_step +let get_cur_step ~runtime_id k = + try + let m = IntMap.find runtime_id !cur_step in + try StrMap.find k m + with Not_found -> + try StrMap.find "run" m + with Not_found -> 0 with Not_found -> 0 -let condition k = +let condition ~runtime_id k = (* -trace-on *) !debug && (* -trace-at *) let loc, first_step, last_step = !where_loc in ((!hot && k <> loc) || (k = loc && - let cur_step = get_cur_step k in + let cur_step = get_cur_step ~runtime_id k in hot := cur_step >= first_step && cur_step <= last_step; - !hot)) + !hot) || + (get_cur_step ~runtime_id:0 "run" = 0 && first_step = 0 && k = "user:newgoal")) (* -trace-only *) && (!fonly = [] || List.exists (fun p -> Str.string_match p k 0) !fonly) (* -trace-skip *) @@ -130,7 +135,7 @@ let condition k = List.exists (fun p -> Str.string_match p pred 0) !ponly) let init ?(where="",0,max_int) ?(skip=[]) ?(only=[]) ?(only_pred=[]) b = - cur_step := StrMap.empty; + cur_step := IntMap.empty; debug := b; filter := List.map Str.regexp skip; fonly := List.map Str.regexp only; @@ -139,23 +144,32 @@ let init ?(where="",0,max_int) ?(skip=[]) ?(only=[]) ?(only_pred=[]) b = hot := false; ;; -let incr_cur_step k = - let n = get_cur_step k in - cur_step := StrMap.add k (n+1) !cur_step +let incr_cur_step ~runtime_id k = + let n = get_cur_step ~runtime_id k in + let n = n + 1 in + try + let m = IntMap.find runtime_id !cur_step in + let m = StrMap.add k n m in + cur_step := IntMap.add runtime_id m !cur_step + with Not_found -> + let m = StrMap.empty in + let m = StrMap.add k n m in + cur_step := IntMap.add runtime_id m !cur_step + end let enter ~runtime_id k payload = - Trace.incr_cur_step k; - if Trace.condition k then begin + Trace.incr_cur_step ~runtime_id k; + if Trace.condition ~runtime_id k then begin Perf.collect_perf_enter k; if not !trace_noprint then - !printer { runtime_id; goal_id = 0; name = k; step = Trace.get_cur_step k; kind = Start; payload = [J((fun fmt () -> payload fmt),())] } + !printer { runtime_id; goal_id = 0; name = k; step = Trace.get_cur_step ~runtime_id k; kind = Start; payload = [J((fun fmt () -> payload fmt),())] } end let info ~runtime_id ?(goal_id=0) k payload = - if not !trace_noprint && Trace.condition k then - !printer { runtime_id; goal_id ; name = k; step = Trace.get_cur_step k; kind = Info; payload } + if not !trace_noprint && Trace.condition ~runtime_id k then + !printer { runtime_id; goal_id ; name = k; step = Trace.get_cur_step ~runtime_id k; kind = Info; payload } exception TREC_CALL of Obj.t * Obj.t (* ('a -> 'b) * 'a *) @@ -167,10 +181,10 @@ let pr_exc = function let exit ~runtime_id k tailcall e time = let e = match e with None -> OK | Some x -> x in - if Trace.condition k then begin + if Trace.condition ~runtime_id k then begin Perf.collect_perf_exit time; if not !trace_noprint then - !printer { runtime_id; goal_id = 0; name = k; step = Trace.get_cur_step k; kind = Stop { cause = (if tailcall then "->" else pr_exc e); time }; payload = [J((fun _ _ -> ()),())] } + !printer { runtime_id; goal_id = 0; name = k; step = Trace.get_cur_step ~runtime_id k; kind = Stop { cause = (if tailcall then "->" else pr_exc e); time }; payload = [J((fun _ _ -> ()),())] } end (* Json *) @@ -230,11 +244,11 @@ let pp_kind fmt = function let print_json fmt = (); fun { runtime_id; goal_id; kind; name; step; payload } -> pp_d fmt [ + "step", J(pp_i,step); "kind", J(pp_kind,kind); "goal_id", J(pp_i,goal_id); "runtime_id", J(pp_i,runtime_id); "name", J(pp_s,name); - "step", J(pp_i,step); "payload", J(pp_as, payload) ]; F.pp_print_newline fmt (); @@ -277,9 +291,10 @@ let set_trace_output format formatter = (* we should make another file... *) let collecting_stats = ref false let logs = ref [] -let log name key value = +let log ~runtime_id name key value = if !collecting_stats then - logs := (name,key,Trace.get_cur_step "run",value) :: !logs + logs := (name,key,Trace.get_cur_step ~runtime_id "run",value) :: !logs + let () = at_exit (fun () -> if !logs != [] then begin @@ -383,4 +398,4 @@ let parse_argv argv = ;; let set_cur_pred x = cur_pred := x -let get_cur_step x = Trace.get_cur_step x \ No newline at end of file +let get_cur_step ~runtime_id x = Trace.get_cur_step ~runtime_id x \ No newline at end of file diff --git a/trace/runtime/runtime.mli b/trace/runtime/runtime.mli index 4df1c1ed7..37f792a7f 100644 --- a/trace/runtime/runtime.mli +++ b/trace/runtime/runtime.mli @@ -14,9 +14,9 @@ val info : runtime_id:int -> ?goal_id:int -> string -> j list -> unit val exit : runtime_id:int -> string -> bool -> exn option -> float -> unit val set_cur_pred : string option -> unit -val get_cur_step : string -> int +val get_cur_step : runtime_id:int -> string -> int -val log : string -> string -> int -> unit +val log : runtime_id:int -> string -> string -> int -> unit val debug : bool ref val parse_argv : string list -> string list diff --git a/trace_atd.ts b/trace_atd.ts new file mode 100644 index 000000000..750a84eec --- /dev/null +++ b/trace_atd.ts @@ -0,0 +1,1141 @@ +// Generated by atdts from type definitions in 'trace.atd'. +// +// Type-safe translations from/to JSON +// +// For each type 'Foo', there is a pair of functions: +// - 'writeFoo': convert a 'Foo' value into a JSON-compatible value. +// - 'readFoo': convert a JSON-compatible value into a TypeScript value +// of type 'Foo'. + + +export type Item = { + kind: Kind[]; + goal_id: Int; + runtime_id: Int; + step: Int; + name: string; + payload: string[]; +} + +export type Kind = +| { kind: 'Start' } +| { kind: 'Info' } +| { kind: 'Stop'; value: Stop } + +export type Stop = { + cause: string; + time: number; +} + +export type RawTrace = Item[] + +export type Trace = Card[] + +export type Card = { + step_id: StepId; + runtime_id: RuntimeId; + step: Step; + color: Color; +} + +export type Color = +| { kind: 'Red' } +| { kind: 'Green' } +| { kind: 'Grey' } +| { kind: 'YellowGreen' } +| { kind: 'YellowRed' } + +export type Step = +| { kind: 'Inference'; value: Inference } +| { kind: 'Findall'; value: Findall } +| { kind: 'Cut'; value: Cut } +| { kind: 'Suspend'; value: Suspend } +| { kind: 'Resume'; value: Resume } +| { kind: 'CHR'; value: Chr } +| { kind: 'Init'; value: Goal } + +export type Inference = { + current_goal_id: GoalId; + current_goal_text: GoalText; + current_goal_predicate: string; + failed_attempts: Attempt[]; + successful_attempts: SuccessfulAttempt[]; + more_successful_attempts: StepId[]; + stack: Stack; +} + +export type Attempt = { + rule: Rule; + events: Event[]; +} + +export type Rule = +| { kind: 'BuiltinRule'; value: BuiltinName } +| { 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 Location = +| { kind: 'File'; value: FileLocation } +| { kind: 'Context'; value: StepId } + +export type FileLocation = { + filename: string; + line: Int; + column: Int; + character: Int; +} + +export type Event = +| { kind: 'Assign'; value: string } +| { kind: 'Fail'; value: string } +| { kind: 'ResumeGoal'; value: GoalId[] } + +export type RuleText = string + +export type SuccessfulAttempt = { + attempt: Attempt; + siblings: Goal[]; + siblings_aggregated_outcome: Outcome; +} + +export type Goal = { + goal_text: string; + goal_id: GoalId; +} + +export type Outcome = +| { kind: 'Fail' } +| { kind: 'Success' } + +export type Stack = Frame[] + +export type Frame = { + rule: Rule; + step_id: StepId; + runtime_id: RuntimeId; +} + +export type GoalId = Int + +export type StepId = Int + +export type RuntimeId = Int + +export type GoalText = string + +export type Findall = { + findall_goal_id: GoalId; + findall_goal_text: GoalText; + findall_cards: Trace; + findall_solution_text: SolutionText; + findall_stack: Stack; +} + +export type SolutionText = string[] + +export type Suspend = { + suspend_goal_id: GoalId; + suspend_goal_text: GoalText; + suspend_sibling: Goal; + suspend_stack: Stack; +} + +export type Cut = Cutted[] + +export type Cutted = { + cut_branch_for_goal: Goal; + cut_branch: UserRule; +} + +export type Resume = Goal[] + +export type Chr = { + chr_failed_attempts: ChrAttempt[]; + chr_successful_attempts: SuccessfulChrAttempt[]; + chr_store_before: Goal[]; + chr_store_after: Goal[]; +} + +export type ChrAttempt = { + chr_text: ChrText; + chr_loc: FileLocation; + chr_condition_cards: Trace; +} + +export type SuccessfulChrAttempt = { + chr_attempt: ChrAttempt; + chr_removed_goals: GoalId[]; + chr_new_goals: Goal[]; +} + +export type ChrText = string + +export function writeItem(x: Item, context: any = x): any { + return { + 'kind': _atd_write_required_field('Item', 'kind', _atd_write_array(writeKind), x.kind, x), + 'goal_id': _atd_write_required_field('Item', 'goal_id', _atd_write_int, x.goal_id, x), + 'runtime_id': _atd_write_required_field('Item', 'runtime_id', _atd_write_int, x.runtime_id, x), + 'step': _atd_write_required_field('Item', 'step', _atd_write_int, x.step, x), + 'name': _atd_write_required_field('Item', 'name', _atd_write_string, x.name, x), + 'payload': _atd_write_required_field('Item', 'payload', _atd_write_array(_atd_write_string), x.payload, x), + }; +} + +export function readItem(x: any, context: any = x): Item { + return { + kind: _atd_read_required_field('Item', 'kind', _atd_read_array(readKind), x['kind'], x), + goal_id: _atd_read_required_field('Item', 'goal_id', _atd_read_int, x['goal_id'], x), + runtime_id: _atd_read_required_field('Item', 'runtime_id', _atd_read_int, x['runtime_id'], x), + step: _atd_read_required_field('Item', 'step', _atd_read_int, x['step'], x), + name: _atd_read_required_field('Item', 'name', _atd_read_string, x['name'], x), + payload: _atd_read_required_field('Item', 'payload', _atd_read_array(_atd_read_string), x['payload'], x), + }; +} + +export function writeKind(x: Kind, context: any = x): any { + switch (x.kind) { + case 'Start': + return 'Start' + case 'Info': + return 'Info' + case 'Stop': + return ['Stop', writeStop(x.value, x)] + } +} + +export function readKind(x: any, context: any = x): Kind { + if (typeof x === 'string') { + switch (x) { + case 'Start': + return { kind: 'Start' } + case 'Info': + return { kind: 'Info' } + default: + _atd_bad_json('Kind', x, context) + throw new Error('impossible') + } + } + else { + _atd_check_json_tuple(2, x, context) + switch (x[0]) { + case 'Stop': + return { kind: 'Stop', value: writeStop(x[1], x) } + default: + _atd_bad_json('Kind', x, context) + throw new Error('impossible') + } + } +} + +export function writeStop(x: Stop, context: any = x): any { + return { + 'cause': _atd_write_required_field('Stop', 'cause', _atd_write_string, x.cause, x), + 'time': _atd_write_required_field('Stop', 'time', _atd_write_float, x.time, x), + }; +} + +export function readStop(x: any, context: any = x): Stop { + return { + cause: _atd_read_required_field('Stop', 'cause', _atd_read_string, x['cause'], x), + time: _atd_read_required_field('Stop', 'time', _atd_read_float, x['time'], x), + }; +} + +export function writeRawTrace(x: RawTrace, context: any = x): any { + return _atd_write_array(writeItem)(x, context); +} + +export function readRawTrace(x: any, context: any = x): RawTrace { + return _atd_read_array(readItem)(x, context); +} + +export function writeTrace(x: Trace, context: any = x): any { + return _atd_write_array(writeCard)(x, context); +} + +export function readTrace(x: any, context: any = x): Trace { + return _atd_read_array(readCard)(x, context); +} + +export function writeCard(x: Card, context: any = x): any { + return { + 'step_id': _atd_write_required_field('Card', 'step_id', writeStepId, x.step_id, x), + 'runtime_id': _atd_write_required_field('Card', 'runtime_id', writeRuntimeId, x.runtime_id, x), + 'step': _atd_write_required_field('Card', 'step', writeStep, x.step, x), + 'color': _atd_write_required_field('Card', 'color', writeColor, x.color, x), + }; +} + +export function readCard(x: any, context: any = x): Card { + return { + step_id: _atd_read_required_field('Card', 'step_id', readStepId, x['step_id'], x), + runtime_id: _atd_read_required_field('Card', 'runtime_id', readRuntimeId, x['runtime_id'], x), + step: _atd_read_required_field('Card', 'step', readStep, x['step'], x), + color: _atd_read_required_field('Card', 'color', readColor, x['color'], x), + }; +} + +export function writeColor(x: Color, context: any = x): any { + switch (x.kind) { + case 'Red': + return 'Red' + case 'Green': + return 'Green' + case 'Grey': + return 'Grey' + case 'YellowGreen': + return 'YellowGreen' + case 'YellowRed': + return 'YellowRed' + } +} + +export function readColor(x: any, context: any = x): Color { + switch (x) { + case 'Red': + return { kind: 'Red' } + case 'Green': + return { kind: 'Green' } + case 'Grey': + return { kind: 'Grey' } + case 'YellowGreen': + return { kind: 'YellowGreen' } + case 'YellowRed': + return { kind: 'YellowRed' } + default: + _atd_bad_json('Color', x, context) + throw new Error('impossible') + } +} + +export function writeStep(x: Step, context: any = x): any { + switch (x.kind) { + case 'Inference': + return ['Inference', writeInference(x.value, x)] + case 'Findall': + return ['Findall', writeFindall(x.value, x)] + case 'Cut': + return ['Cut', writeCut(x.value, x)] + case 'Suspend': + return ['Suspend', writeSuspend(x.value, x)] + case 'Resume': + return ['Resume', writeResume(x.value, x)] + case 'CHR': + return ['CHR', writeChr(x.value, x)] + case 'Init': + return ['Init', writeGoal(x.value, x)] + } +} + +export function readStep(x: any, context: any = x): Step { + _atd_check_json_tuple(2, x, context) + switch (x[0]) { + case 'Inference': + return { kind: 'Inference', value: writeInference(x[1], x) } + case 'Findall': + return { kind: 'Findall', value: writeFindall(x[1], x) } + case 'Cut': + return { kind: 'Cut', value: writeCut(x[1], x) } + case 'Suspend': + return { kind: 'Suspend', value: writeSuspend(x[1], x) } + case 'Resume': + return { kind: 'Resume', value: writeResume(x[1], x) } + case 'CHR': + return { kind: 'CHR', value: writeChr(x[1], x) } + case 'Init': + return { kind: 'Init', value: writeGoal(x[1], x) } + default: + _atd_bad_json('Step', x, context) + throw new Error('impossible') + } +} + +export function writeInference(x: Inference, context: any = x): any { + return { + 'current_goal_id': _atd_write_required_field('Inference', 'current_goal_id', writeGoalId, x.current_goal_id, x), + 'current_goal_text': _atd_write_required_field('Inference', 'current_goal_text', writeGoalText, x.current_goal_text, x), + 'current_goal_predicate': _atd_write_required_field('Inference', 'current_goal_predicate', _atd_write_string, x.current_goal_predicate, x), + 'failed_attempts': _atd_write_required_field('Inference', 'failed_attempts', _atd_write_array(writeAttempt), x.failed_attempts, x), + 'successful_attempts': _atd_write_required_field('Inference', 'successful_attempts', _atd_write_array(writeSuccessfulAttempt), x.successful_attempts, x), + 'more_successful_attempts': _atd_write_required_field('Inference', 'more_successful_attempts', _atd_write_array(writeStepId), x.more_successful_attempts, x), + 'stack': _atd_write_required_field('Inference', 'stack', writeStack, x.stack, x), + }; +} + +export function readInference(x: any, context: any = x): Inference { + return { + current_goal_id: _atd_read_required_field('Inference', 'current_goal_id', readGoalId, x['current_goal_id'], x), + current_goal_text: _atd_read_required_field('Inference', 'current_goal_text', readGoalText, x['current_goal_text'], x), + current_goal_predicate: _atd_read_required_field('Inference', 'current_goal_predicate', _atd_read_string, x['current_goal_predicate'], x), + failed_attempts: _atd_read_required_field('Inference', 'failed_attempts', _atd_read_array(readAttempt), x['failed_attempts'], x), + successful_attempts: _atd_read_required_field('Inference', 'successful_attempts', _atd_read_array(readSuccessfulAttempt), x['successful_attempts'], x), + more_successful_attempts: _atd_read_required_field('Inference', 'more_successful_attempts', _atd_read_array(readStepId), x['more_successful_attempts'], x), + stack: _atd_read_required_field('Inference', 'stack', readStack, x['stack'], x), + }; +} + +export function writeAttempt(x: Attempt, context: any = x): any { + return { + 'rule': _atd_write_required_field('Attempt', 'rule', writeRule, x.rule, x), + 'events': _atd_write_required_field('Attempt', 'events', _atd_write_array(writeEvent), x.events, x), + }; +} + +export function readAttempt(x: any, context: any = x): Attempt { + return { + rule: _atd_read_required_field('Attempt', 'rule', readRule, x['rule'], x), + events: _atd_read_required_field('Attempt', 'events', _atd_read_array(readEvent), x['events'], x), + }; +} + +export function writeRule(x: Rule, context: any = x): any { + switch (x.kind) { + case 'BuiltinRule': + return ['BuiltinRule', writeBuiltinName(x.value, x)] + case 'UserRule': + return ['UserRule', writeUserRule(x.value, x)] + } +} + +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: writeBuiltinName(x[1], x) } + case 'UserRule': + return { kind: 'UserRule', value: writeUserRule(x[1], x) } + default: + _atd_bad_json('Rule', x, context) + throw new Error('impossible') + } +} + +export function writeUserRule(x: UserRule, context: any = x): any { + return { + 'rule_text': _atd_write_required_field('UserRule', 'rule_text', writeRuleText, x.rule_text, x), + 'rule_loc': _atd_write_required_field('UserRule', 'rule_loc', writeLocation, x.rule_loc, x), + }; +} + +export function readUserRule(x: any, context: any = x): UserRule { + return { + rule_text: _atd_read_required_field('UserRule', 'rule_text', readRuleText, x['rule_text'], x), + rule_loc: _atd_read_required_field('UserRule', 'rule_loc', readLocation, x['rule_loc'], x), + }; +} + +export function writeBuiltinName(x: BuiltinName, context: any = x): any { + switch (x.kind) { + case 'Logic': + return ['Logic', _atd_write_string(x.value, x)] + case 'FFI': + return ['FFI', _atd_write_string(x.value, x)] + } +} + +export function readBuiltinName(x: any, context: any = x): BuiltinName { + _atd_check_json_tuple(2, x, context) + switch (x[0]) { + case 'Logic': + return { kind: 'Logic', value: _atd_write_string(x[1], x) } + case 'FFI': + return { kind: 'FFI', value: _atd_write_string(x[1], x) } + default: + _atd_bad_json('BuiltinName', x, context) + throw new Error('impossible') + } +} + +export function writeLocation(x: Location, context: any = x): any { + switch (x.kind) { + case 'File': + return ['File', writeFileLocation(x.value, x)] + case 'Context': + return ['Context', writeStepId(x.value, x)] + } +} + +export function readLocation(x: any, context: any = x): Location { + _atd_check_json_tuple(2, x, context) + switch (x[0]) { + case 'File': + return { kind: 'File', value: writeFileLocation(x[1], x) } + case 'Context': + return { kind: 'Context', value: writeStepId(x[1], x) } + default: + _atd_bad_json('Location', x, context) + throw new Error('impossible') + } +} + +export function writeFileLocation(x: FileLocation, context: any = x): any { + return { + 'filename': _atd_write_required_field('FileLocation', 'filename', _atd_write_string, x.filename, x), + 'line': _atd_write_required_field('FileLocation', 'line', _atd_write_int, x.line, x), + 'column': _atd_write_required_field('FileLocation', 'column', _atd_write_int, x.column, x), + 'character': _atd_write_required_field('FileLocation', 'character', _atd_write_int, x.character, x), + }; +} + +export function readFileLocation(x: any, context: any = x): FileLocation { + return { + filename: _atd_read_required_field('FileLocation', 'filename', _atd_read_string, x['filename'], x), + line: _atd_read_required_field('FileLocation', 'line', _atd_read_int, x['line'], x), + column: _atd_read_required_field('FileLocation', 'column', _atd_read_int, x['column'], x), + character: _atd_read_required_field('FileLocation', 'character', _atd_read_int, x['character'], x), + }; +} + +export function writeEvent(x: Event, context: any = x): any { + switch (x.kind) { + case 'Assign': + return ['Assign', _atd_write_string(x.value, x)] + case 'Fail': + return ['Fail', _atd_write_string(x.value, x)] + case 'ResumeGoal': + return ['ResumeGoal', _atd_write_array(writeGoalId)(x.value, x)] + } +} + +export function readEvent(x: any, context: any = x): Event { + _atd_check_json_tuple(2, x, context) + switch (x[0]) { + case 'Assign': + return { kind: 'Assign', value: _atd_write_string(x[1], x) } + case 'Fail': + return { kind: 'Fail', value: _atd_write_string(x[1], x) } + case 'ResumeGoal': + return { kind: 'ResumeGoal', value: _atd_write_array(writeGoalId)(x[1], x) } + default: + _atd_bad_json('Event', x, context) + throw new Error('impossible') + } +} + +export function writeRuleText(x: RuleText, context: any = x): any { + return _atd_write_string(x, context); +} + +export function readRuleText(x: any, context: any = x): RuleText { + return _atd_read_string(x, context); +} + +export function writeSuccessfulAttempt(x: SuccessfulAttempt, context: any = x): any { + return { + 'attempt': _atd_write_required_field('SuccessfulAttempt', 'attempt', writeAttempt, x.attempt, x), + 'siblings': _atd_write_required_field('SuccessfulAttempt', 'siblings', _atd_write_array(writeGoal), x.siblings, x), + 'siblings_aggregated_outcome': _atd_write_required_field('SuccessfulAttempt', 'siblings_aggregated_outcome', writeOutcome, x.siblings_aggregated_outcome, x), + }; +} + +export function readSuccessfulAttempt(x: any, context: any = x): SuccessfulAttempt { + return { + attempt: _atd_read_required_field('SuccessfulAttempt', 'attempt', readAttempt, x['attempt'], x), + siblings: _atd_read_required_field('SuccessfulAttempt', 'siblings', _atd_read_array(readGoal), x['siblings'], x), + siblings_aggregated_outcome: _atd_read_required_field('SuccessfulAttempt', 'siblings_aggregated_outcome', readOutcome, x['siblings_aggregated_outcome'], x), + }; +} + +export function writeGoal(x: Goal, context: any = x): any { + return { + 'goal_text': _atd_write_required_field('Goal', 'goal_text', _atd_write_string, x.goal_text, x), + 'goal_id': _atd_write_required_field('Goal', 'goal_id', writeGoalId, x.goal_id, x), + }; +} + +export function readGoal(x: any, context: any = x): Goal { + return { + goal_text: _atd_read_required_field('Goal', 'goal_text', _atd_read_string, x['goal_text'], x), + goal_id: _atd_read_required_field('Goal', 'goal_id', readGoalId, x['goal_id'], x), + }; +} + +export function writeOutcome(x: Outcome, context: any = x): any { + switch (x.kind) { + case 'Fail': + return 'Fail' + case 'Success': + return 'Success' + } +} + +export function readOutcome(x: any, context: any = x): Outcome { + switch (x) { + case 'Fail': + return { kind: 'Fail' } + case 'Success': + return { kind: 'Success' } + default: + _atd_bad_json('Outcome', x, context) + throw new Error('impossible') + } +} + +export function writeStack(x: Stack, context: any = x): any { + return _atd_write_array(writeFrame)(x, context); +} + +export function readStack(x: any, context: any = x): Stack { + return _atd_read_array(readFrame)(x, context); +} + +export function writeFrame(x: Frame, context: any = x): any { + return { + 'rule': _atd_write_required_field('Frame', 'rule', writeRule, x.rule, x), + 'step_id': _atd_write_required_field('Frame', 'step_id', writeStepId, x.step_id, x), + 'runtime_id': _atd_write_required_field('Frame', 'runtime_id', writeRuntimeId, x.runtime_id, x), + }; +} + +export function readFrame(x: any, context: any = x): Frame { + return { + rule: _atd_read_required_field('Frame', 'rule', readRule, x['rule'], x), + step_id: _atd_read_required_field('Frame', 'step_id', readStepId, x['step_id'], x), + runtime_id: _atd_read_required_field('Frame', 'runtime_id', readRuntimeId, x['runtime_id'], x), + }; +} + +export function writeGoalId(x: GoalId, context: any = x): any { + return _atd_write_int(x, context); +} + +export function readGoalId(x: any, context: any = x): GoalId { + return _atd_read_int(x, context); +} + +export function writeStepId(x: StepId, context: any = x): any { + return _atd_write_int(x, context); +} + +export function readStepId(x: any, context: any = x): StepId { + return _atd_read_int(x, context); +} + +export function writeRuntimeId(x: RuntimeId, context: any = x): any { + return _atd_write_int(x, context); +} + +export function readRuntimeId(x: any, context: any = x): RuntimeId { + return _atd_read_int(x, context); +} + +export function writeGoalText(x: GoalText, context: any = x): any { + return _atd_write_string(x, context); +} + +export function readGoalText(x: any, context: any = x): GoalText { + return _atd_read_string(x, context); +} + +export function writeFindall(x: Findall, context: any = x): any { + return { + 'findall_goal_id': _atd_write_required_field('Findall', 'findall_goal_id', writeGoalId, x.findall_goal_id, x), + 'findall_goal_text': _atd_write_required_field('Findall', 'findall_goal_text', writeGoalText, x.findall_goal_text, x), + 'findall_cards': _atd_write_required_field('Findall', 'findall_cards', writeTrace, x.findall_cards, x), + 'findall_solution_text': _atd_write_required_field('Findall', 'findall_solution_text', writeSolutionText, x.findall_solution_text, x), + 'findall_stack': _atd_write_required_field('Findall', 'findall_stack', writeStack, x.findall_stack, x), + }; +} + +export function readFindall(x: any, context: any = x): Findall { + return { + findall_goal_id: _atd_read_required_field('Findall', 'findall_goal_id', readGoalId, x['findall_goal_id'], x), + findall_goal_text: _atd_read_required_field('Findall', 'findall_goal_text', readGoalText, x['findall_goal_text'], x), + findall_cards: _atd_read_required_field('Findall', 'findall_cards', readTrace, x['findall_cards'], x), + findall_solution_text: _atd_read_required_field('Findall', 'findall_solution_text', readSolutionText, x['findall_solution_text'], x), + findall_stack: _atd_read_required_field('Findall', 'findall_stack', readStack, x['findall_stack'], x), + }; +} + +export function writeSolutionText(x: SolutionText, context: any = x): any { + return _atd_write_array(_atd_write_string)(x, context); +} + +export function readSolutionText(x: any, context: any = x): SolutionText { + return _atd_read_array(_atd_read_string)(x, context); +} + +export function writeSuspend(x: Suspend, context: any = x): any { + return { + 'suspend_goal_id': _atd_write_required_field('Suspend', 'suspend_goal_id', writeGoalId, x.suspend_goal_id, x), + 'suspend_goal_text': _atd_write_required_field('Suspend', 'suspend_goal_text', writeGoalText, x.suspend_goal_text, x), + 'suspend_sibling': _atd_write_required_field('Suspend', 'suspend_sibling', writeGoal, x.suspend_sibling, x), + 'suspend_stack': _atd_write_required_field('Suspend', 'suspend_stack', writeStack, x.suspend_stack, x), + }; +} + +export function readSuspend(x: any, context: any = x): Suspend { + return { + suspend_goal_id: _atd_read_required_field('Suspend', 'suspend_goal_id', readGoalId, x['suspend_goal_id'], x), + suspend_goal_text: _atd_read_required_field('Suspend', 'suspend_goal_text', readGoalText, x['suspend_goal_text'], x), + suspend_sibling: _atd_read_required_field('Suspend', 'suspend_sibling', readGoal, x['suspend_sibling'], x), + suspend_stack: _atd_read_required_field('Suspend', 'suspend_stack', readStack, x['suspend_stack'], x), + }; +} + +export function writeCut(x: Cut, context: any = x): any { + return _atd_write_array(writeCutted)(x, context); +} + +export function readCut(x: any, context: any = x): Cut { + return _atd_read_array(readCutted)(x, context); +} + +export function writeCutted(x: Cutted, context: any = x): any { + return { + 'cut_branch_for_goal': _atd_write_required_field('Cutted', 'cut_branch_for_goal', writeGoal, x.cut_branch_for_goal, x), + 'cut_branch': _atd_write_required_field('Cutted', 'cut_branch', writeUserRule, x.cut_branch, x), + }; +} + +export function readCutted(x: any, context: any = x): Cutted { + return { + cut_branch_for_goal: _atd_read_required_field('Cutted', 'cut_branch_for_goal', readGoal, x['cut_branch_for_goal'], x), + cut_branch: _atd_read_required_field('Cutted', 'cut_branch', readUserRule, x['cut_branch'], x), + }; +} + +export function writeResume(x: Resume, context: any = x): any { + return _atd_write_array(writeGoal)(x, context); +} + +export function readResume(x: any, context: any = x): Resume { + return _atd_read_array(readGoal)(x, context); +} + +export function writeChr(x: Chr, context: any = x): any { + return { + 'chr_failed_attempts': _atd_write_required_field('Chr', 'chr_failed_attempts', _atd_write_array(writeChrAttempt), x.chr_failed_attempts, x), + 'chr_successful_attempts': _atd_write_required_field('Chr', 'chr_successful_attempts', _atd_write_array(writeSuccessfulChrAttempt), x.chr_successful_attempts, x), + 'chr_store_before': _atd_write_required_field('Chr', 'chr_store_before', _atd_write_array(writeGoal), x.chr_store_before, x), + 'chr_store_after': _atd_write_required_field('Chr', 'chr_store_after', _atd_write_array(writeGoal), x.chr_store_after, x), + }; +} + +export function readChr(x: any, context: any = x): Chr { + return { + chr_failed_attempts: _atd_read_required_field('Chr', 'chr_failed_attempts', _atd_read_array(readChrAttempt), x['chr_failed_attempts'], x), + chr_successful_attempts: _atd_read_required_field('Chr', 'chr_successful_attempts', _atd_read_array(readSuccessfulChrAttempt), x['chr_successful_attempts'], x), + chr_store_before: _atd_read_required_field('Chr', 'chr_store_before', _atd_read_array(readGoal), x['chr_store_before'], x), + chr_store_after: _atd_read_required_field('Chr', 'chr_store_after', _atd_read_array(readGoal), x['chr_store_after'], x), + }; +} + +export function writeChrAttempt(x: ChrAttempt, context: any = x): any { + return { + 'chr_text': _atd_write_required_field('ChrAttempt', 'chr_text', writeChrText, x.chr_text, x), + 'chr_loc': _atd_write_required_field('ChrAttempt', 'chr_loc', writeFileLocation, x.chr_loc, x), + 'chr_condition_cards': _atd_write_required_field('ChrAttempt', 'chr_condition_cards', writeTrace, x.chr_condition_cards, x), + }; +} + +export function readChrAttempt(x: any, context: any = x): ChrAttempt { + return { + chr_text: _atd_read_required_field('ChrAttempt', 'chr_text', readChrText, x['chr_text'], x), + chr_loc: _atd_read_required_field('ChrAttempt', 'chr_loc', readFileLocation, x['chr_loc'], x), + chr_condition_cards: _atd_read_required_field('ChrAttempt', 'chr_condition_cards', readTrace, x['chr_condition_cards'], x), + }; +} + +export function writeSuccessfulChrAttempt(x: SuccessfulChrAttempt, context: any = x): any { + return { + 'chr_attempt': _atd_write_required_field('SuccessfulChrAttempt', 'chr_attempt', writeChrAttempt, x.chr_attempt, x), + 'chr_removed_goals': _atd_write_required_field('SuccessfulChrAttempt', 'chr_removed_goals', _atd_write_array(writeGoalId), x.chr_removed_goals, x), + 'chr_new_goals': _atd_write_required_field('SuccessfulChrAttempt', 'chr_new_goals', _atd_write_array(writeGoal), x.chr_new_goals, x), + }; +} + +export function readSuccessfulChrAttempt(x: any, context: any = x): SuccessfulChrAttempt { + return { + chr_attempt: _atd_read_required_field('SuccessfulChrAttempt', 'chr_attempt', readChrAttempt, x['chr_attempt'], x), + chr_removed_goals: _atd_read_required_field('SuccessfulChrAttempt', 'chr_removed_goals', _atd_read_array(readGoalId), x['chr_removed_goals'], x), + chr_new_goals: _atd_read_required_field('SuccessfulChrAttempt', 'chr_new_goals', _atd_read_array(readGoal), x['chr_new_goals'], x), + }; +} + +export function writeChrText(x: ChrText, context: any = x): any { + return _atd_write_string(x, context); +} + +export function readChrText(x: any, context: any = x): ChrText { + return _atd_read_string(x, context); +} + + +///////////////////////////////////////////////////////////////////// +// Runtime library +///////////////////////////////////////////////////////////////////// + +export type Int = number + +export type Option = null | { value: T } + +function _atd_missing_json_field(type_name: string, json_field_name: string) { + throw new Error(`missing field '${json_field_name}'` + + ` in JSON object of type '${type_name}'`) +} + +function _atd_missing_ts_field(type_name: string, ts_field_name: string) { + throw new Error(`missing field '${ts_field_name}'` + + ` in TypeScript object of type '${type_name}'`) +} + +function _atd_bad_json(expected_type: string, json_value: any, context: any) { + let value_str = JSON.stringify(json_value) + if (value_str.length > 200) + value_str = value_str.substring(0, 200) + '…'; + + throw new Error(`incompatible JSON value where` + + ` type '${expected_type}' was expected: '${value_str}'.` + + ` Occurs in '${JSON.stringify(context)}'.`) +} + +function _atd_bad_ts(expected_type: string, ts_value: any, context: any) { + let value_str = JSON.stringify(ts_value) + if (value_str.length > 200) + value_str = value_str.substring(0, 200) + '…'; + + throw new Error(`incompatible TypeScript value where` + + ` type '${expected_type}' was expected: '${value_str}'.` + + ` Occurs in '${JSON.stringify(context)}'.`) +} + +function _atd_check_json_tuple(len: Int, x: any, context: any) { + if (! Array.isArray(x) || x.length !== len) + _atd_bad_json('tuple of length ' + len, x, context); +} + +function _atd_read_unit(x: any, context: any): null { + if (x === null) + return null + else { + _atd_bad_json('null', x, context) + throw new Error('impossible') + } +} + +function _atd_read_bool(x: any, context: any): boolean { + if (typeof x === 'boolean') + return x + else { + _atd_bad_json('boolean', x, context) + throw new Error('impossible') + } +} + +function _atd_read_int(x: any, context: any): Int { + if (Number.isInteger(x)) + return x + else { + _atd_bad_json('integer', x, context) + throw new Error('impossible') + } +} + +function _atd_read_float(x: any, context: any): number { + if (isFinite(x)) + return x + else { + _atd_bad_json('number', x, context) + throw new Error('impossible') + } +} + +function _atd_read_string(x: any, context: any): string { + if (typeof x === 'string') + return x + else { + _atd_bad_json('string', x, context) + throw new Error('impossible') + } +} + +function _atd_read_required_field(type_name: string, + field_name: string, + read_elt: (x: any, context: any) => T, + x: any, + context: any): T { + if (x === undefined) { + _atd_missing_json_field(type_name, field_name) + throw new Error('impossible') + } + else + return read_elt(x, context) +} + +function _atd_read_optional_field(read_elt: (x: any, context: any) => T, + x: any, + context: any): T { + if (x === undefined || x === null) + return x + else + return read_elt(x, context) +} + +function _atd_read_field_with_default(read_elt: (x: any, context: any) => T, + default_: T, + x: any, + context: any): T { + if (x === undefined || x === null) + return default_ + else + return read_elt(x, context) +} + +function _atd_read_option(read_elt: (x: any, context: any) => T): + (x: any, context: any) => Option { + function read_option(x: any, context: any): Option { + if (x === 'None') + return null + else { + _atd_check_json_tuple(2, x, context); + switch (x[0]) { + case 'Some': + return { value: read_elt(x[1], context) } + default: + _atd_bad_json('option', x, context) + throw new Error('impossible') + } + } + } + return read_option +} + +function _atd_read_nullable(read_elt: (x: any, context: any) => T): + (x: any, context: any) => T | null { + function read_nullable(x: any, context: any): T | null { + if (x === null) + return null + else + return read_elt(x, context) + } + return read_nullable +} + +function _atd_read_array(read_elt: (x: any, context: any) => T): + (elts: any, context: any) => T[] { + function read_array(elts: any, context: any): T[] { + if (Array.isArray(elts)) + return elts.map((x) => read_elt(x, elts)) + else { + _atd_bad_json('array', elts, context) + throw new Error('impossible') + } + } + return read_array +} + +function _atd_read_assoc_array_into_map( + read_key: (key: any, context: any) => K, + read_value: (value: any, context: any) => V + ): (x: any, context: any) => Map { + function read_assoc(elts: any, context: any): Map { + if (Array.isArray(elts)) { + const res = new Map([]) + for (const x of elts) { + if (Array.isArray(x) && x.length === 2) + res.set(read_key(x[0], x), read_value(x[1], x)) + else { + _atd_bad_json('pair', x, elts) + throw new Error('impossible') + } + } + return res + } + else { + _atd_bad_json('array', elts, context) + throw new Error('impossible') + } + } + return read_assoc +} + +function _atd_read_assoc_object_into_map( + read_value: (value: any, context: any) => T + ): (x: any, context: any) => Map { + function read_assoc(elts: any, context: any): Map { + if (typeof elts === 'object') { + const res = new Map([]) + for (const [key, value] of Object.entries(elts)) + res.set(key, read_value(value, elts)) + return res + } + else { + _atd_bad_json('object', elts, context) + throw new Error('impossible') + } + } + return read_assoc +} + +function _atd_read_assoc_object_into_array( + read_value: (value: any, context: any) => T + ): (x: any, context: any) => [string, T][] { + function read_assoc(elts: any, context: any): [string, T][] { + if (typeof elts === 'object') { + const res: [string, T][] = [] + for (const [key, value] of Object.entries(elts)) + res.push([key, read_value(value, elts)]) + return res + } + else { + _atd_bad_json('object', elts, context) + throw new Error('impossible') + } + } + return read_assoc +} + +function _atd_write_unit(x: any, context: any) { + if (x === null) + return x + else { + _atd_bad_ts('null', x, context) + throw new Error('impossible') + } +} + +function _atd_write_bool(x: any, context: any): boolean { + if (typeof x === 'boolean') + return x + else { + _atd_bad_ts('boolean', x, context) + throw new Error('impossible') + } +} + +function _atd_write_int(x: any, context: any): Int { + if (Number.isInteger(x)) + return x + else { + _atd_bad_ts('integer', x, context) + throw new Error('impossible') + } +} + +function _atd_write_float(x: any, context: any): number { + if (isFinite(x)) + return x + else { + _atd_bad_ts('number', x, context) + throw new Error('impossible') + } +} + +function _atd_write_string(x: any, context: any): string { + if (typeof x === 'string') + return x + else { + _atd_bad_ts('string', x, context) + throw new Error('impossible') + } +} + +function _atd_write_option(write_elt: (x: T, context: any) => any): + (elts: Option, context: any) => any { + function write_option(x: Option, context: any): any { + if (x === null) + return 'None' + else + return ['Some', write_elt(x.value, context)] + } + return write_option +} + +function _atd_write_nullable(write_elt: (x: T | null, context: any) => any): + (x: T | null, context: any) => any { + function write_option(x: T | null, context: any): any { + if (x === null) + return null + else + return write_elt(x, context) + } + return write_option +} + +function _atd_write_array(write_elt: (elt: T, context: any) => any): + (elts: T[], context: any) => any { + return ((elts: T[], context: any): any => + elts.map((x) => write_elt(x, elts)) + ) +} + +function _atd_write_assoc_map_to_array( + write_key: (key: K, context: any) => any, + write_value: (value: V, context: any) => any + ): (elts: Map, context: any) => any { + function write_assoc(elts: Map, context: any): any { + const res: any = [] + elts.forEach((value: V, key: K) => + res.push([write_key(key, elts), write_value(value, elts)]) + ) + return res + } + return write_assoc +} + +function _atd_write_assoc_map_to_object( + write_value: (value: T, context: any) => any + ): (elts: Map, context: any) => any { + function write_assoc(elts: Map, context: any): any { + const res: any = {} + elts.forEach((value: T, key: string) => + res[key] = write_value(value, elts) + ) + return res + } + return write_assoc +} + +function _atd_write_assoc_array_to_object( + write_value: (value: T, context: any) => any + ): (elts: [string, T][], context: any) => any { + function write_assoc(elts: [string, T][], context: any): any { + const res: any = {} + for (const [key, value] of elts) + res[key] = write_value(value, elts) + return res + } + return write_assoc +} + +function _atd_write_required_field(type_name: string, + field_name: string, + write_elt: (x: T, context: any) => any, + x: T, + context: any): any { + if (x === undefined) { + _atd_missing_ts_field(type_name, field_name) + throw new Error('impossible') + } + else + return write_elt(x, context) +} + +function _atd_write_optional_field(write_elt: (x: T, context: any) => any, + x: T, + context: any): any { + if (x === undefined || x === null) + return x + else + return write_elt(x, context) +} + +function _atd_write_field_with_default( + write_elt: (x: T, context: any) => any, + default_: T, + x: T, + context: any +): T { + const value = (x === undefined || x === null) ? default_ : x + return write_elt(value, context) +} +