diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/PrintPure.ml | 28 | ||||
| -rw-r--r-- | 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. |