Make good progress on adding generics to global constants

8 files changed, 172 insertions, 47 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index a93ed6e4..3c5ea15b 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -185,9 +185,17 @@ let extract_adt_g_value
   | _ -> raise (Failure "Inconsistent typed value")
 
 (* Extract globals in the same way as variables *)
-let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
-    (id : A.GlobalDeclId.id) : unit =
-  F.pp_print_string fmt (ctx_get_global id ctx)
+let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+    (id : A.GlobalDeclId.id) (generics : generic_args) : unit =
+  let use_brackets = inside && generics <> empty_generic_args in
+  F.pp_open_hvbox fmt ctx.indent_incr;
+  if use_brackets then F.pp_print_string fmt "(";
+  (* Extract the global name *)
+  F.pp_print_string fmt (ctx_get_global id ctx);
+  (* Extract the generics *)
+  extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
+  if use_brackets then F.pp_print_string fmt ")";
+  F.pp_close_box fmt ()
 
 (* Filter the generics of a function if it is builtin *)
 let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
@@ -321,7 +329,9 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       match qualif.id with
       | FunOrOp fun_id ->
           extract_function_call ctx fmt inside fun_id qualif.generics args
-      | Global global_id -> extract_global ctx fmt global_id
+      | Global global_id ->
+          assert (args = []);
+          extract_global ctx fmt inside global_id qualif.generics
       | AdtCons adt_cons_id ->
           extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args
       | Proj proj ->
@@ -1691,7 +1701,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     of those declarations. See {!extract_global_decl} for more explanations.
  *)
 let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
-    (kind : decl_kind) (name : string) (ty : ty)
+    (kind : decl_kind) (name : string) (generics : generic_params)
+    (type_params : string list) (cg_params : string list)
+    (trait_clauses : string list) (ty : ty)
     (extract_body : (F.formatter -> unit) Option.t) : unit =
   let is_opaque = Option.is_none extract_body in
 
@@ -1708,9 +1720,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_open_hvbox fmt 0;
   F.pp_open_hvbox fmt ctx.indent_incr;
 
-  (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
+  (* Open "QUALIF NAME PARAMS : TYPE =" box (depth=1) *)
   F.pp_open_hovbox fmt ctx.indent_incr;
-  (* Print "QUALIF NAME " *)
+  (* Print "QUALIF NAME PARAMS " *)
   (match fun_decl_kind_to_qualif kind with
   | Some qualif ->
       F.pp_print_string fmt qualif;
@@ -1719,6 +1731,12 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_string fmt name;
   F.pp_print_space fmt ();
 
+  (* Extract the generic parameters *)
+  let space = ref true in
+  extract_generic_params ctx fmt TypeDeclId.Set.empty ~space:(Some space)
+    generics type_params cg_params trait_clauses;
+  if not !space then F.pp_print_space fmt ();
+
   (* Open ": TYPE =" box (depth=2) *)
   F.pp_open_hvbox fmt 0;
   (* Print ": " *)
@@ -1775,7 +1793,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
     but I could not find a better way.
  *)
 let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
-    (name : string) (ty : ty) : unit =
+    (name : string) (generics : generic_params) (ty : ty) : unit =
+  (* TODO: non-empty generics *)
+  assert (generics = empty_generic_params);
   (* Open the definition boxe (depth=0) *)
   F.pp_open_hvbox fmt ctx.indent_incr;
   (* [val ..._def = new_constant ("...",] *)
@@ -1815,58 +1835,92 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
     and {!extract_fun_decl}.
  *)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
+    (global : global_decl) (body : fun_decl) (interface : bool) : unit =
   assert body.is_global_decl_body;
   assert (body.signature.inputs = []);
-  assert (body.signature.generics = empty_generic_params);
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
   let name =
     if !Config.extract_external_name_patterns && not global.is_local then
-      Some global.name
+      Some global.llbc_name
     else None
   in
   extract_comment_with_span ctx fmt
-    [ "[" ^ name_to_string ctx global.name ^ "]" ]
+    [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
     name global.meta.span;
   F.pp_print_space fmt ();
 
   let decl_name = ctx_get_global global.def_id ctx in
   let body_name =
-    ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body), None)) ctx
+    ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body_id), None)) ctx
   in
-
   let decl_ty, body_ty =
     let ty = body.signature.output in
     if body.signature.fwd_info.effect_info.can_fail then
       (unwrap_result_ty ty, ty)
     else (ty, mk_result_ty ty)
   in
+  (* Add the type parameters *)
+  let ctx, type_params, cg_params, trait_clauses =
+    ctx_add_generic_params global.llbc_name global.llbc_generics global.generics
+      ctx
+  in
   match body.body with
   | None ->
       (* No body: only generate a [val x_c : u32] declaration *)
       let kind = if interface then Declared else Assumed in
       if !backend = HOL4 then
-        extract_global_decl_hol4_opaque ctx fmt decl_name decl_ty
-      else extract_global_decl_body_gen ctx fmt kind decl_name decl_ty None
+        extract_global_decl_hol4_opaque ctx fmt decl_name global.generics
+          decl_ty
+      else
+        extract_global_decl_body_gen ctx fmt kind decl_name global.generics
+          type_params cg_params trait_clauses decl_ty None
   | Some body ->
       (* There is a body *)
       (* Generate: [let x_body : result u32 = Return 3] *)
-      extract_global_decl_body_gen ctx fmt SingleNonRec body_name body_ty
+      extract_global_decl_body_gen ctx fmt SingleNonRec body_name
+        global.generics type_params cg_params trait_clauses body_ty
         (Some (fun fmt -> extract_texpression ctx fmt false body.body));
       F.pp_print_break fmt 0 0;
       (* Generate: [let x_c : u32 = eval_global x_body] *)
-      extract_global_decl_body_gen ctx fmt SingleNonRec decl_name decl_ty
+      extract_global_decl_body_gen ctx fmt SingleNonRec decl_name
+        global.generics type_params cg_params trait_clauses decl_ty
         (Some
            (fun fmt ->
-             let body =
+             let all_params = [ type_params; cg_params; trait_clauses ] in
+             let extract_params () =
+               List.iter
+                 (fun p ->
+                   F.pp_print_space fmt ();
+                   F.pp_print_string fmt p)
+                 (List.concat all_params)
+             in
+             let use_brackets = all_params <> [] in
+             (* Extract the name *)
+             let before, after =
                match !backend with
-               | FStar | Lean -> "eval_global " ^ body_name
-               | Coq -> body_name ^ "%global"
-               | HOL4 -> "get_return_value " ^ body_name
+               | FStar | Lean ->
+                   ( (fun () ->
+                       F.pp_print_string fmt "eval_global";
+                       F.pp_print_space fmt ()),
+                     fun () -> () )
+               | Coq ->
+                   ((fun () -> ()), fun () -> F.pp_print_string fmt "%global")
+               | HOL4 ->
+                   ( (fun () ->
+                       F.pp_print_string fmt "get_return_value";
+                       F.pp_print_space fmt ()),
+                     fun () -> () )
              in
-             F.pp_print_string fmt body));
+             before ();
+             if use_brackets then F.pp_print_string fmt "(";
+             F.pp_print_string fmt body_name;
+             (* Extract the generic params *)
+             extract_params ();
+             if use_brackets then F.pp_print_string fmt ")";
+             (* *)
+             after ()));
       (* Add a break to insert lines between declarations *)
       F.pp_print_break fmt 0 0
 
@@ -2592,7 +2646,12 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
         let item_name = ctx_get_trait_const trait_decl_id name ctx in
         let ty () =
           F.pp_print_space fmt ();
