diff options
Diffstat (limited to 'src/SymbolicToPure.ml')
-rw-r--r-- | src/SymbolicToPure.ml | 88 |
1 files changed, 1 insertions, 87 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index e4fdebff..14bbc63f 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -15,92 +15,6 @@ module PP = PrintPure (** The local logger *) let log = L.symbolic_to_pure_log -(** TODO: move this, it is not useful for symbolic -> pure *) -type name = - | FunName of A.FunDefId.id * T.RegionVarId.id option - | TypeName of T.TypeDefId.id -[@@deriving show, ord] - -let name_to_string (n : name) : string = show_name n - -module NameOrderedType = struct - type t = name - - let compare = compare_name - - let to_string = name_to_string - - let pp_t = pp_name - - let show_t = show_name -end - -module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType) -(** Notice that we use the *injective* map to map identifiers to names. - - Of course, even if those names (which are string lists) don't collide, - when converting them to strings we can still introduce collisions: we - check that later. - - Note that we use injective maps for sanity: though we write the name - generation with collision in mind, it is always good to have such checks. - *) - -let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) : - Id.name = - let sg = fdef.signature in - (* General function to generate a suffix for a region group - * (i.e., an abstraction)*) - let rg_to_string (rg : T.region_var_group) : string = - (* We are just a little bit smart: - - if there is exactly one region id in the region group and this region - has a name, we use this name - - otherwise, we use the region number (note that region names shouldn't - start with numbers) - *) - match rg.T.regions with - | [ rid ] -> ( - let rvar = T.RegionVarId.nth sg.region_params rid in - match rvar.name with - | None -> T.RegionGroupId.to_string rg.T.id - | Some name -> name) - | _ -> T.RegionGroupId.to_string rg.T.id - in - (* There are several cases: - - this is a forward function: we add "_fwd" - - this is a backward function: - - this function has one backward function: we add "_back" - - this function has several backward function: we add "_back" and an - additional suffix to identify the precise backward function - *) - let suffix = - match bid with - | None -> "_fwd" - | Some bid -> ( - match sg.regions_hierarchy with - | [] -> - failwith "Unreachable" - (* we can't get there if we ask for a back function *) - | [ _ ] -> - (* Exactly one backward function *) - "_back" - | _ -> - (* Several backward functions *) - let rg = T.RegionGroupId.nth sg.regions_hierarchy bid in - "_back" ^ rg_to_string rg) - in - (* Final name *) - let rec add_to_last (n : Id.name) : Id.name = - match n with - | [] -> failwith "Unreachable" - | [ x ] -> [ x ^ suffix ] - | x :: n -> x :: add_to_last n - in - add_to_last fdef.name - -(** Generates a name for a type (simply reuses the name in the definition) *) -let translate_type_name (def : T.type_def) : Id.name = def.T.name - (* TODO: move *) let mk_place_from_var (v : var) : place = { var = v.id; projection = [] } @@ -373,7 +287,7 @@ let translate_type_def_kind (kind : T.type_def_kind) : type_def_kind = let translate_type_def (def : T.type_def) : type_def = (* Translate *) let def_id = def.T.def_id in - let name = translate_type_name def in + let name = def.name in (* Can't translate types with regions for now *) assert (def.region_params = []); let type_params = def.type_params in |