From e1b9c968752946e36aeaed1f01272f8481b1a6f1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 22 Sep 2022 18:40:08 +0200
Subject: Make minor cleanup

---
 src/PrintPure.ml | 28 ++++++++--------------------
 src/Pure.ml      |  6 ++++--
 2 files changed, 12 insertions(+), 22 deletions(-)

diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 597330bf..0a7091f0 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -2,16 +2,6 @@
 
 open Pure
 open PureUtils
-module T = Types
-module V = Values
-module E = Expressions
-module A = LlbcAst
-module TypeDeclId = T.TypeDeclId
-module TypeVarId = T.TypeVarId
-module RegionId = T.RegionId
-module VariantId = T.VariantId
-module FieldId = T.FieldId
-module SymbolicValueId = V.SymbolicValueId
 
 type type_formatter = {
   type_var_id_to_string : TypeVarId.id -> string;
@@ -43,8 +33,8 @@ type ast_formatter = {
   adt_field_to_string :
     TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option;
   adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
-  fun_decl_id_to_string : A.FunDeclId.id -> string;
-  global_decl_id_to_string : A.GlobalDeclId.id -> string;
+  fun_decl_id_to_string : FunDeclId.id -> string;
+  global_decl_id_to_string : GlobalDeclId.id -> string;
 }
 
 let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
@@ -86,12 +76,10 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
    functions (there is a difference between the forward/backward functions...)
    while we only need those definitions to lookup proper names for the def ids.
 *)
-let mk_ast_formatter
-    (type_decls : T.type_decl TypeDeclId.Map.t)
-    (fun_decls : A.fun_decl A.FunDeclId.Map.t)
-    (global_decls : A.global_decl A.GlobalDeclId.Map.t)
-    (type_params : type_var list) :
-    ast_formatter =
+let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
+    (fun_decls : A.fun_decl FunDeclId.Map.t)
+    (global_decls : A.global_decl GlobalDeclId.Map.t)
+    (type_params : type_var list) : ast_formatter =
   let type_var_id_to_string vid =
     let var = T.TypeVarId.nth type_params vid in
     type_var_to_string var
@@ -114,11 +102,11 @@ let mk_ast_formatter
     Print.LlbcAst.type_ctx_to_adt_field_to_string_fun type_decls
   in
   let fun_decl_id_to_string def_id =
-    let def = A.FunDeclId.Map.find def_id fun_decls in
+    let def = FunDeclId.Map.find def_id fun_decls in
     fun_name_to_string def.name
   in
   let global_decl_id_to_string def_id =
-    let def = A.GlobalDeclId.Map.find def_id global_decls in
+    let def = GlobalDeclId.Map.find def_id global_decls in
     global_name_to_string def.name
   in
   {
diff --git a/src/Pure.ml b/src/Pure.ml
index ced56c6a..afda2caa 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -10,6 +10,8 @@ module RegionGroupId = T.RegionGroupId
 module VariantId = T.VariantId
 module FieldId = T.FieldId
 module SymbolicValueId = V.SymbolicValueId
+module FunDeclId = A.FunDeclId
+module GlobalDeclId = A.GlobalDeclId
 
 module SynthPhaseId = IdGen ()
 (** We give an identifier to every phase of the synthesis (forward, backward
@@ -302,7 +304,7 @@ type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
 
 type qualif_id =
   | Func of fun_id
-  | Global of A.GlobalDeclId.id
+  | Global of GlobalDeclId.id
   | AdtCons of adt_cons_id  (** A function or ADT constructor identifier *)
   | Proj of projection  (** Field projector *)
 [@@deriving show]
@@ -566,7 +568,7 @@ type fun_body = {
 }
 
 type fun_decl = {
-  def_id : A.FunDeclId.id;
+  def_id : FunDeclId.id;
   back_id : T.RegionGroupId.id option;
   basename : fun_name;
       (** The "base" name of the function.
-- 
cgit v1.2.3