HighOrd is new Map

0. define Map.map 'a 'b as an alias 'a -> 'b
1. define Set.set as an alias for 'a -> bool
2. rename HighOrd.func to (->)
3. remove HighOrd.pred
4. update drivers

drivers/alt_ergo_common.drv

@@ -168,9 +168,14 @@ theory algebra.AC
   remove prop Assoc
 end
 
-theory map.Map
-  syntax type  map "(%1,%2) farray"
+theory HighOrd
+  syntax type     (->) "(%1,%2) farray"
+  meta "material_type_arg" type (->), 1
+
+  syntax function (@)  "(%1[%2])"
+end
 
+theory map.Map
   syntax function get "(%1[%2])"
   syntax function set "(%1[%2 <- %3])"
 

drivers/cvc3_bare.drv

@@ -147,19 +147,21 @@ theory bool.Bool
    syntax function notb  "(~ %1)"
 end
 
+theory HighOrd
+  syntax type     (->) "(ARRAY %1 OF %2)"
+  meta "material_type_arg" type (->), 1
+
+  syntax function (@)  "(%1[%2])"
+  meta "encoding : lskept" function (@)
+end
 
 theory map.Map
-  syntax type map "(ARRAY %1 OF %2)"
   meta "encoding : lskept" function get
   meta "encoding : lskept" function set
 
   syntax function get "(%1[%2])"
   syntax function set "(%1 WITH [%2] := %3)"
-end
 
-(*
-Local Variables:
-mode: why
-compile-command: "unset LANG; make -C .. bench"
-End:
-*)
+  remove prop Select_eq
+  remove prop Select_neq
+end

drivers/mathsat.drv

@@ -166,20 +166,20 @@ theory real.Truncate
 end
 *)
 
+theory HighOrd
+  syntax type     (->) "(Array %1 %2)"
+  meta "material_type_arg" type (->), 1
+
+  syntax function (@)  "(select %1 %2)"
+  meta "encoding : lskept" function (@)
+end
+
 theory map.Map
-  syntax type map "(Array %1 %2)"
   meta "encoding : lskept" function get
   meta "encoding : lskept" function set
   meta "encoding : lskept" function const
 
-  syntax function get   "(select %1 %2)"
-  syntax function set   "(store %1 %2 %3)"
+  syntax function get "(select %1 %2)"
+  syntax function set "(store %1 %2 %3)"
 (*  syntax function const "(const[%t0] %1)" *)
 end
-
-(*
-Local Variables:
-mode: why
-compile-command: "unset LANG; make -C .. bench"
-End:
-*)

drivers/smt-libv2.drv

@@ -140,8 +140,15 @@ theory real.Truncate
 end
 *)
 
+theory HighOrd
+  syntax type     (->) "(Array %1 %2)"
+  meta "material_type_arg" type (->), 1
+
+  syntax function (@)  "(select %1 %2)"
+  meta "encoding : lskept" function (@)
+end
+
 theory map.Map
-  syntax type map "(Array %1 %2)"
   meta "encoding : lskept" function get
   meta "encoding : lskept" function set
   meta "encoding : lskept" function const

drivers/yices.drv

@@ -135,9 +135,15 @@ theory bool.Bool
    syntax function notb  "(not %1)"
 end
 
+theory HighOrd
+  syntax type (->) "(-> %1 %2)"
+  meta "material_type_arg" type (->), 1
+
+  syntax function (@)  "(%1 %2)"
+  meta "encoding : lskept" function (@)
+end
 
 theory map.Map
-  syntax type map "(-> %1 %2)"
   meta "encoding : lskept" function get
   meta "encoding : lskept" function set
 
@@ -146,14 +152,5 @@ theory map.Map
   syntax function set    "(update %1 (%2) %3)"
   syntax function ([<-]) "(update %1 (%2) %3)"
 
-
   meta "encoding : lskept" function const
-
 end
-
-(*
-Local Variables:
-mode: why
-compile-command: "unset LANG; make -C .. bench"
-End:
-*)

src/core/decl.ml

@@ -717,7 +717,6 @@ let check_foundness kn d =
 let rec ts_extract_pos kn sts ts =
   assert (ts.ts_def = None);
   if ts_equal ts ts_func then [false;true] else
