Typeclasses: remove old mk_class

src/parser/FStar.Parser.Const.fst

@@ -497,7 +497,6 @@ let tactic_lid = fstar_tactics_lid' ["Effect"; "tactic"]
 let meta_projectors_attr = fstar_tactics_lid' ["MkProjectors"; "meta_projectors"]
 let mk_projs_lid   = fstar_tactics_lid' ["MkProjectors"; "mk_projs"]
 
-let mk_class_lid   = fstar_tactics_lid' ["Typeclasses"; "mk_class"]
 let tcresolve_lid  = fstar_tactics_lid' ["Typeclasses"; "tcresolve"]
 let tcclass_lid = fstar_tactics_lid' ["Typeclasses"; "tcclass"]
 let tcinstance_lid = fstar_tactics_lid' ["Typeclasses"; "tcinstance"]

ulib/FStar.Tactics.Typeclasses.fst

@@ -307,126 +307,3 @@ let tcresolve () : Tac unit =
     | TacticFailure (msg,r) ->
       fail_doc_at ([text "Typeclass resolution failed."] @ msg) r
     | e -> raise e
-
-(**** Generating methods from a class ****)
-
-(* In TAC, not Tot *)
-private
-let rec mk_abs (bs : list binder) (body : term) : Tac term (decreases bs) =
-    match bs with
-    | [] -> body
-    | b::bs -> pack (Tv_Abs b (mk_abs bs body))
-
-private
-let rec last (l : list 'a) : Tac 'a =
-  match l with
-  | [] -> fail "last: empty list"
-  | [x] -> x
-  | _::xs -> last xs
-
-private
-let filter_no_method_binders (bs:binders)
-  : binders
-  = let open FStar.Reflection.TermEq.Simple in
-    let has_no_method_attr (b:binder) : bool =
-      L.existsb (term_eq (`no_method)) b.attrs
-    in
-    bs |> L.filter (fun b -> not (has_no_method_attr b))
-
-private
-let binder_set_meta (b : binder) (t : term) : binder =
-  { b with qual = Q_Meta t }
-
-[@@plugin]
-let mk_class (nm:string) : Tac decls =
-    let ns = explode_qn nm in
-    let r = lookup_typ (top_env ()) ns in
-    guard (Some? r);
-    let Some se = r in
-    let to_propagate = L.filter (function Inline_for_extraction | NoExtract -> true | _ -> false) (sigelt_quals se) in
-    let sv = inspect_sigelt se in
-    guard (Sg_Inductive? sv);
-    let Sg_Inductive {nm=name;univs=us;params;typ=ity;ctors} = sv in
-    debug (fun () -> "params = " ^ Tactics.Util.string_of_list binder_to_string params);
-    debug (fun () -> "got it, name = " ^ implode_qn name);
-    debug (fun () -> "got it, ity = " ^ term_to_string ity);
-    let ctor_name = last name in
-    // Must have a single constructor
-    guard (L.length ctors = 1);
-    let [(c_name, ty)] = ctors in
-    debug (fun () -> "got ctor " ^ implode_qn c_name ^ " of type " ^ term_to_string ty);
-    let bs, cod = collect_arr_bs ty in
-    let r = inspect_comp cod in
-    guard (C_Total? r);
-    let C_Total cod = r in (* must be total *)
-
-    debug (fun () -> "params = " ^ Tactics.Util.string_of_list binder_to_string params);
-    debug (fun () -> "n_params = " ^ string_of_int (List.Tot.Base.length params));
-    debug (fun () -> "n_univs = " ^ string_of_int (List.Tot.Base.length us));
-    debug (fun () -> "cod = " ^ term_to_string cod);
-
-    (* print ("n_bs = " ^ string_of_int (List.Tot.Base.length bs)); *)
-
-    let base : string = "__proj__Mk" ^ ctor_name ^ "__item__" in
-
-    (* Make a sigelt for each method *)
-    filter_no_method_binders bs
-    |> Tactics.Util.map (fun (b:binder) ->
-      let s = name_of_binder b in
-      debug (fun () -> "processing method " ^ s);
-      let ns = cur_module () in
-      let sfv = pack_fv (ns @ [s]) in
-      let dbv = fresh_namedv_named "d" in
-      let tcr = (`tcresolve) in
-      let tcdict = {
-        ppname = seal "dict";
-        sort   = cod;
-        uniq   = fresh();
-        qual   = Q_Meta tcr;
-        attrs  = [];
-      } in
-      let proj_name = cur_module () @ [base ^ s] in
-      let proj = pack (Tv_FVar (pack_fv proj_name)) in
-
-      let proj_lb =
-        match lookup_typ (top_env ()) proj_name with
-        | None -> fail "mk_class: proj not found?"
-        | Some se ->
-          match inspect_sigelt se with
-          | Sg_Let {lbs} -> lookup_lb lbs proj_name
-          | _ -> fail "mk_class: proj not Sg_Let?"
-      in
-      (* print ("proj_ty = " ^ term_to_string proj_lb.lb_typ); *)
-
-      let ty =
-        let bs, cod = collect_arr_bs proj_lb.lb_typ in
-        let ps, bs = List.Tot.Base.splitAt (List.Tot.Base.length params) bs in
-        match bs with
-        | [] -> fail "mk_class: impossible, no binders"
-        | b1::bs' ->
-            let b1 = binder_set_meta b1 tcr in
-            mk_arr (ps@(b1::bs')) cod
-      in
-      let def =
-        let bs, body = collect_abs proj_lb.lb_def in
-        let ps, bs = List.Tot.Base.splitAt (List.Tot.Base.length params) bs in
-        match bs with
-        | [] -> fail "mk_class: impossible, no binders"
-        | b1::bs' ->
-            let b1 = binder_set_meta b1 tcr in
-            mk_abs (ps@(b1::bs')) body
-      in
-      debug (fun () -> "def = " ^ term_to_string def);
-      debug (fun () -> "ty  = " ^ term_to_string ty);
-
-      let ty : term = ty in
-      let def : term = def in
-      let sfv : fv = sfv in
-
-      let lb = { lb_fv=sfv; lb_us=proj_lb.lb_us; lb_typ=ty; lb_def=def } in
-      let se = pack_sigelt (Sg_Let {isrec=false; lbs=[lb]}) in
-      let se = set_sigelt_quals to_propagate se in
-      let se = set_sigelt_attrs b.attrs se in
-      //debug (fun () -> "trying to return : " ^ term_to_string (quote se));
-      se
-    )

ulib/FStar.Tactics.Typeclasses.fsti

@@ -40,10 +40,8 @@ val no_method : unit
 run this tactics without having to know its definition in the .fst *)
 val tcresolve : unit -> Tac unit
 
-(* The metaprogram to generate class methods. Also a plugin. This
-is inserted automatically by the desugaring phase for any `class`
-declaration. *)
-val mk_class (nm:string) : Tac decls
+(* NB: The generation of methods for a class is implemented in
+FStar.Tactics.MkProjectors.fst *)
 
 (* Helper to solve an explicit argument by typeclass resolution *)
 [@@tcnorm]