summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-09-22 18:40:08 +0200
committerSon Ho2022-09-22 18:40:08 +0200
commite1b9c968752946e36aeaed1f01272f8481b1a6f1 (patch)
treee01ff191672761135872c60bfb65500dc5527ea8
parent34fed5feb6b768cdf1489936cc1529898bdcc4e9 (diff)
Make minor cleanup
Diffstat (limited to '')
-rw-r--r--src/PrintPure.ml28
-rw-r--r--src/Pure.ml6
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.