diff --git a/bench/typing/bad/clone_record1.mlw b/bench/typing/bad/clone_record1.mlw index 9b6c7cf1dd34e4b569221dba0cb1931f0bb7c874..6866e352c29133a6a01572bfae3d108e6fcb82ae 100644 --- a/bench/typing/bad/clone_record1.mlw +++ b/bench/typing/bad/clone_record1.mlw @@ -5,5 +5,5 @@ end module M type t = { a: bool } (* bad type for a *) - clone S with type t = t + clone import S with type t = t end diff --git a/bench/typing/bad/clone_record2.mlw b/bench/typing/bad/clone_record2.mlw index 982a2200db6a0cbded63ab9dbd1c62cb6e6b9c0b..edb994de3ff3e152085efbf8aa591d3f243f9b27 100644 --- a/bench/typing/bad/clone_record2.mlw +++ b/bench/typing/bad/clone_record2.mlw @@ -5,5 +5,5 @@ end module M type t = { b: int } (* no field a *) - clone S with type t = t + clone import S with type t = t end diff --git a/bench/typing/bad/unbound_theory1.why b/bench/typing/bad/unbound_theory1.why index fec678397c81ec30e2bcce9e19b3451155d72111..d08dfeaf0b16e7ac7ab7c72dbdb0070f5175b8ac 100644 --- a/bench/typing/bad/unbound_theory1.why +++ b/bench/typing/bad/unbound_theory1.why @@ -1 +1 @@ -theory A use B end +theory A use export B end diff --git a/bench/typing/good/already_theory1.why b/bench/typing/good/already_theory1.why index f8cca2e7b899b06d3239e9b4c2e2917828788b18..6c4cc38204aa3b4bcbb27ded7b20e9aecfe17399 100644 --- a/bench/typing/good/already_theory1.why +++ b/bench/typing/good/already_theory1.why @@ -1,2 +1,2 @@ theory A end -theory B use A use A end +theory B use import A use import A end diff --git a/bench/typing/good/already_theory2.why b/bench/typing/good/already_theory2.why index 677560225b1adafdcedcdca8c29cc65ad8e9c6a0..4a0b46b19c298b0b8b855b3da5f8e28e375a08f9 100644 --- a/bench/typing/good/already_theory2.why +++ b/bench/typing/good/already_theory2.why @@ -1,3 +1,3 @@ theory A end theory B end -theory C use A use B as A end +theory C use A as A use B as A end diff --git a/bench/typing/good/clash_namespace1.why b/bench/typing/good/clash_namespace1.why index c0c5ae330b3f52fecee8ed571049d9572f07ea45..1bb07ddab1f28f2af0f141b1ef54e754102af625 100644 --- a/bench/typing/good/clash_namespace1.why +++ b/bench/typing/good/clash_namespace1.why @@ -7,7 +7,7 @@ theory A end theory B - use A - use A + use A as A + use A as A end diff --git a/bench/typing/good/uses1.why b/bench/typing/good/uses1.why index 956c45a47ee4a579e78777db58f442b170c9f482..d3518d642e342f04ef5343d8d03ff25edf3204a1 100644 --- a/bench/typing/good/uses1.why +++ b/bench/typing/good/uses1.why @@ -3,5 +3,5 @@ theory A end theory B - use A + use A as A end diff --git a/examples/WP_revisited/blocking_semantics5.mlw b/examples/WP_revisited/blocking_semantics5.mlw index 1fa79a785ec1229f55724038898c7e675c433783..16b401ef5a4a90ba7c78a711df3db94d42b2d174 100644 --- a/examples/WP_revisited/blocking_semantics5.mlw +++ b/examples/WP_revisited/blocking_semantics5.mlw @@ -202,7 +202,7 @@ end theory TestSemantics use import SemOp -use map.Const +use import map.Const function my_sigma : env = Const.const (Vint 0) constant x : ident diff --git a/examples/WP_revisited/formula.why b/examples/WP_revisited/formula.why index 453103990d6cfbadc5f0c360ea1ec9ce1b1e864b..9ced9d6391b958d7dfcb6f5cebef78314e507e20 100644 --- a/examples/WP_revisited/formula.why +++ b/examples/WP_revisited/formula.why @@ -44,7 +44,7 @@ function eval (f:prop_fmla) (v:idmap bool) : bool = end - use map.Const + use import map.Const goal Test1 : let x = mk_ident 0 in diff --git a/examples/WP_revisited/imp_n.why b/examples/WP_revisited/imp_n.why index 250ee60eed5145846063d4794274d72d22a0e5d2..7a1bbce4ad346273049e7c39a504be7553edeb30 100644 --- a/examples/WP_revisited/imp_n.why +++ b/examples/WP_revisited/imp_n.why @@ -56,7 +56,7 @@ function eval_expr (s:state) (e:expr) : int = eval_bin (eval_expr s e1) op (eval_expr s e2) end - use map.Const + use import map.Const goal Test13 : let s = Const.const 0 in diff --git a/examples/WP_revisited/wp2.mlw b/examples/WP_revisited/wp2.mlw index 9a41b222cb846699a4e5bfc2f2e4e5e7349a5535..98a65c223fa7825ca434794777af1c97b9782602 100644 --- a/examples/WP_revisited/wp2.mlw +++ b/examples/WP_revisited/wp2.mlw @@ -262,7 +262,7 @@ end theory TestSemantics use import Imp -use map.Const +use import map.Const function my_sigma : env = Const.const (Vint 0) function my_pi : env = Const.const (Vint 42) @@ -425,7 +425,7 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) = eval_fmla sigma' pi' result } - use HoareLogic + use import HoareLogic let rec wp (i:stmt) (q:fmla) ensures { valid_triple result i q } diff --git a/examples/bag.mlw b/examples/bag.mlw index bd22065a386a61731b74d8032bb773afee17d14c..2eba6f80c0b9a57d5009db2c7a15bef1b48e03a0 100644 --- a/examples/bag.mlw +++ b/examples/bag.mlw @@ -49,7 +49,7 @@ module ResizableArraySpec use import int.Int use import map.Map - use map.Const + use import map.Const type rarray 'a = private { ghost mutable len: int; @@ -93,9 +93,9 @@ module BagImpl use import int.Int use import Bag use import ResizableArraySpec as R - use map.Map - use int.NumOf - use null.Null + use map.Map as Map + use int.NumOf as NumOf + use null.Null as Null function numof (r: rarray (Null.t 'a)) (x: 'a) (l u: int) : int = NumOf.numof (fun i -> (Map.get r.R.data i).Null.v = Null.Value x) l u @@ -164,7 +164,7 @@ module BagImpl resize t.data n; t.size <- n - clone BagSpec with + clone import BagSpec with type t = t, val create = create, val clear = clear, diff --git a/examples/bellman_ford.mlw b/examples/bellman_ford.mlw index 5aa1ce9888a4761a9e61ac447c2611b439593739..cdb4b98f52aa7aa80f54f2824bafa3ee5993f996 100644 --- a/examples/bellman_ford.mlw +++ b/examples/bellman_ford.mlw @@ -9,7 +9,6 @@ theory Graph use export list.List use export list.Append use export list.Length - use list.Mem use export int.Int use export set.Fset @@ -61,7 +60,7 @@ theory Graph Two cases depending on l3=[] (and thus u=v) conclude the proof. Qed. *) - clone pigeon.ListAndSet with type t = vertex + clone import pigeon.ListAndSet with type t = vertex predicate cyc_decomp (v: vertex) (l: list vertex) (vi: vertex) (l1 l2 l3: list vertex) = diff --git a/examples/binary_sqrt.mlw b/examples/binary_sqrt.mlw index 8d8ed78ab851456ff327c557d8ec8b557190993d..7349b561fd13b1b71630643ed6030a21f7c91dcd 100644 --- a/examples/binary_sqrt.mlw +++ b/examples/binary_sqrt.mlw @@ -8,10 +8,10 @@ module BinarySqrt use import real.Real - use int.Int - use real.MinMax - use real.FromInt - use real.Truncate + use int.Int as Int + use real.MinMax as MinMax + use real.FromInt as FromInt + use real.Truncate as Truncate let rec sqrt (r: real) (eps: real) (ghost n:int) (ghost eps0:real) : real requires { 0.0 <= r } diff --git a/examples/binomial_heap.mlw b/examples/binomial_heap.mlw index 5d1b6c46e0886fd8c8138e3cefe6a3c15ef2fffa..a939d51537cff1c4fd3ab70784318360e8680e36 100644 --- a/examples/binomial_heap.mlw +++ b/examples/binomial_heap.mlw @@ -20,7 +20,7 @@ module BinomialHeap type elt val predicate le elt elt - clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . (** Trees. diff --git a/examples/bitcount.mlw b/examples/bitcount.mlw index 4b7fc8a8002a92c7db23a5b042941fbdcb42afd0..7fcc8ce8f3db70d74000219cb138d16bacce9ffc 100644 --- a/examples/bitcount.mlw +++ b/examples/bitcount.mlw @@ -18,7 +18,7 @@ module BitCount8bit_fact lemma nth_as_bv_is_int : forall a i. t'int (nth_as_bv a i) = nth_as_int a (t'int i) - use import int.EuclideanDivision + use import int.EuclideanDivision let ghost step1 (n x1 : t) (i : int) : unit requires { 0 <= i < 4 } @@ -390,7 +390,7 @@ module AsciiCode odd number of changes on a valid ascii character, the result will be invalid, hence the validity of the encoding. *) - use Hamming + use import Hamming let rec lemma tmp (a b : t) (i j : int) requires { i < j } diff --git a/examples/bitvector_examples.mlw b/examples/bitvector_examples.mlw index 1751add631dce801c9052e617981fa20f724811d..a1d6bddc84312198abeffb4c3227311c0f323e4d 100644 --- a/examples/bitvector_examples.mlw +++ b/examples/bitvector_examples.mlw @@ -22,8 +22,8 @@ module Test_proofinuse (* Mask example --------------------- *) - use bv.BV8 - use bv.BV64 + use bv.BV8 as BV8 + use bv.BV64 as BV64 use bv.BVConverter_32_64 as C32_46 use bv.BVConverter_8_32 as C8_32 diff --git a/examples/bitvectors/bitvector.why b/examples/bitvectors/bitvector.why index f907ef0aaf769257df9d37816a4e173f191db472..29684404562b11c6ffbab116ed36c7a9f55c93a7 100644 --- a/examples/bitvectors/bitvector.why +++ b/examples/bitvectors/bitvector.why @@ -375,8 +375,8 @@ theory BV32_64 use import int.Int - use BV32 - use BV64 + use BV32 as BV32 + use BV64 as BV64 function concat BV32.bv BV32.bv : BV64.bv diff --git a/examples/bitvectors/double_of_int.why b/examples/bitvectors/double_of_int.why index ae8d516c4603144658f4b30055f3bf6541cc86aa..82ed5b3e6afcf1959392ae1b32ea29b75104b989 100644 --- a/examples/bitvectors/double_of_int.why +++ b/examples/bitvectors/double_of_int.why @@ -7,11 +7,11 @@ theory DoubleOfInt use import real.RealInfix use import real.FromInt - use power2.Pow2int - use power2.Pow2real - use bitvector.BV32 - use bitvector.BV64 - use bitvector.BV32_64 + use power2.Pow2int as Pow2int + use power2.Pow2real as Pow2real + use bitvector.BV32 as BV32 + use bitvector.BV64 as BV64 + use bitvector.BV32_64 as BV32_64 use import double.BV_double (*********************************************************************) diff --git a/examples/bitvectors/power2.why b/examples/bitvectors/power2.why index dd0532ad98c26c21980e4b3229dc20a1511aa1e9..a02a0ab6daad0f89dbd5a45c1bc596ea331ced06 100644 --- a/examples/bitvectors/power2.why +++ b/examples/bitvectors/power2.why @@ -143,16 +143,10 @@ theory Pow2real lemma Power_sum : forall n m: int. pow2 (n+m) = pow2 n *. pow2 m - use Pow2int + use Pow2int as P2I use import real.FromInt lemma Pow2_int_real: - forall x:int. x >= 0 -> pow2 x = from_int (Pow2int.pow2 x) + forall x:int. x >= 0 -> pow2 x = from_int (P2I.pow2 x) end - -(* -Local Variables: -compile-command: "why3 ide power2.why" -End: -*) diff --git a/examples/braun_trees.mlw b/examples/braun_trees.mlw index 549f3df352ccdea7cb5c4184ba219bbfbb587a06..da1f76075e516bd977447f8733e048cde7cc9294 100644 --- a/examples/braun_trees.mlw +++ b/examples/braun_trees.mlw @@ -26,7 +26,7 @@ module BraunHeaps val predicate le elt elt - clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . (* [e] is no greater than the root of [t], if any *) let predicate le_root (e: elt) (t: tree elt) = match t with diff --git a/examples/bts/13002.why b/examples/bts/13002.why index 421ee66366c9d4e03c8ddb46784720324efab1a8..a250f2d1d3fcaa62efe60e9bececa02acf132a56 100644 --- a/examples/bts/13002.why +++ b/examples/bts/13002.why @@ -1,4 +1,4 @@ theory T -use real.Real +use import real.Real goal toto: true end diff --git a/examples/bts/17184.mlw b/examples/bts/17184.mlw index d01b0dfffcbd65193a9b0cefc76ed1805df75387..c6e1d0062f6c902d6ce9f9d57786255db2b95805 100644 --- a/examples/bts/17184.mlw +++ b/examples/bts/17184.mlw @@ -21,7 +21,7 @@ module B type t = { ghost a : unit } - clone A with type t = t + clone export A with type t = t (* FIXME ! let sub (x:t) : unit = A.add x diff --git a/examples/bts/20445.mlw b/examples/bts/20445.mlw index 2c2d9d15e2503e315d9734839f3ce7da8e7dad63..8784a8022eb0160a201de18778f991c573fbcd3a 100644 --- a/examples/bts/20445.mlw +++ b/examples/bts/20445.mlw @@ -5,5 +5,5 @@ end module B goal G : false -clone A with goal G -end \ No newline at end of file +clone A as A with goal G +end diff --git a/examples/bts/79_compute_unsound.mlw b/examples/bts/79_compute_unsound.mlw index 363f55e8d4d2be09e3297506a3b94724f520a34a..5494d86e1c636885bbbd3ddd3ee73475de6a515d 100644 --- a/examples/bts/79_compute_unsound.mlw +++ b/examples/bts/79_compute_unsound.mlw @@ -1,6 +1,5 @@ module Soundness use import int.Int - use HighOrd function f0 (x y z:int) : int = x * y + z predicate p (f:int -> int) = diff --git a/examples/check-builtin/ac.why b/examples/check-builtin/ac.why index c6b9b2d479d4278d28e19beee93ddede7c7f37b2..366b3c82797c5c7c72185dcc5af7aa8c73c360b1 100644 --- a/examples/check-builtin/ac.why +++ b/examples/check-builtin/ac.why @@ -1,7 +1,7 @@ theory Test type t function f t t : t - clone algebra.AC with type t = t, function op = f, axiom . + clone import algebra.AC with type t = t, function op = f, axiom . goal G1 : forall x y : t. f x y = f y x goal G2 : forall x y z : t. f (f x y) z = f x (f y z) end diff --git a/examples/check-builtin/floats.why b/examples/check-builtin/floats.why index e3fa4d3d0115c3ecf9a4ed3b41bc8c494aca139c..78286390484bf0fcaa3cde83873e8a4b5e56b9f9 100644 --- a/examples/check-builtin/floats.why +++ b/examples/check-builtin/floats.why @@ -5,7 +5,7 @@ theory TestGappa use import real.Abs use import real.Square use import floating_point.Rounding - use floating_point.Single + use floating_point.Single as Single use import floating_point.Double goal Round_single_01: diff --git a/examples/cursor_examples.mlw b/examples/cursor_examples.mlw index 2ac0226bfd42f8759b7a1876e3b07a060b6ccffc..1994eaa3f0b0a15adce476a8d7b04c6b720aee58 100644 --- a/examples/cursor_examples.mlw +++ b/examples/cursor_examples.mlw @@ -85,7 +85,7 @@ module ListCursorImpl (* : ListCursor *) ensures { result.to_visit = t } = { visited = empty; collection = t; to_visit = t } - clone cursor.ListCursor with + clone import cursor.ListCursor with type cursor = cursor, val create = create, val C.has_next = has_next, @@ -187,7 +187,7 @@ module ArrayCursorImpl (* : ArrayCursor *) c.index <- c.index + 1; x end - clone cursor.ArrayCursor with + clone import cursor.ArrayCursor with type cursor = cursor, val C.next = next, val C.has_next = has_next, @@ -246,4 +246,4 @@ module TestArrayCursorLink val ArrayCursor.C.has_next = has_next, val ArrayCursor.create = create -end \ No newline at end of file +end diff --git a/examples/defunctionalization.mlw b/examples/defunctionalization.mlw index 85607cb219b0fcc0a2045d29749f4adcc2dba053..8b91469ad5b8b8a5cfef8359bc70bb96722e6049 100644 --- a/examples/defunctionalization.mlw +++ b/examples/defunctionalization.mlw @@ -675,12 +675,12 @@ function size_e (e:expr) : int = lemma size_e_pos: forall e: expr. size_e e >= 1 -use Defunctionalization +use Defunctionalization as D function size_c (c:cont) : int = match c with | I -> 0 - | A e2 k -> 2 + Defunctionalization.size_e e2 + size_c k + | A e2 k -> 2 + D.size_e e2 + size_c k | B _ k -> 1 + size_c k end @@ -698,7 +698,7 @@ let rec continue_4 (c:cont) (v:int) : value end with eval_4 (e:expr) (c:cont) : value - variant { size_c c + Defunctionalization.size_e e } + variant { size_c c + D.size_e e } ensures { eval_cont c (eval_0 e) result } = match e with @@ -886,9 +886,9 @@ predicate is_empty_context (c:context) = end -use Defunctionalization (* for size_e *) +use Defunctionalization as D (* for size_e *) -function size_e (e:expr) : int = Defunctionalization.size_e e +function size_e (e:expr) : int = D.size_e e function size_c (c:context) : int = match c with @@ -1099,9 +1099,9 @@ use import SemWithError type context = Empty | Left context expr | Right int context -use Defunctionalization (* for size_e *) +use Defunctionalization as D (* for size_e *) -function size_e (e:expr) : int = Defunctionalization.size_e e +function size_e (e:expr) : int = D.size_e e function size_c (c:context) : int = match c with diff --git a/examples/euler001.mlw b/examples/euler001.mlw index 11c780bc792c9888b25d728a88da9ca2218f93f7..c952bb805a1368a8a60514e2ff05f583e50490a4 100644 --- a/examples/euler001.mlw +++ b/examples/euler001.mlw @@ -60,7 +60,7 @@ theory TriangularNumbers use import int.Int use import int.ComputerDivision use import int.Div2 - use DivModHints + use DivModHints as DMH lemma tr_mod_2: forall n:int. n >= 0 -> mod (n*(n+1)) 2 = 0 @@ -105,8 +105,7 @@ theory SumMultiple predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula_aux n - use DivModHints - use TriangularNumbers + use DivModHints as DMH lemma mod_15: forall n:int. diff --git a/examples/foveoos11-cm/tree_max.mlw b/examples/foveoos11-cm/tree_max.mlw index 4bcabdd870665eeb8ab7acf9ed8639eed6367d6c..46c515b654305522742178dff1aebee81a2abf0f 100644 --- a/examples/foveoos11-cm/tree_max.mlw +++ b/examples/foveoos11-cm/tree_max.mlw @@ -52,7 +52,7 @@ end module TreeMax use import int.Int - use int.MinMax + use import int.MinMax use import BinTree let rec max_aux (t:tree) (acc:int) variant {t} diff --git a/examples/gcd.mlw b/examples/gcd.mlw index c5acaa90a6cae0b75bd17303c4ec411bc40574e0..086458067e3004297064873d529da493e76f62aa 100644 --- a/examples/gcd.mlw +++ b/examples/gcd.mlw @@ -52,7 +52,7 @@ module BinaryGcd lemma odd1: forall n: int. 0 <= n -> not (even n) <-> n = 2 * div n 2 + 1 lemma div_nonneg: forall n: int. 0 <= n -> 0 <= div n 2 - use number.Coprime + use import number.Coprime lemma gcd_even_even: forall u v: int. 0 <= v -> 0 <= u -> gcd (2 * u) (2 * v) = 2 * gcd u v diff --git a/examples/gcd_vc_sp.mlw b/examples/gcd_vc_sp.mlw index 315a604cb648491a92e8a13f16800c03d959d564..c826d35209a190482bb2d81b7ac4d3efa15decee 100644 --- a/examples/gcd_vc_sp.mlw +++ b/examples/gcd_vc_sp.mlw @@ -52,7 +52,7 @@ module BinaryGcd lemma odd1: forall n: int. 0 <= n -> not (even n) <-> n = 2 * div n 2 + 1 lemma div_nonneg: forall n: int. 0 <= n -> 0 <= div n 2 - use number.Coprime + use import number.Coprime lemma gcd_even_even: forall u v: int. 0 <= v -> 0 <= u -> gcd (2 * u) (2 * v) = 2 * gcd u v diff --git a/examples/hashtbl_impl.mlw b/examples/hashtbl_impl.mlw index 716f94a63c48262fe70f657f39990541d8b59114..277f77117afb27ad4d5461e722e350fcd4c90016 100644 --- a/examples/hashtbl_impl.mlw +++ b/examples/hashtbl_impl.mlw @@ -12,7 +12,7 @@ module HashtblImpl use import list.List use import list.Mem use import map.Map - use map.Const + use import map.Const use import array.Array type key diff --git a/examples/hillel_challenge.mlw b/examples/hillel_challenge.mlw index c288679a537369f763f8a9552c271803f9ec75e3..49a7d5de9bb7cd2e1ee3251a1a1031e2c919506f 100644 --- a/examples/hillel_challenge.mlw +++ b/examples/hillel_challenge.mlw @@ -55,20 +55,20 @@ module Unique use import int.Int use import ref.Refint - clone hashtbl.Hashtbl with type key = int + clone hashtbl.Hashtbl as H with type key = int use import array.Array predicate mem (x: int) (a: array int) (i: int) = exists j. 0 <= j < i /\ a[j] = x - predicate hmem (x: int) (h: Hashtbl.t unit) = - Hashtbl.contents h x <> Hashtbl.List.Nil + predicate hmem (x: int) (h: H.t unit) = + H.contents h x <> H.List.Nil let unique (a: array int) : array int ensures { forall x. mem x result (length result) <-> mem x a (length a) } ensures { forall i j. 0 <= i < j < length result -> result[i] <> result[j] } = let n = length a in - let h = Hashtbl.create n in + let h = H.create n in let res = Array.make n 0 in let len = ref 0 in for i = 0 to n - 1 do @@ -76,8 +76,8 @@ module Unique invariant { forall x. mem x a i <-> hmem x h } invariant { forall x. mem x a i <-> mem x res !len } invariant { forall i j. 0 <= i < j < !len -> res[i]<>res[j] } - if not (Hashtbl.mem h a[i]) then begin - Hashtbl.add h a[i] (); + if not (H.mem h a[i]) then begin + H.add h a[i] (); res[!len] <- a[i]; incr len end diff --git a/examples/in_progress/2wp_gen/base.mlw b/examples/in_progress/2wp_gen/base.mlw index 9f15699f90b25133c83c92c1ff41dc1083508d14..e65684558c1ca1482b7d783712a8b8ceaa0bac0c 100644 --- a/examples/in_progress/2wp_gen/base.mlw +++ b/examples/in_progress/2wp_gen/base.mlw @@ -2,8 +2,6 @@ (* Basic arrow definitions *) module Fun - use export HighOrd - predicate ext (f g:'a -> 'b) = forall x. f x = g x predicate equalizer (a:'a -> bool) (f g:'a -> 'b) = forall x. a x -> f x = g x diff --git a/examples/in_progress/alphaBeta.mlw b/examples/in_progress/alphaBeta.mlw index d8c37e41f88d2acfce295a531e39a644921e50b9..4c1151386fd810f339f01e29df88c8c3777f6e44 100644 --- a/examples/in_progress/alphaBeta.mlw +++ b/examples/in_progress/alphaBeta.mlw @@ -61,8 +61,8 @@ theory TwoPlayerGame type elt = move, function cost = cost - use list.Elements - use set.Fset + use import list.Elements + use import set.Fset axiom minmax_depth_non_zero: forall p:position, n:int. n > 0 -> @@ -71,7 +71,7 @@ theory TwoPlayerGame if Fset.is_empty moves then position_value p else - MinMaxRec.min (p,n-1) moves - use list.Mem + use import list.Mem goal Test: forall p:position, m:move. @@ -103,8 +103,8 @@ module AlphaBeta use TwoPlayerGame as G use import list.List - use list.Elements - use set.Fset + use import list.Elements + use import set.Fset let rec move_value_alpha_beta alpha beta pos depth move = requires { depth >= 1 } diff --git a/examples/in_progress/avl/association_list.mlw b/examples/in_progress/avl/association_list.mlw index 19ae4be1d6f8fa6429795dcf01302aad43284fc2..6b1edaaea3ecb3c5859a2b5e115154358094a8bd 100644 --- a/examples/in_progress/avl/association_list.mlw +++ b/examples/in_progress/avl/association_list.mlw @@ -3,46 +3,45 @@ (* Association with respect to an equivalence relation. *) module Assoc - + clone import key_type.KeyType as K clone import relations_params.EquivalenceParam as Eq with type t = key - + use import list.List use import list.Mem use import list.Append use import option.Option - use import HighOrd - + predicate appear (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) = exists x. mem x l /\ correct_for p k /\ Eq.rel p k (key x) - + lemma appear_append : forall p:param 'a,k:key 'a,l r:list (t 'a 'b). appear p k (l++r) <-> appear p k l \/ appear p k r - + (* Correction. *) predicate correct (p:param 'a) (l:list (t 'a 'b)) = forall x. mem x l -> let kx = key x in correct_for p kx - + (* Unique occurence (a desirable property of an association list). *) predicate unique (p:param 'a) (l:list (t 'a 'b)) = match l with | Nil -> true | Cons x q -> not appear p (key x) q /\ unique p q end - + (* functional update with equivalence classes. *) function param_update (p:param 'a) (f:key 'a -> 'b) (k:key 'a) (b:'b) : key 'a -> 'b = \k2. if Eq.rel p k k2 then b else f k2 - + function const_none : 'a -> option 'b = \x.None - + (* functional model of an association list. *) function model (p:param 'a) (l:list (t 'a 'b)) : key 'a -> option (t 'a 'b) = match l with | Nil -> const_none | Cons d q -> param_update p (model p q) (key d) (Some d) end - + (* A key is bound iff it occurs in the association lists. *) let rec lemma model_occurence (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit @@ -53,7 +52,7 @@ module Assoc ensures { not appear p k l <-> model p l k = None } variant { l } = match l with Cons _ q -> model_occurence p k q | _ -> () end - + (* A key is bound to a value with an equivalent key. *) let rec lemma model_link (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit requires { correct p l } @@ -62,7 +61,7 @@ module Assoc | Some d -> Eq.rel p k (key d) end } variant { l } = match l with Cons _ q -> model_link p k q | _ -> () end - + (* Two equivalent keys are bound to the same value. *) let rec lemma model_equal (p:param 'a) (k1 k2:key 'a) (l:list (t 'a 'b)) : unit @@ -76,7 +75,7 @@ module Assoc model_equal p k1 k2 q | _ -> () end - + (* If the list satisfies the uniqueness property, then every value occuring in the list is the image of its key. *) let rec lemma model_unique (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit @@ -86,7 +85,7 @@ module Assoc ensures { forall d. mem d l -> model p l (key d) = Some d } variant { l } = match l with Cons _ q -> model_unique p k q | _ -> () end - + (* Singleton association list. *) let lemma model_singleton (p:param 'a) (k:key 'a) (d:t 'a 'b) : unit requires { correct_for p d.key } @@ -95,7 +94,7 @@ module Assoc then Some d else None } = () - + (* Unique union of association list by concatenation. *) let rec lemma model_concat (p:param 'a) (k:key 'a) (l r:list (t 'a 'b)) : unit requires { correct p (l++r) /\ correct p l /\ correct p r } @@ -116,19 +115,19 @@ module Assoc && false }; model_concat p k q r end - + end (* Sorted (increasing) association list. *) module AssocSorted - + use import list.List use import list.Append use import list.Mem use import option.Option - + clone import key_type.KeyType as K clone import preorder.FullParam as O with type t = key clone export Assoc with namespace K = K, @@ -144,7 +143,7 @@ module AssocSorted predicate O.correct_for = O.correct_for, predicate O.rel = O.lt, goal O.trans - + (* Sorted lists are correct association lists with unicity property. *) let rec lemma increasing_unique_and_correct (o:order 'a) (l:list (t 'a 'b)) : unit @@ -153,7 +152,7 @@ module AssocSorted ensures { unique o l } variant { l } = match l with Cons _ q -> increasing_unique_and_correct o q | _ -> () end - + let lemma model_cut (o:order 'a) (k:key 'a) (l r:list (t 'a 'b)) : unit requires { correct_for o k } requires { S.increasing o r } @@ -187,7 +186,7 @@ module AssocSorted end && false | _ -> false end && false } - + let lemma model_split (o:order 'a) (d:t 'a 'b) (l r:list (t 'a 'b)) : unit requires { correct_for o d.key } requires { S.increasing o l } @@ -205,6 +204,6 @@ module AssocSorted ensures { forall k2. correct_for o k2 /\ le o d.key k2 -> model o l k2 = None } = () - + end diff --git a/examples/in_progress/avl/avl.mlw b/examples/in_progress/avl/avl.mlw index 3584a5bdeef0b1b734e04cd8bec347eac928c6e4..eb972b806795fb82c13449fc9599bf8b0b98cad2 100644 --- a/examples/in_progress/avl/avl.mlw +++ b/examples/in_progress/avl/avl.mlw @@ -1,20 +1,19 @@ (* Part factorized out (without parameters). *) module Base - + use import int.Int use import bool.Bool use import list.Append use import list.Length - use import HighOrd use import program_type.TypeParams - + (* tree representation. The two integer parameters corresponds to height and size of the tree, stored at every node. *) type tree 'a = | Empty | Node (tree 'a) 'a (tree 'a) int int - + (* Model of an avl. Intended to expose: - The list representation. - The height. *) @@ -22,30 +21,30 @@ module Base lis : list 'b; hgt : int; } - + (* Shortcut. *) function node_model (l:list 'a) (d:'a) (r:list 'a) : list 'a = l ++ Cons d r - + (* list obtained from a tree by infix traversal + model mapping. *) function list_model (f:'a -> 'b) (t:tree 'a) : list 'b = match t with | Empty -> Nil | Node l d r _ _ -> node_model (list_model f l) (f d) (list_model f r) end - + (* Height of the tree. *) function real_height (t:tree 'a) : int = match t with | Empty -> 0 | Node l _ r _ _ -> let hl = real_height l in let hr = real_height r in 1 + if hl < hr then hr else hl end - + (* Size of the tree. *) function real_size (t:tree 'a) : int = match t with | Empty -> 0 | Node l _ r _ _ -> real_size l + 1 + real_size r end - + (* Height and size are non-negative. *) let rec lemma real_height_and_size_nonnegatives (t:tree 'a) : unit ensures { real_height t >= 0 } @@ -56,7 +55,7 @@ module Base | Node l _ r _ _ -> real_height_and_size_nonnegatives l; real_height_and_size_nonnegatives r end - + (* Balanced tree + correctness of stored height and size. *) predicate balanced (balancing:int) (t:tree 'a) = match t with | Empty -> true @@ -65,7 +64,7 @@ module Base -balancing <= real_height r - real_height l <= balancing /\ balanced balancing l /\ balanced balancing r end - + (* Stored data correction. *) predicate avl_data_correct (inv:'a -> bool) (t:tree 'a) = match t with @@ -73,13 +72,13 @@ module Base | Node l d r _ _ -> avl_data_correct inv l /\ inv d /\ avl_data_correct inv r end - + (* Tree rotations are the core of balancing, so we show that they preserve the model. *) lemma rotation_preserve_model : forall ld rd:'a,fl fm fr:list 'a. node_model (node_model fl ld fm) rd fr = node_model fl ld (node_model fm rd fr) - + (* Avl type. *) type t 'a 'b = { (* Representation as a binary tree. *) @@ -90,7 +89,7 @@ module Base type information) *) ghost prm : type_params 'a 'b; } - + (* Invariant. *) predicate c_balancing (balancing:int) (a:t 'a 'b) = let tree = a.repr in @@ -98,7 +97,7 @@ module Base avl_data_correct a.prm.inv tree /\ a.m.lis = list_model a.prm.mdl tree /\ a.m.hgt = real_height tree - + (* Get the height of the avl. *) let height (t:t 'a 'b) : int requires { exists balancing. c_balancing balancing t } @@ -107,7 +106,7 @@ module Base | Empty -> 0 | Node _ _ _ h _ -> h end - + (* Internal function, get the size of the avl. *) let internal_size (t:t 'a 'b) : int requires { exists balancing. c_balancing balancing t } @@ -116,7 +115,7 @@ module Base | Empty -> 0 | Node _ _ _ _ s -> s end - + (* Get the size of the list representation (specification wrapper). *) let size (t:t 'a 'b) : int requires { exists balancing. c_balancing balancing t } @@ -128,22 +127,21 @@ module Base variant { t } = match t with Empty -> () | Node l _ r _ _ -> aux l; aux r end in aux t.repr; s - + end (* Doubly-ended lists as avl. *) module AVL - + use import int.Int use import bool.Bool use import list.Append use import list.Length - use import HighOrd use import program_type.TypeParams use import option.Option use import ref.Ref use export Base - + (* Parameter: balancing. The balancing can be any positive integer. This is a trade-off between the cost of balancing and the cost of finding: @@ -152,13 +150,13 @@ module AVL constant balancing : int (* Parameter: the balancing is positive. *) axiom balancing_positive : balancing > 0 - + predicate c (a:t 'a 'b) = c_balancing balancing a - + (* Make avl parameters for use in polymorphic code. *) clone export program_type.Type1Prm with type t = t, type m = m, predicate c = c, function m = m, function prm = prm - + (* Empty avl. *) let empty (ghost p:type_params 'a 'b) : t 'a 'b ensures { c result } @@ -166,7 +164,7 @@ module AVL ensures { result.prm = p } ensures { result.m.hgt = 0 } = { repr = Empty; m = { lis = Nil; hgt = 0 }; prm = p } - + (* Node constructor. Restricted to perfect balancing. *) let node (l:t 'a 'b) (d:'a) (r:t 'a 'b) : t 'a 'b requires { l.prm = r.prm } @@ -185,7 +183,7 @@ module AVL hgt = h }; prm = r.prm } in res - + (* Create a one-element avl. *) let singleton (ghost p:type_params 'a 'b) (d:'a) : t 'a 'b requires { p.inv d } @@ -196,7 +194,7 @@ module AVL = { repr = Node Empty d Empty 1 1; m = { lis = Cons (p.mdl d) Nil; hgt = 1 }; prm = p } - + (* Emptyness test. *) let is_empty (t:t 'a 'b) : bool requires { c t } @@ -205,12 +203,12 @@ module AVL | Empty -> true | _ -> false end - + (* View of an avl. *) type view 'a 'b = | AEmpty | ANode (t 'a 'b) 'a (t 'a 'b) int - + (* Pattern-matching. Could be done directly over the representation, but this rebuild the records. *) let view (t:t 'a 'b) : view 'a 'b @@ -236,7 +234,7 @@ module AVL prm = p } h end - + (* Node constructor, defective balancing allowed in input. *) let balance (l:t 'a 'b) (d:'a) (r:t 'a 'b) : t 'a 'b requires { l.prm = r.prm } @@ -281,7 +279,7 @@ module AVL end end else node l d r - + (* Decompose l ++ [d] ++ r as head::tail, avl version. Internal function. *) let rec decompose_front_node (l:t 'a 'b) (d:'a) (r:t 'a 'b) : ('a,t 'a 'b) requires { c l /\ l.prm.inv d /\ c r /\ l.prm = r.prm } @@ -297,7 +295,7 @@ module AVL | ANode l d2 r2 _ -> let (d3,left) = decompose_front_node l d2 r2 in (d3,balance left d r) end - + (* Pattern-matching over the model list front. *) let decompose_front (t:t 'a 'b) : option ('a,t 'a 'b) requires { c t } @@ -308,7 +306,7 @@ module AVL | AEmpty -> None | ANode l d r _ -> Some (decompose_front_node l d r) end - + let rec decompose_back_node (l:t 'a 'b) (d:'a) (r:t 'a 'b) : (t 'a 'b,'a) requires { c l /\ l.prm.inv d /\ c r /\ l.prm = r.prm } requires { -balancing <= l.m.hgt - r.m.hgt <= balancing } @@ -323,7 +321,7 @@ module AVL | ANode l2 d2 r _ -> let (right,d3) = decompose_back_node l2 d2 r in (balance l d right,d3) end - + (* Pattern-matching over the model list back. *) let decompose_back (t:t 'a 'b) : option (t 'a 'b,'a) requires { c t } @@ -335,7 +333,7 @@ module AVL | AEmpty -> None | ANode l d r _ -> Some (decompose_back_node l d r) end - + let rec front_node (ghost li:ref (list 'b)) (l:t 'a 'b) (d:'a) : 'a requires { c l /\ l.prm.inv d } ensures { let p = l.prm in @@ -346,7 +344,7 @@ module AVL | ANode l d2 r _ -> let res = front_node li l d2 in li := !li ++ r.m.lis ++ Cons (r.prm.mdl d) Nil; res end - + (* Get the front of a non-empty list. The ghost reference is used to get an explicit view of the tail (no existential). *) let front (ghost li:ref (list 'b)) (t:t 'a 'b) : 'a @@ -358,7 +356,7 @@ module AVL | ANode l d2 r _ -> let res = front_node li l d2 in li := !li ++ r.m.lis; res end - + let rec back_node (ghost li:ref (list 'b)) (d:'a) (r:t 'a 'b) : 'a requires { c r /\ r.prm.inv d } ensures { let p = r.prm in @@ -369,7 +367,7 @@ module AVL | ANode l d2 r _ -> let res = back_node li d2 r in li := Cons (r.prm.mdl d) l.m.lis ++ !li; res end - + (* Get the back of a non-empty list. *) let back (ghost li:ref (list 'b)) (t:t 'a 'b) : 'a requires { c t /\ match t.m.lis with Nil -> false | _ -> true end } @@ -380,7 +378,7 @@ module AVL | ANode l d2 r _ -> let res = back_node li d2 r in li := l.m.lis ++ !li; res end - + (* Concatenation of avl, suppose inputs balanced (e.g left and right childs of a node) *) let fuse (l r:t 'a 'b) : t 'a 'b @@ -400,7 +398,7 @@ module AVL balance l d0 r' end end - + (* list cons with avl. *) let rec cons (d:'a) (t:t 'a 'b) : t 'a 'b requires { t.prm.inv d /\ c t } @@ -413,7 +411,7 @@ module AVL | AEmpty -> singleton t.prm d | ANode l d2 r _ -> balance (cons d l) d2 r end - + (* Reverse cons. *) let rec snoc (t:t 'a 'b) (d:'a) : t 'a 'b requires { c t /\ t.prm.inv d } @@ -425,7 +423,7 @@ module AVL | AEmpty -> singleton t.prm d | ANode l d2 r _ -> balance l d2 (snoc r d) end - + (* Node constructor, any (correct) input. *) let rec join (l:t 'a 'b) (d:'a) (r:t 'a 'b) : t 'a 'b requires { c l /\ l.prm.inv d /\ c r /\ l.prm = r.prm } @@ -448,7 +446,7 @@ module AVL else node l d r end end - + (* Concatenation, any (correct) input allowed. *) let concat (l:t 'a 'b) (r:t 'a 'b) : t 'a 'b requires { c l /\ c r /\ l.prm = r.prm } @@ -462,44 +460,44 @@ module AVL join l d0 r' end end - + (* Efficient enumeration of avl elements. Of course, it can be done by successful application of decompose_{front|back}, but this would be O(n*log(n)), while this method is O(n). *) namespace Enum - + use import list.Reverse - + (* Missing in list.Reverse. *) let rec lemma reverse_append_gen (l1 l2:list 'a) : unit ensures { reverse (l1 ++ l2) = reverse l2 ++ reverse l1 } variant { l1 } = match l1 with Cons _ q -> reverse_append_gen q l2 | _ -> () end - + (* Base representation. Basically the path to the current element. *) type base 'a 'b = End | More 'a (t 'a 'b) (base 'a 'b) - + (* Model of a left-to-right enumeration. *) function model_lr (f:'a -> 'b) (e:base 'a 'b) : list 'b = match e with | End -> Nil | More d r q -> Cons (f d) (r.m.lis ++ model_lr f q) end - + (* right-to-left version. *) function model_rl (f:'a -> 'b) (e:base 'a 'b) : list 'b = match e with | End -> Nil | More d l q -> Cons (f d) (reverse l.m.lis ++ model_rl f q) end - + predicate base_correct (p:type_params 'a 'b) (e:base 'a 'b) = match e with | End -> true | More d t next -> p.inv d /\ c t /\ base_correct p next /\ t.prm = p end - + (* Model: a list, and a boolean. The boolean let us know whether we are enumerating the elements from left to right (usual order) or from right to left (reverse order). *) @@ -507,36 +505,36 @@ module AVL lis : list 'b; left_to_right : bool; } - + type t 'a 'b = { repr : base 'a 'b; ghost left_to_right_t : bool; ghost prm : type_params 'a 'b; } - + (* Model function. *) function m (t:t 'a 'b) : m 'b = { lis = if t.left_to_right_t then model_lr t.prm.mdl t.repr else model_rl t.prm.mdl t.repr; left_to_right = t.left_to_right_t } - + (* Invariant. *) predicate c (e: t 'a 'b) = base_correct e.prm e.repr /\ e.m.lis = if e.m.left_to_right then model_lr e.prm.mdl e.repr else model_rl e.prm.mdl e.repr - + clone export program_type.Type1Prm with type t = t, type m = m, predicate c = c, function m = m, function prm = prm - + end (* Trick to avoid aliasing. *) namespace Enum - + use import list.Reverse - + (* Create an empty enumeration going the given way. *) let empty_enum (ghost ltr:bool) (ghost p:type_params 'a 'b) : Enum.t 'a 'b ensures { result.Enum.m.Enum.left_to_right = ltr } @@ -551,7 +549,7 @@ module AVL then m = Enum.model_lr p.mdl Enum.End && false else m = Enum.model_rl p.mdl Enum.End && false) && false }; res - + (* Add the elements of the avl in front of the given enumeration. Requires a left-to-right enumeration. *) let rec enum_lr (t:t 'a 'b) (acc:Enum.t 'a 'b) : Enum.t 'a 'b @@ -568,7 +566,7 @@ module AVL Enum.left_to_right_t = acc.Enum.left_to_right_t; Enum.prm = p } end - + (* Add the elements of the avl in front of the given enumeration, in reverse order. Requires a right-to-left enumeration. *) let rec enum_rl (t:t 'a 'b) (acc:Enum.t 'a 'b) : Enum.t 'a 'b @@ -585,7 +583,7 @@ module AVL Enum.left_to_right_t = acc.Enum.left_to_right_t; Enum.prm = p } end - + (* left-to-right enumeration pattern-matching. *) let decompose_lr (t:Enum.t 'a 'b) : option ('a,Enum.t 'a 'b) requires { Enum.c t } @@ -602,7 +600,7 @@ module AVL Enum.prm = t.Enum.prm } in Some (d,enum_lr r q') end - + (* right-to-left enumeration pattern-matching. *) let decompose_rl (t:Enum.t 'a 'b) : option ('a,Enum.t 'a 'b) requires { Enum.c t } @@ -619,44 +617,44 @@ module AVL Enum.prm = t.Enum.prm } in Some (d,enum_rl l q') end - + end - + end (* Part factorised out of selection module (for cloning). *) theory SelectionTypes - + use import list.List use import option.Option use import list.Append use Base - + type position 'a = { left : list 'a; middle : option 'a; right : list 'a; } - + type way_base 'a = Left 'a | Right 'a | Here - + function rebuild (p:position 'a) : list 'a = match p.middle with | Some x -> Base.node_model p.left x p.right | None -> p.left ++ p.right end - + function option_to_list (o:option 'a) : list 'a = match o with | Some x -> Cons x Nil | None -> Nil end - + lemma rebuild_aternative_def : forall p:position 'a. rebuild p = p.left ++ option_to_list p.middle ++ p.right - + end (* Addition/Removal/Etc(split,etc) algorithms based on selection. @@ -675,49 +673,48 @@ end Note: it would also work for non-deterministic selection. The result would be unspecified within the set of selected elements. *) module Selection - + use import int.Int use import bool.Bool use import list.Append use import option.Option use import program_type.TypeParams - use import HighOrd - + use export SelectionTypes - + (* Avl base. *) clone export AVL - + (* Parameter: shape of stored data. This is because the selector might requires a special shape for stored data to work. *) clone program_type.Type2 as D - + (* shortcut *) type s 'a 'b 'c 'd = t (D.t 'a 'b 'c 'd) (D.m 'b 'd) - + (* Parameter: selector type. *) type selector 'a 'b 'c 'd - + (* Parameter: correctness predicate for a selector with respect to the avl, e.g the selector can select something in its list + representation invariants. *) predicate selector_correct (type_params 'a 'b) (type_params 'c 'd) (selector 'a 'b 'c 'd) (s 'a 'b 'c 'd) - + (* Parameter: a position is selected by a selector in the list corresponding to the avl. *) predicate selected (type_params 'a 'b) (type_params 'c 'd) (selector 'a 'b 'c 'd) (position (D.m 'b 'd)) (s 'a 'b 'c 'd) - + (* way to the position. *) type way 'a 'b 'c 'd = way_base (selector 'a 'b 'c 'd) - + (* Parameter: a correct selector for the empty list always select its only possible position. *) axiom selector_correct_empty : forall p1,p2,s:selector 'a 'b 'c 'd,t. selector_correct p1 p2 s t /\ t.m.lis = Nil -> selected p1 p2 s { left = Nil ; middle = None ; right = Nil } t - + (* Parameter: branch on a node. *) val selected_way (ghost p1:type_params 'a 'b) (ghost p2:type_params 'c 'd) (s:selector 'a 'b 'c 'd) (ghost base:s 'a 'b 'c 'd) @@ -739,14 +736,14 @@ module Selection forall e. selected p1 p2 sr e r /\ rebuild e = r.m.lis -> let e2 = { e with left = node_model l.m.lis (l.prm.mdl d) e.left } in selected p1 p2 s e2 base /\ rebuild e2 = base.m.lis } - + use import ref.Ref - + (* Create a reference over a dummy position. For use as argument for the functions taking such a reference. *) let ghost default_position () : ref (position 'a) = ref { left = Nil; middle = None; right = Nil } - + (* Split the avl using the given selector into l ++ (maybe something) ++ r, and rebuild it with d in the middle (potentially erasing whatever was there before): build l ++ [d] ++ r. @@ -779,7 +776,7 @@ module Selection node tl d tr end end - + (* Split the avl using the given selector into l ++ (maybe) ++ r, and rebuild it without whatever was in the middle: build l ++ r. *) @@ -810,7 +807,7 @@ module Selection fuse tl tr end end - + (* Split the avl according to the selector. *) let rec split (ghost p1:type_params 'a 'b) (ghost p2:type_params 'c 'd) (ghost r:ref (position (D.m 'b 'd))) (s:selector 'a 'b 'c 'd) @@ -841,7 +838,7 @@ module Selection (tl,Some td,tr) end end - + (* Return the middle value obtained by splitting the avl with respect to the selector. *) let rec get (ghost p1:type_params 'a 'b) (ghost p2:type_params 'c 'd) @@ -870,7 +867,7 @@ module Selection Some td end end - + (* (* Check whether there is a middle value when splitting the avl with respect to the selector. *) @@ -897,6 +894,6 @@ module Selection true end end*) - + end diff --git a/examples/in_progress/avl/monoid/association_list.mlw b/examples/in_progress/avl/monoid/association_list.mlw index d33a6c73e2da1ddf8be31147d1c0602b2e86ccd3..bc90eb115d665b350833b1f67fe68e8c511e4a56 100644 --- a/examples/in_progress/avl/monoid/association_list.mlw +++ b/examples/in_progress/avl/monoid/association_list.mlw @@ -3,41 +3,40 @@ (* Association with respect to an equivalence relation. *) module Assoc - + clone import key_type.KeyType as K clone import relations.Equivalence as Eq with type t = key - + use import list.List use import list.Mem use import list.Append use import option.Option - use import HighOrd - + predicate appear (k:key) (l:list (t 'a)) = exists x. mem x l /\ Eq.rel k x.key - + lemma appear_append : forall k:key,l r:list (t 'a). appear k (l++r) <-> appear k l \/ appear k r - + (* Unique occurence (a desirable property of an association list). *) predicate unique (l:list (t 'a)) = match l with | Nil -> true | Cons x q -> not appear x.key q /\ unique q end - + (* functional update with equivalence classes. *) function equiv_update (f:key -> 'b) (k:key) (b:'b) : key -> 'b = \k2. if Eq.rel k k2 then b else f k2 - + function const_none : 'a -> option 'b = \x.None - + (* functional model of an association list. *) function model (l:list (t 'a)) : key -> option (t 'a) = match l with | Nil -> const_none | Cons d q -> equiv_update (model q) d.key (Some d) end - + (* A key is bound iff it occurs in the association lists. *) let rec lemma model_occurence (k:key) (l:list (t 'a)) : unit ensures { appear k l <-> match model l k with None -> false @@ -45,14 +44,14 @@ module Assoc ensures { not appear k l <-> model l k = None } variant { l } = match l with Cons _ q -> model_occurence k q | _ -> () end - + (* A key is bound to a value with an equivalent key. *) let rec lemma model_link (k:key) (l:list (t 'a)) : unit ensures { match model l k with None -> true | Some d -> Eq.rel k d.key end } variant { l } = match l with Cons _ q -> model_link k q | _ -> () end - + (* Two equivalent keys are bound to the same value. *) let rec lemma model_equal (k1 k2:key) (l:list (t 'a)) : unit requires { Eq.rel k1 k2 } @@ -62,7 +61,7 @@ module Assoc | Cons _ q -> model_equal k1 k2 q | _ -> () end - + (* If the list satisfies the uniqueness property, then every value occuring in the list is the image of its key. *) let rec lemma model_unique (k:key) (l:list (t 'a)) : unit @@ -70,12 +69,12 @@ module Assoc ensures { forall d. mem d l -> model l d.key = Some d } variant { l } = match l with Cons _ q -> model_unique k q | _ -> () end - + (* Singleton association list. *) let lemma model_singleton (k:key) (d:t 'a) : unit ensures { model (Cons d Nil) k = if rel k d.key then Some d else None } = () - + (* Unique union of association list by concatenation. *) let rec lemma model_concat (k:key) (l r:list (t 'a)) : unit requires { unique (l++r) /\ unique l /\ unique r } @@ -91,19 +90,19 @@ module Assoc | Nil -> () | Cons _ q -> model_concat k q r end - + end (* Sorted (increasing) association list. *) module AssocSorted - + use import list.List use import list.Append use import list.Mem use import option.Option - + clone import key_type.KeyType as K clone import preorder.Full as O with type t = key clone export Assoc with type K.key = K.key, @@ -119,14 +118,14 @@ module AssocSorted function K.key = K.key, predicate O.rel = O.lt, goal O.Trans - + (* Sorted lists are association lists with unicity property. *) let rec lemma increasing_unique (l:list (t 'a)) : unit requires { S.increasing l } ensures { unique l } variant { l } = match l with Cons _ q -> increasing_unique q | _ -> () end - + let lemma model_cut (k:key) (l r:list (t 'a)) : unit requires { S.increasing r } requires { S.increasing l } @@ -156,7 +155,7 @@ module AssocSorted end && false }; assert { forall k2. eq k k2 -> model (l++r) k2 <> None -> (not appear k2 l /\ not appear k2 r) && false } - + let lemma model_split (d:t 'a) (l r:list (t 'a)) : unit requires { S.increasing l } requires { S.increasing r } @@ -168,6 +167,6 @@ module AssocSorted ensures { forall k2. lt k2 d.key -> model (l++Cons d r) k2 = model l k2 } ensures { forall k2. le d.key k2 -> model l k2 = None } = () - + end diff --git a/examples/in_progress/avl/monoid/avl.mlw b/examples/in_progress/avl/monoid/avl.mlw index 03e11d6d6d113d44e80cce114d5de4d5a612d536..2a05fc7b7b2f726e21cf3234e521c23926e4387c 100644 --- a/examples/in_progress/avl/monoid/avl.mlw +++ b/examples/in_progress/avl/monoid/avl.mlw @@ -1,69 +1,68 @@ (* Part factorised out of selection module (for cloning). *) theory SelectionTypes - + use import list.List use import option.Option use import list.Append - + type split 'a = { left : list 'a; middle : option 'a; right : list 'a; } - + type part_base 'a = Left 'a | Right 'a | Here - + function rebuild (p:split 'a) : list 'a = match p.middle with | Some x -> p.left ++ Cons x p.right | None -> p.left ++ p.right end - + function option_to_list (o:option 'a) : list 'a = match o with | Some x -> Cons x Nil | None -> Nil end - + lemma rebuild_aternative_def : forall p:split 'a. rebuild p = p.left ++ option_to_list p.middle ++ p.right - + function left_extend (l:list 'a) (d:'a) (e:split 'a) : split 'a = { e with left = l ++ Cons d e.left } - + function right_extend (e:split 'a) (d:'a) (r:list 'a) : split 'a = { e with right = e.right ++ Cons d r } - + end module AVL - + use import int.Int use import bool.Bool use import list.Append - use import HighOrd use import program_type.TypeParams use import option.Option use import ref.Ref - + clone monoid.ComputableMonoid as M clone monoid.MonoidList as M with type M.t = M.m, constant M.zero = M.zero, function M.op = M.op, goal M.assoc, goal M.neutral - - namespace D + + scope D clone export program_type.Type1 function measure (m 'b) : M.m val measure (ghost p:type_params 'a 'b) (x:t 'a 'b) : M.t requires { p.mp.inv x } ensures { M.c result /\ measure (p.mp.mdl x) = result.M.m } end - + (* Parameter: balancing. The balancing can be any positive integer. This is a trade-off between the cost of balancing and the cost of finding: @@ -72,12 +71,12 @@ module AVL constant balancing : int (* Parameter: the balancing is positive. *) axiom balancing_positive : balancing > 0 - + (* tree representation. *) type tree 'a 'b = | Empty | Node (tree 'a 'b) (D.t 'a 'b) (tree 'a 'b) int M.t - + (* Model of an avl. Intended to expose: - The list representation. - The height. *) @@ -85,11 +84,11 @@ module AVL lis : list (D.m 'b); hgt : int; } - + (* Shortcut. *) function node_model (l:list 'a) (d:'a) (r:list 'a) : list 'a = l ++ Cons d r - + (* list obtained from a tree by infix traversal + model mapping. *) function list_model (p:type_params (D.t 'a 'b) (D.m 'b)) (t:tree 'a 'b) : list (D.m 'b) = @@ -97,14 +96,14 @@ module AVL | Empty -> Nil | Node l d r _ _ -> node_model (list_model p l) (p.mdl d) (list_model p r) end - + (* Height of the tree. *) function real_height (t:tree 'a 'b) : int = match t with | Empty -> 0 | Node l _ r _ _ -> let hl = real_height l in let hr = real_height r in 1 + if hl < hr then hr else hl end - + (* Height is non-negative. *) let rec lemma real_height_nonnegative (t:tree 'a 'b) : unit ensures { real_height t >= 0 } @@ -113,7 +112,7 @@ module AVL | Empty -> () | Node l _ r _ _ -> real_height_nonnegative l; real_height_nonnegative r end - + (* Balanced tree + correctness of stored height and total. *) predicate balanced (p:type_params 'a 'b) (t:tree 'a 'b) = match t with | Empty -> true @@ -122,13 +121,13 @@ module AVL -balancing <= real_height r - real_height l <= balancing /\ balanced p l /\ balanced p r end - + (* Tree rotations are the core of balancing, so we show that they preserve the model. *) lemma rotation_preserve_model : forall ld rd:'a,fl fm fr:list 'a. node_model (node_model fl ld fm) rd fr = node_model fl ld (node_model fm rd fr) - + (* Avl type. *) type t 'a 'b = { (* Representation as a binary tree. *) @@ -139,19 +138,19 @@ module AVL type information) *) ghost prm : type_params 'a 'b; } - + function dprm (t:t 'a 'b) : type_params (D.t 'a 'b) (D.m 'b) = t.prm.D.mp let ghost dprm (t:t 'a 'b) : type_params (D.t 'a 'b) (D.m 'b) ensures { result = t.dprm } = t.prm.D.mp - + (* Invariant. *) predicate c (a:t 'a 'b) = let tree = a.repr in balanced a.prm tree /\ a.m.lis = list_model a.dprm tree /\ a.m.hgt = real_height tree - + (* Get the height of the avl. *) let height (t:t 'a 'b) : int requires { c t } @@ -160,7 +159,7 @@ module AVL | Empty -> 0 | Node _ _ _ h _ -> h end - + let total (t:t 'a 'b) : M.t requires { c t } ensures { M.c result /\ result.M.m = M.sum D.measure t.m.lis } @@ -168,11 +167,11 @@ module AVL | Empty -> M.zero () | Node _ _ _ _ m -> m end - + (* Make avl parameters for use in polymorphic code. *) clone export program_type.Type1Prm with type t = t, type m = m, predicate c = c, function m = m, function prm = prm - + (* Empty avl. *) let empty (ghost p:type_params 'a 'b) : t 'a 'b ensures { c result } @@ -180,7 +179,7 @@ module AVL ensures { result.prm = p } ensures { result.m.hgt = 0 } = { repr = Empty; m = { lis = Nil; hgt = 0 }; prm = p } - + (* Node constructor. Restricted to perfect balancing. *) let node (l:t 'a 'b) (d:D.t 'a 'b) (r:t 'a 'b) : t 'a 'b requires { l.prm = r.prm } @@ -199,7 +198,7 @@ module AVL hgt = h }; prm = r.prm } in res - + (* Create a one-element avl. *) let singleton (ghost p:type_params 'a 'b) (d:D.t 'a 'b) : t 'a 'b requires { p.D.mp.inv d } @@ -211,7 +210,7 @@ module AVL m = { lis = Cons (p.D.mp.mdl d) Nil; hgt = 1 }; prm = p } in res - + (* Emptyness test. *) let is_empty (t:t 'a 'b) : bool requires { c t } @@ -220,12 +219,12 @@ module AVL | Empty -> true | _ -> false end - + (* View of an avl. *) type view 'a 'b = | AEmpty | ANode (t 'a 'b) (D.t 'a 'b) (t 'a 'b) int M.t - + (* Pattern-matching. Could be done directly over the representation, but this rebuild the records. *) let view (t:t 'a 'b) : view 'a 'b @@ -253,7 +252,7 @@ module AVL h s end - + (* Node constructor, defective balancing allowed in input. *) let balance (l:t 'a 'b) (d:D.t 'a 'b) (r:t 'a 'b) : t 'a 'b requires { l.prm = r.prm } @@ -298,7 +297,7 @@ module AVL end end else node l d r - + (* Decompose l ++ [d] ++ r as head::tail, avl version. Internal function. *) let rec decompose_front_node (l:t 'a 'b) (d:D.t 'a 'b) (r:t 'a 'b) : (D.t 'a 'b,t 'a 'b) @@ -315,7 +314,7 @@ module AVL | ANode l d2 r2 _ _ -> let (d3,left) = decompose_front_node l d2 r2 in (d3,balance left d r) end - + (* Pattern-matching over the model list front. *) let decompose_front (t:t 'a 'b) : option (D.t 'a 'b,t 'a 'b) requires { c t } @@ -326,7 +325,7 @@ module AVL | AEmpty -> None | ANode l d r _ _ -> Some (decompose_front_node l d r) end - + let rec decompose_back_node (l:t 'a 'b) (d:D.t 'a 'b) (r:t 'a 'b) : (t 'a 'b,D.t 'a 'b) requires { c l /\ l.dprm.inv d /\ c r /\ l.prm = r.prm } @@ -342,7 +341,7 @@ module AVL | ANode l2 d2 r _ _ -> let (right,d3) = decompose_back_node l2 d2 r in (balance l d right,d3) end - + (* Pattern-matching over the model list back. *) let decompose_back (t:t 'a 'b) : option (t 'a 'b,D.t 'a 'b) requires { c t } @@ -353,7 +352,7 @@ module AVL | AEmpty -> None | ANode l d r _ _ -> Some (decompose_back_node l d r) end - + let rec front_node (ghost li:ref (list (D.m 'b))) (l:t 'a 'b) (d:D.t 'a 'b) : D.t 'a 'b requires { c l /\ l.dprm.inv d } @@ -365,7 +364,7 @@ module AVL | ANode l d2 r _ _ -> let res = front_node li l d2 in li := !li ++ r.m.lis ++ Cons (r.dprm.mdl d) Nil; res end - + (* Get the front of a non-empty list. The ghost reference is used to get an explicit view of the tail (no existential). *) let front (ghost li:ref (list (D.m 'b))) @@ -377,7 +376,7 @@ module AVL | ANode l d2 r _ _ -> let res = front_node li l d2 in li := !li ++ r.m.lis; res end - + let rec back_node (ghost li:ref (list (D.m 'b))) (d:D.t 'a 'b) (r:t 'a 'b) : D.t 'a 'b requires { c r /\ r.dprm.inv d } @@ -389,7 +388,7 @@ module AVL | ANode l d2 r _ _ -> let res = back_node li d2 r in li := Cons (r.dprm.mdl d) l.m.lis ++ !li; res end - + (* Get the back of a non-empty list. *) let back (ghost li:ref (list (D.m 'b))) (t:t 'a 'b) : D.t 'a 'b @@ -401,7 +400,7 @@ module AVL | ANode l d2 r _ _ -> let res = back_node li d2 r in li := l.m.lis ++ !li; res end - + (* Concatenation of avl, suppose inputs balanced (e.g left and right childs of a node) *) let fuse (l r:t 'a 'b) : t 'a 'b @@ -421,7 +420,7 @@ module AVL balance l d0 r' end end - + (* list cons with avl. *) let rec cons (d:D.t 'a 'b) (t:t 'a 'b) : t 'a 'b requires { t.dprm.inv d /\ c t } @@ -433,7 +432,7 @@ module AVL | AEmpty -> singleton t.prm d | ANode l d2 r _ _ -> balance (cons d l) d2 r end - + (* Reverse cons. *) let rec snoc (t:t 'a 'b) (d:D.t 'a 'b) : t 'a 'b requires { c t /\ t.dprm.inv d } @@ -445,7 +444,7 @@ module AVL | AEmpty -> singleton t.prm d | ANode l d2 r _ _ -> balance l d2 (snoc r d) end - + (* Node constructor, any (correct) input. *) let rec join (l:t 'a 'b) (d:D.t 'a 'b) (r:t 'a 'b) : t 'a 'b requires { c l /\ l.dprm.inv d /\ c r /\ l.prm = r.prm } @@ -467,7 +466,7 @@ module AVL else node l d r end end - + (* Concatenation, any (correct) input allowed. *) let concat (l r:t 'a 'b) : t 'a 'b requires { c l /\ c r /\ l.prm = r.prm } @@ -481,7 +480,7 @@ module AVL join l d0 r' end end - + (* Insertion/Removal/Lookup/split/etc algorithms based on selection. Basic idea: functions add/remove/split/etc on an avl do not need an order over the stored data, but rather a @@ -498,29 +497,29 @@ module AVL - others... Note: it would also work for non-deterministic selection. The result would be unspecified within the set of selected elements. *) - + use export SelectionTypes - + (* Parameter: selector type. *) type selector - + (* Parameter: correctness predicate for a selector with respect to the list e.g the selector can select something in the list + representation invariants. *) predicate selection_possible selector (list (D.m 'b)) - + (* Parameter: a position is selected by a selector in the. *) predicate selected selector (split (D.m 'b)) - + (* Selected part. *) type part = part_base selector - + (* Parameter: a correct selector for the empty list always select its only possible position. *) axiom selection_empty : forall s. let nil = (Nil:list (D.m 'b)) in selection_possible s nil -> selected s { left = nil ; middle = None ; right = nil } - + (* Parameter: branch on a node. *) val selected_part (ghost p:type_params 'a 'b) (ghost llis:list (D.m 'b)) @@ -539,14 +538,14 @@ module AVL | Right sr -> selection_possible sr rlis /\ forall e. selected sr e /\ rebuild e = rlis -> selected s (left_extend llis (p.D.mp.mdl d) e) } - + use import ref.Ref - + (* Create a reference over a dummy split. For use as argument for the functions taking such a reference. *) let ghost default_split () : ref (split 'a) = ref { left = Nil; middle = None; right = Nil } - + (* Split the avl using the given selector into l ++ (maybe something) ++ r, and rebuild it with d in the middle (potentially erasing whatever was there before): build l ++ [d] ++ r. @@ -576,7 +575,7 @@ module AVL node tl d tr end end - + (* Split the avl using the given selector into l ++ (maybe) ++ r, and rebuild it without whatever was in the middle: build l ++ r. *) @@ -604,7 +603,7 @@ module AVL fuse tl tr end end - + let rec extract (ghost r:ref (split (D.m 'b))) (s:selector) (t:t 'a 'b) : (option (D.t 'a 'b),t 'a 'b) requires { selection_possible s t.m.lis /\ c t } @@ -631,8 +630,8 @@ module AVL (Some td,fuse tl tr) end end - - + + (* Split the avl according to the selector. *) let rec split (ghost r:ref (split (D.m 'b))) (s:selector) (t:t 'a 'b) : (t 'a 'b,option (D.t 'a 'b),t 'a 'b) @@ -662,7 +661,7 @@ module AVL (tl,Some td,tr) end end - + (* Return the middle value obtained by splitting the avl with respect to the selector. *) let rec get (ghost r:ref (split (D.m 'b))) (s:selector) @@ -687,6 +686,6 @@ module AVL Some td end end - + end diff --git a/examples/in_progress/avl/monoid/monoid.mlw b/examples/in_progress/avl/monoid/monoid.mlw index cabdff11ac1965c135d8f32e1732a84e816a9b01..b45c0adf309eb396e54645bfec21c42e912edff4 100644 --- a/examples/in_progress/avl/monoid/monoid.mlw +++ b/examples/in_progress/avl/monoid/monoid.mlw @@ -1,39 +1,37 @@ module Monoid - + type t - + constant zero : t function op (a b:t) : t - + axiom assoc : forall a b c:t. op a (op b c) = op (op a b) c axiom neutral : forall x:t. op x zero = x = op zero x - + end module MonoidList - + use import list.Append - use import HighOrd clone import Monoid as M - + (* Because definitions cannot be replicated via cloning. *) function sum (f:'a -> t) (l:list 'a) : t axiom sum_def_nil : forall f:'a -> t. sum f Nil = zero axiom sum_def_cons : forall f:'a -> t,x,q. sum f (Cons x q) = op (f x) (sum f q) - + let rec lemma sum_append (f:'a -> t) (l r:list 'a) : unit ensures { sum f (l ++ r) = op (sum f l) (sum f r) } variant { l } = match l with Cons _ q -> sum_append f q r | _ -> () end - + end module MonoidListDef use import list.List - use import HighOrd - + namespace M type t constant zero : t @@ -46,21 +44,21 @@ module MonoidListDef clone export MonoidList with type M.t = M.t,constant M.zero = M.zero, function M.op = M.op,function sum = sum, goal sum_def_nil,goal sum_def_cons - + end module ComputableMonoid - + use import program_type.TypeParams clone export program_type.Type0 clone export Monoid with type t = m - + val zero () : t ensures { c result /\ result.m = zero } - + val op (a b:t) : t requires { c a /\ c b } ensures { c result /\ result.m = op a.m b.m } - + end diff --git a/examples/in_progress/avl/monoid/program_type.mlw b/examples/in_progress/avl/monoid/program_type.mlw index d7c1ca4585f384283b3b73b533c5ea35e85aac31..592c3d4cf61413a6dee781badc2f91341cf1a7bf 100644 --- a/examples/in_progress/avl/monoid/program_type.mlw +++ b/examples/in_progress/avl/monoid/program_type.mlw @@ -3,9 +3,7 @@ This additional parameterization is rather administrative. *) module TypeParams - - use import HighOrd - + (* Additional information for parametric programs: 'a represent the program type (the effective datatype), 'b represent its logical model (the reasoning datatype), @@ -18,7 +16,7 @@ module TypeParams inv : 'a -> bool; mdl : 'a -> 'b; } - + (* For purely logical types. *) constant default_params : type_params 'a 'a (* Definition axiomatized to avoid a very harmful effect @@ -27,13 +25,13 @@ module TypeParams inv = \n. true; mdl = \x. x; } - + end module Type0 - + use import TypeParams - + (* Program version of the type. *) type t (* Its logical model. *) @@ -44,30 +42,30 @@ module Type0 function m t : m (* Parametric information (for use in polymorphic code). *) constant mp : type_params t m = { inv = (\t. c t); mdl = (\t. m t) } - + end (* Variants with different number of type variables. *) module Type1 - + use import TypeParams - + (* Need two types variables to represent both the program and logic worlds. *) type t 'a 'b type m 'b (* Parametric model and invariants. *) - function mp (type_params 'a 'b) : type_params (t 'a 'b) (m 'b) - + function mp (type_params 'a 'b) : type_params (t 'a 'b) (m 'b) + end (* Variant for a type storing explicitly its parameters (typically in ghost fields). *) module Type1Prm - + use import TypeParams - + type t 'a 'b type m 'b predicate c (t 'a 'b) @@ -76,35 +74,35 @@ module Type1Prm function mp (p:type_params 'a 'b) : type_params (t 'a 'b) (m 'b) = { inv = (\t. c t /\ prm t = p); mdl = (\t. m t) } - + end module Type2 - + use import TypeParams - + type t 'a 'b 'c 'd type m 'b 'd function mp (type_params 'a 'b) (type_params 'c 'd) : type_params (t 'a 'b 'c 'd) (m 'b 'd) - + end module Type2Prm - + use import TypeParams - + type t 'a 'b 'c 'd type m 'b 'd predicate c (t 'a 'b 'c 'd) function m (t 'a 'b 'c 'd) : m 'b 'd function prm1 (t 'a 'b 'c 'd) : type_params 'a 'b function prm2 (t 'a 'b 'c 'd) : type_params 'c 'd - function mp (p1:type_params 'a 'b) (p2:type_params 'c 'd) : + function mp (p1:type_params 'a 'b) (p2:type_params 'c 'd) : type_params (t 'a 'b 'c 'd) (m 'b 'd) = { inv = (\t. c t /\ prm1 t = p1 /\ prm2 t = p2); mdl = (\t. m t) } - + end diff --git a/examples/in_progress/avl/program_type.mlw b/examples/in_progress/avl/program_type.mlw index fa9b1b499f73eb840d2fde612d4fa7b810b095c9..ac986e57a4aa7ea1285b9a94813bdcb5b713e961 100644 --- a/examples/in_progress/avl/program_type.mlw +++ b/examples/in_progress/avl/program_type.mlw @@ -1,8 +1,6 @@ module TypeParams - - use import HighOrd - + (* Additional information for parametric programs: 'a represent the program type (the effective datatype), 'b represent its logical model (the reasoning datatype), @@ -15,19 +13,19 @@ module TypeParams inv : 'a -> bool; mdl : 'a -> 'b; } - + (* For purely logical types. *) constant default_params : type_params 'a 'a = { inv = \n. true; mdl = \x. x; } - + end module Type0 - + use import TypeParams - + (* Program version of the type. *) type t (* Its logical model. *) @@ -38,30 +36,30 @@ module Type0 function m t : m (* Parametric information (for use in polymorphic code). *) constant p : type_params t m = { inv = (\t. c t); mdl = (\t. m t) } - + end (* Variants with different number of type variables. *) module Type1 - + use import TypeParams - + (* Need two types variables to represent both the program and logic worlds. *) type t 'a 'b type m 'b (* Parametric model and invariants. *) - function make_params (type_params 'a 'b) : type_params (t 'a 'b) (m 'b) - + function make_params (type_params 'a 'b) : type_params (t 'a 'b) (m 'b) + end (* Variant for a type storing explicitly its parameters (typically in ghost fields). *) module Type1Prm - + use import TypeParams - + type t 'a 'b type m 'b predicate c (t 'a 'b) @@ -70,35 +68,35 @@ module Type1Prm function make_params (p:type_params 'a 'b) : type_params (t 'a 'b) (m 'b) = { inv = (\t. c t /\ prm t = p); mdl = (\t. m t) } - + end module Type2 - + use import TypeParams - + type t 'a 'b 'c 'd type m 'b 'd function make_params (type_params 'a 'b) (type_params 'c 'd) : type_params (t 'a 'b 'c 'd) (m 'b 'd) - + end module Type2Prm - + use import TypeParams - + type t 'a 'b 'c 'd type m 'b 'd predicate c (t 'a 'b 'c 'd) function m (t 'a 'b 'c 'd) : m 'b 'd function prm1 (t 'a 'b 'c 'd) : type_params 'a 'b function prm2 (t 'a 'b 'c 'd) : type_params 'c 'd - function make_params (p1:type_params 'a 'b) (p2:type_params 'c 'd) : + function make_params (p1:type_params 'a 'b) (p2:type_params 'c 'd) : type_params (t 'a 'b 'c 'd) (m 'b 'd) = { inv = (\t. c t /\ prm1 t = p1 /\ prm2 t = p2); mdl = (\t. m t) } - + end diff --git a/examples/in_progress/avl_generic_dev/association_list.mlw b/examples/in_progress/avl_generic_dev/association_list.mlw index e545632d39dc6fdf3fe647584821d3f9e0ce08bb..26124712c3c8827f9fe77d541f68f2838726766c 100644 --- a/examples/in_progress/avl_generic_dev/association_list.mlw +++ b/examples/in_progress/avl_generic_dev/association_list.mlw @@ -3,42 +3,41 @@ (* Association with respect to an equivalence relation. *) module Assoc - + clone import key_type.KeyType as K clone import relations_params.EquivalenceParam as Eq with type t = key - + use import list.List use import list.Mem use import option.Option - use import HighOrd - + predicate appear (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) = exists x. mem x l /\ correct_for p k /\ Eq.rel p k (key x) - + (* Correction. *) predicate correct (p:param 'a) (l:list (t 'a 'b)) = match l with | Nil -> true | Cons x q -> let kx = key x in correct_for p kx /\ correct p q end - + (* Unique occurence (a desirable property of an association list). *) predicate unique (p:param 'a) (l:list (t 'a 'b)) = match l with | Nil -> true | Cons x q -> not appear p (key x) q /\ unique p q end - + (* functional update with equivalence classes. *) function param_update (p:param 'a) (f:key 'a -> 'b) (k:key 'a) (b:'b) : key 'a -> 'b = \k2. if Eq.rel p k k2 then b else f k2 - + (* functional model of an association list. *) function model (p:param 'a) (l:list (t 'a 'b)) : key 'a -> option (t 'a 'b) = match l with | Nil -> \x. None | Cons d q -> param_update p (model p q) (key d) (Some d) end - + (* A key is bound iff it occurs in the association lists. *) let rec lemma model_occurence (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit @@ -48,7 +47,7 @@ module Assoc | Some _ -> true end } variant { l } = match l with Cons _ q -> model_occurence p k q | _ -> () end - + (* A key is bound to a value with an equivalent key. *) let rec lemma model_link (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit requires { correct p l } @@ -57,7 +56,7 @@ module Assoc | Some d -> Eq.rel p k (key d) end } variant { l } = match l with Cons _ q -> model_link p k q | _ -> () end - + (* Two equivalent keys are bound to the same value. *) let rec lemma model_equal (p:param 'a) (k1 k2:key 'a) (l:list (t 'a 'b)) : unit @@ -67,7 +66,7 @@ module Assoc ensures { model p l k1 = model p l k2 } variant { l } = match l with Cons _ q -> model_equal p k1 k2 q | _ -> () end - + (* If the list satisfies the uniqueness property, then every value occuring in the list is the image of its key. *) let rec lemma model_unique (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit @@ -77,19 +76,19 @@ module Assoc ensures { forall d. mem d l -> model p l (key d) = Some d } variant { l } = match l with Cons _ q -> model_unique p k q | _ -> () end - + end (* Sorted (increasing) association list. *) module AssocSorted - + use import list.List use import list.Append use import list.Mem use import option.Option - + clone import key_type.KeyType as K clone import preorder.FullParam as O with type t = key (* The commented out part do not work, unfortunately. *) @@ -107,7 +106,7 @@ module AssocSorted predicate O.correct_for = O.correct_for, predicate O.rel = O.lt, goal O.trans - + (* Sorted lists are correct association lists with unicity property. *) let rec lemma increasing_unique_and_correct (o:order 'a) (l:list (t 'a 'b)) : unit @@ -116,7 +115,7 @@ module AssocSorted ensures { unique o l } variant { l } = match l with Cons _ q -> increasing_unique_and_correct o q | _ -> () end - + let lemma absent (o:order 'a) (k:key 'a) (l r:list (t 'a 'b)) : unit requires { correct_for o k } requires { S.increasing o l } @@ -126,7 +125,7 @@ module AssocSorted ensures { model o (l++r) k = None } = assert { S.precede o l r && not appear o k (l++r) && match model o (l++r) k with None -> true | _ -> false end } - + let lemma present (o:order 'a) (k:key 'a) (l r:list (t 'a 'b)) (d:t 'a 'b) : unit requires { correct_for o k } @@ -138,6 +137,6 @@ module AssocSorted requires { eq o k (key d) } ensures { model o (l++Cons d r) k = Some d } = assert { S.increasing o (l++Cons d r) } - + end diff --git a/examples/in_progress/avl_generic_dev/avl.mlw b/examples/in_progress/avl_generic_dev/avl.mlw index 48f32b723e12f1da474f8d1584405fab6dfd6724..6290da4c2e19fa90a6b56e74b10b44c90532639a 100644 --- a/examples/in_progress/avl_generic_dev/avl.mlw +++ b/examples/in_progress/avl_generic_dev/avl.mlw @@ -2,79 +2,78 @@ (* Technical reason: type must be declared outside for clones to work properly. *) theory ParamsTypes - + use import int.Int type view_base 'c 'd = | VEmpty | VNode 'c 'd 'c int - + type m_base 'c = | Empty | Node (m_base 'c) 'c (m_base 'c) int - + end (* AVL parameters: a binary tree structure (exact representation is unknown), + a positive balancing constant. *) module Params - + use import int.Int - + (* type for data stored in the nodes. *) clone program_type.Type2 as Data - + (* Abstract binary tree structure. *) namespace Tree - + use export ParamsTypes type m 'a 'b = m_base (Data.m 'a 'b) - + clone export program_type.Type2 with type m = m - + type view 'a 'b = view_base (t 'a 'b) (Data.t 'a 'b) - + (* Construction/pattern-matching over the tree. *) val empty () : t 'a 'b ensures { result.m = Empty } ensures { c result } - + val node (l:t 'a 'b) (d:Data.t 'a 'b) (r:t 'a 'b) (h:int) : t 'a 'b requires { c l /\ Data.c d /\ c r } ensures { result.m = Node l.m d.Data.m r.m h } ensures { c result } - + val view (t:t 'a 'b) : view 'a 'b ensures { match result with | VEmpty -> t.m = Empty | VNode l d r h -> t.m = Node l.m d.Data.m r.m h /\ c l /\ Data.c d /\ c r end } - + end - + (* Balancing constant for the tree. This will bound the height difference between the subtrees at a node of the avl. Larger constant mean deeper trees but less balancing operations. *) constant balancing : int axiom balancing_positive : balancing > 0 - + end (* AVL, modeled as a doubly-ended list + a non-negative height. *) module AVL - + use import int.Int use import bool.Bool use import list.Append - use import HighOrd use import option.Option use import ref.Ref - + (* AVL Parameters. *) clone import Params as P - + (* The model of an avl is morally a list. *) type l 'a 'b = list (Data.m 'a 'b) (* Excepted that we also expose an integer (the height of the tree), @@ -84,24 +83,24 @@ module AVL hgt : int; inv : Data.m 'a 'b -> bool; } - + (* Shortcut. *) function node_model (l:l 'a 'b) (d:Data.m 'a 'b) (r:l 'a 'b) : l 'a 'b = l ++ Cons d r - + (* list obtained from a tree by infix traversal. *) function list_model (t:Tree.m 'a 'b) : l 'a 'b = match t with | Tree.Empty -> Nil | Tree.Node l d r _ -> node_model (list_model l) d (list_model r) end - + (* Height of the tree. *) function real_height (t:Tree.m 'a 'b) : int = match t with | Tree.Empty -> 0 | Tree.Node l _ r _ -> let hl = real_height l in let hr = real_height r in 1 + if hl < hr then hr else hl end - + let rec lemma real_height_nonnegative (t:Tree.m 'a 'b) : unit ensures { real_height t >= 0 } variant { t } @@ -109,7 +108,7 @@ module AVL | Tree.Empty -> () | Tree.Node l _ r _ -> real_height_nonnegative l; real_height_nonnegative r end - + (* Balanced tree + correctness of stored height. *) predicate balanced (t:Tree.m 'a 'b) = match t with | Tree.Empty -> true @@ -117,7 +116,7 @@ module AVL -balancing <= real_height r - real_height l <= balancing /\ balanced l /\ balanced r end - + (* Well-formedness of the data is guaranteed by the parameters. We also allow user to specify additional properties satisfied by the stored data. *) @@ -127,13 +126,13 @@ module AVL | Tree.Node l d r _ -> avl_data_correct inv l /\ inv d /\ avl_data_correct inv r end - + (* Tree rotations are the core of balancing, so we show that they preserve the model. *) lemma rotation_preserve_model : forall ld rd:Data.m 'a 'b,fl fm fr:l 'a 'b. node_model (node_model fl ld fm) rd fr = node_model fl ld (node_model fm rd fr) - + (* Avl type. *) type t 'a 'b = { (* Representation as a binary tree. *) @@ -141,7 +140,7 @@ module AVL (* Model. *) ghost m : m 'a 'b; } - + (* Invariant. *) predicate c (a:t 'a 'b) = let tm = a.repr.Tree.m in @@ -150,14 +149,14 @@ module AVL a.m.lis = list_model tm /\ a.m.hgt = real_height tm /\ Tree.c a.repr - + (* Get the height of the avl. *) let height (a:t 'a 'b) : int requires { c a } ensures { result = a.m.hgt } = match Tree.view a.repr with Tree.VEmpty -> 0 | Tree.VNode _ _ _ h -> h end - - + + (* Constructors. *) (* The empty avl. *) let empty (ghost dinv:Data.m 'a 'b -> bool) : t 'a 'b @@ -167,7 +166,7 @@ module AVL ensures { result.m.hgt = 0 } = { repr = Tree.empty (); m = { lis = Nil; inv = dinv; hgt = 0 } } - + (* Node. Restricted to perfect balancing. *) let node (l:t 'a 'b) (d:Data.t 'a 'b) (r:t 'a 'b) : t 'a 'b requires { l.m.inv = r.m.inv } @@ -186,7 +185,7 @@ module AVL m = { lis = node_model l.m.lis d.Data.m r.m.lis; inv = r.m.inv; hgt = h } } - + (* Useful constructor. *) let singleton (ghost dinv:Data.m 'a 'b -> bool) (d:Data.t 'a 'b) : t 'a 'b requires { Data.c d /\ dinv d.Data.m } @@ -198,12 +197,12 @@ module AVL let e = Tree.empty () in { repr = Tree.node e d e 1; m = { lis = Cons d.Data.m Nil; inv = dinv; hgt = 1 } } - + (* View of an avl, in similar fashion to Tree.view. *) type view 'a 'b = | AEmpty | ANode (t 'a 'b) (Data.t 'a 'b) (t 'a 'b) int - + (* Pattern-matching. *) let view (t:t 'a 'b) : view 'a 'b requires { c t } @@ -229,7 +228,7 @@ module AVL hgt = real_height r.Tree.m } } h end - + (* Emptyness test. *) let is_empty (t:t 'a 'b) : bool requires { c t } @@ -239,7 +238,7 @@ module AVL | Tree.VEmpty -> true | _ -> false end - + (* Node constructor, defective balancing allowed in input. *) let balance (l:t 'a 'b) (d:Data.t 'a 'b) (r:t 'a 'b) : t 'a 'b requires { l.m.inv = r.m.inv } @@ -286,7 +285,7 @@ module AVL end end else node l d r - + (* Decompose l ++ [d] ++ r as head::tail,avl version. Internal function. *) let rec decompose_front_node (l:t 'a 'b) (d:Data.t 'a 'b) (r:t 'a 'b) : (Data.t 'a 'b,t 'a 'b) @@ -304,7 +303,7 @@ module AVL | ANode l d2 r2 _ -> let (d3,left) = decompose_front_node l d2 r2 in (d3,balance left d r) end - + (* Pattern-matching over the model list front. *) let decompose_front (t:t 'a 'b) : option (Data.t 'a 'b,t 'a 'b) requires { c t } @@ -315,7 +314,7 @@ module AVL | AEmpty -> None | ANode l d r _ -> Some (decompose_front_node l d r) end - + let rec decompose_back_node (l:t 'a 'b) (d:Data.t 'a 'b) (r:t 'a 'b) : (t 'a 'b,Data.t 'a 'b) requires { c l /\ Data.c d /\ c r /\ l.m.inv = r.m.inv /\ l.m.inv d.Data.m } @@ -332,7 +331,7 @@ module AVL | ANode l2 d2 r _ -> let (right,d3) = decompose_back_node l2 d2 r in (balance l d right,d3) end - + (* Pattern-matching over the model list back. *) let decompose_back (t:t 'a 'b) : option (t 'a 'b,Data.t 'a 'b) requires { c t } @@ -343,7 +342,7 @@ module AVL | AEmpty -> None | ANode l d r _ -> Some (decompose_back_node l d r) end - + let rec front_node (ghost li:ref (l 'a 'b)) (l:t 'a 'b) (d:Data.t 'a 'b) : Data.t 'a 'b requires { c l /\ Data.c d /\ l.m.inv d.Data.m } @@ -355,7 +354,7 @@ module AVL | ANode l d2 r _ -> let res = front_node li l d2 in li := !li ++ r.m.lis ++ Cons d.Data.m Nil; res end - + (* Get the front of a non-empty list. *) let front (ghost li:ref (l 'a 'b)) (t:t 'a 'b) : Data.t 'a 'b requires { c t /\ match t.m.lis with Nil -> false | _ -> true end } @@ -366,7 +365,7 @@ module AVL | ANode l d2 r _ -> let res = front_node li l d2 in li := !li ++ r.m.lis; res end - + let rec back_node (ghost li:ref (l 'a 'b)) (d:Data.t 'a 'b) (r:t 'a 'b) : Data.t 'a 'b requires { c r /\ Data.c d /\ r.m.inv d.Data.m } @@ -378,7 +377,7 @@ module AVL | ANode l d2 r _ -> let res = back_node li d2 r in li := Cons d.Data.m l.m.lis ++ !li; res end - + (* Get the back of a non-empty list. *) let back (ghost li:ref (l 'a 'b)) (t:t 'a 'b) : Data.t 'a 'b requires { c t /\ match t.m.lis with Nil -> false | _ -> true end } @@ -389,7 +388,7 @@ module AVL | ANode l d2 r _ -> let res = back_node li d2 r in li := l.m.lis ++ !li; res end - + (* Concatenation of avl, balancing hypothesis on inputs. *) let fuse (l r:t 'a 'b) : t 'a 'b requires { c l /\ c r /\ l.m.inv = r.m.inv } @@ -408,8 +407,8 @@ module AVL balance l d0 r' end end - - + + (* list cons with avl. *) let rec cons (d:Data.t 'a 'b) (t:t 'a 'b) : t 'a 'b requires { Data.c d /\ c t /\ t.m.inv d.Data.m } @@ -422,7 +421,7 @@ module AVL | AEmpty -> singleton t.m.inv d | ANode l d2 r _ -> balance (cons d l) d2 r end - + (* Reverse cons. *) let rec snoc (t:t 'a 'b) (d:Data.t 'a 'b) : t 'a 'b requires { c t /\ Data.c d /\ t.m.inv d.Data.m } @@ -434,7 +433,7 @@ module AVL | AEmpty -> singleton t.m.inv d | ANode l d2 r _ -> balance l d2 (snoc r d) end - + (* Node constructor, allow no balancing hypothesis at all. *) let rec join (l:t 'a 'b) (d:Data.t 'a 'b) (r:t 'a 'b) : t 'a 'b requires { c l /\ Data.c d /\ c r } @@ -458,7 +457,7 @@ module AVL else node l d r end end - + (* Concatenation, no balancing hypothesis on inputs. *) let concat (l:t 'a 'b) (r:t 'a 'b) : t 'a 'b requires { c l /\ c r /\ l.m.inv = r.m.inv } @@ -472,54 +471,54 @@ module AVL join l d0 r' end end - + (* Efficient enumeration of avl elements. Of course, it can be done by successful application of decompose, but this is O(n*log(n)), while this method is O(n). *) namespace Enum - + use import list.Reverse - + (* Missing in list.Reverse. *) let rec lemma reverse_append_gen (l1 l2:list 'a) : unit ensures { reverse (l1 ++ l2) = reverse l2 ++ reverse l1 } variant { l1 } = match l1 with Cons _ q -> reverse_append_gen q l2 | _ -> () end - + type base 'a 'b = End | More (Data.t 'a 'b) (t 'a 'b) (base 'a 'b) - + (* Model of a left-to-right enumeration. *) function model_lr (e:base 'a 'b) : l 'a 'b = match e with | End -> Nil | More d r q -> Cons d.Data.m (r.m.lis ++ model_lr q) end - + (* right-to-left version. *) function model_rl (e:base 'a 'b) : l 'a 'b = match e with | End -> Nil | More d l q -> Cons d.Data.m (reverse l.m.lis ++ model_rl q) end - + predicate base_correct (di:Data.m 'a 'b -> bool) (e:base 'a 'b) = match e with | End -> true | More d t next -> Data.c d /\ c t /\ base_correct di next /\ t.m.inv = di /\ di d.Data.m end - + type m 'a 'b = { inv : Data.m 'a 'b -> bool; lis : l 'a 'b; left_to_right : bool; } - + type t 'a 'b = { repr : base 'a 'b; ghost m : m 'a 'b; } - + predicate c (e: t 'a 'b) = base_correct e.m.inv e.repr /\ e.m.lis = if e.m.left_to_right @@ -528,7 +527,7 @@ module AVL end (* Trick to avoid aliasing. *) namespace Enum - + use import list.Reverse let empty_enum (ghost ltr:bool) (ghost dinv:Data.m 'a 'b -> bool) : Enum.t 'a 'b @@ -538,7 +537,7 @@ module AVL ensures { Enum.c result } = { Enum.repr = Enum.End; Enum.m = { Enum.inv = dinv; Enum.lis = Nil; Enum.left_to_right = ltr } } - + let rec enum_lr (t:t 'a 'b) (acc:Enum.t 'a 'b) : Enum.t 'a 'b requires { c t /\ Enum.c acc } requires { let accm = acc.Enum.m in @@ -554,7 +553,7 @@ module AVL Enum.m = { accm with Enum.lis = Cons d.Data.m (r.m.lis ++ accm.Enum.lis) } } end - + let rec enum_rl (t:t 'a 'b) (acc:Enum.t 'a 'b) : Enum.t 'a 'b requires { Enum.c acc /\ c t } requires { let accm = acc.Enum.m in @@ -571,7 +570,7 @@ module AVL Enum.m = { accm with Enum.lis = Cons d.Data.m (rl ++ accm.Enum.lis) } } end - + let decompose_lr (t:Enum.t 'a 'b) : option (Data.t 'a 'b,Enum.t 'a 'b) requires { Enum.c t } requires { t.Enum.m.Enum.left_to_right } @@ -593,7 +592,7 @@ module AVL Enum.m = { t.Enum.m with Enum.lis = l0 } } in Some (d,enum_lr r q') end - + let decompose_rl (t:Enum.t 'a 'b) : option (Data.t 'a 'b,Enum.t 'a 'b) requires { Enum.c t } requires { not t.Enum.m.Enum.left_to_right } @@ -610,26 +609,26 @@ module AVL Enum.m = { t.Enum.m with Enum.lis = l0 } } in Some (d,enum_rl l q') end - + end - + end theory SelectionTypes - + use import list.List use import option.Option - + type position_base 'a = { left : list 'a; middle : option 'a; right : list 'a; } - + type way_base 'a = Left 'a | Right 'a | Here - + end (* Addition/Removal/Etc(split,etc) algorithms based on selection. @@ -651,51 +650,50 @@ end Note: it would also work for non-deterministic selection. The result would be unspecified within the set of selected elements. *) module Selection - + use import int.Int use import bool.Bool use import list.Append use import option.Option - use import HighOrd - + clone export AVL use export SelectionTypes - + (* Position inside a list l. *) type position 'a 'b = position_base (P.Data.m 'a 'b) - + function rebuild (p:position 'a 'b) : l 'a 'b = match p.middle with | None -> p.left ++ p.right | Some d -> node_model p.left d p.right end - + function option_to_list (o:option 'a) : list 'a = match o with | None -> Nil | Some d -> Cons d Nil end - + lemma rebuild_alternative_def : forall p:position 'a 'b. rebuild p = p.left ++ option_to_list p.middle ++ p.right - + (* selector type. *) clone program_type.Type2 as S - + (* Correctness of a selector with respect to a list. *) predicate selector_correct (s:S.m 'a 'b) (l:l 'a 'b) - + (* A position is selected by a selector. *) predicate selected (s:S.m 'a 'b) (e:position 'a 'b) - + (* way to the position. *) type way 'a 'b = way_base (S.t 'a 'b) - + (* A correct selector for the empty list always select its only possible position. *) axiom selector_correct_empty : forall s:S.m 'a 'b. selector_correct s Nil -> selected s { left = Nil ; middle = None ; right = Nil } - + (* Branch on a position. *) val selected_way (s:S.t 'a 'b) (l:t 'a 'b) (d:P.Data.t 'a 'b) (r:t 'a 'b) : way 'a 'b @@ -713,12 +711,12 @@ module Selection | Right sr -> selector_correct sr.S.m r.m.lis /\ S.c sr /\ forall e. selected sr.S.m e -> selected s.S.m { e with left = node_model l.m.lis d.P.Data.m e.left } } - + use import ref.Ref - + let ghost default_position () : position 'a 'b = { left = Nil; middle = None; right = Nil } - + let rec add (ghost r:ref (position 'a 'b)) (s:S.t 'a 'b) (d:P.Data.t 'a 'b) (t:t 'a 'b) : t 'a 'b requires { selector_correct s.S.m t.m.lis } @@ -746,7 +744,7 @@ module Selection node tl d tr end end - + let rec remove (ghost r:ref (position 'a 'b)) (s:S.t 'a 'b) (t:t 'a 'b) : t 'a 'b requires { selector_correct s.S.m t.m.lis } @@ -774,7 +772,7 @@ module Selection fuse tl tr end end - + let rec split (ghost r:ref (position 'a 'b)) (s:S.t 'a 'b) (t:t 'a 'b) : (t 'a 'b,option (P.Data.t 'a 'b),t 'a 'b) requires { selector_correct s.S.m t.m.lis } @@ -804,7 +802,7 @@ module Selection (tl,Some td,tr) end end - + let rec get (ghost r:ref (position 'a 'b)) (s:S.t 'a 'b) (t:t 'a 'b) : option (P.Data.t 'a 'b) requires { selector_correct s.S.m t.m.lis } @@ -831,7 +829,7 @@ module Selection Some td end end - + let rec mem (ghost r:ref (position 'a 'b)) (s:S.t 'a 'b) (t:t 'a 'b) : bool requires { selector_correct s.S.m t.m.lis } @@ -856,7 +854,7 @@ module Selection true end end - + end (* @@ -864,17 +862,16 @@ end (* Instantiation to sorted (increasing) avl. Those implement ordered associative tables. *) module AVLSorted - + use import int.Int use import option.Option use import bool.Bool - use import HighOrd use import list.Append use import list.Mem use import list.Length - + clone import AVL as A - + (* Key used for ordering. *) type key 'a type key_model 'a @@ -894,10 +891,10 @@ module AVLSorted type A.KT.key = key_model, type A.KT.t = data_model, type A.param = order - - + + (* - + (* Comparison is computable. *) val compare (o:order 'a) (k1 k2:key 'a) : int requires { correct_for_order o (key_model k1) /\ key_correct k1 } @@ -905,21 +902,21 @@ module AVLSorted ensures { result > 0 <-> lt o (key_model k2) (key_model k1) } ensures { result < 0 <-> lt o (key_model k1) (key_model k2) } ensures { result = 0 <-> eq o (key_model k1) (key_model k2) } - + predicate majorate (o:order 'a) (k:key_model 'a) (l:list_model 'a 'b) = forall d0. mem d0 l -> let k0 = get_key_m d0 in correct_for_order o k0 /\ lt o k0 k - + predicate minorate (o:order 'a) (k:key_model 'a) (l:list_model 'a 'b) = forall d0. mem d0 l -> let k0 = get_key_m d0 in correct_for_order o k0 /\ lt o k k0 - + predicate sorted (o:order 'a) (l:list_model 'a 'b) = match l with | Nil -> true | Cons d q -> let k = get_key_m d in correct_for_order o k /\ minorate o k q /\ sorted o q end - + (* Sorted with a midpoint. *) let rec lemma sorted_def_midpoint (o:order 'a) (l:list_model 'a 'b) (d:data_model 'a 'b) (r:list_model 'a 'b) : unit @@ -935,12 +932,12 @@ module AVLSorted | Nil -> () | Cons _ ql -> sorted_def_midpoint o ql d r end - + predicate before (o:order 'a) (l:list_model 'a 'b) (r:list_model 'a 'b) = forall d1 d2. mem d1 l /\ mem d2 r -> let k1 = get_key_m d1 in let k2 = get_key_m d2 in correct_for_order o k1 /\ correct_for_order o k2 /\ lt o k1 k2 - + (* Other variant: condition for a concatenation to be sorted. *) let rec lemma sorted_def_concat (o:order 'a) (l:list_model 'a 'b) (r:list_model 'a 'b) : unit @@ -952,21 +949,21 @@ module AVLSorted | Nil -> () | Cons _ ql -> sorted_def_concat o ql r end - + type position 'a 'b = { left : list_model 'a 'b; middle : option (data_model 'a 'b); right : list_model 'a 'b; } - + (* Selection will be done by ordered key. *) type selector 'a 'b = (order 'a,key 'a) - + (* Correctness is sortedness. *) predicate selector_correct (s:selector 'a 'b) (l:list_model 'a 'b) = let (o,k) = s in sorted o l /\ correct_for_order o (key_model k) /\ key_correct k - + (* Selected position is: - The position of the element equivalent to the key for the corresponding order. @@ -981,12 +978,12 @@ module AVLSorted eq o (get_key_m d) (key_model k) /\ correct_for_order o (get_key_m d) end - + (* Way to the position. *) type way 'a 'b= Left (selector 'a 'b) | Right (selector 'a 'b) | Here - + (* Way selection. *) let selected_way (s:selector 'a 'b) (l:avl 'a 'b) (d:data 'a 'b) (r:avl 'a 'b) : way 'a 'b @@ -1015,7 +1012,7 @@ module AVLSorted else if cmp > 0 then Right s else Here - + (* In an ideal world... 1) It would be nice to have the two cloned AVL modules unified (they are intended to be the same), as well as the two (identical) @@ -1030,26 +1027,26 @@ module AVLSorted lemma selected_append, lemma selector_correct_empty, val selected_way = selected_way*) - + (* And we would get this (or something close). Right now, this is done by hand. *) - + namespace import F use import ref.Ref - + lemma selected_append : forall s,e,l:list_model 'a 'b. selected s e l /\ selector_correct s l -> match e.middle with | Some d -> l = node_model e.left d e.right | None -> l = e.left ++ e.right end - + lemma selector_correct_empty : forall s:selector 'a 'b. selector_correct s (Nil:list_model 'a 'b) -> selected s { left = Nil ; middle = None ; right = Nil } (Nil:list_model 'a 'b) - + val ghost default_position () : position 'a 'b - + val add (ghost r:ref (position 'a 'b)) (s:selector 'a 'b) (d:data 'a 'b) (a:avl 'a 'b) : avl 'a 'b requires { selector_correct s a.model } @@ -1061,7 +1058,7 @@ module AVLSorted ensures { avl_correct result } ensures { result.data_inv = a.data_inv } writes { r } - + val remove (ghost r:ref (position 'a 'b)) (s:selector 'a 'b) (a:avl 'a 'b) : avl 'a 'b requires { selector_correct s a.model } @@ -1072,7 +1069,7 @@ module AVLSorted ensures { avl_correct result } ensures { result.data_inv = a.data_inv } writes { r } - + val split (ghost p:ref (position 'a 'b)) (s:selector 'a 'b) (a:avl 'a 'b) : (avl 'a 'b,option (data 'a 'b),avl 'a 'b) requires { avl_correct a } @@ -1085,7 +1082,7 @@ module AVLSorted | None -> true | Some d -> data_correct d /\ a.data_inv (data_model d) end /\ l.data_inv = a.data_inv /\ r.data_inv = a.data_inv } writes { p } - + val get (ghost p:ref (position 'a 'b)) (s:selector 'a 'b) (a:avl 'a 'b) : option (data 'a 'b) requires { avl_correct a } @@ -1096,7 +1093,7 @@ module AVLSorted | None -> true | Some d -> data_correct d /\ a.data_inv (data_model d) end } writes { p } - + val mem (ghost p:ref (position 'a 'b)) (s:selector 'a 'b) (a:avl 'a 'b) : bool requires { avl_correct a } @@ -1105,10 +1102,10 @@ module AVLSorted selected s !p a.model } writes { p } end - + (* Functional model. *) type fun_model 'a 'b = key_model 'a -> option (data_model 'a 'b) - + function functional_model (o:order 'a) (l:list_model 'a 'b) : fun_model 'a 'b = match l with @@ -1117,22 +1114,22 @@ module AVLSorted \y. if correct_for_order o y && eq o y (get_key_m x) then Some x else f0 y end - + type map 'a 'b = { avl_repr : avl 'a 'b; order : order 'a; ghost fmodel : fun_model 'a 'b; } - + function map_data_inv (m:map 'a 'b) : data_model 'a 'b -> bool = m.avl_repr.data_inv - + predicate map_correct (m:map 'a 'b) = avl_correct m.avl_repr /\ sorted m.order m.avl_repr.model /\ m.fmodel = functional_model m.order m.avl_repr.model /\ (forall d. m.map_data_inv d -> correct_for_order m.order (get_key_m d)) - + (* A key that is either minorated/majorated in some list is not represented in its functional model. *) let rec lemma fun_model_minorate (o:order 'a) (k:key_model 'a) @@ -1143,7 +1140,7 @@ module AVLSorted ensures { functional_model o l k = None } variant { l } = match l with Nil -> () | Cons _ ql -> fun_model_minorate o k ql end - + let rec lemma fun_model_majorate (o:order 'a) (k:key_model 'a) (l:list_model 'a 'b) (r:list_model 'a 'b) : unit requires { sorted o l } @@ -1152,7 +1149,7 @@ module AVLSorted ensures { functional_model o (l++r) k = functional_model o r k } variant { l } = match l with Nil -> () | Cons _ ql -> fun_model_majorate o k ql r end - + let rec lemma fun_model_selected (o:order 'a) (k:key 'a) (p:position 'a 'b) (l:list_model 'a 'b) (ks:key_model 'a) : unit requires { selected (o,k) p l } @@ -1193,7 +1190,7 @@ module AVLSorted && not eq o kpl ks }; fun_model_selected o k { p with left = qpl } ql ks end - + let rec lemma fun_model_concat (o:order 'a) (k:key_model 'a) (l:list_model 'a 'b) (r:list_model 'a 'b) : unit requires { sorted o l } @@ -1208,8 +1205,8 @@ module AVLSorted functional_model o (l++r) k = Some d } variant { l } = match l with Nil -> () | Cons _ ql -> fun_model_concat o k ql r end - - + + (* (* Functional model of a concatenation. *) let rec lemma fun_model_concat (o:order 'a) (k:key_model 'a) @@ -1221,7 +1218,7 @@ module AVLSorted ensures { functional_model o (l++r) k = functional_model o l k } variant { l } = match l with Nil -> () | Cons _ ql -> fun_model_concat o k ql r end - + (* Node selection. *) let rec lemma fun_model_node (o:order 'a) (k:key_model 'a) (l:list_model 'a 'b) (d:data_model 'a 'b) (r:list_model 'a 'b) : unit @@ -1231,14 +1228,14 @@ module AVLSorted ensures { functional_model o (node_model l d r) k = Some d } variant { l } = match l with Nil -> () | Cons _ ql -> fun_model_node o k ql d r end*) - + let rec lemma fun_model_incorrect (o:order 'a) (k:key_model 'a) (l:list_model 'a 'b) : unit requires { not(correct_for_order o k) } ensures { functional_model o l k = None } variant { l } = match l with Nil -> () | Cons _ ql -> fun_model_incorrect o k ql end - + let rec lemma fun_model_nonnone (o:order 'a) (d:data_model 'a 'b) (l:list_model 'a 'b) : unit requires { sorted o l } @@ -1250,9 +1247,9 @@ module AVLSorted then fun_model_nonnone o d ql else () end - + use import ref.Ref - + let map_empty (o:order 'a) (inv:data_model 'a 'b -> bool) : map 'a 'b requires { forall d. inv d -> correct_for_order o (get_key_m d) } ensures { result.order = o } @@ -1264,7 +1261,7 @@ module AVLSorted { avl_repr = rp; order = o; fmodel = functional_model o rp.model } - + let map_singleton (o:order 'a) (inv:data_model 'a 'b -> bool) (d:data 'a 'b) : map 'a 'b requires { forall d. inv d -> correct_for_order o (get_key_m d) } @@ -1285,7 +1282,7 @@ module AVLSorted { avl_repr = rp; order = o; fmodel = functional_model o rp.model } - + let map_add (d:data 'a 'b) (m:map 'a 'b) : map 'a 'b requires { m.map_data_inv (data_model d) /\ data_correct d } requires { map_correct m } @@ -1309,7 +1306,7 @@ module AVLSorted assert { selected (o,k) { !r with middle = Some (data_model d) } res0.model }; res - + let map_mem (k:key 'a) (m:map 'a 'b) : bool requires { key_correct k /\ correct_for_order m.order (key_model k) } requires { map_correct m } @@ -1319,7 +1316,7 @@ module AVLSorted let ghost r = ref (default_position ()) in let o = m.order in mem r (o,k) m.avl_repr - + let map_remove (k:key 'a) (m:map 'a 'b) : map 'a 'b requires { key_correct k /\ correct_for_order m.order (key_model k) } requires { map_correct m } @@ -1340,8 +1337,8 @@ module AVLSorted fmodel = functional_model o res0.model } in assert { selected (o,k) { !r with middle = None } res0.model }; res - - + + let map_find (k:key 'a) (m:map 'a 'b) : option (data 'a 'b) requires { key_correct k /\ correct_for_order m.order (key_model k) } requires { map_correct m } @@ -1354,7 +1351,7 @@ module AVLSorted let ghost r = ref (default_position ()) in let o = m.order in get r (o,k) m.avl_repr - + let map_split (k:key 'a) (m:map 'a 'b) : (map 'a 'b,option (data 'a 'b),map 'a 'b) requires { key_correct k /\ correct_for_order m.order (key_model k) } @@ -1391,7 +1388,7 @@ module AVLSorted order = m.order; fmodel = functional_model o r0.model } in (l,o0,r) - + let map_concat (m1 m2:map 'a 'b) : map 'a 'b requires { map_correct m1 /\ map_correct m2 /\ m1.map_data_inv = m2.map_data_inv /\ diff --git a/examples/in_progress/bigInt.mlw b/examples/in_progress/bigInt.mlw index bb9335702eebf84f1beaaf5548efcf16cb2ff7ac..9f0b2b6bae1e5787390a2155a342daeef4e2ecf2 100644 --- a/examples/in_progress/bigInt.mlw +++ b/examples/in_progress/bigInt.mlw @@ -48,7 +48,7 @@ module N to_int (Map.get x n) + base * value_sub x (n+1) m l else 0 - use map.MapEq + use import map.MapEq let rec lemma value_sub_frame (x y:map int int31) (n m l:int) requires { MapEq.map_eq_sub x y n m } @@ -479,7 +479,7 @@ module Z to_int (Map.get x n) + base * value_sub x (n+1) m l else 0 - use map.MapEq + use import map.MapEq let rec lemma value_sub_frame (x y:map int int31) (n m l:int) requires { MapEq.map_eq_sub x y n m } diff --git a/examples/in_progress/mini-compiler-backward/logic.mlw b/examples/in_progress/mini-compiler-backward/logic.mlw index 60374054a9d24e30d139025adf0ac7835a08fb2a..90a8add1588efc43d983308854265be391882ba9 100644 --- a/examples/in_progress/mini-compiler-backward/logic.mlw +++ b/examples/in_progress/mini-compiler-backward/logic.mlw @@ -7,7 +7,6 @@ module Compiler_logic use import vm.Vm use import vm.VMClock use import state.State - use import HighOrd function fst (p: ('a,'b)) : 'a = let (x,_) = p in x meta rewrite_def function fst diff --git a/examples/in_progress/mini-compiler-backward/specs.mlw b/examples/in_progress/mini-compiler-backward/specs.mlw index 78f6dbc5001c8d9b141ea831c5b8b59c8d922c7a..067bf43553ec0d76d7d959baf64246b9fe0b89eb 100644 --- a/examples/in_progress/mini-compiler-backward/specs.mlw +++ b/examples/in_progress/mini-compiler-backward/specs.mlw @@ -9,14 +9,13 @@ module VM_instr_spec use import vm.Vm use import vm.VMClock use import state.State - use import HighOrd use import logic.Compiler_logic function ifun_post (f:machine_state -> machine_state) : post 'a = \x p mc mc'. let VMC p s m c = mc in let VMC p' s' m' c' = mc' in VMS p' s' m' = f (VMS p s m) /\ c' = c + 1 meta rewrite_def function ifun_post - + let ifunf (ghost pre:pre 'a) (code_f:code) (ghost f:machine_state -> machine_state) : hl 'a requires { forall c p. codeseq_at c p code_f -> @@ -55,7 +54,7 @@ module VM_instr_spec \a p ms ms'. forall s m clock. ms = VMC p s m clock -> ms' = VMC (p+1) (push m[x] s) m (clock+1) meta rewrite_def function ivar_post - + function ivar_fun (x:id) : machine_state -> machine_state = \ms. let VMS p s m = ms in VMS (p+1) (push m[x] s) m meta rewrite_def function ivar_fun @@ -149,7 +148,7 @@ module VM_instr_spec (cond n1 n2 -> ms' = VMC (p + ofs + 1) s m (c+1)) /\ (not cond n1 n2 -> ms' = VMC (p+1) s m (c+1)) meta rewrite_def function icjump_post - + function icjump_fun (cond:cond) (ofs:int) : machine_state -> machine_state = \ms. match ms with | VMS p (Cons n2 (Cons n1 s)) m -> diff --git a/examples/in_progress/mini-compiler-backward/vm.mlw b/examples/in_progress/mini-compiler-backward/vm.mlw index 7c77e80c5a0dcaa19d5a8971b21ae2ba3ee3f289..f558632b1b60a55a5728de698a0425936a49bfc0 100644 --- a/examples/in_progress/mini-compiler-backward/vm.mlw +++ b/examples/in_progress/mini-compiler-backward/vm.mlw @@ -147,8 +147,7 @@ module Vm "Virtual Machine for IMP language" end module VMClock - - use import HighOrd + use import state.State use import int.Int use import list.List @@ -158,44 +157,44 @@ module VMClock use import list.NthLengthAppend use import option.Option use import Vm - + type clock_state = VMC pos stack state int type parameter = (code,clock_state -> bool) - + predicate transition_out (p:(code,clock_state -> bool)) (mc1 mc2:clock_state) = let (c,inside) = p in not inside mc1 /\ not inside mc2 /\ let VMC p1 s1 m1 c1 = mc1 in let VMC p2 s2 m2 c2 = mc2 in transition c (VMS p1 s1 m1) (VMS p2 s2 m2) /\ c2 = c1 + 1 - + clone ReflTransClosure as C with type parameter = parameter, type state = clock_state, predicate transition = transition_out - + lemma transition_star_endpoints : forall c p s0 s1. C.transition_star (c,p) s0 s1 -> s0 <> s1 -> not p s0 /\ not p s1 - + lemma transition_star_weakening : forall c p q s0 s1. (forall x. q x -> p x) -> C.transition_star (c,p) s0 s1 -> C.transition_star (c,q) s0 s1 - + let lemma transition_deterministic (c:code) (ms ms' ms'':machine_state) : unit requires { transition c ms ms' } requires { transition c ms ms'' } ensures { ms' = ms'' } = assert { forall p i. ("inversion" codeseq_at c p (Cons i Nil)) -> nth p c = Some i } - + lemma transition_out_deterministic : forall p mc1 mc2 mc3. transition_out p mc1 mc2 /\ transition_out p mc1 mc3 -> mc2 = mc3 - - + + let lemma halt_stuck (c:code) (p:pos) (s:stack) (m:state) : unit requires { codeseq_at c p ihalt } ensures { forall ms'. not transition c (VMS p s m) ms' } = assert { forall p i. codeseq_at c p (Cons i Nil) -> nth p c = Some i } - + end (* diff --git a/examples/in_progress/multiprecision/mp2.mlw b/examples/in_progress/multiprecision/mp2.mlw index 3a8e6c861344a9094f8bf0e021a403c1b7bf9f26..938e94857bb65049036a0042b0c6586f4aa168fc 100644 --- a/examples/in_progress/multiprecision/mp2.mlw +++ b/examples/in_progress/multiprecision/mp2.mlw @@ -54,8 +54,8 @@ module N use import array.Array use import map.Map - use map.MapEq - use map.Const + use import map.MapEq + use import map.Const use import int.Int (** {3 complements to map standard library} *) diff --git a/examples/in_progress/next_digit_sum.mlw b/examples/in_progress/next_digit_sum.mlw index 28fac3848311de1277f9c66fa9183fe845d9c897..29509a85a8af9e4ebba4f7a7b351b12a78c2e02b 100644 --- a/examples/in_progress/next_digit_sum.mlw +++ b/examples/in_progress/next_digit_sum.mlw @@ -43,7 +43,7 @@ module M = if i < j then interp_eq x1 x2 (i+1) j (* the sum of the elements of x[i..j[ *) - use int.Sum + use import int.Sum function sum (m: M.map int int) (i j: int) : int = Sum.sum (fun k -> M.get m k) i (j - 1) diff --git a/examples/in_progress/sudoku_reloaded.mlw b/examples/in_progress/sudoku_reloaded.mlw index 89c36e60cb550a9e971789be1f7a4cb280c0a3be..05b181894ee17ffd8e1cd2cce462ef206fecda1c 100644 --- a/examples/in_progress/sudoku_reloaded.mlw +++ b/examples/in_progress/sudoku_reloaded.mlw @@ -662,7 +662,7 @@ module Test use import TheClassicalSudokuGrid use import Solver - use mach.array.Array31 + use import mach.array.Array31 use import map.Map use import mach.int.Int31 diff --git a/examples/in_progress/sum_of_digits.mlw b/examples/in_progress/sum_of_digits.mlw index cd0f3c996f3a7062675886d960fe51063b724135..1957aa069a92693c044ba98a9d4caa8c72b900e0 100644 --- a/examples/in_progress/sum_of_digits.mlw +++ b/examples/in_progress/sum_of_digits.mlw @@ -21,7 +21,7 @@ module Euler290 use import ref.Ref use import int.EuclideanDivision as E use import int.Power - use int.NumOf + use import int.NumOf function sum_digits int : int diff --git a/examples/in_progress/union_find.mlw b/examples/in_progress/union_find.mlw index 4192364c8b293a5420f5c9d414d8f56ea34824b1..4ff450b2b60c7f2e3976af3bbe0450f6951e173d 100644 --- a/examples/in_progress/union_find.mlw +++ b/examples/in_progress/union_find.mlw @@ -39,7 +39,6 @@ end module Impl use import int.Int - use map.Map use import array.Array (* there is a path from x to y of length at most d *) @@ -182,7 +181,7 @@ module Impl end - clone Intf with + clone import Intf with type t = t, val create = create, val find = find, diff --git a/examples/in_progress/why3_logic/support.mlw b/examples/in_progress/why3_logic/support.mlw index 1896cbd9669e326c1b8657529556f430b0062a53..0cf5af4246dfd38373be5c46b379b26f30057f6d 100644 --- a/examples/in_progress/why3_logic/support.mlw +++ b/examples/in_progress/why3_logic/support.mlw @@ -17,45 +17,43 @@ end (* Higher-order miscellaneous support definitions. *) module HO - - use export HighOrd - + predicate extensional_equal (f g:'a -> 'b) = forall x. f x = g x - + function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c = \x. g (f x) function rcompose (f:'a -> 'b) (g:'b -> 'c) : 'a -> 'c = compose g f - + function id : 'a -> 'a = \x.x - + function const (x:'b) : 'a -> 'b = \_.x - + function ho_ite (p:'a -> bool) (th:'a -> 'b) (el:'a -> 'b) : 'a -> 'b = \x. if p x then th x else el x - + function update (f:'a -> 'b) (x:'a) (y:'b) : 'a -> 'b = \z. if z = x then y else f z - + function ([ <- ]) (f:'a -> 'b) (x:'a) (y:'b) : 'a -> 'b = update f x y - + constant all : 'a -> bool = \_.true constant none : 'a -> bool = \_.false - + function union (a b:'a -> bool) : 'a -> bool = \x. a x \/ b x - + predicate subset (a b:'a -> bool) = forall x. a x -> b x - + predicate maps_to (a:'a -> bool) (f:'a -> 'b) (b:'b -> bool) = forall x. a x -> b (f x) - + predicate equalizer (a:'a -> bool) (f g:'a -> 'b) = forall x. a x -> f x = g x - + use import int.Int - + function range (a b:int) : int -> bool = \x. a <= x < b - + end (* The verification of the following modules is delayed to the HOProof module. @@ -64,7 +62,7 @@ end The advantage of this otherwise complex setup is that the part of the context that is needed to carry proof does not have to be exported along the properties, hence considerably limiting context explosion. - + The trade-off is that the system unfortunately does not check yet the correct integration between the declaration and the proof module, so the following things could happen (and their absence @@ -76,7 +74,7 @@ end (missing axiom<-goals substitutions) (thankfully, it is enough to check whether the count of axiom declarations and goal substitutions coincides) - + This mechanism triggers a lot of warnings on a normal setup because: 1) The cloned theory does not contains abstract symbols 2) The axioms we write does not contains abstract symbols neither. @@ -87,121 +85,121 @@ end to the provers) *) module HOExt - + clone import Dummy as DHOExt use export HO - + axiom extensionality : forall f g:'a -> 'b. extensional_equal f g -> f = g /\ forall _:d.true - + let ghost extensionality (f g:'a -> 'b) requires { extensional_equal f g } ensures { f = g } = () - + end module HOCompose - + clone import Dummy as DHOCompose use export HO - + axiom compose_associative : forall f:'a -> 'b,g:'b -> 'c,h:'c -> 'd. compose (compose h g) f = compose h (compose g f) /\ forall _:d.true - + axiom id_neutral : forall f:'a -> 'b. compose f id = f = compose id f /\ forall _:d.true - + end module HOConst - + clone import Dummy as DHOConst use export HO - + axiom compose_const_right : forall x:'c,f:'a -> 'b. compose (const x) f = const x /\ forall _:d.true - + axiom compose_const_left : forall x:'b,f:'b -> 'c. compose f (const x:'a -> 'b) = const (f x) /\ forall _:d.true - + end module HOIte - + clone import Dummy as DHOIte use export HO - + axiom ho_ite_compose_left : forall p,th el:'a -> 'b,f:'b -> 'c. compose f (ho_ite p th el) = ho_ite p (compose f th) (compose f el) /\ forall _:d.true - + axiom ho_ite_compose_right : forall p,th el:'b -> 'c,f:'a -> 'b. compose (ho_ite p th el) f = ho_ite (compose p f) (compose th f) (compose el f) /\ forall _:d.true - + end module HOFull - + use export HOExt use export HOCompose use export HOConst use export HOIte - + end module HOProof - + use import HO use import NoDiscriminate - + predicate hack (f g h:'a -> 'b) = f = g = h let lemma extensionality (f g:'a -> 'b) requires { extensional_equal f g } ensures { f = g } = assert { hack f (\x.f x) g } - + let lemma id_neutral (f:'a -> 'b) ensures { compose f id = f = compose id f } = assert { extensional_equal f (compose f id) /\ extensional_equal (compose id f) f } - + let lemma compose_associative (f:'a -> 'b) (g:'b -> 'c) (h:'c -> 'd) (a b:'a -> 'd) requires { a = compose h (compose g f) /\ b = compose (compose h g) f } ensures { a = b } = assert { extensional_equal a b } - + let lemma compose_const_left (x:'b) (f:'b -> 'c) (a:'a -> 'c) requires { a = compose f (const x) } ensures { a = const (f x) } = assert { extensional_equal a (const (f x)) } - + let lemma compose_const_right (x:'c) (f:'a -> 'b) ensures { const x = compose (const x) f } = assert { extensional_equal (const x) (compose (const x) f) } - + let lemma ho_ite_compose_left (p:'a -> bool) (th el:'a -> 'b) (f:'b -> 'c) (a b:'a -> 'c) requires { a = compose f (ho_ite p th el) } requires { b = ho_ite p (compose f th) (compose f el) } ensures { a = b } = assert { extensional_equal a b } - + let lemma ho_ite_compose_right (p:'b -> bool) (th el:'b -> 'c) (f:'a -> 'b) (a b:'a -> 'c) requires { a = compose (ho_ite p th el) f } requires { b = ho_ite (compose p f) (compose th f) (compose el f) } ensures { a = b } = assert { extensional_equal a b } - + clone HOExt with type DHOExt.d = unit, goal extensionality clone HOCompose with type DHOCompose.d = unit, @@ -210,98 +208,98 @@ module HOProof goal compose_const_left, goal compose_const_right clone HOIte with type DHOIte.d = unit, goal ho_ite_compose_left, goal ho_ite_compose_right - + end module PartialMap - + use import HO use import option.Option - + type pmap 'a 'b = 'a -> option 'b - + function extend (m1:'a -> option 'b) (m2:'a -> option 'b) : 'a -> option 'b = \x. match m1 x with | None -> m2 x | s -> s end - + function domain (m:'a -> option 'b) : 'a -> bool = \x. m x <> None - + function complete (m:'a -> option 'b) (d:'a -> 'b) : 'a -> 'b = \x. match m x with | None -> d x | Some x -> x end - + end module Bind - + use import HO - + type bind 'a 'b = | Old 'a | Fresh 'b - + function bfold (o:'a -> 'c) (f:'b -> 'c) : bind 'a 'b -> 'c = \x. match x with Old x -> o x | Fresh y -> f y end - + (* For the practical use cases (representing binders), there is no need to map over the second component. ==> Keep the function simple. *) function bmap (f:'a -> 'b) : bind 'a 'c -> bind 'b 'c = bfold (compose Old f) Fresh - + end (* Proof delegated to BindProof. *) module BindFull - + clone import Dummy as DBindFull use import HO use export Bind - + axiom bfold_identity : bfold Old Fresh = (id:bind 'a 'b -> bind 'a 'b) /\ forall _:d.true - + axiom bfold_compose : forall o:'a -> 'c,f:'b -> 'c,g:'c -> 'd. compose g (bfold o f) = bfold (compose g o) (compose g f) /\ forall _:d.true - + axiom bfold_constructor : forall o:'a -> 'c,f:'b -> 'c. compose (bfold o f) Old = o /\ compose (bfold o f) Fresh = f /\ forall _:d.true - + axiom bfold_all : bfold all all = (all:bind 'a 'b -> bool) /\ forall _:d.true - + axiom bfold_map_compose : forall a:'a -> 'b,o:'b -> 'e,f:'c -> 'e. compose (bfold o f) (bmap a) = bfold (compose o a) f /\ forall _:d.true - + axiom bmap_compose : forall g:'b -> 'c,f:'a -> 'b. bmap (compose g f) = compose (bmap g) (bmap f:bind 'a 'd -> bind 'b 'd) /\ forall _:d.true - + axiom bmap_identity : bmap id = (id:bind 'a 'b -> bind 'a 'b) /\ forall _:d.true - + end module BindProof - + use import HOFull use import Bind use import NoDiscriminate - + let lemma bfold_identity () ensures { bfold Old Fresh = (id:bind 'a 'b -> bind 'a 'b) } = assert { extensional_equal (bfold Old Fresh) (id:bind 'a 'b -> bind 'a 'b) } - + let lemma bfold_compose (o:'a -> 'c) (f:'b -> 'c) (g:'c -> 'd) ensures { compose g (bfold o f) = bfold (compose g o) (compose g f) } = assert { let a = compose g (bfold o f) in @@ -309,17 +307,17 @@ module BindProof not(extensional_equal a b) -> (forall x. a x <> b x -> match x with | Old _ -> a x = b x && false | Fresh _ -> false end && false) && false } - + let lemma bfold_constructor (o:'a -> 'c) (f:'b -> 'c) ensures { compose (bfold o f) Old = o } ensures { compose (bfold o f) Fresh = f } = assert { extensional_equal (compose (bfold o f) Old) o /\ extensional_equal (compose (bfold o f) Fresh) f } - + let lemma bfold_all () : unit ensures { bfold all all = (all:bind 'a 'b -> bool) } = extensionality (bfold all all) (all:bind 'a 'b -> bool) - + clone BindFull with type DBindFull.d = unit, goal bfold_identity, goal bfold_compose, @@ -328,43 +326,43 @@ module BindProof goal bmap_compose, goal bmap_identity, goal bfold_map_compose - + end (* Useful higher-order definition about lists. *) module HOList - + use import list.List use import list.Nth use import option.Option use import HO - + function map (f:'a -> 'b) (l:list 'a) : list 'b = match l with | Nil -> Nil | Cons x q -> Cons (f x) (map f q) end - + predicate for_all (p:'a -> bool) (l:list 'a) = match l with | Nil -> true | Cons x q -> p x /\ for_all p q end - + predicate exist (p:'a -> bool) (l:list 'a) = match l with | Nil -> false | Cons x q -> p x \/ exist p q end - + function list_nth (l:list 'a) (d:int -> 'a) : int -> 'a = \n. match nth n l with | None -> d n | Some x -> x end - + end (* Delayed proof in HOListProof. *) module HOListFull - + clone import Dummy as DHOListFull use import list.List use import list.Nth @@ -372,34 +370,34 @@ module HOListFull use import option.Option use import HO use export HOList - + axiom map_nth : forall f:'a -> 'b,l:list 'a,n:int. nth n (map f l) = match nth n l with None -> None | Some x -> Some (f x) end /\ forall _:d. true - + axiom map_nth2 : forall f:'a -> 'b,l:list 'a,n:int. match nth n (map f l) with | None -> nth n l = None | Some x -> exists y. nth n l = Some y /\ f y = x end /\ forall _:d. true - + axiom map_length : forall f:'a -> 'b,l:list 'a. length (map f l) = length l /\ forall _:d. true - + axiom for_all_nth : forall p:'a -> bool,l:list 'a. for_all p l <-> forall n. match nth n l with Some x -> p x | _ -> true end /\ forall _:d.true - + axiom exist_nth : forall p:'a -> bool,l:list 'a. exist p l <-> exists n y. nth n l = Some y /\ p y /\ forall _:d.true - + end module HOListProof - + use import list.List use import list.Nth use import list.NthLength @@ -408,7 +406,7 @@ module HOListProof use import int.Int use import HOList use import NoDiscriminate - + let rec lemma map_nth (f:'a -> 'b) (l:list 'a) (n:int) : unit ensures { nth n (map f l) = match nth n l with | None -> None @@ -416,19 +414,19 @@ module HOListProof end } variant { l } = match l with Cons _ q -> map_nth f q (n-1) | _ -> () end - + let lemma map_nth2 (f:'a -> 'b) (l:list 'a) (n:int) : unit ensures { match nth n (map f l) with | None -> nth n l = None | Some x -> exists y. nth n l = Some y /\ f y = x end } = match nth n l with None -> "keep_on_simp" () | _ -> () end - + let rec lemma map_length (f:'a -> 'b) (l:list 'a) : unit ensures { length (map f l) = length l } variant { l } = match l with Cons _ q -> map_length f q | _ -> () end - + let rec lemma for_all_nth (p:'a -> bool) (l:list 'a) : unit ensures { for_all p l <-> forall n. match nth n l with Some x -> p x | _ -> true end } @@ -441,7 +439,7 @@ module HOListProof for_all p q && nth 0 l = Some x && for_all p l } | _ -> () end - + let rec lemma exist_nth (p:'a -> bool) (l:list 'a) : unit ensures { exist p l <-> exists n y. nth n l = Some y /\ p y } variant { l } @@ -452,20 +450,19 @@ module HOListProof (forall n y. nth n q = Some y /\ p y -> nth (n+1) l = Some y) } | _ -> () end - + clone HOListFull with type DHOListFull.d = unit, goal map_nth, goal map_nth2, goal map_length, goal for_all_nth, goal exist_nth - + end (* Axiomatic module: arbitrary choice. *) module Choice - - use import HighOrd + use import option.Option constant default : 'a function choice (p:'a -> bool) : 'a @@ -478,11 +475,11 @@ module Choice returns { Some x -> p x | None -> forall x. not (p x) } = let u = choice p in if p u then Some u else None - + end module Finite - + use import HO use import Choice use import int.Int @@ -490,20 +487,20 @@ module Finite n >= 0 /\ exists f g. (forall x. range 0 n x -> p (f x) /\ g (f x) = x) /\ (forall x. p x -> range 0 n (g x) /\ f (g x) = x) - + predicate finite (p:'a -> bool) = exists n. equirange p n function cardinal (p:'a -> bool) : int = choice (equirange p) - + end (* Proof delegated to FiniteProof. *) module FiniteFull - + clone import Dummy as DFiniteFull use import HO use import int.Int use export Finite - + axiom finite_empty : finite (none:'a -> bool) /\ forall _:d.true axiom finite_add : forall x,y:'a. finite x -> finite (update x y true) @@ -539,7 +536,7 @@ module FiniteFull /\ forall _:d.true axiom cardinal_range : forall a b. a <= b -> cardinal (range a b) = b-a /\ forall _:d.true - + end module FiniteProof @@ -550,14 +547,14 @@ module FiniteProof use import Finite use import option.Option use import NoDiscriminate - + predicate equirange_with (n:int) (p:'a -> bool) (f:int -> 'a) (g:'a -> int) = (forall x. range 0 n x -> p (f x) /\ g (f x) = x) /\ (forall x. p x -> range 0 n (g x) /\ f (g x) = x) - + lemma equirange_def : forall n,p:'a -> bool. equirange p n <-> (n >= 0 /\ exists f g. equirange_with n p f g) - + let lemma equirange_add (n:int) (p:'a -> bool) (x:'a) (f:int -> 'a) (g:'a -> int) requires { equirange_with n p f g /\ not p x /\ n >= 0 } @@ -565,7 +562,7 @@ module FiniteProof = let f2 = f[n <- x] in let g2 = g[x <- n] in assert { equirange_with (n+1) (update p x true) f2 g2 } - + let lemma equirange_remove (n:int) (p:'a -> bool) (x:'a) (f:int -> 'a) (g:'a -> int) requires { equirange_with n p f g /\ p x } @@ -578,7 +575,7 @@ module FiniteProof let g2 = g[y <- i] in assert { extensional_equal (range 0 m) (update (range 0 n) m false) }; assert { equirange_with m (update p x false) f2 g2 } - + let rec lemma equirange_unique (n m:int) (p:'a -> bool) requires { equirange p n /\ equirange p m /\ n >= 0 /\ m >= 0 } ensures { n = m } @@ -588,40 +585,40 @@ module FiniteProof then equirange_unique (n-1) (m-1) (update p x false) else assert { forall u. equirange p u -> u > 0 -> (forall f g. equirange_with u p f g -> p (f 0) && false) && false } - + lemma equirange_cardinal : forall p:'a -> bool. finite p <-> equirange p (cardinal p) - + let lemma cardinal_empty (a:'a -> bool) requires { a = none } ensures { finite a } ensures { cardinal a = 0 } = assert { equirange_with 0 a default default } - + let lemma finite_add (p:'a -> bool) (x:'a) requires { finite p } ensures { finite (update p x true) } = if p x then assert { extensional_equal p (update p x true) } - + let lemma finite_remove (p:'a -> bool) (x:'a) requires { finite p } ensures { finite (update p x false) } = if p x then assert { extensional_equal (update (update p x false) x true) p } else assert { extensional_equal (update p x false) p } - + let lemma cardinal_remove (p:'a -> bool) (x:'a) requires { finite p /\ p x } ensures { cardinal (update p x false) = cardinal p - 1 } = assert { equirange (update p x false) (cardinal p - 1) } - + let lemma cardinal_add (p:'a -> bool) (x:'a) requires { finite p /\ not p x } ensures { cardinal (update p x true) = cardinal p + 1 } = assert { equirange (update p x true) (cardinal p + 1) } - + function diff (a b:'a -> bool) : 'a -> bool = \x. a x /\ not (b x) - + let rec lemma cardinal_subset (p1 p2:'a -> bool) requires { finite p1 /\ subset p2 p1 } ensures { finite p2 /\ cardinal p2 <= cardinal p1 } @@ -630,13 +627,13 @@ module FiniteProof | Some x -> cardinal_subset (update p1 x false) p2 | None -> assert { subset p1 p2 && extensional_equal p1 p2 } end - + let lemma cardinal_zero (p:'a -> bool) requires { finite p /\ cardinal p = 0 } ensures { p = none } = assert { forall x. p x -> (exists y. range 0 0 y) && false }; extensionality p none - + let rec lemma cardinal_eq_subset (p1 p2:'a -> bool) requires { finite p2 /\ subset p1 p2 } requires { cardinal p1 = cardinal p2 } @@ -647,7 +644,7 @@ module FiniteProof extensionality p1 p2 | None -> extensionality p1 none end - + let rec lemma finite_union (p1 p2:'a -> bool) requires { finite p1 /\ finite p2 } ensures { finite (union p1 p2) } @@ -658,14 +655,14 @@ module FiniteProof let u = union (update p1 x true) (update p2 x false) in assert { extensional_equal u (union p1 p2) } else assert { extensional_equal p1 (union p1 p2) } - + let lemma finite_range (a b:int) : unit ensures { finite (range a b) } ensures { a <= b -> cardinal (range a b) = b - a } = if a > b then extensionality (range a b) none else assert { equirange_with (b-a) (range a b) ((+) a) ((+) (-a)) } - + clone FiniteFull with type DFiniteFull.d = unit, goal finite_empty, goal finite_add, @@ -680,6 +677,6 @@ module FiniteProof goal cardinal_eq_subset, goal finite_range, goal cardinal_range - + end diff --git a/examples/insertion_sort_list.mlw b/examples/insertion_sort_list.mlw index 6dfc458b6cea44653bee58503ec102d7236333d8..bbcb91221019e5b9aa24d94d054c6822a2625bea 100644 --- a/examples/insertion_sort_list.mlw +++ b/examples/insertion_sort_list.mlw @@ -6,7 +6,7 @@ module InsertionSort type elt val predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . clone export list.Sorted with type t = elt, predicate le = le, goal Transitive.Trans diff --git a/examples/insertion_sort_naive.mlw b/examples/insertion_sort_naive.mlw index 57f155ee4f87ecf6f9419ef89488b971d8121624..414588e0298a28aabea8df333eac71ee205f3f49 100644 --- a/examples/insertion_sort_naive.mlw +++ b/examples/insertion_sort_naive.mlw @@ -107,7 +107,7 @@ module InsertionSortParam use import int.Int use import ref.Ref use import ref.Refint - use map.Map + use import map.Map use import array.Array use import array.ArrayPermut @@ -168,7 +168,7 @@ module InsertionSortParamBad use import int.Int use import ref.Ref use import ref.Refint - use map.Map + use import map.Map use import array.Array use import array.ArrayPermut diff --git a/examples/inverse_in_place.mlw b/examples/inverse_in_place.mlw index 61414cbe4cbe8d2420d87dadad18a9f1bfe2ebe6..33901cfb1f147083b2c0c25fa3291b234a4d72bd 100644 --- a/examples/inverse_in_place.mlw +++ b/examples/inverse_in_place.mlw @@ -18,7 +18,7 @@ module InverseInPlace use import int.Int - use int.NumOf + use import int.NumOf use import ref.Ref use import array.Array diff --git a/examples/leftist_heap.mlw b/examples/leftist_heap.mlw index 4bd5c9493cb836af6172ebdf8e602f615720ae13..38d49d6ebbaf6aed64516ef9ef1af75246528077 100644 --- a/examples/leftist_heap.mlw +++ b/examples/leftist_heap.mlw @@ -14,7 +14,7 @@ module Heap type elt predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . type heap @@ -104,7 +104,7 @@ module LeftistHeap type elt val predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . use import TreeRank diff --git a/examples/linear_probing.mlw b/examples/linear_probing.mlw index b8c9d2829a962bc129108f95022eb72545e18c17..72607df1507a235d494b83eeba5ac83491816255 100644 --- a/examples/linear_probing.mlw +++ b/examples/linear_probing.mlw @@ -37,7 +37,7 @@ module LinearProbing use import option.Option use import list.Mem use import map.Map - use map.Const + use import map.Const use import ref.Ref use import array.Array @@ -52,7 +52,7 @@ module LinearProbing (** number of dummy values in array `a` between `l` and `u` *) scope NumOfDummy - use int.NumOf + use import int.NumOf function numof (a: array key) (l u: int) : int = NumOf.numof (fun i -> eq a[i] dummy) l u diff --git a/examples/linked_list_rev.mlw b/examples/linked_list_rev.mlw index 3c2dc8490bf36ea9ff6fff6629dbf35741a3b53f..f17eb366c5ef941570be53a2dc446dc7f2a95499 100644 --- a/examples/linked_list_rev.mlw +++ b/examples/linked_list_rev.mlw @@ -19,7 +19,7 @@ module InPlaceRev use import ref.Ref use import int.Int use import list.List - use list.Quant + use list.Quant as Q use import list.Append use import list.Mem use import list.Length @@ -200,7 +200,7 @@ end module InPlaceRevSeq use import int.Int - use map.Map + use map.Map as Map use import seq.Seq use import seq.Mem use import seq.Reverse diff --git a/examples/max_matrix.mlw b/examples/max_matrix.mlw index 23607d35fc4c64603be20428388cb48b1d584be7..33e0b79bbeaab091afb93dda9eb2962a5153ce73 100644 --- a/examples/max_matrix.mlw +++ b/examples/max_matrix.mlw @@ -89,7 +89,7 @@ module MaxMatrixMemo use import int.MinMax use import ref.Ref use import Bitset - use map.Map + use import map.Map clone import appmap.Appmap with type key = int, axiom . diff --git a/examples/maximum_subarray.mlw b/examples/maximum_subarray.mlw index a7c6380021c13ecd415a93b1b39567c1e5254cb7..fc0eda09076d183a29b6c8f8275bbff717bb393a 100644 --- a/examples/maximum_subarray.mlw +++ b/examples/maximum_subarray.mlw @@ -251,7 +251,7 @@ module BoundedIntegers use import mach.int.Refint63 use import seq.Seq use import mach.array.Array63 - use int.Sum + use import int.Sum function sum (a: array int63) (lo hi: int) : int = Sum.sum (fun i -> (a[i] : int)) lo hi diff --git a/examples/mergesort_array.mlw b/examples/mergesort_array.mlw index 075b26da6d8383587211c2ce03dea8d34eb777b5..cd2e58508cb02ccf8199c6729c3aa036890286e1 100644 --- a/examples/mergesort_array.mlw +++ b/examples/mergesort_array.mlw @@ -15,7 +15,7 @@ module Elt val predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . clone export array.Sorted with type diff --git a/examples/mergesort_list.mlw b/examples/mergesort_list.mlw index e73c5f3fcaa8e28739dd4ae262efabc37b2ee896..1904e8f2749f828eded92ca5fd758aa81878b181 100644 --- a/examples/mergesort_list.mlw +++ b/examples/mergesort_list.mlw @@ -14,7 +14,7 @@ module Elt type elt val predicate le elt elt - clone relations.TotalPreOrder + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . clone export list.Sorted with type t = elt, predicate le = le, goal Transitive.Trans diff --git a/examples/mergesort_queue.mlw b/examples/mergesort_queue.mlw index ab8953e352d41cc777a5fb65395382fc8105b259..aeeffc9a11a7922020a65e7d1c6ccce1ed2eeacd 100644 --- a/examples/mergesort_queue.mlw +++ b/examples/mergesort_queue.mlw @@ -15,7 +15,7 @@ module MergesortQueue type elt val predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . clone export list.Sorted with type t = elt, predicate le = le, goal Transitive.Trans diff --git a/examples/multiprecision/lemmas.mlw b/examples/multiprecision/lemmas.mlw index 61e1609d178836e50fb5622ccd72854f97ba67d7..63cdd557328efc8225c92efb1d4f0e9cd25e9480 100644 --- a/examples/multiprecision/lemmas.mlw +++ b/examples/multiprecision/lemmas.mlw @@ -2,8 +2,8 @@ module Lemmas use import array.Array use import map.Map - use map.MapEq - use map.Const + use import map.MapEq + use import map.Const use import int.Int (** {3 Complements to map standard library} *) diff --git a/examples/pairing_heap.mlw b/examples/pairing_heap.mlw index c99e3329315e81e9e82ecb009e152c31aceab21d..06e8ee73d5b7c6325374fca9e84524a5f764b59c 100644 --- a/examples/pairing_heap.mlw +++ b/examples/pairing_heap.mlw @@ -14,7 +14,7 @@ module Heap type elt val predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . type heap diff --git a/examples/pairing_heap_bin.mlw b/examples/pairing_heap_bin.mlw index 6950082a38d70c74bb76864a5752aec272573831..d3fa6e99e7d0f87c16fcc88ea10fd07331f07e30 100644 --- a/examples/pairing_heap_bin.mlw +++ b/examples/pairing_heap_bin.mlw @@ -14,7 +14,7 @@ module Heap type elt val predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . type heap diff --git a/examples/prover/Choice.mlw b/examples/prover/Choice.mlw index eeb5c95c633d56e242d4d985feef5007cca6886b..5570e8e1b31c5a6c38ed11fb224334f87f5202b7 100644 --- a/examples/prover/Choice.mlw +++ b/examples/prover/Choice.mlw @@ -1,18 +1,16 @@ module Choice - - use import HighOrd - + (* no why3 type is empty. *) - + constant default : 'a - + (* Axiom of choice : we can explicitely pick an element whom existence is proven. *) - + function choice (p: 'a -> bool) : 'a axiom choice_behaviour : forall p: 'a -> bool, x: 'a. p x -> p (choice p) - + end diff --git a/examples/prover/Firstorder_semantics.mlw b/examples/prover/Firstorder_semantics.mlw index 40497dd5109d78b990e94a6b37fd02242a3138c9..cc21e6408ae794661db1209005ac0684291282a6 100644 --- a/examples/prover/Firstorder_semantics.mlw +++ b/examples/prover/Firstorder_semantics.mlw @@ -3,7 +3,6 @@ module Sem use import Choice.Choice use import Functions.Func - use export HighOrd use import Firstorder_symbol_spec.Spec use import Firstorder_term_spec.Spec use import Firstorder_formula_spec.Spec diff --git a/examples/prover/Functions.mlw b/examples/prover/Functions.mlw index 9453c60e2337c54ae65c99babd6f45104f4cce56..6da4bbfd4d790634b71c22d087dbd0e630e59c7e 100644 --- a/examples/prover/Functions.mlw +++ b/examples/prover/Functions.mlw @@ -1,8 +1,6 @@ module Func - use export HighOrd - predicate extensionalEqual (f g:'a -> 'b) = forall x:'a. f x = g x diff --git a/examples/prover/Predicates.mlw b/examples/prover/Predicates.mlw index 503ddf1ae7da6885f0b659650a0239187c11bef4..98f7e9de97e8557813cf09b452b981157f237ddd 100644 --- a/examples/prover/Predicates.mlw +++ b/examples/prover/Predicates.mlw @@ -1,7 +1,6 @@ module Pred - use export HighOrd use import Functions.Func use import bool.Bool diff --git a/examples/queens_bv.mlw b/examples/queens_bv.mlw index 9fb8735376e19bd7272d76fdecb32620a1b6c3e0..193100f9b070b1523e7b8b35d9fc75ace3a0c8e5 100644 --- a/examples/queens_bv.mlw +++ b/examples/queens_bv.mlw @@ -128,7 +128,7 @@ module BitsSpec ensures { !min = min_elt a.mdl } ensures { result.mdl = singleton !min } - use bv.BV32 + use bv.BV32 as BV32 val below (n: BV32.t) : t requires { BV32.ule n (32:BV32.t) } ensures { result.mdl = interval 0 (BV32.t'int n) } diff --git a/examples/quicksort.mlw b/examples/quicksort.mlw index 146a5c146dd4421451debdc1e344004b2311e082..53214736062fc230e24e2ef854deb9d1623a6d6b 100644 --- a/examples/quicksort.mlw +++ b/examples/quicksort.mlw @@ -76,7 +76,7 @@ module Shuffle use import array.Array use import array.ArraySwap use import array.ArrayPermut - use random.Random + use import random.Random let shuffle (a: array int) : unit writes { a, Random.s } diff --git a/examples/resizable_array.mlw b/examples/resizable_array.mlw index b7df81a6349a91ce9835ff446e8f42cd792fdaa5..7e16f3c02b39612b3511a7e25d8d805e4cb185c2 100644 --- a/examples/resizable_array.mlw +++ b/examples/resizable_array.mlw @@ -3,7 +3,7 @@ module ResizableArraySpec use import int.Int use import map.Map - use map.Const + use import map.Const type rarray 'a = private { ghost mutable length: int; diff --git a/examples/ring_decision/strassen.mlw b/examples/ring_decision/strassen.mlw index ebe2cd220737a6092c0dba4f39adfd8108f56124..32fa70eb6e282643022fd0840796a427ac3e0d27 100644 --- a/examples/ring_decision/strassen.mlw +++ b/examples/ring_decision/strassen.mlw @@ -105,7 +105,6 @@ end module InfMatrix - use HighOrd type t constant tzero: t diff --git a/examples/skew_heaps.mlw b/examples/skew_heaps.mlw index 426ccb91665aeeb32cd6679f3d8a4b9328af4aa8..617095f818467b5dee123828d11587bafa83e458 100644 --- a/examples/skew_heaps.mlw +++ b/examples/skew_heaps.mlw @@ -10,7 +10,7 @@ module Heap type elt predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . type t @@ -70,7 +70,7 @@ module SkewHeaps type elt val predicate le elt elt - clone relations.TotalPreOrder with + clone import relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . (* [e] is no greater than the root of [t], if any *) diff --git a/examples/sumrange.mlw b/examples/sumrange.mlw index 3cc7b22cece125b4744e6fdc335f83796a9ad499..620081819ee66d11430a5cd60eb4ba968fcced4c 100644 --- a/examples/sumrange.mlw +++ b/examples/sumrange.mlw @@ -25,8 +25,8 @@ with logarithmic time operations. module ArraySum - use export int.Int - use export array.Array + use import int.Int + use import array.Array (** `sum a i j` denotes the sum `\sum_{i <= k < j} a[k]`. It is axiomatizated by the two following axioms expressing @@ -60,6 +60,8 @@ end module Simple + use import int.Int + use import array.Array use import ArraySum use import ref.Ref @@ -85,7 +87,8 @@ end module ExtraLemmas - use array.Array + use import int.Int + use import array.Array use import ArraySum (** summation in adjacent intervals *) @@ -127,9 +130,10 @@ end module CumulativeArray - use array.Array + use import int.Int + use import array.Array use import ArraySum - use ExtraLemmas + use import ExtraLemmas predicate is_cumulative_array_for (c:array int) (a:array int) = c.length = a.length + 1 /\ @@ -195,9 +199,10 @@ end module CumulativeTree - use array.Array + use import int.Int + use import array.Array use import ArraySum - use ExtraLemmas + use import ExtraLemmas use import int.ComputerDivision type indexes = @@ -367,7 +372,7 @@ module CumulativeTree end lemma depth_min : forall t. depth t >= 1 - + use import bv.Pow2int let rec lemma depth_is_log (t:tree) (a :array int) (k:int) @@ -445,5 +450,4 @@ module CumulativeTree query_aux_complexity l a i m c + query_aux_complexity r a m j c end - end diff --git a/examples/tests-provers/bv.why b/examples/tests-provers/bv.why index c4b72b9b4dc81316dbca4b445247c792b771cc5c..07733f6029f54391ed49dad11ee2e6a28a49329a 100644 --- a/examples/tests-provers/bv.why +++ b/examples/tests-provers/bv.why @@ -1,6 +1,6 @@ theory CheckBV64 use import bv.BV64 - use int.Int + use int.Int as Int constant one : t = 1 constant two : t = 2 @@ -143,7 +143,7 @@ end theory CheckBV32 use import bv.BV32 - use int.Int + use int.Int as Int constant one : t = 1 constant two : t = 2 @@ -201,7 +201,7 @@ end theory CheckBV16 use import bv.BV16 - use int.Int + use int.Int as Int constant one : t = 1 constant two : t = 2 @@ -259,7 +259,7 @@ end theory CheckBV8 use import bv.BV8 - use int.Int + use int.Int as Int constant one : t = 1 constant two : t = 2 diff --git a/examples/tests-provers/gappa.why b/examples/tests-provers/gappa.why index c30f0454738399dde8b3b26cc44de8787148e0d4..59b15bebaca0b083cadfadf72f951c903086df37 100644 --- a/examples/tests-provers/gappa.why +++ b/examples/tests-provers/gappa.why @@ -5,7 +5,7 @@ theory TestGappa use import real.Abs use import real.Square use import floating_point.Rounding - use floating_point.Single + use floating_point.Single as Single use import floating_point.Double lemma Round_single_01: diff --git a/examples/tests-provers/ieee_float.mlw b/examples/tests-provers/ieee_float.mlw index 040f7cd8b3b419d5a892c0a55caf72f2153f3728..97234e2453b1a3f5280ace2a2dd234023d224439 100644 --- a/examples/tests-provers/ieee_float.mlw +++ b/examples/tests-provers/ieee_float.mlw @@ -1,7 +1,7 @@ theory A - use ieee_float.Float32 - use ieee_float.Float64 + use ieee_float.Float32 as Float32 + use ieee_float.Float64 as Float64 lemma ebsb32 : Float32.t'eb = 8 /\ Float32.t'sb = 24 lemma ebsb64 : Float64.t'eb = 11 /\ Float64.t'sb = 53 diff --git a/examples/tests/bitvector-test.why b/examples/tests/bitvector-test.why index f9a6537a35f705b0c7fcef7389d1c1f5ce58b9b7..0b74d4331b978e315dd5ab9213f568600a8cdcc5 100644 --- a/examples/tests/bitvector-test.why +++ b/examples/tests/bitvector-test.why @@ -27,15 +27,15 @@ theory NthConvert use import mach.int.Int - use bv.BV8 - use bv.BV64 + use bv.BV8 as BV8 + use bv.BV64 as BV64 use bv.BVConverter_8_64 as BVC lemma bv8_to_bv64_low: forall x i. 0 <= i < 8 -> BV64.nth (BVC.toBig x) i = BV8.nth x i - by forall i. + by forall i. BV64.nth_bv (BVC.toBig x) (BVC.toBig i) = BV8.nth_bv x i - + lemma bv8_to_bv64_high: forall x i. 8 <= i < 64 -> BV64.nth (BVC.toBig x) i = false end diff --git a/examples/topological_sorting.mlw b/examples/topological_sorting.mlw index 49370ef2978ebafa2a0aa2b64c91065cfb1388e3..a0880ca53bd504e5717eec9210a5726ed7d4b884 100644 --- a/examples/topological_sorting.mlw +++ b/examples/topological_sorting.mlw @@ -47,7 +47,7 @@ module Static use import ref.Ref use import Graph - use set.Fset + use set.Fset as Fset clone impset.Impset as S with type elt = vertex clone appset.Appset as SA with type elt = vertex diff --git a/examples/verifythis_2016_matrix_multiplication/matrices.mlw b/examples/verifythis_2016_matrix_multiplication/matrices.mlw index b546181c1b13d135dc4c270a40bab307dbd09886..efe5ec03fdfae50ffedf68296a4a6a33ef463b23 100644 --- a/examples/verifythis_2016_matrix_multiplication/matrices.mlw +++ b/examples/verifythis_2016_matrix_multiplication/matrices.mlw @@ -50,7 +50,6 @@ end theory Matrix use import int.Int - use HighOrd type mat 'a diff --git a/examples/verifythis_2018_array_based_queuing_lock_2.mlw b/examples/verifythis_2018_array_based_queuing_lock_2.mlw index d839da4333f79579cb743c087411d4ad916e8204..a93a2b6ae70f856a0fa7f510f08b4c0117643217 100644 --- a/examples/verifythis_2018_array_based_queuing_lock_2.mlw +++ b/examples/verifythis_2018_array_based_queuing_lock_2.mlw @@ -42,7 +42,6 @@ let fetch_and_add (r:ref tick) predicate lt (tick1 tick2: tick) = tick1.v < tick2.v -use relations.Transitive use import list.List use import list.HdTl use import list.Append @@ -457,4 +456,4 @@ let main () : unit -end \ No newline at end of file +end diff --git a/examples/verifythis_fm2012_LRS.mlw b/examples/verifythis_fm2012_LRS.mlw index 79b7cdcc4bd7ef064423792e9fbf66e4c7dbf4f2..b128aee3f59cf0190ada6f9451c7d42a9bab8305 100644 --- a/examples/verifythis_fm2012_LRS.mlw +++ b/examples/verifythis_fm2012_LRS.mlw @@ -196,7 +196,7 @@ module SuffixSort use import int.Int use import ref.Refint use import array.Array - use LCP + use import LCP (** order by prefix *) predicate lt (a : array int) (x y:int) = @@ -224,14 +224,13 @@ let compare (a:array int) (x y:int) : int if a[x + l] > a[y + l] then 1 else absurd - - use map.MapInjection + use map.MapInjection as Inj (** `range a` is true when for each `i`, `a[i]` is between `0` and `a.length-1` *) - predicate range (a:array int) = MapInjection.range a.elts a.length + predicate range (a:array int) = Inj.range a.elts a.length (** for the `permut` predicate (permutation of elements) *) - use array.ArrayPermut + use import array.ArrayPermut predicate le (a : array int) (x y:int) = x = y \/ lt a x y @@ -244,7 +243,7 @@ let compare (a:array int) (x y:int) : int le a x y /\ le a y z -> le a x z (** spec of sorted in increasing prefix order *) - use map.Map + use map.Map as Map predicate sorted_sub (a:array int) (data:Map.map int int) (l u:int) = forall i1 i2 : int. l <= i1 <= i2 < u -> @@ -257,17 +256,17 @@ let sort (a:array int) (data : array int) requires { data.length = a.length } requires { range data } ensures { sorted a data } - ensures { ArrayPermut.permut_all (old data) data } + ensures { permut_all (old data) data } = for i = 0 to data.length - 1 do - invariant { ArrayPermut.permut_all (old data) data } + invariant { permut_all (old data) data } invariant { sorted_sub a data.elts 0 i } invariant { range data } let j = ref i in while !j > 0 && compare a data[!j-1] data[!j] > 0 do invariant { 0 <= !j <= i } invariant { range data } - invariant { ArrayPermut.permut_all (old data) data } + invariant { permut_all (old data) data } invariant { sorted_sub a data.elts 0 !j } invariant { sorted_sub a data.elts !j (i+1) } invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i -> @@ -278,7 +277,7 @@ let sort (a:array int) (data : array int) let t = data[!j] in data[!j] <- data[b]; data[b] <- t; - assert { ArrayPermut.exchange (data at L) data (!j-1) !j }; + assert { exchange (data at L) data (!j-1) !j }; decr j done; (* needed to prove the invariant `sorted_sub a data.elts 0 i` *) @@ -293,8 +292,8 @@ module SuffixSort_test use import int.Int use import array.Array - use LCP - use SuffixSort + use import LCP + use import SuffixSort exception BenchFailure @@ -327,13 +326,13 @@ module SuffixArray use import int.Int use import array.Array -use LCP -use SuffixSort -use map.Map -use map.MapInjection +use import LCP +use import SuffixSort +use map.Map as Map +use map.MapInjection as Inj predicate permutation (m:Map.map int int) (u : int) = - MapInjection.range m u /\ MapInjection.injective m u + Inj.range m u /\ Inj.injective m u type suffixArray = { values : array int; @@ -349,11 +348,11 @@ let select (s:suffixArray) (i:int) : int ensures { result = s.suffixes[i] } = s.suffixes[i] -use array.ArrayPermut +use import array.ArrayPermut (** needed to establish invariant in function `create` *) lemma permut_permutation : forall a1 a2:array int. - ArrayPermut.permut_all a1 a2 /\ permutation a1.elts a1.length -> + permut_all a1 a2 /\ permutation a1.elts a1.length -> permutation a2.elts a2.length (** constructor of suffixArray structure *) @@ -438,10 +437,10 @@ module LRS use import int.Int use import ref.Ref use import array.Array - use map.MapInjection - use LCP - use SuffixSort - use SuffixArray + use map.MapInjection as Inj + use import LCP + use import SuffixSort + use import SuffixArray (** additional properties relating `le` and `longest_common_prefix` *) diff --git a/examples/verifythis_fm2012_treedel.mlw b/examples/verifythis_fm2012_treedel.mlw index ca346fa3c3e029df5c8e42748982fd4f649b55d6..6dc15d7f65f49dc5b5790f74aa73fa7d38f477bb 100644 --- a/examples/verifythis_fm2012_treedel.mlw +++ b/examples/verifythis_fm2012_treedel.mlw @@ -87,7 +87,7 @@ module Treedel use import bintree.Tree use import bintree.Inorder use import list.List - use list.Mem + use import list.Mem use import list.Append use import list.Distinct diff --git a/src/parser/parser.mly b/src/parser/parser.mly index 5a3a94f4549c1e4de2e7825c59216029a7199cca..9035ebf6adef4db1ba27b950699d743d005bad45 100644 --- a/src/parser/parser.mly +++ b/src/parser/parser.mly @@ -246,14 +246,16 @@ use_clone: { Typing.add_decl (floc $startpos $endpos) (Dclone ($3, $4)) } | USE boption(IMPORT) tqualid option(preceded(AS, uident)) { let loc = floc $startpos $endpos in + let import = $2 || $4 = None in Typing.open_scope loc (use_as $3 $4); Typing.add_decl loc (Duse $3); - Typing.close_scope loc ~import:$2 } + Typing.close_scope loc ~import } | CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst { let loc = floc $startpos $endpos in + let import = $2 || $4 = None in Typing.open_scope loc (use_as $3 $4); Typing.add_decl loc (Dclone ($3, $5)); - Typing.close_scope loc ~import:$2 } + Typing.close_scope loc ~import } clone_subst: | (* epsilon *) { [] } diff --git a/stdlib/array.mlw b/stdlib/array.mlw index f905ab99806449820af5c3a27f3024decc291081..eff74e92a5a211c064b011f893c69b252b74c2d5 100644 --- a/stdlib/array.mlw +++ b/stdlib/array.mlw @@ -130,7 +130,6 @@ module Init use import int.Int use export Array - use HighOrd val init (n: int) (f: int -> 'a) : array 'a requires { [@expl:array creation size] n >= 0 } diff --git a/stdlib/bv.mlw b/stdlib/bv.mlw index a71824f1cc05124991f1cf339286fef368119898..9c145b4a2021b3a89f6f4f35858abb8677a863d5 100644 --- a/stdlib/bv.mlw +++ b/stdlib/bv.mlw @@ -413,7 +413,7 @@ module BV64 constant size : int = 64 constant two_power_size : int = 0x1_0000_0000_0000_0000 - use int.Int (* needed to use range types *) + use int.Int as Int (* needed to use range types *) type t = < range 0 0xFFFF_FFFF_FFFF_FFFF > @@ -434,7 +434,7 @@ module BV32 constant size : int = 32 constant two_power_size : int = 0x1_0000_0000 - use int.Int (* needed to use range types *) + use int.Int as Int (* needed to use range types *) type t = < range 0 0xFFFF_FFFF > @@ -455,7 +455,7 @@ module BV16 constant size : int = 16 constant two_power_size : int = 0x1_0000 - use int.Int (* needed to use range types *) + use int.Int as Int (* needed to use range types *) type t = < range 0 0xFFFF > @@ -476,7 +476,7 @@ module BV8 constant size : int = 8 constant two_power_size : int = 0x1_00 - use int.Int (* needed to use range types *) + use int.Int as Int (* needed to use range types *) type t = < range 0 0xFF > @@ -521,8 +521,8 @@ end (** {2 Converters of common size_bvs} *) module BVConverter_32_64 - use BV32 - use BV64 + use BV32 as BV32 + use BV64 as BV64 predicate in_range (b : BV64.t) = BV64.ule b (0xFFFF_FFFF:BV64.t) @@ -538,8 +538,8 @@ module BVConverter_32_64 end module BVConverter_16_64 - use BV16 - use BV64 + use BV16 as BV16 + use BV64 as BV64 predicate in_range (b : BV64.t) = BV64.ule b (0xFFFF:BV64.t) @@ -554,8 +554,8 @@ module BVConverter_16_64 end module BVConverter_8_64 - use BV8 - use BV64 + use BV8 as BV8 + use BV64 as BV64 predicate in_range (b : BV64.t) = BV64.ule b (0xFF:BV64.t) @@ -570,8 +570,8 @@ module BVConverter_8_64 end module BVConverter_16_32 - use BV16 - use BV32 + use BV16 as BV16 + use BV32 as BV32 predicate in_range (b : BV32.t) = BV32.ule b (0xFFFF:BV32.t) @@ -586,8 +586,8 @@ module BVConverter_16_32 end module BVConverter_8_32 - use BV8 - use BV32 + use BV8 as BV8 + use BV32 as BV32 predicate in_range (b : BV32.t) = BV32.ule b (0xFF:BV32.t) @@ -602,8 +602,8 @@ module BVConverter_8_32 end module BVConverter_8_16 - use BV8 - use BV16 + use BV8 as BV8 + use BV16 as BV16 predicate in_range (b : BV16.t) = BV16.ule b (0xFF:BV16.t) diff --git a/stdlib/floating_point.mlw b/stdlib/floating_point.mlw index cb7c078e85efc6324d75dcc454957ecbae4588cf..b2c508c732015395bd3b4404174b2d13a4fcf8f4 100644 --- a/stdlib/floating_point.mlw +++ b/stdlib/floating_point.mlw @@ -87,7 +87,7 @@ module GenFloat use import real.Real use import real.Abs use import real.FromInt - use int.Int + use int.Int as Int type t diff --git a/stdlib/ieee_float.mlw b/stdlib/ieee_float.mlw index 98880caa44df72a8583eefc8ef9d59642b9970ee..4a1a6726fd24f1641b4c9a6d83e05bcc57a44b95 100644 --- a/stdlib/ieee_float.mlw +++ b/stdlib/ieee_float.mlw @@ -35,9 +35,9 @@ module GenericFloat use import int.Int use import bv.Pow2int - use real.Abs - use real.FromInt - use real.Truncate + use real.Abs as Abs + use real.FromInt as FromInt + use real.Truncate as Truncate use import real.RealInfix use export RoundingMode @@ -495,17 +495,17 @@ module GenericFloat no_overflow m (to_real x *. to_real y +. to_real z) /\ to_real (fma m x y z) = round m (to_real x *. to_real y +. to_real z) - use real.Square + use real.Square as S axiom sqrt_finite: forall m:mode, x:t [sqrt m x]. is_finite x -> to_real x >=. 0. -> is_finite (sqrt m x) /\ - to_real (sqrt m x) = round m (Square.sqrt (to_real x)) + to_real (sqrt m x) = round m (S.sqrt (to_real x)) lemma sqrt_finite_rev: forall m:mode, x:t [sqrt m x]. is_finite (sqrt m x) -> is_finite x /\ to_real x >=. 0. /\ - to_real (sqrt m x) = round m (Square.sqrt (to_real x)) + to_real (sqrt m x) = round m (S.sqrt (to_real x)) predicate same_sign_real (x:t) (r:real) = (is_positive x /\ r >. 0.0) \/ (is_negative x /\ r <. 0.0) @@ -649,7 +649,7 @@ module GenericFloat (* _____________ *) - use real.Truncate + use real.Truncate as Truncate (* This predicate specify if a float is finite and is an integer *) predicate is_int (x:t) @@ -789,10 +789,10 @@ end (** {2 Conversions to/from bitvectors} *) module Float_BV_Converter - use bv.BV8 - use bv.BV16 - use bv.BV32 - use bv.BV64 + use bv.BV8 as BV8 + use bv.BV16 as BV16 + use bv.BV32 as BV32 + use bv.BV64 as BV64 use import RoundingMode (* with unsigned int as bitvector *) @@ -809,7 +809,7 @@ module Float_BV_Converter function to_ubv64 mode t : BV64.t use import real.RealInfix - use real.FromInt + use real.FromInt as FromInt predicate is_finite t predicate le t t @@ -845,7 +845,7 @@ end (** {2 Standard simple precision floats (32 bits)} *) module Float32 - use int.Int + use int.Int as Int use import real.Real type t = < float 8 24 > @@ -881,7 +881,7 @@ end (** {2 Standard double precision floats (64 bits)} *) module Float64 - use int.Int + use int.Int as Int use import real.Real type t = < float 11 53 > @@ -918,8 +918,8 @@ end module FloatConverter - use Float64 - use Float32 + use Float64 as Float64 + use Float32 as Float32 use export RoundingMode diff --git a/stdlib/int.mlw b/stdlib/int.mlw index cd6310827a2ae9d197927cfbdd7dbcf4de8798b3..6dcc06ac41aeb6b3a6bfdbd461e49cbcc1502b93 100644 --- a/stdlib/int.mlw +++ b/stdlib/int.mlw @@ -56,10 +56,7 @@ module MinMax use import Int - clone export relations.MinMax with - type t = int, predicate le = (<=), - goal TotalOrder.Refl, goal TotalOrder.Trans, - goal TotalOrder.Antisymm, goal TotalOrder.Total + clone export relations.MinMax with type t = int, predicate le = (<=), goal . let min (x y : int) : int ensures { result = min x y } diff --git a/stdlib/io.mlw b/stdlib/io.mlw index e920f21d6a6b0617265ace03890349143a308a2e..ffb3bd4be27e6077a9b82e4c6da8b4a55c1895c5 100644 --- a/stdlib/io.mlw +++ b/stdlib/io.mlw @@ -6,7 +6,7 @@ module StdIO (** ghost references to represent the standard output *) use import int.Int use import list.List - use list.Reverse + use import list.Reverse use import ref.Ref type prdata = PrChar char | PrInt int @@ -42,6 +42,6 @@ module StdIO ensures { !cur_pos = 0 } ensures { !current_line = Nil } ensures { !cur_linenum = (old !cur_linenum) + 1 } - ensures { !flushed = Cons (Reverse.reverse (old !current_line)) (old !flushed) } + ensures { !flushed = Cons (reverse (old !current_line)) (old !flushed) } end diff --git a/stdlib/list.mlw b/stdlib/list.mlw index b785d8d6c583c90631236c6c380f30128e1d6057..f72d9bf61a7bf4a0e1d35fe8efff9cca4144d276 100644 --- a/stdlib/list.mlw +++ b/stdlib/list.mlw @@ -338,7 +338,8 @@ module Sorted type t predicate le t t - clone relations.Transitive with type t = t, predicate rel = le, axiom Trans + clone import relations.Transitive with + type t = t, predicate rel = le, axiom Trans inductive sorted (l: list t) = | Sorted_Nil: @@ -384,8 +385,8 @@ module RevSorted use import List - clone Sorted as Incr with type t = t, predicate le = le, goal Transitive.Trans - clone Sorted as Decr with type t = t, predicate le = ge, goal Transitive.Trans + clone Sorted as Incr with type t = t, predicate le = le, goal . + clone Sorted as Decr with type t = t, predicate le = ge, goal . predicate compat (s t: list t) = match s, t with diff --git a/stdlib/mach/int.mlw b/stdlib/mach/int.mlw index 177f98849fe0266d3c681fab844e9b44bacfb675..693ccbff7ff7625990d6e8a5e32e8339316d2f3b 100644 --- a/stdlib/mach/int.mlw +++ b/stdlib/mach/int.mlw @@ -221,7 +221,7 @@ module Int31 lemma to_int_in_bounds, lemma extensionality -(* use bv.BV31 +(* use bv.BV31 as BV31 val to_bv (x: int31) : BV31.t ensures { BV31.to_int result = to_int x } @@ -247,8 +247,9 @@ module Int32 function to_int = int32'int, lemma to_int_in_bounds, lemma extensionality + (* - use bv.BV32 + use bv.BV32 as BV32 val to_bv (x: int32) : BV32.t ensures { BV32.to_int result = to_int x } @@ -261,7 +262,7 @@ module Int32BV use export Int32 - use bv.BV32 + use bv.BV32 as BV32 val to_bv (x: int32) : BV32.t ensures { BV32.to_int result = to_int x } @@ -358,7 +359,7 @@ module UInt32GMP requires { Int32.to_int x >= 0 } ensures { to_int result = Int32.to_int x } -(* use bv.BV32 +(* use bv.BV32 as BV32 val to_bv (x: uint32) : BV32.t ensures { BV32.to_uint result = to_int x } @@ -390,7 +391,7 @@ module Int63 let constant max_int = of_int max_int63 let constant min_int = of_int min_int63 -(* use bv.BV63 +(* use bv.BV63 as BV63 val to_bv (x: int63) : BV63.t ensures { BV63.to_int result = to_int x } @@ -516,7 +517,7 @@ module Int64 lemma to_int_in_bounds, lemma extensionality -(* use bv.BV64 +(* use bv.BV64 as BV64 val to_bv (x: int64) : BV64.t ensures { BV64.to_int result = to_int x } @@ -553,7 +554,7 @@ module UInt64 lemma to_int_in_bounds, lemma extensionality -(* use bv.BV64 +(* use bv.BV64 as BV64 val to_bv (x: uint64) : BV64.t ensures { BV64.to_uint result = to_int x } diff --git a/stdlib/number.mlw b/stdlib/number.mlw index e0e06309c28836e975ef36ccc820b2851b39c09e..fc7a28fd16f64d29b9f227eb276d5d206abd935f 100644 --- a/stdlib/number.mlw +++ b/stdlib/number.mlw @@ -80,19 +80,19 @@ module Divisibility lemma divides_bounds: forall a b: int. divides a b -> b <> 0 -> abs a <= abs b - use int.EuclideanDivision + use int.EuclideanDivision as ED lemma mod_divides_euclidean: - forall a b: int. b <> 0 -> EuclideanDivision.mod a b = 0 -> divides b a + forall a b: int. b <> 0 -> ED.mod a b = 0 -> divides b a lemma divides_mod_euclidean: - forall a b: int. b <> 0 -> divides b a -> EuclideanDivision.mod a b = 0 + forall a b: int. b <> 0 -> divides b a -> ED.mod a b = 0 - use int.ComputerDivision + use int.ComputerDivision as CD lemma mod_divides_computer: - forall a b: int. b <> 0 -> ComputerDivision.mod a b = 0 -> divides b a + forall a b: int. b <> 0 -> CD.mod a b = 0 -> divides b a lemma divides_mod_computer: - forall a b: int. b <> 0 -> divides b a -> ComputerDivision.mod a b = 0 + forall a b: int. b <> 0 -> divides b a -> CD.mod a b = 0 use import Parity @@ -123,7 +123,7 @@ module Gcd (* gcd is associative commutative *) - clone algebra.AC with type t = int, function op = gcd + clone import algebra.AC with type t = int, function op = gcd lemma gcd_0_pos: forall a: int. 0 <= a -> gcd a 0 = a lemma gcd_0_neg: forall a: int. a < 0 -> gcd a 0 = -a @@ -132,17 +132,17 @@ module Gcd lemma gcd_euclid: forall a b q: int. gcd a b = gcd a (b - q * a) - use int.ComputerDivision + use int.ComputerDivision as CD lemma Gcd_computer_mod: - forall a b: int [gcd b (ComputerDivision.mod a b)]. - b <> 0 -> gcd b (ComputerDivision.mod a b) = gcd a b + forall a b: int [gcd b (CD.mod a b)]. + b <> 0 -> gcd b (CD.mod a b) = gcd a b - use int.EuclideanDivision + use int.EuclideanDivision as ED lemma Gcd_euclidean_mod: - forall a b: int [gcd b (EuclideanDivision.mod a b)]. - b <> 0 -> gcd b (EuclideanDivision.mod a b) = gcd a b + forall a b: int [gcd b (ED.mod a b)]. + b <> 0 -> gcd b (ED.mod a b) = gcd a b lemma gcd_mult: forall a b c: int. 0 <= c -> gcd (c * a) (c * b) = c * gcd a b diff --git a/stdlib/ocaml.mlw b/stdlib/ocaml.mlw index d61cd6606b9448409eae3b20e7d95aa3d883313e..a937f8cf6c4641dc212378098047679a4bd54dd7 100644 --- a/stdlib/ocaml.mlw +++ b/stdlib/ocaml.mlw @@ -38,12 +38,11 @@ end module OCaml use export int.Int - use mach.int.Int63 + use mach.int.Int63 as Int63 use export int.MinMax use export option.Option use export Pervasives - - use Sys + use import Sys use mach.array.Array63 as Array type array 'a = Array.array 'a diff --git a/stdlib/pigeon.mlw b/stdlib/pigeon.mlw index 4202ad631cc2b90abf9d88150117a1a885ce67fb..b4af112fcad0d78109110fe50afcb6dece65d138 100644 --- a/stdlib/pigeon.mlw +++ b/stdlib/pigeon.mlw @@ -36,7 +36,7 @@ module ListAndSet use import list.List use import list.Length use import list.Append - use list.Mem + use list.Mem as Mem use import set.Fset type t @@ -48,7 +48,8 @@ module ListAndSet exists e: t, l1 l2 l3: list t. l = l1 ++ (Cons e (l2 ++ (Cons e l3))) - clone set.FsetInduction with type t = t, predicate p = pigeon_set + clone set.FsetInduction as FSI with + type t = t, predicate p = pigeon_set lemma corner: forall s: set t, l: list t. diff --git a/stdlib/python.mlw b/stdlib/python.mlw index 491d1dcd437c557be706ffa15541ad2a7134c667..6c5a5037de19a01d42def1ef5e71d99f20bb618c 100644 --- a/stdlib/python.mlw +++ b/stdlib/python.mlw @@ -2,34 +2,34 @@ module Python use import int.Int use import ref.Ref - use array.Array + use array.Array as A (* Python's lists are actually resizable arrays, but we simplify here *) - type list 'a = Array.array 'a + type list 'a = A.array 'a function ([]) (l: list 'a) (i: int) : 'a = - Array.([]) l i + A.([]) l i function ([<-]) (l: list 'a) (i: int) (v: 'a) : list 'a = - Array.([<-]) l i v + A.([<-]) l i v let function len (l: list 'a) : int - = Array.length l + = A.length l let ([]) (l: list 'a) (i: int) : 'a - requires { 0 <= i < Array.length l } + requires { 0 <= i < A.length l } ensures { result = l[i] } - = Array.([]) l i + = A.([]) l i let ([]<-) (l: list 'a) (i: int) (v: 'a) : unit - requires { 0 <= i < Array.length l } + requires { 0 <= i < A.length l } writes { l } - ensures { l = Array.([<-]) (old l) i v } - = Array.([]<-) l i v + ensures { l = A.([<-]) (old l) i v } + = A.([]<-) l i v val range (l u: int) : list int requires { l <= u } - ensures { Array.length result = u - l } + ensures { A.length result = u - l } ensures { forall i. l <= i < u -> result[i] = i } (* ad-hoc facts about exchange *) @@ -37,7 +37,7 @@ module Python use import map.Occ function occurrence (v: 'a) (l: list 'a) : int = - Occ.occ v l.Array.elts 0 l.Array.length + Occ.occ v l.A.elts 0 l.A.length (* Python's division and modulus according are neither Euclidean division, nor computer division, but something else defined in diff --git a/stdlib/real.mlw b/stdlib/real.mlw index f43ee28b263694fbce1175218d4f52df9e9fe881..8d186264a045e472c8b356c909a58faf5ed0f4fb 100644 --- a/stdlib/real.mlw +++ b/stdlib/real.mlw @@ -99,8 +99,7 @@ end module MinMax use import Real - clone export relations.MinMax with - type t = real, predicate le = (<=), goal . + clone export relations.MinMax with type t = real, predicate le = (<=), goal . end @@ -108,7 +107,7 @@ end module FromInt - use int.Int + use int.Int as Int use import Real function from_int int : real diff --git a/stdlib/relations.mlw b/stdlib/relations.mlw index ca86e86111583b77b6ce536793d8e5de98f67065..43dde685b20234477a940c2df270cd21a1b0bf44 100644 --- a/stdlib/relations.mlw +++ b/stdlib/relations.mlw @@ -142,7 +142,7 @@ module MinMax type t predicate le t t - clone TotalOrder with type t = t, predicate rel = le, axiom . + clone TotalOrder as TO with type t = t, predicate rel = le, axiom . function min (x y : t) : t = if le x y then x else y function max (x y : t) : t = if le x y then y else x diff --git a/stdlib/seq.mlw b/stdlib/seq.mlw index 43f328fd35a6a8b293e5818114dd20c517724cc6..433b8d9feb1bfa7d009cfd1132e22ac527dbd3ad 100644 --- a/stdlib/seq.mlw +++ b/stdlib/seq.mlw @@ -369,7 +369,8 @@ module Sorted type t predicate le t t - clone relations.TotalOrder with type t = t, predicate rel = le, axiom . + clone relations.TotalOrder as TO with + type t = t, predicate rel = le, axiom . predicate sorted_sub (s: seq t) (l u: int) = forall i1 i2. l <= i1 <= i2 < u -> le s[i1] s[i2] @@ -401,9 +402,7 @@ end module SortedInt (** sorted sequences of integers *) use import int.Int - clone export Sorted with type t = int, predicate le = (<=), - goal TotalOrder.Refl, goal TotalOrder.Trans, - goal TotalOrder.Antisymm, goal TotalOrder.Total + clone export Sorted with type t = int, predicate le = (<=), goal . end diff --git a/stdlib/tptp.mlw b/stdlib/tptp.mlw index 2654b1afb04a0e447dc11d2c0422b0551b1aab4f..5de85e21c31615d71573c7e260cb84234cee6bb5 100644 --- a/stdlib/tptp.mlw +++ b/stdlib/tptp.mlw @@ -41,7 +41,7 @@ module IntDivF end module Rat - use int.Int + use int.Int as Int type rat @@ -122,8 +122,8 @@ end module RealTrunc use import Real - use real.FromInt - use real.Truncate + use real.FromInt as FromInt + use real.Truncate as Truncate function floor (x : real) : real = FromInt.from_int (Truncate.floor x) function ceiling (x : real) : real = FromInt.from_int (Truncate.ceil x) @@ -164,7 +164,7 @@ module IntToRat end module IntToReal - use real.FromInt + use real.FromInt as FromInt function to_real (x : int) : real = FromInt.from_int x end @@ -179,7 +179,7 @@ end module RatToReal use import Rat use import real.Real - use real.FromInt + use real.FromInt as FromInt function to_real (x : rat) : real = FromInt.from_int (numerator x) / FromInt.from_int (denominator x)