Commit 96addbf6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Reduce amount of "use export" in the standard library.

parent 2015eda9
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
module M module M
use import int.Int
use import ref.Refint use import ref.Refint
use import array.Array use import array.Array
......
...@@ -9,6 +9,7 @@ ...@@ -9,6 +9,7 @@
module Roberval module Roberval
use export int.Int
use export ref.Refint use export ref.Refint
type outcome = Left | Equal | Right type outcome = Left | Equal | Right
...@@ -174,4 +175,4 @@ module Puzzle12 ...@@ -174,4 +175,4 @@ module Puzzle12
end end
end end
end end
\ No newline at end of file
...@@ -6,7 +6,10 @@ ...@@ -6,7 +6,10 @@
theory Graph theory Graph
use export list.List
use import list.Append
use export list.Length use export list.Length
use list.Mem
use export int.Int use export int.Int
use export set.Fset use export set.Fset
......
...@@ -6,6 +6,7 @@ ...@@ -6,6 +6,7 @@
module CheckingALargeRoutine module CheckingALargeRoutine
use import int.Int
use import int.Fact use import int.Fact
use import ref.Ref use import ref.Ref
......
...@@ -42,6 +42,7 @@ ...@@ -42,6 +42,7 @@
module Conjugate module Conjugate
use import int.Int
use import ref.Refint use import ref.Refint
use import array.Array use import array.Array
...@@ -137,4 +138,4 @@ end ...@@ -137,4 +138,4 @@ end
B[i] = partc - 1; B[i] = partc - 1;
} }
} }
*) *)
\ No newline at end of file
...@@ -17,7 +17,7 @@ ...@@ -17,7 +17,7 @@
module Spec module Spec
use import int.Int use export int.Int
use export array.Array use export array.Array
use export array.IntArraySorted use export array.IntArraySorted
......
...@@ -3,11 +3,12 @@ ...@@ -3,11 +3,12 @@
module FactRecursive module FactRecursive
use import int.Int
use import int.Fact use import int.Fact
let rec fact_rec (x:int) : int let rec fact_rec (x:int) : int
requires { x >= 0 } requires { x >= 0 }
variant { x } variant { x }
ensures { result = fact x } ensures { result = fact x }
= if x = 0 then 1 else x * fact_rec (x-1) = if x = 0 then 1 else x * fact_rec (x-1)
...@@ -20,6 +21,7 @@ end ...@@ -20,6 +21,7 @@ end
module FactImperative module FactImperative
use import int.Int
use import int.Fact use import int.Fact
use import ref.Ref use import ref.Ref
......
...@@ -240,6 +240,7 @@ end ...@@ -240,6 +240,7 @@ end
module FibonacciLogarithmic module FibonacciLogarithmic
use import int.Int
use import int.Fibonacci use import int.Fibonacci
use import int.EuclideanDivision use import int.EuclideanDivision
use import Mat22 use import Mat22
......
...@@ -7,6 +7,7 @@ ...@@ -7,6 +7,7 @@
module Max module Max
use import int.Int
use import ref.Refint use import ref.Refint
use import array.Array use import array.Array
......
...@@ -7,6 +7,7 @@ ...@@ -7,6 +7,7 @@
module TwoEqualElements module TwoEqualElements
use import int.Int
use import ref.Refint use import ref.Refint
use import array.Array use import array.Array
......
...@@ -129,6 +129,7 @@ module M ...@@ -129,6 +129,7 @@ module M
(** behavior *) (** behavior *)
use import list.List
use import list.Append use import list.Append
use import list.Reverse use import list.Reverse
...@@ -298,6 +299,7 @@ module M2 ...@@ -298,6 +299,7 @@ module M2
(** behavior *) (** behavior *)
use import list.List
use import list.Append use import list.Append
use import list.Reverse use import list.Reverse
......
...@@ -8,9 +8,10 @@ ...@@ -8,9 +8,10 @@
module RandomAccessList module RandomAccessList
use import int.Int use import int.Int
use import option.Option
use import list.List
use import list.Append use import list.Append
use import list.HdTl use import list.HdTl
use import list.Nth
type tree 'a = type tree 'a =
| Leaf 'a | Leaf 'a
......
...@@ -8,6 +8,7 @@ module InsertionSort ...@@ -8,6 +8,7 @@ module InsertionSort
clone relations.TotalPreOrder with type t = elt, predicate rel = le clone relations.TotalPreOrder with type t = elt, predicate rel = le
clone export list.Sorted with type t = elt, predicate le = le clone export list.Sorted with type t = elt, predicate le = le
use import list.List
use import list.Permut use import list.Permut
let rec insert (x: elt) (l: list elt) : list elt let rec insert (x: elt) (l: list elt) : list elt
......
...@@ -33,6 +33,7 @@ end ...@@ -33,6 +33,7 @@ end
(* Naive solution, in O(N^3) *) (* Naive solution, in O(N^3) *)
module Algo1 module Algo1
use import int.Int
use import ref.Refint use import ref.Refint
use import Spec use import Spec
...@@ -70,6 +71,7 @@ end ...@@ -70,6 +71,7 @@ end
module Algo2 module Algo2
use import int.Int
use import ref.Refint use import ref.Refint
use import Spec use import Spec
...@@ -103,6 +105,7 @@ end ...@@ -103,6 +105,7 @@ end
module Algo3 module Algo3
use import int.Int
use import ref.Refint use import ref.Refint
use import int.ComputerDivision use import int.ComputerDivision
use import Spec use import Spec
...@@ -172,6 +175,7 @@ end ...@@ -172,6 +175,7 @@ end
module Algo4 module Algo4
use import int.Int
use import ref.Refint use import ref.Refint
use import Spec use import Spec
......
...@@ -7,6 +7,7 @@ ...@@ -7,6 +7,7 @@
module Elt module Elt
use export int.Int use export int.Int
use export list.List
use export list.Length use export list.Length
use export list.Append use export list.Append
use export list.Permut use export list.Permut
......
...@@ -6,6 +6,7 @@ ...@@ -6,6 +6,7 @@
module MergesortQueue module MergesortQueue
use import int.Int use import int.Int
use import list.List
use import list.Mem use import list.Mem
use import list.Length use import list.Length
use import list.Append use import list.Append
......
...@@ -7,6 +7,7 @@ ...@@ -7,6 +7,7 @@
module Relabel module Relabel
use import list.List
use import list.Mem use import list.Mem
use import list.Append use import list.Append
use import list.Distinct use import list.Distinct
......
...@@ -241,6 +241,7 @@ module Balance ...@@ -241,6 +241,7 @@ module Balance
use import String use import String
use import Rope as R use import Rope as R
use import int.Int
use import int.Fibonacci use import int.Fibonacci
use import int.MinMax use import int.MinMax
use import array.Array use import array.Array
......
...@@ -92,6 +92,7 @@ end ...@@ -92,6 +92,7 @@ end
module MoreHoareLogic module MoreHoareLogic
use import int.Int use import int.Int
use import option.Option
use import ref.Ref use import ref.Ref
use import list.List use import list.List
use import list.HdTl use import list.HdTl
......
...@@ -56,6 +56,7 @@ end ...@@ -56,6 +56,7 @@ end
module SkewHeaps module SkewHeaps
use import int.Int
use import bintree.Tree use import bintree.Tree
use export bintree.Size use export bintree.Size
use export bintree.Occ use export bintree.Occ
......
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
module FindInSortedList module FindInSortedList
use import int.Int use import int.Int
use import list.List
use import list.Mem use import list.Mem
use import list.SortedInt use import list.SortedInt
......
...@@ -51,6 +51,7 @@ end ...@@ -51,6 +51,7 @@ end
module Palindrome module Palindrome
use import int.Int use import int.Int
use import option.Option
use import list.List use import list.List
use import list.Length use import list.Length
use import list.Append use import list.Append
......
...@@ -11,6 +11,7 @@ ...@@ -11,6 +11,7 @@
theory GilbreathCardTrickPure theory GilbreathCardTrickPure
use export int.Int use export int.Int
use import option.Option
use export list.List use export list.List
use export list.Length use export list.Length
use export list.Append use export list.Append
......
...@@ -73,6 +73,8 @@ module Treedel ...@@ -73,6 +73,8 @@ module Treedel
use import Memory use import Memory
use import bintree.Tree use import bintree.Tree
use import bintree.Inorder use import bintree.Inorder
use import list.List
use import list.Append
use import list.Distinct use import list.Distinct
(* there is a binary tree t rooted at p in memory m *) (* there is a binary tree t rooted at p in memory m *)
......
...@@ -9,7 +9,8 @@ ...@@ -9,7 +9,8 @@
module AmortizedQueue module AmortizedQueue
use import int.Int use import int.Int
use export list.ListRich use import option.Option
use import list.ListRich
type queue 'a = { front: list 'a; lenf: int; type queue 'a = { front: list 'a; lenf: int;
rear : list 'a; lenr: int; } rear : list 'a; lenr: int; }
......
...@@ -9,9 +9,10 @@ ...@@ -9,9 +9,10 @@
module SearchingALinkedList module SearchingALinkedList
use import int.Int use import int.Int
use export list.List use import option.Option
use export list.Length use import list.List
use export list.Nth use import list.Length
use import list.Nth
predicate zero_at (l: list int) (i: int) = predicate zero_at (l: list int) (i: int) =
nth i l = Some 0 /\ forall j:int. 0 <= j < i -> nth j l <> Some 0 nth i l = Some 0 /\ forall j:int. 0 <= j < i -> nth j l <> Some 0
......
...@@ -10,6 +10,8 @@ ...@@ -10,6 +10,8 @@
module RingBuffer module RingBuffer
use import int.Int use import int.Int
use import option.Option
use import list.List
use import list.NthLengthAppend as L use import list.NthLengthAppend as L
use import array.Array use import array.Array
......
...@@ -31,7 +31,7 @@ a few operations specific to integer references *) ...@@ -31,7 +31,7 @@ a few operations specific to integer references *)
module Refint module Refint
use export int.Int use import int.Int
use export Ref use export Ref
let incr (r: ref int) ensures { !r = old !r + 1 } = r := !r + 1 let incr (r: ref int) ensures { !r = old !r + 1 } = r := !r + 1
......
...@@ -9,8 +9,8 @@ end ...@@ -9,8 +9,8 @@ end
theory Size "number of nodes" theory Size "number of nodes"
use export Tree use import Tree
use export int.Int use import int.Int
function size (t: tree 'a) : int = match t with function size (t: tree 'a) : int = match t with
| Empty -> 0 | Empty -> 0
...@@ -25,8 +25,8 @@ end ...@@ -25,8 +25,8 @@ end
theory Occ "occurrences in a binary tree" theory Occ "occurrences in a binary tree"
use export Tree use import Tree
use export int.Int use import int.Int
function occ (x: 'a) (t: tree 'a) : int = match t with function occ (x: 'a) (t: tree 'a) : int = match t with
| Empty -> 0 | Empty -> 0
...@@ -43,8 +43,9 @@ end ...@@ -43,8 +43,9 @@ end
theory Inorder "inorder traversal" theory Inorder "inorder traversal"
use export Tree use import Tree
use export list.Append use import list.List
use import list.Append
function inorder (t: tree 'a) : list 'a = match t with function inorder (t: tree 'a) : list 'a = match t with
| Empty -> Nil | Empty -> Nil
...@@ -55,8 +56,9 @@ end ...@@ -55,8 +56,9 @@ end
theory Preorder "preorder traversal" theory Preorder "preorder traversal"
use export Tree use import Tree
use export list.Append use import list.List
use import list.Append
function preorder (t: tree 'a) : list 'a = match t with function preorder (t: tree 'a) : list 'a = match t with
| Empty -> Nil | Empty -> Nil
...@@ -67,8 +69,10 @@ end ...@@ -67,8 +69,10 @@ end
theory InorderLength theory InorderLength
use import Tree
use import Size use import Size
use import Inorder use import Inorder
use import list.List
use import list.Length use import list.Length
lemma inorder_length: forall t: tree 'a. length (inorder t) = size t lemma inorder_length: forall t: tree 'a. length (inorder t) = size t
...@@ -77,7 +81,7 @@ end ...@@ -77,7 +81,7 @@ end
theory Zipper "Huet's zipper" theory Zipper "Huet's zipper"
use export Tree use import Tree
type zipper 'a = type zipper 'a =
| Top | Top
......
...@@ -3,8 +3,8 @@ ...@@ -3,8 +3,8 @@
theory Path theory Path
use export list.List use import list.List
use export list.Append use import list.Append
type vertex type vertex
...@@ -45,7 +45,9 @@ end ...@@ -45,7 +45,9 @@ end
theory IntPathWeight theory IntPathWeight
clone export Path clone export Path
use export int.Int use import int.Int
use import list.List
use import list.Append
function weight vertex vertex : int function weight vertex vertex : int
......
...@@ -350,7 +350,7 @@ end ...@@ -350,7 +350,7 @@ end
theory Fact theory Fact
use export Int use import Int
function fact int : int function fact int : int
...@@ -473,7 +473,7 @@ end ...@@ -473,7 +473,7 @@ end
theory Fibonacci "Fibonacci numbers" theory Fibonacci "Fibonacci numbers"
use export Int use import Int
function fib int : int function fib int : int
......
...@@ -31,7 +31,7 @@ end ...@@ -31,7 +31,7 @@ end
(** {2 Membership in a list} *) (** {2 Membership in a list} *)
theory Mem theory Mem
use export List use import List
predicate mem (x: 'a) (l: list 'a) = match l with predicate mem (x: 'a) (l: list 'a) = match l with
| Nil -> false | Nil -> false
...@@ -61,8 +61,8 @@ end ...@@ -61,8 +61,8 @@ end
theory Nth theory Nth
use export List use import List
use export option.Option use import option.Option
use import int.Int use import int.Int
function nth (n: int) (l: list 'a) : option 'a = match l with function nth (n: int) (l: list 'a) : option 'a = match l with
...@@ -74,7 +74,7 @@ end ...@@ -74,7 +74,7 @@ end
theory NthNoOpt theory NthNoOpt
use export List use import List
use import int.Int use import int.Int
function nth (n: int) (l: list 'a) : 'a function nth (n: int) (l: list 'a) : 'a
...@@ -87,9 +87,11 @@ end ...@@ -87,9 +87,11 @@ end
theory NthLength theory NthLength
use import int.Int
use import option.Option
use import List
use export Nth use export Nth
use export Length use export Length
use import int.Int
lemma nth_none_1: lemma nth_none_1:
forall l: list 'a, i: int. i < 0 -> nth i l = None forall l: list 'a, i: int. i < 0 -> nth i l = None
...@@ -106,8 +108,8 @@ end ...@@ -106,8 +108,8 @@ end
theory HdTl theory HdTl
use export List use import List
use export option.Option use import option.Option
function hd (l: list 'a) : option 'a = match l with function hd (l: list 'a) : option 'a = match l with
| Nil -> None | Nil -> None
...@@ -123,7 +125,7 @@ end ...@@ -123,7 +125,7 @@ end
theory HdTlNoOpt theory HdTlNoOpt
use export List use import List
function hd (l: list 'a) : 'a function hd (l: list 'a) : 'a
...@@ -140,6 +142,8 @@ end ...@@ -140,6 +142,8 @@ end
theory NthHdTl theory NthHdTl
use import int.Int use import int.Int
use import option.Option
use import List
use import Nth use import Nth
use import HdTl use import HdTl
...@@ -155,7 +159,8 @@ end ...@@ -155,7 +159,8 @@ end
(** {2 Appending two lists} *) (** {2 Appending two lists} *)
theory Append theory Append
use export List
use import List
function (++) (l1 l2: list 'a) : list 'a = match l1 with function (++) (l1 l2: list 'a) : list 'a = match l1 with
| Nil -> l2 | Nil -> l2
...@@ -189,9 +194,10 @@ end ...@@ -189,9 +194,10 @@ end
theory NthLengthAppend theory NthLengthAppend
use import int.Int
use import List
use export NthLength use export NthLength
use export Append use export Append
use import int.Int
lemma nth_append_1: lemma nth_append_1:
forall l1 l2: list 'a, i: int. forall l1 l2: list 'a, i: int.
...@@ -207,7 +213,7 @@ end ...@@ -207,7 +213,7 @@ end
theory Reverse theory Reverse
use export List use import List
use import Append use import Append
function reverse (l: list 'a) : list 'a = match l with function reverse (l: list 'a) : list 'a = match l with
...@@ -278,7 +284,7 @@ end ...@@ -278,7 +284,7 @@ end
theory Combine theory Combine
use export List use import List
function combine (x: list 'a) (y: list 'b) : list ('a, 'b) = function com