Merge pull request #509 from Nadrieril/use-crate-in-envs

Author: Nadrieril

charon-ml/src/LlbcAst.ml

@@ -10,4 +10,4 @@ type fun_body = expr_body [@@deriving show]
 type fun_decl = statement gfun_decl [@@deriving show]
 
 (** LLBC crate *)
-type crate = statement gcrate
+type crate = statement gcrate [@@deriving show]

charon-ml/src/NameMatcher.ml

@@ -220,37 +220,12 @@ end
 module VarMap = Collections.MakeMap (VarOrderedType)
 
 (** Context to lookup definitions *)
-type ctx = {
-  type_decls : T.type_decl T.TypeDeclId.Map.t;
-  global_decls : LlbcAst.global_decl T.GlobalDeclId.Map.t;
-  fun_decls : A.fun_decl A.FunDeclId.Map.t;
-  trait_decls : A.trait_decl T.TraitDeclId.Map.t;
-  trait_impls : A.trait_impl T.TraitImplId.Map.t;
-}
+type ctx = { crate : A.crate }
 
 let ctx_to_fmt_env (ctx : ctx) : PrintLlbcAst.fmt_env =
-  {
-    type_decls = ctx.type_decls;
-    fun_decls = ctx.fun_decls;
-    global_decls = ctx.global_decls;
-    trait_decls = ctx.trait_decls;
-    trait_impls = ctx.trait_impls;
-    generics = [];
-    locals = [];
-  }
+  { crate = ctx.crate; generics = []; locals = [] }
 
-let ctx_from_crate (crate : LlbcAst.crate) : ctx =
-  let {
-    LlbcAst.type_decls;
-    fun_decls;
-    global_decls;
-    trait_decls;
-    trait_impls;
-    _;
-  } =
-    crate
-  in
-  { type_decls; global_decls; trait_decls; fun_decls; trait_impls }
+let ctx_from_crate (crate : LlbcAst.crate) : ctx = { crate }
 
 (** Match configuration *)
 type match_config = {
@@ -512,7 +487,7 @@ and match_pattern_with_type_id (ctx : ctx) (c : match_config) (m : maps)
   match id with
   | TAdtId id ->
       (* Lookup the type decl and match the name *)
-      let d = T.TypeDeclId.Map.find id ctx.type_decls in
+      let d = T.TypeDeclId.Map.find id ctx.crate.type_decls in
       match_name_with_generics ctx c ~m pid d.item_meta.name generics
   | TTuple -> false
   | TBuiltin id -> (
@@ -574,10 +549,10 @@ and match_expr_with_ty (ctx : ctx) (c : match_config) (m : maps) (pty : expr)
 and match_expr_with_trait_impl_id (ctx : ctx) (c : match_config) (ptr : expr)
     (impl_id : T.TraitImplId.id) : bool =
   (* Lookup the trait implementation *)
-  let impl = T.TraitImplId.Map.find impl_id ctx.trait_impls in
+  let impl = T.TraitImplId.Map.find impl_id ctx.crate.trait_impls in
   (* Lookup the trait declaration *)
   let d =
-    T.TraitDeclId.Map.find impl.impl_trait.trait_decl_id ctx.trait_decls
+    T.TraitDeclId.Map.find impl.impl_trait.trait_decl_id ctx.crate.trait_decls
   in
   (* Match *)
   match ptr with
@@ -590,7 +565,7 @@ and match_trait_decl_ref (ctx : ctx) (c : match_config) (m : maps)
     (pid : pattern) (tr : T.trait_decl_ref T.region_binder) : bool =
   (* Lookup the trait declaration *)
   let d =
-    T.TraitDeclId.Map.find tr.binder_value.trait_decl_id ctx.trait_decls
+    T.TraitDeclId.Map.find tr.binder_value.trait_decl_id ctx.crate.trait_decls
   in
   (* Push a region group in the map, if necessary - TODO: make this more precise *)
   let m = maps_push_bound_regions_group_if_nonempty m tr.binder_regions in
@@ -680,7 +655,7 @@ and match_expr_with_const_generic (ctx : ctx) (c : match_config) (m : maps)
   | EVar pv, _ -> opt_update_cmap c m pv cg
   | EComp pat, CgGlobal gid ->
       (* Lookup the decl and match the name *)
-      let d = T.GlobalDeclId.Map.find gid ctx.global_decls in
+      let d = T.GlobalDeclId.Map.find gid ctx.crate.global_decls in
       match_name ctx c pat d.item_meta.name
   | _ -> false
 
@@ -733,7 +708,7 @@ let match_fn_ptr (ctx : ctx) (c : match_config) (p : pattern) (func : E.fn_ptr)
           let name = builtin_fun_id_to_string fid in
           match_name_with_generics ctx c p (to_name [ name ]) func.generics)
   | FunId (FRegular fid) ->
-      let d = A.FunDeclId.Map.find fid ctx.fun_decls in
+      let d = A.FunDeclId.Map.find fid ctx.crate.fun_decls in
       (* Match the pattern on the name of the function. *)
       let match_function_name =
         match_name_with_generics ctx c p d.item_meta.name func.generics
@@ -948,7 +923,7 @@ and impl_elem_to_pattern (ctx : ctx) (c : to_pat_config) (impl : T.impl_elem) :
   | ImplElemTy bound_ty ->
       PImpl (ty_to_pattern ctx c bound_ty.binder_params bound_ty.binder_value)
   | ImplElemTrait impl_id ->
-      let impl = T.TraitImplId.Map.find impl_id ctx.trait_impls in
+      let impl = T.TraitImplId.Map.find impl_id ctx.crate.trait_impls in
       PImpl (trait_decl_ref_to_pattern ctx c impl.generics impl.impl_trait)
 
 and trait_decl_ref_to_pattern (ctx : ctx) (c : to_pat_config)
@@ -958,7 +933,7 @@ and trait_decl_ref_to_pattern (ctx : ctx) (c : to_pat_config)
   let { T.trait_decl_id; decl_generics } = tr in
   let generics = generic_args_to_pattern ctx c m decl_generics in
   (* Lookup the declaration *)
-  let d = T.TraitDeclId.Map.find trait_decl_id ctx.trait_decls in
+  let d = T.TraitDeclId.Map.find trait_decl_id ctx.crate.trait_decls in
   EComp
     (name_with_generic_args_to_pattern_aux ctx c d.item_meta.name
        (Some generics))
@@ -971,7 +946,7 @@ and ty_to_pattern_aux (ctx : ctx) (c : to_pat_config) (m : constraints)
       match id with
       | TAdtId id ->
           (* Lookup the declaration *)
-          let d = T.TypeDeclId.Map.find id ctx.type_decls in
+          let d = T.TypeDeclId.Map.find id ctx.crate.type_decls in
           EComp
             (name_with_generic_args_to_pattern_aux ctx c d.item_meta.name
                (Some generics))
@@ -1017,7 +992,7 @@ and trait_ref_item_with_generics_to_pattern (ctx : ctx) (c : to_pat_config)
     let trait_decl_ref = trait_ref.trait_decl_ref in
     let d =
       T.TraitDeclId.Map.find trait_decl_ref.binder_value.trait_decl_id
-        ctx.trait_decls
+        ctx.crate.trait_decls
     in
     (* Push a regions map if necessary - TODO: make this more precise *)
     let m =
@@ -1048,7 +1023,7 @@ and const_generic_to_pattern (ctx : ctx) (c : to_pat_config) (m : constraints)
   | CgVar v -> GExpr (EVar (const_generic_var_to_pattern m v))
   | CgValue v -> GValue (literal_to_pattern c v)
   | CgGlobal gid ->
-      let d = T.GlobalDeclId.Map.find gid ctx.global_decls in
+      let d = T.GlobalDeclId.Map.find gid ctx.crate.global_decls in
       let n = name_to_pattern_aux ctx c d.item_meta.name in
       GExpr (EComp n)
 
@@ -1138,7 +1113,7 @@ let fn_ptr_to_pattern (ctx : ctx) (c : to_pat_config)
             let fid = builtin_fun_id_to_string fid in
             [ PIdent (fid, args) ])
     | FunId (FRegular fid) ->