-  if ts_equal ts ts_pred then [false] else
   if Sts.mem ts sts then List.map Util.ttrue ts.ts_args else
   match find_constructors kn ts with
     | [] ->

src/core/theory.ml

@@ -815,7 +815,6 @@ let highord_theory =
   let uc = empty_theory (id_fresh "HighOrd") ["why3";"HighOrd"] in
   let uc = use_export uc bool_theory in
   let uc = add_ty_decl uc ts_func in
-  let uc = add_ty_decl uc ts_pred in
   let uc = add_param_decl uc fs_func_app in
   close_theory uc
 

src/core/ty.ml

@@ -221,16 +221,11 @@ let ty_bool = ty_app ts_bool []
 let ts_func =
   let tv_a = create_tvsymbol (id_fresh "a") in
   let tv_b = create_tvsymbol (id_fresh "b") in
-  create_tysymbol (id_fresh "func") [tv_a;tv_b] None
+  create_tysymbol (id_fresh "infix ->") [tv_a;tv_b] None
 
 let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b]
 
-let ts_pred =
-  let tv_a = create_tvsymbol (id_fresh "a") in
-  let def = Some (ty_func (ty_var tv_a) ty_bool) in
-  create_tysymbol (id_fresh "pred") [tv_a] def
-
-let ty_pred ty_a = ty_app ts_pred [ty_a]
+let ty_pred ty_a = ty_app ts_func [ty_a;ty_bool]
 
 let ts_tuple_ids = Hid.create 17
 

src/core/ty.mli

@@ -129,7 +129,6 @@ val ty_real : ty
 val ty_bool : ty
 
 val ts_func : tysymbol
-val ts_pred : tysymbol
 
 val ty_func : ty -> ty -> ty
 val ty_pred : ty -> ty (* ty_pred 'a == ty_func 'a bool *)

src/mlw/ity.ml

@@ -603,14 +603,13 @@ let its_int  = its_of_ts ts_int  true
 let its_real = its_of_ts ts_real true
 let its_bool = its_of_ts ts_bool true
 let its_func = its_of_ts ts_func true
-let its_pred = its_of_ts ts_pred true
 
 let ity_int  = ity_pur its_int  []
 let ity_real = ity_pur its_real []
 let ity_bool = ity_pur its_bool []
 
 let ity_func a b = ity_pur its_func [a;b]
-let ity_pred a   = ity_pur its_pred [a]
+let ity_pred a   = ity_pur its_func [a;ity_bool]
 
 let its_tuple = Hint.memo 17 (fun n -> its_of_ts (ts_tuple n) false)
 

src/mlw/ity.mli

@@ -211,7 +211,6 @@ val its_real : itysymbol
 val its_bool : itysymbol
 val its_unit : itysymbol
 val its_func : itysymbol
-val its_pred : itysymbol
 
 val ity_int  : ity
 val ity_real : ity

src/mlw/pdecl.ml

@@ -460,11 +460,9 @@ let pd_int, pd_real, pd_equ = match builtin_theory.th_decls with
       mk_decl PDpure [de]
   | _ -> assert false
 
-let pd_func, pd_pred, pd_func_app = match highord_theory.th_decls with
-  | [{td_node = Use _bo};
-     {td_node = Decl df}; {td_node = Decl dp}; {td_node = Decl da}] ->
+let pd_func, pd_func_app = match highord_theory.th_decls with
+  | [{td_node = Use _bo}; {td_node = Decl df}; {td_node = Decl da}] ->
       mk_decl (PDtype [mk_itd its_func [] [] []]) [df],
-      mk_decl (PDtype [mk_itd its_pred [] [] []]) [dp],
       mk_decl (PDlet ld_func_app) [da]
   | _ -> assert false
 

src/mlw/pdecl.mli

@@ -71,7 +71,6 @@ val pd_equ : pdecl
 val pd_bool : pdecl
 val pd_tuple : int -> pdecl
 val pd_func : pdecl
-val pd_pred : pdecl
 val pd_func_app : pdecl
 
 (** {2 Known identifiers} *)

src/mlw/pmodule.ml

@@ -302,7 +302,6 @@ let highord_module =
   let uc = empty_module None (id_fresh "HighOrd") ["why3";"HighOrd"] in
   let uc = use_export uc bool_module in
   let uc = add_pdecl uc pd_func in
