Merge pull request #91 from AeneasVerif/son/hax

Prepare the merge in hax

compiler/AssociatedTypes.ml

@@ -51,9 +51,10 @@ let compute_norm_trait_types_from_preds
        that it would be enough to only visit the field [ty] of the trait type
        constraint, but for safety we visit all the fields *)
     assert (trait_type_constraint_no_regions c);
-    let trait_ty = TTraitType (c.trait_ref, c.generics, c.type_name) in
+    let { trait_ref; type_name; ty } : trait_type_constraint = c in
+    let trait_ty = TTraitType (trait_ref, type_name) in
     let trait_ty_ref = get_ref trait_ty in
-    let ty_ref = get_ref c.ty in
+    let ty_ref = get_ref ty in
     let new_repr = UnionFind.get ty_ref in
     let merged = UnionFind.union trait_ty_ref ty_ref in
     (* Not sure the set operation is necessary, but I want to control which
@@ -72,9 +73,7 @@ let compute_norm_trait_types_from_preds
     List.filter_map
       (fun (k, v) ->
         match k with
-        | TTraitType (trait_ref, generics, type_name) ->
-            assert (generics = empty_generic_args);
-            Some ({ trait_ref; type_name }, v)
+        | TTraitType (trait_ref, type_name) -> Some ({ trait_ref; type_name }, v)
         | _ -> None)
       rbindings
   in
@@ -225,20 +224,15 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
       let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in
       let output = norm_ctx_normalize_ty ctx output in
       TArrow (regions, inputs, output)
-  | TTraitType (trait_ref, generics, type_name) -> (
+  | TTraitType (trait_ref, type_name) -> (
       log#ldebug
         (lazy
           ("norm_ctx_normalize_ty:\n- trait type: " ^ ty_to_string ctx ty
          ^ "\n- trait_ref: "
           ^ trait_ref_to_string ctx trait_ref
-          ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref
-          ^ "\n- generics:\n"
-          ^ generic_args_to_string ctx generics));
+          ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref));
       (* Normalize and attempt to project the type from the trait ref *)
       let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in
-      let generics = norm_ctx_normalize_generic_args ctx generics in
-      (*  For now, we don't support higher order types *)
-      assert (generics = empty_generic_args);
       let ty : ty =
         match trait_ref.trait_id with
         | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ }
@@ -284,7 +278,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
                 ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref));
             (* We can't project *)
             assert (trait_instance_id_is_local_clause trait_ref.trait_id);
-            TTraitType (trait_ref, generics, type_name)
+            TTraitType (trait_ref, type_name)
       in
       let tr : trait_type_ref = { trait_ref; type_name } in
       (* Lookup the representative, if there is *)
@@ -484,11 +478,10 @@ and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx)
 
 let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx)
     (ttc : trait_type_constraint) : trait_type_constraint =
-  let { trait_ref; generics; type_name; ty } = ttc in
+  let { trait_ref; type_name; ty } : trait_type_constraint = ttc in
   let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in
-  let generics = norm_ctx_normalize_generic_args ctx generics in
   let ty = norm_ctx_normalize_ty ctx ty in
-  { trait_ref; generics; type_name; ty }
+  { trait_ref; type_name; ty }
 
 let mk_norm_ctx (ctx : eval_ctx) : norm_ctx =
   {

compiler/Extract.ml

@@ -326,19 +326,15 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
           extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args
       | Proj proj ->
           extract_field_projector ctx fmt inside app proj qualif.generics args
-      | TraitConst (trait_ref, generics, const_name) ->
-          let use_brackets = generics <> empty_generic_args in
-          if use_brackets then F.pp_print_string fmt "(";
+      | TraitConst (trait_ref, const_name) ->
           extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref;
-          extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
           let name =
             ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id
               const_name ctx
           in
           let add_brackets (s : string) =
             if !backend = Coq then "(" ^ s ^ ")" else s
           in
-          if use_brackets then F.pp_print_string fmt ")";
           F.pp_print_string fmt ("." ^ add_brackets name))
   | _ ->
       (* "Regular" expression *)

compiler/ExtractBase.ml

@@ -1682,7 +1682,7 @@ let ctx_compute_var_basename (ctx : extraction_ctx) (basename : string option)
       | TLiteral lty -> (
           match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
       | TArrow _ -> "f"
-      | TTraitType (_, _, name) -> name_from_type_ident name)
+      | TTraitType (_, name) -> name_from_type_ident name)
 
 (** Generates a type variable basename. *)
 let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :

