val coerce_eq: #a: Type -> #b: Type -> x: a -> squash (a == b) -> y: b{y == x}
let coerce_eq (#a #b:Type) (x:a) (_:squash (a == b)) : y:b{y == x} = x
val coerce_eq: #a: Type -> #b: Type -> x: a -> squash (a == b) -> y: b{y == x}
let coerce_eq (#a: Type) (#b: Type) (x: a) (_: squash (a == b)) : y: b{y == x} =
x
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
Prims.squash Prims.eq2
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

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

module RT = FStar.Reflection.Typing

let rec try_solve_uvars (g:env) (uvs:env { disjoint uvs g })
  (p q:term)
  : T.Tac (ss:PS.ss_t { PS.dom ss `Set.subset` freevars q }) =
  
  assume (Set.equal (PS.dom PS.empty) Set.empty);
  
  if not (contains_uvar q uvs g)
  then PS.empty
  else begin
    match is_reveal_uvar q uvs, is_reveal p with
    | Some (u, ty, n), false ->
      let w = mk_hide u ty p in
      assume (~ (PS.contains PS.empty n));
      let ss = PS.push PS.empty n w in
      assume (n `Set.mem` freevars q);
      assume (Set.equal (PS.dom ss) (Set.singleton n));
      ss
     | _ ->
       match is_uvar q uvs with
       | Some n ->
         let w = p in
         assume (~ (PS.contains PS.empty n));
         let ss = PS.push PS.empty n w in
         assume (n `Set.mem` freevars q);
         assume (Set.equal (PS.dom ss) (Set.singleton n));
         ss
       | _ ->
         match p.t, q.t with
         | Tm_Pure p1, Tm_Pure q1 -> try_solve_uvars g uvs p1 q1

         | _, _ ->
           match is_pure_app p, is_pure_app q with
           | Some (head_p, qual_p, arg_p), Some (head_q, qual_q, arg_q) ->
            let ss_head = try_solve_uvars g uvs head_p head_q in
            let ss_arg = try_solve_uvars g uvs arg_p arg_q in
            if PS.check_disjoint ss_head ss_arg  // TODO: should implement a better compose
            then begin
              let ss = PS.push_ss ss_head ss_arg in
              assume (Set.equal (PS.dom ss) (Set.union (PS.dom ss_head) (PS.dom ss_arg)));
              assume ((Set.union (freevars head_q) (freevars arg_q)) `Set.subset` freevars q);
              ss
            end
            else PS.empty
           | _, _ -> PS.empty
  end

let unify (g:env) (uvs:env { disjoint uvs g})
  (p q:term)
  : T.Tac (option (ss:PS.ss_t { PS.dom ss `Set.subset` freevars q } &
                   RT.equiv (elab_env g) (elab_term p) (elab_term ss.(q)))) =

  let ss = try_solve_uvars g uvs p q in
  let q = ss.(q) in
  if eq_tm p q
  then Some (| ss, RT.Rel_refl _ _ _ |)
  else if contains_uvar q uvs g
  then None
  else if eligible_for_smt_equality g p q
  then let v0 = elab_term p in
       let v1 = elab_term q in
       match check_equiv_now (elab_env g) v0 v1 with
       | Some token, _ -> Some (| ss, RT.Rel_eq_token _ _ _ (FStar.Squash.return_squash token) |)
       | None, _ -> None
  else None

let try_match_pq (g:env) (uvs:env { disjoint uvs g}) (p q:vprop)
  : T.Tac (option (ss:PS.ss_t { PS.dom ss `Set.subset` freevars q } &
                   vprop_equiv g p ss.(q))) =

  let r = unify g uvs p q in
  match r with
  | None -> None
  | Some (| ss, _ |) ->
    let ss : ss:PS.ss_t { PS.dom ss `Set.subset` freevars q } = ss in
    Some (| ss, magic () |)
val coerce_eq: #a: Type -> #b: Type -> x: a -> squash (a == b) -> y: b{y == x}
x: a -> _: Prims.squash (a == b) -> y: b{y == x}