val mk_class (nm:string) : Tac decls
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
    (* print ("params = " ^ Tactics.Util.string_of_list binder_to_string params); *)
    (* print ("got it, name = " ^ implode_qn name); *)
    (* print ("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
    (* print ("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 *)

    (* print ("params = " ^ Tactics.Util.string_of_list binder_to_string params); *)
    (* print ("n_params = " ^ string_of_int (List.Tot.Base.length params)); *)
    (* print ("n_univs = " ^ string_of_int (List.Tot.Base.length us)); *)
    (* print ("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 *)
    Tactics.Util.map (fun (b:binder) ->
                  let s = name_of_binder b in
                  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
                  (* print ("def = " ^ term_to_string def); *)
                  (* print ("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
                  (* print ("trying to return : " ^ term_to_string (quote se)); *)
                  se
    ) (filter_no_method_binders bs)
val mk_class (nm:string) : Tac decls
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 = params ; typ = ity ; ctors = ctors } = sv in
let ctor_name = last name in
guard (L.length ctors = 1);
let [c_name, ty] = ctors in
let bs, cod = collect_arr_bs ty in
let r = inspect_comp cod in
guard (C_Total? r);
let C_Total cod = r in
let base:string = "__proj__Mk" ^ ctor_name ^ "__item__" in
Tactics.Util.map (fun (b: binder) ->
      let s = name_of_binder b in
      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 = lbs } -> lookup_lb lbs proj_name
          | _ -> fail "mk_class: proj not Sg_Let?"
      in
      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
      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
      se)
  (filter_no_method_binders bs)
FStar.Tactics.Typeclasses.fst.checked
prims.fst.checked FStar.Tactics.V2.SyntaxHelpers.fst.checked FStar.Tactics.V2.SyntaxCoercions.fst.checked FStar.Tactics.V2.Derived.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.Util.fst.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.Common.fsti.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked
FStar.Tactics.Typeclasses.fst
Prims.string FStar.Reflection.Types.sigelt FStar.Reflection.Types.name Prims.list FStar.Tactics.NamedView.univ_name FStar.Tactics.NamedView.binders FStar.Reflection.Types.typ FStar.Reflection.V2.Data.ctor FStar.Tactics.NamedView.binder FStar.Tactics.NamedView.comp FStar.Tactics.Util.map FStar.Reflection.V2.Builtins.set_sigelt_attrs FStar.Tactics.NamedView.__proj__Mkbinder__item__attrs FStar.Reflection.V2.Builtins.set_sigelt_quals FStar.Tactics.NamedView.pack_sigelt FStar.Tactics.NamedView.Sg_Let FStar.Tactics.NamedView.Mknamed_sigelt_view__Sg_Let__payload Prims.Cons FStar.Tactics.NamedView.letbinding Prims.Nil FStar.Tactics.NamedView.Mkletbinding FStar.Tactics.NamedView.__proj__Mkletbinding__item__lb_us FStar.Reflection.Types.fv FStar.Tactics.NamedView.term FStar.Tactics.V2.Derived.fail FStar.Tactics.Typeclasses.mk_abs FStar.Tactics.Typeclasses.op_At FStar.Tactics.Typeclasses.binder_set_meta FStar.Pervasives.Native.tuple2 FStar.List.Tot.Base.splitAt FStar.List.Tot.Base.length FStar.Tactics.V2.SyntaxHelpers.collect_abs FStar.Tactics.NamedView.__proj__Mkletbinding__item__lb_def FStar.Tactics.V2.SyntaxHelpers.mk_arr FStar.Tactics.V2.SyntaxHelpers.collect_arr_bs FStar.Tactics.NamedView.__proj__Mkletbinding__item__lb_typ Prims.bool FStar.Tactics.V2.SyntaxHelpers.lookup_lb FStar.Tactics.NamedView.named_sigelt_view FStar.Tactics.NamedView.inspect_sigelt FStar.Pervasives.Native.option FStar.Reflection.V2.Builtins.lookup_typ FStar.Reflection.Types.env FStar.Tactics.V2.Builtins.top_env FStar.Tactics.NamedView.pack FStar.Tactics.NamedView.Tv_FVar FStar.Reflection.V2.Builtins.pack_fv Prims.op_Hat FStar.Tactics.V2.Derived.cur_module FStar.Tactics.NamedView.Mkbinder FStar.Sealed.seal FStar.Reflection.V2.Data.Q_Meta Prims.nat FStar.Tactics.V2.Builtins.fresh FStar.Reflection.Types.term FStar.Tactics.NamedView.namedv FStar.Tactics.V2.Derived.fresh_namedv_named FStar.Tactics.V2.Derived.name_of_binder FStar.Tactics.Typeclasses.filter_no_method_binders FStar.Reflection.Types.decls Prims.unit FStar.Tactics.V2.Derived.guard FStar.Reflection.V2.Data.uu___is_C_Total FStar.Tactics.NamedView.inspect_comp Prims.op_Equality Prims.int FStar.Tactics.Typeclasses.last FStar.Tactics.NamedView.uu___is_Sg_Inductive FStar.Reflection.V2.Data.qualifier Prims.l_Forall Prims.l_imp FStar.List.Tot.Base.memP Prims.b2t FStar.List.Tot.Base.filter FStar.Reflection.V2.Builtins.sigelt_quals FStar.Pervasives.Native.uu___is_Some FStar.Reflection.V2.Builtins.explode_qn
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Tactics.Typeclasses

open FStar.Reflection.V2
open FStar.Tactics.Common
open FStar.Tactics.Effect
open FStar.Tactics.V2.Builtins
open FStar.Tactics.V2.SyntaxHelpers
open FStar.Tactics.V2.Derived
open FStar.Tactics.V2.SyntaxCoercions
open FStar.Tactics.NamedView

module L = FStar.List.Tot.Base
let (@) = L.op_At

(* The attribute that marks classes *)
irreducible
let tcclass : unit = ()

(* The attribute that marks instances *)
irreducible
let tcinstance : unit = ()

(* The attribute that marks class fields
   to signal that no method should be generated for them *)
irreducible
let no_method : unit = ()

private
let rec first (f : 'a -> Tac 'b) (l : list 'a) : Tac 'b =
    match l with
    | [] -> fail "no cands"
    | x::xs -> (fun () -> f x) `or_else` (fun () -> first f xs)

(* TODO: memoization?. And better errors. *)
private
let rec tcresolve' (seen:list term) (fuel:int) : Tac unit =
    if fuel <= 0 then
        fail "out of fuel";
    debug ("fuel = " ^ string_of_int fuel);
    let g = cur_goal () in
    if L.existsb (term_eq g) seen then
      fail "loop";
    let seen = g :: seen in
    local seen fuel `or_else` (fun () -> global seen fuel `or_else` (fun () -> fail ("could not solve constraint: " ^ term_to_string g)))
and local (seen:list term) (fuel:int) () : Tac unit =
    let bs = vars_of_env (cur_env ()) in
    first (fun (b:binding) -> trywith seen fuel (pack (Tv_Var b))) bs
and global (seen:list term) (fuel:int) () : Tac unit =
    let cands = lookup_attr (`tcinstance) (cur_env ()) in
    first (fun fv -> trywith seen fuel (pack (Tv_FVar fv))) cands
and trywith (seen:list term) (fuel:int) (t:term) : Tac unit =
    debug ("Trying to apply hypothesis/instance: " ^ term_to_string t);
    (fun () -> apply_noinst t) `seq` (fun () -> tcresolve' seen (fuel-1))

private
let rec maybe_intros () : Tac unit =
  let g = cur_goal () in
  match inspect_ln g with
  | Reflection.V2.Tv_Arrow _ _ ->
    ignore (intro ());
    maybe_intros ()
  | _ -> ()

[@@plugin]
let tcresolve () : Tac unit =
    //we sometimes get goal type as _ -> t
    //so intro if that's the case
    //not using intros () directly, since that unfolds aggressively if the term is not an arrow
    maybe_intros ();
    try tcresolve' [] 16
    with
    | TacticFailure s -> fail ("Typeclass resolution failed: " ^ s)
    | 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 has_no_method_attr (b:binder)
      : bool
      = let attrs = b.attrs in
        let is_no_method (t:term)
          : bool
          = match inspect_ln t with
            | Reflection.V2.Tv_FVar fv  ->
              let n = flatten_name (inspect_fv fv) in
              n = `%no_method
            | _ -> false
        in
        L.existsb is_no_method attrs
    in
    L.filter (fun b -> not (has_no_method_attr b)) bs

private
let binder_set_meta (b : binder) (t : term) : binder =
  { b with qual = Q_Meta t }
val mk_class (nm:string) : Tac decls
nm: Prims.string -> FStar.Tactics.Effect.Tac FStar.Reflection.Types.decls