compiler/ExtractTypes.ml

@@ -528,7 +528,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_print_space fmt ();
       extract_rec false ret_ty;
       if inside then F.pp_print_string fmt ")"
-  | TTraitType (trait_ref, generics, type_name) -> (
+  | TTraitType (trait_ref, type_name) -> (
       if !parameterize_trait_types then raise (Failure "Unimplemented")
       else
         let type_name =
@@ -547,19 +547,14 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
         *)
         match trait_ref.trait_id with
         | Self ->
-            assert (generics = empty_generic_args);
             assert (trait_ref.generics = empty_generic_args);
             extract_trait_instance_id_with_dot ctx fmt no_params_tys false
               trait_ref.trait_id;
             F.pp_print_string fmt type_name
         | _ ->
             (* HOL4 doesn't have 1st class types *)
             assert (!backend <> HOL4);
-            let use_brackets = generics <> empty_generic_args in
-            if use_brackets then F.pp_print_string fmt "(";
             extract_trait_ref ctx fmt no_params_tys false trait_ref;
-            extract_generic_args ctx fmt no_params_tys generics;
-            if use_brackets then F.pp_print_string fmt ")";
             F.pp_print_string fmt ("." ^ add_brackets type_name))
 
 and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter)

compiler/InterpreterExpressions.ml

@@ -263,8 +263,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
       match cv.value with
       | CLiteral lit ->
           cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx
-      | CTraitConst (trait_ref, generics, const_name) -> (
-          assert (generics = empty_generic_args);
+      | CTraitConst (trait_ref, const_name) -> (
           match trait_ref.trait_id with
           | TraitImpl _ ->
               (* This shouldn't happen: if we refer to a concrete implementation, we
@@ -294,8 +293,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                        ( ctx0,
                          None,
                          value_as_symbolic v.value,
-                         SymbolicAst.VaTraitConstValue
-                           (trait_ref, generics, const_name),
+                         SymbolicAst.VaTraitConstValue (trait_ref, const_name),
                          e ))))
       | CVar vid -> (
           let ctx0 = ctx in

compiler/InterpreterStatements.ml

@@ -769,12 +769,8 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
               ("trait method call:\n- call: " ^ call_to_string ctx call
              ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n"
               ^ generic_args_to_string ctx func.generics
-              ^ "\n- trait and method generics:\n"
-              ^ generic_args_to_string ctx
-                  (Option.get func.trait_and_method_generic_args)));
-          (* When instantiating, we need to group the generics for the trait ref
-             and the method *)
-          let generics = Option.get func.trait_and_method_generic_args in
+              ^ "\n- trait_ref.trait_decl_ref: "
+              ^ trait_decl_ref_to_string ctx trait_ref.trait_decl_ref));
           (* Lookup the trait method signature - there are several possibilities
              depending on whethere we call a top-level trait method impl or the
              method from a local clause *)
@@ -794,6 +790,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
               | Some (_, id) ->
                   (* This is a required method *)
                   let method_def = ctx_lookup_fun_decl ctx id in
+                  (* We have to concatenate the generics for the impl
+                     and the generics for the method *)
+                  let generics =
+                    merge_generic_args trait_ref.generics func.generics
+                  in
                   (* Instantiate *)
                   let tr_self = TraitRef trait_ref in
                   let fid : fun_id = FRegular id in
@@ -898,6 +899,12 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
               log#ldebug
                 (lazy ("method:\n" ^ fun_decl_to_string ctx method_def));
               (* Instantiate *)
+              (* When instantiating, we need to group the generics for the
+                 trait ref and the generics for the method *)
+              let generics =
+                TypesUtils.merge_generic_args
+                  trait_ref.trait_decl_ref.decl_generics func.generics
+              in
               let regions_hierarchy =
                 LlbcAstUtils.FunIdMap.find (FRegular method_id)
                   ctx.fun_ctx.regions_hierarchies
@@ -1025,7 +1032,6 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) :
         {
           func = FunId (FRegular global.body);
           generics = TypesUtils.empty_generic_args;
-          trait_and_method_generic_args = None;
         }
       in
       let call = { func = FnOpRegular func; args = []; dest } in

compiler/InterpreterUtils.ml

