 Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

### Add support for generic printing of integers and reals.

```Prover capabilities are now represented by a record enumerating each case and which syntax to use then.
This fixes output of nondecimal integers to provers (bug #12981).

TODO: check whether some provers support more than just decimal representations.```
parent b6e03c01
 ... ... @@ -133,7 +133,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \ introduction abstraction close_epsilon lift_epsilon \ eval_match LIB_PRINTER = print_real alt_ergo why3printer smtv1 smtv2 \ LIB_PRINTER = print_number alt_ergo why3printer smtv1 smtv2 \ coq tptp simplify gappa cvc3 yices LIBMODULES = src/config \ ... ...
 theory Number use import int.Int use import real.RealInfix goal dec : 123 = 100 + 23 goal hex : 0x7b = 100 + 23 goal oct : 0o173 = 100 + 23 goal bin : 0b1111011 = 100 + 23 goal real : 1.23e2 = 100. +. 23. goal hexa : 0x7.bp4 = 100. +. 23. end
 ... ... @@ -124,8 +124,8 @@ An arithmetic goal: 2+2 = 4 *) let two : Term.term = Term.t_const (Term.ConstInt "2") let four : Term.term = Term.t_const (Term.ConstInt "4") let two : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "2")) let four : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "4")) let int_theory : Theory.theory = Env.find_theory env ["int"] "Int" let plus_symbol : Term.lsymbol = ... ... @@ -153,7 +153,7 @@ let () = printf "@[On task 3, alt-ergo answers %a@." Call_provers.print_prover_result result3 (* quantifiers: let's build "forall x:int. x*x >= 0" *) let zero : Term.term = Term.t_const (Term.ConstInt "0") let zero : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "0")) let mult_symbol : Term.lsymbol = Theory.ns_find_ls int_theory.Theory.th_export ["infix *"] let ge_symbol : Term.lsymbol = ... ...
 ... ... @@ -121,7 +121,10 @@ let rec print_ty_node inn fmt ty = match ty.ty_node with let print_ty = print_ty_node false let print_const fmt = function | ConstInt s -> fprintf fmt "%s" s | ConstInt (IConstDecimal s) -> fprintf fmt "%s" s | ConstInt (IConstHexa s) -> fprintf fmt "0x%s" s | ConstInt (IConstOctal s) -> fprintf fmt "0o%s" s | ConstInt (IConstBinary s) -> fprintf fmt "0b%s" s | ConstReal (RConstDecimal (i,f,None)) -> fprintf fmt "%s.%s" i f | ConstReal (RConstDecimal (i,f,Some e)) -> fprintf fmt "%s.%se%s" i f e | ConstReal (RConstHexa (i,f,e)) -> fprintf fmt "0x%s.%sp%s" i f e ... ...
 ... ... @@ -255,12 +255,18 @@ type binop = | Timplies | Tiff type integer_constant = | IConstDecimal of string | IConstHexa of string | IConstOctal of string | IConstBinary of string type real_constant = | RConstDecimal of string * string * string option (* int / frac / exp *) | RConstHexa of string * string * string type constant = | ConstInt of string | ConstInt of integer_constant | ConstReal of real_constant type term = { ... ... @@ -462,7 +468,7 @@ let mk_term n ty = Hsterm.hashcons { let t_var v = mk_term (Tvar v) (Some v.vs_ty) let t_const c ty = mk_term (Tconst c) (Some ty) let t_int_const s = mk_term (Tconst (ConstInt s)) (Some Ty.ty_int) let t_int_const s = mk_term (Tconst (ConstInt (IConstDecimal s))) (Some Ty.ty_int) let t_real_const r = mk_term (Tconst (ConstReal r)) (Some Ty.ty_real) let t_app f tl ty = mk_term (Tapp (f, tl)) ty let t_if f t1 t2 = mk_term (Tif (f, t1, t2)) t2.t_ty ... ...
 ... ... @@ -116,12 +116,18 @@ type binop = | Timplies | Tiff type integer_constant = | IConstDecimal of string | IConstHexa of string | IConstOctal of string | IConstBinary of string type real_constant = | RConstDecimal of string * string * string option (* int / frac / exp *) | RConstHexa of string * string * string type constant = | ConstInt of string | ConstInt of integer_constant | ConstReal of real_constant type term = private { ... ...
 ... ... @@ -137,6 +137,17 @@ let loc lb = Loc.extract (lexeme_start_p lb, lexeme_end_p lb) let remove_underscores s = if String.contains s '_' then begin let count = let nb = ref 0 in String.iter (fun c -> if c = '_' then incr nb) s; !nb in let t = String.create (String.length s - count) in let i = ref 0 in String.iter (fun c -> if c <> '_' then (t.[!i] <-c; incr i)) s; t end else s } let newline = '\n' ... ... @@ -147,16 +158,6 @@ let alpha = lalpha | ualpha let digit = ['0'-'9'] let lident = lalpha (alpha | digit | '\'')* let uident = ualpha (alpha | digit | '\'')* let decimal_literal = ['0'-'9'] ['0'-'9' '_']* let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']* let oct_literal = '0' ['o' 'O'] ['0'-'7'] ['0'-'7' '_']* let bin_literal = '0' ['b' 'B'] ['0'-'1'] ['0'-'1' '_']* let int_literal = decimal_literal | hex_literal | oct_literal | bin_literal let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F'] let op_char_1 = ['=' '<' '>' '~'] ... ... @@ -188,8 +189,14 @@ rule token = parse { try Hashtbl.find keywords id with Not_found -> LIDENT id } | uident as id { UIDENT id } | int_literal as s { INTEGER s } | ['0'-'9'] ['0'-'9' '_']* as s { INTEGER (IConstDecimal (remove_underscores s)) } | '0' ['x' 'X'] (['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']* as s) { INTEGER (IConstHexa (remove_underscores s)) } | '0' ['o' 'O'] (['0'-'7'] ['0'-'7' '_']* as s) { INTEGER (IConstOctal (remove_underscores s)) } | '0' ['b' 'B'] (['0'-'1'] ['0'-'1' '_']* as s) { INTEGER (IConstBinary (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))? ... ...
 ... ... @@ -171,7 +171,7 @@ end /* Tokens */ %token LIDENT UIDENT %token INTEGER %token INTEGER %token OP1 OP2 OP3 OP4 OPPREF %token FLOAT %token STRING ... ... @@ -381,7 +381,7 @@ meta_arg: | PREDICATE qualid { PMAps \$2 } | PROP qualid { PMApr \$2 } | STRING { PMAstr \$1 } | INTEGER { PMAint \$1 } | INTEGER { PMAint (match \$1 with Term.IConstDecimal s -> int_of_string s) } ; /* Type declarations */ ... ...
 ... ... @@ -23,6 +23,7 @@ type loc = Loc.position (*s Logical expressions (for both terms and predicates) *) type integer_constant = Term.integer_constant type real_constant = Term.real_constant type constant = Term.constant ... ... @@ -150,7 +151,7 @@ type metarg = | PMAps of qualid | PMApr of qualid | PMAstr of string | PMAint of string | PMAint of int type decl = | TypeDecl of type_decl list ... ...
 ... ... @@ -1190,7 +1190,7 @@ let add_decl env lenv th = function | PMAps q -> MAls (find_psymbol q th) | PMApr q -> MApr (find_prop q th) | PMAstr s -> MAstr s | PMAint i -> MAint (int_of_string i) | PMAint i -> MAint i in let al = List.map convert al in begin try add_meta th (lookup_meta s) al ... ...
 ... ... @@ -73,7 +73,19 @@ and print_tyapp info fmt = function let rec print_term info fmt t = match t.t_node with | Tconst c -> Pretty.print_const fmt c let number_format = { Print_number.long_int_support = true; Print_number.dec_int_support = Print_number.Number_default; Print_number.hex_int_support = Print_number.Number_unsupported; Print_number.oct_int_support = Print_number.Number_unsupported; Print_number.bin_int_support = Print_number.Number_unsupported; Print_number.def_int_support = Print_number.Number_unsupported; Print_number.dec_real_support = Print_number.Number_default; Print_number.hex_real_support = Print_number.Number_default; Print_number.frac_real_support = Print_number.Number_unsupported; Print_number.def_real_support = Print_number.Number_unsupported; } in Print_number.print number_format fmt c | Tvar { vs_name = id } -> print_ident fmt id | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with ... ...
 ... ... @@ -210,10 +210,21 @@ and print_lrfmla opl opr info fmt f = match f.t_label with and print_tnode opl opr info fmt t = match t.t_node with | Tvar v -> print_vs fmt v | Tconst (ConstInt n) -> fprintf fmt "%s%%Z" n | Tconst (ConstReal c) -> Print_real.print_with_integers "(%s)%%R" "(%s * %s)%%R" "(%s / %s)%%R" fmt c | Tconst c -> let number_format = { Print_number.long_int_support = true; Print_number.dec_int_support = Print_number.Number_custom "%s%%Z"; Print_number.hex_int_support = Print_number.Number_unsupported; Print_number.oct_int_support = Print_number.Number_unsupported; Print_number.bin_int_support = Print_number.Number_unsupported; Print_number.def_int_support = Print_number.Number_unsupported; Print_number.dec_real_support = Print_number.Number_unsupported; Print_number.hex_real_support = Print_number.Number_unsupported; Print_number.frac_real_support = Print_number.Number_custom (Print_number.PrintFracReal ("(%s)%%R", "(%s * %s)%%R", "(%s / %s)%%R")); Print_number.def_real_support = Print_number.Number_unsupported; } in Print_number.print number_format fmt c | Tif (f,t1,t2) -> fprintf fmt (protect_on opr "if %a@ then %a@ else %a") (print_fmla info) f (print_term info) t1 (print_opl_term info) t2 ... ...
 ... ... @@ -133,10 +133,21 @@ let print_var_list info fmt vsl = (** expr *) let rec print_term info fmt t = match t.t_node with | Tconst (ConstInt n) -> fprintf fmt "%s" n | Tconst (ConstReal c) -> Print_real.print_with_integers "%s" "(%s * %s)" "(%s / %s)" fmt c | Tconst c -> let number_format = { Print_number.long_int_support = true; Print_number.dec_int_support = Print_number.Number_default; Print_number.hex_int_support = Print_number.Number_unsupported; Print_number.oct_int_support = Print_number.Number_unsupported; Print_number.bin_int_support = Print_number.Number_unsupported; Print_number.def_int_support = Print_number.Number_unsupported; Print_number.dec_real_support = Print_number.Number_unsupported; Print_number.hex_real_support = Print_number.Number_unsupported; Print_number.frac_real_support = Print_number.Number_custom (Print_number.PrintFracReal ("%s", "(%s * %s)", "(%s / %s)")); Print_number.def_real_support = Print_number.Number_unsupported; } in Print_number.print number_format fmt c | Tvar v -> print_var fmt v | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with | Some s -> syntax_arguments_typed s (print_term info) ... ...
 (**************************************************************************) (* *) (* Copyright (C) 2010-2011 *) (* François Bobot *) (* Jean-Christophe Filliâtre *) (* Claude Marché *) (* Guillaume Melquiond *) (* Andrei Paskevich *) (* *) (* This software is free software; you can redistribute it and/or *) (* modify it under the terms of the GNU Library General Public *) (* License version 2.1, with the special exception on linking *) (* described in file LICENSE. *) (* *) (* This software is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* *) (**************************************************************************) open Format open Big_int open Term let any_to_dec radix s = let n = String.length s in let rec compute acc i = if i = n then acc else begin let v = match s.[i] with | '0'..'9' as c -> Char.code c - Char.code '0' | 'A'..'Z' as c -> 10 + Char.code c - Char.code 'A' | 'a'..'z' as c -> 10 + Char.code c - Char.code 'a' | _ -> assert false in assert (v < radix); compute (add_int_big_int v (mult_int_big_int radix acc)) (i + 1) end in string_of_big_int (compute zero_big_int 0) let power2 n = string_of_big_int (power_int_positive_int 2 n) type integer_format = (string -> unit, Format.formatter, unit) format type real_format = (string -> string -> string -> unit, Format.formatter, unit) format type part_real_format = (string -> string -> unit, Format.formatter, unit) format type dec_real_format = | PrintDecReal of part_real_format * real_format type frac_real_format = | PrintFracReal of integer_format * part_real_format * part_real_format type 'a number_support_kind = | Number_unsupported | Number_default | Number_custom of 'a type integer_support_kind = integer_format number_support_kind type number_support = { long_int_support : bool; dec_int_support : integer_support_kind; hex_int_support : integer_support_kind; oct_int_support : integer_support_kind; bin_int_support : integer_support_kind; def_int_support : integer_support_kind; dec_real_support : dec_real_format number_support_kind; hex_real_support : real_format number_support_kind; frac_real_support : frac_real_format number_support_kind; def_real_support : integer_support_kind; } let check_support support default do_it try_next v = match support with | Number_unsupported -> try_next v | Number_default -> do_it (match default with Some d -> d | None -> assert false) v | Number_custom f -> do_it f v let force_support support do_it v = match support with | Number_unsupported -> assert false | Number_default -> assert false | Number_custom f -> do_it f v let simplify_max_int = big_int_of_string "2147483646" let remove_minus e = if e. = '-' then (let e' = String.copy e in e'. <- 'm'; e') else e let print_dec_int support fmt i = let fallback i = force_support support.def_int_support (fprintf fmt) i in if not support.long_int_support && (compare_big_int (big_int_of_string i) simplify_max_int > 0) then fallback i else check_support support.dec_int_support (Some "%s") (fprintf fmt) fallback i let print_hex_int support fmt = check_support support.hex_int_support (Some "0x%s") (fun s i -> assert support.long_int_support; fprintf fmt s i) (fun i -> print_dec_int support fmt (any_to_dec 16 i)) let print_oct_int support fmt = check_support support.oct_int_support (Some "0o%s") (fun s i -> assert support.long_int_support; fprintf fmt s i) (fun i -> print_dec_int support fmt (any_to_dec 8 i)) let print_bin_int support fmt = check_support support.bin_int_support (Some "0b%s") (fun s i -> assert support.long_int_support; fprintf fmt s i) (fun i -> print_dec_int support fmt (any_to_dec 2 i)) let print_dec_real support fmt = check_support support.dec_real_support (Some (PrintDecReal ("%s.%s", "%s.%se%s"))) (fun (PrintDecReal (noexp,full)) i f e -> match e with | None -> fprintf fmt noexp i f | Some e -> fprintf fmt full i f e) (check_support support.frac_real_support None (fun (PrintFracReal (exp_zero, exp_pos, exp_neg)) i f e -> let f = if f = "0" then "" else f in let e = (match e with None -> 0 | Some e -> int_of_string e) - String.length f in if e = 0 then fprintf fmt exp_zero (i ^ f) else if e > 0 then fprintf fmt exp_pos (i ^ f) ("1" ^ String.make e '0') else fprintf fmt exp_neg (i ^ f) ("1" ^ String.make (-e) '0')) (force_support support.def_real_support (fun def i f e -> fprintf fmt def (sprintf "%s_%s_e%s" i f (match e with None -> "0" | Some e -> remove_minus e))) )) let print_hex_real support fmt = check_support support.hex_real_support (Some "0x%s.%sp%s") (fun s i f e -> fprintf fmt s i f e) (* TODO: add support for decay to decimal floats *) (check_support support.frac_real_support None (fun (PrintFracReal (exp_zero, exp_pos, exp_neg)) i f e -> let f = if f = "0" then "" else f in let dec = any_to_dec 16 (i ^ f) in let e = int_of_string e - 4 * String.length f in if e = 0 then fprintf fmt exp_zero dec else if e > 0 then fprintf fmt exp_pos dec (power2 e) else fprintf fmt exp_neg dec (power2 (-e))) (force_support support.def_real_support (fun def i f e -> fprintf fmt def (sprintf "0x%s_%s_p%s" i f (remove_minus e))) )) let print support fmt = function | ConstInt (IConstDecimal i) -> print_dec_int support fmt i | ConstInt (IConstHexa i) -> print_hex_int support fmt i | ConstInt (IConstOctal i) -> print_oct_int support fmt i | ConstInt (IConstBinary i) -> print_bin_int support fmt i | ConstReal (RConstDecimal (i, f, e)) -> print_dec_real support fmt i f e | ConstReal (RConstHexa (i, f, e)) -> print_hex_real support fmt i f e (* Local Variables: compile-command: "unset LANG; make -C ../.. byte" End: *)
 ... ... @@ -4,6 +4,7 @@ (* François Bobot *) (* Jean-Christophe Filliâtre *) (* Claude Marché *) (* Guillaume Melquiond *) (* Andrei Paskevich *) (* *) (* This software is free software; you can redistribute it and/or *) ... ... @@ -19,10 +20,32 @@ open Format val print : formatter -> Term.real_constant -> unit type integer_format = (string -> unit, Format.formatter, unit) format type real_format = (string -> string -> string -> unit, Format.formatter, unit) format type part_real_format = (string -> string -> unit, Format.formatter, unit) format type dec_real_format = | PrintDecReal of part_real_format * real_format type frac_real_format = | PrintFracReal of integer_format * part_real_format * part_real_format val print_with_integers : (string -> 'a, Format.formatter, unit) format -> (string -> string -> 'a, Format.formatter, unit) format -> (string -> string -> 'a, Format.formatter, unit) format -> Format.formatter -> Term.real_constant -> 'a type 'a number_support_kind = | Number_unsupported | Number_default | Number_custom of 'a type integer_support_kind = integer_format number_support_kind type number_support = { long_int_support : bool; dec_int_support : integer_support_kind; hex_int_support : integer_support_kind; oct_int_support : integer_support_kind; bin_int_support : integer_support_kind; def_int_support : integer_support_kind; dec_real_support : dec_real_format number_support_kind; hex_real_support : real_format number_support_kind; frac_real_support : frac_real_format number_support_kind; def_real_support : integer_support_kind; } val print : number_support -> formatter -> Term.constant -> unit
 (**************************************************************************) (* *) (* Copyright (C) 2010-2011 *) (* François Bobot *) (* Jean-Christophe Filliâtre *) (* Claude Marché *) (* Andrei Paskevich *) (* *) (* This software is free software; you can redistribute it and/or *) (* modify it under the terms of the GNU Library General Public *) (* License version 2.1, with the special exception on linking *) (* described in file LICENSE. *) (* *) (* This software is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* *) (**************************************************************************) open Format open Big_int open Term let print_decimal_no_exponent fmt ~prefix_div = function | "","0",_ | "0","",_ | "0","0",_ -> fprintf fmt "0.0" | "",f, None -> fprintf fmt "0.%s" f | i,"", None -> fprintf fmt "%s.0" i | i,f, None -> fprintf fmt "%s.%s" i f | i,f, Some e -> let e = (int_of_string e) - String.length f in if e = 0 then fprintf fmt "%s%s" i f else let op,s = if e > 0 then "*",(String.make e '0') else "/",(String.make (-e) '0') in if prefix_div then fprintf fmt "(%s %s%s.0 1%s.0)" op i f s else fprintf fmt "(%s%s %s.0 1%s.0)" i f op s let num0 = Num.Int 0 let num10 = Num.Int 10 let num16 = Num.Int 16 let decnumber s = let r = ref num0 in for i=0 to String.length s - 1 do r := Num.add_num (Num.mult_num num10 !r) (Num.num_of_int (Char.code s.[i] - Char.code '0')) done; !r let hexnumber s = let r = ref num0 in for i=0 to String.length s - 1 do let c = s.[i] in let v = match c with | '0'..'9' -> Char.code c - Char.code '0' | 'a'..'f' -> Char.code c - Char.code 'a' + 10 | 'A'..'F' -> Char.code c - Char.code 'A' + 10 | _ -> assert false in r := Num.add_num (Num.mult_num num16 !r) (Num.num_of_int v) done; !r let print_hexa fmt i f e = let mant = hexnumber (i^f) in let v = if e="" then mant else if String.get e 0 = '-' then Num.div_num mant (Num.power_num (Num.Int 2) (decnumber (String.sub e 1 (String.length e - 1)))) else Num.mult_num mant (Num.power_num (Num.Int 2) (decnumber e)) in