diff options
Diffstat (limited to 'src/PureToExtract.ml')
-rw-r--r-- | src/PureToExtract.ml | 26 |
1 files changed, 7 insertions, 19 deletions
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index b7d45deb..255d4e1b 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -29,11 +29,8 @@ module StringSet = Collections.MakeSet (Collections.OrderedString) module StringMap = Collections.MakeMap (Collections.OrderedString) type name = Names.name - type type_name = Names.type_name - type global_name = Names.global_name - type fun_name = Names.fun_name (* TODO: this should a module we give to a functor! *) @@ -229,11 +226,8 @@ module IdOrderedType = struct type t = id let compare = compare_id - let to_string = show_id - let pp_t = pp_id - let show_t = show_id end @@ -452,13 +446,11 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string = let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = ctx_get (GlobalId id) ctx -let ctx_get_function (id : A.fun_id) - (rg : RegionGroupId.id option) +let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get (FunId (id, rg)) ctx -let ctx_get_local_function (id : A.FunDeclId.id) - (rg : RegionGroupId.id option) +let ctx_get_local_function (id : A.FunDeclId.id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get_function (A.Regular id) rg ctx @@ -582,7 +574,7 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) : let name = ctx.fmt.decreases_clause_name def.def_id def.basename in ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx -let ctx_add_global_decl_body (def : A.global_decl) (ctx : extraction_ctx) : +let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = let name = ctx.fmt.global_name def.name in let decl = GlobalId def.def_id in @@ -622,9 +614,8 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) in (* Add the function name if it's not a global *) - if def.is_global_body - then ctx - else ctx_add (FunId (def_id, def.back_id)) name ctx + if def.is_global_decl_body then ctx + else ctx_add (FunId (def_id, def.back_id)) name ctx type names_map_init = { keywords : string list; @@ -690,11 +681,8 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = information. TODO: move all those helpers. *) -let default_fun_suffix - (num_region_groups : int) - (rg : region_group_info option) - ((keep_fwd, num_backs) : bool * int) - : string = +let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) + ((keep_fwd, num_backs) : bool * int) : string = (* There are several cases: - [rg] is `Some`: this is a forward function: - we add "_fwd" |