Commit 6a3b6896 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

[compute] maximal number of steps can be given with meta compute_max_steps

parent fb63f8ba
......@@ -19,9 +19,9 @@ let meta_rewrite = Theory.register_meta "rewrite" [Theory.MTprsymbol]
~desc:"Declares@ the@ given@ proposition@ as@ a@ rewrite@ rule."
let meta_rewrite_def = Theory.register_meta "rewrite_def" [Theory.MTlsymbol]
~desc:"Declares@ the@ definition@ of@ the@ symbol@ as@ as@ rewrite@ rule."
~desc:"Declares@ the@ definition@ of@ the@ symbol@ as@ a@ rewrite@ rule."
let meta_compute_max_steps = Theory.register_meta "compute_max_steps"
let meta_compute_max_steps = Theory.register_meta_excl "compute_max_steps"
[Theory.MTint]
~desc:"Maximal@ number@ of@ reduction@ steps@ done@ by@ compute@ \
transformation"
......@@ -74,14 +74,22 @@ let normalize_goal p env (prs : Decl.Spr.t) task =
| _ -> assert false
let normalize_goal_transf p env =
Trans.on_tagged_pr meta_rewrite
(fun prs -> if p.compute_defs
then Trans.store (normalize_goal p env prs)
else Trans.on_tagged_ls meta_rewrite_def
(fun lss -> let p = { p with compute_def_set = lss } in
Trans.store (normalize_goal p env prs)
))
let normalize_goal_transf p env : 'a Trans.trans =
let tr : 'a Trans.trans =
Trans.on_tagged_pr meta_rewrite
(fun prs -> if p.compute_defs
then Trans.store (normalize_goal p env prs)
else Trans.on_tagged_ls meta_rewrite_def
(fun lss -> let p = { p with compute_def_set = lss } in
Trans.store (normalize_goal p env prs)
))
in
Trans.on_meta_excl meta_compute_max_steps
(function
| None -> tr
| Some [Theory.MAint n] -> compute_max_steps := n; tr
| _ -> assert false)
let normalize_goal_transf_all env =
let p = { compute_defs = true;
......
......@@ -331,6 +331,9 @@ theory NonTerm
goal g5 : fib (S (S (S (S (S O))))) = x
goal g6 : fib (S (S (S (S (S (S O)))))) = x
goal g7 : fib (S (S (S (S (S (S (S O))))))) = x
meta "compute_max_steps" 100000
goal g8 : fib (S (S (S (S (S (S (S (S O)))))))) = x
goal g9 : fib (S (S (S (S (S (S (S (S (S O))))))))) = x
goal g10 : fib (S (S (S (S (S (S (S (S (S (S O)))))))))) = x
......
......@@ -3,184 +3,188 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../test_compute.why" expanded="true">
<theory name="Lambda" sum="ac7b1c25f8dd32d440e0b14d115c7c15">
<goal name="g1">
<transf name="compute_in_goal">
<theory name="Lambda" sum="ac7b1c25f8dd32d440e0b14d115c7c15" expanded="true">
<goal name="g1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="g2">
<transf name="compute_in_goal">
<goal name="g2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="g3">
<goal name="g3" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g3.1" expl="1.">
</goal>
</transf>
</goal>
</theory>
<theory name="A" sum="0e4355327797e8f3d23d6df80a329362">
<theory name="A" sum="0e4355327797e8f3d23d6df80a329362" expanded="true">
<goal name="G1">
</goal>
<goal name="G2">
</goal>
<goal name="G3">
</goal>
<goal name="g">
<goal name="g" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="Test" sum="cd473d7e70fa0fdfbc7f9f5523952c9e">
<goal name="g1">
<theory name="Test" sum="cd473d7e70fa0fdfbc7f9f5523952c9e" expanded="true">
<goal name="g1" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g2">
<transf name="compute_in_goal">
<goal name="g2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="g3">
<goal name="g3" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g10">
<goal name="g10" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g11">
<goal name="g11" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="TestArith" sum="cf84efb4f92d0a90148d60fc86520337">
<goal name="h1">
<theory name="TestArith" sum="cf84efb4f92d0a90148d60fc86520337" expanded="true">
<goal name="h1" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="h2">
<goal name="h2" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="h3">
<goal name="h3" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="j1">
<goal name="j1" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="k1">
</goal>
<goal name="l1">
<goal name="l1" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l2">
<goal name="l2" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l3">
</goal>
<goal name="l4">
<transf name="compute_in_goal">
<goal name="l4" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l4.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="l5">
<transf name="compute_in_goal">
<goal name="l5" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l5.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="l6">
<goal name="l6" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l7">
<goal name="l7" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l8">
<goal name="l8" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l9">
</goal>
<goal name="m1">
<transf name="compute_in_goal">
<goal name="m1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m2">
<transf name="compute_in_goal">
<goal name="m2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m3">
<transf name="compute_in_goal">
<goal name="m3" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m3.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m4">
</goal>
<goal name="n1">
<transf name="compute_in_goal">
<goal name="n1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n2">
<transf name="compute_in_goal">
<goal name="n2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n3">
<transf name="compute_in_goal">
<goal name="n3" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n3.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n4">
<transf name="compute_in_goal">
<goal name="n4" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n4.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="o1">
<transf name="compute_in_goal">
<goal name="o1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="o1.1" expl="1.">
</goal>
</transf>
</goal>
</theory>
<theory name="TestRecord" sum="01e5c2659bedbfaf6934498a0580aaef">
<goal name="i1">
<theory name="TestRecord" sum="01e5c2659bedbfaf6934498a0580aaef" expanded="true">
<goal name="i1" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="i2">
<goal name="i2" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="TestList" sum="ec36d89b8213f71e7ce492154030a520" expanded="true">
<goal name="g1">
<goal name="g1" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g2">
<goal name="g2" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g3">
<goal name="g3" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -190,7 +194,7 @@
</goal>
</transf>
</goal>
<goal name="h2">
<goal name="h2" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -262,7 +266,7 @@
</goal>
</transf>
</goal>
<goal name="g01">
<goal name="g01" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -272,7 +276,7 @@
</goal>
</transf>
</goal>
<goal name="g2">
<goal name="g2" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -352,11 +356,11 @@
</goal>
</transf>
</goal>
<goal name="g2">
<goal name="g2" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g3">
<goal name="g3" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment