Skip to content
Snippets Groups Projects
Commit 89a9cbcd authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

Separate float32 & float64 modules

parent d6d849a8
No related branches found
No related tags found
1 merge request!10Feature/fp
Hide whitespace changes
Inline Side-by-side
src_colibri2/theories/FP/float32.ml 0 → 100644
+ 26
− 0
View file @ 89a9cbcd
(*************************************************************************)
(* 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
src_colibri2/theories/FP/float32.mli 0 → 100644
+ 21
− 0
View file @ 89a9cbcd
(*************************************************************************)
(* 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
src_colibri2/theories/FP/float64.ml 0 → 100644
+ 25
− 0
View file @ 89a9cbcd
(*************************************************************************)
(* 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
src_colibri2/theories/FP/float64.mli 0 → 100644
+ 21
− 0
View file @ 89a9cbcd
(*************************************************************************)
(* 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
src_colibri2/theories/FP/fp.ml
+ 0
− 47
View file @ 89a9cbcd
......@@ -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
src_colibri2/theories/FP/fp_value.ml
+ 1
− 15
View file @ 89a9cbcd
......@@ -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
src_colibri2/theories/FP/fp_value.mli
+ 7
− 2
View file @ 89a9cbcd
......@@ -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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment