[Array] Added Array_dom and used it for map rules

colibri2/core/colibri2_core.mli

@@ -756,10 +756,7 @@ module Datastructure : sig
     type key
 
     val create :
-      'a Format.printer ->
-      string ->
-      (Context.creator -> 'b Egraph.t -> key -> 'a) ->
-      ('a, 'b) t
+      'a Format.printer -> string -> ('b Egraph.t -> key -> 'a) -> ('a, 'b) t
 
     val find : ('a, 'b) t -> 'b Egraph.t -> key -> 'a
     val iter : (key -> 'a -> unit) -> ('a, 'b) t -> 'b Egraph.t -> unit

colibri2/core/datastructure.ml

@@ -210,7 +210,7 @@ module type Memo2 =  sig
   type ('a, 'b) t
   type key
 
-  val create: 'a Format.printer -> string -> (Context.creator -> 'b Egraph.t -> key -> 'a) -> ('a, 'b) t
+  val create: 'a Format.printer -> string -> ('b Egraph.t -> key -> 'a) -> ('a, 'b) t
   val find : ('a, 'b) t -> 'b Egraph.t -> key -> 'a
   val iter : (key -> 'a -> unit) -> ('a, 'b) t -> 'b Egraph.t -> unit
   val fold : (key -> 'a -> 'acc -> 'acc) -> ('a, 'b) t -> 'b Egraph.t -> 'acc -> 'acc
@@ -220,12 +220,12 @@ module Memo2(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo2 with type key :
 
   type ('a, 'b) t' = {
     h: 'a S.H.t;
-    def: (Context.creator -> 'b Egraph.t -> S.t -> 'a);
+    def: ('b Egraph.t -> S.t -> 'a);
   }
 
   type ('a, 'b) t = ('a, 'b) t' Env.Unsaved.t
 
-  let create : type a b. a Colibri2_popop_lib.Pp.pp -> _ -> (Context.creator  -> b Egraph.t -> S.t -> a) -> (a, b) t = fun pp name def ->
+  let create : type a b. a Colibri2_popop_lib.Pp.pp -> _ -> (b Egraph.t -> S.t -> a) -> (a, b) t = fun pp name def ->
     let module M = struct
       type t = (a, b) t'
       let name = name end
@@ -242,7 +242,7 @@ module Memo2(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo2 with type key :
     match S.H.find_opt h.h k with
       | Some r -> r
       | None ->
-        let r = h.def (Egraph.context d) d k in
+        let r = h.def d k in
         S.H.add h.h k r;
         r
 

colibri2/core/datastructure.mli

@@ -72,7 +72,7 @@ module type Memo2 =  sig
   type ('a, 'b) t
   type key
 
-  val create: 'a Format.printer -> string -> (Context.creator -> 'b Egraph.t -> key -> 'a) -> ('a, 'b) t
+  val create: 'a Format.printer -> string -> ('b Egraph.t -> key -> 'a) -> ('a, 'b) t
   val find : ('a, 'b) t -> 'b Egraph.t -> key -> 'a
   val iter : (key -> 'a -> unit) -> ('a, 'b) t -> 'b Egraph.t -> unit
   val fold : (key -> 'a -> 'acc -> 'acc) -> ('a, 'b) t -> 'b Egraph.t -> 'acc -> 'acc

colibri2/theories/array/array_dom.ml

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  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 Colibri2_core
+open Colibri2_popop_lib
+open Popop_stdlib
+
+type map_info = {
+  bi_ind_ty : Ground.Ty.t;
+  bi_val_ty : Ground.Ty.t;
+  a_val_ty : Ground.Ty.t;
+  f_arity : DInt.t;
+}
+[@@deriving eq, ord, hash, show]
+
+module AVal = struct
+  module T = struct
+    type t = {
+      reads : Node.S.t; (* read indexes *)
+      map_parents : map_info Ground.M.t; (* parents that are maps *)
+    }
+    [@@deriving eq, ord, hash, show]
+  end
+
+  include T
+  include MkDatatype (T)
+
+  let name = "Array.dom.value"
+end
+
+module D = struct
+  module Value = Value.Register (AVal)
+
+  type t = AVal.t = { reads : Node.S.t; map_parents : map_info Ground.M.t }
+  [@@deriving eq, show]
+
+  let is_singleton _ _ = None
+
+  let key =
+    Dom.Kind.create
+      (module struct
+        type nonrec t = t
+
+        let name = "Array.dom"
+      end)
+
+  let inter _ { reads = r1; map_parents = mp1 }
+      { reads = r2; map_parents = mp2 } =
+    Some
+      { reads = Node.S.union r1 r2; map_parents = Ground.M.set_union mp1 mp2 }
+end
+
+include D
+include Dom.Lattice (D)
+
+let add_read
+    ?(hook : Egraph.wt -> Node.t -> map_info Ground.M.t -> unit =
+      fun _ _ _ -> ()) env n r =
+  match Egraph.get_dom env key n with
+  | Some { reads; map_parents } ->
+      hook env n map_parents;
+      set_dom env n { reads = Node.S.add r reads; map_parents }
+  | None ->
+      set_dom env n { reads = Node.S.singleton r; map_parents = Ground.M.empty }
+
+let add_map_parent
+    ?(hook : Egraph.wt -> Ground.t -> Node.S.t -> map_info -> unit =
+      fun _ _ _ _ -> ()) env n gt { bi_ind_ty; bi_val_ty; a_val_ty; f_arity } =
+  match Egraph.get_dom env key n with
+  | Some { reads; map_parents } ->
+      hook env gt reads { bi_ind_ty; bi_val_ty; a_val_ty; f_arity };
+      set_dom env n
+        {
+          reads;
+          map_parents =
+            Ground.M.add gt
+              { bi_ind_ty; bi_val_ty; a_val_ty; f_arity }
+              map_parents;
+        }
+  | None ->
+      set_dom env n
+        {
+          reads = Node.S.empty;
+          map_parents =
+            Ground.M.singleton gt { bi_ind_ty; bi_val_ty; a_val_ty; f_arity };
+        }

colibri2/theories/array/array_dom.mli

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  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).           *)
+(*************************************************************************)
+
+type map_info = {
+  bi_ind_ty : Ground.Ty.t;
+  bi_val_ty : Ground.Ty.t;
+  a_val_ty : Ground.Ty.t;
+  f_arity : int;
+}
+
+type t = { reads : Node.S.t; map_parents : map_info Ground.M.t }
+
+val equal : t -> t -> bool
+val pp : Format.formatter -> t -> unit
+val show : t -> string
+val is_singleton : 'a -> 'b -> 'c option
+val key : t Dom.Kind.t
+val inter : 'a -> t -> t -> t option
+val set_dom : Egraph.wt -> Node.t -> t -> unit
+val upd_dom : Egraph.wt -> Node.t -> t -> unit
+
+val add_read :
+  ?hook:(Egraph.wt -> Node.t -> map_info Ground.M.t -> unit) ->
+  Egraph.wt ->
+  Node.t ->
+  Node.t ->
+  unit
+
+val add_map_parent :
+  ?hook:(Egraph.wt -> Ground.t -> Node.S.t -> map_info -> unit) ->
+  Egraph.wt ->
+  Node.t ->
+  Ground.t ->
+  map_info ->
+  unit

colibri2/theories/array/foreign_dom.ml

@@ -27,7 +27,7 @@ module FVal = struct
   module T = struct
     type t = IsForeign [@@deriving eq, ord, hash]
 
-    let pp fmt = function IsForeign -> Fmt.pf fmt "IsForeign"
+    let pp fmt IsForeign = Fmt.pf fmt "IsForeign"
   end
 
   include T
@@ -62,13 +62,13 @@ let new_foreign_array_hooks :
     (Ground.Ty.t -> Node.t -> unit) Datastructure.Push.t =
   Datastructure.Push.create Fmt.nop "Array.new_foreign_array"
 
-let register_hook_new_foreign_array d (f : Ground.Ty.t -> Node.t -> unit) =
-  Datastructure.Push.push new_foreign_array_hooks d f
+let register_hook_new_foreign_array env (f : Ground.Ty.t -> Node.t -> unit) =
+  Datastructure.Push.push new_foreign_array_hooks env f
 
-let set_dom_apply_hooks env ty n d =
+let set_dom env ty n d =
   set_dom env n d;
   Datastructure.Push.iter ~f:(fun f -> f ty n) new_foreign_array_hooks env
 
-let upd_dom_apply_hooks env ty n d =
+let upd_dom env ty n d =
   upd_dom env n d;
   Datastructure.Push.iter ~f:(fun f -> f ty n) new_foreign_array_hooks env

colibri2/theories/array/foreign_dom.mli

@@ -26,11 +26,9 @@ val is_singleton : Egraph.wt -> t -> Colibri2_core.Value.t option
 val key : t Dom.Kind.t
 val inter : Egraph.wt -> t -> t -> t option
 val pp : t Fmt.t
-val set_dom : Egraph.wt -> Node.t -> t -> unit
-val upd_dom : Egraph.wt -> Node.t -> t -> unit
 
 val register_hook_new_foreign_array :
   Egraph.wt -> (Ground.Ty.t -> Node.t -> unit) -> unit
 
-val set_dom_apply_hooks : Egraph.wt -> Ground.Ty.t -> Node.t -> t -> unit
-val upd_dom_apply_hooks : Egraph.wt -> Ground.Ty.t -> Node.t -> t -> unit
+val set_dom : Egraph.wt -> Ground.Ty.t -> Node.t -> t -> unit
+val upd_dom : Egraph.wt -> Ground.Ty.t -> Node.t -> t -> unit