updated more drivers

drivers/coq-ssreflect.drv

@@ -62,7 +62,9 @@ end
 theory map.Map
   syntax type     map "(%1 -> %2)%type"
   syntax function get "(%1 %2)"
+end
 
+theory map.Const
   remove prop Const
 end
 

drivers/mathsat.drv

@@ -170,10 +170,13 @@ 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)"
+end
+
+theory map.Const
+  meta "encoding : lskept" function const
 (*  syntax function const "(const[%t0] %1)" *)
 end
 

drivers/pvs-common.gen

@@ -38,6 +38,9 @@ theory map.Map
   remove prop Select_eq
   remove prop Select_neq
 
+end
+
+theory map.Const
   syntax function const "(LAMBDA (x:%v0): %1)"
   remove prop Const
 end
@@ -263,7 +266,7 @@ end
 
 theory list.Mem
   syntax predicate mem "member(%1, %2)"
-  
+
 end
 
 theory list.Nth

drivers/smt-libv2.drv

@@ -144,9 +144,12 @@ 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)"
+end
+
+theory map.Const
+  meta "encoding : lskept" function const
 (*  syntax function const "(const[%t0] %1)" *)
 end

drivers/why3_smt.drv

@@ -26,6 +26,9 @@ end
 theory map.Map
   meta "encoding : lskept" function get
   meta "encoding : lskept" function set
+end
+
+theory map.Const
   meta "encoding : lskept" function const
 end
 

drivers/yices.drv

@@ -147,8 +147,10 @@ theory map.Map
   syntax function ([<-]) "(update %1 (%2) %3)"
 
 
-  meta "encoding : lskept" function const
+end
 
+theory map.Const
+  meta "encoding : lskept" function const
 end
 
 (*

modules/mach/array.mlw

@@ -50,12 +50,15 @@ module Array32
   = if i < of_int 0 || i >= length a then raise OutOfBounds;
     a[i] <- v
 
-  function make (n: int32) (v: ~'a) : array 'a =
-    { length = n; elts = M.const v }
+  function make (n: int32) (v: ~'a) : array 'a
+  axiom make_length:
+    forall n:int32, v:'a. length (make n v) = n
+  axiom make_elts:
+    forall n:int32, i:int, v:'a. get (make n v) i = v
 
   val make (n: int32) (v: ~'a) : array 'a
     requires { "expl:array creation size" to_int n >= 0 }
-    ensures  { result = make n v }
+    ensures { forall i:int. get result i = v }
 
   val append (a1: array ~'a) (a2: array 'a) : array 'a
     ensures { to_int result.length = to_int a1.length + to_int a2.length }
@@ -167,12 +170,15 @@ module Array31
   = if i < of_int 0 || i >= length a then raise OutOfBounds;
     a[i] <- v
 
-  function make (n: int31) (v: ~'a) : array 'a =
-    { length = n; elts = M.const v }
+  function make (n: int31) (v: ~'a) : array 'a
+  axiom make_length:
+    forall n:int31, v:'a. length (make n v) = n
+  axiom make_elts:
+    forall n:int31, i:int, v:'a. get (make n v) i = v
 
   val make (n: int31) (v: ~'a) : array 'a
     requires { "expl:array creation size" to_int n >= 0 }
-    ensures  { result = make n v }
+    ensures { forall i:int. get result i = v }
 
   val append (a1: array ~'a) (a2: array 'a) : array 'a
     ensures { to_int result.length = to_int a1.length + to_int a2.length }
@@ -284,12 +290,15 @@ module Array63
   = if i < of_int 0 || i >= length a then raise OutOfBounds;
     a[i] <- v
 
-  function make (n: int63) (v: ~'a) : array 'a =
-    { length = n; elts = M.const v }
+  function make (n: int63) (v: ~'a) : array 'a
+  axiom make_length:
+    forall n:int63, v:'a. length (make n v) = n
+  axiom make_elts:
+    forall n:int63, i:int, v:'a. get (make n v) i = v
 
   val make (n: int63) (v: ~'a) : array 'a
     requires { "expl:array creation size" to_int n >= 0 }
-    ensures  { result = make n v }
+    ensures { forall i:int. get result i = v }
 
   val append (a1: array ~'a) (a2: array 'a) : array 'a
     ensures { to_int result.length = to_int a1.length + to_int a2.length }

modules/matrix.mlw

@@ -50,11 +50,14 @@ module Matrix
     if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
     set a i v
 
-  function make (r c: int) (v: 'a) : matrix 'a =
-    { rows = r; columns = c; elts = M.const (M.const v) }
+  function make (r c: int) (v: 'a) : matrix 'a
+  axiom make_rows: forall r c, v:'a. (make r c v).rows = r
+  axiom make_columns: forall r c, v:'a. (make r c v).columns = c
+  axiom make_elts: forall r c, v:'a, i j. get (make r c v) (i,j) = v
 
   val make (r c: int) (v: 'a) : matrix 'a
-    requires { r >= 0 /\ c >= 0 } ensures { result = make r c v }
+    requires { r >= 0 /\ c >= 0 }
+    ensures { result = make r c v }
 
   val copy (a: matrix 'a) : matrix 'a
     ensures  { result.rows = a.rows /\ result.columns = a.columns }
@@ -84,4 +87,3 @@ module Syntax
              a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }
 
 end
-

src/whyml/mlw_interp.ml

@@ -433,10 +433,11 @@ let built_in_theories =
       "mod", None, eval_int_op BigInt.euclidean_mod;
     ] ;
     ["map"],"Map", ["map", builtin_map_type],
-    [ "const", Some ls_map_const, eval_map_const;
-      "get", Some ls_map_get, eval_map_get;
+    [ "get", Some ls_map_get, eval_map_get;
       "set", Some ls_map_set, eval_map_set;
     ] ;
+    ["map"],"Const", [],
+    [ "const", Some ls_map_const, eval_map_const ] ;
   ]
 
 let add_builtin_th env (l,n,t,d) =