val apply_noinst (t: term) : Tac unit
let apply_noinst (t : term) : Tac unit =
    t_apply true true false t
val apply_noinst (t: term) : Tac unit
let apply_noinst (t: term) : Tac unit =
t_apply true true false t
FStar.Tactics.V1.Derived.fst.checked
prims.fst.checked FStar.VConfig.fsti.checked FStar.Tactics.Visit.fst.checked FStar.Tactics.V1.SyntaxHelpers.fst.checked FStar.Tactics.V1.Builtins.fsti.checked FStar.Tactics.Util.fst.checked FStar.Tactics.Types.fsti.checked FStar.Tactics.Result.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Squash.fsti.checked FStar.Reflection.V1.Formula.fst.checked FStar.Reflection.V1.fst.checked FStar.Range.fsti.checked FStar.PropositionalExtensionality.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked
FStar.Tactics.V1.Derived.fst
FStar.Reflection.Types.term FStar.Tactics.V1.Builtins.t_apply Prims.unit
(*
   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.V1.Derived

open FStar.Reflection.V1
open FStar.Reflection.V1.Formula
open FStar.Tactics.Types
open FStar.Tactics.Effect
open FStar.Tactics.Result
open FStar.Tactics.Util
open FStar.Tactics.V1.Builtins
open FStar.Tactics.V1.SyntaxHelpers
open FStar.VConfig

module L = FStar.List.Tot.Base
module V = FStar.Tactics.Visit
private let (@) = L.op_At

let name_of_bv (bv : bv) : Tac string =
    unseal ((inspect_bv bv).bv_ppname)

let bv_to_string (bv : bv) : Tac string =
    (* Could also print type...? *)
    name_of_bv bv

let name_of_binder (b : binder) : Tac string =
    name_of_bv (bv_of_binder b)

let binder_to_string (b : binder) : Tac string =
    bv_to_string (bv_of_binder b) //TODO: print aqual, attributes

exception Goal_not_trivial

let goals () : Tac (list goal) = goals_of (get ())
let smt_goals () : Tac (list goal) = smt_goals_of (get ())

let fail (#a:Type) (m:string)
  : TAC a (fun ps post -> post (Failed (TacticFailure m) ps))
  = raise #a (TacticFailure m)

let fail_silently (#a:Type) (m:string)
  : TAC a (fun _ post -> forall ps. post (Failed (TacticFailure m) ps))
  = set_urgency 0;
    raise #a (TacticFailure m)

(** Return the current *goal*, not its type. (Ignores SMT goals) *)
let _cur_goal () : Tac goal =
    match goals () with
    | []   -> fail "no more goals"
    | g::_ -> g

(** [cur_env] returns the current goal's environment *)
let cur_env () : Tac env = goal_env (_cur_goal ())

(** [cur_goal] returns the current goal's type *)
let cur_goal () : Tac typ = goal_type (_cur_goal ())

(** [cur_witness] returns the current goal's witness *)
let cur_witness () : Tac term = goal_witness (_cur_goal ())

(** [cur_goal_safe] will always return the current goal, without failing.
It must be statically verified that there indeed is a goal in order to
call it. *)
let cur_goal_safe () : TacH goal (requires (fun ps -> ~(goals_of ps == [])))
                                 (ensures (fun ps0 r -> exists g. r == Success g ps0))
 = match goals_of (get ()) with
   | g :: _ -> g

(** [cur_binders] returns the list of binders in the current goal. *)
let cur_binders () : Tac binders =
    binders_of_env (cur_env ())

(** Set the guard policy only locally, without affecting calling code *)
let with_policy pol (f : unit -> Tac 'a) : Tac 'a =
    let old_pol = get_guard_policy () in
    set_guard_policy pol;
    let r = f () in
    set_guard_policy old_pol;
    r

(** [exact e] will solve a goal [Gamma |- w : t] if [e] has type exactly
[t] in [Gamma]. *)
let exact (t : term) : Tac unit =
    with_policy SMT (fun () -> t_exact true false t)

(** [exact_with_ref e] will solve a goal [Gamma |- w : t] if [e] has
type [t'] where [t'] is a subtype of [t] in [Gamma]. This is a more
flexible variant of [exact]. *)
let exact_with_ref (t : term) : Tac unit =
    with_policy SMT (fun () -> t_exact true true t)

let trivial () : Tac unit =
  norm [iota; zeta; reify_; delta; primops; simplify; unmeta];
  let g = cur_goal () in
  match term_as_formula g with
  | True_ -> exact (`())
  | _ -> raise Goal_not_trivial

(* Another hook to just run a tactic without goals, just by reusing `with_tactic` *)
let run_tactic (t:unit -> Tac unit)
  : Pure unit
         (requires (set_range_of (with_tactic (fun () -> trivial (); t ()) (squash True)) (range_of t)))
         (ensures (fun _ -> True))
  = ()

(** Ignore the current goal. If left unproven, this will fail after
the tactic finishes. *)
let dismiss () : Tac unit =
    match goals () with
    | [] -> fail "dismiss: no more goals"
    | _::gs -> set_goals gs

(** Flip the order of the first two goals. *)
let flip () : Tac unit =
    let gs = goals () in
    match goals () with
    | [] | [_]   -> fail "flip: less than two goals"
    | g1::g2::gs -> set_goals (g2::g1::gs)

(** Succeed if there are no more goals left, and fail otherwise. *)
let qed () : Tac unit =
    match goals () with
    | [] -> ()
    | _ -> fail "qed: not done!"

(** [debug str] is similar to [print str], but will only print the message
if the [--debug] option was given for the current module AND
[--debug_level Tac] is on. *)
let debug (m:string) : Tac unit =
    if debugging () then print m

(** [smt] will mark the current goal for being solved through the SMT.
This does not immediately run the SMT: it just dumps the goal in the
SMT bin. Note, if you dump a proof-relevant goal there, the engine will
later raise an error. *)
let smt () : Tac unit =
    match goals (), smt_goals () with
    | [], _ -> fail "smt: no active goals"
    | g::gs, gs' ->
        begin
        set_goals gs;
        set_smt_goals (g :: gs')
        end

let idtac () : Tac unit = ()

(** Push the current goal to the back. *)
let later () : Tac unit =
    match goals () with
    | g::gs -> set_goals (gs @ [g])
    | _ -> fail "later: no goals"

(** [apply f] will attempt to produce a solution to the goal by an application
of [f] to any amount of arguments (which need to be solved as further goals).
The amount of arguments introduced is the least such that [f a_i] unifies
with the goal's type. *)
let apply (t : term) : Tac unit =
    t_apply true false false t
val apply_noinst (t: term) : Tac unit
t: FStar.Reflection.Types.term -> FStar.Tactics.Effect.Tac Prims.unit