val is_reveal (t: term) : bool
let is_reveal (t:term) : bool =
  match leftmost_head t with
  | Some hd ->
    (match is_fvar hd with
     | Some (l, [_]) -> l = RUtil.reveal_lid
     | _ -> false)
  | _ -> false
val is_reveal (t: term) : bool
let is_reveal (t: term) : bool =
match leftmost_head t with
| Some hd ->
  (match is_fvar hd with
    | Some (l, [_]) -> l = RUtil.reveal_lid
    | _ -> false)
| _ -> false
Pulse.Checker.Prover.Match.fst.checked
Pulse.Typing.Util.fsti.checked Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Checker.VPropEquiv.fsti.checked Pulse.Checker.Prover.Util.fsti.checked Pulse.Checker.Prover.Substs.fsti.checked Pulse.Checker.Prover.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.Prover.Match.fst
Pulse.Syntax.Base.term Pulse.Syntax.Pure.leftmost_head Pulse.Syntax.Pure.is_fvar FStar.Reflection.Types.name Pulse.Syntax.Base.universe Prims.op_Equality Prims.list Prims.string Pulse.Reflection.Util.reveal_lid FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 Prims.bool
module Pulse.Checker.Prover.Match

open Pulse.Syntax
open Pulse.Typing
open Pulse.Typing.Combinators
open Pulse.Typing.Metatheory
open Pulse.Typing.Util
open Pulse.Checker.VPropEquiv
open Pulse.Checker.Prover.Base
open Pulse.Checker.Prover.Util

module L = FStar.List.Tot
module R = FStar.Reflection.V2
module TermEq = FStar.Reflection.V2.TermEq
module T = FStar.Tactics.V2

module RUtil = Pulse.Reflection.Util
module P = Pulse.Syntax.Printer
module PS = Pulse.Checker.Prover.Substs

let equational (t:term) : bool =
  match t.t with
  | Tm_FStar host_term ->
    (match R.inspect_ln host_term with
     | R.Tv_Match _ _ _ -> true
     | _ -> false)
  | _ -> false

let type_of_fv (g:env) (fv:R.fv)
  : T.Tac (option R.term)
  = let n = R.inspect_fv fv in
    match R.lookup_typ (fstar_env g) n with
    | None -> None
    | Some se ->
      match R.inspect_sigelt se with
      | R.Unk -> None
      | R.Sg_Let _ lbs -> (
        L.tryPick
          (fun lb -> 
            let lbv = R.inspect_lb lb in
            if R.inspect_fv lbv.lb_fv = n
            then Some lbv.lb_typ
            else None)
          lbs
      )
      | R.Sg_Val _ _ t -> Some t
      | R.Sg_Inductive _nm _univs params typ _ -> None

let is_smt_fallback (t:R.term) : bool =
  match R.inspect_ln t with
  | R.Tv_FVar fv ->
    let name = R.inspect_fv fv in
    name = ["Steel";"Effect";"Common";"smt_fallback"]
  | _ -> false

(*
  When comparing t0 =?= t1, if they are not syntactically equal, we
  have to decide whether or not we should fire an SMT query to compare
  them for provable equality.

  The criterion is as follows:

  1. We allow an SMT query if either t0 or t1 is "equational". For now, that means
     that either is a match expression.

  2. Otherwise, if they are both applications of `f v0...vn` and `f u0...un`
     of the same head symbol `f`, a top-level constant, then we check if the
     type of `f` decorates any of its binders with the `smt_fallback` attribute. 

        - If none of them are marked as such,
          then we check if `f v0...` is syntactically equal to `f u0...`
          and allow an SMT query to check if vn = vm. That is, the default behavior
          for predicates is that they *last* argument is eligible for SMT equality.

        - Otherwise, for each binder that is NOT marked as `smt_fallback`, we check
          if the corresponding argument is syntactically equal. If so, we allow 
          t0 and t1 to be compared for SMT equality.

          For example, Steel.ST.Reference.pts_to is defined like so:

            /// For instance, [pts_to r (sum_perm (half_perm p) (half_perm p)) (v + 1)]
            /// is unifiable with [pts_to r p (1 + v)]
            val pts_to (#a:Type0)
                      (r:ref a)
                      ([@@@smt_fallback] p:perm)
                      ([@@@smt_fallback] v:a)
              : vprop
*)
let eligible_for_smt_equality (g:env) (t0 t1:term) 
  : T.Tac bool
  = let either_equational () = equational t0 || equational t1 in
    let head_eq (t0 t1:R.term) =
      match R.inspect_ln t0, R.inspect_ln t1 with
      | R.Tv_App h0 _, R.Tv_App h1 _ ->
        TermEq.term_eq h0 h1
      | _ -> false
    in
    match t0.t, t1.t with
    | Tm_FStar t0, Tm_FStar t1 -> (
      let h0, args0 = R.collect_app_ln t0 in
      let h1, args1 = R.collect_app_ln t1 in
      if TermEq.term_eq h0 h1 && L.length args0 = L.length args1
      then (
        match R.inspect_ln h0 with
        | R.Tv_FVar fv
        | R.Tv_UInst fv _ -> (
          match type_of_fv g fv with
          | None -> either_equational()
          | Some t ->
            let bs, _ = R.collect_arr_ln_bs t in
            let is_smt_fallback (b:R.binder) = 
                let bview = R.inspect_binder b in
                L.existsb is_smt_fallback bview.attrs
            in
            let some_fallbacks, fallbacks =
              L.fold_right
                (fun b (some_fallbacks, bs) -> 
                  if is_smt_fallback b
                  then true, true::bs
                  else some_fallbacks, false::bs)
                bs (false, [])
            in
            if not some_fallbacks
            then (
                //if none of the binders are marked fallback
                //then, by default, consider only the last argument as
                //fallback
              head_eq t0 t1
            )
            else (
              let rec aux args0 args1 fallbacks =
                match args0, args1, fallbacks with
                | (a0, _)::args0, (a1, _)::args1, b::fallbacks -> 
                  if b
                  then aux args0 args1 fallbacks
                  else if not (TermEq.term_eq a0 a1)
                  then false
                  else aux args0 args1 fallbacks
                | [], [], [] -> true
                | _ -> either_equational() //unequal lengths
              in
              aux args0 args1 fallbacks
            )
        ) 
        | _ -> either_equational ()
      )
      else either_equational ()
    )
    | _ -> either_equational ()


let refl_uvar (t:R.term) (uvs:env) : option var =
  let open R in
  match inspect_ln t with
  | Tv_Var v ->
    let {uniq=n} = inspect_namedv v in
    if contains uvs n then Some n else None
  | _ -> None

let is_uvar (t:term) (uvs:env) : option var =
  match t.t with
  | Tm_FStar t -> refl_uvar t uvs
  | _ -> None

let contains_uvar (t:term) (uvs:env) (g:env) : T.Tac bool =
  not (check_disjoint uvs (freevars t))

let is_reveal_uvar (t:term) (uvs:env) : option (universe & term & var) =
  match is_pure_app t with
  | Some (hd, None, arg) ->
    (match is_pure_app hd with
     | Some (hd, Some Implicit, ty) ->
       let arg_uvar_index_opt = is_uvar arg uvs in
       (match arg_uvar_index_opt with
        | Some n ->
          (match is_fvar hd with
           | Some (l, [u]) ->
             if l = RUtil.reveal_lid
             then Some (u, ty, n)
             else None
           | _ -> None)
        | _ -> None)
     | _ -> None)
  | _ -> None
val is_reveal (t: term) : bool
t: Pulse.Syntax.Base.term -> Prims.bool