From d3ce8e8e22cd0c645ffa96372f944aad09532232 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 31 Jul 2026 17:30:05 -0400 Subject: [PATCH 1/2] Add file system builtins from Sys - Add a helper for conditionally constructing error diagnostics - add builtins for readdir, file_exists, is_directory, remove, rename, chdir, mkdir, rmdir, getcwd, and readdir --- src/builtin.elpi | 48 +++++++++++- src/builtin.ml | 186 +++++++++++++++++++++++++++++++++++++---------- 2 files changed, 195 insertions(+), 39 deletions(-) diff --git a/src/builtin.elpi b/src/builtin.elpi index 80e49cc2d..736e5f8e7 100644 --- a/src/builtin.elpi +++ b/src/builtin.elpi @@ -277,7 +277,7 @@ triple_2 (triple _ B _) B. func triple_3 triple A B C -> C. triple_3 (triple _ _ C) C. - + % The option type (aka Maybe) @@ -344,12 +344,58 @@ external func eof in_stream. % [gettimeofday T] sets T to the number of seconds elapsed since 1/1/1970 external func gettimeofday -> float. +% [sys.file_exists Path] is like [Sys.file_exists]. It succeeds if the file +% at [Path] exists +external func sys.file_exists string. + +% [sys.is_directory Path Diagnostic] is like [Sys.is_directory]. It succeeds +% if [Diagnostic = ok] and [Path] is a directory or [Diagnostic = error Msg] +% and [Msg] describes an encountered system error. +external func sys.is_directory string -> diagnostic. + +% [sys.remove Path Diagnostic] is like [Sys.remove]. It succeeds if +% [Diagnostic = ok] and the file at [Path] is removed or [Diagnostic = error +% Msg] and [Msg] describes an encountered system error. +external func sys.remove string -> diagnostic. + +% [sys.rename OldPath NewPath Diagnostic] is like [Sys.rename]. It succeeds +% if [Diagnostic = ok] and the file at [OldPath] is renamed to [NewPath] or +% [Diagnostic = error Msg] and [Msg] describes an encountered system error. +external func sys.rename string, string -> diagnostic. + % [getenv VarName Value] Like Sys.getenv_opt external func getenv string -> option string. % [system Command RetVal] executes Command and sets RetVal to the exit code external func system string -> int. +% [sys.chdir DirPath Diagnostic] is like [Sys.chdir]. It succeeds if +% [Diagnostic = ok] and the current working directory is updated to +% [DirPath] or [Diagnostic = error Msg] and [Msg] describes an encountered +% system error. +external func sys.chdir string -> diagnostic. + +% [sys.mkdir DirPath Permissions Diagnostic] is like [Sys.mkdir]. It +% succeeds if [Diagnostic = ok] and the directory [DirPath] is created or +% [Diagnostic = error Msg] and [Msg] describes an encountered system error. +external func sys.mkdir string, int -> diagnostic. + +% [sys.rmdir DirPath Diagnostic] is like [Sys.rmdir]. It succeeds if +% [Diagnostic = ok] and the directory [DirPath] is removed or [Diagnostic = +% error Msg] and [Msg] describes an encountered system error. +external func sys.rmdir string -> diagnostic. + +% [sys.getcwd DirPath Diagnostic] is like [Sys.getcwd]. It succeeds if +% [Diagnostic = ok] and [DirPath] is the current working directory or +% [Diagnostic = error Msg] and [Msg] describes an encountered system error. +external func sys.getcwd -> string, diagnostic. + +% [sys.readdir DirPath Contents Diagnostic] is like [Sys.readdir]. It +% succeeds if [Diagnostic = ok] and [Contents] is the list of files in +% [DirPath] or [Diagnostic = error Msg] and [Msg] describes an encountered +% system error. +external func sys.readdir string -> list string, diagnostic. + % -- Unix -- % gathers the standard file descriptors or a process diff --git a/src/builtin.ml b/src/builtin.ml index 7c5287be2..4d2a8d75b 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -129,16 +129,16 @@ let option_decl a = let open AlgebraicData in Decl { constructors = [ K("none","",N, B None, - M (fun ~ok ~ko -> function None -> ok | _ -> ko ())); + M (fun ~ok ~ko -> function None -> ok | _ -> ko ())); K("some","",A(a,N), B (fun x -> Some x), - M (fun ~ok ~ko -> function Some x -> ok x | _ -> ko ())); + M (fun ~ok ~ko -> function Some x -> ok x | _ -> ko ())); ]; } let option_alloc = let open AlgebraicData in allocate_constructors (Param option_decl) -let option a = +let option a = let open AlgebraicData in declare_allocated option_alloc (option_decl a) |> ContextualConversion.(!<) @@ -169,6 +169,12 @@ let diagnostic = let open API.AlgebraicData in declare { let unix_error_to_diagnostic e f a = mkERROR (Printf.sprintf "%s: %s" (if a <> "" then f ^ " " ^ a else f) (Unix.error_message e)) +let fail_or_mkERROR (d : diagnostic ioarg) msg = + match d with + | Data (OK) -> raise No_clause (* fail *) + | NoData -> None (* discard *) + | Data (ERROR _) -> Some (mkERROR msg) (* construct the needed error *) + let cmp = let open AlgebraicData in declare { ty = TyName "cmp"; doc = "Result of a comparison"; @@ -180,7 +186,6 @@ let cmp = let open AlgebraicData in declare { ]; } |> ContextualConversion.(!<) - type 'a unspec = Given of 'a | Unspec let unspecC data = let open API.ContextualConversion in let open API.RawData in { @@ -231,7 +236,7 @@ external func pattern_match A -> A.|}; LPCode "external func (pi) (func A)."; LPCode "external func (sigma) (func A)."; - + MLData BuiltInData.int; MLData BuiltInData.string; MLData BuiltInData.float; @@ -306,7 +311,7 @@ external func pattern_match A -> A.|}; if p (out x) (out y) then () else raise No_clause else if ty2 string x y then let out = to_string in if p (out x) (out y) then () else raise No_clause - else + else type_error ("Wrong arguments to " ^ psym ^ " (or to " ^ pname^ ")") (* HACK: grundlagen.elpi uses the "age" of constants *) | Const t1, Const t2 -> @@ -320,8 +325,8 @@ external func pattern_match A -> A.|}; { p = (<=); psym = "=<"; pname = "le_" } ; { p = (>=); psym = ">="; pname = "ge_" } ] - @ - let build_symb (spref, ty) = + @ + let build_symb (spref, ty) = let op_l = ["gt_";"lt_"; "le_"; "ge_"] in let sym_l = List.map (fun x -> spref ^ x) [">";"<"; "=<"; ">="] in let buildLPCode s op = LPCode (Printf.sprintf "func (%s) %s, %s.\nX %s Y :- %s X Y." s ty ty s op) in @@ -357,11 +362,11 @@ triple_2 (triple _ B _) B. func triple_3 triple A B C -> C. triple_3 (triple _ _ C) C. - + |}; MLData option_decl; - + MLData cmp; MLData diagnostic; @@ -380,7 +385,7 @@ let io_builtins = let open BuiltIn in let open BuiltInData in [ MLData (in_stream); MLData (out_stream); - + MLCode(Pred("open_in", In(string, "FileName", Out(in_stream, "InStream", @@ -489,6 +494,53 @@ let io_builtins = let open BuiltIn in let open BuiltInData in [ (fun _ ~depth -> !:(Unix.gettimeofday ()))), DocAbove); + MLCode (Pred ("sys.file_exists", + In (string, "Path", + Easy "is like [Sys.file_exists]. It succeeds if the file at [Path] exists"), + (fun path ~depth:_ -> + match Sys.file_exists path with + | true -> () + | false -> raise No_clause + | exception Sys_error e -> + (* No recoverable errors are produced by Sys.file_exists *) + Utils.error ("file_exists: " ^ e))), + DocAbove); + + MLCode (Pred ("sys.is_directory", + In (string, "Path", + InOut ((ioarg diagnostic), "Diagnostic", + Easy "is like [Sys.is_directory]. It succeeds if [Diagnostic = ok] and [Path] is \ +a directory or [Diagnostic = error Msg] and [Msg] describes an encountered system error.")), + (fun path d ~depth:_ -> + match Sys.is_directory path with + | false -> raise No_clause + | true -> !: mkOK + | exception Sys_error e -> ?: (fail_or_mkERROR d e))), + DocAbove); + + MLCode (Pred ("sys.remove", + In (string, "Path", + InOut (ioarg diagnostic, "Diagnostic", + Easy "is like [Sys.remove]. It succeeds if [Diagnostic = ok] and the file at [Path] is \ +removed or [Diagnostic = error Msg] and [Msg] describes an encountered system error.")), + (fun path d ~depth:_ -> + match Sys.remove path with + | () -> !: mkOK + | exception Sys_error e -> ?: (fail_or_mkERROR d e))), + DocAbove); + + MLCode (Pred ("sys.rename", + In (string, "OldPath", + In (string, "NewPath", + InOut (ioarg diagnostic, "Diagnostic", + Easy "is like [Sys.rename]. It succeeds if [Diagnostic = ok] and the file at [OldPath] is \ +renamed to [NewPath] or [Diagnostic = error Msg] and [Msg] describes an encountered system error."))), + (fun old_path new_path d ~depth:_ -> + match Sys.rename old_path new_path with + | () -> !: mkOK + | exception Sys_error e -> ?: (fail_or_mkERROR d e))), + DocAbove); + MLCode(Pred("getenv", In(string, "VarName", Out(option string, "Value", @@ -500,9 +552,67 @@ let io_builtins = let open BuiltIn in let open BuiltInData in [ In(string, "Command", Out(int, "RetVal", Easy "executes Command and sets RetVal to the exit code")), - (fun s _ ~depth -> !:(Sys.command s))), + (fun s _ ~depth -> !:(Sys.command s))), + DocAbove); + + MLCode(Pred("sys.chdir", + In(string, "DirPath", + InOut(ioarg diagnostic, "Diagnostic", + Easy "is like [Sys.chdir]. It succeeds if [Diagnostic = ok] and the current working directory \ +is updated to [DirPath] or [Diagnostic = error Msg] and [Msg] describes an encountered system error.")), + (fun path d ~depth:_ -> + match Sys.chdir path with + | () -> !: mkOK + | exception Sys_error e -> ?: (fail_or_mkERROR d e))), + DocAbove); + + MLCode(Pred("sys.mkdir", + In(string, "DirPath", + In(int, "Permissions", + InOut(ioarg diagnostic, "Diagnostic", + Easy "is like [Sys.mkdir]. It succeeds if [Diagnostic = ok] and the directory [DirPath] is created \ +or [Diagnostic = error Msg] and [Msg] describes an encountered system error."))), + (fun path perms d ~depth:_ -> + match Sys.mkdir path perms with + | () -> !: mkOK + | exception Sys_error e -> ?: (fail_or_mkERROR d e))), + DocAbove); + + MLCode(Pred("sys.rmdir", + In(string, "DirPath", + InOut(ioarg diagnostic, "Diagnostic", + Easy "is like [Sys.rmdir]. It succeeds if [Diagnostic = ok] and the directory [DirPath] is removed \ +or [Diagnostic = error Msg] and [Msg] describes an encountered system error.")), + (fun path d ~depth:_ -> + match Sys.rmdir path with + | () -> !: mkOK + | exception Sys_error e -> ?: (fail_or_mkERROR d e))), + DocAbove); + + MLCode(Pred("sys.getcwd", + Out(string, "DirPath", + InOut(ioarg diagnostic, "Diagnostic", + Easy "is like [Sys.getcwd]. It succeeds if [Diagnostic = ok] and [DirPath] is the current working \ +directory or [Diagnostic = error Msg] and [Msg] describes an encountered system error.")), + (fun _ d ~depth:_ -> + match Sys.getcwd () with + | dir -> !: dir +! mkOK + | exception Sys_error e -> ?: None +? (fail_or_mkERROR d e))), + DocAbove); + + MLCode (Pred ("sys.readdir", + In (string, "DirPath", + Out (list string, "Contents", + InOut (ioarg diagnostic, "Diagnostic", + Easy "is like [Sys.readdir]. It succeeds if [Diagnostic = ok] and [Contents] is the list of files \ +in [DirPath] or [Diagnostic = error Msg] and [Msg] describes an encountered system error."))), + (fun path _ d ~depth:_ -> + match Sys.readdir path |> Array.to_list with + | contents -> !: contents +! mkOK + | exception Sys_error e -> ?: None +? (fail_or_mkERROR d e))), DocAbove); + LPDoc " -- Unix --"; MLData process; @@ -707,7 +817,7 @@ rex_split Rx S L :- rex.split Rx S L.|}; ;; (** ELPI specific NON-LOGICAL built-in *********************************** *) - + let safe = OpaqueData.declare { OpaqueData.name = "safe"; pp = (fun fmt (id,l) -> @@ -774,7 +884,7 @@ and same_term_list ~depth xs ys = | x::xs, y::ys -> same_term ~depth x y && same_term_list ~depth xs ys | _ -> false -let elpi_nonlogical_builtins = let open BuiltIn in let open BuiltInData in let open ContextualConversion in [ +let elpi_nonlogical_builtins = let open BuiltIn in let open BuiltInData in let open ContextualConversion in [ LPDoc "== Elpi nonlogical builtins ====================================="; @@ -1002,7 +1112,7 @@ if2 _ _ _ _ E :- !, E. |}; ] ;; -let elpi_stdlib_src = let open BuiltIn in [ +let elpi_stdlib_src = let open BuiltIn in [ LPCode Builtin_stdlib.code @@ -1010,7 +1120,7 @@ let elpi_stdlib_src = let open BuiltIn in [ let ocaml_set_conv ~name (type a) (type b) (alpha : a Conversion.t) (module Set : Util.Set.S with type elt = a and type t = b) = - + let set = OpaqueData.declare { OpaqueData.name; doc = ""; @@ -1023,7 +1133,7 @@ let set = OpaqueData.declare { let set = { set with Conversion.ty = Conversion.(TyName name) } in -let open BuiltIn in let open BuiltInData in +let open BuiltIn in let open BuiltInData in set, [ @@ -1140,7 +1250,7 @@ set, (fun m f _ ~once ~depth _ _ state -> let state, m, gls = HOAdaptors.filter1 ~once ~depth ~filter:Set.filter f m state in - + state, !: m, gls )), DocAbove); @@ -1153,7 +1263,7 @@ set, (fun m f _ ~once ~depth _ _ state -> let state, m, gls = HOAdaptors.map1 ~once ~depth ~map:Set.map f m state in - + state, !: m, gls )), DocAbove); @@ -1167,7 +1277,7 @@ set, (fun m a f _ ~once ~depth _ _ state -> let state, a, gls = HOAdaptors.fold1 ~once ~depth ~fold:Set.fold f m a state in - + state, !: a, gls )), DocAbove); @@ -1182,19 +1292,19 @@ set, (fun m f _ _ ~once ~depth _ _ state -> let state, (m1, m2), gls = HOAdaptors.filter1 ~once ~depth ~filter:Set.partition f m state in - + state, !: m1 +! m2, gls )), DocAbove); -] +] ;; let ocaml_set ~name c m = snd (ocaml_set_conv ~name c m) let ocaml_map ~name (type a) (alpha : a Conversion.t) (module Map : Util.Map.S with type key = a) = - + let closed_A = BuiltInData.closed "A" in let closed_B = BuiltInData.closed "B" in @@ -1211,7 +1321,7 @@ let map = OpaqueData.declare { let map a = { map with Conversion.ty = Conversion.(TyApp(name,TyName a,[])) } in -let open BuiltIn in let open BuiltInData in +let open BuiltIn in let open BuiltInData in [ LPDoc ("CAVEAT: the type parameter of "^name^" must be a closed term"); @@ -1273,7 +1383,7 @@ let open BuiltIn in let open BuiltInData in (fun m f _ ~once ~depth _ _ state -> let state, m, gls = HOAdaptors.filter2 ~once ~depth ~filter:Map.filter f m state in - + state, !: m, gls )), DocAbove); @@ -1286,7 +1396,7 @@ let open BuiltIn in let open BuiltInData in (fun m f _ ~once ~depth _ _ state -> let state, m, gls = HOAdaptors.map2 ~once ~depth ~map:Map.mapi f m state in - + state, !: m, gls )), DocAbove); @@ -1301,31 +1411,31 @@ let open BuiltIn in let open BuiltInData in (fun m a f _ ~once ~depth _ _ state -> let state, a, gls = HOAdaptors.fold2 ~once ~depth ~fold:Map.fold f m a state in - + state, !: a, gls )), DocAbove); -] +] ;; module LocMap : Util.Map.S with type key = Ast.Loc.t = Util.Map.Make(Ast.Loc) let elpi_map = let open BuiltIn in [ - + LPCode Builtin_map.code - + ] let elpi_set = let open BuiltIn in [ - + LPCode Builtin_set.code - + ] let string_set, string_set_decl = ocaml_set_conv ~name:"std.string.set" BuiltInData.string (module API.Compile.StrSet) let int_set, int_set_decl = ocaml_set_conv ~name:"std.int.set" BuiltInData.int (module API.Utils.IntSet) -let loc_set, loc_set_decl = ocaml_set_conv ~name:"std.loc.set" BuiltInData.loc (module API.Utils.LocSet) +let loc_set, loc_set_decl = ocaml_set_conv ~name:"std.loc.set" BuiltInData.loc (module API.Utils.LocSet) let elpi_stdlib = elpi_stdlib_src @ @@ -1339,11 +1449,11 @@ let elpi_stdlib = (fun sep l _ ~depth:_ -> !: (String.concat sep l))), DocAbove); ] @ - ocaml_map ~name:"std.string.map" BuiltInData.string (module Util.StrMap) @ - ocaml_map ~name:"std.int.map" BuiltInData.int (module Util.IntMap) @ - ocaml_map ~name:"std.loc.map" BuiltInData.loc (module LocMap) @ - string_set_decl @ - int_set_decl @ + ocaml_map ~name:"std.string.map" BuiltInData.string (module Util.StrMap) @ + ocaml_map ~name:"std.int.map" BuiltInData.int (module Util.IntMap) @ + ocaml_map ~name:"std.loc.map" BuiltInData.loc (module LocMap) @ + string_set_decl @ + int_set_decl @ loc_set_decl @ [] ;; From 5dccf2f1364e8dd5f63a6ba4aa5d5c75d68d2e46 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Sun, 9 Aug 2026 13:23:07 -0400 Subject: [PATCH 2/2] Update test fixtures --- tests/sources/trace_chr.json | 4 +- tests/sources/trace_w.elab.json | 270 ++++++++++++++++---------------- tests/sources/trace_w.json | 200 +++++++++++------------ 3 files changed, 237 insertions(+), 237 deletions(-) diff --git a/tests/sources/trace_chr.json b/tests/sources/trace_chr.json index 25cccc8b7..df927730d 100644 --- a/tests/sources/trace_chr.json +++ b/tests/sources/trace_chr.json @@ -96,7 +96,7 @@ {"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 1, column 21, characters 21-66:"," \\ (even A0) (odd A0) | (odd z) <=> (true)"]} -{"step":0,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--421 []"]} +{"step":0,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--430 []"]} {"step":0,"kind":["Info"],"goal_id":20,"runtime_id":1,"name":"user:newgoal","payload":["odd z"]} {"step":1,"kind":["Info"],"goal_id":20,"runtime_id":1,"name":"user:curgoal","payload":["odd","odd z"]} {"step":1,"kind":["Info"],"goal_id":20,"runtime_id":1,"name":"user:rule","payload":["backchain"]} @@ -104,7 +104,7 @@ {"step":1,"kind":["Info"],"goal_id":20,"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 2, column 45, characters 67-116:"," \\ (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--422 []"]} +{"step":0,"kind":["Info"],"goal_id":0,"runtime_id":2,"name":"user:assign","payload":["A0 := uvar frozen--431 []"]} {"step":0,"kind":["Info"],"goal_id":21,"runtime_id":2,"name":"user:newgoal","payload":["odd (s z)"]} {"step":1,"kind":["Info"],"goal_id":21,"runtime_id":2,"name":"user:curgoal","payload":["odd","odd (s z)"]} {"step":1,"kind":["Info"],"goal_id":21,"runtime_id":2,"name":"user:rule","payload":["backchain"]} diff --git a/tests/sources/trace_w.elab.json b/tests/sources/trace_w.elab.json index 44d76d14c..89c12c127 100644 --- a/tests/sources/trace_w.elab.json +++ b/tests/sources/trace_w.elab.json @@ -2029,7 +2029,7 @@ "step": [ "Init", { - "goal_text": "generalize [] [] (mono (uvar frozen--452 [] ===> uvar frozen--452 [])) X3", + "goal_text": "generalize [] [] (mono (uvar frozen--461 [] ===> uvar frozen--461 [])) X3", "goal_id": 26 } ], @@ -2042,7 +2042,7 @@ "Inference", { "current_goal_id": 26, - "current_goal_text": "generalize [] [] (mono (uvar frozen--452 [] ===> uvar frozen--452 [])) X3", + "current_goal_text": "generalize [] [] (mono (uvar frozen--461 [] ===> uvar frozen--461 [])) X3", "current_goal_predicate": "generalize", "failed_attempts": [], "successful_attempts": [ @@ -2068,14 +2068,14 @@ [ "Assign", "A2 := []" ], [ "Assign", - "A0 := uvar frozen--452 [] ===> uvar frozen--452 []" + "A0 := uvar frozen--461 [] ===> uvar frozen--461 []" ], [ "Assign", "A6 := X3" ] ] }, "siblings": [ { - "goal_text": "free-ty (mono (uvar frozen--452 [] ===> uvar frozen--452 [])) [] X4", + "goal_text": "free-ty (mono (uvar frozen--461 [] ===> uvar frozen--461 [])) [] X4", "goal_id": 27 }, { @@ -2087,7 +2087,7 @@ "goal_id": 29 }, { - "goal_text": "bind X6 [] (uvar frozen--452 [] ===> uvar frozen--452 []) X3", + "goal_text": "bind X6 [] (uvar frozen--461 [] ===> uvar frozen--461 []) X3", "goal_id": 30 } ], @@ -2127,7 +2127,7 @@ "Inference", { "current_goal_id": 27, - "current_goal_text": "free-ty (mono (uvar frozen--452 [] ===> uvar frozen--452 [])) [] X4", + "current_goal_text": "free-ty (mono (uvar frozen--461 [] ===> uvar frozen--461 [])) [] X4", "current_goal_predicate": "free-ty", "failed_attempts": [], "successful_attempts": [ @@ -2151,7 +2151,7 @@ "events": [ [ "Assign", - "A0 := uvar frozen--452 [] ===> uvar frozen--452 []" + "A0 := uvar frozen--461 [] ===> uvar frozen--461 []" ], [ "Assign", "A1 := []" ], [ "Assign", "A2 := X4" ] @@ -2159,7 +2159,7 @@ }, "siblings": [ { - "goal_text": "free (uvar frozen--452 [] ===> uvar frozen--452 []) [] X4", + "goal_text": "free (uvar frozen--461 [] ===> uvar frozen--461 []) [] X4", "goal_id": 31 } ], @@ -2218,7 +2218,7 @@ "Inference", { "current_goal_id": 31, - "current_goal_text": "free (uvar frozen--452 [] ===> uvar frozen--452 []) [] X4", + "current_goal_text": "free (uvar frozen--461 [] ===> uvar frozen--461 []) [] X4", "current_goal_predicate": "free", "failed_attempts": [], "successful_attempts": [ @@ -2240,19 +2240,19 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--452 []" ], - [ "Assign", "A3 := uvar frozen--452 []" ], + [ "Assign", "A0 := uvar frozen--461 []" ], + [ "Assign", "A3 := uvar frozen--461 []" ], [ "Assign", "A1 := []" ], [ "Assign", "A4 := X4" ] ] }, "siblings": [ { - "goal_text": "free (uvar frozen--452 []) [] X7", + "goal_text": "free (uvar frozen--461 []) [] X7", "goal_id": 32 }, { - "goal_text": "free (uvar frozen--452 []) X7 X4", + "goal_text": "free (uvar frozen--461 []) X7 X4", "goal_id": 33 } ], @@ -2330,7 +2330,7 @@ "Inference", { "current_goal_id": 32, - "current_goal_text": "free (uvar frozen--452 []) [] X7", + "current_goal_text": "free (uvar frozen--461 []) [] X7", "current_goal_predicate": "free", "failed_attempts": [], "successful_attempts": [ @@ -2352,14 +2352,14 @@ } ], "events": [ - [ "Assign", "A1 := uvar frozen--452 []" ], + [ "Assign", "A1 := uvar frozen--461 []" ], [ "Assign", "A0 := []" ], [ "Assign", "A2 := X7" ] ] }, "siblings": [ { - "goal_text": "if (mem [] (uvar frozen--452 [])) (X7 = []) (X7 = [uvar frozen--452 []])", + "goal_text": "if (mem [] (uvar frozen--461 [])) (X7 = []) (X7 = [uvar frozen--461 []])", "goal_id": 34 } ], @@ -2456,7 +2456,7 @@ "Inference", { "current_goal_id": 34, - "current_goal_text": "if (mem [] (uvar frozen--452 [])) (X7 = []) (X7 = [uvar frozen--452 []])", + "current_goal_text": "if (mem [] (uvar frozen--461 [])) (X7 = []) (X7 = [uvar frozen--461 []])", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -2470,9 +2470,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -2480,14 +2480,14 @@ "events": [ [ "Assign", - "A0 := mem [] (uvar frozen--452 [])" + "A0 := mem [] (uvar frozen--461 [])" ], [ "Assign", "A1 := X7 = []" ] ] }, "siblings": [ { - "goal_text": "mem [] (uvar frozen--452 [])", + "goal_text": "mem [] (uvar frozen--461 [])", "goal_id": 35 }, { "goal_text": "!", "goal_id": 36 }, @@ -2507,9 +2507,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -2605,7 +2605,7 @@ "Inference", { "current_goal_id": 35, - "current_goal_text": "mem [] (uvar frozen--452 [])", + "current_goal_text": "mem [] (uvar frozen--461 [])", "current_goal_predicate": "mem", "failed_attempts": [], "successful_attempts": [ @@ -2628,12 +2628,12 @@ ], "events": [ [ "Assign", "A0 := []" ], - [ "Assign", "A1 := frozen--452" ] + [ "Assign", "A1 := frozen--461" ] ] }, "siblings": [ { - "goal_text": "mem! [] (uvar frozen--452 X8)", + "goal_text": "mem! [] (uvar frozen--461 X8)", "goal_id": 38 } ], @@ -2670,9 +2670,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -2768,7 +2768,7 @@ "Inference", { "current_goal_id": 38, - "current_goal_text": "mem! [] (uvar frozen--452 X8)", + "current_goal_text": "mem! [] (uvar frozen--461 X8)", "current_goal_predicate": "mem!", "failed_attempts": [], "successful_attempts": [], @@ -2802,9 +2802,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -2900,7 +2900,7 @@ "Inference", { "current_goal_id": 34, - "current_goal_text": "if (mem [] (uvar frozen--452 [])) (X7 = []) (X7 = [uvar frozen--452 []])", + "current_goal_text": "if (mem [] (uvar frozen--461 [])) (X7 = []) (X7 = [uvar frozen--461 []])", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -2914,22 +2914,22 @@ "File", { "filename": "builtin.elpi", - "line": 537, + "line": 583, "column": 0, - "character": 13964 + "character": 16249 } ] } ], "events": [ [ - "Assign", "A0 := X7 = [uvar frozen--452 []]" + "Assign", "A0 := X7 = [uvar frozen--461 []]" ] ] }, "siblings": [ { - "goal_text": "X7 = [uvar frozen--452 []]", + "goal_text": "X7 = [uvar frozen--461 []]", "goal_id": 39 } ], @@ -2947,9 +2947,9 @@ "File", { "filename": "builtin.elpi", - "line": 537, + "line": 583, "column": 0, - "character": 13964 + "character": 16249 } ] } @@ -3045,7 +3045,7 @@ "Inference", { "current_goal_id": 39, - "current_goal_text": "X7 = [uvar frozen--452 []]", + "current_goal_text": "X7 = [uvar frozen--461 []]", "current_goal_predicate": "=", "failed_attempts": [], "successful_attempts": [ @@ -3060,7 +3060,7 @@ } ], "events": [ - [ "Assign", "X7 := [uvar frozen--452 []]" ] + [ "Assign", "X7 := [uvar frozen--461 []]" ] ] }, "siblings": [], @@ -3086,9 +3086,9 @@ "File", { "filename": "builtin.elpi", - "line": 537, + "line": 583, "column": 0, - "character": 13964 + "character": 16249 } ] } @@ -3184,7 +3184,7 @@ "Inference", { "current_goal_id": 33, - "current_goal_text": "free (uvar frozen--452 []) [uvar frozen--452 []] X4", + "current_goal_text": "free (uvar frozen--461 []) [uvar frozen--461 []] X4", "current_goal_predicate": "free", "failed_attempts": [], "successful_attempts": [ @@ -3206,14 +3206,14 @@ } ], "events": [ - [ "Assign", "A1 := uvar frozen--452 []" ], - [ "Assign", "A0 := [uvar frozen--452 []]" ], + [ "Assign", "A1 := uvar frozen--461 []" ], + [ "Assign", "A0 := [uvar frozen--461 []]" ], [ "Assign", "A2 := X4" ] ] }, "siblings": [ { - "goal_text": "if (mem [uvar frozen--452 []] (uvar frozen--452 [])) \n (X4 = [uvar frozen--452 []]) \n (X4 = [uvar frozen--452 [], uvar frozen--452 []])", + "goal_text": "if (mem [uvar frozen--461 []] (uvar frozen--461 [])) \n (X4 = [uvar frozen--461 []]) \n (X4 = [uvar frozen--461 [], uvar frozen--461 []])", "goal_id": 40 } ], @@ -3310,7 +3310,7 @@ "Inference", { "current_goal_id": 40, - "current_goal_text": "if (mem [uvar frozen--452 []] (uvar frozen--452 [])) \n (X4 = [uvar frozen--452 []]) \n (X4 = [uvar frozen--452 [], uvar frozen--452 []])", + "current_goal_text": "if (mem [uvar frozen--461 []] (uvar frozen--461 [])) \n (X4 = [uvar frozen--461 []]) \n (X4 = [uvar frozen--461 [], uvar frozen--461 []])", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -3324,9 +3324,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -3334,21 +3334,21 @@ "events": [ [ "Assign", - "A0 := mem [uvar frozen--452 []] (uvar frozen--452 [])" + "A0 := mem [uvar frozen--461 []] (uvar frozen--461 [])" ], [ - "Assign", "A1 := X4 = [uvar frozen--452 []]" + "Assign", "A1 := X4 = [uvar frozen--461 []]" ] ] }, "siblings": [ { - "goal_text": "mem [uvar frozen--452 []] (uvar frozen--452 [])", + "goal_text": "mem [uvar frozen--461 []] (uvar frozen--461 [])", "goal_id": 41 }, { "goal_text": "!", "goal_id": 42 }, { - "goal_text": "X4 = [uvar frozen--452 []]", + "goal_text": "X4 = [uvar frozen--461 []]", "goal_id": 43 } ], @@ -3366,9 +3366,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -3464,7 +3464,7 @@ "Inference", { "current_goal_id": 41, - "current_goal_text": "mem [uvar frozen--452 []] (uvar frozen--452 [])", + "current_goal_text": "mem [uvar frozen--461 []] (uvar frozen--461 [])", "current_goal_predicate": "mem", "failed_attempts": [], "successful_attempts": [ @@ -3486,13 +3486,13 @@ } ], "events": [ - [ "Assign", "A0 := [uvar frozen--452 []]" ], - [ "Assign", "A1 := frozen--452" ] + [ "Assign", "A0 := [uvar frozen--461 []]" ], + [ "Assign", "A1 := frozen--461" ] ] }, "siblings": [ { - "goal_text": "mem! [uvar frozen--452 []] (uvar frozen--452 X9)", + "goal_text": "mem! [uvar frozen--461 []] (uvar frozen--461 X9)", "goal_id": 44 } ], @@ -3529,9 +3529,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -3627,7 +3627,7 @@ "Inference", { "current_goal_id": 44, - "current_goal_text": "mem! [uvar frozen--452 []] (uvar frozen--452 X9)", + "current_goal_text": "mem! [uvar frozen--461 []] (uvar frozen--461 X9)", "current_goal_predicate": "mem!", "failed_attempts": [], "successful_attempts": [ @@ -3649,7 +3649,7 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--452 []" ], + [ "Assign", "A0 := uvar frozen--461 []" ], [ "Assign", "X9 := []" ] ] }, @@ -3706,9 +3706,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -3807,7 +3807,7 @@ "cut_victims": [ { "cut_branch_for_goal": { - "goal_text": "mem! [uvar frozen--452 []] (uvar frozen--452 X9)", + "goal_text": "mem! [uvar frozen--461 []] (uvar frozen--461 X9)", "goal_id": 44 }, "cut_branch": { @@ -3838,7 +3838,7 @@ "cut_victims": [ { "cut_branch_for_goal": { - "goal_text": "if (mem [uvar frozen--452 []] (uvar frozen--452 [])) \n (X4 = [uvar frozen--452 []]) \n (X4 = [uvar frozen--452 [], uvar frozen--452 []])", + "goal_text": "if (mem [uvar frozen--461 []] (uvar frozen--461 [])) \n (X4 = [uvar frozen--461 []]) \n (X4 = [uvar frozen--461 [], uvar frozen--461 []])", "goal_id": 40 }, "cut_branch": { @@ -3847,9 +3847,9 @@ "File", { "filename": "builtin.elpi", - "line": 537, + "line": 583, "column": 0, - "character": 13964 + "character": 16249 } ] } @@ -3866,7 +3866,7 @@ "Inference", { "current_goal_id": 43, - "current_goal_text": "X4 = [uvar frozen--452 []]", + "current_goal_text": "X4 = [uvar frozen--461 []]", "current_goal_predicate": "=", "failed_attempts": [], "successful_attempts": [ @@ -3881,7 +3881,7 @@ } ], "events": [ - [ "Assign", "X4 := [uvar frozen--452 []]" ] + [ "Assign", "X4 := [uvar frozen--461 []]" ] ] }, "siblings": [], @@ -3907,9 +3907,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -4087,7 +4087,7 @@ "Inference", { "current_goal_id": 29, - "current_goal_text": "filter [uvar frozen--452 []] (c0 \\ not (mem [] c0)) X6", + "current_goal_text": "filter [uvar frozen--461 []] (c0 \\ not (mem [] c0)) X6", "current_goal_predicate": "filter", "failed_attempts": [], "successful_attempts": [ @@ -4109,17 +4109,17 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--452 []" ], + [ "Assign", "A0 := uvar frozen--461 []" ], [ "Assign", "A2 := []" ], [ "Assign", "A1 := c0 \\\nnot (mem [] c0)" ], [ - "Assign", "X6 := [uvar frozen--452 [] | X10]" + "Assign", "X6 := [uvar frozen--461 [] | X10]" ] ] }, "siblings": [ { - "goal_text": "not (mem [] (uvar frozen--452 []))", + "goal_text": "not (mem [] (uvar frozen--461 []))", "goal_id": 46 }, { "goal_text": "!", "goal_id": 47 }, @@ -4183,7 +4183,7 @@ "Inference", { "current_goal_id": 46, - "current_goal_text": "not (mem [] (uvar frozen--452 []))", + "current_goal_text": "not (mem [] (uvar frozen--461 []))", "current_goal_predicate": "not", "failed_attempts": [], "successful_attempts": [ @@ -4207,13 +4207,13 @@ "events": [ [ "Assign", - "A0 := mem [] (uvar frozen--452 [])" + "A0 := mem [] (uvar frozen--461 [])" ] ] }, "siblings": [ { - "goal_text": "mem [] (uvar frozen--452 [])", + "goal_text": "mem [] (uvar frozen--461 [])", "goal_id": 49 }, { "goal_text": "!", "goal_id": 50 }, @@ -4293,7 +4293,7 @@ "Inference", { "current_goal_id": 49, - "current_goal_text": "mem [] (uvar frozen--452 [])", + "current_goal_text": "mem [] (uvar frozen--461 [])", "current_goal_predicate": "mem", "failed_attempts": [], "successful_attempts": [ @@ -4316,12 +4316,12 @@ ], "events": [ [ "Assign", "A0 := []" ], - [ "Assign", "A1 := frozen--452" ] + [ "Assign", "A1 := frozen--461" ] ] }, "siblings": [ { - "goal_text": "mem! [] (uvar frozen--452 X11)", + "goal_text": "mem! [] (uvar frozen--461 X11)", "goal_id": 52 } ], @@ -4418,7 +4418,7 @@ "Inference", { "current_goal_id": 52, - "current_goal_text": "mem! [] (uvar frozen--452 X11)", + "current_goal_text": "mem! [] (uvar frozen--461 X11)", "current_goal_predicate": "mem!", "failed_attempts": [], "successful_attempts": [], @@ -4512,7 +4512,7 @@ "Inference", { "current_goal_id": 46, - "current_goal_text": "not (mem [] (uvar frozen--452 []))", + "current_goal_text": "not (mem [] (uvar frozen--461 []))", "current_goal_predicate": "not", "failed_attempts": [], "successful_attempts": [ @@ -4739,7 +4739,7 @@ "Inference", { "current_goal_id": 30, - "current_goal_text": "bind [uvar frozen--452 []] [] (uvar frozen--452 [] ===> uvar frozen--452 []) \n X3", + "current_goal_text": "bind [uvar frozen--461 []] [] (uvar frozen--461 [] ===> uvar frozen--461 []) \n X3", "current_goal_predicate": "bind", "failed_attempts": [], "successful_attempts": [ @@ -4761,23 +4761,23 @@ } ], "events": [ - [ "Assign", "A1 := uvar frozen--452 []" ], + [ "Assign", "A1 := uvar frozen--461 []" ], [ "Assign", "A3 := []" ], [ "Assign", "A0 := []" ], [ "Assign", - "A4 := uvar frozen--452 [] ===> uvar frozen--452 []" + "A4 := uvar frozen--461 [] ===> uvar frozen--461 []" ], [ "Assign", "X3 := all X12 c0 \\ X13 c0" ] ] }, "siblings": [ { - "goal_text": "if (mem [] (uvar frozen--452 [])) (X12 = eqt) (X12 = any)", + "goal_text": "if (mem [] (uvar frozen--461 [])) (X12 = eqt) (X12 = any)", "goal_id": 53 }, { - "goal_text": "pi c0 \\\n copy (uvar frozen--452 []) c0 =>\n bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)", + "goal_text": "pi c0 \\\n copy (uvar frozen--461 []) c0 =>\n bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)", "goal_id": 54 } ], @@ -4836,7 +4836,7 @@ "Inference", { "current_goal_id": 53, - "current_goal_text": "if (mem [] (uvar frozen--452 [])) (X12 = eqt) (X12 = any)", + "current_goal_text": "if (mem [] (uvar frozen--461 [])) (X12 = eqt) (X12 = any)", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -4850,9 +4850,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -4860,14 +4860,14 @@ "events": [ [ "Assign", - "A0 := mem [] (uvar frozen--452 [])" + "A0 := mem [] (uvar frozen--461 [])" ], [ "Assign", "A1 := X12 = eqt" ] ] }, "siblings": [ { - "goal_text": "mem [] (uvar frozen--452 [])", + "goal_text": "mem [] (uvar frozen--461 [])", "goal_id": 55 }, { "goal_text": "!", "goal_id": 56 }, @@ -4887,9 +4887,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -4947,7 +4947,7 @@ "Inference", { "current_goal_id": 55, - "current_goal_text": "mem [] (uvar frozen--452 [])", + "current_goal_text": "mem [] (uvar frozen--461 [])", "current_goal_predicate": "mem", "failed_attempts": [], "successful_attempts": [ @@ -4970,12 +4970,12 @@ ], "events": [ [ "Assign", "A0 := []" ], - [ "Assign", "A1 := frozen--452" ] + [ "Assign", "A1 := frozen--461" ] ] }, "siblings": [ { - "goal_text": "mem! [] (uvar frozen--452 X14)", + "goal_text": "mem! [] (uvar frozen--461 X14)", "goal_id": 58 } ], @@ -5012,9 +5012,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -5072,7 +5072,7 @@ "Inference", { "current_goal_id": 58, - "current_goal_text": "mem! [] (uvar frozen--452 X14)", + "current_goal_text": "mem! [] (uvar frozen--461 X14)", "current_goal_predicate": "mem!", "failed_attempts": [], "successful_attempts": [], @@ -5106,9 +5106,9 @@ "File", { "filename": "builtin.elpi", - "line": 536, + "line": 582, "column": 0, - "character": 13943 + "character": 16228 } ] } @@ -5166,7 +5166,7 @@ "Inference", { "current_goal_id": 53, - "current_goal_text": "if (mem [] (uvar frozen--452 [])) (X12 = eqt) (X12 = any)", + "current_goal_text": "if (mem [] (uvar frozen--461 [])) (X12 = eqt) (X12 = any)", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -5180,9 +5180,9 @@ "File", { "filename": "builtin.elpi", - "line": 537, + "line": 583, "column": 0, - "character": 13964 + "character": 16249 } ] } @@ -5206,9 +5206,9 @@ "File", { "filename": "builtin.elpi", - "line": 537, + "line": 583, "column": 0, - "character": 13964 + "character": 16249 } ] } @@ -5305,9 +5305,9 @@ "File", { "filename": "builtin.elpi", - "line": 537, + "line": 583, "column": 0, - "character": 13964 + "character": 16249 } ] } @@ -5365,7 +5365,7 @@ "Inference", { "current_goal_id": 54, - "current_goal_text": "pi c0 \\\n copy (uvar frozen--452 []) c0 =>\n bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)", + "current_goal_text": "pi c0 \\\n copy (uvar frozen--461 []) c0 =>\n bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)", "current_goal_predicate": "pi", "failed_attempts": [], "successful_attempts": [ @@ -5383,7 +5383,7 @@ }, "siblings": [ { - "goal_text": "copy (uvar frozen--452 []) c0 =>\n bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)", + "goal_text": "copy (uvar frozen--461 []) c0 =>\n bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)", "goal_id": 60 } ], @@ -5454,7 +5454,7 @@ "Inference", { "current_goal_id": 60, - "current_goal_text": "copy (uvar frozen--452 []) c0 =>\n bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)", + "current_goal_text": "copy (uvar frozen--461 []) c0 =>\n bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)", "current_goal_predicate": "=>", "failed_attempts": [], "successful_attempts": [ @@ -5472,7 +5472,7 @@ }, "siblings": [ { - "goal_text": "bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)", + "goal_text": "bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)", "goal_id": 61 } ], @@ -5488,7 +5488,7 @@ "name": "implication", "kind": "Logic", "payload": [ - "(copy (uvar frozen--452 []) c0) :- ." + "(copy (uvar frozen--461 []) c0) :- ." ] } ], @@ -5557,7 +5557,7 @@ "Inference", { "current_goal_id": 61, - "current_goal_text": "bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)", + "current_goal_text": "bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)", "current_goal_predicate": "bind", "failed_attempts": [], "successful_attempts": [ @@ -5581,7 +5581,7 @@ "events": [ [ "Assign", - "A0 := uvar frozen--452 [] ===> uvar frozen--452 []" + "A0 := uvar frozen--461 [] ===> uvar frozen--461 []" ], [ "Assign", "X13 := c0 \\\nX15 c0" ], [ "Assign", "X15^1 := mono X16^1" ] @@ -5589,7 +5589,7 @@ }, "siblings": [ { - "goal_text": "copy (uvar frozen--452 [] ===> uvar frozen--452 []) X16^1", + "goal_text": "copy (uvar frozen--461 [] ===> uvar frozen--461 []) X16^1", "goal_id": 62 } ], @@ -5624,7 +5624,7 @@ "name": "implication", "kind": "Logic", "payload": [ - "(copy (uvar frozen--452 []) c0) :- ." + "(copy (uvar frozen--461 []) c0) :- ." ] } ], @@ -5693,7 +5693,7 @@ "Inference", { "current_goal_id": 62, - "current_goal_text": "copy (uvar frozen--452 [] ===> uvar frozen--452 []) X16^1", + "current_goal_text": "copy (uvar frozen--461 [] ===> uvar frozen--461 []) X16^1", "current_goal_predicate": "copy", "failed_attempts": [], "successful_attempts": [ @@ -5715,18 +5715,18 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--452 []" ], - [ "Assign", "A2 := uvar frozen--452 []" ], + [ "Assign", "A0 := uvar frozen--461 []" ], + [ "Assign", "A2 := uvar frozen--461 []" ], [ "Assign", "X16^1 := X17^1 ===> X18^1" ] ] }, "siblings": [ { - "goal_text": "copy (uvar frozen--452 []) X17^1", + "goal_text": "copy (uvar frozen--461 []) X17^1", "goal_id": 63 }, { - "goal_text": "copy (uvar frozen--452 []) X18^1", + "goal_text": "copy (uvar frozen--461 []) X18^1", "goal_id": 64 } ], @@ -5780,7 +5780,7 @@ "name": "implication", "kind": "Logic", "payload": [ - "(copy (uvar frozen--452 []) c0) :- ." + "(copy (uvar frozen--461 []) c0) :- ." ] } ], @@ -5849,7 +5849,7 @@ "Inference", { "current_goal_id": 63, - "current_goal_text": "copy (uvar frozen--452 []) X17^1", + "current_goal_text": "copy (uvar frozen--461 []) X17^1", "current_goal_predicate": "copy", "failed_attempts": [], "successful_attempts": [ @@ -5858,7 +5858,7 @@ "rule": [ "UserRule", { - "rule_text": "(copy (uvar frozen--452 []) c0) :- .", + "rule_text": "(copy (uvar frozen--461 []) c0) :- .", "rule_loc": [ "Context", 32 ] } ], @@ -5874,7 +5874,7 @@ "rule": [ "UserRule", { - "rule_text": "(copy (uvar frozen--452 []) c0) :- .", + "rule_text": "(copy (uvar frozen--461 []) c0) :- .", "rule_loc": [ "Context", 32 ] } ], @@ -5926,7 +5926,7 @@ "name": "implication", "kind": "Logic", "payload": [ - "(copy (uvar frozen--452 []) c0) :- ." + "(copy (uvar frozen--461 []) c0) :- ." ] } ], @@ -5995,7 +5995,7 @@ "Inference", { "current_goal_id": 64, - "current_goal_text": "copy (uvar frozen--452 []) X18^1", + "current_goal_text": "copy (uvar frozen--461 []) X18^1", "current_goal_predicate": "copy", "failed_attempts": [], "successful_attempts": [ @@ -6004,7 +6004,7 @@ "rule": [ "UserRule", { - "rule_text": "(copy (uvar frozen--452 []) c0) :- .", + "rule_text": "(copy (uvar frozen--461 []) c0) :- .", "rule_loc": [ "Context", 32 ] } ], @@ -6020,7 +6020,7 @@ "rule": [ "UserRule", { - "rule_text": "(copy (uvar frozen--452 []) c0) :- .", + "rule_text": "(copy (uvar frozen--461 []) c0) :- .", "rule_loc": [ "Context", 32 ] } ], @@ -6072,7 +6072,7 @@ "name": "implication", "kind": "Logic", "payload": [ - "(copy (uvar frozen--452 []) c0) :- ." + "(copy (uvar frozen--461 []) c0) :- ." ] } ], diff --git a/tests/sources/trace_w.json b/tests/sources/trace_w.json index 23f815720..6fb62564e 100644 --- a/tests/sources/trace_w.json +++ b/tests/sources/trace_w.json @@ -135,136 +135,136 @@ {"step":16,"kind":["Info"],"goal_id":24,"runtime_id":0,"name":"user:rule:builtin","payload":["success"]} {"step":17,"kind":["Info"],"goal_id":25,"runtime_id":0,"name":"user:CHR:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 85, column 36, characters 2027-2199:","(theta A0) \\ (A1 ?- gammabar A2 A3) | (generalize A0 A1 A2 A4) <=> (A3 = A4)"]} {"step":0,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X0 := []"]} -{"step":0,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X1 := mono (uvar frozen--452 [] ===> uvar frozen--452 [])"]} -{"step":0,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A3 := uvar frozen--453 []"]} +{"step":0,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X1 := mono (uvar frozen--461 [] ===> uvar frozen--461 [])"]} +{"step":0,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A3 := uvar frozen--462 []"]} {"step":0,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X2 := []"]} -{"step":0,"kind":["Info"],"goal_id":26,"runtime_id":1,"name":"user:newgoal","payload":["generalize [] [] (mono (uvar frozen--452 [] ===> uvar frozen--452 [])) X3"]} -{"step":1,"kind":["Info"],"goal_id":26,"runtime_id":1,"name":"user:curgoal","payload":["generalize","generalize [] [] (mono (uvar frozen--452 [] ===> uvar frozen--452 [])) X3"]} +{"step":0,"kind":["Info"],"goal_id":26,"runtime_id":1,"name":"user:newgoal","payload":["generalize [] [] (mono (uvar frozen--461 [] ===> uvar frozen--461 [])) X3"]} +{"step":1,"kind":["Info"],"goal_id":26,"runtime_id":1,"name":"user:curgoal","payload":["generalize","generalize [] [] (mono (uvar frozen--461 [] ===> uvar frozen--461 [])) X3"]} {"step":1,"kind":["Info"],"goal_id":26,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":1,"kind":["Info"],"goal_id":26,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 97, column 0, characters 2346-2521:"]} {"step":1,"kind":["Info"],"goal_id":26,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 97, column 0, characters 2346-2521:","(generalize A5 A2 (mono A0) A6) :- (free-ty (mono A0) [] A1), \n (free-gamma A2 [] A3), (filter A1 (c0 \\ (not (mem A3 c0))) A4), \n (bind A4 A5 A0 A6)."]} {"step":1,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A5 := []"]} {"step":1,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A2 := []"]} -{"step":1,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--452 [] ===> uvar frozen--452 []"]} +{"step":1,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--461 [] ===> uvar frozen--461 []"]} {"step":1,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A6 := X3"]} {"step":1,"kind":["Info"],"goal_id":26,"runtime_id":1,"name":"user:subgoal","payload":["27"]} -{"step":1,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:newgoal","payload":["free-ty (mono (uvar frozen--452 [] ===> uvar frozen--452 [])) [] X4"]} +{"step":1,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:newgoal","payload":["free-ty (mono (uvar frozen--461 [] ===> uvar frozen--461 [])) [] X4"]} {"step":1,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:subgoal","payload":["28"]} {"step":1,"kind":["Info"],"goal_id":28,"runtime_id":1,"name":"user:newgoal","payload":["free-gamma [] [] X5"]} {"step":1,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:subgoal","payload":["29"]} {"step":1,"kind":["Info"],"goal_id":29,"runtime_id":1,"name":"user:newgoal","payload":["filter X4 (c0 \\ not (mem X5 c0)) X6"]} {"step":1,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:subgoal","payload":["30"]} -{"step":1,"kind":["Info"],"goal_id":30,"runtime_id":1,"name":"user:newgoal","payload":["bind X6 [] (uvar frozen--452 [] ===> uvar frozen--452 []) X3"]} +{"step":1,"kind":["Info"],"goal_id":30,"runtime_id":1,"name":"user:newgoal","payload":["bind X6 [] (uvar frozen--461 [] ===> uvar frozen--461 []) X3"]} {"step":1,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":2,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:curgoal","payload":["free-ty","free-ty (mono (uvar frozen--452 [] ===> uvar frozen--452 [])) [] X4"]} +{"step":2,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:curgoal","payload":["free-ty","free-ty (mono (uvar frozen--461 [] ===> uvar frozen--461 [])) [] X4"]} {"step":2,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":2,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 105, column 0, characters 2637-2673:"]} {"step":2,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 105, column 0, characters 2637-2673:","(free-ty (mono A0) A1 A2) :- (free A0 A1 A2)."]} -{"step":2,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--452 [] ===> uvar frozen--452 []"]} +{"step":2,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--461 [] ===> uvar frozen--461 []"]} {"step":2,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := []"]} {"step":2,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A2 := X4"]} {"step":2,"kind":["Info"],"goal_id":27,"runtime_id":1,"name":"user:subgoal","payload":["31"]} -{"step":2,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:newgoal","payload":["free (uvar frozen--452 [] ===> uvar frozen--452 []) [] X4"]} +{"step":2,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:newgoal","payload":["free (uvar frozen--461 [] ===> uvar frozen--461 []) [] X4"]} {"step":2,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":3,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:curgoal","payload":["free","free (uvar frozen--452 [] ===> uvar frozen--452 []) [] X4"]} +{"step":3,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:curgoal","payload":["free","free (uvar frozen--461 [] ===> uvar frozen--461 []) [] X4"]} {"step":3,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":3,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 117, column 0, characters 3023-3072:"]} {"step":3,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 117, column 0, characters 3023-3072:","(free (A0 ===> A3) A1 A4) :- (free A0 A1 A2), (free A3 A2 A4)."]} -{"step":3,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--452 []"]} -{"step":3,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A3 := uvar frozen--452 []"]} +{"step":3,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--461 []"]} +{"step":3,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A3 := uvar frozen--461 []"]} {"step":3,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := []"]} {"step":3,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A4 := X4"]} {"step":3,"kind":["Info"],"goal_id":31,"runtime_id":1,"name":"user:subgoal","payload":["32"]} -{"step":3,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:newgoal","payload":["free (uvar frozen--452 []) [] X7"]} +{"step":3,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:newgoal","payload":["free (uvar frozen--461 []) [] X7"]} {"step":3,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:subgoal","payload":["33"]} -{"step":3,"kind":["Info"],"goal_id":33,"runtime_id":1,"name":"user:newgoal","payload":["free (uvar frozen--452 []) X7 X4"]} +{"step":3,"kind":["Info"],"goal_id":33,"runtime_id":1,"name":"user:newgoal","payload":["free (uvar frozen--461 []) X7 X4"]} {"step":3,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":4,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:curgoal","payload":["free","free (uvar frozen--452 []) [] X7"]} +{"step":4,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:curgoal","payload":["free","free (uvar frozen--461 []) [] X7"]} {"step":4,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":4,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 118, column 0, characters 3074-3137:"]} {"step":4,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 118, column 0, characters 3074-3137:","(free (as (uvar _ _) A1) A0 A2) :- (if (mem A0 A1) (A2 = A0) (A2 = [A1 | A0]))."]} -{"step":4,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := uvar frozen--452 []"]} +{"step":4,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := uvar frozen--461 []"]} {"step":4,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := []"]} {"step":4,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A2 := X7"]} {"step":4,"kind":["Info"],"goal_id":32,"runtime_id":1,"name":"user:subgoal","payload":["34"]} -{"step":4,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:newgoal","payload":["if (mem [] (uvar frozen--452 [])) (X7 = []) (X7 = [uvar frozen--452 []])"]} +{"step":4,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:newgoal","payload":["if (mem [] (uvar frozen--461 [])) (X7 = []) (X7 = [uvar frozen--461 []])"]} {"step":4,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":5,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [] (uvar frozen--452 [])) (X7 = []) (X7 = [uvar frozen--452 []])"]} +{"step":5,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [] (uvar frozen--461 [])) (X7 = []) (X7 = [uvar frozen--461 []])"]} {"step":5,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule","payload":["backchain"]} -{"step":5,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 536, column 0, characters 13943-13962:","File \"builtin.elpi\", line 537, column 0, characters 13964-13977:"]} -{"step":5,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 536, column 0, characters 13943-13962:","(if A0 A1 _) :- A0, !, A1."]} -{"step":5,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := mem [] (uvar frozen--452 [])"]} +{"step":5,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 582, column 0, characters 16228-16247:","File \"builtin.elpi\", line 583, column 0, characters 16249-16262:"]} +{"step":5,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 582, column 0, characters 16228-16247:","(if A0 A1 _) :- A0, !, A1."]} +{"step":5,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := mem [] (uvar frozen--461 [])"]} {"step":5,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := X7 = []"]} {"step":5,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:subgoal","payload":["35"]} -{"step":5,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:newgoal","payload":["mem [] (uvar frozen--452 [])"]} +{"step":5,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:newgoal","payload":["mem [] (uvar frozen--461 [])"]} {"step":5,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:subgoal","payload":["36"]} {"step":5,"kind":["Info"],"goal_id":36,"runtime_id":1,"name":"user:newgoal","payload":["!"]} {"step":5,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:subgoal","payload":["37"]} {"step":5,"kind":["Info"],"goal_id":37,"runtime_id":1,"name":"user:newgoal","payload":["X7 = []"]} {"step":5,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":6,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:curgoal","payload":["mem","mem [] (uvar frozen--452 [])"]} +{"step":6,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:curgoal","payload":["mem","mem [] (uvar frozen--461 [])"]} {"step":6,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":6,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 148, column 0, characters 4032-4074:"]} {"step":6,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 148, column 0, characters 4032-4074:","(mem A0 (uvar A1 _)) :- (mem! A0 (uvar A1 A2))."]} {"step":6,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := []"]} -{"step":6,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := frozen--452"]} +{"step":6,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := frozen--461"]} {"step":6,"kind":["Info"],"goal_id":35,"runtime_id":1,"name":"user:subgoal","payload":["38"]} -{"step":6,"kind":["Info"],"goal_id":38,"runtime_id":1,"name":"user:newgoal","payload":["mem! [] (uvar frozen--452 X8)"]} +{"step":6,"kind":["Info"],"goal_id":38,"runtime_id":1,"name":"user:newgoal","payload":["mem! [] (uvar frozen--461 X8)"]} {"step":6,"kind":["Info"],"goal_id":38,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":7,"kind":["Info"],"goal_id":38,"runtime_id":1,"name":"user:curgoal","payload":["mem!","mem! [] (uvar frozen--452 X8)"]} +{"step":7,"kind":["Info"],"goal_id":38,"runtime_id":1,"name":"user:curgoal","payload":["mem!","mem! [] (uvar frozen--461 X8)"]} {"step":7,"kind":["Info"],"goal_id":38,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":7,"kind":["Info"],"goal_id":38,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":[]} {"step":7,"kind":["Info"],"goal_id":38,"runtime_id":1,"name":"user:rule:backchain","payload":["fail"]} -{"step":8,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [] (uvar frozen--452 [])) (X7 = []) (X7 = [uvar frozen--452 []])"]} +{"step":8,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [] (uvar frozen--461 [])) (X7 = []) (X7 = [uvar frozen--461 []])"]} {"step":8,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule","payload":["backchain"]} -{"step":8,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 537, column 0, characters 13964-13977:"]} -{"step":8,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 537, column 0, characters 13964-13977:","(if _ _ A0) :- A0."]} -{"step":8,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := X7 = [uvar frozen--452 []]"]} +{"step":8,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 583, column 0, characters 16249-16262:"]} +{"step":8,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 583, column 0, characters 16249-16262:","(if _ _ A0) :- A0."]} +{"step":8,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := X7 = [uvar frozen--461 []]"]} {"step":8,"kind":["Info"],"goal_id":34,"runtime_id":1,"name":"user:subgoal","payload":["39"]} -{"step":8,"kind":["Info"],"goal_id":39,"runtime_id":1,"name":"user:newgoal","payload":["X7 = [uvar frozen--452 []]"]} +{"step":8,"kind":["Info"],"goal_id":39,"runtime_id":1,"name":"user:newgoal","payload":["X7 = [uvar frozen--461 []]"]} {"step":8,"kind":["Info"],"goal_id":39,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":9,"kind":["Info"],"goal_id":39,"runtime_id":1,"name":"user:curgoal","payload":["=","X7 = [uvar frozen--452 []]"]} +{"step":9,"kind":["Info"],"goal_id":39,"runtime_id":1,"name":"user:curgoal","payload":["=","X7 = [uvar frozen--461 []]"]} {"step":9,"kind":["Info"],"goal_id":39,"runtime_id":1,"name":"user:rule","payload":["eq"]} {"step":9,"kind":["Info"],"goal_id":39,"runtime_id":1,"name":"user:rule:builtin:name","payload":["="]} -{"step":9,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X7 := [uvar frozen--452 []]"]} +{"step":9,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X7 := [uvar frozen--461 []]"]} {"step":9,"kind":["Info"],"goal_id":39,"runtime_id":1,"name":"user:rule:eq","payload":["success"]} -{"step":10,"kind":["Info"],"goal_id":33,"runtime_id":1,"name":"user:curgoal","payload":["free","free (uvar frozen--452 []) [uvar frozen--452 []] X4"]} +{"step":10,"kind":["Info"],"goal_id":33,"runtime_id":1,"name":"user:curgoal","payload":["free","free (uvar frozen--461 []) [uvar frozen--461 []] X4"]} {"step":10,"kind":["Info"],"goal_id":33,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":10,"kind":["Info"],"goal_id":33,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 118, column 0, characters 3074-3137:"]} {"step":10,"kind":["Info"],"goal_id":33,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 118, column 0, characters 3074-3137:","(free (as (uvar _ _) A1) A0 A2) :- (if (mem A0 A1) (A2 = A0) (A2 = [A1 | A0]))."]} -{"step":10,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := uvar frozen--452 []"]} -{"step":10,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := [uvar frozen--452 []]"]} +{"step":10,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := uvar frozen--461 []"]} +{"step":10,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := [uvar frozen--461 []]"]} {"step":10,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A2 := X4"]} {"step":10,"kind":["Info"],"goal_id":33,"runtime_id":1,"name":"user:subgoal","payload":["40"]} -{"step":10,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:newgoal","payload":["if (mem [uvar frozen--452 []] (uvar frozen--452 [])) \n (X4 = [uvar frozen--452 []]) \n (X4 = [uvar frozen--452 [], uvar frozen--452 []])"]} +{"step":10,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:newgoal","payload":["if (mem [uvar frozen--461 []] (uvar frozen--461 [])) \n (X4 = [uvar frozen--461 []]) \n (X4 = [uvar frozen--461 [], uvar frozen--461 []])"]} {"step":10,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":11,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [uvar frozen--452 []] (uvar frozen--452 [])) \n (X4 = [uvar frozen--452 []]) \n (X4 = [uvar frozen--452 [], uvar frozen--452 []])"]} +{"step":11,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [uvar frozen--461 []] (uvar frozen--461 [])) \n (X4 = [uvar frozen--461 []]) \n (X4 = [uvar frozen--461 [], uvar frozen--461 []])"]} {"step":11,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:rule","payload":["backchain"]} -{"step":11,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 536, column 0, characters 13943-13962:","File \"builtin.elpi\", line 537, column 0, characters 13964-13977:"]} -{"step":11,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 536, column 0, characters 13943-13962:","(if A0 A1 _) :- A0, !, A1."]} -{"step":11,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := mem [uvar frozen--452 []] (uvar frozen--452 [])"]} -{"step":11,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := X4 = [uvar frozen--452 []]"]} +{"step":11,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 582, column 0, characters 16228-16247:","File \"builtin.elpi\", line 583, column 0, characters 16249-16262:"]} +{"step":11,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 582, column 0, characters 16228-16247:","(if A0 A1 _) :- A0, !, A1."]} +{"step":11,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := mem [uvar frozen--461 []] (uvar frozen--461 [])"]} +{"step":11,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := X4 = [uvar frozen--461 []]"]} {"step":11,"kind":["Info"],"goal_id":40,"runtime_id":1,"name":"user:subgoal","payload":["41"]} -{"step":11,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:newgoal","payload":["mem [uvar frozen--452 []] (uvar frozen--452 [])"]} +{"step":11,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:newgoal","payload":["mem [uvar frozen--461 []] (uvar frozen--461 [])"]} {"step":11,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:subgoal","payload":["42"]} {"step":11,"kind":["Info"],"goal_id":42,"runtime_id":1,"name":"user:newgoal","payload":["!"]} {"step":11,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:subgoal","payload":["43"]} -{"step":11,"kind":["Info"],"goal_id":43,"runtime_id":1,"name":"user:newgoal","payload":["X4 = [uvar frozen--452 []]"]} +{"step":11,"kind":["Info"],"goal_id":43,"runtime_id":1,"name":"user:newgoal","payload":["X4 = [uvar frozen--461 []]"]} {"step":11,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":12,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:curgoal","payload":["mem","mem [uvar frozen--452 []] (uvar frozen--452 [])"]} +{"step":12,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:curgoal","payload":["mem","mem [uvar frozen--461 []] (uvar frozen--461 [])"]} {"step":12,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":12,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 148, column 0, characters 4032-4074:"]} {"step":12,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 148, column 0, characters 4032-4074:","(mem A0 (uvar A1 _)) :- (mem! A0 (uvar A1 A2))."]} -{"step":12,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := [uvar frozen--452 []]"]} -{"step":12,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := frozen--452"]} +{"step":12,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := [uvar frozen--461 []]"]} +{"step":12,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := frozen--461"]} {"step":12,"kind":["Info"],"goal_id":41,"runtime_id":1,"name":"user:subgoal","payload":["44"]} -{"step":12,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:newgoal","payload":["mem! [uvar frozen--452 []] (uvar frozen--452 X9)"]} +{"step":12,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:newgoal","payload":["mem! [uvar frozen--461 []] (uvar frozen--461 X9)"]} {"step":12,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":13,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:curgoal","payload":["mem!","mem! [uvar frozen--452 []] (uvar frozen--452 X9)"]} +{"step":13,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:curgoal","payload":["mem!","mem! [uvar frozen--461 []] (uvar frozen--461 X9)"]} {"step":13,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":13,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 143, column 0, characters 3903-3920:","File \"tests/sources/trace-w/main.elpi\", line 144, column 0, characters 3922-3948:"]} {"step":13,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 143, column 0, characters 3903-3920:","(mem! [A0 | _] A0) :- !."]} -{"step":13,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--452 []"]} +{"step":13,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--461 []"]} {"step":13,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X9 := []"]} {"step":13,"kind":["Info"],"goal_id":44,"runtime_id":1,"name":"user:subgoal","payload":["45"]} {"step":13,"kind":["Info"],"goal_id":45,"runtime_id":1,"name":"user:newgoal","payload":["!"]} @@ -275,12 +275,12 @@ {"step":14,"kind":["Info"],"goal_id":45,"runtime_id":1,"name":"user:rule:cut","payload":["success"]} {"step":15,"kind":["Info"],"goal_id":42,"runtime_id":1,"name":"user:curgoal","payload":["!","!"]} {"step":15,"kind":["Info"],"goal_id":42,"runtime_id":1,"name":"user:rule","payload":["cut"]} -{"step":15,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:rule:cut:branch","payload":["40","File \"builtin.elpi\", line 537, column 0, characters 13964-13977:","(if _ _ A0) :- A0."]} +{"step":15,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:rule:cut:branch","payload":["40","File \"builtin.elpi\", line 583, column 0, characters 16249-16262:","(if _ _ A0) :- A0."]} {"step":15,"kind":["Info"],"goal_id":42,"runtime_id":1,"name":"user:rule:cut","payload":["success"]} -{"step":16,"kind":["Info"],"goal_id":43,"runtime_id":1,"name":"user:curgoal","payload":["=","X4 = [uvar frozen--452 []]"]} +{"step":16,"kind":["Info"],"goal_id":43,"runtime_id":1,"name":"user:curgoal","payload":["=","X4 = [uvar frozen--461 []]"]} {"step":16,"kind":["Info"],"goal_id":43,"runtime_id":1,"name":"user:rule","payload":["eq"]} {"step":16,"kind":["Info"],"goal_id":43,"runtime_id":1,"name":"user:rule:builtin:name","payload":["="]} -{"step":16,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X4 := [uvar frozen--452 []]"]} +{"step":16,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X4 := [uvar frozen--461 []]"]} {"step":16,"kind":["Info"],"goal_id":43,"runtime_id":1,"name":"user:rule:eq","payload":["success"]} {"step":17,"kind":["Info"],"goal_id":28,"runtime_id":1,"name":"user:curgoal","payload":["free-gamma","free-gamma [] [] X5"]} {"step":17,"kind":["Info"],"goal_id":28,"runtime_id":1,"name":"user:rule","payload":["backchain"]} @@ -289,47 +289,47 @@ {"step":17,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := []"]} {"step":17,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X5 := []"]} {"step":17,"kind":["Info"],"goal_id":28,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":18,"kind":["Info"],"goal_id":29,"runtime_id":1,"name":"user:curgoal","payload":["filter","filter [uvar frozen--452 []] (c0 \\ not (mem [] c0)) X6"]} +{"step":18,"kind":["Info"],"goal_id":29,"runtime_id":1,"name":"user:curgoal","payload":["filter","filter [uvar frozen--461 []] (c0 \\ not (mem [] c0)) X6"]} {"step":18,"kind":["Info"],"goal_id":29,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":18,"kind":["Info"],"goal_id":29,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 139, column 0, characters 3789-3837:","File \"tests/sources/trace-w/main.elpi\", line 140, column 0, characters 3839-3875:"]} {"step":18,"kind":["Info"],"goal_id":29,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 139, column 0, characters 3789-3837:","(filter [A0 | A2] A1 [A0 | A3]) :- (A1 A0), !, (filter A2 A1 A3)."]} -{"step":18,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--452 []"]} +{"step":18,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--461 []"]} {"step":18,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A2 := []"]} {"step":18,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := c0 \\\nnot (mem [] c0)"]} -{"step":18,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X6 := [uvar frozen--452 [] | X10]"]} +{"step":18,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X6 := [uvar frozen--461 [] | X10]"]} {"step":18,"kind":["Info"],"goal_id":29,"runtime_id":1,"name":"user:subgoal","payload":["46"]} -{"step":18,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:newgoal","payload":["not (mem [] (uvar frozen--452 []))"]} +{"step":18,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:newgoal","payload":["not (mem [] (uvar frozen--461 []))"]} {"step":18,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:subgoal","payload":["47"]} {"step":18,"kind":["Info"],"goal_id":47,"runtime_id":1,"name":"user:newgoal","payload":["!"]} {"step":18,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:subgoal","payload":["48"]} {"step":18,"kind":["Info"],"goal_id":48,"runtime_id":1,"name":"user:newgoal","payload":["filter [] (c0 \\ not (mem [] c0)) X10"]} {"step":18,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":19,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:curgoal","payload":["not","not (mem [] (uvar frozen--452 []))"]} +{"step":19,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:curgoal","payload":["not","not (mem [] (uvar frozen--461 []))"]} {"step":19,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":19,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 69, column 0, characters 1189-1208:","File \"builtin.elpi\", line 71, column 0, characters 1211-1216:"]} {"step":19,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 69, column 0, characters 1189-1208:","(not A0) :- A0, !, fail."]} -{"step":19,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := mem [] (uvar frozen--452 [])"]} +{"step":19,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := mem [] (uvar frozen--461 [])"]} {"step":19,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:subgoal","payload":["49"]} -{"step":19,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:newgoal","payload":["mem [] (uvar frozen--452 [])"]} +{"step":19,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:newgoal","payload":["mem [] (uvar frozen--461 [])"]} {"step":19,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:subgoal","payload":["50"]} {"step":19,"kind":["Info"],"goal_id":50,"runtime_id":1,"name":"user:newgoal","payload":["!"]} {"step":19,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:subgoal","payload":["51"]} {"step":19,"kind":["Info"],"goal_id":51,"runtime_id":1,"name":"user:newgoal","payload":["fail"]} {"step":19,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":20,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:curgoal","payload":["mem","mem [] (uvar frozen--452 [])"]} +{"step":20,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:curgoal","payload":["mem","mem [] (uvar frozen--461 [])"]} {"step":20,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":20,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 148, column 0, characters 4032-4074:"]} {"step":20,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 148, column 0, characters 4032-4074:","(mem A0 (uvar A1 _)) :- (mem! A0 (uvar A1 A2))."]} {"step":20,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := []"]} -{"step":20,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := frozen--452"]} +{"step":20,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := frozen--461"]} {"step":20,"kind":["Info"],"goal_id":49,"runtime_id":1,"name":"user:subgoal","payload":["52"]} -{"step":20,"kind":["Info"],"goal_id":52,"runtime_id":1,"name":"user:newgoal","payload":["mem! [] (uvar frozen--452 X11)"]} +{"step":20,"kind":["Info"],"goal_id":52,"runtime_id":1,"name":"user:newgoal","payload":["mem! [] (uvar frozen--461 X11)"]} {"step":20,"kind":["Info"],"goal_id":52,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":21,"kind":["Info"],"goal_id":52,"runtime_id":1,"name":"user:curgoal","payload":["mem!","mem! [] (uvar frozen--452 X11)"]} +{"step":21,"kind":["Info"],"goal_id":52,"runtime_id":1,"name":"user:curgoal","payload":["mem!","mem! [] (uvar frozen--461 X11)"]} {"step":21,"kind":["Info"],"goal_id":52,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":21,"kind":["Info"],"goal_id":52,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":[]} {"step":21,"kind":["Info"],"goal_id":52,"runtime_id":1,"name":"user:rule:backchain","payload":["fail"]} -{"step":22,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:curgoal","payload":["not","not (mem [] (uvar frozen--452 []))"]} +{"step":22,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:curgoal","payload":["not","not (mem [] (uvar frozen--461 []))"]} {"step":22,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":22,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 71, column 0, characters 1211-1216:"]} {"step":22,"kind":["Info"],"goal_id":46,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 71, column 0, characters 1211-1216:","(not _) :- ."]} @@ -344,50 +344,50 @@ {"step":24,"kind":["Info"],"goal_id":48,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 138, column 0, characters 3773-3787:","(filter [] _ []) :- ."]} {"step":24,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X10 := []"]} {"step":24,"kind":["Info"],"goal_id":48,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":25,"kind":["Info"],"goal_id":30,"runtime_id":1,"name":"user:curgoal","payload":["bind","bind [uvar frozen--452 []] [] (uvar frozen--452 [] ===> uvar frozen--452 []) \n X3"]} +{"step":25,"kind":["Info"],"goal_id":30,"runtime_id":1,"name":"user:curgoal","payload":["bind","bind [uvar frozen--461 []] [] (uvar frozen--461 [] ===> uvar frozen--461 []) \n X3"]} {"step":25,"kind":["Info"],"goal_id":30,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":25,"kind":["Info"],"goal_id":30,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 123, column 0, characters 3297-3418:"]} {"step":25,"kind":["Info"],"goal_id":30,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 123, column 0, characters 3297-3418:","(bind [A1 | A3] A0 A4 (all A2 (c0 \\ (A5 c0)))) :- (if (mem A0 A1) (A2 = eqt) \n (A2 = any)), \n (pi c0 \\ (copy A1 c0 => bind A3 A0 A4 (A5 c0)))."]} -{"step":25,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := uvar frozen--452 []"]} +{"step":25,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := uvar frozen--461 []"]} {"step":25,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A3 := []"]} {"step":25,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := []"]} -{"step":25,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A4 := uvar frozen--452 [] ===> uvar frozen--452 []"]} +{"step":25,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A4 := uvar frozen--461 [] ===> uvar frozen--461 []"]} {"step":25,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X3 := all X12 c0 \\ X13 c0"]} {"step":25,"kind":["Info"],"goal_id":30,"runtime_id":1,"name":"user:subgoal","payload":["53"]} -{"step":25,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:newgoal","payload":["if (mem [] (uvar frozen--452 [])) (X12 = eqt) (X12 = any)"]} +{"step":25,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:newgoal","payload":["if (mem [] (uvar frozen--461 [])) (X12 = eqt) (X12 = any)"]} {"step":25,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:subgoal","payload":["54"]} -{"step":25,"kind":["Info"],"goal_id":54,"runtime_id":1,"name":"user:newgoal","payload":["pi c0 \\\n copy (uvar frozen--452 []) c0 =>\n bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)"]} +{"step":25,"kind":["Info"],"goal_id":54,"runtime_id":1,"name":"user:newgoal","payload":["pi c0 \\\n copy (uvar frozen--461 []) c0 =>\n bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)"]} {"step":25,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":26,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [] (uvar frozen--452 [])) (X12 = eqt) (X12 = any)"]} +{"step":26,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [] (uvar frozen--461 [])) (X12 = eqt) (X12 = any)"]} {"step":26,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule","payload":["backchain"]} -{"step":26,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 536, column 0, characters 13943-13962:","File \"builtin.elpi\", line 537, column 0, characters 13964-13977:"]} -{"step":26,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 536, column 0, characters 13943-13962:","(if A0 A1 _) :- A0, !, A1."]} -{"step":26,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := mem [] (uvar frozen--452 [])"]} +{"step":26,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 582, column 0, characters 16228-16247:","File \"builtin.elpi\", line 583, column 0, characters 16249-16262:"]} +{"step":26,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 582, column 0, characters 16228-16247:","(if A0 A1 _) :- A0, !, A1."]} +{"step":26,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := mem [] (uvar frozen--461 [])"]} {"step":26,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := X12 = eqt"]} {"step":26,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:subgoal","payload":["55"]} -{"step":26,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:newgoal","payload":["mem [] (uvar frozen--452 [])"]} +{"step":26,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:newgoal","payload":["mem [] (uvar frozen--461 [])"]} {"step":26,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:subgoal","payload":["56"]} {"step":26,"kind":["Info"],"goal_id":56,"runtime_id":1,"name":"user:newgoal","payload":["!"]} {"step":26,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:subgoal","payload":["57"]} {"step":26,"kind":["Info"],"goal_id":57,"runtime_id":1,"name":"user:newgoal","payload":["X12 = eqt"]} {"step":26,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":27,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:curgoal","payload":["mem","mem [] (uvar frozen--452 [])"]} +{"step":27,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:curgoal","payload":["mem","mem [] (uvar frozen--461 [])"]} {"step":27,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":27,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 148, column 0, characters 4032-4074:"]} {"step":27,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 148, column 0, characters 4032-4074:","(mem A0 (uvar A1 _)) :- (mem! A0 (uvar A1 A2))."]} {"step":27,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := []"]} -{"step":27,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := frozen--452"]} +{"step":27,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A1 := frozen--461"]} {"step":27,"kind":["Info"],"goal_id":55,"runtime_id":1,"name":"user:subgoal","payload":["58"]} -{"step":27,"kind":["Info"],"goal_id":58,"runtime_id":1,"name":"user:newgoal","payload":["mem! [] (uvar frozen--452 X14)"]} +{"step":27,"kind":["Info"],"goal_id":58,"runtime_id":1,"name":"user:newgoal","payload":["mem! [] (uvar frozen--461 X14)"]} {"step":27,"kind":["Info"],"goal_id":58,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":28,"kind":["Info"],"goal_id":58,"runtime_id":1,"name":"user:curgoal","payload":["mem!","mem! [] (uvar frozen--452 X14)"]} +{"step":28,"kind":["Info"],"goal_id":58,"runtime_id":1,"name":"user:curgoal","payload":["mem!","mem! [] (uvar frozen--461 X14)"]} {"step":28,"kind":["Info"],"goal_id":58,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":28,"kind":["Info"],"goal_id":58,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":[]} {"step":28,"kind":["Info"],"goal_id":58,"runtime_id":1,"name":"user:rule:backchain","payload":["fail"]} -{"step":29,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [] (uvar frozen--452 [])) (X12 = eqt) (X12 = any)"]} +{"step":29,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:curgoal","payload":["if","if (mem [] (uvar frozen--461 [])) (X12 = eqt) (X12 = any)"]} {"step":29,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule","payload":["backchain"]} -{"step":29,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 537, column 0, characters 13964-13977:"]} -{"step":29,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 537, column 0, characters 13964-13977:","(if _ _ A0) :- A0."]} +{"step":29,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"builtin.elpi\", line 583, column 0, characters 16249-16262:"]} +{"step":29,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"builtin.elpi\", line 583, column 0, characters 16249-16262:","(if _ _ A0) :- A0."]} {"step":29,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := X12 = any"]} {"step":29,"kind":["Info"],"goal_id":53,"runtime_id":1,"name":"user:subgoal","payload":["59"]} {"step":29,"kind":["Info"],"goal_id":59,"runtime_id":1,"name":"user:newgoal","payload":["X12 = any"]} @@ -397,50 +397,50 @@ {"step":30,"kind":["Info"],"goal_id":59,"runtime_id":1,"name":"user:rule:builtin:name","payload":["="]} {"step":30,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X12 := any"]} {"step":30,"kind":["Info"],"goal_id":59,"runtime_id":1,"name":"user:rule:eq","payload":["success"]} -{"step":31,"kind":["Info"],"goal_id":54,"runtime_id":1,"name":"user:curgoal","payload":["pi","pi c0 \\\n copy (uvar frozen--452 []) c0 =>\n bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)"]} +{"step":31,"kind":["Info"],"goal_id":54,"runtime_id":1,"name":"user:curgoal","payload":["pi","pi c0 \\\n copy (uvar frozen--461 []) c0 =>\n bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)"]} {"step":31,"kind":["Info"],"goal_id":54,"runtime_id":1,"name":"user:rule","payload":["pi"]} {"step":31,"kind":["Info"],"goal_id":54,"runtime_id":1,"name":"user:subgoal","payload":["60"]} -{"step":31,"kind":["Info"],"goal_id":60,"runtime_id":1,"name":"user:newgoal","payload":["copy (uvar frozen--452 []) c0 =>\n bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)"]} +{"step":31,"kind":["Info"],"goal_id":60,"runtime_id":1,"name":"user:newgoal","payload":["copy (uvar frozen--461 []) c0 =>\n bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)"]} {"step":31,"kind":["Info"],"goal_id":60,"runtime_id":1,"name":"user:new-quant","payload":["c0"]} {"step":31,"kind":["Info"],"goal_id":60,"runtime_id":1,"name":"user:rule:pi","payload":["success"]} -{"step":32,"kind":["Info"],"goal_id":60,"runtime_id":1,"name":"user:curgoal","payload":["=>","copy (uvar frozen--452 []) c0 =>\n bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)"]} +{"step":32,"kind":["Info"],"goal_id":60,"runtime_id":1,"name":"user:curgoal","payload":["=>","copy (uvar frozen--461 []) c0 =>\n bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)"]} {"step":32,"kind":["Info"],"goal_id":60,"runtime_id":1,"name":"user:rule","payload":["implication"]} {"step":32,"kind":["Info"],"goal_id":60,"runtime_id":1,"name":"user:subgoal","payload":["61"]} -{"step":32,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:newgoal","payload":["bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)"]} -{"step":32,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:new-hyps","payload":["(copy (uvar frozen--452 []) c0) :- ."]} +{"step":32,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:newgoal","payload":["bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)"]} +{"step":32,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:new-hyps","payload":["(copy (uvar frozen--461 []) c0) :- ."]} {"step":32,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:rule:implication","payload":["success"]} -{"step":33,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:curgoal","payload":["bind","bind [] [] (uvar frozen--452 [] ===> uvar frozen--452 []) (X13 c0)"]} +{"step":33,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:curgoal","payload":["bind","bind [] [] (uvar frozen--461 [] ===> uvar frozen--461 []) (X13 c0)"]} {"step":33,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":33,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 122, column 0, characters 3261-3295:"]} {"step":33,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 122, column 0, characters 3261-3295:","(bind [] _ A0 (mono A1)) :- (copy A0 A1)."]} -{"step":33,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--452 [] ===> uvar frozen--452 []"]} +{"step":33,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--461 [] ===> uvar frozen--461 []"]} {"step":33,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign:simplify:heap","payload":["X13 := c0 \\\nX15 c0"]} {"step":33,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X15^1 := mono X16^1"]} {"step":33,"kind":["Info"],"goal_id":61,"runtime_id":1,"name":"user:subgoal","payload":["62"]} -{"step":33,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:newgoal","payload":["copy (uvar frozen--452 [] ===> uvar frozen--452 []) X16^1"]} +{"step":33,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:newgoal","payload":["copy (uvar frozen--461 [] ===> uvar frozen--461 []) X16^1"]} {"step":33,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":34,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:curgoal","payload":["copy","copy (uvar frozen--452 [] ===> uvar frozen--452 []) X16^1"]} +{"step":34,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:curgoal","payload":["copy","copy (uvar frozen--461 [] ===> uvar frozen--461 []) X16^1"]} {"step":34,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":34,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"tests/sources/trace-w/main.elpi\", line 130, column 0, characters 3475-3527:"]} {"step":34,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"tests/sources/trace-w/main.elpi\", line 130, column 0, characters 3475-3527:","(copy (A0 ===> A2) (A1 ===> A3)) :- (copy A0 A1), (copy A2 A3)."]} -{"step":34,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--452 []"]} -{"step":34,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A2 := uvar frozen--452 []"]} +{"step":34,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A0 := uvar frozen--461 []"]} +{"step":34,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["A2 := uvar frozen--461 []"]} {"step":34,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X16^1 := X17^1 ===> X18^1"]} {"step":34,"kind":["Info"],"goal_id":62,"runtime_id":1,"name":"user:subgoal","payload":["63"]} -{"step":34,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:newgoal","payload":["copy (uvar frozen--452 []) X17^1"]} +{"step":34,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:newgoal","payload":["copy (uvar frozen--461 []) X17^1"]} {"step":34,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:subgoal","payload":["64"]} -{"step":34,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:newgoal","payload":["copy (uvar frozen--452 []) X18^1"]} +{"step":34,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:newgoal","payload":["copy (uvar frozen--461 []) X18^1"]} {"step":34,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":35,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:curgoal","payload":["copy","copy (uvar frozen--452 []) X17^1"]} +{"step":35,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:curgoal","payload":["copy","copy (uvar frozen--461 []) X17^1"]} {"step":35,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":35,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"(context step_id:32)\", line 1, column 0, characters 0-0:","File \"tests/sources/trace-w/main.elpi\", line 133, column 0, characters 3621-3647:"]} -{"step":35,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"(context step_id:32)\", line 1, column 0, characters 0-0:","(copy (uvar frozen--452 []) c0) :- ."]} +{"step":35,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"(context step_id:32)\", line 1, column 0, characters 0-0:","(copy (uvar frozen--461 []) c0) :- ."]} {"step":35,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X17^1 := c0"]} {"step":35,"kind":["Info"],"goal_id":63,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} -{"step":36,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:curgoal","payload":["copy","copy (uvar frozen--452 []) X18^1"]} +{"step":36,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:curgoal","payload":["copy","copy (uvar frozen--461 []) X18^1"]} {"step":36,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:rule","payload":["backchain"]} {"step":36,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:rule:backchain:candidates","payload":["File \"(context step_id:32)\", line 1, column 0, characters 0-0:","File \"tests/sources/trace-w/main.elpi\", line 133, column 0, characters 3621-3647:"]} -{"step":36,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"(context step_id:32)\", line 1, column 0, characters 0-0:","(copy (uvar frozen--452 []) c0) :- ."]} +{"step":36,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:rule:backchain:try","payload":["File \"(context step_id:32)\", line 1, column 0, characters 0-0:","(copy (uvar frozen--461 []) c0) :- ."]} {"step":36,"kind":["Info"],"goal_id":0,"runtime_id":1,"name":"user:assign","payload":["X18^1 := c0"]} {"step":36,"kind":["Info"],"goal_id":64,"runtime_id":1,"name":"user:rule:backchain","payload":["success"]} {"step":17,"kind":["Info"],"goal_id":25,"runtime_id":0,"name":"user:subgoal","payload":["65"]}