diff --git a/src/plugins/wp/Pattern.ml b/src/plugins/wp/Pattern.ml
index 68f12f5b2655b11a6f3370c04a993b0e335deccc..4ac4f4e2737907dcb915416875a092d06876891b 100644
--- a/src/plugins/wp/Pattern.ml
+++ b/src/plugins/wp/Pattern.ml
@@ -38,6 +38,7 @@ and node =
| Range of int * int
| Int of Integer.t
| Bool of bool
+ | String of string
| Assoc of assoc * ast list
| Binop of ast * binop * ast
| Call of string * ast list
@@ -115,6 +116,8 @@ let rec parse ctxt p =
| PLfalse -> { loc ; value = Bool false }
| PLconstant (IntConstant n) ->
{ loc ; value = Int (pinteger ctxt ~loc n) }
+ | PLconstant (StringConstant s) ->
+ { loc ; value = String s }
| PLrange(Some a,Some b) when ctxt.value ->
{ loc ; value = Range(pbound ctxt a,pbound ctxt b) }
| PLapp("\\concat",[],[]) -> { loc ; value = List [] }
@@ -181,6 +184,7 @@ let rec pp fmt (a : ast) =
| Range(a,b) -> Format.fprintf fmt "(%d..%d)" a b
| Int n -> Integer.pretty fmt n
| Bool b -> Format.pp_print_string fmt (if b then "\\true" else "\\false")
+ | String s -> Format.fprintf fmt "%S" s
| Assoc(`Add,[]) -> Format.pp_print_string fmt "0"
| Assoc(`Mul,[]) -> Format.pp_print_string fmt "1"
| Assoc(`Concat,[]) -> Format.pp_print_string fmt "[| |]"
@@ -482,6 +486,7 @@ let rec select (env : sigma) (a : value) =
let cc = select env in
match a.value with
| Any -> error ~loc "Pattern _ is not a value"
+ | String s -> error ~loc "String %S is not a value" s
| Pvar x -> getvar env x
| Named (_,v) -> cc v
| Range(a,b) -> Tactical.range a b
@@ -515,4 +520,14 @@ and compose env ~loc id vs =
| Tactical.Empty -> error ~loc "Computer %S not found" id
| result -> result
+let bool (a : value) =
+ match a.value with
+ | Bool b -> b
+ | _ -> error ~loc:a.loc "Not a boolean value (%a)" pp a
+
+let string (a : value) =
+ match a.value with
+ | String s -> s
+ | _ -> error ~loc:a.loc "Not a string value (%a)" pp a
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Pattern.mli b/src/plugins/wp/Pattern.mli
index deb3906739942b08aa15716fb4ebb1788ae7fd49..bcfbeb2be6853d6b69a7d1fbfd7723bb7488c1b0 100644
--- a/src/plugins/wp/Pattern.mli
+++ b/src/plugins/wp/Pattern.mli
@@ -66,4 +66,10 @@ val psequent : lookup -> sigma -> Conditions.sequent -> sigma option
(** Composing values from matching results *)
val select : sigma -> value -> Tactical.selection
+(** Composing a boolean *)
+val bool : value -> bool
+
+(** Composing a string *)
+val string : value -> string
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index 9d72711ea9a3418a8296e644c75ca2fc30377fe2..f19e426ab3dcaf92b7f806f5830028b28169b682 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -290,7 +290,7 @@ let jtactic ?strategy (tac : tactical) (sel : selection) =
tactic = tac#id ;
params = json_of_parameters tac ;
select = json_of_selection sel ;
- strategy = Option.map ProofStrategy.name strategy ;
+ strategy ;
}
let json_of_tactic t js =
diff --git a/src/plugins/wp/ProofScript.mli b/src/plugins/wp/ProofScript.mli
index 7fe27cbb04d87de398b0cd1e56eb2485194ff8ed..7c4ab83e58fbdbcf8b0eb7b7b24eea9f8a659846 100644
--- a/src/plugins/wp/ProofScript.mli
+++ b/src/plugins/wp/ProofScript.mli
@@ -55,7 +55,7 @@ val has_proof : jscript -> bool
val decode : Json.t -> jscript
val encode : jscript -> Json.t
-val jtactic : ?strategy:ProofStrategy.strategy -> tactical -> selection -> jtactic
+val jtactic : ?strategy:string -> tactical -> selection -> jtactic
val configure : jtactic -> sequent -> (tactical * selection) option
(** Json Codecs *)
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index e51abd50f8073fbb5f4f39fe01eab2c6c299e003..3b4c4cff629785245d08e8609341a61633665caf 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -295,10 +295,104 @@ let provers = function
| Some tm -> tm
| None -> float @@ Wp_parameters.Timeout.get ()
end
- | _ -> [],0.0
+ | Strategy _ | Tactic _ | Auto _ -> [],0.0
let fallback = function
| Strategy s -> resolve s
- | _ -> None
+ | Tactic _ | Auto _ | Provers _ -> None
+
+(* -------------------------------------------------------------------------- *)
+(* --- Strategy Tactical Step --- *)
+(* -------------------------------------------------------------------------- *)
+
+let tactical a =
+ try Tactical.lookup ~id:a.value with Not_found ->
+ Wp_parameters.error ~source:(fst a.loc) ~once:true
+ "Tactical '%s' not found (skipped alternative)." a.value ;
+ raise Not_found
+
+let parameter (t : Tactical.tactical) a =
+ try List.find (fun p -> Tactical.pident p = a.value) t#params
+ with Not_found ->
+ Wp_parameters.error ~source:(fst a.loc) ~once:true
+ "Parameter '%s' not found (skipped alternative)." a.value ;
+ raise Not_found
+
+let configure tactic sigma (a,v) =
+ match parameter tactic a with
+ | Checkbox fd ->
+ begin
+ try tactic#set_field fd (Pattern.bool v)
+ with Not_found ->
+ Wp_parameters.error ~source:(fst a.loc)
+ "Expected boolean for parameter '%s' (%a)" a.value
+ Pattern.pp_value v ;
+ raise Not_found
+ end
+ | Spinner(fd,_) ->
+ begin
+ let value = Pattern.select sigma v in
+ match Tactical.get_int value with
+ | Some v -> tactic#set_field fd v
+ | None ->
+ Wp_parameters.error ~source:(fst a.loc)
+ "Expected integer for parameter '%s' (%a)" a.value
+ Tactical.pp_selection value ;
+ raise Not_found
+ end
+ | Composer(fd,_) -> tactic#set_field fd (Pattern.select sigma v)
+ | Selector(fd,vs,_) ->
+ begin
+ try
+ let id = Pattern.string v in
+ let v = List.find (fun v -> v.Tactical.vid = id) vs in
+ tactic#set_field fd v.value
+ with Not_found ->
+ Wp_parameters.error ~source:(fst a.loc)
+ "Expected string for parameter '%s' (%a)" a.value
+ Pattern.pp_value v ;
+ raise Not_found
+ end
+ | Search(_,_,lookup) ->
+ begin
+ try
+ let id = Pattern.string v in
+ let _v = lookup id in
+ (*TODO: tactic#set_field fd v *)
+ assert false
+ with Not_found ->
+ Wp_parameters.error ~source:(fst a.loc)
+ "Expected string for parameter '%s' (%a)" a.value
+ Pattern.pp_value v ;
+ raise Not_found
+ end
+
+let rec bind sigma sequent = function
+ | [] -> sigma
+ | lookup::binders ->
+ match Pattern.psequent lookup sigma sequent with
+ | None -> raise Not_found
+ | Some sigma -> bind sigma sequent binders
+
+let tactic tree node = function
+ | Strategy _ | Auto _ | Provers _ -> None
+ | Tactic t ->
+ try
+ let tactic = tactical t.tactic in
+ let pool = ProofEngine.pool tree in
+ let title = tactic#title in
+ let ctxt = ProofEngine.node_context node in
+ let sequent = snd @@ Wpo.compute @@ ProofEngine.goal node in
+ let console = new ProofScript.console ~pool ~title in
+ WpContext.on_context ctxt
+ begin fun () ->
+ let sigma = bind Pattern.empty sequent t.lookup in
+ List.iter (configure tactic sigma) t.params ;
+ ignore console ;
+ None
+ end ()
+ with Not_found -> None
+
+let () = ignore tactic
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 4b246d88518f70abd66bf8193b8000f2f7b3577f..623583773bca6432743f9a2c277f50005fb75783 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -313,6 +313,12 @@ and autofork env ~depth fork =
else
( Env.validate env ; Task.return true )
+(* -------------------------------------------------------------------------- *)
+(* --- Proof Strategy Alternatives --- *)
+(* -------------------------------------------------------------------------- *)
+
+(*TODO*)
+
(* -------------------------------------------------------------------------- *)
(* --- Apply Script Tactic --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 1d6c2cc28e90dd2b0f54b6fee77036315f3b4b8a..d10d0611aa48b21c42ac72dfb6e1e19c31971825 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -125,7 +125,15 @@ let get_int = function
| Compose(Cint a) -> get_int_z a
| s ->
match Lang.F.repr (selected s) with
- | Qed.Logic.Kint z -> get_int_z z
+ | Kint z -> get_int_z z
+ | _ -> None
+
+let get_bool = function
+ | Empty -> None
+ | s ->
+ match Lang.F.repr (selected s) with
+ | True -> Some true
+ | False -> Some false
| _ -> None
let subclause clause p =
@@ -326,6 +334,13 @@ let search ~id ~title ~descr ~browse ~find () =
let fd = field ~id ~title ~descr ~default:None in
fd , Search(fd,browse,find)
+let pident = function
+ | Checkbox fd -> ident fd
+ | Spinner(fd,_) -> ident fd
+ | Composer(fd,_) -> ident fd
+ | Selector(fd,_,_) -> ident fd
+ | Search(fd,_,_) -> ident fd
+
(* -------------------------------------------------------------------------- *)
(* --- Feedback --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Tactical.mli b/src/plugins/wp/Tactical.mli
index 5d7e84e9709a3c3bb3355d7b0aec0281b295e6ce..993c4513ffd53877a99234cd2eab04c38449218f 100644
--- a/src/plugins/wp/Tactical.mli
+++ b/src/plugins/wp/Tactical.mli
@@ -54,6 +54,7 @@ val range : int -> int -> selection
val compose : string -> selection list -> selection
val multi : selection list -> selection
val get_int : selection -> int option
+val get_bool : selection -> bool option
val destruct : selection -> selection list
val head : clause -> pred
@@ -99,6 +100,7 @@ type parameter =
val ident : 'a field -> string
val default : 'a field -> 'a
val signature : 'a field -> 'a named
+val pident : parameter -> string
val checkbox :
id:string -> title:string -> descr:string ->