diff --git a/ROADMAP b/ROADMAP index 43bc9999e9f47cbaac708d79ee9007daca04ecbe..ea9abe69c642f6005347a7388f375136b33f561a 100644 --- a/ROADMAP +++ b/ROADMAP @@ -50,7 +50,9 @@ * choisir un logo -=== Roadmap for third release ========================================== +=== Roadmap for third release 0.70 ======================================= + +* increment the magic number in config (A) * enlever les caracteres de tab des sources et les caracteres latin1 (A) diff --git a/bench/programs/bad-typing/alias1.mlw b/bench/programs/bad-typing/alias1.mlw index 64773150be040e70318c0f4bbdb1b34f7721a227..29c23b774aa51d37f0ce73a0e25510cba6ffc2e2 100644 --- a/bench/programs/bad-typing/alias1.mlw +++ b/bench/programs/bad-typing/alias1.mlw @@ -2,7 +2,7 @@ module M use import module ref.Ref - let foo (x : ref int) (y : ref int) = + let foo (x : ref int) (y : ref int) = x := 1; y := 2 diff --git a/bench/programs/bad-typing/alias2.mlw b/bench/programs/bad-typing/alias2.mlw index da5880a3fd84a0f35575cb71d76aedb4bf9eba64..1ceed3ae8ec9b6f82fdfb8f3cf5ff6e9a315c41d 100644 --- a/bench/programs/bad-typing/alias2.mlw +++ b/bench/programs/bad-typing/alias2.mlw @@ -2,7 +2,7 @@ module M use import module ref.Ref - let foo (x : ref int) (y : ref int) = + let foo (x : ref int) (y : ref int) = x := 1; y := 2 diff --git a/bench/programs/bad-typing/alias3.mlw b/bench/programs/bad-typing/alias3.mlw index 767998ac5cfb43ce4095153c070b63ae60b40d91..d20ebeed904d533c0c5c612e01806a074315951b 100644 --- a/bench/programs/bad-typing/alias3.mlw +++ b/bench/programs/bad-typing/alias3.mlw @@ -2,7 +2,7 @@ module M use import module ref.Ref - let foo (x : ref int) (y : ref int) = + let foo (x : ref int) (y : ref int) = x := 1; y := 2 diff --git a/bench/programs/bad-typing/polyref3.mlw b/bench/programs/bad-typing/polyref3.mlw index eaf576c33cfd0e73d814f5355d3de8bed9ec0abc..c586c25652d1598d5f8bd026f6f1adb31bb3564f 100644 --- a/bench/programs/bad-typing/polyref3.mlw +++ b/bench/programs/bad-typing/polyref3.mlw @@ -1,8 +1,8 @@ module M - + use import module stdlib.Ref use import list.List - + val r : ref (list 'a) end diff --git a/bench/programs/bad-typing/variant1.mlw b/bench/programs/bad-typing/variant1.mlw index a5f00d3efb4229bcee60b47929463b7fc86254b8..72a3bc0636a76ee0094d479a08a2babe38a88062 100644 --- a/bench/programs/bad-typing/variant1.mlw +++ b/bench/programs/bad-typing/variant1.mlw @@ -6,7 +6,7 @@ module M (* missing variant *) let rec even (x:int) : int variant {x} = - odd (x-1) + odd (x-1) with odd (x:int) : int = even (x-1) diff --git a/bench/programs/bad-typing/variant2.mlw b/bench/programs/bad-typing/variant2.mlw index 8201818f35d3f912f2a37faef58b6e0f5ad50ab8..40b6b081e3599c3742e8f1ce130c73f43cddd070 100644 --- a/bench/programs/bad-typing/variant2.mlw +++ b/bench/programs/bad-typing/variant2.mlw @@ -2,13 +2,13 @@ (* different relations *) module M - + use import int.Int predicate rel int int let rec even (x:int) : int variant {x} with rel = - odd (x-1) + odd (x-1) with odd (x:int) : int variant {x} = even (x-1) diff --git a/bench/programs/good/complex_arg_1.mlw b/bench/programs/good/complex_arg_1.mlw index 0fa244ff4dc7322b131a3156411d1a9a8d609947..745fe30cdb30f67e7c49fba2f504fa47e09f4136 100644 --- a/bench/programs/good/complex_arg_1.mlw +++ b/bench/programs/good/complex_arg_1.mlw @@ -21,7 +21,7 @@ let f () = end (* -Local Variables: +Local Variables: compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_1" -End: +End: *) diff --git a/bench/programs/good/complex_arg_2.mlw b/bench/programs/good/complex_arg_2.mlw index 902c443f9165ca3f3042c1460650a3606eca8389..22695a8a3b9558ed973907350b6242bbf0046faa 100644 --- a/bench/programs/good/complex_arg_2.mlw +++ b/bench/programs/good/complex_arg_2.mlw @@ -19,7 +19,7 @@ let test () = end (* -Local Variables: +Local Variables: compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_2" -End: +End: *) diff --git a/bench/programs/good/for.mlw b/bench/programs/good/for.mlw index 40ebf1ea15f7a1c67c66e8848956acd558c3f434..dc6dfaaecf84cd3dc4a34e406ef8fbe9640349d6 100644 --- a/bench/programs/good/for.mlw +++ b/bench/programs/good/for.mlw @@ -85,7 +85,7 @@ let test4d x = end (* -Local Variables: +Local Variables: compile-command: "unset LANG; make -C ../../.. bench/programs/good/for" -End: +End: *) diff --git a/examples/programs/arm.mlw b/examples/programs/arm.mlw index 13a5c94ad28b5440c3a27aaa8f337dad7986d5d7..1bcff010da3279e8fdab4956d195a73145db23ff 100644 --- a/examples/programs/arm.mlw +++ b/examples/programs/arm.mlw @@ -20,14 +20,14 @@ module M let i = ref 2 in while !i <= 10 do invariant { 2 <= !i <= 11 /\ inv a /\ - (* ghost *) !loop1 = !i - 2 /\ 2 * !loop2 <= (!i-2) * (!i-1) } + (* ghost *) !loop1 = !i - 2 /\ 2 * !loop2 <= (!i-2) * (!i-1) } variant { 10 - !i } (* ghost *) incr loop1; let j = ref !i in while a[!j] < a[!j - 1] do invariant { 1 <= !j <= !i /\ inv a /\ - (* ghost *) 2 * !loop2 <= (!i-2) * (!i-1) + 2*(!i - !j) } - variant { !j } + (* ghost *) 2 * !loop2 <= (!i-2) * (!i-1) + 2*(!i - !j) } + variant { !j } (* ghost *) incr loop2; let temp = a[!j] in a[!j] <- a[!j - 1]; diff --git a/examples/programs/binary_search.mlw b/examples/programs/binary_search.mlw index 35e3eb8e6055b02c3c6892d05bed5d79ac8b51a9..f2493c198f471549b38b1df6a638ade83a621500 100644 --- a/examples/programs/binary_search.mlw +++ b/examples/programs/binary_search.mlw @@ -21,7 +21,7 @@ module M let u = ref (length a - 1) in while !l <= !u do invariant { - 0 <= !l /\ !u < length a /\ + 0 <= !l /\ !u < length a /\ forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } variant { !u - !l } let m = !l + div (!u - !l) 2 in diff --git a/examples/programs/binary_search_c.mlw b/examples/programs/binary_search_c.mlw index f6e6403771672da90f734fe0d367e6e02d23ab10..dfa405236c3a0773df9de6131a78e836472eaf09 100644 --- a/examples/programs/binary_search_c.mlw +++ b/examples/programs/binary_search_c.mlw @@ -40,7 +40,7 @@ module M1 while !l <= !u do invariant { 0 <= !l /\ !u <= n-1 /\ forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u } - variant { !u - !l } + variant { !u - !l } let m = div (!l + !u) 2 in if get !mem t m < v then l := m + 1 else if get !mem t m > v then u := m - 1 @@ -94,7 +94,7 @@ module M2 while !l <= !u do invariant { 0 <= !l /\ !u <= n-1 /\ forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u } - variant { !u - !l } + variant { !u - !l } let m = div (!l + !u) 2 in if get_ t m < v then l := m + 1 else if get_ t m > v then u := m - 1 @@ -152,7 +152,7 @@ module M3 invariant { 0 <= to_int !l /\ to_int !u <= to_int n - 1 /\ forall k:int. 0 <= k < to_int n -> to_int (get !mem t k) = to_int v -> to_int !l <= k <= to_int !u } - variant { to_int !u - to_int !l } + variant { to_int !u - to_int !l } let m = of_int (to_int !l + to_int diff --git a/examples/programs/course.mlw b/examples/programs/course.mlw index f7dff09e395635e8f818cff8a16bcf457d267708..582f5f3fd122fe2f0a752a8b61c4ef6e9b22261a 100644 --- a/examples/programs/course.mlw +++ b/examples/programs/course.mlw @@ -106,7 +106,7 @@ end predicate invCourse (alloc:first_free_addr) (this:course) = let (rStud,students,count,sum) = this in count >= 0 - /\ + /\ valid_array alloc 0 (count - 1) students /\ injective 0 (count - 1) students @@ -182,7 +182,7 @@ fun SetMark(R:Course, c:[R], s: [c.Rstud], mark: int) : unit end (* -Local Variables: +Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/course" -End: +End: *) diff --git a/examples/programs/dijkstra.mlw b/examples/programs/dijkstra.mlw index f956cbfeff1b61f1b5443d14671c53d3c20489c1..2e6467f34dd82ed6e2d3f7690ded0c87db5ff472 100644 --- a/examples/programs/dijkstra.mlw +++ b/examples/programs/dijkstra.mlw @@ -101,9 +101,9 @@ module M (* paths and shortest paths path x y d = - there is a path from x to y of length d + there is a path from x to y of length d shortest_path x y d = - there is a path from x to y of length d, and no shorter path *) + there is a path from x to y of length d, and no shorter path *) inductive path vertex vertex int = | Path_nil : @@ -195,8 +195,8 @@ module M let su = ref (g_succ u) in while not (set_has_next su) do invariant - { S.subset !su (g_succ u) /\ - inv src !visited !q !d /\ inv_succ2 src !visited !q u !su } + { S.subset !su (g_succ u) /\ + inv src !visited !q !d /\ inv_succ2 src !visited !q u !su } variant { S.cardinal !su } let v = set_next su in relax u v diff --git a/examples/programs/distance.mlw b/examples/programs/distance.mlw index 34049ea053a868068e024513a98aba7e38ab13eb..f2d97be2aecbd5aff122e1099fb6315c0762560d 100644 --- a/examples/programs/distance.mlw +++ b/examples/programs/distance.mlw @@ -1,6 +1,6 @@ (* Correctness of a program computing the minimal distance between - two words (code by Claude Marché). + two words (code by Claude Marché). This program computes a variant of the Levenshtein distance. Given two strings [w1] and [w2] of respective lengths [n1] and [n2], it @@ -98,12 +98,12 @@ module Distance /\ (forall k:int. 0 <= k <= j -> min_suffix w1 w2 (i+1) k t[k]) /\ min_suffix w1 w2 (i+1) (j+1) !o } begin - let temp = !o in + let temp = !o in o := t[j]; - if w1[i] = w2[j] then - t[j] <- temp - else - t[j] <- (min t[j] t[j+1]) + 1 + if w1[i] = w2[j] then + t[j] <- temp + else + t[j] <- (min t[j] t[j+1]) + 1 end done done; diff --git a/examples/programs/euler001/euler001.mlw_SumMultiple_Closed_formula_1.v b/examples/programs/euler001/euler001.mlw_SumMultiple_Closed_formula_1.v index 5ff366c465b2eb2974b76ec58715d541e57eb460..d09ea5002bfc0435d5ceeeec1ac1db59d517d7a1 100644 --- a/examples/programs/euler001/euler001.mlw_SumMultiple_Closed_formula_1.v +++ b/examples/programs/euler001/euler001.mlw_SumMultiple_Closed_formula_1.v @@ -80,7 +80,7 @@ rewrite <- (Z_div_exact_full_2 n 3). assert (h: (n mod 5 = 0 \/ n mod 5 <> 0)%Z) by omega. destruct h. - + rewrite Zdiv0. Qed. (* DO NOT EDIT BELOW *) diff --git a/examples/programs/euler002.mlw b/examples/programs/euler002.mlw index 05d734eeec022bc55f2fcca031fd0f5466876d24..d911404c2a93e2691af7ed51ce510ab0ed4bbaec 100644 --- a/examples/programs/euler002.mlw +++ b/examples/programs/euler002.mlw @@ -43,7 +43,7 @@ theory FibSumEven "sum of even-valued Fibonacci numbers" axiom SumTooLarge: forall m n:int. n >= 0 -> (fib n) >= m -> fib_sum_even_lt_from m n = 0 (* Note: we take for granted that [fib] is an - increasing sequence *) + increasing sequence *) axiom SumYes: forall n m s:int. n >= 0 -> (fib n) < m -> mod (fib n) 2 = 0 -> diff --git a/examples/programs/euler002/euler002.mlw_FibOnlyEven_fib_even_1.v b/examples/programs/euler002/euler002.mlw_FibOnlyEven_fib_even_1.v index 324faad19c109f9f396803c22e3affd8e6e807b8..34b1a8e4c09a0c3c0f8fc453862d715bcb12b483 100644 --- a/examples/programs/euler002/euler002.mlw_FibOnlyEven_fib_even_1.v +++ b/examples/programs/euler002/euler002.mlw_FibOnlyEven_fib_even_1.v @@ -59,14 +59,14 @@ rewrite fibn; auto with zarith. rewrite Zplus_mod. assert (h: (0 <= (n mod 3) < 3)%Z). apply Z_mod_lt; auto with zarith. -assert (h':( n mod 3 = 0 \/ n mod 3 = 1 \/ n mod 3 = 2)%Z) +assert (h':( n mod 3 = 0 \/ n mod 3 = 1 \/ n mod 3 = 2)%Z) by omega. -clear h. +clear h. destruct h' as [h0|[h1|h2]]. split; auto with zarith. - + SearchAbout Zmod. -assert +assert Qed. (* DO NOT EDIT BELOW *) diff --git a/examples/programs/flag.mlw b/examples/programs/flag.mlw index c31a826ccecd5ff93225e72b2f64bd3c1e001c4a..f1ece8ec7440b2618142c72d3ca3c114a24eded3 100644 --- a/examples/programs/flag.mlw +++ b/examples/programs/flag.mlw @@ -29,11 +29,11 @@ module Flag label Init: while !i < !r do invariant { 0 <= !b <= !i <= !r <= n /\ - monochrome a 0 !b Blue /\ - monochrome a !b !i White /\ - monochrome a !r n Red /\ - length a = n /\ - permut_sub a (at a Init) 0 n } + monochrome a 0 !b Blue /\ + monochrome a !b !i White /\ + monochrome a !r n Red /\ + length a = n /\ + permut_sub a (at a Init) 0 n } variant { !r - !i } match a[!i] with | Blue -> diff --git a/examples/programs/my_cosine/my_cosine.mlw_M_WP_parameter my_cosine_1.v b/examples/programs/my_cosine/my_cosine.mlw_M_WP_parameter my_cosine_1.v index 29285682af2faec52928c53821441587a18f33b0..69089e2f5a8958168b6e8713b2e210d044649064 100644 --- a/examples/programs/my_cosine/my_cosine.mlw_M_WP_parameter my_cosine_1.v +++ b/examples/programs/my_cosine/my_cosine.mlw_M_WP_parameter my_cosine_1.v @@ -82,10 +82,10 @@ Parameter atan: R -> R. Axiom Tan_atan : forall (x:R), ((Rtrigo.tan (atan x)) = x). Inductive mode := - | NearestTiesToEven : mode - | ToZero : mode - | Up : mode - | Down : mode + | NearestTiesToEven : mode + | ToZero : mode + | Up : mode + | Down : mode | NearTiesToAway : mode . Parameter single : Type. diff --git a/examples/programs/next_digit_sum.mlw b/examples/programs/next_digit_sum.mlw index 65d4cab7d81cb115fa375ace457347e4b6ee4566..86ec6535c4fa5cf9b371776b5510b5ed0a18e46a 100644 --- a/examples/programs/next_digit_sum.mlw +++ b/examples/programs/next_digit_sum.mlw @@ -37,7 +37,7 @@ module M interpretation on the left (or on the right); requires induction *) lemma Interp_eq: forall x1 x2 : M.map int int, i j : int. - (forall k : int. i <= k < j -> M.get x1 k = M.get x2 k) -> + (forall k : int. i <= k < j -> M.get x1 k = M.get x2 k) -> interp x1 i j = interp x2 i j (* the sum of the elements of x[i..j[ *) @@ -93,11 +93,11 @@ let search_safety () = let delta = y - !s - c + x[d] in if 0 <= delta && delta <= 9 * d then begin x[d] <- c; - let k = div delta 9 in + let k = div delta 9 in for i = 0 to d - 1 do invariant { length x = m } if i < k then x[i] <- 9 - else if i = k then x[i] <- mod delta 9 + else if i = k then x[i] <- mod delta 9 else x[i] <- 0 done; raise Success @@ -134,14 +134,14 @@ let search () = if 0 <= delta && delta <= 9 * d then begin x[d] <- c; assert { sum x.elts d m = y - delta }; - let k = div delta 9 in + let k = div delta 9 in assert { k <= d }; for i = 0 to d - 1 do invariant { length x = m /\ is_integer x.elts /\ sum x.elts d m = y - delta /\ sum x.elts 0 i = if i <= k then 9*i else delta } if i < k then x[i] <- 9 - else if i = k then x[i] <- (mod delta 9) + else if i = k then x[i] <- (mod delta 9) else x[i] <- 0 done; (* assume { sum !x 0 d = delta }; *) @@ -257,21 +257,21 @@ let search_smallest () = for c = x[d] + 1 to 9 do invariant { x = at x Init /\ - forall c' : int. x[d] < c' < c -> + forall c' : int. x[d] < c' < c -> forall u : int. interp (at x.elts Init) 0 m < u <= interp9 (M.set x.elts d c') d m -> - sum_digits u <> y } + sum_digits u <> y } let delta = y - !s - c + x[d] in if 0 <= delta && delta <= 9 * d then begin assert { smallest_size delta <= d }; x[d] <- c; assert { sum x.elts d m = y - delta }; assert { gt_digit x.elts (at x.elts Init) d }; - let k = div delta 9 in + let k = div delta 9 in assert { k <= d }; for i = 0 to d - 1 do invariant { - length x = m /\ is_integer x.elts /\ + length x = m /\ is_integer x.elts /\ sum x.elts d m = y - delta /\ sum x.elts 0 i = (if i <= k then 9*i else delta) /\ (forall j : int. 0 <= j < i -> @@ -279,7 +279,7 @@ let search_smallest () = (j >= smallest_size delta -> x[j] = 0)) /\ gt_digit x.elts (at x.elts Init) d } if i < k then x[i] <- 9 - else if i = k then x[i] <- mod delta 9 + else if i = k then x[i] <- mod delta 9 else x[i] <- 0; assert { is_integer x.elts } done; @@ -327,14 +327,14 @@ let () = for c = x.(d) + 1 to 9 do let delta = y - !s - c + x.(d) in if 0 <= delta && delta <= 9 * d then begin - x.(d) <- c; - let k = delta / 9 in - for i = 0 to d-1 do - x.(i) <- if i < k then 9 else if i = k then delta mod 9 else 0 - done; - for i = max d (n-1) downto 0 do Format.printf "%d" x.(i) done; - Format.printf "@."; - exit 0 + x.(d) <- c; + let k = delta / 9 in + for i = 0 to d-1 do + x.(i) <- if i < k then 9 else if i = k then delta mod 9 else 0 + done; + for i = max d (n-1) downto 0 do Format.printf "%d" x.(i) done; + Format.printf "@."; + exit 0 end done; s := !s - x.(d) diff --git a/examples/programs/quicksort.mlw b/examples/programs/quicksort.mlw index 042d65a6432b7c5fedf0573209d2da825d7c240c..a4032a5689c70fb605f5303b29e8153aac67194f 100644 --- a/examples/programs/quicksort.mlw +++ b/examples/programs/quicksort.mlw @@ -28,7 +28,7 @@ module Quicksort let m = ref l in label L: begin for i = l + 1 to r do - invariant { (forall j:int. l < j <= !m -> t[j] < v) /\ + invariant { (forall j:int. l < j <= !m -> t[j] < v) /\ (forall j:int. !m < j < i -> t[j] >= v) /\ permut_sub t (at t L) l (r+1) /\ t[l] = v /\ l <= !m < i } diff --git a/examples/programs/ropes.mlw b/examples/programs/ropes.mlw index cbf0aa8418a2ed1d8074873ce032631b3e04dd52..b0c2c87c0a2c9d780ce9424818e8ddc1e52e6914 100644 --- a/examples/programs/ropes.mlw +++ b/examples/programs/ropes.mlw @@ -18,7 +18,7 @@ module M | App rope rope (len: int) predicate inv (r: rope) = match r with - | Str s ofs len -> + | Str s ofs len -> len = 0 \/ 0 <= ofs < S.length s /\ ofs + len <= S.length s | App l r _ -> 0 < len l /\ inv l /\ 0 < len r /\ inv r @@ -33,33 +33,33 @@ module M S.length s1 = S.length s2 /\ forall i:int. 0 <= i < S.length s1 -> S.get s1 i = S.get s2 i - let empty () = - {} - Str (S.create 0) 0 0 + let empty () = + {} + Str (S.create 0) 0 0 { len result = 0 /\ inv result /\ eq (model result) (S.create 0) } - - let length r = - {} - len r + + let length r = + {} + len r { result = len r } - + (** - let rec get (r: rope) i = + let rec get (r: rope) i = { inv r /\ 0 <= i < len r } match r with - | Str s ofs len -> + | Str s ofs len -> S.get s (ofs + i) - | App l r _ -> + | App l r _ -> let n = length l in if i < n then get l i else get r (i - n) end { result = S.get (model r) i } **) - + end (* -Local Variables: +Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/ropes" -End: +End: *) diff --git a/examples/programs/same_fringe/same_fringe.mlw_SameFringe_leftlen_nonneg_1.v b/examples/programs/same_fringe/same_fringe.mlw_SameFringe_leftlen_nonneg_1.v index 93a6aa417db3bb56a7cd7c85657360383112bbb5..bb07d1aacf3feb44a55b48310c6e23f076cbeb0b 100644 --- a/examples/programs/same_fringe/same_fringe.mlw_SameFringe_leftlen_nonneg_1.v +++ b/examples/programs/same_fringe/same_fringe.mlw_SameFringe_leftlen_nonneg_1.v @@ -74,7 +74,7 @@ Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)), Parameter elt : Type. Inductive tree := - | Empty : tree + | Empty : tree | Node : tree -> elt -> tree -> tree . Parameter elements: tree -> (list elt). @@ -88,7 +88,7 @@ Axiom elements_def : forall (t:tree), end. Inductive enum := - | Done : enum + | Done : enum | Next : elt -> tree -> enum -> enum . Parameter enum_elements: enum -> (list elt). @@ -112,7 +112,7 @@ Axiom leftlen_def : forall (t:tree), Theorem leftlen_nonneg : forall (t:tree), (0%Z <= (leftlen t))%Z. (* YOU MAY EDIT THE PROOF BELOW *) -induction t; +induction t; intuition. rewrite (leftlen_def Empty). omega. diff --git a/examples/programs/vacid_0_red_black_trees.mlw b/examples/programs/vacid_0_red_black_trees.mlw index 4904c0a4f69037d62d759f6c101f8e9dabc3c353..4211e2ab663f8ab037055dba90e26a3d39b65251 100644 --- a/examples/programs/vacid_0_red_black_trees.mlw +++ b/examples/programs/vacid_0_red_black_trees.mlw @@ -116,9 +116,9 @@ module M match l with | Node Red (Node Red a kx vx b) ky vy c | Node Red a kx vx (Node Red b ky vy c) -> - Node Red (Node Black a kx vx b) ky vy (Node Black c k v r) + Node Red (Node Black a kx vx b) ky vy (Node Black c k v r) | _ -> - Node Black l k v r + Node Black l k v r end { bst result /\ (forall n : int. almost_rbtree n l -> rbtree n r -> rbtree (n+1) result) @@ -141,9 +141,9 @@ module M match r with | Node Red (Node Red b ky vy c) kz vz d | Node Red b ky vy (Node Red c kz vz d) -> - Node Red (Node Black l k v b) ky vy (Node Black c kz vz d) + Node Red (Node Black l k v b) ky vy (Node Black c kz vz d) | _ -> - Node Black l k v r + Node Black l k v r end { bst result /\ (forall n : int. almost_rbtree n r -> rbtree n l -> rbtree (n+1) result) diff --git a/examples/programs/vstte10_search_list/vstte10_search_list.mlw_SearchingALinkedList_WP_parameter search_loop_4.v b/examples/programs/vstte10_search_list/vstte10_search_list.mlw_SearchingALinkedList_WP_parameter search_loop_4.v index e8f37588659b6fc5e767f808c8d090b9148bb981..7dd05f06056b97d2dde73606b83b5cafe23ed1be 100644 --- a/examples/programs/vstte10_search_list/vstte10_search_list.mlw_SearchingALinkedList_WP_parameter search_loop_4.v +++ b/examples/programs/vstte10_search_list/vstte10_search_list.mlw_SearchingALinkedList_WP_parameter search_loop_4.v @@ -109,7 +109,7 @@ discriminate H8. injection H8; intros; subst; clear H8. clear H4 H5. left. -split. +split. rewrite (length_def _ (Cons 0%Z s)) in H2. generalize (Length_nonnegative _ s). omega. diff --git a/src/bench/whybench.ml b/src/bench/whybench.ml index 276efb09df48457270769166e83b3bb6bbee0daa..5011a8505ed4fc46bb7bb96158c663550c378de2 100644 --- a/src/bench/whybench.ml +++ b/src/bench/whybench.ml @@ -325,7 +325,7 @@ let () = && (not !opt_redo) then begin - eprintf "At least one bench is required or one prover and one file or + eprintf "At least one bench is required or one prover and one file or the verification of a database .@."; Arg.usage option_list usage_msg; exit 1 diff --git a/src/ide/db.mli b/src/ide/db.mli index 7586b0fe7de2dd82a93e58c6f48f864a55c10b33..f84789b52a4e171bc984f519ba5fce6a3f17e8f7 100644 --- a/src/ide/db.mli +++ b/src/ide/db.mli @@ -161,7 +161,7 @@ val add_proof_attempt : goal -> prover_id -> proof_attempt val remove_proof_attempt : proof_attempt -> unit (** removes a proof attempt from the database *) - + val set_obsolete : proof_attempt -> unit (** marks this proof as obsolete *) @@ -180,7 +180,7 @@ val add_transformation : goal -> transf_id -> transf @raise AlreadyExist if a transformation with the same id is already there *) -val remove_transformation : transf -> unit +val remove_transformation : transf -> unit (** Removes a proof attempt from the database. Beware that the subgoals are not removed by this function, you must remove them first using [remove_subgoal]. In other words, this function diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index c3517fc0d215ac2a20ef1c4d9c91ab37d1dfa31d..c7a8c40a71f763115f88ea85164249d15275f65a 100644 --- a/src/ide/gconfig.ml +++ b/src/ide/gconfig.ml @@ -334,7 +334,7 @@ let show_about_window () = let ( _ : GWindow.Buttons.about) = about_dialog#run () in about_dialog#destroy () -let set_labels_flag = +let set_labels_flag = let fl = Debug.lookup_flag "print_labels" in fun b -> (if b then Debug.set_flag else Debug.unset_flag) fl diff --git a/src/ide/newmain.ml b/src/ide/newmain.ml index e7d793bea2c35e07ec8d066f04e4aa340df3aa85..0246cf080e9bbea8e9f73e97703fcf8be5b785ce 100644 --- a/src/ide/newmain.ml +++ b/src/ide/newmain.ml @@ -373,7 +373,7 @@ let set_proof_state ~obsolete a = let model_index = Hashtbl.create 17 -let get_any_from_iter row = +let get_any_from_iter row = try let idx = goals_model#get ~row ~column:index_column in Hashtbl.find model_index idx @@ -391,14 +391,14 @@ let get_selected_row_references () = (fun path -> goals_model#get_row_reference path) goals_view#selection#get_selected_rows -let row_expanded b iter _path = +let row_expanded b iter _path = match get_any_from_iter iter with - | M.File f -> + | M.File f -> (* eprintf "file_expanded <- %b@." b; *) M.set_file_expanded f b - | M.Theory t -> + | M.Theory t -> (* eprintf "theory_expanded <- %b@." b; *) @@ -416,20 +416,20 @@ let row_expanded b iter _path = | M.Proof_attempt _ -> () -let (_:GtkSignal.id) = +let (_:GtkSignal.id) = goals_view#connect#row_collapsed ~callback:(row_expanded false) -let (_:GtkSignal.id) = +let (_:GtkSignal.id) = goals_view#connect#row_expanded ~callback:(row_expanded true) let notify any = let row,exp = match any with - | M.Goal g -> + | M.Goal g -> (* if M.goal_expanded g then begin - let n = + let n = Hashtbl.fold (fun _ _ acc -> acc+1) (M.external_proofs g) 0 in eprintf "expand_row on a goal with %d proofs@." n; @@ -441,7 +441,7 @@ let notify any = | M.Proof_attempt a -> a.M.proof_key,false | M.Transformation tr -> tr.M.transf_key,tr.M.transf_expanded in - if exp then goals_view#expand_to_path row#path else + if exp then goals_view#expand_to_path row#path else goals_view#collapse_row row#path; match any with | M.Goal g -> @@ -454,7 +454,7 @@ let notify any = set_proof_state ~obsolete:a.M.proof_obsolete a | M.Transformation tr -> set_row_status row tr.M.transf_proved - + let init = let cpt = ref (-1) in fun row any -> @@ -482,7 +482,7 @@ let init = | M.Goal g -> M.goal_expl g | M.Theory th -> M.theory_name th | M.File f -> Filename.basename f.M.file_name - | M.Proof_attempt a -> + | M.Proof_attempt a -> begin match a.M.prover with | M.Detected_prover p -> @@ -533,14 +533,14 @@ let () = let () = try eprintf "[Info] Opening session...@\n@[ "; - M.open_session ~env:gconfig.env + M.open_session ~env:gconfig.env (* ~provers:gconfig.provers *) ~config:gconfig.Gconfig.config ~init ~notify project_dir; M.maximum_running_proofs := gconfig.max_running_processes; eprintf "@]@\n[Info] Opening session: done@." with e -> - eprintf "@[Error while opening session:@ %a@.@]" + eprintf "@[Error while opening session:@ %a@.@]" Exn_printer.exn_printer e; exit 1 @@ -1175,7 +1175,7 @@ let reload () = with | e -> let e = match e with - | Loc.Located(loc,e) -> + | Loc.Located(loc,e) -> scroll_to_loc ~color:error_tag ~yalign:0.5 loc; e | e -> e in diff --git a/src/ide/session.ml b/src/ide/session.ml index 0e2595585d3767d2a87f5d365fcc56473dcf7e09..4187327f69deb5eb2a98109a1894d30290f61e7d 100644 --- a/src/ide/session.ml +++ b/src/ide/session.ml @@ -781,7 +781,7 @@ let file_exists fn = (**********************************) let reload_proof obsolete goal pid old_a = - let p = + let p = try Detected_prover (Util.Mstr.find pid !current_provers) with Not_found -> @@ -810,7 +810,7 @@ let reload_proof ~provers obsolete goal pid old_a = (* eprintf "proof_obsolete : %b@." obsolete; *) let a = raw_add_external_proof ~obsolete ~timelimit:old_a.timelimit - ~edit:old_a.edited_as goal p old_res + ~edit:old_a.edited_as goal p old_res in !notify_fun (Goal a.proof_goal) with Not_found -> @@ -876,7 +876,7 @@ and reload_trans _goal_obsolete goal _ tr = g.goal_name subgoal_name; *) (Some g, Util.Mstr.remove sum old_subgoals) - with Not_found -> + with Not_found -> (* eprintf "Merge phase 1: no old goal -> new goal '%s'@." subgoal_name; @@ -916,23 +916,23 @@ and reload_trans _goal_obsolete goal _ tr = if merged list starts with g : - g1 < ... gk <= h1 < ... < + g1 < ... gk <= h1 < ... < - then g1 .. g{k-1} are new and gk associated to h1, and then + then g1 .. g{k-1} are new and gk associated to h1, and then recursively merge g{k+1} ... and h2 ... otherwise, list starts - h1 < ... hk <= g1 <= ... < + h1 < ... hk <= g1 <= ... < .... Another formulation : if merged list starts with - - 1) g1 g2 ... - + + 1) g1 g2 ... + associate g1 to nothing and recursively process g2 ... 2) g1 h1 g2 ... with d(g1,h1) < d(h1,g2) @@ -940,20 +940,20 @@ and reload_trans _goal_obsolete goal _ tr = associate g1 to h1 and recursively process g2 ... 3) g1 h1 g2 ... with d(g1,h1) > d(h1,g2) - + ? 4) g1 h1 h2 ... - + PRELIMINARY: store the shape of the conclusion of the goal in the XML - file. + file. *) let rec associate_remaining_goals new_goals_map remaining acc = match new_goals_map with - | [] -> + | [] -> (* eprintf "Merge phase 3: dropping %d old goals@." (List.length remaining); @@ -962,7 +962,7 @@ and reload_trans _goal_obsolete goal _ tr = | (_,id,subgoal_name,subtask,sum,old_subgoal)::new_rem -> let ((obsolete,old_goal,rem) : bool * goal option * (string * goal) list) = match old_subgoal with - | Some _g -> + | Some _g -> (* eprintf "Merge phase 2: old goal '%s' -> new goal '%s'@." g.goal_name subgoal_name; @@ -970,13 +970,13 @@ and reload_trans _goal_obsolete goal _ tr = (false,old_subgoal,remaining) | None -> match remaining with - | [] -> + | [] -> (* eprintf "Merge phase 2: no old goal -> new goal '%s'@." subgoal_name; *) (false,None,[]) - | (_goal_name,g) :: rem -> + | (_goal_name,g) :: rem -> (* eprintf "Merge phase 2: old goal '%s' -> new goal '%s'@." g.goal_name subgoal_name; @@ -1161,7 +1161,7 @@ and load_proof_or_transf ~env mg a = let p = try Detected_prover (Util.Mstr.find prover !current_provers) - with Not_found -> + with Not_found -> Undetected_prover prover in let res = match a.Xml.elements with @@ -1261,7 +1261,7 @@ let open_session ~env ~config ~init ~notify dir = init_fun := init; notify_fun := notify; project_dir := dir; current_env := Some env; let provers = Whyconf.get_provers config in - current_provers := + current_provers := Util.Mstr.fold (get_prover_data env) provers Util.Mstr.empty; begin try let xml = Xml.from_file (Filename.concat dir db_filename) in @@ -1285,7 +1285,7 @@ let save_session () = let f = Filename.concat !project_dir db_filename in begin if Sys.file_exists f then let b = f ^ ".bak" in - if Sys.file_exists b then Sys.remove b ; + if Sys.file_exists b then Sys.remove b ; Sys.rename f b end; save f @@ -1330,7 +1330,7 @@ let rec prover_on_goal ~timelimit p g = let a = try Hashtbl.find g.external_proofs id with Not_found -> - raw_add_external_proof ~obsolete:false ~timelimit ~edit:"" g + raw_add_external_proof ~obsolete:false ~timelimit ~edit:"" g (Detected_prover p) Undone in let () = redo_external_proof ~timelimit g a in @@ -1450,10 +1450,10 @@ let cancel a = (*********************************) type report = - | Wrong_result of Call_provers.prover_result * Call_provers.prover_result + | Wrong_result of Call_provers.prover_result * Call_provers.prover_result | CallFailed of exn - | Prover_not_installed - | No_former_result + | Prover_not_installed + | No_former_result let reports = ref [] @@ -1542,11 +1542,11 @@ let check_all ~callback = !all_files; let timeout () = Printf.eprintf "Progress: %d/%d\r%!" !proofs_done !proofs_to_do; - if !proofs_done = !proofs_to_do then + if !proofs_done = !proofs_to_do then begin Printf.eprintf "\n%!"; decr maximum_running_proofs; - callback !reports; + callback !reports; false end else true diff --git a/src/ide/session.mli b/src/ide/session.mli index c3cd5a1ba6251928719999e1f9185287c2b61f11..75f1cddcfe8198e1c04d710d0e1fb4df257cdda5 100644 --- a/src/ide/session.mli +++ b/src/ide/session.mli @@ -236,7 +236,7 @@ module Make(O: OBSERVER) : sig context_unproved_goals_only:bool -> any -> unit (** [replay a] reruns proofs under [a] if obsolete_only is set then does not rerun non-obsolete proofs - if context_unproved_goals_only is set then reruns only proofs + if context_unproved_goals_only is set then reruns only proofs with result was 'valid' *) @@ -244,14 +244,14 @@ module Make(O: OBSERVER) : sig (** [cancel a] marks all proofs under [a] as obsolete *) type report = - | Wrong_result of Call_provers.prover_result * Call_provers.prover_result + | Wrong_result of Call_provers.prover_result * Call_provers.prover_result | CallFailed of exn - | Prover_not_installed - | No_former_result + | Prover_not_installed + | No_former_result val check_all: callback:((string * string * report) list -> unit) -> unit (** [check_all ()] reruns all the proofs of the session, and reports - all difference with the current state + all difference with the current state (does not change the session state) When finished, calls the callback with the list of failed comparisons, which are triples (goal name, prover, report) diff --git a/src/ide/termcode.ml b/src/ide/termcode.ml index e558d42f2d873705ec185da0f4b514ba008c4aa1..60ee2a7f873249339904f48b3b586e7ab91e120a 100644 --- a/src/ide/termcode.ml +++ b/src/ide/termcode.ml @@ -1,3 +1,22 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010-2011 *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + (* distance of two terms *) let dist_bool b = if b then 0.0 else 1.0 @@ -11,30 +30,30 @@ let rec pat_dist p1 p2 = match p1.pat_node, p2.pat_node with | Pwild, Pwild | Pvar _, Pvar _ -> 0.0 | Papp (f1, l1), Papp (f2, l2) -> - if ls_equal f1 f2 then - 0.5 *. average (List.map2 pat_dist l1 l2) - else 1.0 + if ls_equal f1 f2 then + 0.5 *. average (List.map2 pat_dist l1 l2) + else 1.0 | Pas (p1, _), Pas (p2, _) -> pat_dist p1 p2 | Por (p1, q1), Por (p2, q2) -> - 0.5 *. average [pat_dist p1 p2 ; pat_dist q1 q2 ] + 0.5 *. average [pat_dist p1 p2 ; pat_dist q1 q2 ] | _ -> 1.0 else 1.0 -let rec t_dist c1 c2 m1 m2 e1 e2 = +let rec t_dist c1 c2 m1 m2 e1 e2 = let t_d = t_dist c1 c2 m1 m2 in match e1.t_node, e2.t_node with - | Tvar v1, Tvar v2 -> - begin - try dist_bool (Mvs.find v1 m1 = Mvs.find v2 m2) - with Not_found -> 1.0 - end + | Tvar v1, Tvar v2 -> + begin + try dist_bool (Mvs.find v1 m1 = Mvs.find v2 m2) + with Not_found -> 1.0 + end | Tconst c1, Tconst c2 -> 0.5 *. dist_bool (c1 = c2) | Tapp(ls1,tl1), Tapp(ls2,tl2) -> - if ls_equal ls1 ls2 then - 0.5 *. average (List.map2 t_d tl1 tl2) - else 1.0 + if ls_equal ls1 ls2 then + 0.5 *. average (List.map2 t_d tl1 tl2) + else 1.0 | Tif(c1,t1,e1), Tif(c2,t2,e2) -> - 0.5 *. average [t_d c1 c2 ; t_d t1 t2 ; t_d e1 e2] + 0.5 *. average [t_d c1 c2 ; t_d t1 t2 ; t_d e1 e2] | Tlet(t1,b1), Tlet(t2,b2) -> let u1,e1 = t_open_bound b1 in let u2,e2 = t_open_bound b2 in @@ -42,7 +61,7 @@ let rec t_dist c1 c2 m1 m2 e1 e2 = let m2 = vs_rename_alpha c2 m2 u2 in 0.5 *. average [t_d t1 t2; t_dist c1 c2 m1 m2 e1 e2] | Tcase (t1,bl1), Tcase (t2,bl2) -> - if List.length bl1 = List.length bl2 then + if List.length bl1 = List.length bl2 then let br_dist ((pat1,_,_) as b1) ((pat2,_,_) as b2) = let p1,e1 = t_open_branch b1 in let p2,e2 = t_open_branch b2 in @@ -51,8 +70,8 @@ let rec t_dist c1 c2 m1 m2 e1 e2 = average [pat_dist pat1 pat2 ; t_dist c1 c2 m1 m2 e1 e2] in 0.5 *. average (t_d t1 t2 :: List.map2 br_dist bl1 bl2) - else - 1.0 + else + 1.0 | Teps b1, Teps b2 -> let u1,e1 = t_open_bound b1 in let u2,e2 = t_open_bound b2 in @@ -61,18 +80,18 @@ let rec t_dist c1 c2 m1 m2 e1 e2 = 0.5 *. t_dist c1 c2 m1 m2 e1 e2 | Tquant (q1,((vl1,_,_,_) as b1)), Tquant (q2,((vl2,_,_,_) as b2)) -> if q1 = q2 && - list_all2 (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2 - then + list_all2 (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2 + then let vl1,_,e1 = t_open_quant b1 in let vl2,_,e2 = t_open_quant b2 in let m1 = vl_rename_alpha c1 m1 vl1 in let m2 = vl_rename_alpha c2 m2 vl2 in 0.5 *. t_dist c1 c2 m1 m2 e1 e2 - else - 1.0 + else + 1.0 | Tbinop (a,f1,g1), Tbinop (b,f2,g2) -> if a = b then 0.5 *. average [ t_d f1 f2 ; t_d g1 g2] - else 1.0 + else 1.0 | Tnot f1, Tnot f2 -> 0.5 *. t_d f1 f2 | Ttrue, Ttrue | Tfalse, Tfalse -> 0.0 | _ -> 1.0 @@ -80,22 +99,22 @@ let rec t_dist c1 c2 m1 m2 e1 e2 = let t_dist t1 t2 = t_dist (ref (-1)) (ref (-1)) Mvs.empty Mvs.empty t1 t2 -(* similarity code of terms, or of "shapes" +(* similarity code of terms, or of "shapes" -example: +example: shape(forall x:int, x * x >= 0) = Forall(Int,App(infix_gteq,App(infix_st,Tvar 0,Tvar 0),Const(0))) i.e: de bruijn indexes, first-order term - code of a shape: maps shapes into real numbers in [0..1], such that + code of a shape: maps shapes into real numbers in [0..1], such that compare t1 t2 = code (shape t1) -. code (shape t2) is a good comparison operator code(n:int) = 1 / (1+abs(n)) - so code(0) = 1, code(1) = 0.5, + so code(0) = 1, code(1) = 0.5, code(x:real) = 1 / (1+abs x) @@ -104,17 +123,17 @@ example: more generally, for any type t = C0 x | ... | Cn x code(Ci x) = (2i + h(x)) / (2n+1) - + *) - + (* not good ? for any type t = t0 x ... x tn hash((x0,..,x_n)) = (2i + h(x)) / (2n+1) *) - + let const_code = function | ConstInt n -> 1.0 /. (1.0 +. abs (float_of_string n)) /. 3.0 @@ -124,7 +143,7 @@ let rec t_code c m t = let fn = t_code c m in let divide i c = (float(i+i) +. c) /. 23.0 in (* 12 constructors -> divide by 23 *) - match t.t_node with + match t.t_node with | Tconst c -> divide 0 (const_code c) | Tvar v -> divide 1 (Mvs.find_default v (var_code v) m) | Tapp (s,l) -> diff --git a/src/ide/termcode.mli b/src/ide/termcode.mli index dd9c20d0b84cea38243369654a2c5e24bea08d27..0decfb2ff59fbbfe5af8312f5ca400a12fbef84d 100644 --- a/src/ide/termcode.mli +++ b/src/ide/termcode.mli @@ -1,3 +1,22 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010-2011 *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + val t_dist : term -> term -> float (** returns an heuristic distance between the two given terms. The result is always between 0.0 and 1.0. It is guaranteed that if diff --git a/src/ide/xml.mll b/src/ide/xml.mll index 0594a8b6195669b4e5c91a3e13807f8f47222ff4..957ebac809217079707c73a26a73f505157c8112 100644 --- a/src/ide/xml.mll +++ b/src/ide/xml.mll @@ -58,32 +58,32 @@ let space = [' ' '\t' '\r' '\n'] let digit = ['0'-'9'] let letter = ['a'-'z' 'A'-'Z'] -let ident = (letter | digit | '_') + -let sign = '-' | '+' +let ident = (letter | digit | '_') + +let sign = '-' | '+' let integer = sign? digit+ let mantissa = ['e''E'] sign? digit+ let real = sign? digit* '.' digit* mantissa? -let escape = ['\\''"''n''t''r'] +let escape = ['\\''"''n''t''r'] rule xml_prolog = parse -| space+ +| space+ { xml_prolog lexbuf } | "" { xml_doctype "1.0" "" lexbuf } | "" { xml_doctype "1.0" "" lexbuf } -| "'])* "?>" +| "'])* "?>" { Format.eprintf "[Xml warning] prolog ignored@\n"; xml_doctype "1.0" "" lexbuf } -| _ +| _ { parse_error "wrong prolog" } - + and xml_doctype version encoding = parse -| space+ +| space+ { xml_doctype version encoding lexbuf } -| "']* ">" - { match elements [] [] lexbuf with - | [x] -> +| "']* ">" + { match elements [] [] lexbuf with + | [x] -> { version = version; encoding = encoding; doctype = doctype; @@ -92,37 +92,37 @@ and xml_doctype version encoding = parse } | _ -> parse_error "there should be exactly one root element" } -| _ +| _ { parse_error "wrong DOCTYPE" } - + and elements group_stack element_stack = parse - | space+ + | space+ { elements group_stack element_stack lexbuf } - | '<' (ident as elem) + | '<' (ident as elem) { attributes group_stack element_stack elem [] lexbuf } | "' { match group_stack with - | [] -> - Format.eprintf - "[Xml warning] unexpected closing Xml element `%s'@\n" + | [] -> + Format.eprintf + "[Xml warning] unexpected closing Xml element `%s'@\n" celem; elements group_stack element_stack lexbuf | (elem,att,stack)::g -> if celem <> elem then - Format.eprintf - "[Xml warning] Xml element `%s' closed by `%s'@\n" + Format.eprintf + "[Xml warning] Xml element `%s' closed by `%s'@\n" elem celem; let e = { name = elem; attributes = att; elements = List.rev element_stack; } - in elements g (e::stack) lexbuf + in elements g (e::stack) lexbuf } | '<' { Format.eprintf "[Xml warning] unexpected '<'@\n"; - elements group_stack element_stack lexbuf } - | eof + elements group_stack element_stack lexbuf } + | eof { match group_stack with | [] -> element_stack | (elem,_,_)::_ -> @@ -135,13 +135,13 @@ and elements group_stack element_stack = parse and attributes groupe_stack element_stack elem acc = parse | space+ { attributes groupe_stack element_stack elem acc lexbuf } - | (ident as key) space* '=' + | (ident as key) space* '=' { let v = value lexbuf in attributes groupe_stack element_stack elem ((key,v)::acc) lexbuf } - | '>' + | '>' { elements ((elem,acc,element_stack)::groupe_stack) [] lexbuf } | "/>" - { let e = { name = elem ; + { let e = { name = elem ; attributes = acc; elements = [] } in @@ -152,23 +152,23 @@ and attributes groupe_stack element_stack elem acc = parse { parse_error "unclosed element, `>' expected" } and value = parse - | space+ + | space+ { value lexbuf } - | '"' + | '"' { Buffer.clear buf; - string_val lexbuf } + string_val lexbuf } | _ as c { parse_error ("invalid value starting with " ^ String.make 1 c) } | eof { parse_error "unterminated keyval pair" } -and string_val = parse - | '"' +and string_val = parse + | '"' { Buffer.contents buf } | [^ '\\' '"'] as c { Buffer.add_char buf c; string_val lexbuf } - | '\\' (['\\''\"'] as c) + | '\\' (['\\''\"'] as c) { Buffer.add_char buf c; string_val lexbuf } | '\\' 'n' diff --git a/src/main.ml b/src/main.ml index 7cd49bb7c4effb4054a833de72565ba73bb8ee7b..5b9139be8d13bd393e7c622cf64689c68ca68445 100644 --- a/src/main.ml +++ b/src/main.ml @@ -490,7 +490,7 @@ let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_glist) = if Sys.file_exists oldf then begin - let backup = oldf ^ ".bak" in + let backup = oldf ^ ".bak" in Sys.rename oldf backup; Some(open_in backup) end @@ -515,17 +515,17 @@ let do_input env drv = function if !opt_type_only then () else - match !opt_coq_realization with - | Some f -> - Queue.iter (do_coq_realize_theory env drv f fname m) tlist - | None -> - if Queue.is_empty tlist then - let glist = Queue.create () in - let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in - let do_th _ (t,th) = do_theory env drv fname t th glist in - Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty) - else - Queue.iter (do_local_theory env drv fname m) tlist + match !opt_coq_realization with + | Some f -> + Queue.iter (do_coq_realize_theory env drv f fname m) tlist + | None -> + if Queue.is_empty tlist then + let glist = Queue.create () in + let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in + let do_th _ (t,th) = do_theory env drv fname t th glist in + Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty) + else + Queue.iter (do_local_theory env drv fname m) tlist let () = try diff --git a/src/printer/alt_ergo.ml b/src/printer/alt_ergo.ml index e6486323798299ca30aa486f46e06159ff300649..b7428de831fdb0095ba71369780d3ce026cd858d 100644 --- a/src/printer/alt_ergo.ml +++ b/src/printer/alt_ergo.ml @@ -104,8 +104,8 @@ let rec print_fmla info fmt f = match f.t_node with end | Tquant (q, fq) -> let vl, tl, f = t_open_quant fq in - let q, tl = match q with - | Tforall -> "forall", tl + let q, tl = match q with + | Tforall -> "forall", tl | Texists -> "exists", [] (* Alt-ergo has no triggers for exists *) in let forall fmt v = diff --git a/src/printer/coq.ml b/src/printer/coq.ml index db4cf077b3bf06aa253537b9f81b21bcebdd4f5d..9329200a81c47169329fbb0cf495197b1c6cda86 100644 --- a/src/printer/coq.ml +++ b/src/printer/coq.ml @@ -377,7 +377,7 @@ let produce_remaining_proofs ~old fmt = fprintf fmt "(* OBSOLETE PROOF *)@\n"; try while true do let s = input_line ch in - if s = proof_end then + if s = proof_end then begin fprintf fmt "(* END OF OBSOLETE PROOF *)@\n@\n"; raise Exit @@ -482,7 +482,7 @@ let print_ind_decl info fmt d = (print_ind_decl info fmt d; forget_tvs ()) let print_pkind info fmt = function - | Paxiom -> + | Paxiom -> if info.realization then fprintf fmt "Lemma" else @@ -495,7 +495,7 @@ let print_proof ~old info fmt = function | Plemma | Pgoal -> realization ~old fmt true | Paxiom -> - realization ~old fmt info.realization + realization ~old fmt info.realization | Pskip -> () let print_decl ~old info fmt d = match d.d_node with @@ -560,7 +560,7 @@ let print_theory _env pr thpr ~old fmt th = info_syn = Mid.empty (* get_syntax_map_of_theory th *); info_rem = Mid.empty; realization = true; - } + } in print_tdecls ~old info fmt th.th_decls; produce_remaining_proofs ~old fmt diff --git a/src/printer/gappa.ml b/src/printer/gappa.ml index f486e4c03c0b0499da65d75e167f2b2af45ddf08..7cb6996864ee45abb928fe498c4dcfb693ab96b5 100644 --- a/src/printer/gappa.ml +++ b/src/printer/gappa.ml @@ -166,7 +166,7 @@ let rec print_fmla info fmt f = | None -> print_ident fmt id end | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ -> - (* TODO: distinguish between type of t1 and t2 + (* TODO: distinguish between type of t1 and t2 the following is OK only for real of integer *) begin try diff --git a/src/programs/pgm_env.ml b/src/programs/pgm_env.ml index e617a60a7562c3fd35693f318a961169727eeb28..d022a7f411d686b4702ada14ad1bd062975cba2c 100644 --- a/src/programs/pgm_env.ml +++ b/src/programs/pgm_env.ml @@ -43,7 +43,7 @@ let create env retrieve = { exception ModuleNotFound of string list * string let find_library penv sl = - try + try Hashtbl.find penv.memo sl with Not_found -> Hashtbl.add penv.memo sl (Mstr.empty, Mstr.empty); diff --git a/src/programs/pgm_ttree.ml b/src/programs/pgm_ttree.ml index 38cda2309adc60f49fb9aeb167ffb386204384c6..0ea7d6698007bea504616094d1770b520e64fcd6 100644 --- a/src/programs/pgm_ttree.ml +++ b/src/programs/pgm_ttree.ml @@ -39,7 +39,7 @@ type for_direction = Ptree.for_direction (* phase 1: introduction of destructive types *) (*** -type dregion = { +type dregion = { dr_tv : Denv.type_var; dr_ty : Denv.dty; } @@ -58,7 +58,7 @@ and dtype_c = { dc_result_type : dtype_v; dc_effect : deffect; dc_pre : Denv.dfmla; - dc_post : (Denv.dty * Denv.dfmla) * + dc_post : (Denv.dty * Denv.dfmla) * (Term.lsymbol * (Denv.dty option * Denv.dfmla)) list; } and dbinder = ident * Denv.dty * dtype_v @@ -67,7 +67,7 @@ and dbinder = ident * Denv.dty * dtype_v (* user type_v *) type dpre = Ptree.pre -type dpost_fmla = Ptree.lexpr +type dpost_fmla = Ptree.lexpr type dexn_post_fmla = Ptree.lexpr type dpost = dpost_fmla * (Term.lsymbol * dexn_post_fmla) list diff --git a/src/programs/pgm_types.ml b/src/programs/pgm_types.ml index c70c9071b8d22c67ab9606c45b887580ccf9140c..d7b132b10f2056a2e43409c496c0564063bfcf99 100644 --- a/src/programs/pgm_types.ml +++ b/src/programs/pgm_types.ml @@ -591,7 +591,7 @@ end = struct print_post c.c_post and print_binder fmt x = - fprintf fmt "(%a/%a:%a)" + fprintf fmt "(%a/%a:%a)" print_vs x.pv_effect print_vs x.pv_pure print_type_v x.pv_tv end diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml index 018595e9a13c9c183fbd13683dc0480252caf095..aca397232842abd0f93474d2e16c9a5501409fa7 100644 --- a/src/programs/pgm_typing.ml +++ b/src/programs/pgm_typing.ml @@ -545,27 +545,27 @@ and dexpr_desc ~ghost env loc = function let e2 = dexpr ~ghost env e2 in let x = Typing.string_list_of_qualid [] q in let ls = - try ns_find_ls (get_namespace (impure_uc env.uc)) x - with Not_found -> errorm ~loc "unbound record field %a" print_qualid q + try ns_find_ls (get_namespace (impure_uc env.uc)) x + with Not_found -> errorm ~loc "unbound record field %a" print_qualid q in new_regions_vars (); begin match specialize_lsymbol ~loc (Htv.create 17) ls with - | [ty1], Some ty2 -> - expected_type e1 ty1; - expected_type e2 ty2 - | _ -> - assert false + | [ty1], Some ty2 -> + expected_type e1 ty1; + expected_type e2 ty2 + | _ -> + assert false end; begin match Typing.is_projection (impure_uc env.uc) ls with - | Some (ts, _, i) -> - let mt = get_mtsymbol ts in - let j = - try mutable_field mt.mt_effect i - with Not_found -> errorm ~loc "not a mutable field" - in - DEassign (e1, ls, j, e2), dty_unit env.uc - | None -> - errorm ~loc "unbound record field %a" print_qualid q + | Some (ts, _, i) -> + let mt = get_mtsymbol ts in + let j = + try mutable_field mt.mt_effect i + with Not_found -> errorm ~loc "not a mutable field" + in + DEassign (e1, ls, j, e2), dty_unit env.uc + | None -> + errorm ~loc "unbound record field %a" print_qualid q end | Ptree.Esequence (e1, e2) -> @@ -880,7 +880,7 @@ let iterm env l = Denv.term env.i_pures t let variant_rel_int env loc = - let find s = + let find s = try find_ls ~pure:true env s with Not_found -> errorm ~loc "cannot find symbol %s" s in @@ -985,7 +985,7 @@ let make_logic_app gl loc ty ls el = let t = fs_app ls (List.rev args) (purify ty) in IElogic (t, lvars, gvars) | None -> - IElogic (mk_t_if gl (ps_app ls (List.rev args)), lvars, gvars) + IElogic (mk_t_if gl (ps_app ls (List.rev args)), lvars, gvars) end | ({ iexpr_desc = IElogic (t, lvt, gvt) }, _) :: r -> make (Svs.union lvars lvt) (Spv.union gvars gvt) (t :: args) r @@ -995,7 +995,7 @@ let make_logic_app gl loc ty ls el = make lvars (Spv.add v gvars) (t_var v.pv_pure :: args) r | (e, _) :: r -> let v = create_ivsymbol (id_user "x" loc) e.iexpr_type in - let lvars = Svs.add v.i_impure lvars in + let lvars = Svs.add v.i_impure lvars in let d = mk_iexpr loc ty (make lvars gvars (t_var v.i_pure :: args) r) in IElet (v, e, d) in @@ -1167,22 +1167,22 @@ and iexpr_desc gl env loc ty = function let x1 = create_ivsymbol (id_fresh "x") e1.iexpr_type in let x2 = create_ivsymbol (id_fresh "x") e2.iexpr_type in let r = match e1.iexpr_type.ty_node with - | Ty.Tyapp (ts, tyl) -> - let mt = get_mtsymbol ts in + | Ty.Tyapp (ts, tyl) -> + let mt = get_mtsymbol ts in let r = regions_tyapp mt.mt_effect mt.mt_regions tyl in List.nth r j - | Ty.Tyvar _ -> - assert false + | Ty.Tyvar _ -> + assert false in let ef = { ie_reads = []; ie_writes = [r]; ie_raises = [] } in let q = - let ls = (get_psymbol ls).ps_pure in - t_equ (fs_app ls [t_var x1.i_pure] x2.i_pure.vs_ty) (t_var x2.i_pure) + let ls = (get_psymbol ls).ps_pure in + t_equ (fs_app ls [t_var x1.i_pure] x2.i_pure.vs_ty) (t_var x2.i_pure) in let q = (create_vsymbol (id_fresh "result") ty, q), [] in let c = { - ic_result_type = ITpure ty; ic_effect = ef; - ic_pre = t_true; ic_post = q } + ic_result_type = ITpure ty; ic_effect = ef; + ic_pre = t_true; ic_post = q } in IElet (x1, e1, mk_iexpr loc ty ( IElet (x2, e2, mk_iexpr loc ty ( @@ -1281,11 +1281,11 @@ and iletrec gl env dl = let p, e, q = t in let phi0 = create_ivsymbol (id_fresh "variant") (t_type phi) in let e_phi = { - iexpr_desc = IElogic (phi, Svs.empty, Spv.empty); - (* FIXME: vars(phi) *) - iexpr_type = t_type phi; + iexpr_desc = IElogic (phi, Svs.empty, Spv.empty); + (* FIXME: vars(phi) *) + iexpr_type = t_type phi; iexpr_loc = e.iexpr_loc } - in + in let e = { e with iexpr_desc = IElet (phi0, e_phi, e) } in Some (phi0, phi, r), (p, e, q) in @@ -1595,10 +1595,10 @@ and expr_desc gl env loc ty = function let ef = e1.expr_effect in let ef, inv = option_map_fold term_effect ef a.loop_invariant in let ef, var = match a.loop_variant with - | Some (t, ls) -> - let ef, t = term_effect ef t in ef, Some (t, ls) - | None -> - ef, None + | Some (t, ls) -> + let ef, t = term_effect ef t in ef, Some (t, ls) + | None -> + ef, None in let a = { loop_invariant = inv; loop_variant = var } in Eloop (a, e1), type_v_unit gl, ef diff --git a/src/programs/pgm_wp.ml b/src/programs/pgm_wp.ml index 337a08af50465cb32835e5dd72bd98560b79107f..3237642d9c7198e1bb7a940a1613e5d19841a3fc 100644 --- a/src/programs/pgm_wp.ml +++ b/src/programs/pgm_wp.ml @@ -384,7 +384,7 @@ let wp_expl l f = (* 0 <= phi0 and phi < phi0 *) let default_variant le lt phi phi0 = - t_and + t_and (ps_app le [t_int_const "0"; phi0]) (ps_app lt [phi; phi0]) @@ -394,7 +394,7 @@ let while_post_block inv var lab e = t_true | Some (phi, Vint (le, lt)) -> let old_phi = term_at lab phi in - default_variant le lt phi old_phi + default_variant le lt phi old_phi | Some (phi, Vuser r) -> ps_app r [phi; term_at lab phi] in diff --git a/src/tools/cpulimit-win.c b/src/tools/cpulimit-win.c index 5da6d7a159ed021c2a1fcb71c9a37869f79abc77..5d86168af39fa681521b6aae0350ebf216b2c199 100644 --- a/src/tools/cpulimit-win.c +++ b/src/tools/cpulimit-win.c @@ -39,7 +39,7 @@ int main(int argc, char *argv[]) { for (i = 2; i < argc; i++) s += strlen(argv[i]) + 1; // CreateProcess does not allow more than 32767 bytes for command line parameter - if (s > 32767) { + if (s > 32767) { printf("%s: Error: parameter's length exceeds CreateProcess limits\n", argv[0]); return -1; } @@ -50,7 +50,7 @@ int main(int argc, char *argv[]) { } *p = '\0'; for (i = 2; i < argc; i++) { - strncat(p, argv[i], strlen(argv[i])); + strncat(p, argv[i], strlen(argv[i])); if (i < argc - 1) strcat(p, " "); } // launches "child" process with command line parameter @@ -70,4 +70,4 @@ int main(int argc, char *argv[]) { } // How to compile under Cygwin (needs make, gcc and win32api): -// gcc -Wall -o cpulimit cpulimit.c +// gcc -Wall -o cpulimit cpulimit.c diff --git a/src/transform/close_epsilon.mli b/src/transform/close_epsilon.mli index f0bb15dcd659f89224244909c27692182bfc0d01..0b1efad25169129badb8a15d3571fadb48f665b1 100644 --- a/src/transform/close_epsilon.mli +++ b/src/transform/close_epsilon.mli @@ -18,12 +18,11 @@ (**************************************************************************) (** The aim of this translation is to obtain terms where all epsilon - * abstractions are closed *) + abstractions are closed *) (** We do this by applying the following rewriting rule: - εx.P(x) => εF.(P(F@yâ‚@...@y_n)) where yâ‚...y_n are the free variable in P and - @ is the higher-order application symbol. - *) + eps x.P(x) => eps F.(P(F@y_1@...@y_n)) where y_1...y_n are + the free variables in P and @ is the higher-order application symbol. *) open Term diff --git a/src/transform/encoding_decorate.mli b/src/transform/encoding_decorate.mli index dbbdc9188ad8ac72b10eb35763c4717acddcb011..b69e3a33a0c13ddd732662fa506c4755a3d07134 100644 --- a/src/transform/encoding_decorate.mli +++ b/src/transform/encoding_decorate.mli @@ -16,3 +16,4 @@ (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* *) (**************************************************************************) + diff --git a/src/transform/encoding_twin.mli b/src/transform/encoding_twin.mli index dbbdc9188ad8ac72b10eb35763c4717acddcb011..b69e3a33a0c13ddd732662fa506c4755a3d07134 100644 --- a/src/transform/encoding_twin.mli +++ b/src/transform/encoding_twin.mli @@ -16,3 +16,4 @@ (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* *) (**************************************************************************) + diff --git a/src/util/rc.mll b/src/util/rc.mll index 12858ef88d8d3c0e0fdef753a93bf03b744d44e0..db477741129d06c368a8ebd966175b1b9602f6cc 100644 --- a/src/util/rc.mll +++ b/src/util/rc.mll @@ -354,16 +354,16 @@ let from_file f = let c = try open_in f with Sys_error s -> raise (CannotOpen (f, s)) in - try + try let r = from_channel c in close_in c; r - with + with | SyntaxError s -> close_in c; raise (SyntaxErrorFile (f, s)) | e -> close_in c; raise e let () = Exn_printer.register (fun fmt e -> match e with - | CannotOpen (_, s) -> + | CannotOpen (_, s) -> Format.fprintf fmt "system error: `%s'" s - | SyntaxErrorFile (f, s) -> + | SyntaxErrorFile (f, s) -> Format.fprintf fmt "syntax error in %s: %s" f s | _ -> raise e) diff --git a/src/util/sysutil.ml b/src/util/sysutil.ml index c273c7d2dc55b0a8f1eb23ab612e3d73d0bff888..2ad46305f1e335c504b3355b4b09d6242aea3474 100644 --- a/src/util/sysutil.ml +++ b/src/util/sysutil.ml @@ -157,9 +157,9 @@ let p1 = path_of_file "../src/f.why" let relativize_filename base f = let rec aux ab af = - match ab,af with + match ab,af with | x::rb, y::rf when x=y -> aux rb rf - | _ -> + | _ -> let rec aux2 acc p = match p with | [] -> acc diff --git a/src/util/util.mli b/src/util/util.mli index 63189dc66f68ac75dfb9ba89ec182e61bfc493bb..02ef96b190c300d97912c48cfaaa63c2207e18f4 100644 --- a/src/util/util.mli +++ b/src/util/util.mli @@ -107,13 +107,13 @@ val list_first : ('a -> 'b option) -> 'a list -> 'b val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list val list_iteri : (int -> 'a -> unit) -> 'a list -> unit val list_fold_lefti : ('a -> int -> 'b -> 'a) -> 'a -> 'b list -> 'a - (** similar to List.map, List.iter and List.fold_left, + (** similar to List.map, List.iter and List.fold_left, but with element index passed as extra argument (in 0..len-1) *) val prefix : int -> 'a list -> 'a list (** the first n elements of a list *) val chop : int -> 'a list -> 'a list - (** removes the first n elements of a list; + (** removes the first n elements of a list; raises Invalid_argument if the list is not long enough *) (* boolean fold accumulators *) diff --git a/src/why3doc/doc_html.ml b/src/why3doc/doc_html.ml index e30af8acaf5071b275a96ad9939fffc7a6537562..ce2e77b5ddb648de684a42f77d754d4a5f8a6ed8 100644 --- a/src/why3doc/doc_html.ml +++ b/src/why3doc/doc_html.ml @@ -433,7 +433,7 @@ let print_tdecl fmt td = match td.td_node with m.meta_name (print_list comma print_meta_arg) al let print_theory fmt th = - fprintf fmt "@[%a %a@\n%a@]@\n%a@." + fprintf fmt "@[%a %a@\n%a@]@\n%a@." keyword "theory" print_th th (print_list newline2 print_tdecl) th.th_decls keyword "end" @@ -444,7 +444,7 @@ let print_header fmt ?(title="") ?css () = fprintf fmt "@\n@\n"; begin match css with | None -> () - | Some f -> fprintf fmt + | Some f -> fprintf fmt "@\n" f end; fprintf fmt "%s@\n" title; diff --git a/src/why3doc/doc_main.ml b/src/why3doc/doc_main.ml index 2551838b982e3d3e5be412b85000846a60314f1f..6d3005702f7f20adf5a3ae8c8ea477923a3f6971 100644 --- a/src/why3doc/doc_main.ml +++ b/src/why3doc/doc_main.ml @@ -42,7 +42,7 @@ let option_list = Arg.align [ let add_opt_file x = Queue.add x opt_queue -let () = +let () = Arg.parse option_list add_opt_file usage_msg; let config = Whyconf.read_config None in let main = Whyconf.get_main config in @@ -58,7 +58,7 @@ let css = let do_file env fname = let m = Env.read_file env fname in - let base = + let base = let f = Filename.basename fname in match !opt_output with | None -> f diff --git a/src/why3doc/to_html.mll b/src/why3doc/to_html.mll index b3ef472af0707dfdf1124fd410e41805e72ff470..5d38cb02475aa5c0ebc578ebbee2f65ee45f53c5 100644 --- a/src/why3doc/to_html.mll +++ b/src/why3doc/to_html.mll @@ -55,19 +55,19 @@ let ht = Hashtbl.create 97 in List.iter (fun s -> Hashtbl.add ht s ()) - [ "theory"; "end"; + [ "theory"; "end"; "type"; "function"; "predicate"; "clone"; "use"; "import"; "export"; "axiom"; "inductive"; "goal"; "lemma"; - + "match"; "with"; "let"; "in"; "if"; "then"; "else"; "forall"; "exists"; "as"; "assert"; "begin"; "do"; "done"; "downto"; "else"; "exception"; "val"; "for"; "fun"; - "if"; "in"; + "if"; "in"; "module"; "mutable"; - "rec"; "then"; "to"; + "rec"; "then"; "to"; "try"; "while"; "invariant"; "variant"; "raise"; "label"; ]; fun s -> Hashtbl.mem ht s @@ -78,22 +78,22 @@ let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* rule scan fmt = parse | "(*)" { fprintf fmt "(*)"; scan fmt lexbuf } - | "(*" { fprintf fmt "(*"; - comment fmt lexbuf; + | "(*" { fprintf fmt "(*"; + comment fmt lexbuf; fprintf fmt ""; scan fmt lexbuf } | eof { () } - | ident as s + | ident as s { if is_keyword s then begin fprintf fmt "%s" s - end else - fprintf fmt "%s" s; + end else + fprintf fmt "%s" s; scan fmt lexbuf } | "<" { fprintf fmt "<"; scan fmt lexbuf } | "&" { fprintf fmt "&"; scan fmt lexbuf } | "\n" { newline fmt (); scan fmt lexbuf } | '"' { fprintf fmt "\""; string fmt lexbuf; scan fmt lexbuf } - | "'\"'" + | "'\"'" | _ as s { fprintf fmt "%s" s; scan fmt lexbuf } and comment fmt = parse @@ -104,7 +104,7 @@ and comment fmt = parse | '"' { fprintf fmt "\""; string fmt lexbuf; comment fmt lexbuf } | "<" { fprintf fmt "<"; comment fmt lexbuf } | "&" { fprintf fmt "&"; comment fmt lexbuf } - | "'\"'" + | "'\"'" | _ as s { fprintf fmt "%s" s; comment fmt lexbuf } and string fmt = parse @@ -164,12 +164,12 @@ div.sig_block {margin-left: 2em}"; if not (Sys.file_exists css_fname) then style_css css_fname; Some css_fname end - + let print_header fmt ?(title="") () = fprintf fmt "@\n@\n"; begin match css with | None -> () - | Some f -> fprintf fmt + | Some f -> fprintf fmt "@\n" f end; fprintf fmt "%s@\n" title; @@ -184,7 +184,7 @@ div.sig_block {margin-left: 2em}"; let lb = Lexing.from_channel cin in (* output *) let f = Filename.basename fname in - let base = + let base = match !opt_output with | None -> f | Some dir -> Filename.concat dir f diff --git a/tests/test-pgm-jcf.mlw b/tests/test-pgm-jcf.mlw index 36fd68fe73eadcc5d8aa9104cd9128dd0b4d4b41..acf408b3d048e9db5b5654e3856ea0ed962a12c6 100644 --- a/tests/test-pgm-jcf.mlw +++ b/tests/test-pgm-jcf.mlw @@ -26,8 +26,8 @@ module PoorArrays { 0 <= i < length !a } 'a { result = M.get !a.elts i } val set (a: array 'a) (i: int) (v: 'a) : - { 0 <= i < length !a } - unit writes a + { 0 <= i < length !a } + unit writes a { !a.length = !(old a).length && !a.elts = M.set !(old a).elts i v } end