Merge pull request #751 from hacspec/engine-propagate-trait-generics

Engine: propagate trait generics arguments

engine/backends/fstar/fstar-surface-ast/FStar_Parser_Const.ml

@@ -499,6 +499,8 @@ let (mk_class_lid : FStar_Ident.lid) =
   fstar_tactics_lid' ["Typeclasses"; "mk_class"]
 let (tcresolve_lid : FStar_Ident.lid) =
   fstar_tactics_lid' ["Typeclasses"; "tcresolve"]
+let (solve_lid : FStar_Ident.lid) =
+  fstar_tactics_lid' ["Typeclasses"; "solve"]
 let (tcclass_lid : FStar_Ident.lid) =
   fstar_tactics_lid' ["Typeclasses"; "tcclass"]
 let (tcinstance_lid : FStar_Ident.lid) =

engine/backends/fstar/fstar_ast.ml

@@ -35,6 +35,7 @@ module Attrs = struct
 end
 
 let tcresolve = term @@ AST.Var FStar_Parser_Const.tcresolve_lid
+let solve = term @@ AST.Var FStar_Parser_Const.solve_lid
 
 let pat_var_tcresolve (var : string option) =
   let tcresolve = Some (AST.Meta tcresolve) in

engine/backends/fstar/fstar_backend.ml

@@ -407,17 +407,25 @@ struct
       (* in *)
       F.term @@ F.AST.Const (F.Const.Const_string ("failure", F.dummyRange))
 
-  and fun_application ~span f args generic_args =
-    let generic_args =
-      generic_args
-      |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true)
-      |> List.map ~f:(function
-           | GConst const -> (pexpr const, F.AST.Nothing)
+  and fun_application ~span f args ~trait_generic_args ~generic_args =
+    let pgeneric_args ?qualifier =
+      let qualifier_or default = Option.value ~default qualifier in
+      List.filter ~f:(function GType (TArrow _) -> false | _ -> true)
+      >> List.map ~f:(function
+           | GConst const -> (pexpr const, qualifier_or F.AST.Nothing)
            | GLifetime _ -> .
-           | GType ty -> (pty span ty, F.AST.Hash))
+           | GType ty -> (pty span ty, qualifier_or F.AST.Hash))
     in
     let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
-    F.mk_app f (generic_args @ args)
+    let trait_generic_args =
+      Option.map
+        ~f:
+          (pgeneric_args ~qualifier:F.AST.Hash
+          >> Fn.flip ( @ ) [ (F.solve, F.AST.Hash) ])
+        trait_generic_args
+      |> Option.value ~default:[]
+    in
+    F.mk_app f (trait_generic_args @ pgeneric_args generic_args @ args)
 
   and pexpr_unwrapped (e : expr) =
     match e.e with
@@ -449,7 +457,7 @@ struct
         {
           f = { e = GlobalVar f; _ };
           args = [ { e = Literal (String s); _ } ];
-          generic_args;
+          generic_args = _;
         }
       when Global_ident.eq_name Hax_lib__int__Impl_5___unsafe_from_str f ->
         (match
@@ -463,8 +471,10 @@ struct
             @@ "pexpr: expected a integer, found the following non-digit \
                 chars: '" ^ s ^ "'");
         F.AST.Const (F.Const.Const_int (s, None)) |> F.term
-    | App { f; args; generic_args; bounds_impls = _; impl = _ } ->
-        fun_application ~span:e.span (pexpr f) args generic_args
+    | App { f; args; generic_args; bounds_impls = _; trait } ->
+        let trait_generic_args = Option.map ~f:snd trait in
+        fun_application (pexpr f) args ~span:e.span ~trait_generic_args
+          ~generic_args
     | If { cond; then_; else_ } ->
         F.term
         @@ F.AST.If
@@ -629,12 +639,16 @@ struct
     type kind = Implicit | Tcresolve | Explicit
     type t = { kind : kind; ident : F.Ident.ident; typ : F.AST.term }
 
-    let of_generic_param ?(kind : kind = Implicit) span (p : generic_param) : t
-        =
+    let make_explicit x = { x with kind = Explicit }
+
+    let implicit_to_explicit x =
+      if [%matches? Tcresolve] x.kind then x else make_explicit x
+
+    let of_generic_param span (p : generic_param) : t =
       let ident = plocal_ident p.ident in
       match p.kind with
       | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME"
-      | GPType { default = _ } -> { kind; typ = F.type0_term; ident }
+      | GPType { default = _ } -> { kind = Implicit; typ = F.type0_term; ident }
       | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident }
 
     let of_generic_constraint span (nth : int) (c : generic_constraint) =
@@ -644,8 +658,8 @@ struct
           let typ = c_trait_goal span goal in
           { kind = Tcresolve; ident = F.id name; typ }
 
