diff --git a/src/plugins/qed/export_coq.ml b/src/plugins/qed/export_coq.ml
index 8e06fa9404c3431e141abaf3713952d73278804f..33756bcc50bc9d5d490734a66516cbbbb1c63793 100644
--- a/src/plugins/qed/export_coq.ml
+++ b/src/plugins/qed/export_coq.ml
@@ -362,7 +362,8 @@ struct
begin
self#declare_signature fmt f (List.map tau_of_var xs) t ;
let fix = prefix ^ (link_name (self#link f)) in
- self#declare_axiom fmt fix xs [] (e_eq (e_fun f (List.map e_var xs)) e) ;
+ self#declare_axiom fmt fix xs []
+ (e_eq (e_fun ~result:t f (List.map e_var xs)) e) ;
end
method declare_axiom fmt lemma xs (_:trigger list list) p =
diff --git a/src/plugins/qed/export_why3.ml b/src/plugins/qed/export_why3.ml
index f940aa001d959d5df4e7367751dd1fa65bbde490..84aca8d411871ec01cdd4c1c072369011ca9d969 100644
--- a/src/plugins/qed/export_why3.ml
+++ b/src/plugins/qed/export_why3.ml
@@ -304,7 +304,8 @@ struct
begin
self#declare_signature fmt f (List.map tau_of_var xs) t ;
let fix = prefix ^ (link_name (self#link f)) in
- self#declare_axiom fmt fix xs [] (e_eq (e_fun f (List.map e_var xs)) e) ;
+ self#declare_axiom fmt fix xs []
+ (e_eq (e_fun ~result:t f (List.map e_var xs)) e) ;
end
end
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 7a2a8774a2879c799d600886d122348bdcbe1fcd..11f8e2cf2e24801ac3a03327b171a2a96da6365a 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -884,7 +884,7 @@ struct
let c_record fxs =
match fxs with
- | [] | [_] -> insert(Rdef fxs)
+ | [] -> insert(Rdef fxs)
| fx::gys ->
try
let base (f,v) =
@@ -985,13 +985,13 @@ struct
| x::[] as xs ->
begin
match x.repr with
- | If(c,a,b) -> !extern_ite c (!extern_fun f [a]) (!extern_fun f [b])
+ | If(c,a,b) -> !extern_ite c (!extern_fun f [a] tau) (!extern_fun f [b] tau)
| _ -> operation (FUN(f,xs,tau))
end
| a::b::[] as xs ->
distribute_if_over_operation false
(fun f xs -> operation (FUN(f,xs,tau))) f xs
- (fun a b -> !extern_fun f [a;b]) a b
+ (fun a b -> !extern_fun f [a;b] tau) a b
| xs -> operation (FUN(f,xs,tau))
let c_builtin_fun f xs tau = distribute f tau xs
@@ -1101,12 +1101,12 @@ struct
else modified,xs,ys
in simpl false true xs ys
- let rec element = function
+ let rec element tau = function
| E_none -> assert false
| E_int k -> e_int k
| E_true -> e_true
| E_false -> e_false
- | E_fun (f,l) -> c_fun f (List.map element l) None
+ | E_fun (f,l) -> c_fun f (List.map (element tau) l) tau
let rec is_element e x = match e , x.repr with
| E_int k , Kint z -> Z.equal (Z.of_int k) z
@@ -1144,7 +1144,7 @@ struct
in
if op.absorbant <> E_none &&
List.exists (is_element op.absorbant) xs
- then element op.absorbant
+ then element tau op.absorbant
else
let xs =
if op.neutral <> E_none
@@ -1152,7 +1152,7 @@ struct
else xs in
let xs = if op.idempotent then op_idempotent xs else xs in
match xs with
- | [] when op.neutral <> E_none -> element op.neutral
+ | [] when op.neutral <> E_none -> element tau op.neutral
| [x] when op.associative -> x
| _ -> c_builtin_fun f xs tau
@@ -1161,8 +1161,7 @@ struct
| Logic.Operator op -> op_fun f op xs tau
| _ -> c_builtin_fun f xs tau
- let e_fun ?result f xs = e_fungen f xs result
- let () = extern_fun := e_fun
+ let () = extern_fun := e_fungen
(* -------------------------------------------------------------------------- *)
(* --- Ground & Arithmetics --- *)
@@ -1671,6 +1670,8 @@ struct
(* --- Equality --- *)
(* -------------------------------------------------------------------------- *)
+ let typeof2 x y = if x.tau = None then y.tau else x.tau
+
let rec e_eq x y =
if x == y then e_true else relation eq_symb EQ x y
@@ -1714,13 +1715,17 @@ struct
and eq_invertible x y f xs ys =
let modified,xs,ys = op_invertible ~ac:(is_ac f) xs ys in
if modified
- then eq_symb (e_fun f xs ?result:x.tau) (e_fun f ys ?result:y.tau)
+ then
+ let tr = typeof2 x y in
+ eq_symb (e_fungen f xs tr) (e_fungen f ys tr)
else c_builtin_eq x y
and eq_invertible_both x y f g xs ys =
let modified,xs',ys' = op_invertible ~ac:(is_ac f) xs [y] in
if modified
- then eq_symb (e_fun f xs' ?result:x.tau) (e_fun f ys' ?result:y.tau)
+ then
+ let tr = typeof2 x y in
+ eq_symb (e_fungen f xs' tr) (e_fungen f ys' tr)
else eq_invertible x y g [x] ys
and eq_field (f,x) (g,y) =
@@ -1775,13 +1780,17 @@ struct
and neq_invertible x y f xs ys =
let modified,xs,ys = op_invertible ~ac:(is_ac f) xs ys in
if modified
- then neq_symb (e_fun f xs) (e_fun f ys)
+ then
+ let tr = typeof2 x y in
+ neq_symb (e_fungen f xs tr) (e_fungen f ys tr)
else c_builtin_neq x y
and neq_invertible_both x y f g xs ys =
let modified,xs',ys' = op_invertible ~ac:(is_ac f) xs [y] in
if modified
- then neq_symb (e_fun f xs') (e_fun f ys')
+ then
+ let tr = typeof2 x y in
+ neq_symb (e_fungen f xs' tr) (e_fungen f ys' tr)
else neq_invertible x y g [x] ys
and neq_field (f,x) (g,y) =
@@ -2037,7 +2046,7 @@ struct
| Times(z,t) -> e_times z (f t)
| If(e,a,b) -> e_if (f e) (f a) (f b)
| Imply(hs,p) -> e_imply (List.map f hs) (f p)
- | Fun(g,xs) -> e_fun ?result:e0.tau g (List.map f xs)
+ | Fun(g,xs) -> e_fungen g (List.map f xs) e0.tau
| Acst(t,v) -> e_const t v
| Aget(x,y) -> e_get (f x) (f y)
| Aset(x,y,z) -> e_set (f x) (f y) (f z)
@@ -2072,7 +2081,6 @@ struct
let validate fn e =
if not (lc_closed e) then
begin
- Format.eprintf "Invalid %s: %a@." fn pretty e ;
raise (Invalid_argument (fn ^ ": non lc-closed binding"))
end
@@ -2226,7 +2234,6 @@ struct
List.iter (Subst.add_term sigma) es ;
apply sigma Intmap.empty e es
-
(* -------------------------------------------------------------------------- *)
(* --- convert between states --- *)
(* -------------------------------------------------------------------------- *)
@@ -2259,7 +2266,7 @@ struct
| Times(z,t) -> times z (aux t)
| If(e,a,b) -> e_if (aux e) (aux a) (aux b)
| Imply(hs,p) -> e_imply (List.map aux hs) (aux p)
- | Fun(g,xs) -> e_fun ?result:e.tau g (List.map aux xs)
+ | Fun(g,xs) -> e_fungen g (List.map aux xs) e.tau
| Acst(t,v) -> e_const t (aux v)
| Aget(x,y) -> e_get (aux x) (aux y)
| Aset(x,y,z) -> e_set (aux x) (aux y) (aux z)
@@ -2403,7 +2410,7 @@ struct
| Leq(x,y) -> e_leq x y
| If(e,a,b) -> e_if e a b
| Imply(hs,p) -> e_imply hs p
- | Fun(g,xs) -> e_fun ?result g xs
+ | Fun(g,xs) -> e_fungen g xs result
| Acst(t,v) -> e_const t v
| Aget(m,k) -> e_get m k
| Aset(m,k,v) -> e_set m k v
@@ -2433,6 +2440,8 @@ struct
f a
| _ -> repr_iter f e.repr
+ let e_fun ?result f xs = e_fungen f xs result
+
(* -------------------------------------------------------------------------- *)
(* --- Sub-terms --- *)
(* -------------------------------------------------------------------------- *)
@@ -2506,7 +2515,7 @@ struct
| Aset _ -> bad_position ()
| Rdef _ | Rget _ ->
failwith "change in place for records not yet implemented"
- | Fun (f,ops) -> e_fun ?result:e.tau f (change_in_list ops i l)
+ | Fun (f,ops) -> e_fungen f (change_in_list ops i l) e.tau
| Bind(q,x,t) when i = 0 -> c_bind q x (aux t l)
| Bind _ -> bad_position ()
| Apply(f,args) when i = 0 ->
@@ -2550,7 +2559,8 @@ struct
| _ -> true)
fvs
in
- Some ( base , fothers )
+ if fothers = [] then None (* suspiscious *)
+ else Some ( base , fothers )
(* ------------------------------------------------------------------------ *)
(* --- Symbol --- *)
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 2a40a79b124bb21ed5bd06a79c017168a3adf4eb..9acf448228ae8e33af9c797714522ca1addd52e3 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -353,14 +353,18 @@ class virtual visitor main =
method vparam x = self#vtau (tau_of_var x)
- method private repr ~bool x =
- self#vtau (Lang.F.typeof x);
- match F.repr x with
+ method private repr ~bool t =
+ begin
+ try self#vtau (Lang.F.typeof t);
+ with Not_found ->
+ Wp_parameters.debug ~level:2 "@[<hov 2>Untyped term: %a@]" F.pp_term t ;
+ end ;
+ match F.repr t with
| Fun(f,_) -> self#vsymbol f
| Rget(_,f) -> self#vfield f
| Rdef fts -> List.iter (fun (f,_) -> self#vfield f) fts
| Fvar x -> self#vparam x
- | Bind(_,t,_) -> self#vtau t
+ | Bind(_,qt,_) -> self#vtau qt
| True | False | Kint _ | Kreal _ | Bvar _
| Times _ | Add _ | Mul _ | Div _ | Mod _
| Aget _ | Aset _ | Apply _ -> ()
@@ -422,7 +426,7 @@ class virtual visitor main =
match f with
| Model { m_source = Extern e } -> self#vlibrary e.ext_library
| Model { m_source = Generated _ } | ACSL _ -> self#vlfun f
- | CTOR c -> self#vadt (Lang.atype c.ctor_type)
+ | CTOR c -> self#vadt (Lang.adt c.ctor_type)
end
method private vtrigger = function
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 88258560f1f600fb7a8abddf69aae8a6ba3b2e02..407f98990d661247c025864069dd4497c6717e03 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -220,6 +220,7 @@ class pane (gprovers : GuiConfig.provers) =
cancel proof ;
Task.iter Task.cancel pool ;
state <- Proof proof ;
+ ProofEngine.forward proof ;
printer#reset ;
self#update
@@ -366,6 +367,7 @@ class pane (gprovers : GuiConfig.provers) =
self#update_provers None ;
self#update_tactics None ;
state <- Proof pw ;
+ ProofEngine.forward pw ;
self#update ;
end
@@ -586,6 +588,8 @@ class pane (gprovers : GuiConfig.provers) =
printer#reset ;
self#update ;
end
+ else
+ Wutil.later self#commit
method private schedule pool provers goal =
Prover.spawn goal
diff --git a/src/plugins/wp/GuiProof.ml b/src/plugins/wp/GuiProof.ml
index d352290613b8d9a8e3a4553afd3d71f27b34aae3..1b984174b7b0f54bd374c223529e9ba6b22a773f 100644
--- a/src/plugins/wp/GuiProof.ml
+++ b/src/plugins/wp/GuiProof.ml
@@ -26,12 +26,10 @@ let rec rootchain node ns =
| Some p -> rootchain p (p::ns)
let pp_status fmt node =
- match ProofEngine.state node with
- | `Opened -> Format.fprintf fmt "@{<red>opened@}"
- | `Proved | `Pending 0 -> Format.fprintf fmt "@{<green>proved@}"
- | `Pending 1 -> Format.fprintf fmt "@{<orange>pending@}"
- | `Pending n -> Format.fprintf fmt "@{<orange>pending %d@}" n
- | `Script n -> Format.fprintf fmt "script with %d leaves" n
+ match ProofEngine.pending node with
+ | 0 -> Format.fprintf fmt "@{<green>proved@}"
+ | 1 -> Format.fprintf fmt "@{<orange>pending@}"
+ | n -> Format.fprintf fmt "@{<orange>pending %d@}" n
class printer (text : Wtext.text) =
let nodes : ProofEngine.position Wtext.marker = text#marker in
@@ -66,36 +64,25 @@ class printer (text : Wtext.text) =
VCS.pp_prover prv VCS.pp_result res
) (Wpo.get_results wpo)
- method private pp_state fmt node =
- match ProofEngine.state node with
- | `Proved -> Format.pp_print_string fmt "proved"
- | `Opened -> Format.pp_print_string fmt "opened"
- | `Pending 0 -> Format.pp_print_string fmt "terminated"
- | `Pending 1 -> Format.pp_print_string fmt "pending"
- | `Pending n -> Format.fprintf fmt "pending(%d)" n
- | `Script 0 -> Format.pp_print_string fmt "script"
- | `Script n -> Format.fprintf fmt "script(%d)" n
-
method private tactic header node =
+ text#printf "@{<bf>Tactical@}@} %s:" header ;
match ProofEngine.children node with
| [] ->
- text#printf "@{<bf>Tactical@}@} %s: @{<green>proved@} (Qed).@\n" header
+ text#printf "@{<green>proved@} (Qed).@\n"
| [_,child] ->
- text#printf "@{<bf>Tactical@} %a: %a.@\n" self#pp_node child self#pp_state child
+ text#printf "%a (%a).@\n" pp_status child self#pp_node child
| children ->
- begin match ProofEngine.pending node with
- | 0 -> text#printf "@{<green>@{<bf>Tactical@}@} %s: @{<green>proved@}.@\n" header
- | 1 -> text#printf "@{<bf>Tactical@} %s: @{<orange>pending@}.@\n" header ;
- | n -> text#printf "@{<bf>Tactical@} %s: @{<orange>pending(%d)@}.@\n" header n ;
- end ;
- List.iter
- (fun (part,child) -> text#printf "@{<bf>SubGoal@} %s : %a.@\n"
- part self#pp_state child)
- children
+ begin
+ text#printf " (%a)@\n@{<bf>Sub Goals:@}" pp_status node ;
+ List.iter
+ (fun (part,child) -> text#printf "@\n - %s : %a" part pp_status child)
+ children ;
+ text#printf "@." ;
+ end
method private alternative g a =
let open ProofScript in match a with
- | Tactic(0,{ header },_) -> text#printf "@{<bf>Script@} %s: terminating.@\n" header
+ | Tactic(0,{ header },_) -> text#printf "@{<bf>Script@} %s: finished.@\n" header
| Tactic(n,{ header },_) -> text#printf "@{<bf>Script@} %s: pending %d.@\n" header n
| Error(msg,_) -> text#printf "@{<bf>Script@} Error (%S).@\n" msg
| Prover(p,r) ->
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index a1cd8c082965e828251e992e1f7d4ec8990ea82c..cf1934d1e049824f31ae271281701a52a06300b0 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -196,9 +196,24 @@ let rec varpoly k x = function
| [] -> Warning.error "Unbound type parameter <%s>" x
| y::ys -> if x = y then k else varpoly (succ k) x ys
+type t_builtin = E_mdt of mdt | E_poly of (tau list -> tau)
+
let builtins = Hashtbl.create 131
-let rec tau_of_ltype t = match Logic_utils.unroll_type ~unroll_typedef:false t with
+let adt lt =
+ try match Hashtbl.find builtins lt.lt_name with
+ | E_mdt m -> Mtype m
+ | E_poly _ -> assert false
+ with Not_found -> Atype lt
+
+let atype lt ts =
+ try match Hashtbl.find builtins lt.lt_name with
+ | E_mdt m -> Logic.Data(Mtype m,ts)
+ | E_poly ftau -> ftau ts
+ with Not_found -> Logic.Data(Atype lt,ts)
+
+let rec tau_of_ltype t =
+ match Logic_utils.unroll_type ~unroll_typedef:false t with
| Linteger -> Logic.Int
| Lreal -> Logic.Real
| Ctype typ -> tau_of_ctype typ
@@ -207,14 +222,10 @@ let rec tau_of_ltype t = match Logic_utils.unroll_type ~unroll_typedef:false t w
Warning.error "array type non-supported(%a)"
Printer.pp_logic_type t
| Ltype _ as b when Logic_const.is_boolean_type b -> Logic.Bool
- | Ltype(lt,ps) ->
- let tau =
- (*TODO: check arity *)
- try Mtype(Hashtbl.find builtins lt.lt_name)
- with Not_found -> Atype lt
- in Logic.Data(tau,List.map tau_of_ltype ps)
-
-let tau_of_return l = match l.l_type with
+ | Ltype(lt,lts) -> atype lt (List.map tau_of_ltype lts)
+
+let tau_of_return l =
+ match l.l_type with
| None -> Logic.Prop
| Some t -> tau_of_ltype t
@@ -268,19 +279,20 @@ end
(* --- Datatypes --- *)
(* -------------------------------------------------------------------------- *)
-let atype lt =
- try Mtype(Hashtbl.find builtins lt.lt_name)
- with Not_found -> Atype lt
-
let get_builtin_type ~name ~link ~library =
- try Mtype (Hashtbl.find builtins name)
+ try match Hashtbl.find builtins name with
+ | E_mdt m -> Mtype m
+ | E_poly _ -> assert false
with Not_found ->
let m = new_extern ~link ~library ~debug:name in
- Hashtbl.add builtins name m ; Mtype m
+ Hashtbl.add builtins name (E_mdt m) ; Mtype m
let set_builtin_type ~name ~link ~library =
let m = new_extern ~link ~library ~debug:name in
- Hashtbl.add builtins name m
+ Hashtbl.add builtins name (E_mdt m)
+
+let set_builtin_poly ~name f =
+ Hashtbl.add builtins name (E_poly f)
let mem_builtin_type ~name =
Hashtbl.mem builtins name
@@ -290,7 +302,9 @@ let is_builtin lt = Hashtbl.mem builtins lt.lt_name
let is_builtin_type ~name = function
| Data(Mtype m,_) ->
begin
- try m == Hashtbl.find builtins name
+ try match Hashtbl.find builtins name with
+ | E_mdt m0 -> m == m0
+ | _ -> false
with Not_found -> false
end
| _ -> false
@@ -729,6 +743,20 @@ struct
let is_pfalse = is_false
let is_equal a b = is_true (e_eq a b)
+ let is_int e =
+ try typeof e = Qed.Logic.Int with Not_found -> false
+
+ let is_real e =
+ try typeof e = Qed.Logic.Real with Not_found -> false
+
+ let is_prop e =
+ try match typeof e with Qed.Logic.Prop | Qed.Logic.Bool -> true | _ -> false
+ with Not_found -> false
+
+ let is_arith e =
+ try match typeof e with Qed.Logic.Int | Qed.Logic.Real -> true | _ -> false
+ with Not_found -> false
+
let p_equal = e_eq
let p_equals = List.map (fun (x,y) -> p_equal x y)
let p_neq = e_neq
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 517f9857173e4c91d9fcb76e029d08d280b7ce11..f835b48962e18d8fe6e85d68af25aa8a6b4ecdbd 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -94,6 +94,7 @@ and source =
| Extern of Engine.link extern
val mem_builtin_type : name:string -> bool
+val set_builtin_poly : name:string -> (tau list -> tau) -> unit
val set_builtin_type : name:string -> link:string infoprover -> library:string -> unit
val get_builtin_type : name:string -> link:string infoprover -> library:string -> adt
val is_builtin : logic_type_info -> bool
@@ -101,12 +102,13 @@ val is_builtin_type : name:string -> tau -> bool
val datatype : library:string -> string -> adt
val record :
link:string infoprover -> library:string -> (string * tau) list -> adt
-val atype : logic_type_info -> adt
val comp : compinfo -> adt
val field : adt -> string -> field
val fields_of_adt : adt -> field list
val fields_of_tau : tau -> field list
val fields_of_field : field -> field list
+val atype : logic_type_info -> tau list -> tau
+val adt : logic_type_info -> adt (** Must not be a builtin *)
type balance = Nary | Left | Right
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 8fa7c5044b492f4ace85077d97fbcd48fa0213ee..8b72dbbf23638161d1ef492574243ce79d5b1a1e 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -235,6 +235,8 @@ let add_type ~source name ~library ?(link=Lang.infoprover name) () =
Wp_parameters.warning ~source "Redefinition of type '%s'" name ;
Lang.set_builtin_type ~name ~library ~link
+let hack_type name poly = Lang.set_builtin_poly ~name poly
+
type sanitizer = driver_dir:string -> string -> string
let sanitizers : ( string * string , sanitizer ) Hashtbl.t = Hashtbl.create 10
diff --git a/src/plugins/wp/LogicBuiltins.mli b/src/plugins/wp/LogicBuiltins.mli
index 41a530ff77b0ece0f423052649aa5795b3dc7803..f54c67fd51308b702dc208aa412e2c63797a4eaa 100644
--- a/src/plugins/wp/LogicBuiltins.mli
+++ b/src/plugins/wp/LogicBuiltins.mli
@@ -115,4 +115,7 @@ val lookup : string -> kind list -> builtin
of this symbol with the provided Qed function on terms. *)
val hack : string -> (F.term list -> F.term) -> unit
+(** Replace a logic type definition or predicate by a built-in type. *)
+val hack_type : string -> (F.tau list -> F.tau) -> unit
+
val dump : unit -> unit
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 69e3a0ea22a775b3f89247091212618447289c0e..27f13b6965a9a6129207f2f2d07d0533af2e2f95 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -840,6 +840,7 @@ struct
) sparam
let call_fun env
+ (result:F.tau)
(phi:logic_info)
(labels:logic_label list)
(parameters:F.term list) : F.term =
@@ -847,7 +848,7 @@ struct
| CST c -> e_zint c
| SIG sparam ->
let es = call_params env phi labels sparam parameters in
- F.e_fun (ACSL phi) es
+ F.e_fun ~result (ACSL phi) es
let call_pred env
(phi:logic_info)
@@ -871,11 +872,12 @@ struct
of arity 0 are represented in the AST as a variable not
as an application of the function with no arguments *)
let cst = Logic_env.find_logic_cons x in
+ let result = Lang.tau_of_ltype x.lv_type in
let v =
match LogicBuiltins.logic cst with
- | ACSLDEF -> call_fun env cst [] []
+ | ACSLDEF -> call_fun env result cst [] []
| HACK phi -> phi []
- | LFUN phi -> e_fun phi [] ~result:(Lang.tau_of_ltype x.lv_type)
+ | LFUN phi -> e_fun ~result phi []
in Cvalues.plain x.lv_type v
with Not_found ->
if Logic_env.is_logic_function x.lv_name then
diff --git a/src/plugins/wp/LogicCompiler.mli b/src/plugins/wp/LogicCompiler.mli
index a34f3a35511f0f8ecd7a8f06270419e251ec7c9c..6f818870f67f5de55d733cf86722e415d099db5a 100644
--- a/src/plugins/wp/LogicCompiler.mli
+++ b/src/plugins/wp/LogicCompiler.mli
@@ -111,7 +111,9 @@ sig
(** {3 Application} *)
- val call_fun : env -> logic_info
+ val call_fun : env
+ -> tau
+ -> logic_info
-> logic_label list
-> F.term list -> F.term
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 146dc9732866d70dadffce752605936ea23045af..1a84dcf2d3c491674e8b9d914c48f277182d5de3 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -673,10 +673,11 @@ struct
| Tapp(f,ls,ts) ->
let vs = List.map (val_of_term env) ts in
+ let result = Lang.tau_of_ltype t.term_type in
let r = match LogicBuiltins.logic f with
- | ACSLDEF -> C.call_fun env f ls vs
+ | ACSLDEF -> C.call_fun env result f ls vs
| HACK phi -> phi vs
- | LFUN f -> e_fun f vs ~result:(Lang.tau_of_ltype t.term_type)
+ | LFUN f -> e_fun ~result f vs
in Vexp r
| Tlambda _ ->
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index f86ec63be01681a38f4718160c28dc394a20ee52..d049b1ee2eb99347c69d567009050dac12b0217d 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -206,33 +206,15 @@ let children n =
(* -------------------------------------------------------------------------- *)
type status = [ `Main | `Proved | `Pending of int ]
-type state = [ `Opened | `Proved | `Pending of int | `Script of int ]
let status t : status =
match t.root with
| None ->
if Wpo.is_proved t.main then `Proved else `Main
| Some root ->
- `Pending (pending root)
-
-
-let opened n = not (Wpo.is_proved n.goal)
-
-let state n =
- if Wpo.is_proved n.goal then `Proved else
- match n.script with
- | Opened -> `Opened
- | Script s ->
- begin
- match List.partition ProofScript.is_prover s with
- | [] , s -> `Script (ProofScript.status s)
- | p , [] -> `Pending (ProofScript.status p)
- | provers , scripts ->
- let np = ProofScript.status provers in
- let ns = ProofScript.status scripts in
- `Script( min ns np )
- end
- | Tactic _ -> `Pending (pending n)
+ match root.script with
+ | Opened | Script _ -> `Main
+ | Tactic _ -> `Pending (pending root)
(* -------------------------------------------------------------------------- *)
(* --- Navigation --- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index b36f120911be60d77e3d0c21cd757aa0d5d138c1..2150cbae4c1ffbeae3e3a3dd88ecec4e186d2460 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -36,7 +36,6 @@ val validate : ?incomplete:bool -> tree -> unit
(** Leaves are numbered from 0 to n-1 *)
type status = [ `Main | `Proved | `Pending of int ]
-type state = [ `Opened | `Proved | `Pending of int | `Script of int ]
type current = [ `Main | `Internal of node | `Leaf of int * node ]
type position = [ `Main | `Node of node | `Leaf of int ]
@@ -53,13 +52,11 @@ val head : tree -> Wpo.t
val goal : node -> Wpo.t
val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
-val opened : node -> bool (** not proved *)
-val proved : node -> bool (** not opened *)
val title : node -> string
-val state : node -> state
+val proved : node -> bool
+val pending : node -> int (** 0 means proved *)
val parent : node -> node option
-val pending : node -> int
val children : node -> (string * node) list
val tactical : node -> ProofScript.jtactic option
val get_strategies : node -> int * Strategy.t array (* current index *)
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index 35a027f61a35a1e10590516cd76d315596172eed..1c25e49dd9e0623ad45c792981b0f0363f56d5e9 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -369,16 +369,18 @@ let pending = function
| Tactic(n,_,_) -> n
| Error _ -> 1
-let rec status = function
+let rec pending_any = function
| [] -> 1
| [a] -> pending a
| a::s ->
let n = pending a in
- if n = 0 then 0 else min n (status s)
+ if n = 0 then 0 else min n (pending_any s)
let rec subgoals n = function
| [] -> n
- | (_,a)::s -> subgoals (n + status a) s
+ | (_,js)::s -> subgoals (n + pending_any js) s
+
+let has_proof = List.exists is_tactic
let a_prover p r = Prover(p,r)
let a_tactic tac children = Tactic(subgoals 0 children,tac,children)
diff --git a/src/plugins/wp/ProofScript.mli b/src/plugins/wp/ProofScript.mli
index aca4732eea85763555c4597783ed0c00ec910921..5f599ff49d1cb8f6630f5a36e4c4cb9bcc452ea2 100644
--- a/src/plugins/wp/ProofScript.mli
+++ b/src/plugins/wp/ProofScript.mli
@@ -43,7 +43,8 @@ val a_prover : VCS.prover -> VCS.result -> alternative
val a_tactic : jtactic -> (string * jscript) list -> alternative
val pending : alternative -> int (** pending goals *)
-val status : jscript -> int (** minimum of pending goals *)
+val pending_any : jscript -> int (** minimum of pending goals *)
+val has_proof : jscript -> bool (** Has a tactical alternative *)
val decode : Json.t -> jscript
val encode : jscript -> Json.t
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index 946fc35b9cc5a266d7fff5b1ec0641b78ded0280..a9874efb94c2f35398c1d95826ef27f5e8d964d0 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -173,7 +173,7 @@ class visitor fmt c =
method on_type lt def =
begin
self#lines ;
- engine#declare_type fmt (Lang.atype lt) (List.length lt.lt_params) def ;
+ engine#declare_type fmt (Lang.adt lt) (List.length lt.lt_params) def ;
end
method on_comp c fts =
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index 19b82a4ef4163d4d2ac13019ba5a144082d7d442..9a6f0499405192fd22ea015b1b8496ca10027741 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -178,7 +178,7 @@ class visitor fmt c =
method on_type lt def =
begin
self#lines ;
- engine#declare_type fmt (Lang.atype lt) (List.length lt.lt_params) def ;
+ engine#declare_type fmt (Lang.adt lt) (List.length lt.lt_params) def ;
end
method on_comp c fts =
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 7e2b91afb6f9eb66305c9baee77613b743034ab0..f0ba4bedf839e9865ba25f19b076a84736b63980 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -463,6 +463,7 @@ let search
(* -------------------------------------------------------------------------- *)
let proofs = Hashtbl.create 32
+
let has_proof wpo =
let wid = wpo.Wpo.po_gid in
try Hashtbl.find proofs wid
@@ -471,7 +472,7 @@ let has_proof wpo =
let ok =
try
let script = ProofScript.decode (ProofSession.load wpo) in
- ProofScript.status script = 0
+ ProofScript.has_proof script
with _ -> false in
(Hashtbl.add proofs wid ok ; ok)
else false
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index e3f3b6659e42f7391963d23be06e5b775cfcaaff..1284425bd9855e200a6e4541ffd78759b50e8e25 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -294,7 +294,11 @@ let rec of_term ~cnv expected t : Why3.Term.term =
Wp_parameters.debug ~dkey:dkey_api
"of_term %a %a@."
Lang.F.Tau.pretty expected Lang.F.pp_term t;
- let sort = Lang.F.typeof t in
+ let sort =
+ try Lang.F.typeof t
+ with Not_found ->
+ why3_failure "@[<hov 2>Untyped term: %a@]" Lang.F.pp_term t
+ in
let ($) f x = f x in
let r =
try coerce ~cnv sort expected $ Lang.F.Tmap.find t cnv.subst
@@ -1041,7 +1045,8 @@ type prover_call = {
prover : Why3Provers.t ;
call : Why3.Call_provers.prover_call ;
steps : int option ;
- timeover : float option ;
+ timeout : int ;
+ mutable timeover : float option ;
mutable interrupted : bool ;
mutable killed : bool ;
}
@@ -1051,7 +1056,9 @@ let ping_prover_call p =
| NoUpdates
| ProverStarted ->
let () = match p.timeover with
- | None -> ()
+ | None ->
+ let started = Unix.time () in
+ p.timeover <- Some (started +. 2.0 +. float p.timeout)
| Some timeout ->
let time = Unix.time () in
if time > timeout then
@@ -1076,7 +1083,7 @@ let ping_prover_call p =
| OutOfMemory -> VCS.failed "out of memory"
| StepLimitExceeded -> VCS.result ?steps:p.steps VCS.Stepout
| Unknown _ -> VCS.unknown
- | _ when p.interrupted -> VCS.timeout (int_of_float pr.pr_time)
+ | _ when p.interrupted -> VCS.timeout p.timeout
| Failure s -> VCS.failed s
| HighFailure ->
let alt_ergo_hack =
@@ -1109,15 +1116,12 @@ let call_prover ~timeout ~steplimit drv prover prover_config task =
Why3.Whyconf.print_prover prover
(Why3.Opt.get_def (-1) timeout)
(Why3.Opt.get_def (-1) steps);
- let timeover = match timeout with
- | None -> None | Some tlimit ->
- let started = Unix.time () in
- Some (started +. 2.0 +. float tlimit) in
+ let timeout = match timeout with None -> 0 | Some tlimit -> tlimit in
let pcall = {
call ; prover ;
killed = false ;
interrupted = false ;
- steps ; timeover ;
+ steps ; timeout ; timeover = None ;
} in
let ping = function
| Task.Kill ->
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 91484aa918fd0494b496c942362a430880329c48..df18c879a4fa263f3ef91d51675738da444f4a10 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -192,7 +192,7 @@ class split =
split_cmp "Split (eq.)" x y
| Neq(x,y) when not (is_prop x || is_prop y) ->
split_cmp "Split (neq.)" x y
- | _ when F.is_prop e->
+ | _ when F.is_prop e ->
feedback#set_title "Split (true,false)" ;
feedback#set_descr "Decompose between True and False values" ;
let cases = ["True",F.p_bool e;"False",F.p_not (F.p_bool e)] in
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 473cd6e4c7b3e2905dcb1d3c72a45fc48ed1d660..8784ed5bd1cc7048ff48f963219d229ec4ae412e 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -55,13 +55,10 @@ let l_repeat = Lang.(E.({
let a_list = Lang.get_builtin_type ~library ~name:t_list ~link:l_list
-let _list_of t = L.Data(a_list,[t])
-
let vlist_get_tau = function
| None -> invalid_arg "a list operator without result type"
| Some t -> t
-
let ty_nil = function _ -> invalid_arg "All nil must be typed"
let ty_listelt = function