Commit 4acc6d27 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'new_ide'

parents c58cdd85 c31496d6
......@@ -196,7 +196,7 @@ LIBGENERATED = src/util/config.ml \
LIB_UTIL = config bigInt util opt lists strings \
pp extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer \
hashcons wstdlib exn_printer \
json_base json_parser json_lexer \
debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue
......@@ -2022,7 +2022,7 @@ endif
MODULESTODOC = \
util/util util/opt util/lists util/strings \
util/extmap util/extset util/exthtbl \
util/weakhtbl util/stdlib util/rc util/debug \
util/weakhtbl util/wstdlib util/rc util/debug \
util/loc util/pp util/bigInt util/number \
core/ident core/ty core/term core/decl core/coercion core/theory \
core/env core/task core/trans core/pretty core/printer \
......
......@@ -18,9 +18,14 @@ function f int : int
goal g3: forall x:int.
forall z. z = x+1 ->
forall y. y = z ->
forall y. y+1 = z ->
x = f y -> y = f y + 1
predicate p int
predicate q int
goal g2: forall x. p x -> forall y:int. x = y -> q x
end
module Other
......
......@@ -5,11 +5,7 @@
<file name="../16_subst.mlw">
<theory name="Issue16">
<goal name="g2">
<transf name="simplify_trivial_quantification_in_goal" >
<goal name="g2.0">
</goal>
</transf>
<transf name="split_vc" >
<transf name="introduce_premises" >
<goal name="g2.0">
<transf name="subst" arg1="x">
<goal name="g2.0.0">
......@@ -17,20 +13,70 @@
</transf>
</goal>
</transf>
<transf name="simplify_trivial_quantification_in_goal" >
<goal name="g2.0">
</goal>
</transf>
</goal>
<goal name="g1">
<transf name="introduce_premises" >
<goal name="g1.0">
<transf name="subst_all" >
<goal name="g1.0.0">
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
<theory name="More">
<goal name="g3">
<transf name="introduce_premises" >
<goal name="g3.0">
<transf name="subst" arg1="z,x">
<goal name="g3.0.0">
</goal>
</transf>
<transf name="subst" arg1="z">
<goal name="g3.0.0">
</goal>
</transf>
<transf name="subst" arg1="x">
<goal name="g3.0.0">
</goal>
</transf>
<transf name="subst_all" >
<goal name="g3.0.0">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="g2">
<transf name="introduce_premises" >
<goal name="g2.0">
<transf name="subst" arg1="x">
<goal name="g2.0.0">
</goal>
</transf>
<transf name="subst_all" >
<goal name="g2.0.0">
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
<theory name="Other">
<goal name="g">
<transf name="subst" arg1="x">
<goal name="g.0">
</goal>
</transf>
<transf name="subst" arg1="y">
<goal name="g.0">
</goal>
</transf>
<transf name="subst_all" >
<goal name="g.0">
</goal>
......
......@@ -236,7 +236,7 @@ let () =
(* BEGIN{closemodule} *)
let () = Typing.close_module Loc.dummy_position
let mods : Pmodule.pmodule Stdlib.Mstr.t = Typing.close_file ()
let mods : Pmodule.pmodule Wstdlib.Mstr.t = Typing.close_file ()
(* END{closemodule} *)
(* Checking the VCs *)
......@@ -244,7 +244,7 @@ let mods : Pmodule.pmodule Stdlib.Mstr.t = Typing.close_file ()
(* BEGIN{checkingvcs} *)
let my_tasks : Task.task list =
let mods =
Stdlib.Mstr.fold
Wstdlib.Mstr.fold
(fun _ m acc ->
List.rev_append (Task.split_theory m.Pmodule.mod_theory None None) acc)
mods []
......
......@@ -20,7 +20,7 @@
open Format
open Why3
open Stdlib
open Wstdlib
open Whyconf
open Theory
open Task
......
......@@ -34,7 +34,7 @@
{
open Why3
open Stdlib
open Wstdlib
type vars = Term.term array
let get_indice i =
......
......@@ -45,7 +45,7 @@ open Why3
open Theory
open Term
open Stdlib
open Wstdlib
open Ident
......
......@@ -13,7 +13,7 @@ open Why3
open Pmodule
open Py_ast
open Ptree
open Stdlib
open Wstdlib
let debug = Debug.register_flag "python"
~desc:"mini-python plugin debug flag"
......
......@@ -13,7 +13,7 @@ open Format
open Tptp_ast
open Why3
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -10,5 +10,5 @@
(********************************************************************)
val typecheck : Why3.Env.env -> Why3.Env.pathname ->
Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Stdlib.Mstr.t
Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Wstdlib.Mstr.t
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-2.2.0"
exec = "alt-ergo-2.0.0"
exec = "alt-ergo-1.30"
exec = "alt-ergo-1.01"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok = "2.0.0"
version_old = "1.30"
version_old = "1.30"
version_old = "1.01"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
......@@ -562,6 +562,7 @@ support_library = "%l/coq/version"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.8.0"
version_ok = "^8\.7\.[0-2]$"
version_ok = "8.6.1"
version_ok = "8.6"
......
......@@ -131,6 +131,7 @@ let is_global evd c t = is_global evd (Lazy.force c) t
module Why3tac = struct
open Why3
open Wstdlib
open Call_provers
open Whyconf
open Ty
......@@ -836,11 +837,11 @@ and decompose_definition dep env evd c =
| Some b ->
let tvs = List.fold_left Ty.ty_freevars Stv.empty
(Ty.oty_cons ls.ls_args ls.ls_value) in
let add tv tvm = Stdlib.Mstr.add tv.tv_name.Ident.id_string tv tvm in
let tvm = Stv.fold add tvs Stdlib.Mstr.empty in
let add tv tvm = Mstr.add tv.tv_name.Ident.id_string tv tvm in
let tvm = Stv.fold add tvs Mstr.empty in
let ty = type_of_global env r in
let (_, vars), env, _ = decomp_type_quantifiers env evd ty in
let conv tv = Stdlib.Mstr.find tv.tv_name.Ident.id_string tvm in
let conv tv = Mstr.find tv.tv_name.Ident.id_string tvm in
let vars = List.map conv vars in
let tvm, env, b = decomp_type_lambdas Idmap.empty env evd vars (of_constr b) in
let (bv, vsl), env, b =
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
(** Library environment *)
......
......@@ -11,7 +11,7 @@
(** {1 Environments} *)
open Stdlib
open Wstdlib
(** Local type aliases *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
(** Labels *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Format
open Term
open Ident
......@@ -133,28 +133,28 @@ let array_add_element ~array ~index ~value =
let convert_float_value f =
match f with
| Plus_infinity ->
let m = Mstr.add "cons" (Json_base.String "Plus_infinity") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json_base.String "Plus_infinity") Mstr.empty in
Json_base.Record m
| Minus_infinity ->
let m = Mstr.add "cons" (Json_base.String "Minus_infinity") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json_base.String "Minus_infinity") Mstr.empty in
Json_base.Record m
| Plus_zero ->
let m = Mstr.add "cons" (Json_base.String "Plus_zero") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json_base.String "Plus_zero") Mstr.empty in
Json_base.Record m
| Minus_zero ->
let m = Mstr.add "cons" (Json_base.String "Minus_zero") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json_base.String "Minus_zero") Mstr.empty in
Json_base.Record m
| Not_a_number ->
let m = Mstr.add "cons" (Json_base.String "Not_a_number") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json_base.String "Not_a_number") Mstr.empty in
Json_base.Record m
| Float_value (b, eb, sb) ->
let m = Mstr.add "cons" (Json_base.String "Float_value") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json_base.String "Float_value") Mstr.empty in
let m = Mstr.add "sign" (Json_base.String b) m in
let m = Mstr.add "exponent" (Json_base.String eb) m in
let m = Mstr.add "significand" (Json_base.String sb) m in
Json_base.Record m
| Float_hexa(s,f) ->
let m = Mstr.add "cons" (Json_base.String "Float_hexa") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json_base.String "Float_hexa") Mstr.empty in
let m = Mstr.add "str_hexa" (Json_base.String s) m in
let m = Mstr.add "value" (Json_base.Float f) m in
Json_base.Record m
......@@ -162,46 +162,46 @@ let convert_float_value f =
let rec convert_model_value value : Json_base.json =
match value with
| Integer s ->
let m = Mstr.add "type" (Json_base.String "Integer") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Integer") Mstr.empty in
let m = Mstr.add "val" (Json_base.String s) m in
Json_base.Record m
| Float f ->
let m = Mstr.add "type" (Json_base.String "Float") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Float") Mstr.empty in
let m = Mstr.add "val" (convert_float_value f) m in
Json_base.Record m
| Decimal (int_part, fract_part) ->
let m = Mstr.add "type" (Json_base.String "Decimal") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Decimal") Mstr.empty in
let m = Mstr.add "val" (Json_base.String (int_part^"."^fract_part)) m in
Json_base.Record m
| Fraction (num, den) ->
let m = Mstr.add "type" (Json_base.String "Fraction") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Fraction") Mstr.empty in
let m = Mstr.add "val" (Json_base.String (num^"/"^den)) m in
Json_base.Record m
| Unparsed s ->
let m = Mstr.add "type" (Json_base.String "Unparsed") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Unparsed") Mstr.empty in
let m = Mstr.add "val" (Json_base.String s) m in
Json_base.Record m
| Bitvector v ->
let m = Mstr.add "type" (Json_base.String "Bv") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Bv") Mstr.empty in
let m = Mstr.add "val" (Json_base.String v) m in
Json_base.Record m
| Boolean b ->
let m = Mstr.add "type" (Json_base.String "Boolean") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Boolean") Mstr.empty in
let m = Mstr.add "val" (Json_base.Bool b) m in
Json_base.Record m
| Array a ->
let l = convert_array a in
let m = Mstr.add "type" (Json_base.String "Array") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Array") Mstr.empty in
let m = Mstr.add "val" (Json_base.List l) m in
Json_base.Record m
| Apply (s, lt) ->
let lt = List.map convert_model_value lt in
let slt =
let m = Mstr.add "list" (Json_base.List lt) Stdlib.Mstr.empty in
let m = Mstr.add "list" (Json_base.List lt) Mstr.empty in
let m = Mstr.add "apply" (Json_base.String s) m in
Json_base.Record m
in
let m = Mstr.add "type" (Json_base.String "Apply") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Apply") Mstr.empty in
let m = Mstr.add "val" slt m in
Json_base.Record m
| Record r ->
......@@ -209,21 +209,21 @@ let rec convert_model_value value : Json_base.json =
and convert_array a =
let m_others =
Mstr.add "others" (convert_model_value a.arr_others) Stdlib.Mstr.empty in
Mstr.add "others" (convert_model_value a.arr_others) Mstr.empty in
convert_indices a.arr_indices @ [Json_base.Record m_others]
and convert_indices indices =
match indices with
| [] -> []
| index :: tail ->
let m = Mstr.add "indice" (Json_base.String index.arr_index_key) Stdlib.Mstr.empty in
let m = Mstr.add "indice" (Json_base.String index.arr_index_key) Mstr.empty in
let m = Mstr.add "value" (convert_model_value index.arr_index_value) m in
Json_base.Record m :: convert_indices tail
and convert_record r =
let m = Mstr.add "type" (Json_base.String "Record") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json_base.String "Record") Mstr.empty in
let fields = convert_fields r in
let m_field = Mstr.add "Field" fields Stdlib.Mstr.empty in
let m_field = Mstr.add "Field" fields Mstr.empty in
let m = Mstr.add "val" (Json_base.Record m_field) m in
Json_base.Record m
......@@ -231,7 +231,7 @@ and convert_fields fields =
Json_base.List
(List.map
(fun (f, v) ->
let m = Mstr.add "field" (Json_base.String f) Stdlib.Mstr.empty in
let m = Mstr.add "field" (Json_base.String f) Mstr.empty in
let m = Mstr.add "value" (convert_model_value v) m in
Json_base.Record m)
fields)
......@@ -357,8 +357,8 @@ let print_location fmt m_element =
** Model definitions
***************************************************************
*)
module IntMap = Stdlib.Mint
module StringMap = Stdlib.Mstr
module IntMap = Mint
module StringMap = Mstr
type model_file = model_element list IntMap.t
type model_files = model_file StringMap.t
......@@ -379,7 +379,7 @@ let default_model = {
type model_parser = string -> Printer.printer_mapping -> model
type raw_model_parser =
Stdlib.Sstr.t -> ((string * string) list) Stdlib.Mstr.t ->
Sstr.t -> ((string * string) list) Mstr.t ->
string -> model_element list
(*
......
......@@ -316,7 +316,7 @@ type model_parser = string -> Printer.printer_mapping -> model
*)
type raw_model_parser =
Stdlib.Sstr.t -> ((string * string) list) Stdlib.Mstr.t ->
Wstdlib.Sstr.t -> ((string * string) list) Wstdlib.Mstr.t ->
string -> model_element list
(** Parses the input string into model elements. It contains the list of
projections and a map associating the name of printed projections to the
......
......@@ -11,7 +11,7 @@
open Format
open Pp
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -12,7 +12,7 @@
open Format
open Pp
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......@@ -31,9 +31,9 @@ type 'a pp = Pp.formatter -> 'a -> unit
type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_term_loc : Loc.position option;
queried_terms : Term.term Stdlib.Mstr.t;
list_projections: Stdlib.Sstr.t;
list_records: ((string * string) list) Stdlib.Mstr.t;
queried_terms : Term.term Mstr.t;
list_projections: Sstr.t;
list_records: ((string * string) list) Mstr.t;
}
type printer_args = {
......@@ -56,9 +56,9 @@ exception UnknownPrinter of string
let get_default_printer_mapping = {
lsymbol_m = (function _ -> raise Not_found);
vc_term_loc = None;
queried_terms = Stdlib.Mstr.empty;
list_projections = Stdlib.Sstr.empty;
list_records = Stdlib.Mstr.empty;
queried_terms = Mstr.empty;
list_projections = Sstr.empty;
list_records = Mstr.empty;
}
let register_printer ~desc s p =
......@@ -228,9 +228,9 @@ let get_type_arguments t = match t.t_node with
let m = oty_match Mtv.empty ls.ls_value t.t_ty in
let m = List.fold_left2
(fun m ty t -> oty_match m (Some ty) t.t_ty) m ls.ls_args tl in
let name tv = Stdlib.Mstr.add tv.tv_name.id_string in
let m = Mtv.fold name m Stdlib.Mstr.empty in
Array.of_list (Stdlib.Mstr.values m)
let name tv = Mstr.add tv.tv_name.id_string in
let m = Mtv.fold name m Mstr.empty in
Array.of_list (Mstr.values m)
| _ ->
[||]
......
......@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
open Wstdlib
open Ident
open Ty
open Term
......@@ -28,12 +29,12 @@ type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_term_loc : Loc.position option;
(* The position of the term that triggers the VC *)
queried_terms : Term.term Stdlib.Mstr.t;
queried_terms : Term.term Mstr.t;
(* The list of terms that were queried for the counter-example
by the printer *)
list_projections: Stdlib.Sstr.t;
list_projections: Sstr.t;
(* List of projections as printed in the model *)
list_records: ((string * string) list) Stdlib.Mstr.t;
list_records: ((string * string) list) Mstr.t;
}
type printer_args = {
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
......
......@@ -10,7 +10,7 @@
(********************************************************************)
open Format
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
(** Theories and Namespaces *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ty
open Term
open Decl
......
......@@ -16,7 +16,7 @@ open Term
open Decl
open Theory
open Task
open Stdlib
open Wstdlib
(** {2 Transformations} *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
(** Types *)
......@@ -18,7 +18,7 @@ type tvsymbol = {
tv_name : ident;
}
module Tvar = Stdlib.MakeMSHW (struct
module Tvar = MakeMSHW (struct
type t = tvsymbol
let tag tv = tv.tv_name.id_tag
end)
......@@ -63,7 +63,7 @@ and ty_node =
| Tyvar of tvsymbol
| Tyapp of tysymbol * ty list
module Tsym = Stdlib.MakeMSHW (struct
module Tsym = MakeMSHW (struct
type t = tysymbol
let tag ts = ts.ts_name.id_tag
end)
......
......@@ -40,7 +40,7 @@ The regexp must start with ^.
*)
open Format
open Stdlib
open Wstdlib
open Whyconf
module Wc = Whyconf
open Rc
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Smt2_model_defs
exception Not_value
......
......@@ -9,6 +9,8 @@
(* *)
(********************************************************************)
open Wstdlib
(* Debugging function *)
val print_table:
Smt2_model_defs.correspondence_table -> unit
......@@ -21,10 +23,10 @@ val print_table:
This function has the information of the records that were saved.
*)
val register_apply_to_records:
((string list) Stdlib.Mstr.t -> Smt2_model_defs.term -> Smt2_model_defs.term) ->
((string list) Mstr.t -> Smt2_model_defs.term -> Smt2_model_defs.term) ->
unit
(* From the table generated by the parser, build a list of model_element *)
val create_list:
Stdlib.Sstr.t -> ((string * string) list) Stdlib.Mstr.t -> Smt2_model_defs.correspondence_table ->
Sstr.t -> ((string * string) list) Mstr.t -> Smt2_model_defs.correspondence_table ->
Model_parser.model_element list
......@@ -10,7 +10,7 @@
(********************************************************************)
open Format
open Stdlib
open Wstdlib
open Ident
open Term
open Decl
......
......@@ -46,7 +46,7 @@ let do_parsing model =
~loc:(get_position lexbuf)
"Error@ during@ lexing@ of@ smtlib@ model:@ unexpected text '%s'"
l;
Stdlib.Mstr.empty
Wstdlib.Mstr.empty
| Parse_smtv2_model_parser.Error ->
let l = Lexing.lexeme lexbuf in
Debug.dprintf debug "smtv2 model parser: Error on lexeme '%s'@." l;
......@@ -55,7 +55,7 @@ let do_parsing model =
~loc:loc
"Error@ during@ parsing@ of@ smtlib@ model: unexpected text '%s'"
l;
Stdlib.Mstr.empty
Wstdlib.Mstr.empty
let do_parsing list_proj list_records model =
let m = do_parsing model in
......@@ -71,9 +71,9 @@ let parse : raw_model_parser = fun list_proj list_records input ->
(* let r = Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
ignore (Str.search_forward r input 0);
let match_end = Str.match_end () in*)
let nr = Str.regexp "^)" in
let nr = Str.regexp "^)+" in
let res = Str.search_backward nr input (String.length input) in
let model_string = String.sub input 0 (res + 1) in
let model_string = String.sub input 0 (res + String.length (Str.matched_string input