val binder_set_meta (b: binder) (t: term) : binder
let binder_set_meta (b : binder) (t : term) : binder =
  { b with qual = Q_Meta t }
val binder_set_meta (b: binder) (t: term) : binder
let binder_set_meta (b: binder) (t: term) : binder =
{ b with qual = Q_Meta t }
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
FStar.Tactics.NamedView.binder FStar.Tactics.NamedView.term FStar.Tactics.NamedView.Mkbinder FStar.Tactics.NamedView.__proj__Mkbinder__item__uniq FStar.Tactics.NamedView.__proj__Mkbinder__item__ppname FStar.Tactics.NamedView.__proj__Mkbinder__item__sort FStar.Reflection.V2.Data.Q_Meta FStar.Tactics.NamedView.__proj__Mkbinder__item__attrs
(*
   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
val binder_set_meta (b: binder) (t: term) : binder
b: FStar.Tactics.NamedView.binder -> t: FStar.Tactics.NamedView.term
  -> FStar.Tactics.NamedView.binder