-    let of_generics ?(kind : kind = Implicit) span generics : t list =
-      List.map ~f:(of_generic_param ~kind span) generics.params
+    let of_generics span generics : t list =
+      List.map ~f:(of_generic_param span) generics.params
       @ List.mapi ~f:(of_generic_constraint span) generics.constraints
 
     let of_typ span (nth : int) typ : t =
@@ -676,17 +690,24 @@ struct
     let to_term (x : t) : F.AST.term =
       F.term @@ F.AST.Var (FStar_Ident.lid_of_ns_and_id [] (to_ident x))
 
+    let to_imp (x : t) : F.AST.imp =
+      match x.kind with Tcresolve | Implicit -> Hash | Explicit -> Nothing
+
+    let to_qualified_term : t -> F.AST.term * F.AST.imp = to_term &&& to_imp
+
+    let to_qualifier (x : t) : F.AST.arg_qualifier option =
+      match x.kind with
+      | Tcresolve -> Some TypeClassArg
+      | Implicit -> Some Implicit
+      | Explicit -> None
+
     let to_binder (x : t) : F.AST.binder =
       F.AST.
         {
           b = F.AST.Annotated (x.ident, x.typ);
           brange = F.dummyRange;
           blevel = Un;
-          aqual =
-            (match x.kind with
-            | Tcresolve -> Some TypeClassArg
-            | Implicit -> Some Implicit
-            | Explicit -> None);
+          aqual = to_qualifier x;
           battributes = [];
         }
   end
@@ -1014,7 +1035,8 @@ struct
                [
                  F.AST.TyconRecord
                    ( F.id @@ U.Concrete_ident_view.to_definition_name name,
-                     FStarBinder.of_generics ~kind:Explicit e.span generics
+                     FStarBinder.of_generics e.span generics
+                     |> List.map ~f:FStarBinder.implicit_to_explicit
                      |> List.map ~f:FStarBinder.to_binder,
                      None,
                      [],
@@ -1080,7 +1102,8 @@ struct
                [
                  F.AST.TyconVariant
                    ( F.id @@ U.Concrete_ident_view.to_definition_name name,
-                     FStarBinder.of_generics ~kind:Explicit e.span generics
+                     FStarBinder.of_generics e.span generics
+                     |> List.map ~f:FStarBinder.implicit_to_explicit
                      |> List.map ~f:FStarBinder.to_binder,
                      None,
                      constructors );
@@ -1157,20 +1180,13 @@ struct
             | _ -> unsupported_macro ())
         | _ -> unsupported_macro ())
     | Trait { name; generics; items } ->
-        let bds =
-          List.map
-            ~f:FStarBinder.(of_generic_param e.span >> to_binder)
-            generics.params
-        in
         let name_str = U.Concrete_ident_view.to_definition_name name in
         let name_id = F.id @@ name_str in
         let fields =
           List.concat_map
             ~f:(fun i ->
               let name = U.Concrete_ident_view.to_definition_name i.ti_ident in
-              let generics =
-                FStarBinder.of_generics ~kind:Implicit i.ti_span i.ti_generics
-              in
+              let generics = FStarBinder.of_generics i.ti_span i.ti_generics in
               let bds = generics |> List.map ~f:FStarBinder.to_binder in
               let fields =
                 match i.ti_v with
@@ -1212,14 +1228,16 @@ struct
                     let inputs = generics @ inputs in
                     let output = pty e.span output in
                     let ty_pre_post =
-                      let inputs = List.map ~f:FStarBinder.to_term inputs in
+                      let inputs =
+                        List.map ~f:FStarBinder.to_qualified_term inputs
+                      in
                       let add_pre n = n ^ "_pre" in
                       let pre_name_str =
                         U.Concrete_ident_view.to_definition_name
                           (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident)
                       in
                       let pre =
-                        F.mk_e_app (F.term_of_lid [ pre_name_str ]) inputs
+                        F.mk_app (F.term_of_lid [ pre_name_str ]) inputs
                       in
                       let result = F.term_of_lid [ "result" ] in
                       let add_post n = n ^ "_post" in
@@ -1228,9 +1246,9 @@ struct
                           (Concrete_ident.Create.map_last ~f:add_post i.ti_ident)
                       in
                       let post =
-                        F.mk_e_app
+                        F.mk_app
                           (F.term_of_lid [ post_name_str ])
-                          (inputs @ [ result ])
+                          (inputs @ [ (result, Nothing) ])
                       in
                       let post =
                         F.mk_e_abs
@@ -1277,7 +1295,17 @@ struct
             [ (F.id marker_field, None, [], pty e.span U.unit_typ) ]
           else fields
         in
-        let tcdef = F.AST.TyconRecord (name_id, bds, None, [], fields) in
+        let tcdef =
+          (* Binders are explicit on class definitions *)
+          let bds =
+            List.map
+              ~f:
+                FStarBinder.(
+                  of_generic_param e.span >> implicit_to_explicit >> to_binder)
+              generics.params
+          in
+          F.AST.TyconRecord (name_id, bds, None, [], fields)
+        in
         let d = F.AST.Tycon (false, true, [ tcdef ]) in
         [ `Intf { d; drange = F.dummyRange; quals = []; attrs = [] } ]
     | Impl
@@ -1296,9 +1324,9 @@ struct
           @@ F.AST.PatApp (pat, List.map ~f:FStarBinder.to_pattern generics)
         in
         let typ =
-          fun_application ~span:e.span
+          F.mk_e_app
             (F.term @@ F.AST.Name (pglobal_ident e.span trait))
-            [] generic_args
+            (List.map ~f:(pgeneric_value e.span) generic_args)
         in
         let pat = F.pat @@ F.AST.PatAscribed (pat, (typ, None)) in
         let fields =

engine/lib/ast.ml

@@ -200,7 +200,7 @@ functor
           args : expr list (* ; f_span: span *);
           generic_args : generic_value list;
           bounds_impls : impl_expr list;
-          impl : impl_expr option;
+          trait : (impl_expr * generic_value list) option;
         }
       | Literal of literal
       | Array of expr list

engine/lib/ast_utils.ml

@@ -79,8 +79,9 @@ module Make (F : Features.T) = struct
         * impl_expr list)
         option =
       match e.e with
-      | App { f; args; generic_args; impl; bounds_impls } ->
-          Some (f, args, generic_args, impl, bounds_impls)
+      | App { f; args; generic_args; trait; bounds_impls } ->
+          (* TODO: propagate full trait *)
+          Some (f, args, generic_args, Option.map ~f:fst trait, bounds_impls)
       | _ -> None
 
     let pbinding_simple (p : pat) : (local_ident * ty) option =
@@ -96,7 +97,7 @@ module Make (F : Features.T) = struct
             f = { e = GlobalVar (`Concrete f'); _ };
             args = [ e ];
             generic_args = _;
-            impl = _;
+            trait = _;
             _;
             (* TODO: see issue #328 *)
           }
@@ -201,7 +202,7 @@ module Make (F : Features.T) = struct
                   f = { e = GlobalVar (`Primitive Deref); _ };
                   args = [ { e = Borrow { e = sub; _ }; _ } ];
                   generic_args = _;
-                  impl = _;
+                  trait = _;
                   _;
                   (* TODO: see issue #328 *)
                 } ->
@@ -343,7 +344,7 @@ module Make (F : Features.T) = struct
                   f = { e = GlobalVar (`Primitive Cast); _ } as f;
                   args = [ arg ];
                   generic_args;
-                  impl;
+                  trait;
                   bounds_impls;
                 } ->
                 ascribe
@@ -355,7 +356,7 @@ module Make (F : Features.T) = struct
                           f;
                           args = [ ascribe arg ];
                           generic_args;
-                          impl;
+                          trait;
                           bounds_impls;
                         };
                   }
