Commit 85005b4f authored by Andrei Paskevich's avatar Andrei Paskevich

stdlib: rename *.why to *.mlw, use "module" instead of "theory"

parent 5841dfd6
......@@ -3,7 +3,7 @@
(** {2 Associativity} *)
theory Assoc
module Assoc
type t
function op t t : t
......@@ -13,7 +13,7 @@ end
(** {2 Commutativity} *)
theory Comm
module Comm
type t
function op t t : t
......@@ -23,7 +23,7 @@ end
(** {2 Associativity and Commutativity} *)
theory AC
module AC
clone export Assoc
clone export Comm with type t = t, function op = op
......@@ -33,7 +33,7 @@ end
(** {2 Monoids} *)
theory Monoid
module Monoid
clone export Assoc
constant unit : t
......@@ -44,7 +44,7 @@ end
(** {2 Commutative Monoids} *)
theory CommutativeMonoid
module CommutativeMonoid
clone export Monoid
clone export Comm with type t = t, function op = op
......@@ -54,7 +54,7 @@ end
(** {2 Groups} *)
theory Group
module Group
clone export Monoid
function inv t : t
......@@ -69,7 +69,7 @@ end
(** {2 Commutative Groups} *)
theory CommutativeGroup
module CommutativeGroup
clone export Group
clone export Comm with type t = t, function op = op
......@@ -79,7 +79,7 @@ end
(** {2 Rings} *)
theory Ring
module Ring
type t
constant zero : t
......@@ -101,7 +101,7 @@ end
(** {2 Commutative Rings} *)
theory CommutativeRing
module CommutativeRing
clone export Ring
clone Comm as MulComm with type t = t, function op = (*)
......@@ -111,7 +111,7 @@ end
(** {2 Commutative Rings with Unit} *)
theory UnitaryCommutativeRing
module UnitaryCommutativeRing
clone export CommutativeRing
constant one : t
......@@ -122,7 +122,7 @@ end
(** {2 Ordered Commutative Rings} *)
theory OrderedUnitaryCommutativeRing
module OrderedUnitaryCommutativeRing
clone export UnitaryCommutativeRing
......@@ -142,7 +142,7 @@ end
(** {2 Field theory} *)
theory Field
module Field
clone export UnitaryCommutativeRing
......@@ -178,7 +178,7 @@ end
(** {2 Ordered Fields} *)
theory OrderedField
module OrderedField
clone export Field
......
(** {1 Multisets (aka bags)} *)
theory Bag
module Bag
use import int.Int
......
(** {1 Polymorphic binary trees with elements at nodes} *)
theory Tree
module Tree
type tree 'a = Empty | Node (tree 'a) 'a (tree 'a)
......@@ -11,7 +11,7 @@ theory Tree
end
theory Size "number of nodes"
module Size "number of nodes"
use import Tree
use import int.Int
......@@ -27,7 +27,7 @@ theory Size "number of nodes"
end
theory Occ "occurrences in a binary tree"
module Occ "occurrences in a binary tree"
use import Tree
use import int.Int
......@@ -45,7 +45,7 @@ theory Occ "occurrences in a binary tree"
end
theory Height "height of a tree"
module Height "height of a tree"
use import Tree
use import int.Int
......@@ -61,7 +61,7 @@ theory Height "height of a tree"
end
theory Inorder "inorder traversal"
module Inorder "inorder traversal"
use import Tree
use import list.List
......@@ -74,7 +74,7 @@ theory Inorder "inorder traversal"
end
theory Preorder "preorder traversal"
module Preorder "preorder traversal"
use import Tree
use import list.List
......@@ -87,7 +87,7 @@ theory Preorder "preorder traversal"
end
theory InorderLength
module InorderLength
use import Tree
use import Size
......@@ -99,7 +99,7 @@ theory InorderLength
end
theory Zipper "Huet's zipper"
module Zipper "Huet's zipper"
use import Tree
......
......@@ -3,7 +3,7 @@
(** {2 Basic theory of Booleans} *)
theory Bool
module Bool
let function andb (x y : bool) : bool =
match x with
......@@ -39,7 +39,7 @@ end
(** {2 Operator if-then-else} *)
theory Ite
module Ite
let function ite (b:bool) (x y : 'a) : 'a =
match b with
......
......@@ -2,7 +2,7 @@
(** {2 Powers of two} *)
theory Pow2int
module Pow2int
use import int.Int
......@@ -101,7 +101,7 @@ end
(** {2 Generic theory of Bit Vectors (arbitrary length)} *)
theory BV_Gen
module BV_Gen
use export bool.Bool
use import int.Int
......@@ -409,7 +409,7 @@ end
(** {2 Bit Vectors of common sizes, 8/16/32/64} *)
theory BV64
module BV64
constant size : int = 64
constant two_power_size : int = 0x1_0000_0000_0000_0000
......@@ -429,7 +429,7 @@ theory BV64
end
theory BV32
module BV32
constant size : int = 32
constant two_power_size : int = 0x1_0000_0000
......@@ -449,7 +449,7 @@ theory BV32
end
theory BV16
module BV16
constant size : int = 16
constant two_power_size : int = 0x1_0000
......@@ -469,7 +469,7 @@ theory BV16
end
theory BV8
module BV8
constant size : int = 8
constant two_power_size : int = 0x1_00
......@@ -491,7 +491,7 @@ end
(** {2 Generic Converter} *)
theory BVConverter_Gen
module BVConverter_Gen
type bigBV
type smallBV
......@@ -516,7 +516,7 @@ end
(** {2 Converters of common size_bvs} *)
theory BVConverter_32_64
module BVConverter_32_64
use BV32
use BV64
......@@ -530,7 +530,7 @@ theory BVConverter_32_64
function to_uint_big = BV64.t'int
end
theory BVConverter_16_64
module BVConverter_16_64
use BV16
use BV64
......@@ -544,7 +544,7 @@ theory BVConverter_16_64
function to_uint_big = BV64.t'int
end
theory BVConverter_8_64
module BVConverter_8_64
use BV8
use BV64
......@@ -558,7 +558,7 @@ theory BVConverter_8_64
function to_uint_big = BV64.t'int
end
theory BVConverter_16_32
module BVConverter_16_32
use BV16
use BV32
......@@ -572,7 +572,7 @@ theory BVConverter_16_32
function to_uint_big = BV32.t'int
end
theory BVConverter_8_32
module BVConverter_8_32
use BV8
use BV32
......@@ -586,7 +586,7 @@ theory BVConverter_8_32
function to_uint_big = BV32.t'int
end
theory BVConverter_8_16
module BVConverter_8_16
use BV8
use BV16
......
......@@ -9,7 +9,7 @@ standard</a>}.
(** {2 Definition of IEEE-754 rounding modes} *)
theory Rounding
module Rounding
type mode = NearestTiesToEven | ToZero | Up | Down | NearestTiesToAway
(** nearest ties to even, to zero, upward, downward, nearest ties to away *)
......@@ -25,7 +25,7 @@ href="http://www.lri.fr/~marche/ayad10ijcar.pdf">[Ayad, Marché, IJCAR,
*)
theory SpecialValues
module SpecialValues
type class = Finite | Infinite | NaN
......@@ -81,7 +81,7 @@ every integer between [0] and [n] are representable.
*)
theory GenFloat
module GenFloat
use import Rounding
use import real.Real
......@@ -155,7 +155,7 @@ A.k.a. binary32 numbers.
*)
theory SingleFormat
module SingleFormat
type single
......@@ -177,7 +177,7 @@ A.k.a. binary64 numbers.
*)
theory DoubleFormat
module DoubleFormat
type double
......@@ -193,7 +193,7 @@ theory DoubleFormat
end
theory GenFloatSpecStrict
module GenFloatSpecStrict
use import Rounding
use import real.Real
......@@ -240,7 +240,7 @@ theory GenFloatSpecStrict
end
theory Single
module Single
use export SingleFormat
......@@ -253,7 +253,7 @@ theory Single
end
theory Double
module Double
use export DoubleFormat
......@@ -273,7 +273,7 @@ This theory extends the generic theory above by adding the special values.
*)
theory GenFloatFull
module GenFloatFull
use import SpecialValues
use import Rounding
......@@ -415,7 +415,7 @@ theory GenFloatFull
end
theory GenFloatSpecFull
module GenFloatSpecFull
use import real.Real
use import real.Square
......@@ -609,7 +609,7 @@ end
(** {2 Full theory of single precision floats} *)
theory SingleFull
module SingleFull
use export SingleFormat
......@@ -625,7 +625,7 @@ end
(** {2 Full theory of double precision floats} *)
theory DoubleFull
module DoubleFull
use export DoubleFormat
......@@ -641,7 +641,7 @@ end
theory GenFloatSpecMultiRounding
module GenFloatSpecMultiRounding
use import Rounding
use import real.Real
......@@ -721,7 +721,7 @@ end
(*** TODO: find constants for type single *)
(***
theory SingleMultiRounding
module SingleMultiRounding
constant min_normalized_single : real =
constant eps_normalized_single : real =
......@@ -740,7 +740,7 @@ end
*)
theory DoubleMultiRounding
module DoubleMultiRounding
use export DoubleFormat
......
theory Injective
module Injective
type a
type v
......@@ -12,7 +12,7 @@ theory Injective
end
theory Surjective
module Surjective
type a
type v
......@@ -24,7 +24,7 @@ theory Surjective
end
theory Bijective
module Bijective
clone export Injective
clone Surjective as S with type v = v, type a = a,
......
(** {1 Graph theory} *)
theory Path
module Path
use import list.List
use import list.Append
......@@ -42,7 +42,7 @@ theory Path
end
theory IntPathWeight
module IntPathWeight
clone export Path
use import int.Int
......@@ -70,7 +70,7 @@ theory IntPathWeight
end
(***
theory SimplePath
module SimplePath
use import list.List
use import list.Mem
......
......@@ -18,7 +18,7 @@
(** {2 Rounding Modes} *)
theory RoundingMode
module RoundingMode
type mode = RNE | RNA | RTP | RTN | RTZ
(** {h <ul>
<li>RNE : Round Nearest ties to Even
......@@ -31,7 +31,7 @@ theory RoundingMode
predicate to_nearest (m:mode) = m = RNE \/ m = RNA
end
theory GenericFloat
module GenericFloat
use import int.Int
use import bv.Pow2int
......@@ -788,7 +788,7 @@ end
(** {2 Conversions to/from bitvectors} *)
theory Float_BV_Converter
module Float_BV_Converter
use bv.BV8
use bv.BV16
use bv.BV32
......@@ -844,7 +844,7 @@ end
(** {2 Standard simple precision floats (32 bits)} *)
theory Float32
module Float32
use int.Int
use import real.Real
......@@ -879,7 +879,7 @@ end
(** {2 Standard double precision floats (64 bits)} *)
theory Float64
module Float64
use int.Int
use import real.Real
......@@ -914,7 +914,7 @@ end
(** {2 Conversions between float formats} *)
theory FloatConverter
module FloatConverter
use Float64
use Float32
......@@ -941,7 +941,7 @@ theory FloatConverter
end
theory Float32_BV_Converter
module Float32_BV_Converter
use import Float32
clone export Float_BV_Converter with
......@@ -955,7 +955,7 @@ theory Float32_BV_Converter
t'real (of_ubv32 m x) = round m (FromInt.from_int (BV32.t'int x))
end
theory Float64_BV_Converter
module Float64_BV_Converter
use import Float64
clone export Float_BV_Converter with
......
......@@ -8,7 +8,7 @@ theories for classical functions.
(** {2 Integers and the basic operators} *)
theory Int
module Int
let constant zero : int = 0
let constant one : int = 1
......@@ -36,7 +36,7 @@ end
(** {2 Absolute Value} *)
theory Abs
module Abs
use import Int
......@@ -54,7 +54,7 @@ end
(** {2 Minimum and Maximum} *)
theory MinMax
module MinMax
use import Int
......@@ -76,7 +76,7 @@ end
(** {2 The Basic Well-Founded Order on Integers} *)
theory Lex2
module Lex2
use import Int
......@@ -97,7 +97,7 @@ rounds up when divisor is negative.
*)
theory EuclideanDivision
module EuclideanDivision
use import Int
use import Abs
......@@ -160,7 +160,7 @@ The particular case of Euclidean division by 2
*)
theory Div2
module Div2
use import Int
......@@ -177,7 +177,7 @@ towards zero, and thus [mod x y] has the same sign as [x].
*)
theory ComputerDivision
module ComputerDivision
use import Int
use import Abs
......@@ -237,7 +237,7 @@ end
(** {2 Generic Exponentiation of something to an integer exponent} *)
theory Exponentiation
module Exponentiation
use import Int
......@@ -288,7 +288,7 @@ end
(** {2 Power of an integer to an integer } *)
theory Power
module Power
use import Int
......@@ -310,7 +310,7 @@ end
(** {2 Number of integers satisfying a given predicate} *)
theory NumOf
module NumOf
use import Int
......@@ -379,7 +379,7 @@ end
(** {2 Sum} *)
theory Sum
module Sum
use import Int
......@@ -427,7 +427,7 @@ end
(** {2 Factorial function} *)
theory Fact
module Fact
use import Int
......@@ -440,7 +440,7 @@ end
(** {2 Generic iteration of a function} *)
theory Iter
module Iter
use import Int
......@@ -458,7 +458,7 @@ end
(** {2 Integers extended with an infinite value} *)
theory IntInf
module IntInf
use import Int
......@@ -506,7 +506,7 @@ integers greater or equal a given bound.
*)
theory SimpleInduction
module SimpleInduction
use import Int
......@@ -520,7 +520,7 @@ theory SimpleInduction
end
theory Induction
module Induction
use import Int
......@@ -539,7 +539,7 @@ theory Induction
end
theory Fibonacci "Fibonacci numbers"
module Fibonacci "Fibonacci numbers"
use import Int
......
......@@ -3,7 +3,7 @@
(** {2 Basic theory of polymorphic lists} *)
theory List
module List
type list 'a = Nil | Cons 'a (list 'a)
......@@ -16,7 +16,7 @@ end
(** {2 Length of a list} *)
theory Length
module Length
use import int.Int
use import List
......@@ -58,7 +58,7 @@ end
(** {2 Membership in a list} *)
theory Mem
module Mem
use import List
predicate mem (x: 'a) (l: list 'a) = match l with
......@@ -68,7 +68,7 @@ theory Mem
end
theory Elements
module Elements
use import List
use import Mem
......@@ -87,7 +87,7 @@ end
(** {2 Nth element of a list} *)
theory Nth
module Nth
use import List
use import option.Option
......@@ -101,7 +101,7 @@ theory Nth
end
theory NthNoOpt
module NthNoOpt
use import List
use import int.Int
......@@ -114,7 +114,7 @@ theory NthNoOpt
end
theory NthLength
module NthLength
use import int.Int
use import option.Option
......@@ -135,7 +135,7 @@ end
(** {2 Head and tail} *)
theory HdTl
module HdTl
use import List
use import option.Option
......@@ -152,7 +152,7 @@ theory HdTl
end
theory HdTlNoOpt
module HdTlNoOpt
use import List
......@@ -168,7 +168,7 @@ end
(** {2 Relation between head, tail, and nth} *)
theory NthHdTl
module NthHdTl
use import int.Int
use import option.Option
......@@ -187,7 +187,7 @@ end
(** {2 Appending two lists} *)
theory Append