val lift_div_tac_wp (#a: Type) (wp: pure_wp a) : tac_wp_t a
let lift_div_tac_wp (#a:Type) (wp:pure_wp a) : tac_wp_t a =
  elim_pure_wp_monotonicity wp;  
  fun ps p -> wp (fun x -> p (Success x ps))
val lift_div_tac_wp (#a: Type) (wp: pure_wp a) : tac_wp_t a
let lift_div_tac_wp (#a: Type) (wp: pure_wp a) : tac_wp_t a =
elim_pure_wp_monotonicity wp;
fun ps p -> wp (fun x -> p (Success x ps))
FStar.Tactics.Effect.fsti.checked
prims.fst.checked FStar.Tactics.Types.fsti.checked FStar.Tactics.Result.fsti.checked FStar.Reflection.Types.fsti.checked FStar.Range.fsti.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Pure.fst.checked
FStar.Tactics.Effect.fsti
Prims.pure_wp FStar.Tactics.Types.proofstate FStar.Tactics.Result.__result Prims.l_True FStar.Tactics.Result.Success Prims.pure_pre Prims.unit FStar.Monotonic.Pure.elim_pure_wp_monotonicity FStar.Tactics.Effect.tac_wp_t
(*
   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.Effect

open FStar.Monotonic.Pure

open FStar.Reflection.Types
open FStar.Tactics.Types
open FStar.Tactics.Result

(* This module is extracted, don't add any `assume val`s or extraction
 * will break. (`synth_by_tactic` is fine) *)

type tac_wp_t0 (a:Type) =
  proofstate -> (__result a -> Type0) -> Type0

unfold
let tac_wp_monotonic (#a:Type) (wp:tac_wp_t0 a) =
  forall (ps:proofstate) (p q:__result a -> Type0).
    (forall x. p x ==> q x) ==> (wp ps p ==> wp ps q)

type tac_wp_t (a:Type) = wp:tac_wp_t0 a{tac_wp_monotonic wp}

let tac_repr (a:Type) (wp:tac_wp_t a) =
  ps0:proofstate -> DIV (__result a) (as_pure_wp (wp ps0))

unfold
let tac_return_wp (#a:Type) (x:a) : tac_wp_t a =
  fun ps post -> post (Success x ps)

(* monadic return *)
let tac_return (a:Type) (x:a) : tac_repr a (tac_return_wp x) =
  fun (s:proofstate) -> Success x s

unfold
let tac_bind_wp (#a #b:Type) (wp_f:tac_wp_t a) (wp_g:a -> tac_wp_t b) : tac_wp_t b =
  fun ps post ->
  wp_f ps (fun r ->
           match r with
           | Success x ps -> wp_g x ps post
           | Failed ex ps -> post (Failed ex ps))

/// An optimization to name the continuation

unfold
let tac_wp_compact (a:Type) (wp:tac_wp_t a) : tac_wp_t a =
  fun ps post ->
  forall (k:__result a -> Type0). (forall (r:__result a).{:pattern (guard_free (k r))} post r ==> k r) ==> wp ps k


/// tac_bind_interleave_begin is an ugly hack to get interface interleaving
/// work with admit_smt_queries true for the bind combinator

val tac_bind_interleave_begin : unit


/// We cannot verify the bind combinator, since the body of bind
///   does some operations on the proof state, with which we cannot prove
///   that the proofstate is sequenced. Two ways to fix it:
///
/// 1. We separate the "meta" proofstate s.t. range, depth, etc. from the main
///    proofstate, and then sequencing only applies to the main proofstate
///
/// 2. The pre and post of the TAC effect are just exception pre and post,
///    since we can't prove much about the proofstate anyway, as it is
///    mostly abstract

(* monadic bind *)
#push-options "--admit_smt_queries true"
let tac_bind (a:Type) (b:Type)
  (wp_f:tac_wp_t a)
  (wp_g:a -> tac_wp_t b)
  (r1 r2:range)
  (t1:tac_repr a wp_f)
  (t2:(x:a -> tac_repr b (wp_g x))) : tac_repr b (tac_wp_compact b (tac_bind_wp wp_f wp_g)) =
  fun ps ->
  let ps = set_proofstate_range ps r1 in
  let ps = incr_depth ps in
  let r = t1 ps in
  match r with
  | Success a ps' ->
    let ps' = set_proofstate_range ps' r2 in
    // Force evaluation of __tracepoint q even on the interpreter
    begin match tracepoint ps' with
          | true -> t2 a (decr_depth ps')
    end
  | Failed e ps' -> Failed e ps'
#pop-options


/// tac_bind_interleave_end is an ugly hack to get interface interleaving
/// work with admit_smt_queries true for the bind combinator

val tac_bind_interleave_end : unit

unfold
let tac_if_then_else_wp (#a:Type) (wp_then:tac_wp_t a) (wp_else:tac_wp_t a) (b:bool)
  : tac_wp_t a
  = fun ps post -> (b ==> wp_then ps post) /\
                ((~ b) ==> wp_else ps post)

let tac_if_then_else (a:Type)
  (wp_then:tac_wp_t a)
  (wp_else:tac_wp_t a)
  (f:tac_repr a wp_then)
  (g:tac_repr a wp_else)
  (b:bool)
  : Type
  = tac_repr a (tac_wp_compact a (tac_if_then_else_wp wp_then wp_else b))

let tac_subcomp (a:Type)
  (wp_f:tac_wp_t a)
  (wp_g:tac_wp_t a)
  (f:tac_repr a wp_f)
  : Pure (tac_repr a wp_g)
         (requires forall ps p. wp_g ps p ==> wp_f ps p)
         (ensures fun _ -> True)
  = f

let tac_close (a b:Type)
  (wp_f:b -> tac_wp_t a)
  (f:(x:b -> tac_repr a (wp_f x))) =

  tac_repr a (fun ps post -> forall (x:b). wp_f x ps post)

/// default effect is Tac : meaning, unannotated TAC functions will be
///                         typed as Tac a
///
/// And the bind combinator has range arguments
///   that will be provided when the effect is reified

[@@ default_effect "FStar.Tactics.Effect.Tac"; bind_has_range_args]
reflectable
effect {
  TAC (a:Type) (wp:tac_wp_t a)
  with { repr=tac_repr;
         return=tac_return;
         bind=tac_bind;
         if_then_else=tac_if_then_else;
         subcomp=tac_subcomp;
         close = tac_close }
}

(* Hoare variant *)
effect TacH (a:Type) (pre : proofstate -> Tot Type0) (post : proofstate -> __result a -> Tot Type0) =
    TAC a (fun ps post' -> pre ps /\ (forall r. post ps r ==> post' r))

(* "Total" variant *)
effect Tac (a:Type) = TacH a (requires (fun _ -> True)) (ensures (fun _ _ -> True))

(* Metaprograms that succeed *)
effect TacS (a:Type) = TacH a (requires (fun _ -> True)) (ensures (fun _ps r -> Success? r))

(* A variant that doesn't prove totality (nor type safety!) *)
effect TacF (a:Type) = TacH a (requires (fun _ -> False)) (ensures (fun _ _ -> True))

unfold
val lift_div_tac_wp (#a: Type) (wp: pure_wp a) : tac_wp_t a
wp: Prims.pure_wp a -> FStar.Tactics.Effect.tac_wp_t a