val eligible_for_smt_equality (g: env) (t0 t1: term) : T.Tac bool
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 ()
val eligible_for_smt_equality (g: env) (t0 t1: term) : T.Tac bool
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 (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 ()
                  in
                  aux args0 args1 fallbacks))
        | _ -> either_equational ())
    else either_equational ())
| _ -> either_equational ()
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.Typing.Env.env Pulse.Syntax.Base.term FStar.Pervasives.Native.Mktuple2 Pulse.Syntax.Base.term' Pulse.Syntax.Base.__proj__Mkterm__item__t Pulse.Syntax.Base.host_term FStar.Reflection.Types.term Prims.list FStar.Reflection.V2.Data.argv Prims.op_AmpAmp FStar.Reflection.V2.TermEq.term_eq Prims.op_Equality Prims.nat FStar.List.Tot.Base.length FStar.Reflection.V2.Builtins.inspect_ln FStar.Reflection.Types.fv FStar.Reflection.Types.binder FStar.Reflection.Types.comp Prims.bool Prims.op_Negation FStar.Pervasives.Native.tuple2 FStar.Reflection.V2.Data.aqualv FStar.Pervasives.Native.Mktuple3 FStar.Pervasives.Native.tuple3 FStar.List.Tot.Base.fold_right Prims.Cons Prims.Nil FStar.List.Tot.Base.existsb Pulse.Checker.Prover.Match.is_smt_fallback FStar.Reflection.V2.Data.__proj__Mkbinder_view__item__attrs FStar.Reflection.V2.Data.binder_view Prims.precedes FStar.Reflection.V2.Builtins.inspect_binder FStar.Reflection.V2.Derived.collect_arr_ln_bs FStar.Pervasives.Native.option Pulse.Checker.Prover.Match.type_of_fv FStar.Reflection.V2.Data.universes FStar.Reflection.V2.Data.term_view FStar.Reflection.V2.Derived.collect_app_ln Prims.unit Prims.op_BarBar Pulse.Checker.Prover.Match.equational
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)
val eligible_for_smt_equality (g: env) (t0 t1: term) : T.Tac bool
g: Pulse.Typing.Env.env -> t0: Pulse.Syntax.Base.term -> t1: Pulse.Syntax.Base.term
  -> FStar.Tactics.Effect.Tac Prims.bool