diff --git a/src/elpi_trace_elaborator.ml b/src/elpi_trace_elaborator.ml index 9c5166032..03e74d0f7 100644 --- a/src/elpi_trace_elaborator.ml +++ b/src/elpi_trace_elaborator.ml @@ -393,6 +393,14 @@ try assert(List.length events = 1); let _, events = List.hd events in Builtin { name; outcome; events = List.map decode_infer_event events } + else if name = "pi" || name = "sigma" then + let new_term = match has "user:new-quant" items with + | Some ({ payload = var }, _) -> var + | _ -> [] in + let name = { kind = `Logic; name; payload = [] } in + let () = + push_stack (step,rid) goal_id (`BuiltinRule ({ name with payload = new_term })) siblings in + Builtin { name; outcome; events = [] } else if name = "implication" then let new_hyps = match has "user:new-hyps" items with | Some ({ payload = hyps },_) -> hyps diff --git a/src/runtime/runtime.ml b/src/runtime/runtime.ml index 10dc10114..2fc228456 100644 --- a/src/runtime/runtime.ml +++ b/src/runtime/runtime.ml @@ -4116,6 +4116,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> executabl | Builtin(Pi, [arg]) -> [%spy "user:rule" ~rid ~gid pp_string "pi"]; let f = get_lambda_body ~depth arg in let gid[@trace] = make_subgoal_id gid ((depth+1,f)[@trace]) in + [%spy "user:new-quant" ~rid ~gid pp_constant depth]; [%spy "user:rule:pi" ~rid ~gid pp_string "success"]; [%tcall run (depth+1) p f (gid[@trace]) gs next alts cutto_alts] | Builtin(Sigma, [arg]) -> [%spy "user:rule" ~rid ~gid pp_string "sigma"]; @@ -4123,6 +4124,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> executabl let v = UVar(oref ~depth C.dummy, 0) in let fv = subst depth [v] f in let gid[@trace] = make_subgoal_id gid ((depth,fv)[@trace]) in + [%spy "user:new-quant" ~rid ~gid (uppterm depth [] ~argsdepth:0 empty_env) v]; [%spy "user:rule:sigma" ~rid ~gid pp_string "success"]; [%tcall run depth p fv (gid[@trace]) gs next alts cutto_alts] | Builtin(Delay,args) -> [%spy "user:rule" ~rid ~gid pp_string "builtin"]; [%spy "user:rule:builtin:name" ~rid ~gid pp_string (show_builtin_predicate C.show Delay)]; diff --git a/tests/sources/trace2.elab.json b/tests/sources/trace2.elab.json index 04c0383f1..685a1dfd3 100644 --- a/tests/sources/trace2.elab.json +++ b/tests/sources/trace2.elab.json @@ -160,7 +160,8 @@ "stack": [ { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 3, "runtime_id": 0 @@ -219,14 +220,15 @@ { "rule": [ "BuiltinRule", - { "name": "sigma", "kind": "Logic", "payload": [] } + { "name": "sigma", "kind": "Logic", "payload": [ "X0^1" ] } ], "step_id": 4, "runtime_id": 0 }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 3, "runtime_id": 0 @@ -295,14 +297,15 @@ { "rule": [ "BuiltinRule", - { "name": "sigma", "kind": "Logic", "payload": [] } + { "name": "sigma", "kind": "Logic", "payload": [ "X0^1" ] } ], "step_id": 4, "runtime_id": 0 }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 3, "runtime_id": 0 @@ -382,14 +385,15 @@ { "rule": [ "BuiltinRule", - { "name": "sigma", "kind": "Logic", "payload": [] } + { "name": "sigma", "kind": "Logic", "payload": [ "X0^1" ] } ], "step_id": 4, "runtime_id": 0 }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 3, "runtime_id": 0 @@ -496,14 +500,15 @@ { "rule": [ "BuiltinRule", - { "name": "sigma", "kind": "Logic", "payload": [] } + { "name": "sigma", "kind": "Logic", "payload": [ "X0^1" ] } ], "step_id": 4, "runtime_id": 0 }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 3, "runtime_id": 0 @@ -588,14 +593,15 @@ { "rule": [ "BuiltinRule", - { "name": "sigma", "kind": "Logic", "payload": [] } + { "name": "sigma", "kind": "Logic", "payload": [ "X0^1" ] } ], "step_id": 4, "runtime_id": 0 }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 3, "runtime_id": 0 diff --git a/tests/sources/trace2.json b/tests/sources/trace2.json index 1cbd4eb83..0b4d005d4 100644 --- a/tests/sources/trace2.json +++ b/tests/sources/trace2.json @@ -16,11 +16,13 @@ {"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule","payload" : ["pi"]} {"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["7"]} {"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["sigma c1 \\ fail => (true , fail)"]} +{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:new-quant","payload" : ["c0"]} {"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:pi","payload" : ["success"]} {"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["sigma","sigma c1 \\ fail => (true , fail)"]} {"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule","payload" : ["sigma"]} {"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["8"]} {"step" : 4,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["fail => (true , fail)"]} +{"step" : 4,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:new-quant","payload" : ["X0^1"]} {"step" : 4,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule:sigma","payload" : ["success"]} {"step" : 5,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=>","fail => (true , fail)"]} {"step" : 5,"kind" : ["Info"],"goal_id" : 8,"runtime_id" : 0,"name" : "user:rule","payload" : ["implication"]} diff --git a/tests/sources/trace_w.elab.json b/tests/sources/trace_w.elab.json index ead33f3d4..d2f81b319 100644 --- a/tests/sources/trace_w.elab.json +++ b/tests/sources/trace_w.elab.json @@ -1149,7 +1149,8 @@ "stack": [ { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 11, "runtime_id": 0 @@ -1293,7 +1294,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 11, "runtime_id": 0 @@ -1451,7 +1453,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 11, "runtime_id": 0 @@ -5392,7 +5395,11 @@ { "rule": [ "BuiltinRule", - { "name": "pi", "kind": "Logic", "payload": [] } + { + "name": "pi", + "kind": "Logic", + "payload": [ "c0" ] + } ], "step_id": 31, "runtime_id": 1 @@ -5491,7 +5498,11 @@ { "rule": [ "BuiltinRule", - { "name": "pi", "kind": "Logic", "payload": [] } + { + "name": "pi", + "kind": "Logic", + "payload": [ "c0" ] + } ], "step_id": 31, "runtime_id": 1 @@ -5623,7 +5634,11 @@ { "rule": [ "BuiltinRule", - { "name": "pi", "kind": "Logic", "payload": [] } + { + "name": "pi", + "kind": "Logic", + "payload": [ "c0" ] + } ], "step_id": 31, "runtime_id": 1 @@ -5775,7 +5790,11 @@ { "rule": [ "BuiltinRule", - { "name": "pi", "kind": "Logic", "payload": [] } + { + "name": "pi", + "kind": "Logic", + "payload": [ "c0" ] + } ], "step_id": 31, "runtime_id": 1 @@ -5917,7 +5936,11 @@ { "rule": [ "BuiltinRule", - { "name": "pi", "kind": "Logic", "payload": [] } + { + "name": "pi", + "kind": "Logic", + "payload": [ "c0" ] + } ], "step_id": 31, "runtime_id": 1 @@ -6059,7 +6082,11 @@ { "rule": [ "BuiltinRule", - { "name": "pi", "kind": "Logic", "payload": [] } + { + "name": "pi", + "kind": "Logic", + "payload": [ "c0" ] + } ], "step_id": 31, "runtime_id": 1 @@ -6270,7 +6297,8 @@ "stack": [ { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -6402,7 +6430,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -6566,7 +6595,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -6758,7 +6788,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -6932,7 +6963,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -7127,7 +7159,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -7337,7 +7370,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -7689,7 +7723,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -7960,7 +7995,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -8163,7 +8199,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 @@ -8382,7 +8419,8 @@ }, { "rule": [ - "BuiltinRule", { "name": "pi", "kind": "Logic", "payload": [] } + "BuiltinRule", + { "name": "pi", "kind": "Logic", "payload": [ "c0" ] } ], "step_id": 20, "runtime_id": 0 diff --git a/tests/sources/trace_w.json b/tests/sources/trace_w.json index e225fa1d7..d21f1f084 100644 --- a/tests/sources/trace_w.json +++ b/tests/sources/trace_w.json @@ -95,6 +95,7 @@ {"step" : 11,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 0,"name" : "user:rule","payload" : ["pi"]} {"step" : 11,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["21"]} {"step" : 11,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["of c0 (mono X5) => of c0 (mono X6)"]} +{"step" : 11,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 0,"name" : "user:new-quant","payload" : ["c0"]} {"step" : 11,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 0,"name" : "user:rule:pi","payload" : ["success"]} {"step" : 12,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=>","of c0 (mono X5) => of c0 (mono X6)"]} {"step" : 12,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 0,"name" : "user:rule","payload" : ["implication"]} @@ -400,6 +401,7 @@ {"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: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:rule","payload" : ["implication"]} @@ -464,6 +466,7 @@ {"step" : 20,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:rule","payload" : ["pi"]} {"step" : 20,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["67"]} {"step" : 20,"kind" : ["Info"],"goal_id" : 67,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["of c0 (all any c1 \\ mono (c1 ===> c1)) => of (app c0 (global [])) (mono X3)"]} +{"step" : 20,"kind" : ["Info"],"goal_id" : 67,"runtime_id" : 0,"name" : "user:new-quant","payload" : ["c0"]} {"step" : 20,"kind" : ["Info"],"goal_id" : 67,"runtime_id" : 0,"name" : "user:rule:pi","payload" : ["success"]} {"step" : 21,"kind" : ["Info"],"goal_id" : 67,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["=>","of c0 (all any c1 \\ mono (c1 ===> c1)) => of (app c0 (global [])) (mono X3)"]} {"step" : 21,"kind" : ["Info"],"goal_id" : 67,"runtime_id" : 0,"name" : "user:rule","payload" : ["implication"]}