Predicate and function order (#819)

* compute strongly connected components for resource predicate definitions and specification function definitions, and record in global typing context

* ocamlformat

backend/cn/lib/check.ml

@@ -2285,19 +2285,27 @@ let record_and_check_logical_functions funs =
       recursive
   in
   (* Now check all functions in order. *)
-  ListM.iteriM
-    (fun i (name, def) ->
-      debug
-        2
-        (lazy
-          (headline
-             ("checking welltypedness of function"
-              ^ Pp.of_total i n_funs
-              ^ ": "
-              ^ Sym.pp_string name)));
-      let@ def = WellTyped.function_ def in
-      Global.add_logical_function name def)
-    funs
+  let@ () =
+    ListM.iteriM
+      (fun i (name, def) ->
+        debug
+          2
+          (lazy
+            (headline
+               ("checking welltypedness of function"
+                ^ Pp.of_total i n_funs
+                ^ ": "
+                ^ Sym.pp_string name)));
+        let@ def = WellTyped.function_ def in
+        Global.add_logical_function name def)
+      funs
+  in
+  let@ global = get_global () in
+  let@ () =
+    Global.set_logical_function_order
+      (Some (WellTyped.logical_function_order global.logical_functions))
+  in
+  return ()
 
 
 let record_and_check_resource_predicates preds =
@@ -2309,20 +2317,28 @@ let record_and_check_resource_predicates preds =
         Global.add_resource_predicate name simple_def)
       preds
   in
-  ListM.iteriM
-    (fun i (name, def) ->
-      debug
-        2
-        (lazy
-          (headline
-             ("checking welltypedness of resource pred"
-              ^ Pp.of_total i (List.length preds)
-              ^ ": "
-              ^ Sym.pp_string name)));
-      let@ def = WellTyped.predicate def in
-      (* add simplified def to the context *)
-      Global.add_resource_predicate name def)
-    preds
+  let@ () =
+    ListM.iteriM
+      (fun i (name, def) ->
+        debug
+          2
+          (lazy
+            (headline
+               ("checking welltypedness of resource pred"
+                ^ Pp.of_total i (List.length preds)
+                ^ ": "
+                ^ Sym.pp_string name)));
+        let@ def = WellTyped.predicate def in
+        (* add simplified def to the context *)
+        Global.add_resource_predicate name def)
+      preds
+  in
+  let@ global = get_global () in
+  let@ () =
+    Global.set_resource_predicate_order
+      (Some (WellTyped.resource_predicate_order global.resource_predicates))
+  in
+  return ()
 
 
 let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> LC.t list m =

backend/cn/lib/global.ml

@@ -10,7 +10,9 @@ type t =
     datatype_order : Sym.t list list option;
     fun_decls : (Locations.t * AT.ft option * Sctypes.c_concrete_sig) Sym.Map.t;
     resource_predicates : Definition.Predicate.t Sym.Map.t;
+    resource_predicate_order : Sym.t list list option;
     logical_functions : Definition.Function.t Sym.Map.t;
+    logical_function_order : Sym.t list list option;
     lemmata : (Locations.t * AT.lemmat) Sym.Map.t
   }
 
@@ -21,7 +23,9 @@ let empty =
     datatype_order = None;
     fun_decls = Sym.Map.empty;
     resource_predicates = Sym.Map.(empty |> add Alloc.Predicate.sym Definition.alloc);
+    resource_predicate_order = None;
     logical_functions = Sym.Map.empty;
+    logical_function_order = None;
     lemmata = Sym.Map.empty
   }
 

backend/cn/lib/typing.ml

@@ -286,6 +286,26 @@ module Global = struct
   let get_datatype_order () =
     let@ g = get_global () in
     return g.datatype_order
+
+
+  let set_resource_predicate_order resource_predicate_order =
+    let@ g = get_global () in
+    set_global { g with resource_predicate_order }
+
+
+  let get_resource_predicate_order () =
+    let@ g = get_global () in
+    return g.resource_predicate_order
+
+
+  let set_logical_function_order logical_function_order =
+    let@ g = get_global () in
+    set_global { g with logical_function_order }
+
+
+  let get_logical_function_order () =
+    let@ g = get_global () in
+    return g.logical_function_order
 end
 
 (* end: convenient functions for global typing context *)

backend/cn/lib/typing.mli

@@ -128,6 +128,14 @@ module Global : sig
 
   val get_datatype_order : unit -> Sym.t list list option m
 
