diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml new file mode 100644 index 0000000000000000000000000000000000000000..1a67f19be860e062367f74fdec95ef5fea9b27b1 --- /dev/null +++ b/src_colibri2/theories/FP/float32.ml @@ -0,0 +1,26 @@ +(*************************************************************************) +(* This file is part of Colibri2. *) +(* *) +(* Copyright (C) 2014-2021 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It 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. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(*************************************************************************) + +open Fp_value + +module N32 = struct let name = "Float32" end +module Float32 = ValueKind.Register(MakeFloat(Farith.B32)(N32)) + +include Float32 \ No newline at end of file diff --git a/src_colibri2/theories/FP/float32.mli b/src_colibri2/theories/FP/float32.mli new file mode 100644 index 0000000000000000000000000000000000000000..7a8dbf63018eeb5cb1d2f9052306377a402136f9 --- /dev/null +++ b/src_colibri2/theories/FP/float32.mli @@ -0,0 +1,21 @@ +(*************************************************************************) +(* This file is part of Colibri2. *) +(* *) +(* Copyright (C) 2014-2021 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It 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. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(*************************************************************************) + +include ValueKind.Registered with type s = Farith.B32.t diff --git a/src_colibri2/theories/FP/float64.ml b/src_colibri2/theories/FP/float64.ml new file mode 100644 index 0000000000000000000000000000000000000000..59f1f237d82b4f9130f4ba954b2ad836e4bf1e8e --- /dev/null +++ b/src_colibri2/theories/FP/float64.ml @@ -0,0 +1,25 @@ +(*************************************************************************) +(* This file is part of Colibri2. *) +(* *) +(* Copyright (C) 2014-2021 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It 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. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(*************************************************************************) + +open Fp_value +module N64 = struct let name = "Float64" end +module Float64 = ValueKind.Register(MakeFloat(Farith.B64)(N64)) + +include Float64 \ No newline at end of file diff --git a/src_colibri2/theories/FP/float64.mli b/src_colibri2/theories/FP/float64.mli new file mode 100644 index 0000000000000000000000000000000000000000..1411ed432bc1309aa81c2d9c73f7d2204ea1cdd5 --- /dev/null +++ b/src_colibri2/theories/FP/float64.mli @@ -0,0 +1,21 @@ +(*************************************************************************) +(* This file is part of Colibri2. *) +(* *) +(* Copyright (C) 2014-2021 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It 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. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(*************************************************************************) + +include ValueKind.Registered with type s = Farith.B64.t diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml index 5c900f5d42c6ab82a7599304b775069b4d1ddf66..c82fdefc835efbfa7fbcaf9163b98e1fab0c7df0 100644 --- a/src_colibri2/theories/FP/fp.ml +++ b/src_colibri2/theories/FP/fp.ml @@ -18,51 +18,4 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -(* open Colibri2_popop_lib - open Popop_stdlib - - (** Extends [Farith.B32] with [hash_fold_t] and [sexp_of_t] *) - module Float32 = struct - include Farith.B32 - let hash_fold_t s t = Base.Hash.fold_int s (hash t) - let sexp_of_t = sexp_of_t_of_pp Farith.B32.pp - end - - (** Extends [Float32] to be of type [ValueKind.Value] *) - module DFloat32 = struct - include Float32 - module M = Map.Make(Float32) - module S = Extset.MakeOfMap(M) - module H = XHashtbl.Make(Float32) - end - - (** Register Float32 as a new ValueKind *) - module Float32Value = ValueKind.Register(struct - include DFloat32 - let key = ValueKind.create_key (module struct type t = Farith.B32.t let name = "Float32" end) - end) *) - -(* * Extends [Farith.B64] with [hash_fold_t] and [sexp_of_t] - module Float64 = struct - include Farith.B64 - let hash_fold_t s t = Base.Hash.fold_int s (hash t) - let sexp_of_t = sexp_of_t_of_pp Farith.B64.pp - end - - (** Extends [Float64] to be of type [ValueKind.Value] *) - module DFloat64 = struct - include Float64 - module M = Map.Make(Float64) - module S = Extset.MakeOfMap(M) - module H = XHashtbl.Make(Float64) - end - - (** Register Float64 as a new ValueKind *) - module Float64Value = ValueKind.Register(struct - include DFloat64 - let key = ValueKind.create_key (module struct type t = Farith.B64.t let name = "Float64" end) - end) *) - -(* let () = Egraph.add_default_theory (fun _ -> ()) *) - let th_register _ = failwith "Unimplemented" \ No newline at end of file diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml index b4717a9facf6f75ab8b923fa1004eb54b9255574..0b9c719e637b64a4b2b14d5a5667ead352e09504 100644 --- a/src_colibri2/theories/FP/fp_value.ml +++ b/src_colibri2/theories/FP/fp_value.ml @@ -40,18 +40,4 @@ module MakeFloat (F : Farith.S) (N : FloatName) = struct let key = ValueKind.create_key (module struct type t = F.t let name = N.name end) -end - -(*************************************************************************) -(* Float32 *) -(*************************************************************************) - -module N32 = struct let name = "Float32" end -module Float32Value = ValueKind.Register(MakeFloat(Farith.B32)(N32)) - -(*************************************************************************) -(* Float64 *) -(*************************************************************************) - -module N64 = struct let name = "Float64" end -module Float64Value = ValueKind.Register(MakeFloat(Farith.B64)(N64)) \ No newline at end of file +end \ No newline at end of file diff --git a/src_colibri2/theories/FP/fp_value.mli b/src_colibri2/theories/FP/fp_value.mli index fd5192597e75e2ddaf1a6fe567e3e38fa10bddaa..1f075fa6d27b83cd471c7edf45bf6c451ccf19cc 100644 --- a/src_colibri2/theories/FP/fp_value.mli +++ b/src_colibri2/theories/FP/fp_value.mli @@ -18,6 +18,11 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -module Float32Value : ValueKind.Registered with type s = Farith.B32.t +module type FloatName = sig val name : string end -module Float64Value : ValueKind.Registered with type s = Farith.B64.t \ No newline at end of file +(** Extends a module of type [Farith.S] to be of type [ValueKind.Value] *) +module MakeFloat (F : Farith.S) (N : FloatName) : ValueKind.Value with type t = F.t + +(* module Float32Value : ValueKind.Registered with type s = Farith.B32.t + + module Float64Value : ValueKind.Registered with type s = Farith.B64.t *) \ No newline at end of file