Commit acff993f authored by Andrei Paskevich's avatar Andrei Paskevich

[] and [<-] are again syntactic sugar for set and get

another birthday gift for François
parent 132bd08d
...@@ -2,8 +2,8 @@ import "alt_ergo.drv" ...@@ -2,8 +2,8 @@ import "alt_ergo.drv"
theory map.Map theory map.Map
syntax type map "(%1,%2) farray" syntax type map "(%1,%2) farray"
syntax logic ([]) "(%1[%2])" syntax logic get "(%1[%2])"
syntax logic ([<-]) "(%1[%2 <- %3])" syntax logic set "(%1[%2 <- %3])"
end end
(* (*
......
...@@ -134,11 +134,11 @@ end ...@@ -134,11 +134,11 @@ end
theory map.Map theory map.Map
syntax type map "(ARRAY %1 OF %2)" syntax type map "(ARRAY %1 OF %2)"
meta "encoding : lskept" logic ([]) meta "encoding : lskept" logic get
meta "encoding : lskept" logic ([<-]) meta "encoding : lskept" logic set
syntax logic ([]) "(%1[%2])" syntax logic get "(%1[%2])"
syntax logic ([<-]) "(%1 WITH [%2] := %3)" syntax logic set "(%1 WITH [%2] := %3)"
end end
(* (*
......
...@@ -150,12 +150,12 @@ end ...@@ -150,12 +150,12 @@ end
theory map.Map theory map.Map
syntax type map "(Array %1 %2)" syntax type map "(Array %1 %2)"
meta "encoding : lskept" logic ([]) meta "encoding : lskept" logic get
meta "encoding : lskept" logic ([<-]) meta "encoding : lskept" logic set
meta "encoding : lskept" logic const meta "encoding : lskept" logic const
syntax logic ([]) "(select %1 %2)" syntax logic get "(select %1 %2)"
syntax logic ([<-]) "(store %1 %2 %3)" syntax logic set "(store %1 %2 %3)"
syntax logic const "(const[%t0] %1)" syntax logic const "(const[%t0] %1)"
end end
......
...@@ -8,15 +8,20 @@ module Array ...@@ -8,15 +8,20 @@ module Array
type array 'a model {| length : int; mutable elts : map int 'a |} type array 'a model {| length : int; mutable elts : map int 'a |}
logic ([]) (a: array 'a) (i :int) : 'a = M.([]) a.elts i logic get (a: array 'a) (i: int) : 'a = M.get a.elts i
logic ([<-]) (a: array 'a) (i :int) (v: 'a) : array 'a =
{| a with elts = M.([<-]) a.elts i v |} logic set (a: array 'a) (i: int) (v: 'a) : array 'a =
{| a with elts = M.set a.elts i v |}
(* syntactic sugar *)
logic ([]) (a: array 'a) (i: int) : 'a = get a i
logic ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
parameter ([]) : a:array 'a -> i:int -> parameter ([]) : a:array 'a -> i:int ->
{ 0 <= i < length a } 'a reads a { result = a[i] } { 0 <= i < length a } 'a reads a { result = a[i] }
parameter ([]<-) : a:array 'a -> i:int -> v:'a -> parameter ([]<-) : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < length a } unit writes a { a.elts = M.([<-]) (old a.elts) i v } { 0 <= i < length a } unit writes a { a.elts = M.set (old a.elts) i v }
(* unsafe get/set operations with no precondition *) (* unsafe get/set operations with no precondition *)
exception OutOfBounds exception OutOfBounds
......
...@@ -3,12 +3,12 @@ theory Map "Theory of maps" ...@@ -3,12 +3,12 @@ theory Map "Theory of maps"
type map 'a 'b type map 'a 'b
logic ([]) (map 'a 'b) 'a : 'b logic get (map 'a 'b) 'a : 'b
logic ([<-]) (map 'a 'b) 'a 'b : map 'a 'b logic set (map 'a 'b) 'a 'b : map 'a 'b
(* aliases to use under qualifiers *) (* syntactic sugar *)
logic get (a : map 'a 'b) (i : 'a) : 'b = a[i] logic ([]) (a : map 'a 'b) (i : 'a) : 'b = get a i
logic set (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = a[i <- v] logic ([<-]) (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = set a i v
axiom Select_eq : axiom Select_eq :
forall m : map 'a 'b. forall a1 a2 : 'a. forall m : map 'a 'b. forall a1 a2 : 'a.
......
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