Commit e2c99a74 authored by Guillaume Melquiond's avatar Guillaume Melquiond Committed by Raphael Rieu-Helft

Add support for fixed-point arithmetic to the Gappa driver.

As many computations as possible are now performed in Why3, so that the
parameters of the "fixed" rounding operator are literals once sent to
Gappa.
parent e2134bf9
......@@ -23,6 +23,7 @@ transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_unknown_lsymbols"
transformation "simplify_trivial_quantification"
transformation "simplify_computations"
transformation "introduce_premises"
transformation "instantiate_predicate"
transformation "abstract_unknown_lsymbols"
......@@ -43,7 +44,7 @@ theory int.Int
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function ( * ) "(%1 * %2)"
syntax function (*) "(%1 * %2)"
syntax function (-_) "(-%1)"
syntax predicate (<=) "dummy"
......@@ -56,6 +57,7 @@ theory int.Int
meta "gappa arith" predicate (<), "not ", ">=", "<="
meta "gappa arith" predicate (>), "not ", "<=", ">="
meta "inline:no" function (-)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
......@@ -87,7 +89,7 @@ theory real.Real
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function ( * ) "(%1 * %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function (-_) "(-%1)"
syntax function inv "(1.0 / %1)"
......@@ -102,6 +104,7 @@ theory real.Real
meta "gappa arith" predicate (<), "not ", ">=", "<="
meta "gappa arith" predicate (>), "not ", "<=", ">="
meta "inline:no" function (-)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
......@@ -215,3 +218,9 @@ theory floating_point.DoubleMultiRounding
meta "instantiate:auto" prop Bounded_value
end
theory mach.fxp.Fxp
syntax function trunc_at "fixed<%2,dn>(%1)"
end
......@@ -28,6 +28,14 @@ let syntactic_transform transf =
| _ -> assert false) Sls.empty metas in
transf (fun ls -> Sls.mem ls symbols))
let syntactic_transform_env transf env =
Trans.on_meta meta_syntax_logic (fun metas ->
let symbols = List.fold_left (fun acc meta_arg ->
match meta_arg with
| [MAls ls; MAstr _; MAint _] -> Sls.add ls acc
| _ -> assert false) Sls.empty metas in
transf (fun ls -> Sls.mem ls symbols) env)
let () =
Trans.register_transform "abstract_unknown_lsymbols"
(syntactic_transform Abstraction.abstraction)
......@@ -48,7 +56,11 @@ let () =
])))
~desc:"Same@ as@ simplify_trivial_quantification_in_goal,@ but@ instead@ \
of@ substituting@ quantified@ variables,@ substitute@ applications@ \
of@ non-built-in@ symbols.@ Used@ by@ the@ Gappa@ pretty-printer."
of@ non-built-in@ symbols.@ Used@ by@ the@ Gappa@ pretty-printer.";
Trans.register_env_transform "simplify_computations"
(syntactic_transform_env (fun check_ls -> Compute.simplify (fun ls -> check_ls ls)))
~desc:"Perform computations and simplify non-builtin symbols.@ \
Used by the Gappa pretty-printer.";
(* patterns (TODO: add a parser and generalize it out of Gappa) *)
......
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