@@ -43,6 +43,8 @@ let fun_sig_to_string = Print.EvalCtx.fun_sig_to_string
 let inst_fun_sig_to_string = Print.EvalCtx.inst_fun_sig_to_string
 let ty_to_string = Print.EvalCtx.ty_to_string
 let generic_args_to_string = Print.EvalCtx.generic_args_to_string
+let trait_ref_to_string = Print.EvalCtx.trait_ref_to_string
+let trait_decl_ref_to_string = Print.EvalCtx.trait_decl_ref_to_string
 
 let fun_id_or_trait_method_ref_to_string =
   Print.EvalCtx.fun_id_or_trait_method_ref_to_string

compiler/Print.ml

@@ -531,6 +531,10 @@ module EvalCtx = struct
     let env = eval_ctx_to_fmt_env ctx in
     trait_ref_to_string env x
 
+  let trait_decl_ref_to_string (ctx : eval_ctx) (x : trait_decl_ref) : string =
+    let env = eval_ctx_to_fmt_env ctx in
+    trait_decl_ref_to_string env x
+
   let trait_instance_id_to_string (ctx : eval_ctx) (x : trait_instance_id) :
       string =
     let env = eval_ctx_to_fmt_env ctx in

compiler/PrintPure.ml

@@ -159,14 +159,9 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
         ty_to_string env true arg_ty ^ " -> " ^ ty_to_string env false ret_ty
       in
       if inside then "(" ^ ty ^ ")" else ty
-  | TTraitType (trait_ref, generics, type_name) ->
+  | TTraitType (trait_ref, type_name) ->
       let trait_ref = trait_ref_to_string env false trait_ref in
-      let s =
-        if generics = empty_generic_args then trait_ref ^ "::" ^ type_name
-        else
-          let generics = generic_args_to_string env generics in
-          "(" ^ trait_ref ^ " " ^ generics ^ ")::" ^ type_name
-      in
+      let s = trait_ref ^ "::" ^ type_name in
       if inside then "(" ^ s ^ ")" else s
 
 and generic_args_to_strings (env : fmt_env) (inside : bool)
@@ -624,14 +619,9 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string)
             let field_s = adt_field_to_string env adt_id field_id in
             (* Adopting an F*-like syntax *)
             (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, [])
-        | TraitConst (trait_ref, generics, const_name) ->
+        | TraitConst (trait_ref, const_name) ->
             let trait_ref = trait_ref_to_string env true trait_ref in
-            let generics_s = generic_args_to_string env generics in
-            let qualif =
-              if generics <> empty_generic_args then
-                "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name
-              else trait_ref ^ "." ^ const_name
-            in
+            let qualif = trait_ref ^ "." ^ const_name in
             (qualif, []))
     | _ ->
         (* "Regular" expression case *)

compiler/Pure.ml

@@ -283,7 +283,7 @@ type ty =
   | TVar of type_var_id
   | TLiteral of literal_type
   | TArrow of ty * ty