-          F.pp_print_string fmt (ctx_get_global id ctx)
+          F.pp_print_string fmt (ctx_get_global id ctx);
+          List.iter
+            (fun p ->
+              F.pp_print_space fmt ();
+              F.pp_print_string fmt p)
+            (List.concat [ type_params; cg_params; trait_clauses ])
         in
 
         extract_trait_impl_item ctx fmt item_name ty)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index eef9e2c9..95a2956b 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -949,9 +949,9 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
     | Assign (p, rvalue) -> (
         (* We handle global assignments separately *)
         match rvalue with
-        | Global gid ->
+        | Global (gid, generics) ->
             (* Evaluate the global *)
-            eval_global config p gid cf ctx
+            eval_global config p gid generics cf ctx
         | _ ->
             (* Evaluate the rvalue *)
             let cf_eval_rvalue = eval_rvalue_not_global config rvalue in
@@ -1021,31 +1021,37 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
   (* Compose and apply *)
   comp cc cf_eval_st cf ctx
 
-and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) :
-    st_cm_fun =
+and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
+    (generics : generic_args) : st_cm_fun =
  fun cf ctx ->
   let global = ctx_lookup_global_decl ctx gid in
   match config.mode with
   | ConcreteMode ->
-      (* Treat the evaluation of the global as a call to the global body (without arguments) *)
-      let func =
-        {
-          func = FunId (FRegular global.body);
-          generics = TypesUtils.empty_generic_args;
-        }
-      in
+      (* Treat the evaluation of the global as a call to the global body *)
+      let func = { func = FunId (FRegular global.body); generics } in
       let call = { func = FnOpRegular func; args = []; dest } in
       (eval_transparent_function_call_concrete config global.body call) cf ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
       assert (ty_no_regions global.ty);