+  val set_resource_predicate_order : Sym.t list list option -> unit m
+
+  val get_resource_predicate_order : unit -> Sym.t list list option m
+
+  val set_logical_function_order : Sym.t list list option -> unit m
+
+  val get_logical_function_order : unit -> Sym.t list list option m
+
   val add_resource_predicate : Sym.t -> Definition.Predicate.t -> unit m
 
   val add_logical_function : Sym.t -> Definition.Function.t -> unit m

backend/cn/lib/wellTyped.ml

@@ -2288,6 +2288,45 @@ module WRPD = struct
            return (Some clauses)
        in
        return Def.Predicate.{ loc; pointer; iargs; oarg_bt; clauses })
+
+
+  module G = Graph.Persistent.Digraph.Concrete (Sym)
+  module Components = Graph.Components.Make (G)
+
+  let resource_predicate_order predicates =
+    let graph = G.empty in
+    let graph = Sym.Map.fold (fun p _ graph -> G.add_vertex graph p) predicates graph in
+    let graph =
+      Sym.Map.fold
+        (fun p pdef graph ->
+          match pdef.Definition.Predicate.clauses with
+          | None -> graph
+          | Some clauses ->
+            List.fold_left
+              (fun graph clause ->
+                let rec aux graph packing_ft =
+                  let open LogicalArgumentTypes in
+                  match packing_ft with
+                  | Define (_, _, packing_ft) -> aux graph packing_ft
+                  | Resource ((_, (req, _)), _, packing_ft) ->
+                    let graph =
+                      match req with
+                      | P { name = Owned _; _ } | Q { name = Owned _; _ } -> graph
+                      | P { name = PName p'; _ } | Q { name = PName p'; _ } ->
+                        G.add_edge graph p p'
+                    in
+                    aux graph packing_ft
+                  | Constraint (_, _, packing_ft) -> aux graph packing_ft
+                  | I _return_value -> graph
+                in
+                aux graph clause.Definition.Clause.packing_ft)
+              graph
+              clauses)
+        predicates
+        graph
+    in
+    let sccs = Components.scc_list graph in
+    sccs
 end
 
 module WLFD = struct
@@ -2316,6 +2355,31 @@ module WLFD = struct
          | Uninterp -> return Uninterp
        in
        return { loc; args; return_bt; emit_coq; body })
+
+
+  module G = Graph.Persistent.Digraph.Concrete (Sym)
+  module Components = Graph.Components.Make (G)
+
+  let logical_function_order functions =
+    let graph = G.empty in
+    let graph =
+      Sym.Map.fold (fun fname _ graph -> G.add_vertex graph fname) functions graph
+    in
+    let graph =
+      Sym.Map.fold
+        (fun fname fdef graph ->
+          let calls =
+            match fdef.body with
+            | Def body -> IT.preds_of body
+            | Rec_Def body -> IT.preds_of body
+            | Uninterp -> Sym.Set.empty
+          in
+          Sym.Set.fold (fun fname' graph -> G.add_edge graph fname fname') calls graph)
+        functions
+        graph
+    in
+    let sccs = Components.scc_list graph in
+    sccs
 end
 
 module WLemma = struct
@@ -2437,6 +2501,10 @@ let datatype = WDT.welltyped
 
 let datatype_recursion = WDT.check_recursion_ok
 
+let logical_function_order = WLFD.logical_function_order
+
+let resource_predicate_order = WRPD.resource_predicate_order
+
 let lemma = WLemma.welltyped
 
 let function_ = WLFD.welltyped
@@ -2508,6 +2576,10 @@ module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = stru
 
   let datatype_recursion = lift1 datatype_recursion
 
+  let logical_function_order = (* lift1 *) logical_function_order
+
+  let resource_predicate_order = (* lift1 *) resource_predicate_order
+
   let lemma x y z = lift3 lemma x y z
 
   let function_ = lift1 function_

backend/cn/lib/wellTyped_intf.ml

@@ -70,4 +70,8 @@ module type S = sig
   val datatype : 'a * Mucore.datatype -> ('a * Mucore.datatype) t
 
   val datatype_recursion : (Sym.t * Mucore.datatype) list -> Sym.t list list t
+
+  val logical_function_order : Definition.Function.t Sym.Map.t -> Sym.t list list
+
+  val resource_predicate_order : Definition.Predicate.t Sym.Map.t -> Sym.t list list
 end