From d6d849a87ae2e8a19ad84e4444b03e28ab1e99f2 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Tue, 18 May 2021 13:49:24 +0200
Subject: [PATCH] Refactor FP modules using Functors to avoid copy pasting code
---
src_colibri2/bin/dune | 20 +++----
src_colibri2/theories/FP/fp.ml | 81 +++++++++++++--------------
src_colibri2/theories/FP/fp.mli | 3 +-
src_colibri2/theories/FP/fp_value.ml | 37 ++++++++++++
src_colibri2/theories/FP/fp_value.mli | 3 +
5 files changed, 86 insertions(+), 58 deletions(-)
diff --git a/src_colibri2/bin/dune b/src_colibri2/bin/dune
index c79742e17..c476650dd 100644
--- a/src_colibri2/bin/dune
+++ b/src_colibri2/bin/dune
@@ -5,9 +5,9 @@
(flags -linkall)
(libraries
colibri2_main
+ colibri2.theories.fp
colibri2.theories.LRA.stages.stage0)
- (modules colibri2_stage0)
-)
+ (modules colibri2_stage0))
(rule
(target colibri2_stage0.ml)
@@ -18,14 +18,11 @@
(executable
(name colibri2_stage1)
-; (public_name colibri2)
-; (package colibri2)
+ ; (public_name colibri2)
+ ; (package colibri2)
(flags -linkall)
- (libraries
- colibri2_main
- colibri2.theories.LRA.stages.stage1)
- (modules colibri2_stage1)
-)
+ (libraries colibri2_main colibri2.theories.LRA.stages.stage1)
+ (modules colibri2_stage1))
(rule
(target colibri2_stage1.ml)
@@ -53,10 +50,7 @@
colibri2.theories.LRA
colibri2.theories.quantifiers
colibri2.theories.adt)
- (modules
- main options
- )
-)
+ (modules main options))
; Rule to generate a man page for colibrics
diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml
index cd7b0bfe3..5c900f5d4 100644
--- a/src_colibri2/theories/FP/fp.ml
+++ b/src_colibri2/theories/FP/fp.ml
@@ -18,56 +18,51 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Colibri2_popop_lib
-open Popop_stdlib
-
-(*************************************************************************)
-(* Float32 *)
-(*************************************************************************)
+(* 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 [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
-(** 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
+ (** 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)
+ end) *)
-(*************************************************************************)
-(* Float64 *)
-(*************************************************************************)
-
-(** 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 [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
+ (** 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
+ (** 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)
\ No newline at end of file
+ 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.mli b/src_colibri2/theories/FP/fp.mli
index 7cdcd3667..712593b9b 100644
--- a/src_colibri2/theories/FP/fp.mli
+++ b/src_colibri2/theories/FP/fp.mli
@@ -21,6 +21,5 @@
(** FloatingPoint theory as described in SMT-LIB 2 *)
(** TODO : Register the theory *)
-(* val th_register : Egraph.t -> unit *)
+val th_register : Egraph.t -> unit
-module Float32Value : ValueKind.Registered
\ 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 616184a9c..b4717a9fa 100644
--- a/src_colibri2/theories/FP/fp_value.ml
+++ b/src_colibri2/theories/FP/fp_value.ml
@@ -18,3 +18,40 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+open Colibri2_popop_lib
+open Popop_stdlib
+
+module type FloatName = sig val name : string end
+
+(** Extends a module of type [Farith.S] to be of type [ValueKind.Value] *)
+module MakeFloat (F : Farith.S) (N : FloatName) = struct
+
+ (** Extends a module of type [Farith.S] with [hash_fold_t] and [sexp_of_t] *)
+ module HF = struct
+ include F
+ let hash_fold_t s t = Base.Hash.fold_int s (hash t)
+ let sexp_of_t = sexp_of_t_of_pp F.pp
+ end
+
+ include HF
+ module M = Map.Make(HF)
+ module S = Extset.MakeOfMap(M)
+ module H = XHashtbl.Make(HF)
+
+ 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
diff --git a/src_colibri2/theories/FP/fp_value.mli b/src_colibri2/theories/FP/fp_value.mli
index 616184a9c..fd5192597 100644
--- a/src_colibri2/theories/FP/fp_value.mli
+++ b/src_colibri2/theories/FP/fp_value.mli
@@ -18,3 +18,6 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+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
--
GitLab