Commit 6def0492 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'feature/ignore_map_polymorphism'

parents 85edfb97 5bb881e8
......@@ -62,4 +62,18 @@ theory int.EuclideanDivision
end
*)
theory map.Map
meta "encoding:ignore_polymorphism_ts" type map
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
meta "encoding:ignore_polymorphism_ls" function ([<-])
meta "encoding:ignore_polymorphism_pr" prop Select_eq
meta "encoding:ignore_polymorphism_pr" prop Select_neq
remove prop Select_eq
remove prop Select_neq
end
import "cvc4_bv.gen"
......@@ -3,17 +3,8 @@
printer "why3"
filename "%f-%t-%g.why"
(* transformation "detect_polymorphism" *)
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax predicate (=) "(%1 = %2)"
(* meta "encoding:ignore_polymorphism_ls" predicate (=) *)
end
(*
theory list.List
meta "encoding:ignore_polymorphism_ts" type list
end
*)
......@@ -4,20 +4,30 @@ printer "why3"
filename "%f-%t-%g.why"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
transformation "discriminate"
transformation "encoding_smt"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax predicate (=) "(%1 = %2)"
meta "encoding:ignore_polymorphism_ls" predicate (=)
meta "encoding : kept" type int
meta "encoding : kept" type real
......@@ -26,10 +36,17 @@ end
theory map.Map
meta "encoding : lskept" function get
meta "encoding : lskept" function set
end
theory map.Const
meta "encoding : lskept" function const
meta "encoding:ignore_polymorphism_ts" type map
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
meta "encoding:ignore_polymorphism_ls" function ([<-])
meta "encoding:ignore_polymorphism_pr" prop Select_eq
meta "encoding:ignore_polymorphism_pr" prop Select_neq
remove prop Select_eq
remove prop Select_neq
end
import "discrimination.gen"
......@@ -94,3 +94,30 @@ goal g: forall x:'a. x = x
(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolyProp -G g *)
end
theory Map
use import int.Int
use import map.Map
goal g: forall m:map int int.
let m' = m[0<-42][1<-42] in
m'[0] + m'[1] >= 0
(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -D why3_smt -T Map -G g *)
end
theory TestTuple
use import int.Int
use import bool.Bool
type t = (int,bool)
goal g: forall x:t. match x with (a,b) -> a >= 0 /\ b end
end
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