diff --git a/examples/dijkstra.mlw b/examples/dijkstra.mlw index a8fe7ee2c9fe7dcaf0f71c7a2f7694a2878e481f..71595c702daf12d844f12effcd5740cb8ecf2b9a 100644 --- a/examples/dijkstra.mlw +++ b/examples/dijkstra.mlw @@ -26,9 +26,8 @@ module DijkstraShortestPath axiom G_succ_sound : forall x: vertex. S.subset (g_succ x) v - function weight vertex vertex : int (* edge weight, if there is an edge *) - - axiom Weight_nonneg: forall x y: vertex. weight x y >= 0 + val function weight vertex vertex : int (* edge weight, if there is an edge *) + ensures { result >= 0 } (** Data structures for the algorithm. *) diff --git a/examples/fibonacci.mlw b/examples/fibonacci.mlw index 33204f947793f4539b2c835fa7a79cdb6ffef715..fe81b995a2a2a8cc2021402dbc90211cc0bd1c01 100644 --- a/examples/fibonacci.mlw +++ b/examples/fibonacci.mlw @@ -275,7 +275,9 @@ theory Mat22 "2x2 integer matrices" (* clone algebra.Assoc with type t = t, function op = mult, lemma Assoc *) clone export - int.Exponentiation with type t = t, function one = id, function (*) = mult + int.Exponentiation with + type t = t, function one = id, function (*) = mult, + goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r end diff --git a/examples/in_progress/cek.mlw b/examples/in_progress/cek.mlw index 0e2d6318c691be78ac991b9b1167f09c3e171549..312c30c60c5aa0fd82547eb42fbb49f7df218e1a 100644 --- a/examples/in_progress/cek.mlw +++ b/examples/in_progress/cek.mlw @@ -187,8 +187,8 @@ type context = let rec function recompose (c:context) (t:term) (e:environment) : term = match c with | Empty -> t - | Left c t1 e1 -> App (recompose c t e) t1 - | Right (Closure x t1 e1) c -> App (Lambda x t1) (recompose c t e) + | Left c t1 _e1 -> App (recompose c t e) t1 + | Right (Closure x t1 _e1) c -> App (Lambda x t1) (recompose c t e) end (* @@ -218,7 +218,7 @@ let rec lemma recompose_values (c:context) (t1 t2:expr) (e:environment) : unit let rec eval (t:term) (e:environment) (c:context) : value diverges - returns { Closure x t1 e1 -> + returns { Closure x t1 _e1 -> weak_normalize (recompose c t e) (Lambda x t1) } = match t with | Var x -> cont c (lookup x e) diff --git a/examples/in_progress/gmp_square_root.mlw b/examples/in_progress/gmp_square_root.mlw index 4d5ff506d7bb59774cdb7baba0e304581c50dbcd..6dae1283e9bbdbaad5efd7c113d002c4ce834d32 100644 --- a/examples/in_progress/gmp_square_root.mlw +++ b/examples/in_progress/gmp_square_root.mlw @@ -16,9 +16,8 @@ module GmpModel - use export int.Int - use export int.ComputerDivision - use export array.Array + use import int.Int + use import array.Array constant beta' : int axiom beta'_gt_1: 1 < beta' @@ -75,8 +74,11 @@ end module GmpAuxiliaryfunctions use export GmpModel - use export ref.Ref - use export int.Power + use import int.Int + use import int.ComputerDivision + use import int.Power + use import ref.Ref + use import array.Array val rb: ref bool diff --git a/examples/in_progress/immutable_string.mlw b/examples/in_progress/immutable_string.mlw index 85bf07b5280af022c2e288513a104ce18e47335c..6ad398ba4f5f8bb2b970d2991bb3c55930088837 100644 --- a/examples/in_progress/immutable_string.mlw +++ b/examples/in_progress/immutable_string.mlw @@ -10,7 +10,7 @@ module String function ([]) (s: string) (i: int) : char = s.chars i - constant empty : string = { length = 0; chars = fun (i: int) -> dummy_char } + constant empty : string = { length = 0; chars = fun (_: int) -> dummy_char } val get (s: string) (i:int) : char requires { 0 <= i < s.length } diff --git a/examples/random_access_list.mlw b/examples/random_access_list.mlw index 8c4c72d01eaa7d0d3af96c2383df4dad3b48cfd6..84538144293f735d7e8bc789d7099c6496692e09 100644 --- a/examples/random_access_list.mlw +++ b/examples/random_access_list.mlw @@ -250,7 +250,7 @@ module RandomAccessListWithSeq function setf (s: seq 'a) (i: int) (f: 'a -> 'a) : seq 'a = set s i (f s[i]) - function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) = + let function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) = fun z -> let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y) let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a diff --git a/examples/vstte12_ring_buffer.mlw b/examples/vstte12_ring_buffer.mlw index b1a4f9d498b2fac2f3d6f105fc00d95a081c91f9..9a052deb4e688ac777f448417955a02b3b7dd77a 100644 --- a/examples/vstte12_ring_buffer.mlw +++ b/examples/vstte12_ring_buffer.mlw @@ -152,7 +152,7 @@ module RingBufferSeq mutable first: int; mutable len : int; data : array 'a; - ghost mutable sequence: S.seq 'a; + ghost mutable sequence: S.seq {'a}; } invariant { let size = Array.length data in