-  | TTraitType of trait_ref * generic_args * string
+  | TTraitType of trait_ref * string
       (** The string is for the name of the associated type *)
 
 and trait_ref = {
@@ -374,7 +374,6 @@ type generic_params = {
 
 type trait_type_constraint = {
   trait_ref : trait_ref;
-  generics : generic_args;
   type_name : trait_item_name;
   ty : ty;
 }
@@ -599,8 +598,7 @@ type qualif_id =
   | Global of global_decl_id
   | AdtCons of adt_cons_id  (** A function or ADT constructor identifier *)
   | Proj of projection  (** Field projector *)
-  | TraitConst of trait_ref * generic_args * string
-      (** A trait associated constant *)
+  | TraitConst of trait_ref * string  (** A trait associated constant *)
 [@@deriving show]
 
 (** An instantiated qualifier.

compiler/RegionsHierarchy.ml

@@ -169,7 +169,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t)
         (* Continue *)
         explore_ty outer ty
     | TRawPtr (ty, _) -> explore_ty outer ty
-    | TTraitType (trait_ref, _generic_args, _) ->
+    | TTraitType (trait_ref, _) ->
         (* The trait should reference a clause, and not an implementation
            (otherwise it should have been normalized) *)
         assert (

compiler/SymbolicAst.ml

@@ -251,8 +251,7 @@ and value_aggregate =
   | VaCgValue of const_generic_var_id
       (** This is used when evaluating a const generic value: in the interpreter,
           we introduce a fresh symbolic value. *)
-  | VaTraitConstValue of trait_ref * generic_args * string
-      (** A trait constant value *)
+  | VaTraitConstValue of trait_ref * string  (** A trait constant value *)
 [@@deriving
   show,
     visitors

compiler/SymbolicToPure.ml

@@ -474,10 +474,9 @@ let rec translate_sty (ty : T.ty) : ty =
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
       TAdt (TAssumed (TRawPtr mut), generics)
-  | TTraitType (trait_ref, generics, type_name) ->
+  | TTraitType (trait_ref, type_name) ->
       let trait_ref = translate_strait_ref trait_ref in
-      let generics = translate_sgeneric_args generics in
-      TTraitType (trait_ref, generics, type_name)
+      TTraitType (trait_ref, type_name)
   | TArrow _ -> raise (Failure "TODO")
 
 and translate_sgeneric_args (generics : T.generic_args) : generic_args =
@@ -497,11 +496,10 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause =
 
 let translate_strait_type_constraint (ttc : T.trait_type_constraint) :
     trait_type_constraint =
-  let { T.trait_ref; generics; type_name; ty } = ttc in
+  let { T.trait_ref; type_name; ty } = ttc in
   let trait_ref = translate_strait_ref trait_ref in
-  let generics = translate_sgeneric_args generics in
   let ty = translate_sty ty in
-  { trait_ref; generics; type_name; ty }
+  { trait_ref; type_name; ty }
 
 let translate_predicates (preds : T.predicates) : predicates =
   let trait_type_constraints =
@@ -638,10 +636,9 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty =
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
       TAdt (TAssumed (TRawPtr mut), generics)
-  | TTraitType (trait_ref, generics, type_name) ->
+  | TTraitType (trait_ref, type_name) ->
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
-      let generics = translate_fwd_generic_args type_infos generics in
-      TTraitType (trait_ref, generics, type_name)
+      TTraitType (trait_ref, type_name)
   | TArrow _ -> raise (Failure "TODO")
 
 and translate_fwd_generic_args (type_infos : type_infos)
@@ -737,16 +734,14 @@ let rec translate_back_ty (type_infos : type_infos)
   | TRawPtr _ ->
       (* TODO: not sure what to do here *)
       None
-  | TTraitType (trait_ref, generics, type_name) ->
-      assert (generics.regions = []);
+  | TTraitType (trait_ref, type_name) ->
       assert (
         AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id);
       if inside_mut then
-        (* Translate the trait ref and the generics as "forward" generics -
+        (* Translate the trait ref as a "forward" trait ref -
            we do not want to filter any type *)
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
-        let generics = translate_fwd_generic_args type_infos generics in
-        Some (TTraitType (trait_ref, generics, type_name))
+        Some (TTraitType (trait_ref, type_name))
       else None
   | TArrow _ -> raise (Failure "TODO")
 
@@ -2956,11 +2951,10 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
         in
         { e = StructUpdate su; ty = var.ty }
     | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
-    | VaTraitConstValue (trait_ref, generics, const_name) ->
+    | VaTraitConstValue (trait_ref, const_name) ->
         let type_infos = ctx.type_ctx.type_infos in
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
-        let generics = translate_fwd_generic_args type_infos generics in
-        let qualif_id = TraitConst (trait_ref, generics, const_name) in
+        let qualif_id = TraitConst (trait_ref, const_name) in
         let qualif = { id = qualif_id; generics = empty_generic_args } in
         { e = Qualif qualif; ty = var.ty }
   in

compiler/Translate.ml

@@ -1086,7 +1086,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     let exe_dir = Filename.dirname Sys.argv.(0) in
     let primitives_src_dest =
       match !Config.backend with
-      | FStar -> Some ("/backends/fstar/merge/Primitives.fst", "Primitives.fst")
+      | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
       | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
       | Lean -> None
       | HOL4 -> None

compiler/TypesUtils.ml

@@ -105,9 +105,8 @@ let generic_args_no_regions (x : generic_args) : bool =
 (** Return [true] if the trait type constraint doesn't contain regions (including erased regions) *)
 let trait_type_constraint_no_regions (x : trait_type_constraint) : bool =
   try
-    let { trait_ref; generics; type_name = _; ty } = x in
+    let { trait_ref; type_name = _; ty } = x in
     raise_if_region_ty_visitor#visit_trait_ref () trait_ref;
-    raise_if_region_ty_visitor#visit_generic_args () generics;
     raise_if_region_ty_visitor#visit_ty () ty;
     true
   with Found -> false