val term_as_formula' (t: term) : Tac formula
let term_as_formula' (t:term) : Tac formula =
    match inspect_unascribe t with
    | Tv_Var n ->
        Name n

    | Tv_FVar fv
    | Tv_UInst fv _ ->
        // Cannot use `when` clauses when verifying!
        let qn = inspect_fv fv in
        if qn = true_qn then True_
        else if qn = false_qn then False_
        else FV fv

    // TODO: l_Forall
    // ...or should we just try to drop all squashes?
    // TODO: b2t at this point ?
    | Tv_App h0 t -> begin
        let (h, ts) = collect_app h0 in
        let h = un_uinst h in
        match inspect h, ts@[t] with
        | Tv_FVar fv, [(a1, Q_Implicit); (a2, Q_Explicit); (a3, Q_Explicit)] ->
            let qn = inspect_fv fv in
            if      qn = eq2_qn then Comp (Eq     (Some a1)) a2 a3
            else if qn = eq1_qn then Comp (BoolEq (Some a1)) a2 a3
            else if qn = lt_qn  then Comp Lt a2 a3
            else if qn = lte_qn then Comp Le a2 a3
            else if qn = gt_qn  then Comp Gt a2 a3
            else if qn = gte_qn then Comp Ge a2 a3
            else App h0 (fst t)
        | Tv_FVar fv, [(a1, Q_Explicit); (a2, Q_Explicit)] ->
            let qn = inspect_fv fv in
            if qn = imp_qn then Implies a1 a2
            else if qn = and_qn then And a1 a2
            else if qn = iff_qn then Iff a1 a2
            else if qn = or_qn  then Or a1 a2
            // Non-annotated comparisons
            else if qn = eq2_qn then Comp (Eq     None) a1 a2
            else if qn = eq1_qn then Comp (BoolEq None) a1 a2
            else App h0 (fst t)

        | Tv_FVar fv, [(a1, Q_Implicit); (a2, Q_Explicit)] ->
            let qn = inspect_fv fv in
                 if qn = forall_qn then mk_Forall a1 a2
            else if qn = exists_qn then mk_Exists a1 a2
            else App h0 (fst t)
        | Tv_FVar fv, [(a, Q_Explicit)] ->
            let qn = inspect_fv fv in
            if qn = not_qn then Not a
            else if qn = b2t_qn then begin
              if term_eq a (`false) then False_
              else if term_eq a (`true) then True_
              else App h0 (fst t)
            end
            else App h0 (fst t)
        | _ ->
            App h0 (fst t)
        end

    | Tv_Const (C_Int i) ->
        IntLit i

    (* Not formulas. *)
    | Tv_Let _ _ _ _ _
    | Tv_Match _ _ _
    | Tv_Type _
    | Tv_Abs _ _
    | Tv_Arrow _ _
    | Tv_Uvar _ _
    | Tv_Unknown
    | Tv_Unsupp
    | Tv_Refine _ _ -> F_Unknown

    (* Other constants? *)
    | Tv_Const _ -> F_Unknown

    (* Should not occur, we're using inspect *)
    | Tv_BVar _ -> F_Unknown
    | _ -> raise (TacticFailure "???")
val term_as_formula' (t: term) : Tac formula
let term_as_formula' (t: term) : Tac formula =
match inspect_unascribe t with
| Tv_Var n -> Name n
| Tv_FVar fv
| Tv_UInst fv _ ->
  let qn = inspect_fv fv in
  if qn = true_qn then True_ else if qn = false_qn then False_ else FV fv
| Tv_App h0 t ->
  let h, ts = collect_app h0 in
  let h = un_uinst h in
  (match inspect h, ts @ [t] with
    | Tv_FVar fv, [a1, Q_Implicit ; a2, Q_Explicit ; a3, Q_Explicit] ->
      let qn = inspect_fv fv in
      if qn = eq2_qn
      then Comp (Eq (Some a1)) a2 a3
      else
        if qn = eq1_qn
        then Comp (BoolEq (Some a1)) a2 a3
        else
          if qn = lt_qn
          then Comp Lt a2 a3
          else
            if qn = lte_qn
            then Comp Le a2 a3
            else
              if qn = gt_qn
              then Comp Gt a2 a3
              else if qn = gte_qn then Comp Ge a2 a3 else App h0 (fst t)
    | Tv_FVar fv, [a1, Q_Explicit ; a2, Q_Explicit] ->
      let qn = inspect_fv fv in
      if qn = imp_qn
      then Implies a1 a2
      else
        if qn = and_qn
        then And a1 a2
        else
          if qn = iff_qn
          then Iff a1 a2
          else
            if qn = or_qn
            then Or a1 a2
            else
              if qn = eq2_qn
              then Comp (Eq None) a1 a2
              else if qn = eq1_qn then Comp (BoolEq None) a1 a2 else App h0 (fst t)
    | Tv_FVar fv, [a1, Q_Implicit ; a2, Q_Explicit] ->
      let qn = inspect_fv fv in
      if qn = forall_qn
      then mk_Forall a1 a2
      else if qn = exists_qn then mk_Exists a1 a2 else App h0 (fst t)
    | Tv_FVar fv, [a, Q_Explicit] ->
      let qn = inspect_fv fv in
      if qn = not_qn
      then Not a
      else
        if qn = b2t_qn
        then
          if term_eq a (`false) then False_ else if term_eq a (`true) then True_ else App h0 (fst t)
        else App h0 (fst t)
    | _ -> App h0 (fst t))
| Tv_Const (C_Int i) -> IntLit i
| Tv_Let _ _ _ _ _
| Tv_Match _ _ _
| Tv_Type _
| Tv_Abs _ _
| Tv_Arrow _ _
| Tv_Uvar _ _
| Tv_Unknown
| Tv_Unsupp
| Tv_Refine _ _ -> F_Unknown
| Tv_Const _ -> F_Unknown
| Tv_BVar _ -> F_Unknown
| _ -> raise (TacticFailure "???")
FStar.Reflection.V2.Formula.fst.checked
prims.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.Common.fsti.checked FStar.Reflection.V2.Derived.fst.checked FStar.Reflection.V2.Data.fsti.checked FStar.Reflection.V2.Builtins.fsti.checked FStar.Reflection.Types.fsti.checked FStar.Reflection.Const.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked
FStar.Reflection.V2.Formula.fst
FStar.Tactics.NamedView.term FStar.Tactics.NamedView.namedv FStar.Reflection.V2.Formula.Name FStar.Reflection.V2.Formula.formula FStar.Reflection.Types.fv Prims.op_Equality Prims.list Prims.string FStar.Reflection.Const.true_qn FStar.Reflection.V2.Formula.True_ Prims.bool FStar.Reflection.Const.false_qn FStar.Reflection.V2.Formula.False_ FStar.Reflection.V2.Formula.FV FStar.Reflection.Types.name FStar.Reflection.V2.Builtins.inspect_fv FStar.Reflection.V2.Data.universes FStar.Reflection.V2.Data.argv FStar.Reflection.Types.term FStar.Reflection.Const.eq2_qn FStar.Reflection.V2.Formula.Comp FStar.Reflection.V2.Formula.Eq FStar.Pervasives.Native.Some FStar.Reflection.Types.typ FStar.Reflection.Const.eq1_qn FStar.Reflection.V2.Formula.BoolEq FStar.Reflection.Const.lt_qn FStar.Reflection.V2.Formula.Lt FStar.Reflection.Const.lte_qn FStar.Reflection.V2.Formula.Le FStar.Reflection.Const.gt_qn FStar.Reflection.V2.Formula.Gt FStar.Reflection.Const.gte_qn FStar.Reflection.V2.Formula.Ge FStar.Reflection.V2.Formula.App FStar.Pervasives.Native.fst FStar.Reflection.V2.Data.aqualv FStar.Reflection.Const.imp_qn FStar.Reflection.V2.Formula.Implies FStar.Reflection.Const.and_qn FStar.Reflection.V2.Formula.And FStar.Reflection.Const.iff_qn FStar.Reflection.V2.Formula.Iff FStar.Reflection.Const.or_qn FStar.Reflection.V2.Formula.Or FStar.Pervasives.Native.None FStar.Reflection.Const.forall_qn FStar.Reflection.V2.Formula.mk_Forall FStar.Reflection.Const.exists_qn FStar.Reflection.V2.Formula.mk_Exists FStar.Reflection.Const.not_qn FStar.Reflection.V2.Formula.Not FStar.Reflection.Const.b2t_qn FStar.Reflection.V2.Builtins.term_eq FStar.Pervasives.Native.tuple2 FStar.Tactics.NamedView.named_term_view FStar.Pervasives.Native.Mktuple2 FStar.List.Tot.Base.op_At Prims.Cons Prims.Nil FStar.Tactics.NamedView.inspect FStar.Reflection.V2.Derived.un_uinst FStar.Reflection.V2.Formula.collect_app Prims.int FStar.Reflection.V2.Formula.IntLit FStar.Tactics.NamedView.simple_binder FStar.Reflection.V2.Formula.F_Unknown FStar.Pervasives.Native.option FStar.Tactics.NamedView.match_returns_ascription FStar.Tactics.NamedView.branch FStar.Tactics.NamedView.universe FStar.Tactics.NamedView.binder FStar.Tactics.NamedView.comp Prims.nat FStar.Reflection.Types.ctx_uvar_and_subst FStar.Reflection.V2.Data.vconst FStar.Tactics.NamedView.bv FStar.Tactics.Effect.raise FStar.Tactics.Common.TacticFailure FStar.Tactics.NamedView.term_view FStar.Reflection.V2.Formula.inspect_unascribe
(*
   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.Reflection.V2.Formula

open FStar.List.Tot.Base

open FStar.Reflection.Types
open FStar.Reflection.Const
open FStar.Reflection.V2.Builtins
open FStar.Reflection.V2.Derived
open FStar.Reflection.V2.Data

open FStar.Tactics.Common
open FStar.Tactics.Effect
open FStar.Tactics.V2.Builtins
open FStar.Tactics.NamedView

///// Helpers (we cannot use the ones in Tactics.V2.Derived, those are for named views /////
private let rec inspect_unascribe (t:term) : Tac term_view =
  match inspect t with
  | Tv_AscribedT t _ _ _
  | Tv_AscribedC t _ _ _ ->
    inspect_unascribe t
  | tv -> tv

private let rec collect_app' (args : list argv) (t : term)
  : Tac (term * list argv) (decreases t) =
    match inspect_unascribe t with
    | Tv_App l r ->
        collect_app' (r::args) l
    | _ -> (t, args)

private let collect_app = collect_app' []
/////

[@@plugin]
noeq type comparison =
  | Eq     of option typ  (* Propositional equality (eq2), maybe annotated *)
  | BoolEq of option typ  (* Decidable, boolean equality (eq), maybe annotated *)
  | Lt | Le | Gt | Ge     (* Orderings, at type `int` (and subtypes) *)

[@@plugin]
noeq type formula =
  | True_  : formula
  | False_ : formula
  | Comp   : comparison -> term -> term -> formula
  | And    : term -> term -> formula
  | Or     : term -> term -> formula
  | Not    : term -> formula
  | Implies: term -> term -> formula
  | Iff    : term -> term -> formula
  | Forall : bv -> typ -> term -> formula
  | Exists : bv -> typ -> term -> formula
  | App    : term -> term -> formula
  | Name   : namedv -> formula
  | FV     : fv -> formula
  | IntLit : int -> formula
  | F_Unknown : formula // Also a baked-in "None"

let mk_Forall (typ : term) (pred : term) : Tot formula =
    let b = pack_bv ({ ppname = as_ppname "x";
                       sort = seal typ;
                       index = 0; }) in
    Forall b typ (pack (Tv_App pred (pack (Tv_BVar b), Q_Explicit)))

let mk_Exists (typ : term) (pred : term) : Tot formula =
    let b = pack_bv ({ ppname = as_ppname "x";
                       sort = seal typ;
                       index = 0; }) in
    Exists b typ (pack (Tv_App pred (pack (Tv_BVar b), Q_Explicit)))

[@@plugin]
val term_as_formula' (t: term) : Tac formula
t: FStar.Tactics.NamedView.term -> FStar.Tactics.Effect.Tac FStar.Reflection.V2.Formula.formula