CN: Tidy resource types

backend/cn/lib/argumentTypes.ml

@@ -2,9 +2,8 @@ open Locations
 module BT = BaseTypes
 module IT = IndexTerms
 module LS = LogicalSorts
-module RET = ResourceTypes
+module Req = Request
 module LC = LogicalConstraints
-module SymSet = Set.Make (Sym)
 module LAT = LogicalArgumentTypes
 
 type 'i t =
@@ -29,7 +28,7 @@ and alpha_rename i_subst s t =
 
 
 and suitably_alpha_rename i_subst syms s t =
-  if SymSet.mem s syms then
+  if Sym.Set.mem s syms then
     alpha_rename i_subst s t
   else
     (s, t)
@@ -82,7 +81,7 @@ let alpha_unique ss =
     match at with
     | Computational ((name, bt), info, t) ->
       let name, t = rename_if ss name t in
-      let t = f (SymSet.add name ss) t in
+      let t = f (Sym.Set.add name ss) t in
       Computational ((name, bt), info, t)
     | L t -> L (LAT.alpha_unique ss t)
   in

backend/cn/lib/cLogicalFuns.ml

@@ -3,8 +3,6 @@ open Typing
 
 open Effectful.Make (Typing)
 
-module SymMap = Map.Make (Sym)
-module SymSet = Set.Make (Sym)
 module StringMap = Map.Make (String)
 module IntMap = Map.Make (Int)
 module CF = Cerb_frontend
@@ -47,7 +45,7 @@ type state =
 type context =
   { label_defs : (Sym.t, unit Mu.label_def) Pmap.map;
     (* map from c functions to logical functions which we are building *)
-    c_fun_pred_map : (Locations.t * Sym.t) SymMap.t;
+    c_fun_pred_map : (Locations.t * Sym.t) Sym.Map.t;
     call_funinfo : (Sym.t, Sctypes.c_concrete_sig) Pmap.map
   }
 
@@ -131,7 +129,7 @@ let rec is_const_num = function
 let rec add_pattern p v var_map =
   let (Mu.Pattern (loc, _, _, pattern)) = p in
   match pattern with
-  | CaseBase (Some s, _) -> return (SymMap.add s v var_map)
+  | CaseBase (Some s, _) -> return (Sym.Map.add s v var_map)
   | CaseBase (None, _) -> return var_map
   | CaseCtor (Ctuple, ps) ->
     let@ vs =
@@ -245,7 +243,7 @@ let rec symb_exec_pexpr ctxt var_map pexpr =
   in
   match pe with
   | PEsym sym ->
