Commit d926138c authored by Andrei Paskevich's avatar Andrei Paskevich

fix parsing of hex reals

parent 450e2e61
......@@ -291,8 +291,8 @@ access the internal identifier for addition: it must be retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why} (see
Chap~\ref{chap:library}).
\begin{ocamlcode}
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 two : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "2"))
let four : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "4"))
let int_theory : Theory.theory =
Env.find_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol =
......@@ -325,7 +325,7 @@ To illustrate how to build quantified formulas, let us consider
the formula $\forall x:int. x*x \geq 0$. The first step is to
obtain the symbols from \texttt{Int}.
\begin{ocamlcode}
let zero : Term.term = Term.t_const (Term.ConstInt "0")
let zero : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "0"))
let mult_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_symbol : Term.lsymbol =
......
......@@ -127,8 +127,8 @@ An arithmetic goal: 2+2 = 4
*)
let two : Term.term = Term.t_const (Term.ConstInt (Term.int_const_decimal "2"))
let four : Term.term = Term.t_const (Term.ConstInt (Term.int_const_decimal "4"))
let two : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "2"))
let four : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "4"))
let int_theory : Theory.theory =
Env.find_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol =
......@@ -156,7 +156,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 (Term.int_const_decimal "0"))
let zero : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "0"))
let mult_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_symbol : Term.lsymbol =
......@@ -201,9 +201,9 @@ let mul_int : Term.lsymbol =
let unit_type = Ty.ty_tuple []
let d =
let d =
let args =
[Mlw_ty.create_pvsymbol
[Mlw_ty.create_pvsymbol
(Ident.id_fresh "_dummy") (Mlw_ty.vty_value Mlw_ty.ity_unit)]
in
let result = Term.create_vsymbol (Ident.id_fresh "result") unit_type in
......@@ -217,13 +217,13 @@ let d =
}
in
let body =
let c6 = Term.t_const (Term.ConstInt (Term.int_const_decimal "6")) in
let c7 = Term.t_const (Term.ConstInt (Term.int_const_decimal "7")) in
let c42 = Term.t_const (Term.ConstInt (Term.int_const_decimal "42")) in
let p =
let c6 = Term.t_const (Number.ConstInt (Number.int_const_dec "6")) in
let c7 = Term.t_const (Number.ConstInt (Number.int_const_dec "7")) in
let c42 = Term.t_const (Number.ConstInt (Number.int_const_dec "42")) in
let p =
Term.t_equ (Term.t_app_infer mul_int [c6;c7]) c42
in
Mlw_expr.e_assert Mlw_expr.Aassert p
Mlw_expr.e_assert Mlw_expr.Aassert p
in
let lambda = {
Mlw_expr.l_args = args;
......
......@@ -195,10 +195,10 @@ rule token = parse
| (digit+ as i) '.' (digit* as f) (['e' 'E'] (['-' '+']? digit+ as e))?
| (digit* as i) '.' (digit+ as f) (['e' 'E'] (['-' '+']? digit+ as e))?
{ FLOAT (Number.real_const_dec i f (Opt.map remove_leading_plus e)) }
| '0' ['x' 'X'] (digit+ as i) ("" as f) ['p' 'P'] (['-' '+']? digit+ as e)
| '0' ['x' 'X'] (digit+ as i) '.' (digit* as f)
| '0' ['x' 'X'] (hexadigit+ as i) ("" as f) ['p' 'P'] (['-' '+']? digit+ as e)
| '0' ['x' 'X'] (hexadigit+ as i) '.' (hexadigit* as f)
(['p' 'P'] (['-' '+']? digit+ as e))?
| '0' ['x' 'X'] (digit* as i) '.' (digit+ as f)
| '0' ['x' 'X'] (hexadigit* as i) '.' (hexadigit+ as f)
(['p' 'P'] (['-' '+']? digit+ as e))?
{ FLOAT (Number.real_const_hex i f (Opt.map remove_leading_plus e)) }
| "(*)"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment