diff --git a/drivers/alt_ergo_common.drv b/drivers/alt_ergo_common.drv index f1d01d744b2e405f351b795b2369446df1b14635..67f5fba027a083b932d3365e2530b12325787106 100644 --- a/drivers/alt_ergo_common.drv +++ b/drivers/alt_ergo_common.drv @@ -174,9 +174,6 @@ theory HighOrd end theory map.Map - syntax function get "(%1[%2])" - syntax function set "(%1[%2 <- %3])" - - remove prop Select_eq - remove prop Select_neq + syntax function get "(%1[%2])" + syntax function set "(%1[%2 <- %3])" end diff --git a/drivers/pvs-common.gen b/drivers/pvs-common.gen index edfed4244d764a999bc17cdf57497ca8bffb78f7..355c7b51749374cc2a91895af7fcb8c3ce7282e1 100644 --- a/drivers/pvs-common.gen +++ b/drivers/pvs-common.gen @@ -32,16 +32,11 @@ theory HighOrd end theory map.Map - - syntax function get "%1(%2)" + syntax function get "%1(%2)" syntax function ([]) "%1(%2)" syntax function set "(%1 WITH [(%2) |-> %3])" syntax function ([<-]) "(%1 WITH [(%2) |-> %3])" - - remove prop Select_eq - remove prop Select_neq - end theory Bool diff --git a/drivers/smt-libv2.drv b/drivers/smt-libv2.drv index 7902ab946a4e8ce4ff34b1908ee3b916c1985dff..2bb812d1e2f4298d54923c5f3ab14c1505302861 100644 --- a/drivers/smt-libv2.drv +++ b/drivers/smt-libv2.drv @@ -161,11 +161,6 @@ theory map.Map 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 theory map.Const diff --git a/drivers/why3_smt.drv b/drivers/why3_smt.drv index 0d8ae9054c026a1b023e92fe587a9f3564b2ba38..210942ea5f752a3576d7301b9368a24900f12caa 100644 --- a/drivers/why3_smt.drv +++ b/drivers/why3_smt.drv @@ -51,11 +51,6 @@ theory map.Map 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" diff --git a/theories/map.why b/theories/map.why index 27ced66c73409be03c513dd32a0b89ecd95c4c67..8574d0ba4f41509f6f780b31708dd45b771dde39 100644 --- a/theories/map.why +++ b/theories/map.why @@ -8,34 +8,15 @@ theory Map type map 'a 'b = 'a -> 'b - (* FIXME: add meta "material_type_arg" type func, 1 for (->) *) - (* FIXME: remove Select_eq, Select_neq, and Const ? *) - (* FIXME: we cannot remove the defining axiom for set in a driver. *) - -(* - (** if ['b] is an infinite type, then [map 'a 'b] is infinite *) - meta "material_type_arg" type func, 1 -*) - function get (f: map 'a 'b) (x: 'a) : 'b = f x function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = fun y -> if y = x then v else f y (** syntactic sugar *) - function ([]) (f: map 'a 'b) (x: 'a) : 'b = get f x + function ([]) (f: map 'a 'b) (x: 'a) : 'b = f x function ([<-]) (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = set f x v - lemma Select_eq : - forall m : map 'a 'b. forall a1 a2 : 'a. - forall b : 'b [m[a1 <- b][a2]]. - a1 = a2 -> m[a1 <- b][a2] = b - - lemma Select_neq : - forall m : map 'a 'b. forall a1 a2 : 'a. - forall b : 'b [m[a1 <- b][a2]]. - a1 <> a2 -> m[a1 <- b][a2] = m[a2] - end theory Const