-  let uc = add_pdecl uc pd_pred in
   let uc = add_pdecl uc pd_func_app in
   let m = close_module uc in
   { m with mod_theory = highord_theory }

src/transform/close_epsilon.ml

@@ -15,8 +15,7 @@ open Term
 
 let is_func_ty t =
   match t.Ty.ty_node with
-  | Ty.Tyapp (s,_) ->
-      Ty.ts_equal s Ty.ts_func || Ty.ts_equal s Ty.ts_pred
+  | Ty.Tyapp (s,_) -> Ty.ts_equal s Ty.ts_func
   | _ -> false
 
 type lambda_match =

theories/int.why

@@ -216,9 +216,11 @@ theory Exponentiation
   type t
   constant one : t
   function (*) t t : t
+
   clone export algebra.CommutativeMonoid
     with type t = t, constant unit = one, function op = (*)
 
+  (* TODO: implement with let rec once let cloning is done *)
   function power t int : t
 
   axiom Power_0 : forall x: t. power x 0 = one
@@ -233,7 +235,7 @@ theory Exponentiation
     power x (n+m) = power x n * power x m
 
   lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m ->
-    power x (Int.( * ) n m) = power (power x n) m
+    power x (Int.(*) n m) = power (power x n) m
 
   lemma Power_mult2 : forall x y: t, n: int. 0 <= n ->
     power (x * y) n = power x n * power y n
@@ -257,8 +259,13 @@ theory Power
 
   use import Int
 
-  clone export Exponentiation with type t = int, constant one = one,
-    function (*) = (*), goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r
+  (* TODO: remove once power is implemented in Exponentiation *)
+  val function power int int : int
+
+  clone export Exponentiation with
+    type t = int, constant one = one,
+    function (*) = (*), function power = power,
+    goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r
 
   lemma Power_non_neg:
      forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
@@ -274,20 +281,12 @@ theory NumOf
 
   use import Int
 
-  function numof (p: int -> bool) (a b: int) : int
   (** number of [n] such that [a <= n < b] and [p n] *)
-
-  axiom Numof_empty :
-    forall p: int -> bool, a b: int.
-    b <= a -> numof p a b = 0
-
-  axiom Numof_right_no_add :
-    forall p : int -> bool, a b : int.
-    a < b -> not (p (b-1)) -> numof p a b = numof p a (b-1)
-
-  axiom Numof_right_add :
-    forall p : int -> bool, a b : int.
-    a < b -> p (b-1) -> numof p a b = 1 + numof p a (b-1)
+  let rec function numof (p: int -> bool) (a b: int) : int
+    variant { b - a }
+  = if b <= a then 0 else
+    if p (b - 1) then 1 + numof p a (b - 1) else
+                          numof p a (b - 1)
 
   lemma Numof_bounds :
     forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a
@@ -351,39 +350,38 @@ theory Sum
 
   use import Int
 
-  function sum (a b: int) (f: int -> int) : int
-  (** sum of [f n] for [a <= n <= b] *)
-
-  axiom sum_def1:
-    forall f: int -> int, a b: int.
-    b < a -> sum a b f = 0
-
-  axiom sum_def2:
-    forall f: int -> int, a b: int.
-    a <= b -> sum a b f = sum a (b - 1) f + f b
+  (** sum of [f n] for [a <= n < b] *)
+  let rec function sum (f: int -> int) (a b: int) : int
+    variant { b - a }
+  = if b <= a then 0 else sum f a (b - 1) + f (b - 1)
 
   lemma sum_left:
     forall f: int -> int, a b: int.
-    a <= b -> sum a b f = f a + sum (a + 1) b f
+    a < b -> sum f a b = f a + sum f (a + 1) b
 
   lemma sum_ext:
     forall f g: int -> int, a b: int.
-    (forall i. a <= i <= b -> f i = g i) ->
-    sum a b f = sum a b g
+    (forall i. a <= i < b -> f i = g i) ->
+    sum f a b = sum g a b
 
   lemma sum_le:
     forall f g: int -> int, a b: int.