-        let d = A.FunDeclId.Map.find fid ctx.fun_decls in
+        let d = A.FunDeclId.Map.find fid ctx.crate.fun_decls in
         name_with_generic_args_to_pattern_aux ctx c d.item_meta.name (Some args)
     | TraitMethod (tr, method_name, _) ->
         trait_ref_item_with_generics_to_pattern ctx c m tr method_name

charon-ml/src/PrintLlbcAst.ml

@@ -143,16 +143,8 @@ end
 module Crate = struct
   open Ast
 
-  let crate_to_fmt_env (m : crate) : fmt_env =
-    {
-      type_decls = m.type_decls;
-      fun_decls = m.fun_decls;
-      global_decls = m.global_decls;
-      trait_decls = m.trait_decls;
-      trait_impls = m.trait_impls;
-      generics = [];
-      locals = [];
-    }
+  let crate_to_fmt_env (crate : crate) : fmt_env =
+    { crate; generics = []; locals = [] }
 
   let crate_fun_decl_to_string (m : crate) (d : fun_decl) : string =
     let env = crate_to_fmt_env m in

charon-ml/src/PrintTypes.ml

@@ -177,17 +177,17 @@ let rec type_id_to_string (env : 'a fmt_env) (id : type_id) : string =
 
 and type_decl_id_to_string env def_id =
   (* We don't want the printing functions to crash if the crate is partial *)
-  match TypeDeclId.Map.find_opt def_id env.type_decls with
+  match TypeDeclId.Map.find_opt def_id env.crate.type_decls with
   | None -> type_decl_id_to_pretty_string def_id
   | Some def -> name_to_string env def.item_meta.name
 
 and fun_decl_id_to_string (env : 'a fmt_env) (id : FunDeclId.id) : string =
-  match FunDeclId.Map.find_opt id env.fun_decls with
+  match FunDeclId.Map.find_opt id env.crate.fun_decls with
   | None -> fun_decl_id_to_pretty_string id
   | Some def -> name_to_string env def.item_meta.name
 
 and global_decl_id_to_string env def_id =
-  match GlobalDeclId.Map.find_opt def_id env.global_decls with
+  match GlobalDeclId.Map.find_opt def_id env.crate.global_decls with
   | None -> global_decl_id_to_pretty_string def_id
   | Some def -> name_to_string env def.item_meta.name
 
@@ -198,12 +198,12 @@ and global_decl_ref_to_string (env : 'a fmt_env) (gr : global_decl_ref) : string
   global_id ^ generics
 
 and trait_decl_id_to_string env id =
-  match TraitDeclId.Map.find_opt id env.trait_decls with
+  match TraitDeclId.Map.find_opt id env.crate.trait_decls with
   | None -> trait_decl_id_to_pretty_string id
   | Some def -> name_to_string env def.item_meta.name
 
 and trait_impl_id_to_string env id =
-  match TraitImplId.Map.find_opt id env.trait_impls with
+  match TraitImplId.Map.find_opt id env.crate.trait_impls with
   | None -> trait_impl_id_to_pretty_string id
   | Some def -> name_to_string env def.item_meta.name
 
@@ -321,7 +321,7 @@ and impl_elem_to_string (env : 'a fmt_env) (elem : impl_elem) : string =
       let env = fmt_env_update_generics_and_preds env bound_ty.binder_params in
       ty_to_string env bound_ty.binder_value
   | ImplElemTrait impl_id -> begin
-      match TraitImplId.Map.find_opt impl_id env.trait_impls with
+      match TraitImplId.Map.find_opt impl_id env.crate.trait_impls with
       | None -> trait_impl_id_to_string env impl_id
       | Some impl ->
           (* Locally replace the generics and the predicates *)
@@ -483,7 +483,7 @@ let type_decl_to_string (env : 'a fmt_env) (def : type_decl) : string =
 
 let adt_variant_to_string (env : 'a fmt_env) (def_id : TypeDeclId.id)
     (variant_id : VariantId.id) : string =
-  match TypeDeclId.Map.find_opt def_id env.type_decls with
+  match TypeDeclId.Map.find_opt def_id env.crate.type_decls with
   | None ->
       type_decl_id_to_pretty_string def_id
       ^ "::"
@@ -498,7 +498,7 @@ let adt_variant_to_string (env : 'a fmt_env) (def_id : TypeDeclId.id)
 
 let adt_field_names (env : 'a fmt_env) (def_id : TypeDeclId.id)
     (opt_variant_id : VariantId.id option) : string list option =
-  match TypeDeclId.Map.find_opt def_id env.type_decls with
+  match TypeDeclId.Map.find_opt def_id env.crate.type_decls with
   | None -> None
   | Some def ->
       let fields = type_decl_get_fields def opt_variant_id in
@@ -515,7 +515,7 @@ let adt_field_names (env : 'a fmt_env) (def_id : TypeDeclId.id)
 let adt_field_to_string (env : 'a fmt_env) (def_id : TypeDeclId.id)
     (opt_variant_id : VariantId.id option) (field_id : FieldId.id) :
     string option =
-  match TypeDeclId.Map.find_opt def_id env.type_decls with
+  match TypeDeclId.Map.find_opt def_id env.crate.type_decls with
   | None -> None
   | Some def ->
       let fields = type_decl_get_fields def opt_variant_id in

charon-ml/src/PrintUllbcAst.ml

@@ -111,18 +111,11 @@ end
 module Crate = struct
   open Ast
 
+  let crate_to_fmt_env (crate : crate) : fmt_env =
+    { crate; generics = []; locals = [] }
+
   let crate_to_string (m : crate) : string =
-    let env : fmt_env =
-      {
-        type_decls = m.type_decls;
-        fun_decls = m.fun_decls;
-        global_decls = m.global_decls;
-        trait_decls = m.trait_decls;
-        trait_impls = m.trait_impls;
-        generics = [];
-        locals = [];
-      }
-    in
+    let env : fmt_env = crate_to_fmt_env m in
 
     (* The types *)
     let type_decls =

charon-ml/src/PrintUtils.ml

@@ -14,11 +14,7 @@ let block_id_to_string (id : UllbcAst.BlockId.id) : string =
     (for instance we can't find the type variable for a given index) we print
     the id in raw format. *)
 type 'fun_body fmt_env = {
-  type_decls : type_decl TypeDeclId.Map.t;
-  fun_decls : 'fun_body gfun_decl FunDeclId.Map.t;
-  global_decls : global_decl GlobalDeclId.Map.t;
-  trait_decls : trait_decl TraitDeclId.Map.t;
-  trait_impls : trait_impl TraitImplId.Map.t;
+  crate : 'fun_body gcrate;
   generics : generic_params list;
       (** We have a stack of generic parameters, because we can dive into
           binders (for instance because of the arrow type).

charon-ml/src/UllbcAst.ml

@@ -11,4 +11,4 @@ type fun_body = expr_body [@@deriving show]
 type fun_decl = blocks gfun_decl [@@deriving show]
 
 (** ULLBC crate *)
-type crate = blocks gcrate
+type crate = blocks gcrate [@@deriving show]