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

WhyML: "use/clone T" imports by default (in absence of "as")

For the previous behaviour (no import), write "use/clone T as T".

This shortens the most used "use/clone import" to simply "use/clone".
parent 585b99a6
......@@ -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
......@@ -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
theory A use B end
theory A use export B end
theory A end
theory B use A use A end
theory B use import A use import A end
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
......@@ -7,7 +7,7 @@ theory A
end
theory B
use A
use A
use A as A
use A as A
end
......@@ -3,5 +3,5 @@ theory A
end
theory B
use A
use A as A
end
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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 }
......
......@@ -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,
......
......@@ -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) =
......
......@@ -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 }
......
......@@ -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.
......
......@@ -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 }
......
......@@ -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
......
......@@ -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
......
......@@ -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
(*********************************************************************)
......
......@@ -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:
*)
......@@ -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
......
theory T
use real.Real
use import real.Real
goal toto: true
end
......@@ -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
......
......@@ -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
module Soundness
use import int.Int
use HighOrd
function f0 (x y z:int) : int = x * y + z
predicate p (f:int -> int) =
......
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
......@@ -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:
......
......@@ -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
......@@ -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
......
......@@ -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.
......
......@@ -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}
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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 }
......
......@@ -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
This diff is collapsed.
......@@ -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