-    (match SymMap.find_opt sym var_map with
+    (match Sym.Map.find_opt sym var_map with
      | Some r -> return r
      | _ -> fail_n { loc; msg = Unknown_variable sym })
   | PEval v ->
@@ -541,8 +539,8 @@ let rec symb_exec_expr ctxt state_vars expr =
       | None -> fail_fun_it "not a constant function address"
       | Some (nm, _) -> return nm
     in
-    if SymMap.mem nm ctxt.c_fun_pred_map then (
-      let loc, l_sym = SymMap.find nm ctxt.c_fun_pred_map in
+    if Sym.Map.mem nm ctxt.c_fun_pred_map then (
+      let loc, l_sym = Sym.Map.find nm ctxt.c_fun_pred_map in
       let@ def = get_logical_function_def loc l_sym in
       rcval (IT.apply_ l_sym args_its def.LogicalFunctions.return_bt loc) state)
     else (
@@ -578,7 +576,7 @@ let rec filter_syms ss p =
   let (Mu.Pattern (a, b, c, pat)) = p in
   let mk pat = Mu.Pattern (a, b, c, pat) in
   match pat with
-  | CaseBase (Some s, bt) -> if SymSet.mem s ss then p else mk (CaseBase (None, bt))
+  | CaseBase (Some s, bt) -> if Sym.Set.mem s ss then p else mk (CaseBase (None, bt))
   | CaseBase (None, _) -> p
   | CaseCtor (Ctuple, ps) ->
     let ps = List.map (filter_syms ss) ps in
@@ -645,7 +643,7 @@ let c_fun_to_it id_loc glob_context (id : Sym.t) fsym def (fn : 'bty Mu.fun_map_
       match (args_and_body, def_args) with
       | Mu.Computational ((s, bt), _, args_and_body), v :: def_args ->
         if BT.equal bt (IT.bt v) then
-          mk_var_map (SymMap.add s v acc) args_and_body def_args
+          mk_var_map (Sym.Map.add s v acc) args_and_body def_args
         else
           fail_n
             { loc;
@@ -676,7 +674,7 @@ let c_fun_to_it id_loc glob_context (id : Sym.t) fsym def (fn : 'bty Mu.fun_map_
           (fun () -> in_computational_ctxt args_and_body m)
       | L _ -> m
     in
-    let@ arg_map, (body, labels, rt) = mk_var_map SymMap.empty args_and_body def_args in
+    let@ arg_map, (body, labels, rt) = mk_var_map Sym.Map.empty args_and_body def_args in
     let@ () =
       match rt with
       | ReturnTypes.Computational ((_, bt), _, _) ->
@@ -729,8 +727,8 @@ let upd_def (loc, sym, def_tm) =
 let add_logical_funs_from_c call_funinfo funs_to_convert funs =
   let c_fun_pred_map =
     List.fold_left
-      (fun m Mu.{ c_fun_sym; loc; l_fun_sym } -> SymMap.add c_fun_sym (loc, l_fun_sym) m)
-      SymMap.empty
+      (fun m Mu.{ c_fun_sym; loc; l_fun_sym } -> Sym.Map.add c_fun_sym (loc, l_fun_sym) m)
+      Sym.Map.empty
       funs_to_convert
   in
   let global_context =

backend/cn/lib/check.ml

@@ -6,8 +6,6 @@ module RT = ReturnTypes
 module AT = ArgumentTypes
 module LAT = LogicalArgumentTypes
 module IdSet = Set.Make (Id)
-module SymSet = Set.Make (Sym)
-module SymMap = Map.Make (Sym)
 module Loc = Locations
 module RI = ResourceInference
 open IT
@@ -339,7 +337,7 @@ let check_single_ct loc expr =
 let is_fun_addr global t =
   match IT.is_sym t with
   | Some (s, _) ->
-    if SymMap.mem s global.Global.fun_decls then
+    if Sym.Map.mem s global.Global.fun_decls then
       Some s
     else
       None
@@ -353,7 +351,7 @@ let known_function_pointer loc p =
     match already_known with
     | Some _ -> (* no need to find more eqs *) return ()
     | None ->
-      let global_funs = SymMap.bindings global.Global.fun_decls in
+      let global_funs = Sym.Map.bindings global.Global.fun_decls in
       let fun_addrs =
         List.map (fun (sym, (loc, _, _)) -> IT.sym_ (sym, BT.(Loc ()), loc)) global_funs
       in
@@ -1192,7 +1190,7 @@ let _check_used_distinct loc used =
   ListM.iterM check_rd (List.concat (List.map fst used))
 
 
-(*type labels = (AT.lt * label_kind) SymMap.t*)
+(*type labels = (AT.lt * label_kind) Sym.Map.t*)
 
 let load loc pointer ct =
   let@ value =
@@ -1218,7 +1216,7 @@ let instantiate loc filter arg =
   let extra_assumptions1 =
     List.filter_map
       (function LC.Forall ((s, bt), t) when filter t -> Some ((s, bt), t) | _ -> None)
-      (ResourceTypes.LCSet.elements constraints)
+      (LC.Set.elements constraints)
   in
   let extra_assumptions2, type_mismatch =
     List.partition (fun ((_, bt), _) -> BT.equal bt (IT.bt arg_it)) extra_assumptions1
@@ -1273,7 +1271,7 @@ let add_trace_information _labels annots =
   return ()
 
 
-let bytes_qpred sym size pointer init : RET.qpredicate_type =
+let bytes_qpred sym size pointer init : Req.QPredicate.t =
   let here = Locations.other __FUNCTION__ in
   let bt' = WellTyped.quantifier_bt in
   { q = (sym, bt');
@@ -1302,7 +1300,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
         debug 3 (lazy (item "expr" (group (Pp_mucore.pp_expr e))));
         debug 3 (lazy (item "ctxt" (Context.pp ctxt))))
     in
-    let bytes_qpred sym ct pointer init : RET.qpredicate_type =
+    let bytes_qpred sym ct pointer init : Req.QPredicate.t =
       let here = Locations.other __FUNCTION__ in
       bytes_qpred sym (sizeOf_ ct here) pointer init
     in
@@ -1631,7 +1629,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
               else
                 return ()
             in
-            let@ () = add_r loc (P (RET.make_alloc ret), O lookup) in
+            let@ () = add_r loc (P (Req.make_alloc ret), O lookup) in
             let@ () = record_action (Create ret, loc) in
             k ret)
         | CreateReadOnly (_sym1, _ct, _sym2, _prefix) ->
@@ -1650,7 +1648,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
                 ({ name = Owned (ct, Uninit); pointer = arg; iargs = [] }, None)
             in
             let@ _ =
-              RI.Special.predicate_request loc (Access Kill) (RET.make_alloc arg, None)
+              RI.Special.predicate_request loc (Access Kill) (Req.make_alloc arg, None)
             in
             let@ () = record_action (Kill arg, loc) in
             k (unit_ loc))
@@ -1807,7 +1805,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
        in
        aux es [] []
      | CN_progs (_, cn_progs) ->
-       let bytes_pred ct pointer init : RET.predicate_type =
+       let bytes_pred ct pointer init : Req.Predicate.t =
          { name = Owned (ct, init); pointer; iargs = [] }
        in
        let bytes_constraints ~(value : IT.t) ~(byte_arr : IT.t) (ct : Sctypes.t) =
@@ -1921,16 +1919,16 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
                fail (fun _ -> { loc; msg = Generic !^msg })
              | E_Pred (CN_owned (Some ct)) ->
                let@ () = WellTyped.WCT.is_ct loc ct in
-               return (ResourceTypes.Owned (ct, Init))
+               return (Request.Owned (ct, Init))
              | E_Pred (CN_block None) ->
                let msg = "'extract' requires a C-type annotation for 'Block'" in
                fail (fun _ -> { loc; msg = Generic !^msg })
              | E_Pred (CN_block (Some ct)) ->
                let@ () = WellTyped.WCT.is_ct loc ct in
-               return (ResourceTypes.Owned (ct, Uninit))
+               return (Request.Owned (ct, Uninit))
              | E_Pred (CN_named pn) ->
                let@ _ = get_resource_predicate_def loc pn in
-               return (ResourceTypes.PName pn)
+               return (Request.PName pn)
            in
            let@ it = WellTyped.WIT.infer it in
            let@ original_rs, _ = all_resources_tagged loc in
@@ -2064,7 +2062,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
      | Erun (label_sym, pes) ->
        let@ () = ensure_base_type loc ~expect Unit in
        let@ lt, lkind =
-         match SymMap.find_opt label_sym labels with
+         match Sym.Map.find_opt label_sym labels with
          | None ->
            fail (fun _ ->
              { loc; msg = Generic (!^"undefined code label" ^/^ Sym.pp label_sym) })
@@ -2175,7 +2173,7 @@ let check_procedure
                   bind_arguments loc label_args_and_body
                 in
                 let@ () = add_rs loc label_resources in
-                let _, label_kind, loc = SymMap.find lsym label_context in
+                let _, label_kind, loc = Sym.Map.find lsym label_context in
                 let@ () =
                   modify_where Where.(set_section (Label { loc; label = label_kind }))
                 in
@@ -2384,27 +2382,27 @@ let c_function_name ((fsym, (_loc, _args_and_body)) : c_function) : string =
 
 (** Filter functions according to [skip_and_only]: first according to "only",
     then according to "skip" *)
-let select_functions (fsyms : SymSet.t) : SymSet.t =
+let select_functions (fsyms : Sym.Set.t) : Sym.Set.t =
   let matches_str s fsym = String.equal s (Sym.pp_string fsym) in
   let str_fsyms s =
-    let ss = SymSet.filter (matches_str s) fsyms in
-    if SymSet.is_empty ss then (
+    let ss = Sym.Set.filter (matches_str s) fsyms in
+    if Sym.Set.is_empty ss then (
       Pp.warn_noloc (!^"function" ^^^ !^s ^^^ !^"not found");
-      SymSet.empty)
+      Sym.Set.empty)
     else
       ss
   in
   let strs_fsyms ss =
-    ss |> List.map str_fsyms |> List.fold_left SymSet.union SymSet.empty
+    ss |> List.map str_fsyms |> List.fold_left Sym.Set.union Sym.Set.empty
   in
   let skip = strs_fsyms (fst !skip_and_only) in
   let only = strs_fsyms (snd !skip_and_only) in
   let only_funs =
     match snd !skip_and_only with
     | [] -> fsyms
-    | _ss -> SymSet.filter (fun fsym -> SymSet.mem fsym only) fsyms
+    | _ss -> Sym.Set.filter (fun fsym -> Sym.Set.mem fsym only) fsyms
   in
-  SymSet.filter (fun fsym -> not (SymSet.mem fsym skip)) only_funs
+  Sym.Set.filter (fun fsym -> not (Sym.Set.mem fsym skip)) only_funs
 
 
 (** Check a single C function. Failure of the check is encoded monadically. *)
@@ -2467,9 +2465,9 @@ let check_c_functions_all (funs : c_function list) : (string * TypeErrors.t) lis
     with the name of the function in which they occurred. When [fail_fast] is
     set, the first error encountered will halt checking. *)
 let check_c_functions (funs : c_function list) : (string * TypeErrors.t) list m =
-  let selected_fsyms = select_functions (SymSet.of_list (List.map fst funs)) in
+  let selected_fsyms = select_functions (Sym.Set.of_list (List.map fst funs)) in
   let selected_funs =
-    List.filter (fun (fsym, _) -> SymSet.mem fsym selected_fsyms) funs
+    List.filter (fun (fsym, _) -> Sym.Set.mem fsym selected_fsyms) funs
   in
   match !fail_fast with
   | true ->
@@ -2541,8 +2539,8 @@ let memcpy_proxy_ft =
   let map_bt = BT.Map (q_bt, uchar_bt) in
   let destIn_sym, _ = IT.fresh_named map_bt "destIn" here in
   let srcIn_sym, srcIn = IT.fresh_named map_bt "srcIn" here in
-  let destRes str init = RET.Q (bytes_qpred (Sym.fresh_named str) n dest init) in
-  let srcRes str = RET.Q (bytes_qpred (Sym.fresh_named str) n src Init) in
+  let destRes str init = Req.Q (bytes_qpred (Sym.fresh_named str) n dest init) in
+  let srcRes str = Req.Q (bytes_qpred (Sym.fresh_named str) n src Init) in
   (* ensures *)
   let ret_sym, ret = IT.fresh_named (BT.Loc ()) "return" here in
   let destOut_sym, destOut = IT.fresh_named map_bt "destOut" here in
@@ -2647,7 +2645,7 @@ let check_decls_lemmata_fun_specs (file : unit Mu.file) =
   let@ () = record_globals file.globs in
   let@ () = register_fun_syms file in
   let@ () =
-    ListM.iterM (add_stdlib_spec file.call_funinfo) (SymSet.elements file.stdlib_syms)
+    ListM.iterM (add_stdlib_spec file.call_funinfo) (Sym.Set.elements file.stdlib_syms)
   in
   Pp.debug 3 (lazy (Pp.headline "added top-level types and constants."));
   let@ () = record_and_check_logical_functions file.logical_predicates in

backend/cn/lib/cn_internal_to_ail.ml

@@ -2567,7 +2567,7 @@ let cn_to_ail_resource_internal
   _loc
   =
   let calculate_return_type = function
-    | ResourceTypes.Owned (sct, _) ->
+    | Request.Owned (sct, _) ->
       ( Sctypes.to_ctype sct,
         BT.of_sct Memory.is_signed_integer_type Memory.size_of_integer_type sct )
     | PName pname ->
@@ -2590,7 +2590,7 @@ let cn_to_ail_resource_internal
   in
   (* let make_deref_expr_ e_ = A.(AilEunary (Indirection, mk_expr e_)) in *)
   function
-  | ResourceTypes.P p ->
+  | Request.P p ->
     let ctype, bt = calculate_return_type p.name in
     let b, s, e = cn_to_ail_expr_internal dts globals p.pointer PassBack in
     let enum_str = if is_pre then "GET" else "PUT" in
@@ -2639,7 +2639,7 @@ let cn_to_ail_resource_internal
       | _ -> A.(AilSdeclaration [ (sym, Some rhs) ])
     in
     (b @ bs, s @ ss @ [ s_decl ])
-  | ResourceTypes.Q q ->
+  | Request.Q q ->
     (*
        Input is expr of the form:
       take sym = each (integer q.q; q.permission){ Owned(q.pointer + (q.q * q.step)) }
@@ -3339,7 +3339,7 @@ let rec cn_to_ail_lat_internal_2
         else
           (loc, s) :: remove_duplicates (loc :: locs) ss
     in
-    (* let substitution : IT.t Subst.t = {replace = [(Sym.fresh_pretty "return", IT.(IT (Sym (Sym.fresh_pretty "__cn_ret"), BT.Unit)))]; relevant = SymSet.empty} in *)
+    (* let substitution : IT.t Subst.t = {replace = [(Sym.fresh_pretty "return", IT.(IT (Sym (Sym.fresh_pretty "__cn_ret"), BT.Unit)))]; relevant = Sym.Set.empty} in *)
     (* let post_with_ret = RT.subst substitution post in *)
     let return_cn_binding, return_cn_decl =
       match rm_ctype c_return_type with
@@ -3535,7 +3535,7 @@ let cn_to_ail_assume_resource_internal
   loc
   =
   let calculate_return_type = function
-    | ResourceTypes.Owned (sct, _) ->
+    | Request.Owned (sct, _) ->
       ( Sctypes.to_ctype sct,
         BT.of_sct Memory.is_signed_integer_type Memory.size_of_integer_type sct )
     | PName pname ->
@@ -3558,7 +3558,7 @@ let cn_to_ail_assume_resource_internal
   in
   (* let make_deref_expr_ e_ = A.(AilEunary (Indirection, mk_expr e_)) in *)
   function
-  | ResourceTypes.P p ->
+  | Request.P p ->
     let ctype, bt = calculate_return_type p.name in
     let b, s, e = cn_to_ail_expr_internal dts globals p.pointer PassBack in
     let rhs, bs, ss, _owned_ctype =
@@ -3611,7 +3611,7 @@ let cn_to_ail_assume_resource_internal
       | _ -> A.(AilSdeclaration [ (sym, Some rhs) ])
     in
     (b @ bs, s @ ss @ [ s_decl ])
-  | ResourceTypes.Q q ->
+  | Request.Q q ->
     (*
        Input is expr of the form:
         take sym = each (integer q.q; q.permission){ Owned(q.pointer + (q.q * q.step)) }