1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
open Lang
open Lang.F
open Tactical
let rec range pool e a b =
if a <= b then
let descr = Printf.sprintf "Value %d" b in
let cond = p_equal e (e_int b) in
range ((descr,cond)::pool) e a (pred b)
else pool
let enum ?at e a b sequent =
let lower = Printf.sprintf "Lower %d" a , p_lt e (e_int a) in
let upper = Printf.sprintf "Upper %d" b , p_lt (e_int b) e in
let cases = lower :: range [upper] e a b in
Tactical.insert ?at cases sequent
let vmin,pmin = Tactical.spinner ~id:"inf"
~title:"Inf" ~descr:"Range lower bound (inclusive)." ()
let vmax,pmax = Tactical.spinner ~id:"sup"
~title:"Sup" ~descr:"Range upper bound (inclusive)." ()
class range =
object(self)
inherit Tactical.make ~id:"Wp.range"
~title:"Range"
~descr:"Enumerate a range of values for an integer term."
~params:[pmin;pmax]
method select feedback (s : Tactical.selection) =
let at = Tactical.at s in
let e = Tactical.selected s in
if F.is_int e then
begin
let a = self#get_field vmin in
let b = self#get_field vmax in
if not (a <= b) then
( feedback#set_error "Empty Range (shall have Inf <= Sup)" ;
Not_configured )
else
( feedback#set_title "Range (%d-%d)" a b ;
feedback#set_descr "Enumerate lower, range %d-%d and upper." a b ;
Applicable(enum ?at e a b) )
end
else
Not_applicable
end
let tactical = Tactical.export (new range)
let strategy ?(priority=1.0) selection ~vmin:a ~vmax:b =
Strategy.{
priority ; tactical ; selection ;
arguments = [ arg vmin a ; arg vmax b ] ;
}