Commit 32935523 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'master' into new_system

parents 8b15686f b9e41718
......@@ -15,7 +15,7 @@ goods () {
ERROR=
rm -f bench_errors
for f in $1/*.[wm][hl][yw] ; do
echo -n " $f... "
printf " $f... "
# running Why
if ! $pgm $2 $f > /dev/null 2> bench_error; then
echo "FAILED!"
......@@ -42,7 +42,7 @@ goods () {
bads () {
pgm="bin/why3prove$suffix"
for f in $1/*.[wm][hl][yw] ; do
echo -n " $f... "
printf " $f... "
if $pgm $2 $f > /dev/null 2>&1; then
echo "SHOULD FAIL!"
# echo "env: WHY3DATA='$WHY3DATA'"
......@@ -58,7 +58,7 @@ drivers () {
for f in $1/*.drv; do
if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
if [[ $f == drivers/c.drv ]]; then continue; fi
echo -n " $f... "
printf " $f... "
# running Why
if ! echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f - > /dev/null; then
echo "why FAILED"
......@@ -72,7 +72,7 @@ drivers () {
valid_goals () {
pgm="bin/why3prove$suffix"
for f in $1/*.mlw; do
echo -n " "$f"... "
printf " "$f"... "
if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
echo "valid test $f failed!"
echo "$pgm -P alt-ergo $f"
......@@ -87,7 +87,7 @@ valid_goals () {
invalid_goals () {
pgm="bin/why3prove$suffix"
for f in $1/*.mlw; do
echo -n " "$f"... "
printf " "$f"... "
if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then
echo "invalid test $f failed!"
echo "$pgm -P alt-ergo $f"
......@@ -101,7 +101,7 @@ invalid_goals () {
execute () {
pgm="bin/why3execute$suffix"
echo -n "$1 $2... "
printf "$1 $2... "
if $pgm $1 $2 > /dev/null; then
echo "ok"
else
......@@ -117,17 +117,17 @@ extract_and_run () {
shift
prg=$1
shift
echo -n "$dir... "
printf "$dir... "
rm -f $dir/$prg
echo -n "clean... "
printf "clean... "
if BENCH=yes make -C $dir clean > /dev/null; then
echo -n "extract... "
printf "extract... "
if BENCH=yes make -C $dir extract > /dev/null; then
echo -n "compile... "
printf "compile... "
if BENCH=yes make -C $dir > /dev/null; then
echo -n "execute... "
printf "execute... "
if $dir/main.opt "$@" > /dev/null; then
echo -n "doc... "
printf "doc... "
if BENCH=yes make -C $dir doc > /dev/null; then
echo "ok"
else
......@@ -164,7 +164,7 @@ extract_and_run () {
list_stuff () {
pgm="bin/why3$suffix"
echo -n "$1 "
printf '%s ' "$1"
if $pgm $1 > /dev/null; then
echo "ok"
else
......
......@@ -15,7 +15,7 @@ esac
cd $dir
run_cvc4_15 () {
echo -n " $1... "
printf " $1... "
../bin/why3prove.opt -P "CVC4,1.5" --timelimit 1 --get-ce $1 | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
......
......@@ -25,7 +25,7 @@
# See the GNU Library General Public License version 2 for more details
# (enclosed in the file LGPL).
AC_INIT([Why3], m4_esyscmd([. ./Version; echo -n "$VERSION"]))
AC_INIT([Why3], m4_esyscmd([. ./Version; printf "$VERSION"]))
# verbosemake
......
......@@ -6,6 +6,7 @@ valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "eliminate_negative_constants"
transformation "eliminate_epsilon"
transformation "eliminate_if_fmla"
transformation "eliminate_let_fmla"
......
......@@ -22,6 +22,7 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_negative_constants"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
module Issue43
type t = < range 0 1 >
constant c : int = t'minInt
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../43_range_module.mlw" proved="true">
<theory name="Issue43" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
......@@ -39,11 +39,11 @@ export shapes=""
run_dir () {
for f in `ls $1/*/why3session.xml`; do
d=`dirname $f`
echo -n "Replaying $d ... "
printf "Replaying $d ... "
../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP
ret=$?
if test "$ret" != "0" ; then
echo -n "FAILED (ret code=$ret):"
printf "FAILED (ret code=$ret):"
out=`head -1 $TMP`
if test -z "$out" ; then
echo "standard error: (standard output empty)"
......@@ -53,7 +53,7 @@ run_dir () {
fi
res=1
else
echo -n "OK"
printf "OK"
cat $TMP $TMPERR
success=`expr $success + 1`
fi
......
......@@ -290,8 +290,7 @@ let d2 =
(* e1 : the appropriate instance of "ref" *)
let e1 = Mlw_expr.e_arrow ref_fun [Mlw_ty.ity_int] ity in
(* we apply it to 0 *)
let c0 = Mlw_expr.e_const
(Number.ConstInt (Number.int_const_dec "0")) Mlw_ty.ity_int in
let c0 = Mlw_expr.e_const (Number.const_of_int 0) Mlw_ty.ity_int in
Mlw_expr.e_app e1 [c0]
in
(* building the first part of the let x = ref 0 *)
......
......@@ -81,7 +81,7 @@ let mk_lexpr p = { term_loc = Loc.dummy_position;
term_desc = p }
let mk_const s =
mk_lexpr (Tconst(Number.ConstInt(Number.int_const_dec s)))
mk_lexpr (Tconst Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s }))
let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position }
......
......@@ -44,10 +44,10 @@ let deref_id ~loc id =
mk_expr ~loc (Eidapp (prefix ~loc "!", [mk_expr ~loc (Eident (Qident id))]))
let array_set ~loc a i v =
mk_expr ~loc (Eidapp (mixfix ~loc "[]<-", [a; i; v]))
let constantd ~loc s =
mk_expr ~loc (Econst (Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec s})))
let constant ~loc n =
mk_expr ~loc (Econst (Number.(ConstInt (int_const_of_int n))))
let constant ~loc i =
mk_expr ~loc (Econst (Number.const_of_int i))
let constant_s ~loc s =
mk_expr ~loc (Econst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s})))
let len ~loc =
Qident (mk_id ~loc "len")
let break ~loc =
......@@ -137,7 +137,7 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
| Py_ast.Ebool b ->
mk_expr ~loc (if b then Etrue else Efalse)
| Py_ast.Eint s ->
constantd ~loc s
constant_s ~loc s
| Py_ast.Estring _s ->
mk_unit ~loc (*FIXME*)
| Py_ast.Eident id ->
......
......@@ -307,7 +307,7 @@ term_arg: mk_term(term_arg_) { $1 }
term_arg_:
| ident { Tident (Qident $1) }
| INTEGER { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec $1})) }
| INTEGER { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec $1})) }
| NONE { Ttuple [] }
| TRUE { Ttrue }
| FALSE { Tfalse }
......
......@@ -285,7 +285,7 @@ let rec ty denv env impl { e_loc = loc; e_node = n } = match n with
| Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected
let t_int_const s =
t_const (Number.(ConstInt { ic_negative = false; ic_abs = int_const_dec s})) ty_int
t_const (Number.(ConstInt { ic_negative = false; ic_abs = int_literal_dec s})) ty_int
(* unused
let t_real_const r = t_const (Number.ConstReal r)
......
[ATP alt-ergo-prv]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-1.20.prv"
exec = "alt-ergo-1.10.prv"
exec = "alt-ergo-1.00.prv"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_old = "1.20.prv"
version_old = "1.10.prv"
version_old = "1.00.prv"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
driver = "alt_ergo"
editor = "altgr-ergo"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
......@@ -43,6 +27,22 @@ command_steps = "%e -no-rm-eq-existential -steps-bound %S %f"
driver = "alt_ergo"
editor = "altgr-ergo"
[ATP alt-ergo-prv]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-1.20.prv"
exec = "alt-ergo-1.10.prv"
exec = "alt-ergo-1.00.prv"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_old = "1.20.prv"
version_old = "1.10.prv"
version_old = "1.00.prv"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
driver = "alt_ergo"
editor = "altgr-ergo"
# CVC4 version 1.5
[ATP cvc4-15]
name = "CVC4"
......@@ -522,8 +522,9 @@ compile_time_support = true
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.6"
version_ok = "8.7.0"
version_ok = "8.6.1"
version_ok = "8.6"
command = "%e -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
driver = "coq"
editor = "coqide"
......
......@@ -463,17 +463,15 @@ exception NotArithConstant
(* translates a closed Coq term p:positive into a FOL term of type int *)
let big_two = Big_int.succ_big_int Big_int.unit_big_int
let rec tr_positive evd p = match kind evd p with
| Construct _ when is_global evd coq_xH p ->
Big_int.unit_big_int
BigInt.one
| App (f, [|a|]) when is_global evd coq_xI f ->
(* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive evd a))
BigInt.succ (BigInt.mul_int 2 (tr_positive evd a))
| App (f, [|a|]) when is_global evd coq_xO f ->
(* Mult (Cst 2, tr_positive a) *)
Big_int.mult_big_int big_two (tr_positive evd a)
BigInt.mul_int 2 (tr_positive evd a)
| Cast (p, _, _) ->
tr_positive evd p
| _ ->
......@@ -482,21 +480,21 @@ let rec tr_positive evd p = match kind evd p with
let const_of_big_int is_neg b =
Term.t_const
(Number.(ConstInt { ic_negative = is_neg ;
ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) }))
ic_abs = int_literal_raw b }))
ty_int
let const_of_big_int_real is_neg b =
let s = Big_int.string_of_big_int b in
Term.t_const
(Number.(ConstReal { rc_negative = is_neg ;
rc_abs = real_const_dec s "0" None}))
let s = BigInt.to_string b in
Term.t_const (Number.(ConstReal { rc_negative = is_neg ;
rc_abs = real_const_dec s "0" None}))
ty_real
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
let rec tr_arith_constant_IZR evd dep t = match kind evd t with
| Construct _ when is_global evd coq_Z0 t ->
Term.t_const (Number.(ConstReal { rc_negative = false ;
rc_abs = real_const_dec "0" "0" None })) ty_real
rc_abs = real_const_dec "0" "0" None}))
ty_real
| App (f, [|a|]) when is_global evd coq_Zpos f ->
const_of_big_int_real false (tr_positive evd a)
| App (f, [|a|]) when is_global evd coq_Zneg f ->
......
......@@ -330,7 +330,14 @@ let t_compare trigger label t1 t2 =
| Tvar v1, Tvar v2 ->
comp_raise (vs_compare v1 v2)
| Tconst c1, Tconst c2 ->
perv_compare c1 c2
let open Number in
begin match c1, c2 with
| ConstInt { ic_negative = s1; ic_abs = IConstRaw b1 },
ConstInt { ic_negative = s2; ic_abs = IConstRaw b2 } ->
perv_compare s1 s2;
comp_raise (BigInt.compare b1 b2)
| _, _ -> perv_compare c1 c2
end
| Tapp (s1,l1), Tapp (s2,l2) ->
comp_raise (ls_compare s1 s2);
List.iter2 (t_compare bnd vml1 vml2) l1 l2
......@@ -828,8 +835,7 @@ let ps_app ps tl = t_app ps tl None
let t_nat_const n =
assert (n >= 0);
let a = Number.int_const_of_int n in
t_const (Number.ConstInt a) ty_int
t_const (Number.const_of_int n) ty_int
let t_bigint_const n = t_const (Number.const_of_big_int n) Ty.ty_int
......
......@@ -191,7 +191,7 @@ let create_tysymbol name args def =
ignore (ty_v_all check def)
| Range ir ->
if args <> [] then raise IllegalTypeParameters;
if BigInt.lt ir.Number.ir_upper_val ir.Number.ir_lower_val
if BigInt.lt ir.Number.ir_upper ir.Number.ir_lower
then raise EmptyRange
| Float fp ->
if args <> [] then raise IllegalTypeParameters;
......
......@@ -354,7 +354,7 @@ let generate_auto_strategies config =
List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
let code = flush_str_formatter () in
let auto0 = {
strategy_name = "Auto level 0";
strategy_name = "Auto_level_0";
strategy_desc = "Automatic@ run@ of@ main@ provers";
strategy_shortcut = "0";
strategy_code = code }
......@@ -365,7 +365,7 @@ let generate_auto_strategies config =
List.iter (fun s -> fprintf str_formatter "c %s 10 4000@\n" s) provers_level1;
let code = flush_str_formatter () in
let auto1 = {
strategy_name = "Auto level 1";
strategy_name = "Auto_level_1";
strategy_desc = "Automatic@ run@ of@ main@ provers";
strategy_shortcut = "1";
strategy_code = code }
......@@ -392,7 +392,7 @@ let generate_auto_strategies config =
List.iter (fun s -> fprintf str_formatter "c %s 30 4000@\n" s) provers_level2;
let code = flush_str_formatter () in
let auto2 = {
strategy_name = "Auto level 2";
strategy_name = "Auto_level_2";
strategy_desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations";
strategy_shortcut = "2";
strategy_code = code }
......
This diff is collapsed.
......@@ -484,8 +484,7 @@ let e_const c ity =
let e_nat_const n =
assert (n >= 0);
let a = Number.int_const_of_int n in
e_const (Number.ConstInt a) ity_int
e_const (Number.const_of_int n) ity_int
let e_ghostify gh ({e_effect = eff} as e) =
if not gh then e else
......
......@@ -346,12 +346,12 @@ let create_type_decl dl =
(* create max attribute *)
let max_id = id_derive (nm ^ "'maxInt") id in
let max_ls = create_fsymbol max_id [] ty_int in
let max_defn = t_const Number.(ConstInt ir.ir_upper) ty_int in
let max_defn = t_const Number.(const_of_big_int ir.ir_upper) ty_int in
let max_decl = create_logic_decl [make_ls_defn max_ls [] max_defn] in
(* create min attribute *)
let min_id = id_derive (nm ^ "'minInt") id in
let min_ls = create_fsymbol min_id [] ty_int in
let min_defn = t_const Number.(ConstInt ir.ir_lower) ty_int in
let min_defn = t_const Number.(const_of_big_int ir.ir_lower) ty_int in
let min_decl = create_logic_decl [make_ls_defn min_ls [] min_defn] in
let pure = [create_ty_decl ts; pj_decl; max_decl; min_decl] in
let meta = Theory.(meta_range, [MAts ts; MAls pj_ls]) in
......
......@@ -151,13 +151,13 @@ rule token = parse
| uident_quote as id
{ UIDENT_QUOTE id }
| ['0'-'9'] ['0'-'9' '_']* as s
{ INTEGER (Number.int_const_dec (Lexlib.remove_underscores s)) }
{ INTEGER (Number.int_literal_dec (Lexlib.remove_underscores s)) }
| '0' ['x' 'X'] (['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']* as s)
{ INTEGER (Number.int_const_hex (Lexlib.remove_underscores s)) }
{ INTEGER (Number.int_literal_hex (Lexlib.remove_underscores s)) }
| '0' ['o' 'O'] (['0'-'7'] ['0'-'7' '_']* as s)
{ INTEGER (Number.int_const_oct (Lexlib.remove_underscores s)) }
{ INTEGER (Number.int_literal_oct (Lexlib.remove_underscores s)) }
| '0' ['b' 'B'] (['0'-'1'] ['0'-'1' '_']* as s)
{ INTEGER (Number.int_const_bin (Lexlib.remove_underscores s)) }
{ INTEGER (Number.int_literal_bin (Lexlib.remove_underscores s)) }
| (digit+ as i) ("" as f) ['e' 'E'] (['-' '+']? digit+ as e)
| (digit+ as i) '.' (digit* as f) (['e' 'E'] (['-' '+']? digit+ as e))?
| (digit* as i) '.' (digit+ as f) (['e' 'E'] (['-' '+']? digit+ as e))?
......
......@@ -323,15 +323,14 @@ typedefn:
{ $2, TDalias $3 }
(* FIXME: allow negative bounds *)
| EQUAL LT RANGE int_constant int_constant GT
{ (Public, false),
TDrange ($4,$5) }
{ (Public, false), TDrange ($4, $5) }
| EQUAL LT FLOAT INTEGER INTEGER GT
{ (Public, false),
TDfloat (Number.to_small_integer $4, Number.to_small_integer $5) }
int_constant:
| INTEGER { mk_int_const false $1 }
| MINUS INTEGER { mk_int_const true $2 }
| INTEGER { Number.compute_int_literal $1 }
| MINUS INTEGER { BigInt.minus (Number.compute_int_literal $2) }
vis_mut:
| (* epsilon *) { Public, false }
......
......@@ -172,7 +172,7 @@ type type_def =
| TDalias of pty
| TDalgebraic of (Loc.position * ident * param list) list
| TDrecord of field list
| TDrange of Number.integer_constant * Number.integer_constant
| TDrange of BigInt.t * BigInt.t
| TDfloat of int * int
type visibility = Public | Private | Abstract (* = Private + ghost fields *)
......
......@@ -200,13 +200,13 @@ let rec print_term info defs fmt t = match t.t_node with
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = true;
Number.negative_int_support = Number.Number_default;
Number.negative_int_support = Number.Number_unsupported;
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_unsupported;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.negative_real_support = Number.Number_default;
Number.negative_real_support = Number.Number_unsupported;
Number.dec_real_support = Number.Number_unsupported;
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
......
......@@ -81,7 +81,7 @@ type controller =
controller_env: Env.env;
controller_provers:
(Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_strategies : (string * string * Strategy.instruction array) Stdlib.Hstr.t;
controller_strategies : (string * string * string * Strategy.instruction array) Stdlib.Hstr.t;
controller_running_proof_attempts : unit Hpan.t;
}
......
......@@ -88,7 +88,7 @@ type controller = private
controller_config : Whyconf.config;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_strategies : (string * string * Strategy.instruction array) Stdlib.Hstr.t;
controller_strategies : (string * string * string * Strategy.instruction array) Stdlib.Hstr.t;
controller_running_proof_attempts : unit Hpan.t;
}
......
......@@ -45,7 +45,7 @@ type message_notification =
| Help of string
| Information of string
| Task_Monitor of int * int * int
| Parse_Or_Type_Error of Loc.position * string
| Parse_Or_Type_Error of Loc.position * Loc.position * string
| File_Saved of string
| Error of string
| Open_File_Error of string
......
......@@ -48,8 +48,9 @@ type message_notification =
| Information of string
(** Number of task scheduled, running, etc *)
| Task_Monitor of int * int * int
(** A file was read or reloaded and now contains a parsing or typing error *)
| Parse_Or_Type_Error of Loc.position * string
(** A file was read or reloaded and now contains a parsing or typing error.
second loc is relative to the session file *)
| Parse_Or_Type_Error of Loc.position * Loc.position * string
(** [File_Saved f] f was saved *)
| File_Saved of string
(** An error happened that could not be identified in server *)
......
......@@ -286,7 +286,7 @@ let print_msg fmt m =
| Help _s -> fprintf fmt "help"
| Information s -> fprintf fmt "info %s" s
| Task_Monitor _ -> fprintf fmt "task montor"
| Parse_Or_Type_Error (_, s) -> fprintf fmt "parse_or_type_error:\n %s" s
| Parse_Or_Type_Error (_, _, s) -> fprintf fmt "parse_or_type_error:\n %s" s
| File_Saved s -> fprintf fmt "file saved %s" s
| Error s -> fprintf fmt "%s" s
| Open_File_Error s -> fprintf fmt "%s" s
......@@ -642,13 +642,12 @@ end
let capture_parse_or_type_errors f cont =
try let _ = f cont in None with
| Loc.Located (loc, e) ->
let loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a at %a@."
Exn_printer.exn_printer e Loc.report_position loc in
Some (loc, s)
let rel_loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a" Exn_printer.exn_printer e in
Some (loc, rel_loc, s)
| e when not (Debug.test_flag Debug.stack_trace) ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
Some (Loc.dummy_position, s)
let s = Format.asprintf "%a" Exn_printer.exn_printer e in
Some (Loc.dummy_position, Loc.dummy_position, s)
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
......@@ -936,10 +935,11 @@ end
| None ->
let file = get_file cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (file_name file)
| Some(loc,s) ->
read_and_send (file_name file);
P.notify (Message (Information "file added in session"))
| Some(loc,rel_loc,s) ->
read_and_send fn;
P.notify (Message (Parse_Or_Type_Error(loc,s)))
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s)))
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
......@@ -998,9 +998,10 @@ end
focus on a specific node. *)
get_focused_label := None;
match x with
| None -> ()
| Some(loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,s)))
| None ->
P.notify (Message (Information "Session initialized succesfully"))
| Some(loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s)))
(* ----------------- Schedule proof attempt -------------------- *)
......@@ -1149,7 +1150,7 @@ end
let d = get_server_data () in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
try
let (n,_,st) = Hstr.find d.cont.controller_strategies s in
let (n,_,_,st) = Hstr.find d.cont.controller_strategies s in
Debug.dprintf debug_strat "[strategy_exec] running strategy '%s'@." n;
let callback sts =
Debug.dprintf debug_strat "[strategy_exec] strategy status: %a@." print_strategy_status sts
......@@ -1211,9 +1212,10 @@ end
match reload_files d.cont ~use_shapes:true with
| None ->
(* TODO: try to restore the previous focus : focused_node := old_focus; *)
reset_and_send_the_whole_tree ()
| Some(loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,s)))
reset_and_send_the_whole_tree ();
P.notify (Message (Information "Session refresh successful"))
| Some(loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s)))
let replay ~valid_only nid : unit =
let d = get_server_data () in
......
......@@ -271,9 +271,10 @@ let convert_message (m: message_notification) =
| Task_Monitor (n, k, p) ->
convert_record ["mess_notif", cc m;
"monitor", List [Int n; Int k; Int p]]
| Parse_Or_Type_Error (loc, s) ->
| Parse_Or_Type_Error (loc, rel_loc,s) ->
convert_record ["mess_notif", cc m;
"loc", convert_loc loc;
"rel_loc", convert_loc rel_loc;
"error", String s]
| Error s ->
convert_record ["mess_notif", cc m;
......@@ -652,8 +653,9 @@ let parse_message constr j =
| "Parse_Or_Type_Error" ->
let loc = parse_loc (get_field j "loc") in
let rel_loc = parse_loc (get_field j "rel_loc") in
let error = get_string (get_field j "error") in
Parse_Or_Type_Error (loc, error)
Parse_Or_Type_Error (loc, rel_loc, error)
| _ -> raise NotMessage
......
......@@ -148,15 +148,15 @@ let load_strategies cont =
let code = Strategy_parser.parse env config code in
let shortcut = st.Whyconf.strategy_shortcut in
Debug.dprintf debug "[session server info] Strategy '%s' loaded.@." name;
Stdlib.Hstr.add cont.Controller_itp.controller_strategies shortcut
(name, st.Whyconf.strategy_desc, code)
Stdlib.Hstr.add cont.Controller_itp.controller_strategies name
(name, shortcut, st.Whyconf.strategy_desc, code)
with Strategy_parser.SyntaxError msg ->
Format.eprintf "Fatal: loading strategy '%s' failed: %s@." name msg;
exit 1)
strategies
let list_strategies cont =
Stdlib.Hstr.fold (fun s (a,_,_) acc -> (s,a)::acc) cont.Controller_itp.controller_strategies []
Stdlib.Hstr.fold (fun _ (name,short,_,_) acc -> (short,name)::acc) cont.Controller_itp.controller_strategies []
let symbol_name s =
......
......@@ -300,6 +300,7 @@ let ident_shape id = id_string_shape id.Ident.id_string
open Number
let integer_const_shape = function
| IConstRaw i -> push (BigInt.to_string i)
| IConstDec s -> push s
| IConstHex s -> push "0x"; push s
| IConstOct s -> push "0o"; push s
......@@ -499,6 +500,7 @@ module Checksum = struct
| CV2 -> ident_v2 b id
let integer_const b = function
| IConstRaw i -> raw_string b (BigInt.to_string i)
| IConstDec s -> raw_string b s
| IConstHex s -> raw_string b "0x"; raw_string b s
| IConstOct s -> raw_string b "0o"; raw_string b s
......
......@@ -119,7 +119,7 @@ g -> print the current task\n\
p -> print the session@." s
| Information s -> fprintf fmt "%s@." s
| Task_Monitor (_t, _s, _r) -> () (* TODO do we want to print something for this? *)
| Parse_Or_Type_Error (_, s) -> fprintf fmt "%s@." s
| Parse_Or_Type_Error (_, _, s) -> fprintf fmt "%s@." s
| Error s ->
fprintf fmt "%s@." s
| Open_File_Error s -> fprintf fmt "%s@." s
......
......@@ -65,8 +65,8 @@ let elim le_int le_real neg_real type_kept kn
let pr = create_prsymbol (id_fresh (ts.ts_name.id_string ^ "'axiom")) in
let v = create_vsymbol (id_fresh "i") (ty_app ts []) in
let v_term = t_app to_int [t_var v] (Some ty_int) in
let a_term = t_const (Number.ConstInt lo) ty_int in
let b_term = t_const (Number.ConstInt hi) ty_int in
let a_term = t_bigint_const lo in
let b_term = t_bigint_const hi in
let f = t_and (t_app le_int [a_term; v_term] None)
(t_app le_int [v_term; b_term] None)
in
......
......@@ -149,7 +149,7 @@ let induction x bound env =
(* Default bound is 0 if not given *)
let bound =
match bound with
| None -> Term.t_const (Number.ConstInt (Number.int_const_of_int 0)) Ty.ty_int
| None -> Term.t_nat_const 0
| Some bound -> bound
in
......
......@@ -14,6 +14,7 @@ open Format
(** Construction *)
type integer_literal =
| IConstRaw of BigInt.t
| IConstDec of string