Commit 72b832c5 authored by Andrei Paskevich's avatar Andrei Paskevich

support mixfix symbols to drivers

parent b71623a7
import "alt_ergo.drv" import "alt_ergo.drv"
theory map.Map theory map.Map
syntax type map "(%1,%2) farray" syntax type map "(%1,%2) farray"
syntax logic get "(%1[%2])" syntax logic ([]) "(%1[%2])"
syntax logic set "(%1[%2 <- %3])" syntax logic ([<-]) "(%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 get meta "encoding : lskept" logic ([])
meta "encoding : lskept" logic set meta "encoding : lskept" logic ([<-])
syntax logic get "(%1[%2])" syntax logic ([]) "(%1[%2])"
syntax logic set "(%1 WITH [%2] := %3)" syntax logic ([<-]) "(%1 WITH [%2] := %3)"
end end
(* (*
......
...@@ -150,13 +150,13 @@ end ...@@ -150,13 +150,13 @@ end
theory map.Map theory map.Map
syntax type map "(Array %1 %2)" syntax type map "(Array %1 %2)"
meta "encoding : lskept" logic get meta "encoding : lskept" logic ([])
meta "encoding : lskept" logic set meta "encoding : lskept" logic ([<-])
meta "encoding : lskept" logic const meta "encoding : lskept" logic const
syntax logic get "(select %1 %2)" syntax logic ([]) "(select %1 %2)"
syntax logic set "(store %1 %2 %3)" syntax logic ([<-]) "(store %1 %2 %3)"
syntax logic const "(const[%t0] %1)" syntax logic const "(const[%t0] %1)"
end end
......
...@@ -5,13 +5,13 @@ module M ...@@ -5,13 +5,13 @@ module M
(* preliminaries *) (* preliminaries *)
use map.Map as M use import map.Map as M
type array 'a = M.map int 'a type array 'a = M.map int 'a
logic injective (n:int) (m:int) (a:array 'a) = logic injective (n:int) (m:int) (a:array 'a) =
forall i j:int. n <= i <= m -> n <= j <= m -> forall i j:int. n <= i <= m -> n <= j <= m ->
M.get a i = M.get a j -> i = j a[i] = a[j] -> i = j
type string type string
...@@ -26,7 +26,7 @@ module M ...@@ -26,7 +26,7 @@ module M
logic valid (a:first_free_addr) (p:pointer) = p < a logic valid (a:first_free_addr) (p:pointer) = p < a
logic valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) = logic valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) =
forall i:int. n <= i <= m -> valid a (M.get r i) forall i:int. n <= i <= m -> valid a (r[i])
parameter alloc : ref first_free_addr parameter alloc : ref first_free_addr
...@@ -76,7 +76,7 @@ end ...@@ -76,7 +76,7 @@ end
axiom MarkSumNonEmpty : axiom MarkSumNonEmpty :
forall r:region student, i j:int, a : array pointer. forall r:region student, i j:int, a : array pointer.
i <= j -> i <= j ->
let (_,mark) = M.get r (M.get a j) in let (_,mark) = r[a[j]] in
markSum r i j a = markSum r i (j-1) a + mark markSum r i j a = markSum r i (j-1) a + mark
(* (*
...@@ -92,13 +92,13 @@ end ...@@ -92,13 +92,13 @@ end
lemma MarkSum_set_array_outside : lemma MarkSum_set_array_outside :
forall r:region student, i j k:int, a: array pointer, p:pointer. forall r:region student, i j k:int, a: array pointer, p:pointer.
not (i <= k <= j) -> not (i <= k <= j) ->
markSum r i j (M.set a k p) = markSum r i j a markSum r i j (a[k <- p]) = markSum r i j a
lemma MarkSum_set_region_outside : lemma MarkSum_set_region_outside :
forall r:region student, i j:int, a: array pointer, p:pointer, s:student. forall r:region student, i j:int, a: array pointer, p:pointer, s:student.
(forall k:int. i <= k <= j -> M.get a k <> p) -> (forall k:int. i <= k <= j -> a[k] <> p) ->
markSum (M.set r p s) i j a = markSum r i j a markSum (r[p <- s]) i j a = markSum r i j a
...@@ -128,9 +128,9 @@ fun CreateCourse(R:[Course]): [R] ...@@ -128,9 +128,9 @@ fun CreateCourse(R:[Course]): [R]
let createCourse (r: (ref (region course))) : pointer = let createCourse (r: (ref (region course))) : pointer =
{ } { }
let c = new_pointer () in let c = new_pointer () in
let (rStud,student,count,sum) = M.get !r c in let (rStud,student,count,sum) = !r[c] in
let newc = (rStud,student,0,0) in let newc = (rStud,student,0,0) in
r := M.set !r c newc; r := !r[c <- newc];
assert { invCourse !alloc newc }; assert { invCourse !alloc newc };
c c
{ valid !alloc result } { valid !alloc result }
...@@ -152,12 +152,12 @@ fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud] ...@@ -152,12 +152,12 @@ fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
let registerStudent let registerStudent
(r: (ref (region course))) (c:pointer) (name:string) : pointer = (r: (ref (region course))) (c:pointer) (name:string) : pointer =
{ valid !alloc c and invCourse !alloc (M.get !r c) } { valid !alloc c and invCourse !alloc !r[c] }
let s = new_pointer () in let s = new_pointer () in
let (rStud,student,count,sum) = M.get !r c in let (rStud,student,count,sum) = !r[c] in
let newstud = (name,0) in let newstud = (name,0) in
let newc = (M.set rStud s newstud,M.set student count s,count+1,sum) in let newc = (rStud[s <- newstud],student[count <- s],count+1,sum) in
r := M.set !r c newc; r := !r[c <- newc];
assert { invCourse !alloc newc }; assert { invCourse !alloc newc };
s s
{ valid !alloc result } { valid !alloc result }
......
...@@ -5,7 +5,7 @@ module M ...@@ -5,7 +5,7 @@ module M
use import int.Int use import int.Int
use import module ref.Ref use import module ref.Ref
use set.Fset as S use set.Fset as S
use map.Map as M use import map.Map as M
(* iteration on a set *) (* iteration on a set *)
...@@ -66,32 +66,32 @@ module M ...@@ -66,32 +66,32 @@ module M
unit writes visited q d unit writes visited q d
{ S.is_empty !visited and { S.is_empty !visited and
!q = S.add src S.empty and !q = S.add src S.empty and
!d = M.set (old !d) src 0 } !d = (old !d)[src <- 0] }
let relax u v = let relax u v =
{} {}
if not (S.mem v !visited) then if not (S.mem v !visited) then
let x = M.get !d u + weight u v in let x = !d[u] + weight u v in
if S.mem v !q then begin if S.mem v !q then begin
if x < M.get !d v then d := M.set !d v x if x < !d[v] then d := !d[v <- x]
end else begin end else begin
q := S.add v !q; q := S.add v !q;
d := M.set !d v x d := !d[v <- x]
end end
{ (S.mem v !visited and !q = old !q and !d = old !d) { (S.mem v !visited and !q = old !q and !d = old !d)
or or
(S.mem v !q and M.get !d u + weight u v >= M.get !d v and (S.mem v !q and !d[u] + weight u v >= !d[v] and
!q = old !q and !d = old !d) !q = old !q and !d = old !d)
or or
(S.mem v !q and M.get (old !d) u + weight u v < M.get (old !d) v and (S.mem v !q and (old !d)[u] + weight u v < (old !d)[v] and
!q = old !q and !d = M.set (old !d) v (M.get (old !d) u + weight u v)) !q = old !q and !d = (old !d)[v <- (old !d)[u] + weight u v])
or or
(not S.mem v !visited and not S.mem v (old !q) and !q = S.add v (old !q) and (not S.mem v !visited and not S.mem v (old !q) and !q = S.add v (old !q) and
!d = M.set (old !d) v (M.get (old !d) u + weight u v)) } !d = (old !d)[v <- (old !d)[u] + weight u v]) }
logic min (m:vertex) (q:S.set vertex) (d:M.map vertex int) = logic min (m:vertex) (q:S.set vertex) (d:M.map vertex int) =
S.mem m q and S.mem m q and
forall x:vertex. S.mem x q -> M.get d m <= M.get d x forall x:vertex. S.mem x q -> d[m] <= d[x]
parameter q_extract_min : parameter q_extract_min :
unit -> unit ->
...@@ -158,15 +158,15 @@ module M ...@@ -158,15 +158,15 @@ module M
(forall v:vertex. S.mem v q -> S.mem v s -> false) (forall v:vertex. S.mem v q -> S.mem v s -> false)
(* we already found the shortest paths for vertices in S *) (* we already found the shortest paths for vertices in S *)
and and
(forall v:vertex. S.mem v s -> shortest_path src v (M.get d v)) (forall v:vertex. S.mem v s -> shortest_path src v d[v])
(* there are paths for vertices in Q *) (* there are paths for vertices in Q *)
and and
(forall v:vertex. S.mem v q -> path src v (M.get d v)) (forall v:vertex. S.mem v q -> path src v d[v])
(* vertices at distance < min(Q) are already in S *) (* vertices at distance < min(Q) are already in S *)
and and
(forall m:vertex. min m q d -> (forall m:vertex. min m q d ->
forall x:vertex. forall dx:int. shortest_path src x dx -> forall x:vertex. forall dx:int. shortest_path src x dx ->
dx < M.get d m -> S.mem x s) dx < d[m] -> S.mem x s)
logic inv_succ (src:vertex) (s q : S.set vertex) = logic inv_succ (src:vertex) (s q : S.set vertex) =
(* successors of vertices in S are either in S or in Q *) (* successors of vertices in S are either in S or in Q *)
...@@ -190,7 +190,7 @@ module M ...@@ -190,7 +190,7 @@ module M
invariant { inv src !visited !q !d and inv_succ src !visited !q } invariant { inv src !visited !q !d and inv_succ src !visited !q }
variant { S.cardinal v - S.cardinal !visited } variant { S.cardinal v - S.cardinal !visited }
let u = q_extract_min () in let u = q_extract_min () in
assert { shortest_path src u (M.get !d u) }; assert { shortest_path src u !d[u] };
visited_add u; visited_add u;
let su = ref (g_succ u) in let su = ref (g_succ u) in
while not (set_has_next su) do while not (set_has_next su) do
...@@ -203,7 +203,7 @@ module M ...@@ -203,7 +203,7 @@ module M
done done
done done
{ (forall v:vertex. { (forall v:vertex.
S.mem v !visited -> shortest_path src v (M.get !d v)) S.mem v !visited -> shortest_path src v !d[v])
and and
(forall v:vertex. (forall v:vertex.
not S.mem v !visited -> forall dv:int. not path src v dv) } not S.mem v !visited -> forall dv:int. not path src v dv) }
......
...@@ -12,18 +12,18 @@ module M ...@@ -12,18 +12,18 @@ module M
type option 'a = None | Some 'a type option 'a = None | Some 'a
use map.Map as M use import map.Map as M
type table = M.map int (option int) type table = M.map int (option int)
logic inv (t : table) = logic inv (t : table) =
forall x y : int. M.get t x = Some y -> y = fib x forall x y : int. t[x] = Some y -> y = fib x
parameter table : ref table parameter table : ref table
parameter add : parameter add :
x:int -> y:int -> x:int -> y:int ->
{} unit writes table { !table = M.set (old !table) x (Some y) } {} unit writes table { !table = (old !table)[x <- Some y] }
exception Not_found exception Not_found
...@@ -31,8 +31,8 @@ module M ...@@ -31,8 +31,8 @@ module M
x:int -> x:int ->
{} {}
int reads table raises Not_found int reads table raises Not_found
{ M.get !table x = Some result } { !table[x] = Some result }
| Not_found -> { M.get !table x = None } | Not_found -> { !table[x] = None }
let rec fibo n = let rec fibo n =
{ 0 <= n and inv !table } { 0 <= n and inv !table }
......
This diff is collapsed.
...@@ -6,7 +6,7 @@ module Muller ...@@ -6,7 +6,7 @@ module Muller
use import module array.Array use import module array.Array
type param = M.map int int type param = M.map int int
logic pr (a : param) (n : int) = M.get a n <> 0 logic pr (a : param) (n : int) = M.([]) a n <> 0
clone import int.NumOfParam with type param = param, logic pr = pr clone import int.NumOfParam with type param = param, logic pr = pr
let compact (a : array int) = let compact (a : array int) =
......
...@@ -9,17 +9,17 @@ theory Sorted ...@@ -9,17 +9,17 @@ theory Sorted
logic n : int = 4 logic n : int = 4
logic sorted(m : array) = logic sorted(m : array) =
forall x y:int. x<=y -> Real.(<=)(get m x) (get m y) forall x y:int. x<=y -> Real.(<=) m[x] m[y]
logic count(m : array) (i j : int) (v : real) : int logic count(m : array) (i j : int) (v : real) : int
axiom Count : axiom Count :
forall m : array. forall i j : int. forall v : real. count m i j v = forall m : array. forall i j : int. forall v : real. count m i j v =
(if i = j then 0 else (if i = j then 0 else
let c = count m (i+1) j v in let c = count m (i+1) j v in
(if get m i = v then c + 1 else c)) (if m[i] = v then c + 1 else c))
logic model(m1 : array) (m2 : multi) = logic model(m1 : array) (m2 : multi) =
forall v:real. count m1 1 (n+1) v = get m2 v forall v:real. count m1 1 (n+1) v = m2[v]
(* (*
logic model_aux(m1 : array, i : int) : multi logic model_aux(m1 : array, i : int) : multi
...@@ -43,32 +43,32 @@ theory Sorted ...@@ -43,32 +43,32 @@ theory Sorted
goal G : goal G :
forall m1 : array. forall m1 : array.
get m1 1 = 42. -> m1[1] = 42. ->
get m1 2 = 13. -> m1[2] = 13. ->
get m1 3 = 42. -> m1[3] = 42. ->
get m1 4 = 45. -> m1[4] = 45. ->
forall m2 : array. forall m2 : array.
forall multi : multi. forall multi : multi.
model m1 multi -> model m1 multi ->
model m2 multi -> model m2 multi ->
sorted m2 -> sorted m2 ->
get m2 1 = 13. and m2[1] = 13. and
get m2 2 = 42. and m2[2] = 42. and
get m2 3 = 42. and m2[3] = 42. and
get m2 4 = 45. m2[4] = 45.
(* goal G_false : (* goal G_false :
forall m1 : array. forall m1 : array.
get m1 1 = 42. -> m1[1] = 42. ->
get m1 2 = 13. -> m1[2] = 13. ->
get m1 3 = 42. -> m1[3] = 42. ->
forall m2 : array. forall m2 : array.
forall multi : multi. forall multi : multi.
model m1 multi -> model m1 multi ->
model m2 multi -> model m2 multi ->
sorted m2 -> sorted m2 ->
get m2 1 = 42. and m2[1] = 42. and
get m2 2 = 13. and m2[2] = 13. and
get m2 3 = 42. m2[3] = 42.
*) *)
end end
\ No newline at end of file
...@@ -8,7 +8,7 @@ module Hashtbl ...@@ -8,7 +8,7 @@ module Hashtbl
type t 'a model {| mutable contents: map key (list 'a) |} type t 'a model {| mutable contents: map key (list 'a) |}
logic ([]) (h: t 'a) (k: key) : list 'a = get h.contents k logic ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
parameter create: n:int -> parameter create: n:int ->
{} t 'a { forall k: key. result[k] = Nil } {} t 'a { forall k: key. result[k] = Nil }
......
...@@ -80,6 +80,12 @@ rule token = parse ...@@ -80,6 +80,12 @@ rule token = parse
{ try Hashtbl.find keywords id with Not_found -> IDENT id } { try Hashtbl.find keywords id with Not_found -> IDENT id }
| digit+ as i | digit+ as i
{ INTEGER (int_of_string i) } { INTEGER (int_of_string i) }
| "<-"
{ LARROW }
| "["
{ LEFTSQ }
| "]"
{ RIGHTSQ }
| "(" | "("
{ LEFTPAR } { LEFTPAR }
| ")" | ")"
......
...@@ -24,6 +24,7 @@ ...@@ -24,6 +24,7 @@
let loc_i i = Loc.extract (rhs_start_pos i, rhs_end_pos i) let loc_i i = Loc.extract (rhs_start_pos i, rhs_end_pos i)
let infix s = "infix " ^ s let infix s = "infix " ^ s
let prefix s = "prefix " ^ s let prefix s = "prefix " ^ s
let mixfix s = "mixfix " ^ s
%} %}
%token <string> INPUT /* never reaches the parser */ %token <string> INPUT /* never reaches the parser */
...@@ -37,6 +38,7 @@ ...@@ -37,6 +38,7 @@
%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF %token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
%token LOGIC TYPE PROP FILENAME TRANSFORM PLUGIN %token LOGIC TYPE PROP FILENAME TRANSFORM PLUGIN
%token LEFTPAR_STAR_RIGHTPAR COMMA %token LEFTPAR_STAR_RIGHTPAR COMMA
%token LEFTSQ RIGHTSQ LARROW
%type <Driver_ast.file> file %type <Driver_ast.file> file
%start file %start file
...@@ -142,9 +144,15 @@ ident: ...@@ -142,9 +144,15 @@ ident:
; ;
ident_rich: ident_rich:
| ident { $1 } | ident { $1 }
| LEFTPAR_STAR_RIGHTPAR { infix "*" } | LEFTPAR_STAR_RIGHTPAR { infix "*" }
| LEFTPAR OPERATOR RIGHTPAR { infix $2 } | LEFTPAR operator RIGHTPAR { $2 }
| LEFTPAR OPERATOR UNDERSCORE RIGHTPAR { prefix $2 } ;
operator:
| OPERATOR { infix $1 }
| OPERATOR UNDERSCORE { prefix $1 }
| LEFTSQ RIGHTSQ { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
; ;
...@@ -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 get (a : map 'a 'b) (i : 'a) : 'b logic ([]) (map 'a 'b) 'a : 'b
logic set (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b logic ([<-]) (map 'a 'b) 'a 'b : map 'a 'b
(* syntactic sugar *) (* aliases to use under qualifiers *)
logic ([]) (a : map 'a 'b) (i : 'a) : 'b = get a i logic get (a : map 'a 'b) (i : 'a) : 'b = a[i]
logic ([<-]) (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = set a i v logic set (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = 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