Degraded performance of auto-invert-solve in OCaml 5.0.0 #267
Description
The t/harpoon/nats_and_bools_tps_auto_invert.input test case using the auto-invert-solve tactic takes ~80 seconds to succeed when Harpoon is compiled using OCaml 5.0.0.
That test case is reported to fail with the upgraded OCaml compiler because the TEST.sh script has a 10 seconds time limit for each test case.
With OCaml 4.14.1, that same test case succeeds in ~0.07 seconds. This seems to suggest that some optimizations done during the compilation of the Logic module with OCaml 4.14.1 are not performed in OCaml 5.0.0.
Load the signature t/harpoon/nats_and_bools_tps_auto_invert.input in Harpoon and input the commands in t/harpoon/nats_and_bools_tps_auto_invert.input.
The degraded performance happens specifically when inputting auto-invert-solve in the following Harpoon states:
Theorem: tps
intros <- split x (case e_if_then_else)
Meta-context:
M1 : ( |- term)
M3 : ( |- term)
M4 : ( |- term)
M2 : ( |- term)
A : ( |- tp)
S : ( |- step M1 M2)
Computational context:
x : [ |- step (if_then_else M1 M3 M4) (if_then_else M2 M3 M4)]
x1 : [ |- hastype (if_then_else M1 M3 M4) A]
--------------------------------------------------------------------------------
[ |- hastype (if_then_else M2 M3 M4) A]
Theorem: tps
intros <- split x (case e_if_false)
Meta-context:
M1 : ( |- term)
N : ( |- term)
A : ( |- tp)
Computational context:
x : [ |- step (if_then_else false M1 N) N]
x1 : [ |- hastype (if_then_else false M1 N) A]
--------------------------------------------------------------------------------
[ |- hastype N A]
Theorem: tps
intros <- split x (case e_if_true)
Meta-context:
N : ( |- term)
M2 : ( |- term)
A : ( |- tp)
Computational context:
x : [ |- step (if_then_else true N M2) N]
x1 : [ |- hastype (if_then_else true N M2) A]
--------------------------------------------------------------------------------
[ |- hastype N A]