bitwidth added to Domain type

grayswandyr · Apr 29, 2024 · 654ad6f · 654ad6f
1 parent fa75238
commit 654ad6f
Show file tree

Hide file tree

Showing 2 changed files with 39 additions and 19 deletions.
diff --git a/src/Domain.ml b/src/Domain.ml
@@ -15,20 +15,31 @@
 open Containers
 module Map = Name.Map
 
-type t = Relation.t Map.t
+type t = {
+  decl : Relation.t Map.t;
+  bitwidth : int;
+}
 
-let equal dom1 dom2 = Map.equal Relation.equal dom1 dom2
-let empty = Map.empty
-let mem = Map.mem
+let equal dom1 dom2 = (Map.equal Relation.equal dom1.decl dom2.decl) && dom1.bitwidth = dom2.bitwidth
+let empty = {decl = Map.empty; bitwidth = 0;}
 
-let add name rel domain =
-  assert (not @@ Map.mem name domain);
-  Map.add name rel domain
+let mem name dom = Map.mem name dom.decl
 
-let get_exn = Map.find
-let get = Map.get
-let to_list = Map.to_list
-let of_list = Map.of_list
+let add name rel domain =
+  assert (not @@ Map.mem name domain.decl);
+  {
+    decl = Map.add name rel domain.decl;
+    bitwidth = domain.bitwidth;
+  }
+
+let get_exn name domain = Map.find name domain.decl
+let get name domain = Map.get name domain.decl
+let to_list domain= Map.to_list domain.decl
+let of_list bw list= 
+  {
+    decl = Map.of_list list;
+    bitwidth = bw;
+  } 
 
 let univ_atoms domain =
   let open Relation in
@@ -61,15 +72,18 @@ let sup name domain =
   get_exn name domain |> Relation.scope |> Scope.sup
 
 let musts ?(with_univ_and_ident = true) domain =
-  (if with_univ_and_ident then domain
-  else domain |> Map.remove Name.univ |> Map.remove Name.iden)
-  |> Map.map Relation.must |> to_list
+  (if with_univ_and_ident then domain.decl
+  else domain.decl |> Map.remove Name.univ |> Map.remove Name.iden)
+  |> Map.map Relation.must |> Map.to_list
 
-let arities = Fun.(Map.map Relation.arity %> to_list)
+let arities domain = 
+  let arities = Map.map Relation.arity domain.decl in
+  Map.to_list arities
 
 let update_domain_with_instance domain instance =
   let module R = Relation in
   let module I = Instance in
+  let bw = domain.bitwidth in
   let relation_of_instance_item inst_item rel =
     assert (R.is_const rel);
     R.const (R.name rel) (R.arity rel) (Scope.exact inst_item)
@@ -83,19 +97,24 @@ let update_domain_with_instance domain instance =
            instance is in the domain *)
         assert false
   in
-  Map.merge_safe ~f:keep_instance domain (Instance.to_map instance)
+  {
+    decl = Map.merge_safe ~f:keep_instance domain.decl (Instance.to_map instance);
+    bitwidth = bw;
+  }
+
 
 let rename atom_renaming name_renaming domain =
+  let bitwidth = domain.bitwidth in
   to_list domain
   |> List.map (fun (name, rel) ->
          ( List.assoc ~eq:Name.equal name name_renaming,
            Relation.rename atom_renaming name_renaming rel ))
-  |> of_list
+  |> (of_list bitwidth)
 
 module P = Intf.Print.Mixin (struct
   type nonrec t = t
 
-  let pp = pp
+  let pp out {decl; _;}= pp out decl
 end)
 
 include P
diff --git a/src/Domain.mli b/src/Domain.mli
@@ -44,7 +44,8 @@ val univ_atoms : t -> Tuple_set.t
 val to_list : t -> (Name.t * Relation.t) list
 (** Returns the map as an association list *)
 
-val of_list : (Name.t * Relation.t) list -> t
+val of_list : int -> (Name.t * Relation.t) list -> t
+
 val equal : t -> t -> bool
 
 val must : Name.t -> t -> Tuple_set.t