Commit eae547d9 authored by Andrei Paskevich's avatar Andrei Paskevich

stdlib, examples: remove redundant "import"

parent 7b0929a7
......@@ -201,8 +201,8 @@ end
theory TestSemantics
use import SemOp
use import map.Const
use SemOp
use map.Const
function my_sigma : env = Const.const (Vint 0)
constant x : ident
......@@ -358,8 +358,8 @@ end
theory TypingAndSemantics
use import SemOp
use import Typing
use SemOp
use Typing
(*
inductive compatible datatype value =
......@@ -406,8 +406,8 @@ end
theory FreshVariables
use import SemOp
use import list.Append
use SemOp
use list.Append
lemma Cons_append: forall a: 'a, l1 l2: list 'a.
Cons a (l1 ++ l2) = (Cons a l1) ++ l2
......@@ -509,9 +509,9 @@ end
theory HoareLogic
use import Syntax
use import SemOp
use import FreshVariables
use Syntax
use SemOp
use FreshVariables
(* Used by Hoare_logic/seq_rule*)
lemma many_steps_seq:
......@@ -594,10 +594,10 @@ end
theory WP
use import SemOp
use import Typing
use import TypingAndSemantics
use import FreshVariables
use SemOp
use Typing
use TypingAndSemantics
use FreshVariables
function fresh_from (f:fmla) : ident
......
......@@ -20,8 +20,8 @@ end
theory PropositionalCalculus
use import bool.Bool
use import Formula
use bool.Bool
use Formula
type prop_fmla = fmla ident
......@@ -44,7 +44,7 @@ function eval (f:prop_fmla) (v:idmap bool) : bool =
end
use import map.Const
use map.Const
goal Test1 :
let x = mk_ident 0 in
......
......@@ -35,7 +35,7 @@ lemma check_skip:
(* program states *)
use map.Map as IdMap
use import int.Int
use int.Int
type state = IdMap.map ident int
......@@ -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 import map.Const
use map.Const
goal Test13 :
let s = Const.const 0 in
......
......@@ -27,8 +27,8 @@ type fmla =
| Flet ident term fmla
| Fforall ident datatype fmla
use import int.Int
use import bool.Bool
use int.Int
use bool.Bool
type value =
| Vint int
......@@ -261,8 +261,8 @@ end
theory TestSemantics
use import Imp
use import map.Const
use Imp
use map.Const
function my_sigma : env = Const.const (Vint 0)
function my_pi : env = Const.const (Vint 42)
......@@ -302,7 +302,7 @@ end
theory HoareLogic
use import Imp
use Imp
(** Hoare logic rules (partial correctness) *)
......@@ -360,7 +360,7 @@ end
module WP
use import Imp
use Imp
use set.Fset as Set
......@@ -425,7 +425,7 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
eval_fmla sigma' pi' result
}
use import HoareLogic
use HoareLogic
let rec wp (i:stmt) (q:fmla)
ensures { valid_triple result i q }
......
......@@ -27,7 +27,7 @@ end
module AddListRec
use import SumList
use SumList
let rec sum (l: list or_integer_float) : (si: int, sf: real) =
variant { l }
......@@ -56,8 +56,8 @@ end
module AddListImp
use import SumList
use import ref.Ref
use SumList
use ref.Ref
let sum (l: list or_integer_float) : (si: int, sf: real) =
ensures { si = add_int l /\ sf = add_real l }
......
......@@ -27,7 +27,7 @@ end
module AddListRec
use import SumList
use SumList
let rec sum (l: list or_integer_float) : (si: int, sf: real) =
variant { l }
......@@ -58,8 +58,8 @@ end
module AddListImp
use import SumList
use import ref.Ref
use SumList
use ref.Ref
let sum (l: list or_integer_float) : (si: int, sf: real) =
ensures { si = add_int l /\ sf = add_real l }
......
......@@ -13,10 +13,10 @@ Pages: 321 - 322
module Algo63
use import int.Int
use import ref.Refint
use import array.Array
use import array.ArrayPermut
use int.Int
use ref.Refint
use array.Array
use array.ArrayPermut
(* we pass m and n (as ghost arguments) to ensure [permut_sub];
this will help solvers in the proof of partition *)
......
......@@ -13,11 +13,11 @@ Pages: 321 - 322
module Algo64
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArrayPermut
use import array.IntArraySorted
use int.Int
use ref.Ref
use array.Array
use array.ArrayPermut
use array.IntArraySorted
(* Algorithm 63 *)
......
......@@ -13,10 +13,10 @@ Pages: 321 - 322
module Algo65
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArrayPermut
use int.Int
use ref.Ref
use array.Array
use array.ArrayPermut
(* algorithm 63 *)
......
......@@ -8,9 +8,9 @@
module AllDistinct
use import int.Int
use import ref.Ref
use import array.Array
use int.Int
use ref.Ref
use array.Array
exception Duplicate
......
......@@ -2,9 +2,9 @@
module M
use import int.Int
use import ref.Refint
use import array.Array
use int.Int
use ref.Refint
use array.Array
val a : array int
......@@ -98,7 +98,7 @@ main:
module InsertionSortExample
use import ARM
use ARM
(* i = fp-16
j = fp-20
......
......@@ -4,10 +4,10 @@ module Sum
(* computes the sum a[1] + ... + a[n] *)
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArraySum
use int.Int
use ref.Ref
use array.Array
use array.ArraySum
let sum (a: array int) (n: int)
requires { 0 <= n < a.length }
......@@ -32,8 +32,8 @@ module Division
we do not seek for a variant which decreases at each statement, but
only at each execution of the loop body. *)
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
let division (x: int) (y: int) : (q: int, r: int)
requires { 0 <= x /\ 0 < y }
......
......@@ -5,8 +5,8 @@
(** {2 Preliminary definitions} *)
theory SelectionTypes
use import seq.Seq
use import option.Option
use seq.Seq
use option.Option
(** Describe a position in the sequence `left ++ middle ++ right`
(see `rebuild`) *)
......@@ -55,12 +55,12 @@ module AVL
routine (monoid operations, element measure,...) is assumed to
take constant time) *)
use import int.Int
use import bool.Bool
use int.Int
use bool.Bool
use import seq.Seq as S
use import seq.FreeMonoid
use import option.Option
use import ref.Ref
use seq.FreeMonoid
use option.Option
use ref.Ref
use mach.peano.Peano as I
(** The implementation is parameterized by an abstract monoid.
......@@ -495,7 +495,7 @@ module AVL
*)
use import SelectionTypes
use SelectionTypes
(** Parameter: selector type. The elements of that type
are intended to describe the class of splits we wish to find. *)
......@@ -542,7 +542,7 @@ module AVL
forall e. selected sr e /\ rebuild e = rseq ->
selected s (left_extend lseq d e) }
use import ref.Ref
use ref.Ref
(** Create a reference over a dummy split. All the binary-search-based
routines take a ghost reference to explicitly return the existential
......
......@@ -23,7 +23,7 @@ end
(** {2 Abstract monoid with aggregation} *)
module MonoidSum
use import seq.Seq
use seq.Seq
clone import Monoid as M with axiom .
function agg (f:'a -> t) (s:seq 'a) : t
......@@ -38,8 +38,8 @@ end
(** {2 Definition of aggregation (refinement of MonoidSum} *)
module MonoidSumDef
use import seq.Seq
use import seq.FreeMonoid
use seq.Seq
use seq.FreeMonoid
(* TODO: do that refinement correctly ! *)
clone import Monoid as M with axiom .
......
......@@ -38,7 +38,7 @@ end
(** {2 Computable total preorder} *)
module Computable
use import int.Int
use int.Int
clone export TotalFull with axiom .
(** Comparison is computable. *)
......
......@@ -5,12 +5,12 @@
module PQueue
use import int.Int
use import avl.SelectionTypes
use import option.Option
use import ref.Ref
use int.Int
use avl.SelectionTypes
use option.Option
use ref.Ref
use import seq.Seq as S
use import seq.FreeMonoid
use seq.FreeMonoid
use mach.peano.Peano as I
(** {2 Implementation parameters} *)
......@@ -213,7 +213,7 @@ module PQueue
(** Conversion from sequences to bags:
from number of occurences. *)
use import seq.Occ
use seq.Occ
let ghost function to_bag (s:seq 'a) : 'a -> int =
fun x -> occ x s 0 (length s)
......
......@@ -7,13 +7,13 @@ module RAL
(** {2 Instantiation of the AVL tree module} *)
use import int.Int
use int.Int
use import mach.peano.Peano as I
use import seq.Seq
use import seq.FreeMonoid
use import option.Option
use import avl.SelectionTypes
use import ref.Ref
use seq.Seq
use seq.FreeMonoid
use option.Option
use avl.SelectionTypes
use ref.Ref
(** Remaining parameters. A fully concrete implementation would
have to provide an explicit positive integer. *)
......
......@@ -8,11 +8,11 @@
(** {2 Shared base implementation between set and map structures} *)
module MapBase
use import int.Int
use import avl.SelectionTypes
use import option.Option
use import ref.Ref
use import seq.Seq
use int.Int
use avl.SelectionTypes
use option.Option
use ref.Ref
use seq.Seq
use mach.peano.Peano as I
(** {3 Implementation parameters *)
......@@ -502,9 +502,9 @@ end
(** {2 Instantiation of the base to key-value ordered associative tables} *)
module Map
use import int.Int
use import option.Option
use import ref.Ref
use int.Int
use option.Option
use ref.Ref
use mach.peano.Peano as I
val constant balancing : I.t
......@@ -700,9 +700,9 @@ end
(** {2 Instantiation of the base to ordered sets} *)
module Set
use import int.Int
use import option.Option
use import ref.Ref
use int.Int
use option.Option
use ref.Ref
use import mach.peano.Peano as I
(** The balancing level is left abstract. *)
......@@ -899,7 +899,7 @@ end
(** Example instances: integer keys/elements *)
module IMapAndSet
use import int.Int
use int.Int
use mach.peano.Peano as I
scope K type t = int end
......
module Bag
use import int.Int
use int.Int
type bag 'a = 'a -> int
......@@ -21,8 +21,8 @@ end
module BagSpec
use import int.Int
use import Bag
use int.Int
use Bag
type t 'a = private {
mutable size: int;
......@@ -47,9 +47,9 @@ end
module ResizableArraySpec
use import int.Int
use import map.Map
use import map.Const
use int.Int
use map.Map
use map.Const
type rarray 'a = private {
ghost mutable len: int;
......@@ -90,8 +90,8 @@ end
module BagImpl
use import int.Int
use import Bag
use int.Int
use Bag
use import ResizableArraySpec as R
use map.Map as Map
use int.NumOf as NumOf
......@@ -164,7 +164,7 @@ module BagImpl
resize t.data n;
t.size <- n
clone import BagSpec with
clone BagSpec with
type t = t,
val create = create,
val clear = clear,
......@@ -174,9 +174,9 @@ end
module Harness
use import int.Int
use import Bag
use import BagImpl
use int.Int
use Bag
use BagImpl
let test1 () =
let b = create () in
......
......@@ -45,8 +45,8 @@ end
module Puzzle8
use import Roberval
use import array.Array
use Roberval
use array.Array
(** All values in `balls[lo..hi-1]` are equal to `w`, apart from `balls[lb]`
which is smaller. *)
......@@ -97,8 +97,8 @@ end
module Puzzle12
use import Roberval
use import array.Array
use Roberval
use array.Array
(** The index `j` of the intruder, its status `b` (whether it is
lighter or heavier), and the weight `w` of the other balls are
......
......@@ -60,7 +60,7 @@ theory Graph
Two cases depending on l3=[] (and thus u=v) conclude the proof. Qed.
*)
clone import pigeon.ListAndSet with type t = vertex
clone pigeon.ListAndSet with type t = vertex
predicate cyc_decomp (v: vertex) (l: list vertex)
(vi: vertex) (l1 l2 l3: list vertex) =
......@@ -141,11 +141,11 @@ end
module BellmanFord
use import Graph
use Graph
use int.IntInf as D
use import ref.Ref
use ref.Ref
clone impset.Impset as S with type elt = (vertex, vertex)
clone import impmap.ImpmapNoDom with type key = vertex
clone impmap.ImpmapNoDom with type key = vertex