diff --git a/src/lib/constraints/simple.template.mlw b/src/lib/constraints/simple.template.mlw
index 27761e3737789034e89738d9940e6e42ed5eed31..260800f0d3ac304b40f828ead27217219ab5b8c2 100644
--- a/src/lib/constraints/simple.template.mlw
+++ b/src/lib/constraints/simple.template.mlw
@@ -3,12 +3,12 @@ module Simple
use cp.Type
use cp.Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use cp.DomI
use cp.DomB
use seq.Seq as Seq
- use cp.Int63 as Int63
+ use utils.extstd.Int63 as Int63
use export cp.ConstraintHelpers
{% for cstr in constraints %} use {{ cstr.file }}.{{ cstr.module }} as {{ cstr.module }}
diff --git a/src/lib/cp.mlw b/src/lib/cp.mlw
index 18223145b0945f0a94ac062dcc1205b959abb5e5..811eb1bff75f9f2b086fc82e3aef5484420ea1cf 100644
--- a/src/lib/cp.mlw
+++ b/src/lib/cp.mlw
@@ -9,664 +9,9 @@
(* *)
(********************************************************************)
-module Bool
- use export bool.Bool
-
- let function andb' (x y : bool) : bool
- ensures { result = (x /\ y) } =
- match x with
- | True -> y
- | False -> False
- end
-
- let function eqb (x y:bool) =
- match x,y with
- | True, True | False, False -> true
- | _ -> false
- end
-end
-
-module Int63
-
- use export mach.int.Int63
-
- let function min x y = if x <= y then x else y
- let function max x y = if x <= y then y else x
-
-end
-
-module S
-
- use int.Int
- use Int63 as Int63
-
- type key
-
- val function tag (_:key): Int63.int63
- ensures { 0 <= result }
-
- axiom tag_correct: forall x y. tag x = tag y -> x = y
-
-end
-
-module TagtblIntf
-
- use int.Int
- use import Int63 as Int63
- use map.Map
- use map.Const
- use set.Fset as S
- use list.List
- use list.Mem as LMem
- use import mach.array.Array63 as Array
- use seq.Seq as Seq
- use bool.Bool
- use mach.peano.Peano as Peano
- use mach.peano.Int63 as PeanoInt63
-
- clone import S as S with axiom tag_correct
-
- type t 'a = private {
- ghost mutable contents: map key 'a;
- ghost defined: S.fset key;
- }
-
- function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
-
- val create (s:Int63.int63) (def:'a) (ghost defined: S.fset key): t 'a
- requires { forall k. S.mem k defined -> tag k <= s }
- requires { -1 <= s < Int63.max_int63 }
- ensures { result.contents = const def }
- ensures { result.defined = defined }
-
- predicate mem (k: key) (h: t 'a) = S.mem k h.defined
-
- val function max_tags (h: t 'a) : Int63.int63
- ensures { forall k. mem k h -> tag k <= result }
- ensures { -1 <= result < Int63.max_int63 }
-
- predicate set_ (h1: t 'a) (h2: t 'a) (k: key) (v: 'a) =
- h1.defined = h2.defined /\ h1.contents = h2.contents[k<-v]
-
- val set (h: t 'a) (k: key) (v: 'a) : unit
- requires { mem k h }
- ensures { set_ h (old h) k v }
- writes { h.contents }
-
- function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
-
- val function find (h: t 'a) (k: key) : 'a
- requires { mem k h }
- ensures { result = h[k] }
-
- scope Lock
- type t 'a = abstract {
- contents: map key 'a;
- defined: S.fset key;
- }
-
- function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
-
- predicate mem (k: key) (h: t 'a) = S.mem k h.defined
-
- function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
-
- val function find (h: t 'a) (k: key) : 'a
- requires { mem k h }
- ensures { result = h[k] }
-
- end
-
- val copy_lock (h: t 'a): Lock.t 'a
- ensures { result.Lock.defined = h.defined }
- ensures { result.Lock.contents = h.contents }
-
- val copy_unlock (h: Lock.t 'a): t 'a
- ensures { h.Lock.defined = result.defined }
- ensures { h.Lock.contents = result.contents }
-
-
-end
-
-
-module Tagtbl
-
- use int.Int
- use import Int63 as Int63
- use map.Map
- use map.Const
- use set.Fset as S
- use list.List
- use list.Mem as LMem
- use import mach.array.Array63 as Array
- use seq.Seq as Seq
- use bool.Bool
- use mach.peano.Peano as Peano
- use mach.peano.Int63 as PeanoInt63
-
-scope Make
- clone S as S with axiom tag_correct
-
- type key = S.key
-
- type t 'a = {
- arr : Array.array 'a;
- ghost mutable contents: map key 'a;
- ghost defined: S.fset key;
- }
- invariant { forall k. S.mem k defined -> S.tag k < Seq.length arr }
- invariant { forall k. S.mem k defined -> Map.([]) contents k = Seq.get arr (S.tag k) }
- by {
- arr = (Array.make 0 (any 'a): Array.array 'a);
- defined = S.empty;
- contents = (const (any 'a): map key 'a);
- }
-
- function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
-
- let create (s:Int63.int63) (def:'a) (ghost defined: S.fset key): t 'a
- requires { forall k. S.mem k defined -> S.tag k <= s }
- requires { -1 <= s < Int63.max_int63 }
- ensures { result.contents = const def }
- ensures { result.defined = defined } =
- {
- arr = Array.make (Int63.(+) s 1) def;
- contents = const def;
- defined = defined;
- }
-
- predicate mem (k: key) (h: t 'a) = S.mem k h.defined
-
- let function max_tags (h: t 'a) : Int63.int63
- ensures { forall k. mem k h -> S.tag k <= result }
- ensures { -1 <= result < Int63.max_int63 }
- =
- Int63.(-) (Array.length h.arr) 1
-
- predicate set_ (h1: t 'a) (h2: t 'a) (k: key) (v: 'a) =
- h1.defined = h2.defined /\ h1.contents = h2.contents[k<-v]
-
- let set (h: t 'a) (k: key) (v: 'a) : unit
- requires { mem k h }
- ensures { set_ h (old h) k v }
- =
- let t = S.tag k in
- h.arr[t] <- v;
- h.contents <- Map.set h.contents k v
-
- function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
-
-
- let function find (h: t 'a) (k: key) : 'a
- requires { mem k h }
- ensures { result = h[k] } =
- let t = S.tag k in
- h.arr[t]
-
- scope Lock
- type t 'a = {
- arr : Array.array 'a;
- ghost contents: map key 'a;
- ghost defined: S.fset key;
- }
- invariant { forall k. S.mem k defined -> S.tag k < Seq.length arr }
- invariant { forall k. S.mem k defined -> Map.([]) contents k = Seq.get arr (S.tag k) }
- by {
- arr = (Array.make 0 (any 'a): Array.array 'a);
- defined = S.empty;
- contents = (const (any 'a): map key 'a);
- }
-
- function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
-
- predicate mem (k: key) (h: t 'a) = S.mem k h.defined
-
- function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
-
-
- let function find (h: t 'a) (k: key) : 'a
- requires { mem k h }
- ensures { result = h[k] } =
- let t = S.tag k in
- h.arr[t]
-
- end
-
- let copy_lock (h: t 'a): Lock.t 'a
- ensures { result.Lock.defined = h.defined }
- ensures { result.Lock.contents = h.contents } =
- { Lock.arr = Array.copy h.arr;
- Lock.contents = h.contents;
- Lock.defined = h.defined;
- }
-
- let copy_unlock (h: Lock.t 'a): t 'a
- ensures { h.Lock.defined = result.defined }
- ensures { h.Lock.contents = result.contents } =
- { arr = Array.copy h.Lock.arr;
- contents = h.Lock.contents;
- defined = h.Lock.defined;
- }
-(*
- clone TagtblIntf with
- type S.key = S.key,
- val S.tag = S.tag,
- lemma S.tag_correct,
- type t = t,
- val create = create,
- val max_tags = max_tags,
- val find = find,
- val set = set,
- type Lock.t = Lock.t,
- val Lock.find = Lock.find
-*)
-end
-end
-
-
-module TagtblBacktrackableIntf
-
- use int.Int
- use import Int63 as Int63
- use map.Map
- use map.Const
- use set.Fset as S
- use list.List
- use list.Mem as LMem
- use import mach.array.Array63 as Array
- use seq.Seq as Seq
- use bool.Bool
- use mach.peano.Peano as Peano
- use mach.peano.Int63 as PeanoInt63
-
- clone import S as S with axiom tag_correct
-
- type token 'a
- function saved_contents (token 'a) : map key 'a
- function saved_tokens (token 'a): list (token 'a)
-
- type t 'a = private {
- ghost mutable contents: map key 'a;
- ghost defined: S.fset key;
- ghost mutable tokens : list (token 'a);
- }
-
- function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
-
- val create (s:Int63.int63) (def:'a) (ghost defined: S.fset key): t 'a
- requires { forall k. S.mem k defined -> tag k <= s }
- requires { -1 <= s < Int63.max_int63 }
- ensures { result.contents = const def }
- ensures { result.tokens = Nil }
- ensures { result.defined = defined }
-
- predicate mem (k: key) (h: t 'a) = S.mem k h.defined
-
- val function max_tags (h: t 'a) : Int63.int63
- ensures { forall k. mem k h -> tag k <= result }
- ensures { -1 <= result < Int63.max_int63 }
-
- predicate set_ (h1: t 'a) (h2: t 'a) (k: key) (v: 'a) =
- h1.defined = h2.defined /\ h1.contents = h2.contents[k<-v]
-
- val partial set (h: t 'a) (k: key) (v: 'a) : unit
- requires { mem k h }
- ensures { set_ h (old h) k v }
- writes { h.contents }
-
- function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
-
- val function find (h: t 'a) (k: key) : 'a
- requires { mem k h }
- ensures { result = h[k] }
-
- val create_backtrack_point (h: t 'a) : token 'a
- writes { h.tokens }
- ensures { result.saved_contents = old h.contents }
- ensures { result.saved_tokens = (old h.tokens) }
- ensures { h.tokens = Cons result (old h.tokens) }
-
-
- val backtrack (h: t 'a) (token:token 'a): unit
- requires { LMem.mem token h.tokens }
- ensures { h.tokens = Cons token token.saved_tokens }
- ensures { h.contents = token.saved_contents }
- writes { h.tokens, h.contents }
-
-end
-
-
-module TagtblBacktrackable
-
- use int.Int
- use import Int63 as Int63
- use map.Map
- use map.Const
- use set.Fset as S
- use list.List
- use list.Mem as LMem
- use import mach.array.Array63 as Array
- use seq.Seq as Seq
- use bool.Bool
- use mach.peano.Peano as Peano
- use mach.peano.Int63 as PeanoInt63
-
-scope Make
- clone S as S with axiom tag_correct
-
- type key = S.key
-
- type token 'a = {
- offset: Int63.int63;
- ghost saved_contents: map key 'a;
- ghost saved_tokens: list (token 'a);
- }
-
-
- type history_item 'a = {
- hist_offset : Int63.int63;
- hist_value : 'a;
- }
-
- predicate good_contents (contents:map key 'a) (arr:Seq.seq 'a) =
- forall e. S.tag e < (Seq.length arr) -> contents[e] = Seq.get arr (S.tag e)
-
- function revert_arr (arr:Seq.seq 'a) (history:Seq.seq (history_item 'a)) (current_offset : int) : Seq.seq 'a =
- let hi = Seq.get history current_offset in
- let arr = Seq.set arr (Int63.to_int hi.hist_offset) hi.hist_value in
- arr
-
-
- let rec ghost function good_tokens
- (arr:Seq.seq 'a) (history:Seq.seq (history_item 'a))
- (current_offset : int)
- (l: list (token 'a)) : bool
- variant { current_offset+1, l }
- =
- match l with
- | Nil -> true
- | Cons t l' ->
- if (current_offset = (Int63.to_int t.offset))
- then begin
- andb (pure {l' = t.saved_tokens})
- (andb (good_contents t.saved_contents arr)
- (good_tokens arr history current_offset l'))
- end
- else begin
- (0 <= current_offset) &&
- let arr = revert_arr arr history current_offset in
- good_tokens arr history (current_offset - 1) l
- end
- end
-
- let rec lemma good_tokens_frame_history
- (arr:Seq.seq 'a) (history1:Seq.seq (history_item 'a))
- (history2:Seq.seq (history_item 'a))
- (current_offset : int)
- (l: list (token 'a)) : unit
- requires { current_offset < Seq.length history1 }
- requires { current_offset < Seq.length history2 }
- requires { forall i. 0 <= i <= current_offset -> Seq.get history1 i = Seq.get history2 i }
- requires { forall i. 0 <= i <= current_offset -> 0 <= (Seq.get history1 i).hist_offset < Seq.length arr }
- requires { good_tokens arr history1 current_offset l }
- variant { current_offset, l }
- ensures { good_tokens arr history2 current_offset l }
- =
- match l with
- | Nil -> ()
- | Cons t l' ->
- if (current_offset = (Int63.to_int t.offset))
- then begin
- assert { l' = t.saved_tokens };
- assert { good_contents t.saved_contents arr };
- assert { good_tokens arr history1 current_offset l' };
- good_tokens_frame_history arr history1 history2 current_offset l'
- end
- else begin
- let arr = revert_arr arr history2 current_offset in
- good_tokens_frame_history arr history1 history2 (current_offset - 1) l
- end
- end
-
- let rec lemma good_tokens_smaller_offset
- (arr:Seq.seq 'a) (history:Seq.seq (history_item 'a))
- (current_offset : int)
- (l: list (token 'a)) : unit
- requires { current_offset < Seq.length history }
- requires { good_tokens arr history current_offset l }
- variant { current_offset, l }
- ensures { forall t. LMem.mem t l -> (Int63.to_int t.offset) <= current_offset }
- =
- match l with
- | Nil -> ()
- | Cons t l' ->
- if (current_offset = (Int63.to_int t.offset))
- then begin
- good_tokens_smaller_offset arr history current_offset l'
- end
- else begin
- let arr = revert_arr arr history current_offset in
- good_tokens_smaller_offset arr history (current_offset - 1) l
- end
- end
-
-
- type t 'a = {
- arr : Array.array 'a;
- ghost mutable contents: map key 'a;
- ghost defined: S.fset key;
- ghost mutable tokens : list (token 'a);
- mutable current_offset: Int63.int63;
- mutable co_peano: Peano.t;
- mutable history: Array.array (history_item 'a);
- }
- invariant { good_contents contents arr }
- invariant { good_tokens arr history current_offset tokens }
- invariant { -1 <= current_offset < Array.length history }
- invariant { 0 < history.length }
- invariant { forall k. S.mem k defined -> S.tag k < Seq.length arr }
- invariant { current_offset = co_peano - 2 }
- invariant { current_offset < Seq.length history }
- invariant { forall i. 0 <= i <= current_offset -> 0 <= (Seq.get history i).hist_offset < arr.length }
- invariant { forall i. 0 <= i <= current_offset -> exists k. (Seq.get history i).hist_offset = S.tag k }
- by {
- arr = (Array.make 0 (any 'a): Array.array 'a);
- history = (Array.make 1 {hist_offset = 0; hist_value = any 'a});
- tokens = Nil;
- current_offset = -1;
- co_peano = Peano.one;
- defined = S.empty;
- contents = (const (any 'a): map key 'a);
- }
-
- function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
-
- let create (s:Int63.int63) (def:'a) (ghost defined: S.fset key): t 'a
- requires { forall k. S.mem k defined -> S.tag k <= s }
- requires { -1 <= s < Int63.max_int63 }
- ensures { result.contents = const def }
- ensures { result.tokens = Nil }
- ensures { result.defined = defined } =
- {
- arr = Array.make (Int63.(+) s 1) def;
- contents = const def;
- tokens = Nil;
- current_offset = -1;
- co_peano = Peano.one;
- defined = defined;
- history = Array.make 8 {hist_offset = 0; hist_value = def};
- }
-
- predicate mem (k: key) (h: t 'a) = S.mem k h.defined
-
- let function max_tags (h: t 'a) : Int63.int63
- ensures { forall k. mem k h -> S.tag k <= result }
- ensures { -1 <= result < Int63.max_int63 }
- =
- Int63.(-) (Array.length h.arr) 1
-
- let resize (h: t 'a) : unit
- writes { h.history }
- ensures { h.current_offset + 1 < Array.length h.history }
- =
- let s = Array.length h.history in
- if h.current_offset + 1 = s then
- let _co_peano = PeanoInt63.to_int63 h.co_peano in
- assert { h.current_offset < _co_peano <= Int63.max_int };
- assert { s < Int63.max_int };
- let s' = if Int63.(/) Int63.max_int 2 < s then Int63.max_int else Int63.(*) s 2 in
- let ndata = Array.make s' (Array.([]) h.history 0) in
- Array.blit h.history 0 ndata 0 s;
- good_tokens_frame_history h.arr.elts h.history.elts ndata.elts (Int63.to_int h.current_offset) h.tokens;
- h.history <- ndata
-
- predicate set_ (h1: t 'a) (h2: t 'a) (k: key) (v: 'a) =
- h1.defined = h2.defined /\ h1.contents = h2.contents[k<-v]
-
- let set (h: t 'a) (k: key) (v: 'a) : unit
- requires { mem k h }
- ensures { set_ h (old h) k v }
- =
- resize h;
- assert { forall i. 0 <= i <= h.current_offset -> 0 <= (Seq.get h.history i).hist_offset < h.arr.length };
- let t = S.tag k in
- let ghost h_before = h.history.elts in
- let ghost arr_before = h.arr.elts in
- let ghost co_before = h.current_offset in
- h.current_offset <- h.current_offset + 1;
- let old_v = (Array.([]) h.arr t) in
-(* assert { 0 <= t < h.arr.length };
- assert { forall i. 0 <= i <= co_before -> 0 <= (Seq.get h.history i).hist_offset < h.arr.length }; *)
- h.history[h.current_offset] <- {hist_offset=t; hist_value=old_v};
-(* assert { forall i. 0 <= i <= co_before -> (Seq.get h.history i).hist_offset = (Seq.get h_before i).hist_offset }; *)
-(* assert { forall i. 0 <= i <= co_before -> 0 <= (Seq.get h.history i).hist_offset < h.arr.length }; *)
- assert { forall i. 0 <= i <= h.current_offset -> 0 <= (Seq.get h.history i).hist_offset < h.arr.length
- by (forall i. 0 <= i <= co_before -> (Seq.get h.history i).hist_offset = (Seq.get h_before i).hist_offset)
- };
- assert { exists k. (Seq.get h.history h.current_offset).hist_offset = S.tag k };
- good_tokens_frame_history h.arr.elts h_before h.history.elts (Int63.to_int h.current_offset - 1) h.tokens;
- assert { exists k. (Seq.get h.history h.current_offset).hist_offset = S.tag k };
- assert { forall i. 0 <= i <= h.current_offset - 1 -> exists k. (Seq.get h.history i).hist_offset = S.tag k };
- h.arr[t] <- v;
- h.contents <- Map.set h.contents k v;
- h.co_peano <- Peano.succ h.co_peano;
- assert { arr_before = Seq.set h.arr.elts (Int63.to_int t) old_v };
- assert { match h.tokens with
- | Nil -> true
- | Cons t _ -> t.offset <= (old h.current_offset)
- end };
- ()
-
- function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
-
-
- let function find (h: t 'a) (k: key) : 'a
- requires { mem k h }
- ensures { result = h[k] } =
- let t = S.tag k in
- h.arr[t]
-
- let create_backtrack_point (h: t 'a) : token 'a
- writes { h.tokens }
- ensures { result.saved_contents = old h.contents }
- ensures { result.saved_tokens = old h.tokens }
- ensures { h.tokens = Cons result (old h.tokens) } =
- let t = { offset = h.current_offset;
- saved_tokens = h.tokens;
- saved_contents = h.contents;
- } in
- h.tokens <- Cons t h.tokens;
- t
-
- predicate backtrack_aux (token : token 'a) (h: t 'a) =
- if token.offset = h.current_offset
- then begin
- good_contents token.saved_contents h.arr
- /\ good_tokens h.arr h.history h.current_offset h.tokens
- /\ Cons token token.saved_tokens = h.tokens
- end
- else begin
- LMem.mem token h.tokens
- /\ (0 <= h.current_offset) /\
- let arr = revert_arr h.arr h.history h.current_offset in
- good_tokens arr h.history (h.current_offset - 1) h.tokens
- end
-
- let backtrack (h: t 'a) (token:token 'a): unit
- requires { LMem.mem token h.tokens }
- ensures { h.tokens = Cons token token.saved_tokens }
- ensures { h.contents = token.saved_contents } =
- let rec aux () : unit
- requires { LMem.mem token h.tokens }
- variant { h.current_offset }
- ensures { h.tokens = Cons token token.saved_tokens }
- ensures { h.contents = token.saved_contents }
- =
- let rec ghost aux' (l: list (token 'a)) : unit
- requires { LMem.mem token l }
- requires { good_tokens h.arr h.history h.current_offset l }
- ensures { backtrack_aux token h }
- variant { l }
- =
- match l with
- | Nil -> absurd
- | Cons t l' ->
- if pure { h.current_offset = t.offset }
- then begin if pure { t = token }
- then h.tokens <- l
- else aux' l'
- end
- else begin
- assert { LMem.mem token l };
- let arr = revert_arr h.arr.elts h.history.elts (Int63.to_int h.current_offset) in
- assert { good_tokens arr h.history (h.current_offset - 1) l };
- h.tokens <- l
- end
- end
- in
- aux' h.tokens;
- if (Int63.(=) h.current_offset token.offset)
- then begin
- h.contents <- token.saved_contents
- end
- else begin
- let hi = Array.([]) h.history h.current_offset in
- Array.([]<-) h.arr hi.hist_offset hi.hist_value;
- let ghost k = any key ensures { hi.hist_offset = S.tag result } in
- h.contents <- Map.set h.contents k hi.hist_value;
- h.current_offset <- h.current_offset - 1;
- h.co_peano <- Peano.pred h.co_peano;
- assert { Map.get h.contents k = Seq.get h.arr (S.tag k) };
- assert { forall e. S.tag e < (Seq.length h.arr) -> Map.get h.contents e = Seq.get h.arr (S.tag e) };
- assert { good_tokens h.arr h.history h.current_offset h.tokens };
- aux ()
- end
- in
- aux ()
-
-
- clone TagtblBacktrackableIntf with
- type S.key = S.key,
- val S.tag = S.tag,
- lemma S.tag_correct,
- type token = token,
- function saved_contents = saved_contents,
- function saved_tokens = saved_tokens,
- type t = t,
- val create = create,
- val max_tags = max_tags,
- val find = find,
- val set = set,
- val create_backtrack_point = create_backtrack_point,
- val backtrack = backtrack
-
-
-end
-end
-
module Var0
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use int.Int
type ti = { vi: Int63.int63 } invariant { 0 <= vi < Int63.max_int63 } by { vi = 1 }
@@ -723,12 +68,12 @@ module Var
use export Var0
- clone TagtblBacktrackableIntf as Hbi with type S.key = ti, val S.tag = tag_ti
- clone TagtblBacktrackableIntf as Hbb with type S.key = tb, val S.tag = tag_tb
+ clone utils.tagtbl.TagtblBacktrackableIntf as Hbi with type S.key = ti, val S.tag = tag_ti
+ clone utils.tagtbl.TagtblBacktrackableIntf as Hbb with type S.key = tb, val S.tag = tag_tb
clone mach.tagset.TagSetIntf as Si with type S.key = ti, val S.tag = tag_ti, val S.dummy = dummy_ti
clone mach.tagset.TagSetIntf as Sb with type S.key = tb, val S.tag = tag_tb, val S.dummy = dummy_tb
- clone TagtblIntf as Hi with type S.key = ti, val S.tag = tag_ti
- clone TagtblIntf as Hb with type S.key = tb, val S.tag = tag_tb
+ clone utils.tagtbl.TagtblIntf as Hi with type S.key = ti, val S.tag = tag_ti
+ clone utils.tagtbl.TagtblIntf as Hb with type S.key = tb, val S.tag = tag_tb
end
@@ -736,12 +81,12 @@ end
module Impl0
use Var0
- clone TagtblBacktrackable as Hbi with type Make.S.key = Var0.ti, val Make.S.tag = Var0.tag_ti
- clone TagtblBacktrackable as Hbb with type Make.S.key = Var0.tb, val Make.S.tag = Var0.tag_tb
+ clone utils.tagtbl.TagtblBacktrackable as Hbi with type Make.S.key = Var0.ti, val Make.S.tag = Var0.tag_ti
+ clone utils.tagtbl.TagtblBacktrackable as Hbb with type Make.S.key = Var0.tb, val Make.S.tag = Var0.tag_tb
clone mach.tagset.TagSet as Si with type S.key = ti, val S.tag = tag_ti, val S.dummy = dummy_ti
clone mach.tagset.TagSet as Sb with type S.key = tb, val S.tag = tag_tb, val S.dummy = dummy_tb
- clone Tagtbl as Hi with type Make.S.key = Var0.ti, val Make.S.tag = Var0.tag_ti
- clone Tagtbl as Hb with type Make.S.key = Var0.tb, val Make.S.tag = Var0.tag_tb
+ clone utils.tagtbl.Tagtbl as Hi with type Make.S.key = Var0.ti, val Make.S.tag = Var0.tag_ti
+ clone utils.tagtbl.Tagtbl as Hb with type Make.S.key = Var0.tb, val Make.S.tag = Var0.tag_tb
end
@@ -815,11 +160,11 @@ module Constraint
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use list.List
use list.Mem as LMem
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use seq.Seq
use mach.array.Array63
@@ -897,12 +242,12 @@ module Engine
clone Dom as DomB with axiom .
clone Constraint as Constraint with type value1 = DomI.value, type value2 = DomB.value, axiom .
use set.Fset as S
- use Bool
+ use utils.extstd.Bool
use list.List
use mach.int.Int
use import Type as Type
use list.Mem as LMem
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ref.Ref
type env = Type.env DomI.t DomB.t
@@ -1407,7 +752,7 @@ end
module DomB
- use Bool
+ use utils.extstd.Bool
use mach.int.Int
use Type
@@ -1490,7 +835,7 @@ end
module DomI
- use Bool
+ use utils.extstd.Bool
use mach.int.Int
use Type
@@ -1561,12 +906,12 @@ module ConstraintHelpers
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
type env = Type.env DomI.t DomB.t
type interp = Type.interp DomI.value DomB.value
@@ -1796,12 +1141,12 @@ module ConstraintCst
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ConstraintHelpers
@@ -1871,12 +1216,12 @@ module ConstraintIsTrue
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ConstraintHelpers
@@ -1934,12 +1279,12 @@ module ConstraintAdd
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ConstraintHelpers
@@ -2077,12 +1422,12 @@ module ConstraintLe
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ConstraintHelpers
@@ -2157,12 +1502,12 @@ module ConstraintOr
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ConstraintHelpers
@@ -2226,12 +1571,12 @@ module ConstraintEquiv
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ConstraintHelpers
@@ -2295,12 +1640,12 @@ module ConstraintNot
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ConstraintHelpers
@@ -2365,12 +1710,12 @@ module ConstraintBoolPresent
use Type
use Var as Var
use mach.int.Int
- use Bool
+ use utils.extstd.Bool
use set.Fset as S
use DomI
use DomB
use seq.Seq as Seq
- use Int63 as Int63
+ use utils.extstd.Int63 as Int63
use ConstraintHelpers
diff --git a/src/lib/dune b/src/lib/dune
index 64ea512384e55422a9883396546f9db5eeabe211..b20899b84d000f5ca8cc9f31a1b15b91d1ef2c8e 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -1,16 +1,16 @@
(library
(public_name colibrics)
- (modules cp__Int63 cp__Bool cp__Impl0 cp__Var0 cp__Type cp__Var cp__DomI cp__DomB constraints__simple__Simple cp__ConstraintIsTrue cp__ConstraintAdd cp__ConstraintLe cp__ConstraintOr cp__ConstraintEquiv cp__ConstraintNot cp__ConstraintBoolPresent cp__ConstraintCst all__All cp__ConstraintHelpers all__API all__APIDefensive colibrics)
+ (modules utils__extstd__Int63 utils__extstd__Bool cp__Impl0 cp__Var0 cp__Type cp__Var cp__DomI cp__DomB constraints__simple__Simple cp__ConstraintIsTrue cp__ConstraintAdd cp__ConstraintLe cp__ConstraintOr cp__ConstraintEquiv cp__ConstraintNot cp__ConstraintBoolPresent cp__ConstraintCst all__All cp__ConstraintHelpers all__API all__APIDefensive colibrics)
(libraries zarith)
(private_modules
- cp__Int63 cp__Bool cp__Impl0 cp__Var0 cp__Type cp__Var cp__DomI cp__DomB constraints__simple__Simple cp__ConstraintIsTrue cp__ConstraintAdd cp__ConstraintLe cp__ConstraintOr cp__ConstraintEquiv cp__ConstraintNot cp__ConstraintBoolPresent cp__ConstraintCst all__All cp__ConstraintHelpers all__API all__APIDefensive)
+ utils__extstd__Int63 utils__extstd__Bool cp__Impl0 cp__Var0 cp__Type cp__Var cp__DomI cp__DomB constraints__simple__Simple cp__ConstraintIsTrue cp__ConstraintAdd cp__ConstraintLe cp__ConstraintOr cp__ConstraintEquiv cp__ConstraintNot cp__ConstraintBoolPresent cp__ConstraintCst all__All cp__ConstraintHelpers all__API all__APIDefensive)
(flags (-w -3))
)
(rule
(deps cp.mlw all.mlw cp.drv constraints/simple.mlw)
- (targets cp__Int63.ml cp__Bool.ml cp__Impl0.ml cp__Var.ml cp__Var0.ml cp__Type.ml cp__DomB.ml cp__DomI.ml constraints__simple__Simple.ml cp__ConstraintIsTrue.ml cp__ConstraintAdd.ml cp__ConstraintLe.ml cp__ConstraintOr.ml cp__ConstraintEquiv.ml cp__ConstraintNot.ml cp__ConstraintBoolPresent.ml cp__ConstraintCst.ml cp__ConstraintHelpers.ml all__All.ml all__API.ml all__APIDefensive.ml)
+ (targets utils__extstd__Int63.ml utils__extstd__Bool.ml cp__Impl0.ml cp__Var.ml cp__Var0.ml cp__Type.ml cp__DomB.ml cp__DomI.ml constraints__simple__Simple.ml cp__ConstraintIsTrue.ml cp__ConstraintAdd.ml cp__ConstraintLe.ml cp__ConstraintOr.ml cp__ConstraintEquiv.ml cp__ConstraintNot.ml cp__ConstraintBoolPresent.ml cp__ConstraintCst.ml cp__ConstraintHelpers.ml all__All.ml all__API.ml all__APIDefensive.ml)
(action (run why3 extract -L . -D ocaml64 -D cp.drv -o . --modular
- cp.Int63 cp.Bool cp.Impl0 cp.Var cp.Var0 cp.Type cp.DomI cp.DomB cp.ConstraintCst cp.ConstraintCst
+ utils.extstd.Int63 utils.extstd.Bool cp.Impl0 cp.Var cp.Var0 cp.Type cp.DomI cp.DomB cp.ConstraintCst cp.ConstraintCst
cp.ConstraintIsTrue cp.ConstraintAdd cp.ConstraintLe cp.ConstraintCst cp.ConstraintOr cp.ConstraintEquiv cp.ConstraintNot cp.ConstraintBoolPresent constraints.simple.Simple cp.ConstraintHelpers all.All all.API all.APIDefensive))
)
diff --git a/src/lib/utils/bool.mlw b/src/lib/utils/bool.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..54534cb9b9f5754cd2d0fcc248cfe17fbf6cfba0
--- /dev/null
+++ b/src/lib/utils/bool.mlw
@@ -0,0 +1,25 @@
+module Bool
+ use export bool.Bool
+
+ let function andb' (x y : bool) : bool
+ ensures { result = (x /\ y) } =
+ match x with
+ | True -> y
+ | False -> False
+ end
+
+ let function eqb (x y:bool) =
+ match x,y with
+ | True, True | False, False -> true
+ | _ -> false
+ end
+end
+
+module Int63
+
+ use export mach.int.Int63
+
+ let function min x y = if x <= y then x else y
+ let function max x y = if x <= y then y else x
+
+end
diff --git a/src/lib/utils/extstd.mlw b/src/lib/utils/extstd.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..54534cb9b9f5754cd2d0fcc248cfe17fbf6cfba0
--- /dev/null
+++ b/src/lib/utils/extstd.mlw
@@ -0,0 +1,25 @@
+module Bool
+ use export bool.Bool
+
+ let function andb' (x y : bool) : bool
+ ensures { result = (x /\ y) } =
+ match x with
+ | True -> y
+ | False -> False
+ end
+
+ let function eqb (x y:bool) =
+ match x,y with
+ | True, True | False, False -> true
+ | _ -> false
+ end
+end
+
+module Int63
+
+ use export mach.int.Int63
+
+ let function min x y = if x <= y then x else y
+ let function max x y = if x <= y then y else x
+
+end
diff --git a/src/lib/utils/tagtbl.mlw b/src/lib/utils/tagtbl.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..94ba8414c7a3e69f155eaf9fee66e32961533a0c
--- /dev/null
+++ b/src/lib/utils/tagtbl.mlw
@@ -0,0 +1,628 @@
+module S
+
+ use int.Int
+ use utils.extstd.Int63 as Int63
+
+ type key
+
+ val function tag (_:key): Int63.int63
+ ensures { 0 <= result }
+
+ axiom tag_correct: forall x y. tag x = tag y -> x = y
+
+end
+
+module TagtblIntf
+
+ use int.Int
+ use import utils.extstd.Int63 as Int63
+ use map.Map
+ use map.Const
+ use set.Fset as S
+ use list.List
+ use list.Mem as LMem
+ use import mach.array.Array63 as Array
+ use seq.Seq as Seq
+ use bool.Bool
+ use mach.peano.Peano as Peano
+ use mach.peano.Int63 as PeanoInt63
+
+ clone import S as S with axiom tag_correct
+
+ type t 'a = private {
+ ghost mutable contents: map key 'a;
+ ghost defined: S.fset key;
+ }
+
+ function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
+
+ val create (s:Int63.int63) (def:'a) (ghost defined: S.fset key): t 'a
+ requires { forall k. S.mem k defined -> tag k <= s }
+ requires { -1 <= s < Int63.max_int63 }
+ ensures { result.contents = const def }
+ ensures { result.defined = defined }
+
+ predicate mem (k: key) (h: t 'a) = S.mem k h.defined
+
+ val function max_tags (h: t 'a) : Int63.int63
+ ensures { forall k. mem k h -> tag k <= result }
+ ensures { -1 <= result < Int63.max_int63 }
+
+ predicate set_ (h1: t 'a) (h2: t 'a) (k: key) (v: 'a) =
+ h1.defined = h2.defined /\ h1.contents = h2.contents[k<-v]
+
+ val set (h: t 'a) (k: key) (v: 'a) : unit
+ requires { mem k h }
+ ensures { set_ h (old h) k v }
+ writes { h.contents }
+
+ function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
+
+ val function find (h: t 'a) (k: key) : 'a
+ requires { mem k h }
+ ensures { result = h[k] }
+
+ scope Lock
+ type t 'a = abstract {
+ contents: map key 'a;
+ defined: S.fset key;
+ }
+
+ function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
+
+ predicate mem (k: key) (h: t 'a) = S.mem k h.defined
+
+ function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
+
+ val function find (h: t 'a) (k: key) : 'a
+ requires { mem k h }
+ ensures { result = h[k] }
+
+ end
+
+ val copy_lock (h: t 'a): Lock.t 'a
+ ensures { result.Lock.defined = h.defined }
+ ensures { result.Lock.contents = h.contents }
+
+ val copy_unlock (h: Lock.t 'a): t 'a
+ ensures { h.Lock.defined = result.defined }
+ ensures { h.Lock.contents = result.contents }
+
+
+end
+
+
+module Tagtbl
+
+ use int.Int
+ use import utils.extstd.Int63 as Int63
+ use map.Map
+ use map.Const
+ use set.Fset as S
+ use list.List
+ use list.Mem as LMem
+ use import mach.array.Array63 as Array
+ use seq.Seq as Seq
+ use bool.Bool
+ use mach.peano.Peano as Peano
+ use mach.peano.Int63 as PeanoInt63
+
+scope Make
+ clone S as S with axiom tag_correct
+
+ type key = S.key
+
+ type t 'a = {
+ arr : Array.array 'a;
+ ghost mutable contents: map key 'a;
+ ghost defined: S.fset key;
+ }
+ invariant { forall k. S.mem k defined -> S.tag k < Seq.length arr }
+ invariant { forall k. S.mem k defined -> Map.([]) contents k = Seq.get arr (S.tag k) }
+ by {
+ arr = (Array.make 0 (any 'a): Array.array 'a);
+ defined = S.empty;
+ contents = (const (any 'a): map key 'a);
+ }
+
+ function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
+
+ let create (s:Int63.int63) (def:'a) (ghost defined: S.fset key): t 'a
+ requires { forall k. S.mem k defined -> S.tag k <= s }
+ requires { -1 <= s < Int63.max_int63 }
+ ensures { result.contents = const def }
+ ensures { result.defined = defined } =
+ {
+ arr = Array.make (Int63.(+) s 1) def;
+ contents = const def;
+ defined = defined;
+ }
+
+ predicate mem (k: key) (h: t 'a) = S.mem k h.defined
+
+ let function max_tags (h: t 'a) : Int63.int63
+ ensures { forall k. mem k h -> S.tag k <= result }
+ ensures { -1 <= result < Int63.max_int63 }
+ =
+ Int63.(-) (Array.length h.arr) 1
+
+ predicate set_ (h1: t 'a) (h2: t 'a) (k: key) (v: 'a) =
+ h1.defined = h2.defined /\ h1.contents = h2.contents[k<-v]
+
+ let set (h: t 'a) (k: key) (v: 'a) : unit
+ requires { mem k h }
+ ensures { set_ h (old h) k v }
+ =
+ let t = S.tag k in
+ h.arr[t] <- v;
+ h.contents <- Map.set h.contents k v
+
+ function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
+
+
+ let function find (h: t 'a) (k: key) : 'a
+ requires { mem k h }
+ ensures { result = h[k] } =
+ let t = S.tag k in
+ h.arr[t]
+
+ scope Lock
+ type t 'a = {
+ arr : Array.array 'a;
+ ghost contents: map key 'a;
+ ghost defined: S.fset key;
+ }
+ invariant { forall k. S.mem k defined -> S.tag k < Seq.length arr }
+ invariant { forall k. S.mem k defined -> Map.([]) contents k = Seq.get arr (S.tag k) }
+ by {
+ arr = (Array.make 0 (any 'a): Array.array 'a);
+ defined = S.empty;
+ contents = (const (any 'a): map key 'a);
+ }
+
+ function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
+
+ predicate mem (k: key) (h: t 'a) = S.mem k h.defined
+
+ function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
+
+
+ let function find (h: t 'a) (k: key) : 'a
+ requires { mem k h }
+ ensures { result = h[k] } =
+ let t = S.tag k in
+ h.arr[t]
+
+ end
+
+ let copy_lock (h: t 'a): Lock.t 'a
+ ensures { result.Lock.defined = h.defined }
+ ensures { result.Lock.contents = h.contents } =
+ { Lock.arr = Array.copy h.arr;
+ Lock.contents = h.contents;
+ Lock.defined = h.defined;
+ }
+
+ let copy_unlock (h: Lock.t 'a): t 'a
+ ensures { h.Lock.defined = result.defined }
+ ensures { h.Lock.contents = result.contents } =
+ { arr = Array.copy h.Lock.arr;
+ contents = h.Lock.contents;
+ defined = h.Lock.defined;
+ }
+(*
+ clone TagtblIntf with
+ type S.key = S.key,
+ val S.tag = S.tag,
+ lemma S.tag_correct,
+ type t = t,
+ val create = create,
+ val max_tags = max_tags,
+ val find = find,
+ val set = set,
+ type Lock.t = Lock.t,
+ val Lock.find = Lock.find
+*)
+end
+end
+
+
+module TagtblBacktrackableIntf
+
+ use int.Int
+ use import utils.extstd.Int63 as Int63
+ use map.Map
+ use map.Const
+ use set.Fset as S
+ use list.List
+ use list.Mem as LMem
+ use import mach.array.Array63 as Array
+ use seq.Seq as Seq
+ use bool.Bool
+ use mach.peano.Peano as Peano
+ use mach.peano.Int63 as PeanoInt63
+
+ clone import S as S with axiom tag_correct
+
+ type token 'a
+ function saved_contents (token 'a) : map key 'a
+ function saved_tokens (token 'a): list (token 'a)
+
+ type t 'a = private {
+ ghost mutable contents: map key 'a;
+ ghost defined: S.fset key;
+ ghost mutable tokens : list (token 'a);
+ }
+
+ function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
+
+ val create (s:Int63.int63) (def:'a) (ghost defined: S.fset key): t 'a
+ requires { forall k. S.mem k defined -> tag k <= s }
+ requires { -1 <= s < Int63.max_int63 }
+ ensures { result.contents = const def }
+ ensures { result.tokens = Nil }
+ ensures { result.defined = defined }
+
+ predicate mem (k: key) (h: t 'a) = S.mem k h.defined
+
+ val function max_tags (h: t 'a) : Int63.int63
+ ensures { forall k. mem k h -> tag k <= result }
+ ensures { -1 <= result < Int63.max_int63 }
+
+ predicate set_ (h1: t 'a) (h2: t 'a) (k: key) (v: 'a) =
+ h1.defined = h2.defined /\ h1.contents = h2.contents[k<-v]
+
+ val partial set (h: t 'a) (k: key) (v: 'a) : unit
+ requires { mem k h }
+ ensures { set_ h (old h) k v }
+ writes { h.contents }
+
+ function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
+
+ val function find (h: t 'a) (k: key) : 'a
+ requires { mem k h }
+ ensures { result = h[k] }
+
+ val create_backtrack_point (h: t 'a) : token 'a
+ writes { h.tokens }
+ ensures { result.saved_contents = old h.contents }
+ ensures { result.saved_tokens = (old h.tokens) }
+ ensures { h.tokens = Cons result (old h.tokens) }
+
+
+ val backtrack (h: t 'a) (token:token 'a): unit
+ requires { LMem.mem token h.tokens }
+ ensures { h.tokens = Cons token token.saved_tokens }
+ ensures { h.contents = token.saved_contents }
+ writes { h.tokens, h.contents }
+
+end
+
+
+module TagtblBacktrackable
+
+ use int.Int
+ use import utils.extstd.Int63 as Int63
+ use map.Map
+ use map.Const
+ use set.Fset as S
+ use list.List
+ use list.Mem as LMem
+ use import mach.array.Array63 as Array
+ use seq.Seq as Seq
+ use bool.Bool
+ use mach.peano.Peano as Peano
+ use mach.peano.Int63 as PeanoInt63
+
+scope Make
+ clone S as S with axiom tag_correct
+
+ type key = S.key
+
+ type token 'a = {
+ offset: Int63.int63;
+ ghost saved_contents: map key 'a;
+ ghost saved_tokens: list (token 'a);
+ }
+
+
+ type history_item 'a = {
+ hist_offset : Int63.int63;
+ hist_value : 'a;
+ }
+
+ predicate good_contents (contents:map key 'a) (arr:Seq.seq 'a) =
+ forall e. S.tag e < (Seq.length arr) -> contents[e] = Seq.get arr (S.tag e)
+
+ function revert_arr (arr:Seq.seq 'a) (history:Seq.seq (history_item 'a)) (current_offset : int) : Seq.seq 'a =
+ let hi = Seq.get history current_offset in
+ let arr = Seq.set arr (Int63.to_int hi.hist_offset) hi.hist_value in
+ arr
+
+
+ let rec ghost function good_tokens
+ (arr:Seq.seq 'a) (history:Seq.seq (history_item 'a))
+ (current_offset : int)
+ (l: list (token 'a)) : bool
+ variant { current_offset+1, l }
+ =
+ match l with
+ | Nil -> true
+ | Cons t l' ->
+ if (current_offset = (Int63.to_int t.offset))
+ then begin
+ andb (pure {l' = t.saved_tokens})
+ (andb (good_contents t.saved_contents arr)
+ (good_tokens arr history current_offset l'))
+ end
+ else begin
+ (0 <= current_offset) &&
+ let arr = revert_arr arr history current_offset in
+ good_tokens arr history (current_offset - 1) l
+ end
+ end
+
+ let rec lemma good_tokens_frame_history
+ (arr:Seq.seq 'a) (history1:Seq.seq (history_item 'a))
+ (history2:Seq.seq (history_item 'a))
+ (current_offset : int)
+ (l: list (token 'a)) : unit
+ requires { current_offset < Seq.length history1 }
+ requires { current_offset < Seq.length history2 }
+ requires { forall i. 0 <= i <= current_offset -> Seq.get history1 i = Seq.get history2 i }
+ requires { forall i. 0 <= i <= current_offset -> 0 <= (Seq.get history1 i).hist_offset < Seq.length arr }
+ requires { good_tokens arr history1 current_offset l }
+ variant { current_offset, l }
+ ensures { good_tokens arr history2 current_offset l }
+ =
+ match l with
+ | Nil -> ()
+ | Cons t l' ->
+ if (current_offset = (Int63.to_int t.offset))
+ then begin
+ assert { l' = t.saved_tokens };
+ assert { good_contents t.saved_contents arr };
+ assert { good_tokens arr history1 current_offset l' };
+ good_tokens_frame_history arr history1 history2 current_offset l'
+ end
+ else begin
+ let arr = revert_arr arr history2 current_offset in
+ good_tokens_frame_history arr history1 history2 (current_offset - 1) l
+ end
+ end
+
+ let rec lemma good_tokens_smaller_offset
+ (arr:Seq.seq 'a) (history:Seq.seq (history_item 'a))
+ (current_offset : int)
+ (l: list (token 'a)) : unit
+ requires { current_offset < Seq.length history }
+ requires { good_tokens arr history current_offset l }
+ variant { current_offset, l }
+ ensures { forall t. LMem.mem t l -> (Int63.to_int t.offset) <= current_offset }
+ =
+ match l with
+ | Nil -> ()
+ | Cons t l' ->
+ if (current_offset = (Int63.to_int t.offset))
+ then begin
+ good_tokens_smaller_offset arr history current_offset l'
+ end
+ else begin
+ let arr = revert_arr arr history current_offset in
+ good_tokens_smaller_offset arr history (current_offset - 1) l
+ end
+ end
+
+
+ type t 'a = {
+ arr : Array.array 'a;
+ ghost mutable contents: map key 'a;
+ ghost defined: S.fset key;
+ ghost mutable tokens : list (token 'a);
+ mutable current_offset: Int63.int63;
+ mutable co_peano: Peano.t;
+ mutable history: Array.array (history_item 'a);
+ }
+ invariant { good_contents contents arr }
+ invariant { good_tokens arr history current_offset tokens }
+ invariant { -1 <= current_offset < Array.length history }
+ invariant { 0 < history.length }
+ invariant { forall k. S.mem k defined -> S.tag k < Seq.length arr }
+ invariant { current_offset = co_peano - 2 }
+ invariant { current_offset < Seq.length history }
+ invariant { forall i. 0 <= i <= current_offset -> 0 <= (Seq.get history i).hist_offset < arr.length }
+ invariant { forall i. 0 <= i <= current_offset -> exists k. (Seq.get history i).hist_offset = S.tag k }
+ by {
+ arr = (Array.make 0 (any 'a): Array.array 'a);
+ history = (Array.make 1 {hist_offset = 0; hist_value = any 'a});
+ tokens = Nil;
+ current_offset = -1;
+ co_peano = Peano.one;
+ defined = S.empty;
+ contents = (const (any 'a): map key 'a);
+ }
+
+ function ([]) (h: t 'a) (k: key) : 'a = Map.([]) h.contents k
+
+ let create (s:Int63.int63) (def:'a) (ghost defined: S.fset key): t 'a
+ requires { forall k. S.mem k defined -> S.tag k <= s }
+ requires { -1 <= s < Int63.max_int63 }
+ ensures { result.contents = const def }
+ ensures { result.tokens = Nil }
+ ensures { result.defined = defined } =
+ {
+ arr = Array.make (Int63.(+) s 1) def;
+ contents = const def;
+ tokens = Nil;
+ current_offset = -1;
+ co_peano = Peano.one;
+ defined = defined;
+ history = Array.make 8 {hist_offset = 0; hist_value = def};
+ }
+
+ predicate mem (k: key) (h: t 'a) = S.mem k h.defined
+
+ let function max_tags (h: t 'a) : Int63.int63
+ ensures { forall k. mem k h -> S.tag k <= result }
+ ensures { -1 <= result < Int63.max_int63 }
+ =
+ Int63.(-) (Array.length h.arr) 1
+
+ let resize (h: t 'a) : unit
+ writes { h.history }
+ ensures { h.current_offset + 1 < Array.length h.history }
+ =
+ let s = Array.length h.history in
+ if h.current_offset + 1 = s then
+ let _co_peano = PeanoInt63.to_int63 h.co_peano in
+ assert { h.current_offset < _co_peano <= Int63.max_int };
+ assert { s < Int63.max_int };
+ let s' = if Int63.(/) Int63.max_int 2 < s then Int63.max_int else Int63.(*) s 2 in
+ let ndata = Array.make s' (Array.([]) h.history 0) in
+ Array.blit h.history 0 ndata 0 s;
+ good_tokens_frame_history h.arr.elts h.history.elts ndata.elts (Int63.to_int h.current_offset) h.tokens;
+ h.history <- ndata
+
+ predicate set_ (h1: t 'a) (h2: t 'a) (k: key) (v: 'a) =
+ h1.defined = h2.defined /\ h1.contents = h2.contents[k<-v]
+
+ let set (h: t 'a) (k: key) (v: 'a) : unit
+ requires { mem k h }
+ ensures { set_ h (old h) k v }
+ =
+ resize h;
+ assert { forall i. 0 <= i <= h.current_offset -> 0 <= (Seq.get h.history i).hist_offset < h.arr.length };
+ let t = S.tag k in
+ let ghost h_before = h.history.elts in
+ let ghost arr_before = h.arr.elts in
+ let ghost co_before = h.current_offset in
+ h.current_offset <- h.current_offset + 1;
+ let old_v = (Array.([]) h.arr t) in
+(* assert { 0 <= t < h.arr.length };
+ assert { forall i. 0 <= i <= co_before -> 0 <= (Seq.get h.history i).hist_offset < h.arr.length }; *)
+ h.history[h.current_offset] <- {hist_offset=t; hist_value=old_v};
+(* assert { forall i. 0 <= i <= co_before -> (Seq.get h.history i).hist_offset = (Seq.get h_before i).hist_offset }; *)
+(* assert { forall i. 0 <= i <= co_before -> 0 <= (Seq.get h.history i).hist_offset < h.arr.length }; *)
+ assert { forall i. 0 <= i <= h.current_offset -> 0 <= (Seq.get h.history i).hist_offset < h.arr.length
+ by (forall i. 0 <= i <= co_before -> (Seq.get h.history i).hist_offset = (Seq.get h_before i).hist_offset)
+ };
+ assert { exists k. (Seq.get h.history h.current_offset).hist_offset = S.tag k };
+ good_tokens_frame_history h.arr.elts h_before h.history.elts (Int63.to_int h.current_offset - 1) h.tokens;
+ assert { exists k. (Seq.get h.history h.current_offset).hist_offset = S.tag k };
+ assert { forall i. 0 <= i <= h.current_offset - 1 -> exists k. (Seq.get h.history i).hist_offset = S.tag k };
+ h.arr[t] <- v;
+ h.contents <- Map.set h.contents k v;
+ h.co_peano <- Peano.succ h.co_peano;
+ assert { arr_before = Seq.set h.arr.elts (Int63.to_int t) old_v };
+ assert { match h.tokens with
+ | Nil -> true
+ | Cons t _ -> t.offset <= (old h.current_offset)
+ end };
+ ()
+
+ function get (h: t 'a) (k: key) : 'a = Map.get h.contents k
+
+
+ let function find (h: t 'a) (k: key) : 'a
+ requires { mem k h }
+ ensures { result = h[k] } =
+ let t = S.tag k in
+ h.arr[t]
+
+ let create_backtrack_point (h: t 'a) : token 'a
+ writes { h.tokens }
+ ensures { result.saved_contents = old h.contents }
+ ensures { result.saved_tokens = old h.tokens }
+ ensures { h.tokens = Cons result (old h.tokens) } =
+ let t = { offset = h.current_offset;
+ saved_tokens = h.tokens;
+ saved_contents = h.contents;
+ } in
+ h.tokens <- Cons t h.tokens;
+ t
+
+ predicate backtrack_aux (token : token 'a) (h: t 'a) =
+ if token.offset = h.current_offset
+ then begin
+ good_contents token.saved_contents h.arr
+ /\ good_tokens h.arr h.history h.current_offset h.tokens
+ /\ Cons token token.saved_tokens = h.tokens
+ end
+ else begin
+ LMem.mem token h.tokens
+ /\ (0 <= h.current_offset) /\
+ let arr = revert_arr h.arr h.history h.current_offset in
+ good_tokens arr h.history (h.current_offset - 1) h.tokens
+ end
+
+ let backtrack (h: t 'a) (token:token 'a): unit
+ requires { LMem.mem token h.tokens }
+ ensures { h.tokens = Cons token token.saved_tokens }
+ ensures { h.contents = token.saved_contents } =
+ let rec aux () : unit
+ requires { LMem.mem token h.tokens }
+ variant { h.current_offset }
+ ensures { h.tokens = Cons token token.saved_tokens }
+ ensures { h.contents = token.saved_contents }
+ =
+ let rec ghost aux' (l: list (token 'a)) : unit
+ requires { LMem.mem token l }
+ requires { good_tokens h.arr h.history h.current_offset l }
+ ensures { backtrack_aux token h }
+ variant { l }
+ =
+ match l with
+ | Nil -> absurd
+ | Cons t l' ->
+ if pure { h.current_offset = t.offset }
+ then begin if pure { t = token }
+ then h.tokens <- l
+ else aux' l'
+ end
+ else begin
+ assert { LMem.mem token l };
+ let arr = revert_arr h.arr.elts h.history.elts (Int63.to_int h.current_offset) in
+ assert { good_tokens arr h.history (h.current_offset - 1) l };
+ h.tokens <- l
+ end
+ end
+ in
+ aux' h.tokens;
+ if (Int63.(=) h.current_offset token.offset)
+ then begin
+ h.contents <- token.saved_contents
+ end
+ else begin
+ let hi = Array.([]) h.history h.current_offset in
+ Array.([]<-) h.arr hi.hist_offset hi.hist_value;
+ let ghost k = any key ensures { hi.hist_offset = S.tag result } in
+ h.contents <- Map.set h.contents k hi.hist_value;
+ h.current_offset <- h.current_offset - 1;
+ h.co_peano <- Peano.pred h.co_peano;
+ assert { Map.get h.contents k = Seq.get h.arr (S.tag k) };
+ assert { forall e. S.tag e < (Seq.length h.arr) -> Map.get h.contents e = Seq.get h.arr (S.tag e) };
+ assert { good_tokens h.arr h.history h.current_offset h.tokens };
+ aux ()
+ end
+ in
+ aux ()
+
+
+ clone TagtblBacktrackableIntf with
+ type S.key = S.key,
+ val S.tag = S.tag,
+ lemma S.tag_correct,
+ type token = token,
+ function saved_contents = saved_contents,
+ function saved_tokens = saved_tokens,
+ type t = t,
+ val create = create,
+ val max_tags = max_tags,
+ val find = find,
+ val set = set,
+ val create_backtrack_point = create_backtrack_point,
+ val backtrack = backtrack
+
+
+end
+end