Commit 7e80633b authored by Andrei Paskevich's avatar Andrei Paskevich

no implicit match in type invariants for records

+ the implicitly bound variable in type invariants
  is now called "self"
parent 5e6c85ae
......@@ -769,7 +769,8 @@ The two list lengths are explicitly stored, for better efficiency.
\begin{whycode}
type queue 'a = { front: list 'a; lenf: int;
rear : list 'a; lenr: int; }
invariant { length front = lenf >= length rear = lenr }
invariant {
length self.front = self.lenf >= length self.rear = self.lenr }
\end{whycode}
The type definition is accompanied with an invariant ---
a logical property imposed on any value of the type.
......@@ -868,7 +869,8 @@ module AmortizedQueue
type queue 'a = { front: list 'a; lenf: int;
rear : list 'a; lenr: int; }
invariant { length front = lenf >= length rear = lenr }
invariant {
length self.front = self.lenf >= length self.rear = self.lenr }
function sequence (q: queue 'a) : list 'a = q.front ++ reverse q.rear
......
......@@ -47,7 +47,7 @@ module HashTableImpl
type t 'a 'b = { mutable contents: map 'a (option 'b);
data: array (list ('a, 'b)) }
invariant { length data > 0 }
invariant { length self.data > 0 }
function get (h: t 'a 'b) (k: 'a) : option 'b = Map.get h.contents k
......@@ -77,11 +77,11 @@ module HashTableImpl
type t 'c 'b
(* h[k]=v iff (k,v) is the first pair for k in the bucket for k *)
invariant { forall k: 'c, v: 'b.
get result k = Some v <-> occurs_first k v data[idx result k] }
get self k = Some v <-> occurs_first k v self.data[idx self k] }
(* a pair (k,v) is always stored in the right bucket *)
invariant { forall k: 'c, v: 'b.
forall i: int. 0 <= i < length data ->
mem (k,v) data[i] -> i = idx result k }
forall i: int. 0 <= i < length self.data ->
mem (k,v) self.data[i] -> i = idx self k }
let create (n:int)
requires { 0 < n }
......
......@@ -9,7 +9,7 @@ module ResizableArrayImplem
constant dummy: elt
type rarray = { mutable length: int; mutable data: A.array elt }
invariant { 0 <= length <= A.length data }
invariant { 0 <= self.length <= A.length self.data }
function ([]) (r: rarray) (i: int) : elt = A.get r.data i
function ([<-]) (r: rarray) (i: int) (v: elt) : rarray =
......
......@@ -141,7 +141,7 @@ module ITree
use export BSTree
use export Iterator
type itree = { mutable tree: tree } invariant { bst tree }
type itree = { mutable tree: tree } invariant { bst self.tree }
let create () = { tree = Empty }
......
......@@ -31,11 +31,11 @@ back +-+-+-+-------------------+
mutable card : int;
def : 'a; }
invariant {
0 <= card <= A.length values <= maxlen /\
A.length values = A.length index = A.length back /\
0 <= self.card <= A.length self.values <= maxlen /\
A.length self.values = A.length self.index = A.length self.back /\
forall i : int.
0 <= i < card ->
0 <= back[i] < A.length values /\ index[back[i]] = i
0 <= i < self.card ->
0 <= self.back[i] < A.length self.values /\ self.index[self.back[i]] = i
}
predicate is_elt (a: sparse_array 'a) (i: int) =
......
......@@ -13,7 +13,7 @@ module AmortizedQueue
type queue 'a = { front: list 'a; lenf: int;
rear : list 'a; lenr: int; }
invariant { length front = lenf >= length rear = lenr }
invariant { length self.front = self.lenf >= length self.rear = self.lenr }
function sequence (q: queue 'a) : list 'a =
q.front ++ reverse q.rear
......
......@@ -20,15 +20,15 @@ module RingBuffer
ghost mutable sequence: list 'a;
}
invariant {
let size = Array.length data in
0 <= first < size /\
0 <= len <= size /\
len = L.length sequence /\
forall i: int. 0 <= i < len ->
(first + i < size ->
nth i sequence = Some data[first + i]) /\
(0 <= first + i - size ->
nth i sequence = Some data[first + i - size])
let size = Array.length self.data in
0 <= self.first < size /\
0 <= self.len <= size /\
self.len = L.length self.sequence /\
forall i: int. 0 <= i < self.len ->
(self.first + i < size ->
nth i self.sequence = Some self.data[self.first + i]) /\
(0 <= self.first + i - size ->
nth i self.sequence = Some self.data[self.first + i - size])
}
(* total capacity of the buffer *)
......
......@@ -108,11 +108,11 @@ module HashtblImpl
forall k: key. 0 <= bucket k n < n
type t 'a = { mutable size: int; (* total number of elements *)
mutable data: array (list (key, 'a)); }
invariant { let n = Array.length data in
mutable data: array (list (key, 'a)); }
invariant { let n = Array.length self.data in
0 < n /\
forall i: int. 0 <= i < n ->
forall k: key, v: 'a. mem (k, v) data[i] -> bucket k n = i }
forall k: key, v: 'a. mem (k,v) self.data[i] -> bucket k n = i }
function extract (k: key) (l: list (key, 'a)) : list 'a = match l with
| Nil -> Nil
......
......@@ -1261,7 +1261,7 @@ and expr_lam lenv gh pvl (de, dsp) =
(** Type declaration *)
let add_type_invariant loc uc id params inv =
let x = "result" in
let x = "self" in
let its = match uc_find_ts uc (Qident id) with
| PT its when its.its_inv -> its
| _ -> errorm ~loc "type %s does not have an invariant" id.id in
......@@ -1273,30 +1273,10 @@ let add_type_invariant loc uc id params inv =
let res = create_vsymbol (id_fresh x) ty in
let vars = Mstr.singleton x res in
let denv = Typing.add_var x (dty_of_ty ty) Typing.denv_empty in
(* invariants on records may use field names as variables *)
let fields = try match find_constructors (get_known uc) its with
| [cs, pjl] -> Some (cs, List.map Opt.get pjl)
| _ -> None with _ -> None in
let inv = match fields with
| None ->
let mk_inv f =
let f = Typing.type_fmla (get_theory uc) denv vars f in
t_label_add Split_goal.stop_split f in
List.map mk_inv inv
| Some (cs, pjl) ->
let idl = List.map (fun pj -> PPvar (id_clone pj.pl_ls.ls_name)) pjl in
let ppp = PPlapp (cs.pl_ls, idl) and vty = vty_value (ity_of_ty ty) in
let mpv, { ppat_pattern = pat } = Mlw_expr.make_ppattern ppp vty in
let vars = Mstr.set_union (Mstr.map (fun v -> v.pv_vs) mpv) vars in
let denv = Mstr.fold (fun x pv denv ->
Typing.add_var x (dty_of_ty pv.pv_vs.vs_ty) denv) mpv denv in
let mk_inv f =
let f = Typing.type_fmla (get_theory uc) denv vars f in
let f = match f.t_node with
| Ttrue | Tfalse -> f
| _ -> t_case (t_var res) [t_close_branch pat f] in
t_label_add Split_goal.stop_split f in
List.map mk_inv inv in
let mk_inv f =
let f = Typing.type_fmla (get_theory uc) denv vars f in
t_label_add Split_goal.stop_split f in
let inv = List.map mk_inv inv in
let q = Mlw_ty.create_post res (t_and_simp_l inv) in
let q = if List.for_all2 tv_equal its.its_args tvl then q else
let add mtv u v = Mtv.add u (ty_var v) mtv in
......
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