-      let sval = mk_fresh_symbolic_value global.ty in
+      (* Instantiate the type  *)
+      (* There shouldn't be any reference to Self *)
+      let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
+      let generics = Subst.generic_args_erase_regions generics in
+      let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
+        Subst.make_subst_from_generics global.generics generics tr_self
+      in
+      let ty =
+        Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
+          global.ty
+      in
+      let sval = mk_fresh_symbolic_value ty in
       let cc =
         assign_to_place config (mk_typed_value_from_symbolic_value sval) dest
       in
       let e = cc (cf Unit) ctx in
-      S.synthesize_global_eval gid sval e
+      S.synthesize_global_eval gid generics sval e
 
 (** Evaluate a switch *)
 and eval_switch (config : config) (switch : switch) : st_cm_fun =
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index a735667e..cf6710aa 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1087,6 +1087,26 @@ type fun_decl = {
 }
 [@@deriving show]
 
+type global_decl = {
+  meta : meta;
+  def_id : GlobalDeclId.id;
+  is_local : bool;
+  llbc_name : llbc_name;  (** The original LLBC name. *)
+  name : string;
+      (** We use the name only for printing purposes (for debugging):
+          the name used at extraction time will be derived from the
+          llbc_name.
+       *)
+  llbc_generics : Types.generic_params;
+      (** See the comment for [llbc_generics] in fun_decl. *)
+  generics : generic_params;
+  preds : predicates;
+  ty : ty;
+  kind : item_kind;
+  body_id : FunDeclId.id;
+}
+[@@deriving show]
+
 type trait_decl = {
   def_id : trait_decl_id;
   is_local : bool;
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index a989fd3b..fc94fa4c 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -208,7 +208,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
             get_adt_field_types ctx.type_decls adt_id variant_id adt_generics
           in
           List.iter
-            (fun (fid, fe) ->
+            (fun ((fid, fe) : _ * texpression) ->
               let expected_field_ty = FieldId.nth expected_field_tys fid in
               assert (expected_field_ty = fe.ty);
               check_texpression ctx fe)
@@ -218,7 +218,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
             Collections.List.to_cons_nil adt_generics.types
           in
           List.iter
-            (fun (_, fe) ->
+            (fun ((_, fe) : _ * texpression) ->
               assert (expected_field_ty = fe.ty);
               check_texpression ctx fe)
             supd.updates
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 79c03e58..cc74a16b 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -141,7 +141,7 @@ type expression =
           The context is the evaluation context from after evaluating the asserted
           value. It has the same purpose as for the {!Return} case.
        *)
-  | EvalGlobal of global_decl_id * symbolic_value * expression
+  | EvalGlobal of global_decl_id * generic_args * symbolic_value * expression
       (** Evaluate a global to a fresh symbolic value *)
   | Assertion of Contexts.eval_ctx * typed_value * expression
       (** An assertion.
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 27279327..58fb6d04 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1890,7 +1890,8 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   | Panic -> translate_panic ctx
   | FunCall (call, e) -> translate_function_call call e ctx
   | EndAbstraction (ectx, abs, e) -> translate_end_abstraction ectx abs e ctx
-  | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx
+  | EvalGlobal (gid, generics, sv, e) ->
+      translate_global_eval gid generics sv e ctx
   | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx
   | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
   | IntroSymbolic (ectx, p, sv, v, e) ->
@@ -2662,11 +2663,12 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
           (* Create the let-binding *)
           mk_let effect_info.can_fail output call next_e)
 
-and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
-    (e : S.expression) (ctx : bs_ctx) : texpression =
+and translate_global_eval (gid : A.GlobalDeclId.id) (generics : T.generic_args)
+    (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression =
   let ctx, var = fresh_var_for_symbolic_value sval ctx in
   let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in
-  let global_expr = { id = Global gid; generics = empty_generic_args } in
+  let generics = ctx_translate_fwd_generic_args ctx generics in
+  let global_expr = { id = Global gid; generics } in
   (* We use translate_fwd_ty to translate the global type *)
   let ty = ctx_translate_fwd_ty ctx decl.ty in
   let gval = { e = Qualif global_expr; ty } in
@@ -3838,3 +3840,40 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     required_methods;
     provided_methods;
   }
+
+let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
+    global_decl =
+  let {
+    A.meta;
+    def_id;
+    is_local;
+    name = llbc_name;
+    generics = llbc_generics;
+    preds;
+    ty;
+    kind;
+    body = body_id;
+  } =
+    decl
+  in
+  let name =
+    Print.Types.name_to_string
+      (Print.Contexts.decls_ctx_to_fmt_env ctx)
+      llbc_name
+  in
+  let generics = translate_generic_params llbc_generics in
+  let preds = translate_predicates preds in
+  let ty = translate_fwd_ty ctx.type_ctx.type_infos ty in
+  {
+    meta;
+    def_id;
+    is_local;
+    llbc_name;
+    name;
+    llbc_generics;
+    generics;
+    preds;
+    ty;
+    kind;
+    body_id;
+  }
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 20bc107e..a42c43ac 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -119,9 +119,9 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
       FunCall (call, e))
     e
 
-let synthesize_global_eval (gid : GlobalDeclId.id) (dest : symbolic_value)
-    (e : expression option) : expression option =
-  Option.map (fun e -> EvalGlobal (gid, dest, e)) e
+let synthesize_global_eval (gid : GlobalDeclId.id) (generics : generic_args)
+    (dest : symbolic_value) (e : expression option) : expression option =
+  Option.map (fun e -> EvalGlobal (gid, generics, dest, e)) e
 
 let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
     (call_id : FunCallId.id) (ctx : Contexts.eval_ctx) (sg : fun_sig)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index fba1dfb0..9af3c71b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -469,6 +469,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
        groups are always singletons, so the [extract_global_decl] function
        takes care of generating the delimiters.
     *)
+    let global = SymbolicToPure.translate_global ctx.trans_ctx global in
     Extract.extract_global_decl ctx fmt global body config.interface
 
 (** Utility.