-    (forall i. a <= i <= b -> f i <= g i) ->
-    sum a b f <= sum a b g
+    (forall i. a <= i < b -> f i <= g i) ->
+    sum f a b <= sum g a b
+
+  lemma sum_zero:
+    forall f: int -> int, a b: int.
+    (forall i. a <= i < b -> f i = 0) ->
+    sum f a b = 0
 
   lemma sum_nonneg:
     forall f: int -> int, a b: int.
-    (forall i. a <= i <= b -> 0 <= f i) ->
-    0 <= sum a b f
+    (forall i. a <= i < b -> 0 <= f i) ->
+    0 <= sum f a b
 
   lemma sum_decomp:
     forall f: int -> int, a b c: int. a <= b <= c ->
-    sum a c f = sum a b f + sum (b+1) c f
+    sum f a c = sum f a b + sum f b c
 
 end
 

theories/map.why

@@ -6,31 +6,39 @@
 
 theory Map
 
-  type map 'a 'b
+  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 map, 1
+  meta "material_type_arg" type func, 1
+*)
 
-  function get (map 'a 'b) 'a : 'b
-  function set (map 'a 'b) 'a 'b : map 'a 'b
+  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 ([])   (a : map 'a 'b) (i : 'a) : 'b = get a i
-  function ([<-]) (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = set a i v
+  function ([])   (f: map 'a 'b) (x: 'a) : 'b = get f x
+  function ([<-]) (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = set f x v
 
-  axiom Select_eq :
+  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
+    a1 = a2 -> m[a1 <- b][a2] = b
 
-  axiom Select_neq :
+  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]
 
-  function const 'b : map 'a 'b
+  function const (v: 'b) : map 'a 'b = fun _ -> v
 
-  axiom Const : forall b:'b, a:'a. (const b)[a] = b
+  lemma Const : forall v: 'b, a: 'a. (const v)[a] = v
 
 end
 

theories/set.why

@@ -33,14 +33,14 @@ theory SetGen
 
   predicate is_empty (s: set 'a) = forall x: 'a. not (mem x s)
 
-  axiom empty_def1: is_empty (empty : set 'a)
+  axiom empty_def: is_empty (empty : set 'a)
 
   lemma mem_empty: forall x:'a. mem x empty <-> false
 
   (** addition *)
   function add 'a (set 'a) : set 'a
 
-  axiom add_def1:
+  axiom add_def:
     forall x y: 'a. forall s: set 'a.
     mem x (add y s) <-> x = y \/ mem x s
 
@@ -49,7 +49,7 @@ theory SetGen
   (** removal *)
   function remove 'a (set 'a) : set 'a
 
-  axiom remove_def1:
+  axiom remove_def:
     forall x y : 'a, s : set 'a.
     mem x (remove y s) <-> x <> y /\ mem x s
 
@@ -65,21 +65,21 @@ theory SetGen
   (** union *)
   function union (set 'a) (set 'a) : set 'a
 
-  axiom union_def1:
+  axiom union_def:
     forall s1 s2: set 'a, x: 'a.
     mem x (union s1 s2) <-> mem x s1 \/ mem x s2
 
   (** intersection *)
   function inter (set 'a) (set 'a) : set 'a
 
-  axiom inter_def1:
+  axiom inter_def:
     forall s1 s2: set 'a, x: 'a.
     mem x (inter s1 s2) <-> mem x s1 /\ mem x s2
 
   (** difference *)
   function diff (set 'a) (set 'a) : set 'a
 
-  axiom diff_def1:
+  axiom diff_def:
     forall s1 s2: set 'a, x: 'a.
     mem x (diff s1 s2) <-> mem x s1 /\ not (mem x s2)
 
@@ -98,12 +98,44 @@ end
 
 theory Set
 
-  clone export SetGen
+  use import map.Map
+
+  type set 'a = map 'a bool
+
+  predicate mem (x:'a) (s:set 'a) = s[x]
+
+  constant empty : set 'a = const false
+
+  constant all : set 'a = const true
 
-  (** the set of all x of type 'a *)
-  constant all: set 'a
+  function add (x:'a) (s:set 'a) : set 'a = s[x <- true]
 
-  axiom all_def: forall x: 'a. mem x all
+  function remove (x:'a) (s:set 'a) : set 'a =  s[x <- false]
+
+  function union (s1 s2: set 'a) : set 'a =
+    fun x -> s1[x] \/ s2[x]
+
+  function inter (s1 s2: set 'a) : set 'a =
+    fun x -> s1[x] /\ s2[x]
+
+  function diff (s1 s2: set 'a) : set 'a =
+    fun x -> s1[x] /\ not s2[x]
+
+  function complement (s: set 'a) : set 'a =
+    fun x -> not s[x]
+
+(* dubious axiom: extensionality should be postulated on maps instead
+  axiom Equal_is_eq : forall s1 s2 : set 'a. equal s1 s2 -> s1 = s2
+*)
+
+  clone export SetGen with type set = set,
+    predicate mem = mem, axiom extensionality,
+    constant empty = empty, lemma empty_def,
+    function add = add, lemma add_def,
+    function remove = remove, lemma remove_def,
+    function union = union, lemma union_def,
+    function inter = inter, lemma inter_def,
+    function diff = diff, lemma diff_def
 
 end
 
@@ -185,11 +217,11 @@ theory FsetComprehension
   (** { f x | x in U } *)
   function map (f: 'a -> 'b) (u: set 'a) : set 'b
 
-  axiom map_def:
+  axiom map_def1:
     forall f: 'a -> 'b, u: set 'a.
     forall y: 'b. mem y (map f u) <-> (exists x: 'a. mem x u /\ y = f x)
 
-  lemma map_def1:
+  lemma map_def2:
     forall f: 'a -> 'b, u: set 'a.
     forall x: 'a. mem x u -> mem (f x) (map f u)
 
@@ -246,6 +278,7 @@ theory Fsetint
 
   axiom min_elt_def1:
     forall s: set int. not (is_empty s) -> mem (min_elt s) s
+
   axiom min_elt_def2:
     forall s: set int. forall x: int. mem x s -> min_elt s <= x
 
@@ -253,6 +286,7 @@ theory Fsetint
 
   axiom max_elt_def1:
     forall s: set int. not (is_empty s) -> mem (max_elt s) s
+
   axiom max_elt_def2:
     forall s: set int. forall x: int. mem x s -> x <= max_elt s
 
@@ -330,59 +364,3 @@ theory FsetSum "Sum of the elements of a container limited to a finite set of ke
     (forall k : key. S.mem k s -> f c1 k = f c2 k) -> sum c1 s = sum c2 s
 
 end
-
-
-(** {2 Sets realized as maps} *)
-
-theory SetMap
-
-  use import map.Map
-  use import bool.Bool
-
-  type set 'a = map 'a bool
-
-  predicate mem (x:'a) (s:set 'a) = s[x] = True
-
-  constant empty : set 'a = const False
-
-  predicate is_empty (s : set 'a) = forall x : 'a. not (mem x s)
-
-  goal Empty_def1 : is_empty(empty : set 'a)
-
-  function add (x:'a) (s:set 'a) : set 'a = s[x <- True]
-
-  function remove (x:'a) (s:set 'a) : set 'a =  s[x <- False]
-
-  function union (set 'a) (set 'a) : set 'a
-
-  axiom Union_def :
-    forall s1 s2 : set 'a. forall x : 'a.
-    (union s1 s2)[x] = orb s1[x] s2[x]
-
-  function inter (set 'a) (set 'a) : set 'a
-
-  axiom Inter_def :
-    forall s1 s2 : set 'a. forall x : 'a.
-    (inter s1 s2)[x] = andb s1[x] s2[x]
-
-  function diff (set 'a) (set 'a) : set 'a
-
-  axiom Diff_def1 :
-    forall s1 s2 : set 'a. forall x : 'a.
-    (diff s1 s2)[x] = andb s1[x] (notb s2[x])
-
-  predicate equal(s1 s2 : set 'a) = forall x : 'a. s1[x] = s2[x]
-
-(* dubious axiom: extensionality should be postulated on maps instead
-  axiom Equal_is_eq : forall s1 s2 : set 'a. equal s1 s2 -> s1 = s2
-*)
-
-  predicate subset(s1 s2 : set 'a) = forall x : 'a. mem x s1 -> mem x s2
-
-  function complement (set 'a) : set 'a
-
-  axiom Complement_def :
-    forall s : set 'a. forall x : 'a.
-    (complement s)[x] = notb s[x]
-
-end