diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/PureToExtract.ml | 97 |
1 files changed, 49 insertions, 48 deletions
diff --git a/compiler/PureToExtract.ml b/compiler/PureToExtract.ml index 860949a7..25ad6713 100644 --- a/compiler/PureToExtract.ml +++ b/compiler/PureToExtract.ml @@ -51,7 +51,6 @@ type formatter = { char_name : string; int_name : integer_type -> string; str_name : string; - assert_name : string; field_name : name -> FieldId.id -> string option -> string; (** Inputs: - type name @@ -86,16 +85,12 @@ type formatter = { global_name : global_name -> string; (** Provided a basename, compute a global name. *) fun_name : - A.fun_id -> - fun_name -> - int -> - region_group_info option -> - bool * int -> - string; - (** Inputs: - - function id: this is especially useful to identify whether the - function is an assumed function or a local function - - function basename + fun_name -> int -> region_group_info option -> bool * int -> string; + (** Compute the name of a regular (non-assumed) function. + + Inputs: + - function id + - function basename (TODO: shouldn't appear for assumed functions?...) - number of region groups - region group information in case of a backward function ([None] if forward function) @@ -191,7 +186,7 @@ type formatter = { (** We use identifiers to look for name clashes *) type id = | GlobalId of A.GlobalDeclId.id - | FunId of A.fun_id * RegionGroupId.id option + | FunId of fun_id | DecreasesClauseId of A.fun_id (** The definition which provides the decreases/termination clause. We insert calls to this clause to prove/reason about termination: @@ -290,10 +285,9 @@ let names_map_add_assumed_variant (id_to_string : id -> string) (nm : names_map) : names_map = names_map_add id_to_string (VariantId (Assumed id, variant_id)) name nm -let names_map_add_assumed_function (id_to_string : id -> string) - (fid : A.assumed_fun_id) (rg_id : RegionGroupId.id option) (name : string) - (nm : names_map) : names_map = - names_map_add id_to_string (FunId (A.Assumed fid, rg_id)) name nm +let names_map_add_function (id_to_string : id -> string) (fid : fun_id) + (name : string) (nm : names_map) : names_map = + names_map_add id_to_string (FunId fid) name nm (** Make a (variable) basename unique (by adding an index). @@ -360,25 +354,29 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | GlobalId gid -> let name = (A.GlobalDeclId.Map.find gid global_decls).name in "global name: " ^ Print.global_name_to_string name - | FunId (fid, rg_id) -> - let fun_name = - match fid with - | A.Regular fid -> - Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name - | A.Assumed aid -> A.show_assumed_fun_id aid - in - let fun_kind = - match rg_id with - | None -> "forward" - | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id - in - "fun name (" ^ fun_kind ^ "): " ^ fun_name + | FunId fid -> ( + match fid with + | FromLlbc (fid, rg_id) -> + let fun_name = + match fid with + | Regular fid -> + Print.fun_name_to_string + (A.FunDeclId.Map.find fid fun_decls).name + | Assumed aid -> A.show_assumed_fun_id aid + in + let fun_kind = + match rg_id with + | None -> "forward" + | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id + in + "fun name (" ^ fun_kind ^ "): " ^ fun_name + | Pure fid -> PrintPure.pure_assumed_fun_id_to_string fid) | DecreasesClauseId fid -> let fun_name = match fid with - | A.Regular fid -> + | Regular fid -> Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name - | A.Assumed aid -> A.show_assumed_fun_id aid + | Assumed aid -> A.show_assumed_fun_id aid in "decreases clause for function: " ^ fun_name | TypeId id -> "type name: " ^ get_type_name id @@ -451,13 +449,12 @@ 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) - (ctx : extraction_ctx) : string = - ctx_get (FunId (id, rg)) ctx +let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string = + ctx_get (FunId id) ctx 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 + ctx_get_function (FromLlbc (Regular id, rg)) ctx let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string = assert (id <> Tuple); @@ -488,7 +485,7 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id) let ctx_get_decreases_clause (def_id : A.FunDeclId.id) (ctx : extraction_ctx) : string = - ctx_get (DecreasesClauseId (A.Regular def_id)) ctx + ctx_get (DecreasesClauseId (Regular def_id)) ctx (** Generate a unique type variable name and add it to the context *) let ctx_add_type_var (basename : string) (id : TypeVarId.id) @@ -577,13 +574,13 @@ let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) : let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_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 + ctx_add (DecreasesClauseId (Regular def.def_id)) name 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 - let body = FunId (Regular def.body_id, None) in + let body = FunId (FromLlbc (Regular def.body_id, None)) in let ctx = ctx_add decl (name ^ "_c") ctx in let ctx = ctx_add body (name ^ "_body") ctx in ctx @@ -617,18 +614,19 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in Some { id = rg_id; region_names } in - let def_id = A.Regular def_id in let name = - ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) + ctx.fmt.fun_name def.basename num_rgs rg_info (keep_fwd, num_backs) in - ctx_add (FunId (def_id, def.back_id)) name ctx + ctx_add (FunId (FromLlbc (A.Regular def_id, def.back_id))) name ctx type names_map_init = { keywords : string list; assumed_adts : (assumed_ty * string) list; assumed_structs : (assumed_ty * string) list; assumed_variants : (assumed_ty * VariantId.id * string) list; - assumed_functions : (A.assumed_fun_id * RegionGroupId.id option * string) list; + assumed_llbc_functions : + (A.assumed_fun_id * RegionGroupId.id option * string) list; + assumed_pure_functions : (pure_assumed_fun_id * string) list; } (** Initialize a names map with a proper set of keywords/names coming from the @@ -638,9 +636,7 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map = let keywords = List.concat [ - [ fmt.bool_name; fmt.char_name; fmt.str_name; fmt.assert_name ]; - int_names; - init.keywords; + [ fmt.bool_name; fmt.char_name; fmt.str_name ]; int_names; init.keywords; ] in let names_set = StringSet.of_list keywords in @@ -680,11 +676,16 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map = names_map_add_assumed_variant id_to_string type_id variant_id name nm) nm init.assumed_variants in + let assumed_functions = + List.map + (fun (fid, rg, name) -> (FromLlbc (A.Assumed fid, rg), name)) + init.assumed_llbc_functions + @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions + in let nm = List.fold_left - (fun nm (fun_id, rg_id, name) -> - names_map_add_assumed_function id_to_string fun_id rg_id name nm) - nm init.assumed_functions + (fun nm (fid, name) -> names_map_add_function id_to_string fid name nm) + nm assumed_functions in (* Return *) nm |