@@ -875,7 +876,7 @@ module Make (F : Features.T) = struct
             args;
             generic_args = [];
             bounds_impls = [];
-            impl;
+            trait = Option.map ~f:(fun impl -> (impl, [])) impl;
           };
       typ = ret_typ;
       span;
@@ -924,7 +925,7 @@ module Make (F : Features.T) = struct
           args = [ e ];
           generic_args = _;
           bounds_impls = _;
-          impl = _;
+          trait = _;
         } ->
         next e
     | _ -> e
@@ -960,7 +961,7 @@ module Make (F : Features.T) = struct
                 args = [ e ];
                 generic_args = [];
                 bounds_impls = [];
-                impl = None (* TODO: see issue #328 *);
+                trait = None (* TODO: see issue #328 *);
               };
           typ;
           span;
@@ -1060,7 +1061,7 @@ module Make (F : Features.T) = struct
             args = [ tuple ];
             generic_args = [] (* TODO: see issue #328 *);
             bounds_impls = [];
-            impl = None (* TODO: see issue #328 *);
+            trait = None (* TODO: see issue #328 *);
           };
     }
 
@@ -1104,7 +1105,7 @@ module Make (F : Features.T) = struct
             args = [ place ];
             generic_args = _;
             bounds_impls = _;
-            impl = _;
+            trait = _;
           (* TODO: see issue #328 *)
           } ->
           let* place = of_expr place in
@@ -1115,7 +1116,7 @@ module Make (F : Features.T) = struct
             args = [ place; index ];
             generic_args = _;
             bounds_impls = _;
-            impl = _;
+            trait = _;
           (* TODO: see issue #328 *)
           }
         when Global_ident.eq_name Core__ops__index__Index__index f ->
@@ -1128,7 +1129,7 @@ module Make (F : Features.T) = struct
             args = [ place; index ];
             generic_args = _;
             bounds_impls = _;
-            impl = _;
+            trait = _;
           (* TODO: see issue #328 *)
           }
         when Global_ident.eq_name Core__ops__index__IndexMut__index_mut f ->