diff options
Diffstat (limited to 'src/PureToExtract.ml')
| -rw-r--r-- | src/PureToExtract.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 55a8853a..195eb879 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -6,7 +6,6 @@ open Pure open TranslateCore -open FunIdentifier module C = Contexts module RegionVarId = T.RegionVarId module F = Format @@ -93,7 +92,7 @@ type formatter = { (`None` if forward function) TODO: use the fun id for the assumed functions. *) - decreases_clause_name : FunDeclId.id -> fun_name -> string; + decreases_clause_name : A.FunDeclId.id -> fun_name -> string; (** Generates the name of the definition used to prove/reason about termination. The generated code uses this clause where needed, but its body must be defined by the user. @@ -357,7 +356,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let fun_name = match fid with | A.Regular fid -> - Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name + 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 = @@ -370,7 +369,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let fun_name = match fid with | A.Regular fid -> - Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name + Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name | A.Assumed aid -> A.show_assumed_fun_id aid in "decreases clause for function: " ^ fun_name @@ -445,7 +444,7 @@ 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 : 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 @@ -476,7 +475,7 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id) (ctx : extraction_ctx) : string = ctx_get (VariantId (def_id, variant_id)) ctx -let ctx_get_decreases_clause (def_id : FunDeclId.id) (ctx : extraction_ctx) : +let ctx_get_decreases_clause (def_id : A.FunDeclId.id) (ctx : extraction_ctx) : string = ctx_get (DecreasesClauseId (A.Regular def_id)) ctx @@ -574,7 +573,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (* Lookup the LLBC def to compute the region group information *) let def_id = def.def_id in let llbc_def = - FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls + A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls in let sg = llbc_def.signature in let num_rgs = List.length sg.regions_hierarchy in |