From fcd5dde2692e0232c73ecb4cef9c443df4b18c73 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 28 Oct 2024 13:07:21 +0100 Subject: [PATCH] [builtins] std.list.init and std.list.make --- CHANGES.md | 5 +- src/builtin.elpi | 19 ++- src/builtin_stdlib.elpi | 19 ++- tests/sources/trace_chr.json | 4 +- tests/sources/trace_findall.elab.json | 12 +- tests/sources/trace_findall.json | 4 +- tests/sources/trace_w.elab.json | 180 +++++++++++++------------- tests/sources/trace_w.json | 176 ++++++++++++------------- 8 files changed, 219 insertions(+), 200 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 882a8bf2c..7be86be5a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -18,8 +18,9 @@ Requires Menhir 20211230 and OCaml 4.08 or above. the `:functional` attributes can be passed to higher-order arguments - The piece of information likes modes and functionality is transmitted to the checker (currently this information is not taken into account) - - +- Builtins: + - `std.list.init N E L` builds a list `L = [E, ..., E]` with length `N` + - `std.list.make N F L` builds the list `L = [F 0, F 1, ..., F (N-1)]` # v1.20.0 (September 2024) diff --git a/src/builtin.elpi b/src/builtin.elpi index 4c243cefa..6a5734ee1 100644 --- a/src/builtin.elpi +++ b/src/builtin.elpi @@ -776,12 +776,21 @@ flatten [] []. pred null i:list A. null []. -pred iota i:int, o:list int. -iota N L :- iota.aux 0 N L. +% [make N E L] L is [E, ..., E] and L has length N +pred list.make i:int, i:A, o:list A. +list.make 0 _ [] :- !. +list.make N E [E|L] :- N' is N - 1, list.make N' E L. + +% [init N F L] L is [F 0, ..., F (N-1)] +pred list.init i:int, i:(pred i:int, o:A), o:list A. +list.init N F L :- list.init.aux 0 N F L. -pred iota.aux i:int, i:int, o:list int. -iota.aux X X [] :- !. -iota.aux N X [N|R] :- M is N + 1, iota.aux M X R. +pred list.init.aux i:int, i:int, i:(pred i:int, o:A), o:list A. +list.init.aux N N _ [] :- !. +list.init.aux N M F [E|L] :- F N E, N' is N + 1, list.init.aux N' M F L. + +pred iota i:int, o:list int. +iota N L :- list.init N (x\y\ x = y) L. % [intersperse X L R] R is [L0, X, ..., X, LN] :index(_ 1) diff --git a/src/builtin_stdlib.elpi b/src/builtin_stdlib.elpi index 4d457d0a4..8efd317c2 100644 --- a/src/builtin_stdlib.elpi +++ b/src/builtin_stdlib.elpi @@ -243,12 +243,21 @@ flatten [] []. pred null i:list A. null []. -pred iota i:int, o:list int. -iota N L :- iota.aux 0 N L. +% [make N E L] L is [E, ..., E] and L has length N +pred list.make i:int, i:A, o:list A. +list.make 0 _ [] :- !. +list.make N E [E|L] :- N' is N - 1, list.make N' E L. + +% [init N F L] L is [F 0, ..., F (N-1)] +pred list.init i:int, i:(pred i:int, o:A), o:list A. +list.init N F L :- list.init.aux 0 N F L. -pred iota.aux i:int, i:int, o:list int. -iota.aux X X [] :- !. -iota.aux N X [N|R] :- M is N + 1, iota.aux M X R. +pred list.init.aux i:int, i:int, i:(pred i:int, o:A), o:list A. +list.init.aux N N _ [] :- !. +list.init.aux N M F [E|L] :- F N E, N' is N + 1, list.init.aux N' M F L. + +pred iota i:int, o:list int. +iota N L :- list.init N (x\y\ x = y) L. % [intersperse X L R] R is [L0, X, ..., X, LN] :index(_ 1) diff --git a/tests/sources/trace_chr.json b/tests/sources/trace_chr.json index fb2c55be7..ccddee7a6 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--518 []"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--522 []"]} {"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--519 []"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--523 []"]} {"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_findall.elab.json b/tests/sources/trace_findall.elab.json index b1c46e252..d42022e65 100644 --- a/tests/sources/trace_findall.elab.json +++ b/tests/sources/trace_findall.elab.json @@ -89,9 +89,9 @@ "File", { "filename": "builtin_stdlib.elpi", - "line": 296, + "line": 305, "column": 0, - "character": 9686 + "character": 10054 } ] } @@ -117,9 +117,9 @@ "File", { "filename": "builtin_stdlib.elpi", - "line": 296, + "line": 305, "column": 0, - "character": 9686 + "character": 10054 } ] } @@ -442,9 +442,9 @@ "File", { "filename": "builtin_stdlib.elpi", - "line": 296, + "line": 305, "column": 0, - "character": 9686 + "character": 10054 } ] } diff --git a/tests/sources/trace_findall.json b/tests/sources/trace_findall.json index 03a5d7d7d..8146dc604 100644 --- a/tests/sources/trace_findall.json +++ b/tests/sources/trace_findall.json @@ -10,8 +10,8 @@ {"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]} {"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["std.findall","std.findall (p _) X0"]} {"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]} -{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin_stdlib.elpi\", line 296, column 0, characters 9686-9722:"]} -{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin_stdlib.elpi\", line 296, column 0, characters 9686-9722:","(std.findall A0 A1) :- (findall_solutions A0 A1)."]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin_stdlib.elpi\", line 305, column 0, characters 10054-10090:"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin_stdlib.elpi\", line 305, column 0, characters 10054-10090:","(std.findall A0 A1) :- (findall_solutions A0 A1)."]} {"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := p _"]} {"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A1 := X0"]} {"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["7"]} diff --git a/tests/sources/trace_w.elab.json b/tests/sources/trace_w.elab.json index 84ce05415..f063aeab3 100644 --- a/tests/sources/trace_w.elab.json +++ b/tests/sources/trace_w.elab.json @@ -1988,7 +1988,7 @@ "step": [ "Init", { - "goal_text": "generalize [] [] (mono (uvar frozen--541 [] ==> uvar frozen--541 [])) X3", + "goal_text": "generalize [] [] (mono (uvar frozen--545 [] ==> uvar frozen--545 [])) X3", "goal_id": 26 } ], @@ -2001,7 +2001,7 @@ "Inference", { "current_goal_id": 26, - "current_goal_text": "generalize [] [] (mono (uvar frozen--541 [] ==> uvar frozen--541 [])) X3", + "current_goal_text": "generalize [] [] (mono (uvar frozen--545 [] ==> uvar frozen--545 [])) X3", "current_goal_predicate": "generalize", "failed_attempts": [], "successful_attempts": [ @@ -2027,14 +2027,14 @@ [ "Assign", "A1 := []" ], [ "Assign", - "A2 := uvar frozen--541 [] ==> uvar frozen--541 []" + "A2 := uvar frozen--545 [] ==> uvar frozen--545 []" ], [ "Assign", "A3 := X3" ] ] }, "siblings": [ { - "goal_text": "free-ty (mono (uvar frozen--541 [] ==> uvar frozen--541 [])) [] X4", + "goal_text": "free-ty (mono (uvar frozen--545 [] ==> uvar frozen--545 [])) [] X4", "goal_id": 27 }, { @@ -2046,7 +2046,7 @@ "goal_id": 29 }, { - "goal_text": "bind X6 [] (uvar frozen--541 [] ==> uvar frozen--541 []) X3", + "goal_text": "bind X6 [] (uvar frozen--545 [] ==> uvar frozen--545 []) X3", "goal_id": 30 } ], @@ -2086,7 +2086,7 @@ "Inference", { "current_goal_id": 27, - "current_goal_text": "free-ty (mono (uvar frozen--541 [] ==> uvar frozen--541 [])) [] X4", + "current_goal_text": "free-ty (mono (uvar frozen--545 [] ==> uvar frozen--545 [])) [] X4", "current_goal_predicate": "free-ty", "failed_attempts": [], "successful_attempts": [ @@ -2110,7 +2110,7 @@ "events": [ [ "Assign", - "A0 := uvar frozen--541 [] ==> uvar frozen--541 []" + "A0 := uvar frozen--545 [] ==> uvar frozen--545 []" ], [ "Assign", "A1 := []" ], [ "Assign", "A2 := X4" ] @@ -2118,7 +2118,7 @@ }, "siblings": [ { - "goal_text": "free (uvar frozen--541 [] ==> uvar frozen--541 []) [] X4", + "goal_text": "free (uvar frozen--545 [] ==> uvar frozen--545 []) [] X4", "goal_id": 31 } ], @@ -2177,7 +2177,7 @@ "Inference", { "current_goal_id": 31, - "current_goal_text": "free (uvar frozen--541 [] ==> uvar frozen--541 []) [] X4", + "current_goal_text": "free (uvar frozen--545 [] ==> uvar frozen--545 []) [] X4", "current_goal_predicate": "free", "failed_attempts": [], "successful_attempts": [ @@ -2199,19 +2199,19 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--541 []" ], - [ "Assign", "A1 := uvar frozen--541 []" ], + [ "Assign", "A0 := uvar frozen--545 []" ], + [ "Assign", "A1 := uvar frozen--545 []" ], [ "Assign", "A2 := []" ], [ "Assign", "A3 := X4" ] ] }, "siblings": [ { - "goal_text": "free (uvar frozen--541 []) [] X7", + "goal_text": "free (uvar frozen--545 []) [] X7", "goal_id": 32 }, { - "goal_text": "free (uvar frozen--541 []) X7 X4", + "goal_text": "free (uvar frozen--545 []) X7 X4", "goal_id": 33 } ], @@ -2289,7 +2289,7 @@ "Inference", { "current_goal_id": 32, - "current_goal_text": "free (uvar frozen--541 []) [] X7", + "current_goal_text": "free (uvar frozen--545 []) [] X7", "current_goal_predicate": "free", "failed_attempts": [], "successful_attempts": [ @@ -2311,14 +2311,14 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--541 []" ], + [ "Assign", "A0 := uvar frozen--545 []" ], [ "Assign", "A1 := []" ], [ "Assign", "A2 := X7" ] ] }, "siblings": [ { - "goal_text": "if (mem [] (uvar frozen--541 [])) (X7 = []) (X7 = [uvar frozen--541 []])", + "goal_text": "if (mem [] (uvar frozen--545 [])) (X7 = []) (X7 = [uvar frozen--545 []])", "goal_id": 34 } ], @@ -2415,7 +2415,7 @@ "Inference", { "current_goal_id": 34, - "current_goal_text": "if (mem [] (uvar frozen--541 [])) (X7 = []) (X7 = [uvar frozen--541 []])", + "current_goal_text": "if (mem [] (uvar frozen--545 [])) (X7 = []) (X7 = [uvar frozen--545 []])", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -2439,14 +2439,14 @@ "events": [ [ "Assign", - "A0 := mem [] (uvar frozen--541 [])" + "A0 := mem [] (uvar frozen--545 [])" ], [ "Assign", "A1 := X7 = []" ] ] }, "siblings": [ { - "goal_text": "mem [] (uvar frozen--541 [])", + "goal_text": "mem [] (uvar frozen--545 [])", "goal_id": 35 }, { "goal_text": "!", "goal_id": 36 }, @@ -2564,7 +2564,7 @@ "Inference", { "current_goal_id": 35, - "current_goal_text": "mem [] (uvar frozen--541 [])", + "current_goal_text": "mem [] (uvar frozen--545 [])", "current_goal_predicate": "mem", "failed_attempts": [], "successful_attempts": [ @@ -2587,12 +2587,12 @@ ], "events": [ [ "Assign", "A0 := []" ], - [ "Assign", "A1 := frozen--541" ] + [ "Assign", "A1 := frozen--545" ] ] }, "siblings": [ { - "goal_text": "mem! [] (uvar frozen--541 X8)", + "goal_text": "mem! [] (uvar frozen--545 X8)", "goal_id": 38 } ], @@ -2727,7 +2727,7 @@ "Inference", { "current_goal_id": 38, - "current_goal_text": "mem! [] (uvar frozen--541 X8)", + "current_goal_text": "mem! [] (uvar frozen--545 X8)", "current_goal_predicate": "mem!", "failed_attempts": [], "successful_attempts": [], @@ -2859,7 +2859,7 @@ "Inference", { "current_goal_id": 34, - "current_goal_text": "if (mem [] (uvar frozen--541 [])) (X7 = []) (X7 = [uvar frozen--541 []])", + "current_goal_text": "if (mem [] (uvar frozen--545 [])) (X7 = []) (X7 = [uvar frozen--545 []])", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -2882,13 +2882,13 @@ ], "events": [ [ - "Assign", "A0 := X7 = [uvar frozen--541 []]" + "Assign", "A0 := X7 = [uvar frozen--545 []]" ] ] }, "siblings": [ { - "goal_text": "X7 = [uvar frozen--541 []]", + "goal_text": "X7 = [uvar frozen--545 []]", "goal_id": 39 } ], @@ -3004,7 +3004,7 @@ "Inference", { "current_goal_id": 39, - "current_goal_text": "X7 = [uvar frozen--541 []]", + "current_goal_text": "X7 = [uvar frozen--545 []]", "current_goal_predicate": "=", "failed_attempts": [], "successful_attempts": [ @@ -3012,7 +3012,7 @@ "attempt": { "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], "events": [ - [ "Assign", "X7 := [uvar frozen--541 []]" ] + [ "Assign", "X7 := [uvar frozen--545 []]" ] ] }, "siblings": [], @@ -3133,7 +3133,7 @@ "Inference", { "current_goal_id": 33, - "current_goal_text": "free (uvar frozen--541 []) [uvar frozen--541 []] X4", + "current_goal_text": "free (uvar frozen--545 []) [uvar frozen--545 []] X4", "current_goal_predicate": "free", "failed_attempts": [], "successful_attempts": [ @@ -3155,14 +3155,14 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--541 []" ], - [ "Assign", "A1 := [uvar frozen--541 []]" ], + [ "Assign", "A0 := uvar frozen--545 []" ], + [ "Assign", "A1 := [uvar frozen--545 []]" ], [ "Assign", "A2 := X4" ] ] }, "siblings": [ { - "goal_text": "if (mem [uvar frozen--541 []] (uvar frozen--541 [])) \n (X4 = [uvar frozen--541 []]) \n (X4 = [uvar frozen--541 [], uvar frozen--541 []])", + "goal_text": "if (mem [uvar frozen--545 []] (uvar frozen--545 [])) \n (X4 = [uvar frozen--545 []]) \n (X4 = [uvar frozen--545 [], uvar frozen--545 []])", "goal_id": 40 } ], @@ -3259,7 +3259,7 @@ "Inference", { "current_goal_id": 40, - "current_goal_text": "if (mem [uvar frozen--541 []] (uvar frozen--541 [])) \n (X4 = [uvar frozen--541 []]) \n (X4 = [uvar frozen--541 [], uvar frozen--541 []])", + "current_goal_text": "if (mem [uvar frozen--545 []] (uvar frozen--545 [])) \n (X4 = [uvar frozen--545 []]) \n (X4 = [uvar frozen--545 [], uvar frozen--545 []])", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -3283,21 +3283,21 @@ "events": [ [ "Assign", - "A0 := mem [uvar frozen--541 []] (uvar frozen--541 [])" + "A0 := mem [uvar frozen--545 []] (uvar frozen--545 [])" ], [ - "Assign", "A1 := X4 = [uvar frozen--541 []]" + "Assign", "A1 := X4 = [uvar frozen--545 []]" ] ] }, "siblings": [ { - "goal_text": "mem [uvar frozen--541 []] (uvar frozen--541 [])", + "goal_text": "mem [uvar frozen--545 []] (uvar frozen--545 [])", "goal_id": 41 }, { "goal_text": "!", "goal_id": 42 }, { - "goal_text": "X4 = [uvar frozen--541 []]", + "goal_text": "X4 = [uvar frozen--545 []]", "goal_id": 43 } ], @@ -3413,7 +3413,7 @@ "Inference", { "current_goal_id": 41, - "current_goal_text": "mem [uvar frozen--541 []] (uvar frozen--541 [])", + "current_goal_text": "mem [uvar frozen--545 []] (uvar frozen--545 [])", "current_goal_predicate": "mem", "failed_attempts": [], "successful_attempts": [ @@ -3435,13 +3435,13 @@ } ], "events": [ - [ "Assign", "A0 := [uvar frozen--541 []]" ], - [ "Assign", "A1 := frozen--541" ] + [ "Assign", "A0 := [uvar frozen--545 []]" ], + [ "Assign", "A1 := frozen--545" ] ] }, "siblings": [ { - "goal_text": "mem! [uvar frozen--541 []] (uvar frozen--541 X9)", + "goal_text": "mem! [uvar frozen--545 []] (uvar frozen--545 X9)", "goal_id": 44 } ], @@ -3576,7 +3576,7 @@ "Inference", { "current_goal_id": 44, - "current_goal_text": "mem! [uvar frozen--541 []] (uvar frozen--541 X9)", + "current_goal_text": "mem! [uvar frozen--545 []] (uvar frozen--545 X9)", "current_goal_predicate": "mem!", "failed_attempts": [], "successful_attempts": [ @@ -3598,7 +3598,7 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--541 []" ], + [ "Assign", "A0 := uvar frozen--545 []" ], [ "Assign", "X9 := []" ] ] }, @@ -3756,7 +3756,7 @@ "cut_victims": [ { "cut_branch_for_goal": { - "goal_text": "mem! [uvar frozen--541 []] (uvar frozen--541 X9)", + "goal_text": "mem! [uvar frozen--545 []] (uvar frozen--545 X9)", "goal_id": 44 }, "cut_branch": { @@ -3787,7 +3787,7 @@ "cut_victims": [ { "cut_branch_for_goal": { - "goal_text": "if (mem [uvar frozen--541 []] (uvar frozen--541 [])) \n (X4 = [uvar frozen--541 []]) \n (X4 = [uvar frozen--541 [], uvar frozen--541 []])", + "goal_text": "if (mem [uvar frozen--545 []] (uvar frozen--545 [])) \n (X4 = [uvar frozen--545 []]) \n (X4 = [uvar frozen--545 [], uvar frozen--545 []])", "goal_id": 40 }, "cut_branch": { @@ -3815,7 +3815,7 @@ "Inference", { "current_goal_id": 43, - "current_goal_text": "X4 = [uvar frozen--541 []]", + "current_goal_text": "X4 = [uvar frozen--545 []]", "current_goal_predicate": "=", "failed_attempts": [], "successful_attempts": [ @@ -3823,7 +3823,7 @@ "attempt": { "rule": [ "BuiltinRule", [ "Logic", "eq" ] ], "events": [ - [ "Assign", "X4 := [uvar frozen--541 []]" ] + [ "Assign", "X4 := [uvar frozen--545 []]" ] ] }, "siblings": [], @@ -4026,7 +4026,7 @@ "Inference", { "current_goal_id": 29, - "current_goal_text": "filter [uvar frozen--541 []] (c0 \\ not (mem [] c0)) X6", + "current_goal_text": "filter [uvar frozen--545 []] (c0 \\ not (mem [] c0)) X6", "current_goal_predicate": "filter", "failed_attempts": [], "successful_attempts": [ @@ -4048,17 +4048,17 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--541 []" ], + [ "Assign", "A0 := uvar frozen--545 []" ], [ "Assign", "A1 := []" ], [ "Assign", "A2 := c0 \\\nnot (mem [] c0)" ], [ - "Assign", "X6 := [uvar frozen--541 [] | X10]" + "Assign", "X6 := [uvar frozen--545 [] | X10]" ] ] }, "siblings": [ { - "goal_text": "not (mem [] (uvar frozen--541 []))", + "goal_text": "not (mem [] (uvar frozen--545 []))", "goal_id": 46 }, { "goal_text": "!", "goal_id": 47 }, @@ -4122,7 +4122,7 @@ "Inference", { "current_goal_id": 46, - "current_goal_text": "not (mem [] (uvar frozen--541 []))", + "current_goal_text": "not (mem [] (uvar frozen--545 []))", "current_goal_predicate": "not", "failed_attempts": [], "successful_attempts": [ @@ -4146,13 +4146,13 @@ "events": [ [ "Assign", - "A0 := mem [] (uvar frozen--541 [])" + "A0 := mem [] (uvar frozen--545 [])" ] ] }, "siblings": [ { - "goal_text": "mem [] (uvar frozen--541 [])", + "goal_text": "mem [] (uvar frozen--545 [])", "goal_id": 49 }, { "goal_text": "!", "goal_id": 50 }, @@ -4232,7 +4232,7 @@ "Inference", { "current_goal_id": 49, - "current_goal_text": "mem [] (uvar frozen--541 [])", + "current_goal_text": "mem [] (uvar frozen--545 [])", "current_goal_predicate": "mem", "failed_attempts": [], "successful_attempts": [ @@ -4255,12 +4255,12 @@ ], "events": [ [ "Assign", "A0 := []" ], - [ "Assign", "A1 := frozen--541" ] + [ "Assign", "A1 := frozen--545" ] ] }, "siblings": [ { - "goal_text": "mem! [] (uvar frozen--541 X11)", + "goal_text": "mem! [] (uvar frozen--545 X11)", "goal_id": 52 } ], @@ -4357,7 +4357,7 @@ "Inference", { "current_goal_id": 52, - "current_goal_text": "mem! [] (uvar frozen--541 X11)", + "current_goal_text": "mem! [] (uvar frozen--545 X11)", "current_goal_predicate": "mem!", "failed_attempts": [], "successful_attempts": [], @@ -4451,7 +4451,7 @@ "Inference", { "current_goal_id": 46, - "current_goal_text": "not (mem [] (uvar frozen--541 []))", + "current_goal_text": "not (mem [] (uvar frozen--545 []))", "current_goal_predicate": "not", "failed_attempts": [], "successful_attempts": [ @@ -4678,7 +4678,7 @@ "Inference", { "current_goal_id": 30, - "current_goal_text": "bind [uvar frozen--541 []] [] (uvar frozen--541 [] ==> uvar frozen--541 []) \n X3", + "current_goal_text": "bind [uvar frozen--545 []] [] (uvar frozen--545 [] ==> uvar frozen--545 []) \n X3", "current_goal_predicate": "bind", "failed_attempts": [], "successful_attempts": [ @@ -4700,23 +4700,23 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--541 []" ], + [ "Assign", "A0 := uvar frozen--545 []" ], [ "Assign", "A1 := []" ], [ "Assign", "A2 := []" ], [ "Assign", - "A3 := uvar frozen--541 [] ==> uvar frozen--541 []" + "A3 := uvar frozen--545 [] ==> uvar frozen--545 []" ], [ "Assign", "X3 := all X12 c0 \\ X13 c0" ] ] }, "siblings": [ { - "goal_text": "if (mem [] (uvar frozen--541 [])) (X12 = eqt) (X12 = any)", + "goal_text": "if (mem [] (uvar frozen--545 [])) (X12 = eqt) (X12 = any)", "goal_id": 53 }, { - "goal_text": "pi c0 \\\n copy (uvar frozen--541 []) c0 =>\n bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)", + "goal_text": "pi c0 \\\n copy (uvar frozen--545 []) c0 =>\n bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (X13 c0)", "goal_id": 54 } ], @@ -4775,7 +4775,7 @@ "Inference", { "current_goal_id": 53, - "current_goal_text": "if (mem [] (uvar frozen--541 [])) (X12 = eqt) (X12 = any)", + "current_goal_text": "if (mem [] (uvar frozen--545 [])) (X12 = eqt) (X12 = any)", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -4799,14 +4799,14 @@ "events": [ [ "Assign", - "A0 := mem [] (uvar frozen--541 [])" + "A0 := mem [] (uvar frozen--545 [])" ], [ "Assign", "A1 := X12 = eqt" ] ] }, "siblings": [ { - "goal_text": "mem [] (uvar frozen--541 [])", + "goal_text": "mem [] (uvar frozen--545 [])", "goal_id": 55 }, { "goal_text": "!", "goal_id": 56 }, @@ -4886,7 +4886,7 @@ "Inference", { "current_goal_id": 55, - "current_goal_text": "mem [] (uvar frozen--541 [])", + "current_goal_text": "mem [] (uvar frozen--545 [])", "current_goal_predicate": "mem", "failed_attempts": [], "successful_attempts": [ @@ -4909,12 +4909,12 @@ ], "events": [ [ "Assign", "A0 := []" ], - [ "Assign", "A1 := frozen--541" ] + [ "Assign", "A1 := frozen--545" ] ] }, "siblings": [ { - "goal_text": "mem! [] (uvar frozen--541 X14)", + "goal_text": "mem! [] (uvar frozen--545 X14)", "goal_id": 58 } ], @@ -5011,7 +5011,7 @@ "Inference", { "current_goal_id": 58, - "current_goal_text": "mem! [] (uvar frozen--541 X14)", + "current_goal_text": "mem! [] (uvar frozen--545 X14)", "current_goal_predicate": "mem!", "failed_attempts": [], "successful_attempts": [], @@ -5105,7 +5105,7 @@ "Inference", { "current_goal_id": 53, - "current_goal_text": "if (mem [] (uvar frozen--541 [])) (X12 = eqt) (X12 = any)", + "current_goal_text": "if (mem [] (uvar frozen--545 [])) (X12 = eqt) (X12 = any)", "current_goal_predicate": "if", "failed_attempts": [], "successful_attempts": [ @@ -5294,7 +5294,7 @@ "Inference", { "current_goal_id": 54, - "current_goal_text": "pi c0 \\\n copy (uvar frozen--541 []) c0 =>\n bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)", + "current_goal_text": "pi c0 \\\n copy (uvar frozen--545 []) c0 =>\n bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (X13 c0)", "current_goal_predicate": "pi", "failed_attempts": [], "successful_attempts": [ @@ -5305,7 +5305,7 @@ }, "siblings": [ { - "goal_text": "copy (uvar frozen--541 []) c0 =>\n bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)", + "goal_text": "copy (uvar frozen--545 []) c0 =>\n bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (X13 c0)", "goal_id": 60 } ], @@ -5369,7 +5369,7 @@ "Inference", { "current_goal_id": 60, - "current_goal_text": "copy (uvar frozen--541 []) c0 =>\n bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)", + "current_goal_text": "copy (uvar frozen--545 []) c0 =>\n bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (X13 c0)", "current_goal_predicate": "=>", "failed_attempts": [], "successful_attempts": [ @@ -5382,7 +5382,7 @@ }, "siblings": [ { - "goal_text": "bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)", + "goal_text": "bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (X13 c0)", "goal_id": 61 } ], @@ -5453,7 +5453,7 @@ "Inference", { "current_goal_id": 61, - "current_goal_text": "bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)", + "current_goal_text": "bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (X13 c0)", "current_goal_predicate": "bind", "failed_attempts": [], "successful_attempts": [ @@ -5477,7 +5477,7 @@ "events": [ [ "Assign", - "A0 := uvar frozen--541 [] ==> uvar frozen--541 []" + "A0 := uvar frozen--545 [] ==> uvar frozen--545 []" ], [ "Assign", "X13 := c0 \\\nX15 c0" ], [ "Assign", "X15^1 := mono X16^1" ] @@ -5485,7 +5485,7 @@ }, "siblings": [ { - "goal_text": "copy (uvar frozen--541 [] ==> uvar frozen--541 []) X16^1", + "goal_text": "copy (uvar frozen--545 [] ==> uvar frozen--545 []) X16^1", "goal_id": 62 } ], @@ -5575,7 +5575,7 @@ "Inference", { "current_goal_id": 62, - "current_goal_text": "copy (uvar frozen--541 [] ==> uvar frozen--541 []) X16^1", + "current_goal_text": "copy (uvar frozen--545 [] ==> uvar frozen--545 []) X16^1", "current_goal_predicate": "copy", "failed_attempts": [], "successful_attempts": [ @@ -5597,18 +5597,18 @@ } ], "events": [ - [ "Assign", "A0 := uvar frozen--541 []" ], - [ "Assign", "A1 := uvar frozen--541 []" ], + [ "Assign", "A0 := uvar frozen--545 []" ], + [ "Assign", "A1 := uvar frozen--545 []" ], [ "Assign", "X16^1 := X17^1 ==> X18^1" ] ] }, "siblings": [ { - "goal_text": "copy (uvar frozen--541 []) X17^1", + "goal_text": "copy (uvar frozen--545 []) X17^1", "goal_id": 63 }, { - "goal_text": "copy (uvar frozen--541 []) X18^1", + "goal_text": "copy (uvar frozen--545 []) X18^1", "goal_id": 64 } ], @@ -5717,7 +5717,7 @@ "Inference", { "current_goal_id": 63, - "current_goal_text": "copy (uvar frozen--541 []) X17^1", + "current_goal_text": "copy (uvar frozen--545 []) X17^1", "current_goal_predicate": "copy", "failed_attempts": [], "successful_attempts": [ @@ -5726,7 +5726,7 @@ "rule": [ "UserRule", { - "rule_text": "(copy (uvar frozen--541 []) c0) :- .", + "rule_text": "(copy (uvar frozen--545 []) c0) :- .", "rule_loc": [ "Context", 32 ] } ], @@ -5742,7 +5742,7 @@ "rule": [ "UserRule", { - "rule_text": "(copy (uvar frozen--541 []) c0) :- .", + "rule_text": "(copy (uvar frozen--545 []) c0) :- .", "rule_loc": [ "Context", 32 ] } ], @@ -5849,7 +5849,7 @@ "Inference", { "current_goal_id": 64, - "current_goal_text": "copy (uvar frozen--541 []) X18^1", + "current_goal_text": "copy (uvar frozen--545 []) X18^1", "current_goal_predicate": "copy", "failed_attempts": [], "successful_attempts": [ @@ -5858,7 +5858,7 @@ "rule": [ "UserRule", { - "rule_text": "(copy (uvar frozen--541 []) c0) :- .", + "rule_text": "(copy (uvar frozen--545 []) c0) :- .", "rule_loc": [ "Context", 32 ] } ], @@ -5874,7 +5874,7 @@ "rule": [ "UserRule", { - "rule_text": "(copy (uvar frozen--541 []) c0) :- .", + "rule_text": "(copy (uvar frozen--545 []) c0) :- .", "rule_loc": [ "Context", 32 ] } ], diff --git a/tests/sources/trace_w.json b/tests/sources/trace_w.json index 3b71c14e8..634b342f9 100644 --- a/tests/sources/trace_w.json +++ b/tests/sources/trace_w.json @@ -133,136 +133,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 1999-2171:","(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--541 [] ==> uvar frozen--541 [])"]} -{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A3 := uvar frozen--542 []"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X1 := mono (uvar frozen--545 [] ==> uvar frozen--545 [])"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A3 := uvar frozen--546 []"]} {"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--541 [] ==> uvar frozen--541 [])) X3"]} -{"step" : 1,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["generalize","generalize [] [] (mono (uvar frozen--541 [] ==> uvar frozen--541 [])) X3"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["generalize [] [] (mono (uvar frozen--545 [] ==> uvar frozen--545 [])) X3"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 26,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["generalize","generalize [] [] (mono (uvar frozen--545 [] ==> uvar frozen--545 [])) 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 2318-2493:"]} {"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 2318-2493:","(generalize A0 A1 (mono A2) A3) :- (free-ty (mono A2) [] A4), \n (free-gamma A1 [] A5), (filter A4 (c0 \\ (not (mem A5 c0))) A6), \n (bind A6 A0 A2 A3)."]} {"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := []"]} {"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := []"]} -{"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A2 := uvar frozen--541 [] ==> uvar frozen--541 []"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A2 := uvar frozen--545 [] ==> uvar frozen--545 []"]} {"step" : 1,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A3 := 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--541 [] ==> uvar frozen--541 [])) [] X4"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 27,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["free-ty (mono (uvar frozen--545 [] ==> uvar frozen--545 [])) [] 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--541 [] ==> uvar frozen--541 []) X3"]} +{"step" : 1,"kind" : ["Info"],"goal_id" : 30,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["bind X6 [] (uvar frozen--545 [] ==> uvar frozen--545 []) 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--541 [] ==> uvar frozen--541 [])) [] X4"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 27,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["free-ty","free-ty (mono (uvar frozen--545 [] ==> uvar frozen--545 [])) [] 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 2609-2645:"]} {"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 2609-2645:","(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--541 [] ==> uvar frozen--541 []"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 [] ==> uvar frozen--545 []"]} {"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--541 [] ==> uvar frozen--541 []) [] X4"]} +{"step" : 2,"kind" : ["Info"],"goal_id" : 31,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["free (uvar frozen--545 [] ==> uvar frozen--545 []) [] 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--541 [] ==> uvar frozen--541 []) [] X4"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 31,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["free","free (uvar frozen--545 [] ==> uvar frozen--545 []) [] 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 2995-3043:"]} {"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 2995-3043:","(free (A0 ==> A1) A2 A3) :- (free A0 A2 A4), (free A1 A4 A3)."]} -{"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--541 []"]} -{"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := uvar frozen--541 []"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 []"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := uvar frozen--545 []"]} {"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A2 := []"]} {"step" : 3,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A3 := 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--541 []) [] X7"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 32,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["free (uvar frozen--545 []) [] 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--541 []) X7 X4"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 33,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["free (uvar frozen--545 []) 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--541 []) [] X7"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 32,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["free","free (uvar frozen--545 []) [] 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 3045-3108:"]} {"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 3045-3108:","(free (as (uvar _ _) A0) A1 A2) :- (if (mem A1 A0) (A2 = A1) (A2 = [A0 | A1]))."]} -{"step" : 4,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--541 []"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 []"]} {"step" : 4,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := []"]} {"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--541 [])) (X7 = []) (X7 = [uvar frozen--541 []])"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 34,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["if (mem [] (uvar frozen--545 [])) (X7 = []) (X7 = [uvar frozen--545 []])"]} {"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--541 [])) (X7 = []) (X7 = [uvar frozen--541 []])"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 34,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["if","if (mem [] (uvar frozen--545 [])) (X7 = []) (X7 = [uvar frozen--545 []])"]} {"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 514, column 0, characters 12754-12773:","File \"builtin.elpi\", line 515, column 0, characters 12775-12788:"]} {"step" : 5,"kind" : ["Info"],"goal_id" : 34,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 514, column 0, characters 12754-12773:","(if A0 A1 _) :- A0, (!), A1."]} -{"step" : 5,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := mem [] (uvar frozen--541 [])"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := mem [] (uvar frozen--545 [])"]} {"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--541 [])"]} +{"step" : 5,"kind" : ["Info"],"goal_id" : 35,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["mem [] (uvar frozen--545 [])"]} {"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--541 [])"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 35,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["mem","mem [] (uvar frozen--545 [])"]} {"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 4000-4042:"]} {"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 4000-4042:","(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--541"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := frozen--545"]} {"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--541 X8)"]} +{"step" : 6,"kind" : ["Info"],"goal_id" : 38,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["mem! [] (uvar frozen--545 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--541 X8)"]} +{"step" : 7,"kind" : ["Info"],"goal_id" : 38,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["mem!","mem! [] (uvar frozen--545 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--541 [])) (X7 = []) (X7 = [uvar frozen--541 []])"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 34,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["if","if (mem [] (uvar frozen--545 [])) (X7 = []) (X7 = [uvar frozen--545 []])"]} {"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 515, column 0, characters 12775-12788:"]} {"step" : 8,"kind" : ["Info"],"goal_id" : 34,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 515, column 0, characters 12775-12788:","(if _ _ A0) :- A0."]} -{"step" : 8,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := X7 = [uvar frozen--541 []]"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := X7 = [uvar frozen--545 []]"]} {"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--541 []]"]} +{"step" : 8,"kind" : ["Info"],"goal_id" : 39,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["X7 = [uvar frozen--545 []]"]} {"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--541 []]"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 39,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["=","X7 = [uvar frozen--545 []]"]} {"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--541 []]"]} +{"step" : 9,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X7 := [uvar frozen--545 []]"]} {"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--541 []) [uvar frozen--541 []] X4"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 33,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["free","free (uvar frozen--545 []) [uvar frozen--545 []] 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 3045-3108:"]} {"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 3045-3108:","(free (as (uvar _ _) A0) A1 A2) :- (if (mem A1 A0) (A2 = A1) (A2 = [A0 | A1]))."]} -{"step" : 10,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--541 []"]} -{"step" : 10,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := [uvar frozen--541 []]"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 []"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := [uvar frozen--545 []]"]} {"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--541 []] (uvar frozen--541 [])) \n (X4 = [uvar frozen--541 []]) \n (X4 = [uvar frozen--541 [], uvar frozen--541 []])"]} +{"step" : 10,"kind" : ["Info"],"goal_id" : 40,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["if (mem [uvar frozen--545 []] (uvar frozen--545 [])) \n (X4 = [uvar frozen--545 []]) \n (X4 = [uvar frozen--545 [], uvar frozen--545 []])"]} {"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--541 []] (uvar frozen--541 [])) \n (X4 = [uvar frozen--541 []]) \n (X4 = [uvar frozen--541 [], uvar frozen--541 []])"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 40,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["if","if (mem [uvar frozen--545 []] (uvar frozen--545 [])) \n (X4 = [uvar frozen--545 []]) \n (X4 = [uvar frozen--545 [], uvar frozen--545 []])"]} {"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 514, column 0, characters 12754-12773:","File \"builtin.elpi\", line 515, column 0, characters 12775-12788:"]} {"step" : 11,"kind" : ["Info"],"goal_id" : 40,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 514, column 0, characters 12754-12773:","(if A0 A1 _) :- A0, (!), A1."]} -{"step" : 11,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := mem [uvar frozen--541 []] (uvar frozen--541 [])"]} -{"step" : 11,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := X4 = [uvar frozen--541 []]"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := mem [uvar frozen--545 []] (uvar frozen--545 [])"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := X4 = [uvar frozen--545 []]"]} {"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--541 []] (uvar frozen--541 [])"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 41,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["mem [uvar frozen--545 []] (uvar frozen--545 [])"]} {"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--541 []]"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 43,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["X4 = [uvar frozen--545 []]"]} {"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--541 []] (uvar frozen--541 [])"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 41,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["mem","mem [uvar frozen--545 []] (uvar frozen--545 [])"]} {"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 4000-4042:"]} {"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 4000-4042:","(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--541 []]"]} -{"step" : 12,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := frozen--541"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := [uvar frozen--545 []]"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := frozen--545"]} {"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--541 []] (uvar frozen--541 X9)"]} +{"step" : 12,"kind" : ["Info"],"goal_id" : 44,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["mem! [uvar frozen--545 []] (uvar frozen--545 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--541 []] (uvar frozen--541 X9)"]} +{"step" : 13,"kind" : ["Info"],"goal_id" : 44,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["mem!","mem! [uvar frozen--545 []] (uvar frozen--545 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 3872-3889:","File \"tests/sources/trace-w/main.elpi\", line 144, column 0, characters 3891-3916:"]} {"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 3872-3889:","(mem! [A0 | _] A0) :- (!)."]} -{"step" : 13,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--541 []"]} +{"step" : 13,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 []"]} {"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,10 +275,10 @@ {"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 515, column 0, characters 12775-12788:","(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--541 []]"]} +{"step" : 16,"kind" : ["Info"],"goal_id" : 43,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["=","X4 = [uvar frozen--545 []]"]} {"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--541 []]"]} +{"step" : 16,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X4 := [uvar frozen--545 []]"]} {"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"]} @@ -287,47 +287,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--541 []] (c0 \\ not (mem [] c0)) X6"]} +{"step" : 18,"kind" : ["Info"],"goal_id" : 29,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["filter","filter [uvar frozen--545 []] (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 3758-3806:","File \"tests/sources/trace-w/main.elpi\", line 140, column 0, characters 3808-3844:"]} {"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 3758-3806:","(filter [A0 | A1] A2 [A0 | A3]) :- (A2 A0), (!), (filter A1 A2 A3)."]} -{"step" : 18,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--541 []"]} +{"step" : 18,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 []"]} {"step" : 18,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := []"]} {"step" : 18,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A2 := c0 \\\nnot (mem [] c0)"]} -{"step" : 18,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X6 := [uvar frozen--541 [] | X10]"]} +{"step" : 18,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X6 := [uvar frozen--545 [] | 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--541 []))"]} +{"step" : 18,"kind" : ["Info"],"goal_id" : 46,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["not (mem [] (uvar frozen--545 []))"]} {"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--541 []))"]} +{"step" : 19,"kind" : ["Info"],"goal_id" : 46,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["not","not (mem [] (uvar frozen--545 []))"]} {"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 54, column 0, characters 667-686:","File \"builtin.elpi\", line 56, column 0, characters 689-694:"]} {"step" : 19,"kind" : ["Info"],"goal_id" : 46,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 54, column 0, characters 667-686:","(not A0) :- A0, (!), fail."]} -{"step" : 19,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := mem [] (uvar frozen--541 [])"]} +{"step" : 19,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := mem [] (uvar frozen--545 [])"]} {"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--541 [])"]} +{"step" : 19,"kind" : ["Info"],"goal_id" : 49,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["mem [] (uvar frozen--545 [])"]} {"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--541 [])"]} +{"step" : 20,"kind" : ["Info"],"goal_id" : 49,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["mem","mem [] (uvar frozen--545 [])"]} {"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 4000-4042:"]} {"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 4000-4042:","(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--541"]} +{"step" : 20,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := frozen--545"]} {"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--541 X11)"]} +{"step" : 20,"kind" : ["Info"],"goal_id" : 52,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["mem! [] (uvar frozen--545 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--541 X11)"]} +{"step" : 21,"kind" : ["Info"],"goal_id" : 52,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["mem!","mem! [] (uvar frozen--545 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--541 []))"]} +{"step" : 22,"kind" : ["Info"],"goal_id" : 46,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["not","not (mem [] (uvar frozen--545 []))"]} {"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 56, column 0, characters 689-694:"]} {"step" : 22,"kind" : ["Info"],"goal_id" : 46,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 56, column 0, characters 689-694:","(not _) :- ."]} @@ -342,47 +342,47 @@ {"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 3742-3756:","(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--541 []] [] (uvar frozen--541 [] ==> uvar frozen--541 []) \n X3"]} +{"step" : 25,"kind" : ["Info"],"goal_id" : 30,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["bind","bind [uvar frozen--545 []] [] (uvar frozen--545 [] ==> uvar frozen--545 []) \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 3268-3389:"]} {"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 3268-3389:","(bind [A0 | A1] A2 A3 (all A4 (c0 \\ (A5 c0)))) :- (if (mem A2 A0) (A4 = eqt) \n (A4 = any)), \n (pi (c0 \\ (copy A0 c0 => bind A1 A2 A3 (A5 c0))))."]} -{"step" : 25,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--541 []"]} +{"step" : 25,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 []"]} {"step" : 25,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := []"]} {"step" : 25,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A2 := []"]} -{"step" : 25,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A3 := uvar frozen--541 [] ==> uvar frozen--541 []"]} +{"step" : 25,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A3 := uvar frozen--545 [] ==> uvar frozen--545 []"]} {"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--541 [])) (X12 = eqt) (X12 = any)"]} +{"step" : 25,"kind" : ["Info"],"goal_id" : 53,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["if (mem [] (uvar frozen--545 [])) (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--541 []) c0 =>\n bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)"]} +{"step" : 25,"kind" : ["Info"],"goal_id" : 54,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["pi c0 \\\n copy (uvar frozen--545 []) c0 =>\n bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (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--541 [])) (X12 = eqt) (X12 = any)"]} +{"step" : 26,"kind" : ["Info"],"goal_id" : 53,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["if","if (mem [] (uvar frozen--545 [])) (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 514, column 0, characters 12754-12773:","File \"builtin.elpi\", line 515, column 0, characters 12775-12788:"]} {"step" : 26,"kind" : ["Info"],"goal_id" : 53,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 514, column 0, characters 12754-12773:","(if A0 A1 _) :- A0, (!), A1."]} -{"step" : 26,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := mem [] (uvar frozen--541 [])"]} +{"step" : 26,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := mem [] (uvar frozen--545 [])"]} {"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--541 [])"]} +{"step" : 26,"kind" : ["Info"],"goal_id" : 55,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["mem [] (uvar frozen--545 [])"]} {"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--541 [])"]} +{"step" : 27,"kind" : ["Info"],"goal_id" : 55,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["mem","mem [] (uvar frozen--545 [])"]} {"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 4000-4042:"]} {"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 4000-4042:","(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--541"]} +{"step" : 27,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := frozen--545"]} {"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--541 X14)"]} +{"step" : 27,"kind" : ["Info"],"goal_id" : 58,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["mem! [] (uvar frozen--545 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--541 X14)"]} +{"step" : 28,"kind" : ["Info"],"goal_id" : 58,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["mem!","mem! [] (uvar frozen--545 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--541 [])) (X12 = eqt) (X12 = any)"]} +{"step" : 29,"kind" : ["Info"],"goal_id" : 53,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["if","if (mem [] (uvar frozen--545 [])) (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 515, column 0, characters 12775-12788:"]} {"step" : 29,"kind" : ["Info"],"goal_id" : 53,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 515, column 0, characters 12775-12788:","(if _ _ A0) :- A0."]} @@ -395,48 +395,48 @@ {"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--541 []) c0 =>\n bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)"]} +{"step" : 31,"kind" : ["Info"],"goal_id" : 54,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["pi","pi c0 \\\n copy (uvar frozen--545 []) c0 =>\n bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (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--541 []) c0 =>\n bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)"]} +{"step" : 31,"kind" : ["Info"],"goal_id" : 60,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["copy (uvar frozen--545 []) c0 =>\n bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (X13 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--541 []) c0 =>\n bind [] [] (uvar frozen--541 [] ==> uvar frozen--541 []) (X13 c0)"]} +{"step" : 32,"kind" : ["Info"],"goal_id" : 60,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["=>","copy (uvar frozen--545 []) c0 =>\n bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (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--541 [] ==> uvar frozen--541 []) (X13 c0)"]} +{"step" : 32,"kind" : ["Info"],"goal_id" : 61,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (X13 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--541 [] ==> uvar frozen--541 []) (X13 c0)"]} +{"step" : 33,"kind" : ["Info"],"goal_id" : 61,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["bind","bind [] [] (uvar frozen--545 [] ==> uvar frozen--545 []) (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 3232-3266:"]} {"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 3232-3266:","(bind [] _ A0 (mono A1)) :- (copy A0 A1)."]} -{"step" : 33,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--541 [] ==> uvar frozen--541 []"]} +{"step" : 33,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 [] ==> uvar frozen--545 []"]} {"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--541 [] ==> uvar frozen--541 []) X16^1"]} +{"step" : 33,"kind" : ["Info"],"goal_id" : 62,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["copy (uvar frozen--545 [] ==> uvar frozen--545 []) 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--541 [] ==> uvar frozen--541 []) X16^1"]} +{"step" : 34,"kind" : ["Info"],"goal_id" : 62,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["copy","copy (uvar frozen--545 [] ==> uvar frozen--545 []) 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 3446-3496:"]} {"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 3446-3496:","(copy (A0 ==> A1) (A2 ==> A3)) :- (copy A0 A2), (copy A1 A3)."]} -{"step" : 34,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--541 []"]} -{"step" : 34,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := uvar frozen--541 []"]} +{"step" : 34,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--545 []"]} +{"step" : 34,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A1 := uvar frozen--545 []"]} {"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--541 []) X17^1"]} +{"step" : 34,"kind" : ["Info"],"goal_id" : 63,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["copy (uvar frozen--545 []) 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--541 []) X18^1"]} +{"step" : 34,"kind" : ["Info"],"goal_id" : 64,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["copy (uvar frozen--545 []) 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--541 []) X17^1"]} +{"step" : 35,"kind" : ["Info"],"goal_id" : 63,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["copy","copy (uvar frozen--545 []) 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 3590-3616:"]} -{"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--541 []) 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--545 []) 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--541 []) X18^1"]} +{"step" : 36,"kind" : ["Info"],"goal_id" : 64,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["copy","copy (uvar frozen--545 []) 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 3590-3616:"]} -{"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--541 []) 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--545 []) 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"]}