From 74d48c646217cae96e2c85d6890627a58ea5740c Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc-mak@users.noreply.github.com>
Date: Thu, 26 Dec 2024 01:26:10 +0000
Subject: [PATCH] CN: Add Context interface file

---
 backend/cn/lib/context.ml           |   1 -
 backend/cn/lib/context.mli          | 108 ++++++++++++++++++++++++++++
 backend/cn/lib/resourceInference.ml |   2 +-
 backend/cn/lib/solver.mli           |   2 +-
 backend/cn/lib/typing.ml            |   7 +-
 backend/cn/lib/typing.mli           |   2 +-
 6 files changed, 116 insertions(+), 6 deletions(-)
 create mode 100644 backend/cn/lib/context.mli

diff --git a/backend/cn/lib/context.ml b/backend/cn/lib/context.ml
index 3bd243713..474780df5 100644
--- a/backend/cn/lib/context.ml
+++ b/backend/cn/lib/context.ml
@@ -3,7 +3,6 @@ open List
 module BT = BaseTypes
 module Res = Resource
 module LC = LogicalConstraints
-module Loc = Locations
 module IntMap = Map.Make (Int)
 
 type l_info = Locations.t * Pp.document Lazy.t
diff --git a/backend/cn/lib/context.mli b/backend/cn/lib/context.mli
new file mode 100644
index 000000000..872442846
--- /dev/null
+++ b/backend/cn/lib/context.mli
@@ -0,0 +1,108 @@
+type l_info = Locations.t * Pp.document Lazy.t
+
+val pp_l_info : Pp.document -> l_info -> Pp.document
+
+type basetype_or_value =
+  | BaseType of BaseTypes.t
+  | Value of IndexTerms.t
+
+val bt_of : basetype_or_value -> BaseTypes.t
+
+val has_value : basetype_or_value -> bool
+
+type resource_history =
+  { last_written : Locations.t;
+    reason_written : string;
+    last_written_id : int;
+    last_read : Locations.t;
+    last_read_id : int
+  }
+
+type t =
+  { computational : (basetype_or_value * l_info) Sym.Map.t;
+    logical : (basetype_or_value * l_info) Sym.Map.t;
+    resources : (Resource.t * int) list * int;
+    resource_history : resource_history Map.Make(Int).t;
+    constraints : LogicalConstraints.Set.t;
+    global : Global.t;
+    where : Where.t
+  }
+
+val empty : t
+
+val get_rs : t -> Resource.t list
+
+val pp_basetype_or_value : basetype_or_value -> Pp.document
+
+val pp_variable_bindings : (basetype_or_value * 'a) Sym.Map.t -> Pp.document
+
+val pp_constraints : LogicalConstraints.Set.t -> Pp.document
+
+val pp : t -> Pp.document
+
+val bound_a : Sym.t -> t -> bool
+
+val bound_l : Sym.t -> t -> bool
+
+val bound : Sym.t -> t -> bool
+
+val get_a : Sym.t -> t -> basetype_or_value
+
+val get_l : Sym.t -> t -> basetype_or_value
+
+val add_a_binding : Sym.t -> basetype_or_value -> l_info -> t -> t
+
+val add_a : Sym.t -> BaseTypes.t -> l_info -> t -> t
+
+val add_a_value : Sym.t -> IndexTerms.t -> l_info -> t -> t
+
+val add_l_binding : Sym.t -> basetype_or_value -> l_info -> t -> t
+
+val add_l : Sym.t -> BaseTypes.t -> l_info -> t -> t
+
+val add_l_value : Sym.t -> IndexTerms.t -> l_info -> t -> t
+
+val remove_a : Sym.t -> t -> t
+
+val add_c : LogicalConstraints.Set.elt -> t -> t
+
+val modify_where : (Where.t -> Where.t) -> t -> t
+
+val pp_history : resource_history -> Pp.document
+
+val set_map_history : int -> 'a -> 'a Map.Make(Int).t -> 'a Map.Make(Int).t
+
+val set_history : int -> resource_history -> t -> t
+
+val add_r : Locations.t -> Resource.t -> t -> t
+
+val res_map_history : resource_history Map.Make(Int).t -> int -> resource_history
+
+val res_history : t -> int -> resource_history
+
+val res_read
+  :  Locations.t ->
+  int ->
+  int * resource_history Map.Make(Int).t ->
+  int * resource_history Map.Make(Int).t
+
+val res_written
+  :  Locations.t ->
+  int ->
+  string ->
+  int * resource_history Map.Make(Int).t ->
+  int * resource_history Map.Make(Int).t
+
+val clone_history
+  :  int ->
+  int list ->
+  resource_history Map.Make(Int).t ->
+  resource_history Map.Make(Int).t
+
+val json : t -> Yojson.Safe.t
+
+val not_given_to_solver
+  :  t ->
+  LogicalConstraints.t list
+  * (Sym.t * Definition.Function.t) list
+  * (Sym.t * Definition.Predicate.t) list
diff --git a/backend/cn/lib/resourceInference.ml b/backend/cn/lib/resourceInference.ml
index 4d02ef98b..785514c14 100644
--- a/backend/cn/lib/resourceInference.ml
+++ b/backend/cn/lib/resourceInference.ml
@@ -141,7 +141,7 @@ module General = struct
        | `False ->
          let@ model = model () in
          let@ all_cs = get_cs () in
-         let () = assert (not (Context.LC.Set.mem c all_cs)) in
+         let () = assert (not (LC.Set.mem c all_cs)) in
          debug_constraint_failure_diagnostics 6 model simp_ctxt c;
          let@ () = Diagnostics.investigate model c in
          fail (fun ctxt ->
diff --git a/backend/cn/lib/solver.mli b/backend/cn/lib/solver.mli
index 45f907469..6a3fdf06b 100644
--- a/backend/cn/lib/solver.mli
+++ b/backend/cn/lib/solver.mli
@@ -41,7 +41,7 @@ val provable
   :  loc:Locations.t ->
   solver:solver ->
   global:Global.t ->
-  assumptions:Context.LC.Set.t ->
+  assumptions:LogicalConstraints.Set.t ->
   simp_ctxt:Simplify.simp_ctxt ->
   LogicalConstraints.t ->
   [> `True | `False ]
diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml
index df9cd162a..b61011e04 100644
--- a/backend/cn/lib/typing.ml
+++ b/backend/cn/lib/typing.ml
@@ -1,7 +1,10 @@
-open Context
+module BT = BaseTypes
+module Res = Resource
+module Req = Request
+module LC = LogicalConstraints
+module Loc = Locations
 module IT = IndexTerms
 module ITSet = Set.Make (IT)
-open TypeErrors
 
 type solver = Solver.solver
 
diff --git a/backend/cn/lib/typing.mli b/backend/cn/lib/typing.mli
index b46997b96..409aea56c 100644
--- a/backend/cn/lib/typing.mli
+++ b/backend/cn/lib/typing.mli
@@ -34,7 +34,7 @@ val print_with_ctxt : (Context.t -> unit) -> unit m
 
 val get_global : unit -> Global.t m
 
-val get_cs : unit -> Context.LC.Set.t m
+val get_cs : unit -> LogicalConstraints.Set.t m
 
 val simp_ctxt : unit -> Simplify.simp_ctxt m