Refactor FP modules using Functors to avoid copy pasting code

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
 

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)
+   end) *)
\ No newline at end of file
+
+(* let () = Egraph.add_default_theory (fun _ -> ()) *)
+
+let th_register _ = failwith "Unimplemented"
\ No newline at end of file

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

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

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