From 40e7df701d246faa453003374206014606ca6b6d Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Thu, 2 Feb 2023 23:36:14 -0800
Subject: WIP

---
 compiler/ExtractBase.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'compiler/ExtractBase.ml')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 77170b5b..98a29daf 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -168,6 +168,7 @@ type formatter = {
     int ->
     region_group_info option ->
     bool * int ->
+    bool ->
     string;
       (** Compute the name of a regular (non-assumed) function.
 
@@ -187,6 +188,7 @@ type formatter = {
               The number of extracted backward functions if not necessarily
               equal to the number of region groups, because we may have
               filtered some of them.
+          - whether there is a body or not (indicates assumed function)
           TODO: use the fun id for the assumed functions.
        *)
   decreases_clause_name :
@@ -774,7 +776,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
   in
   let name =
     ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
-      (keep_fwd, num_backs)
+      (keep_fwd, num_backs) (def.body = None)
   in
   ctx_add
     (FunId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
-- 
cgit v1.2.3