val check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_While? t.term})
  (check:check_t)
  : T.Tac (checker_result_t g pre post_hint)
let check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_While? t.term})
  (check:check_t)
  : T.Tac (checker_result_t g pre post_hint) =

  let g = push_context "while loop" t.range g in
  let Tm_While { invariant=inv; condition=cond; body; condition_var } = t.term in
  let (| ex_inv, inv_typing |) =
    check_vprop (push_context "invariant" (term_range inv) g) 
                (tm_exists_sl u0 { binder_ppname=condition_var; binder_ty=tm_bool } inv)
  in

  if not (Tm_ExistsSL? ex_inv.t)
  then fail g (Some t.range)
         (Printf.sprintf "check_while: typechecked invariant %s is not an existential"
            (P.term_to_string ex_inv));

  let Tm_ExistsSL u {binder_ppname=nm; binder_ty=ty} inv = ex_inv.t in

  if not (eq_tm ty tm_bool) ||
     not (eq_univ u u0)
  then fail g (Some nm.range)
         (Printf.sprintf "While loop invariant exists but its witness type is %s, expected bool"
            (P.term_to_string ty));

  let while_cond_comp_typing = while_cond_comp_typing u nm ty inv inv_typing in
  let (| res_typing, cond_pre_typing, x, post_typing |) =
    Metatheory.(st_comp_typing_inversion (comp_typing_inversion while_cond_comp_typing))
  in
  let while_cond_hint : post_hint_for_env g =
    post_hint_from_comp_typing while_cond_comp_typing
  in

  let (| cond, cond_comp, cond_typing |) =
    let ppname = mk_ppname_no_range "_while_c" in
    let r = check
      (push_context "check_while_condition" cond.range g)
      (comp_pre (comp_while_cond nm inv))
      cond_pre_typing
      (Some while_cond_hint)
      ppname
      cond in
    apply_checker_result_k r ppname
  in
  if eq_comp cond_comp (comp_while_cond nm inv)
  then begin
    let while_body_comp_typing = while_body_comp_typing u nm ty inv inv_typing in
    let (| res_typing, body_pre_typing, x, post_typing |) = 
      Metatheory.(st_comp_typing_inversion (comp_typing_inversion while_body_comp_typing))
    in
    let while_post_hint : post_hint_for_env g =
      post_hint_from_comp_typing while_body_comp_typing
    in
    let (| body, body_comp, body_typing |) =
      let ppname = mk_ppname_no_range "_while_b" in
      let r = check
        (push_context "check_while_body" body.range g)
        (comp_pre (comp_while_body nm inv))
        body_pre_typing
        (Some while_post_hint)
        ppname
        body in
      apply_checker_result_k r ppname in
    if eq_comp body_comp (comp_while_body nm inv)
    then
      let d = T_While g inv cond body inv_typing cond_typing body_typing in
      prove_post_hint (try_frame_pre pre_typing (match_comp_res_with_post_hint d post_hint) res_ppname) post_hint t.range
    else fail g None
          (Printf.sprintf "Could not prove the inferred type of the while body matches the annotation\n\
                           Inferred type = %s\n\
                           Annotated type = %s\n"
                           (P.comp_to_string body_comp)
                           (P.comp_to_string (comp_while_body nm inv)))
  end
  else fail g None
         (Printf.sprintf "Could not prove that the inferred type of the while condition matches the annotation\n\
                          Inferred type = %s\n\
                          Annotated type = %s\n"
                          (P.comp_to_string cond_comp)
                          (P.comp_to_string (comp_while_cond nm inv)))
val check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_While? t.term})
  (check:check_t)
  : T.Tac (checker_result_t g pre post_hint)
let check
      (g: env)
      (pre: term)
      (pre_typing: tot_typing g pre tm_vprop)
      (post_hint: post_hint_opt g)
      (res_ppname: ppname)
      (t: st_term{Tm_While? t.term})
      (check: check_t)
    : T.Tac (checker_result_t g pre post_hint) =
let g = push_context "while loop" t.range g in
let Tm_While { invariant = inv ; condition = cond ; body = body ; condition_var = condition_var } =
  t.term
in
let (| ex_inv , inv_typing |) =
  check_vprop (push_context "invariant" (term_range inv) g)
    (tm_exists_sl u0 ({ binder_ppname = condition_var; binder_ty = tm_bool }) inv)
in
if not (Tm_ExistsSL? ex_inv.t)
then
  fail g
    (Some t.range)
    (Printf.sprintf "check_while: typechecked invariant %s is not an existential"
        (P.term_to_string ex_inv));
let Tm_ExistsSL u { binder_ppname = nm ; binder_ty = ty } inv = ex_inv.t in
if not (eq_tm ty tm_bool) || not (eq_univ u u0)
then
  fail g
    (Some nm.range)
    (Printf.sprintf "While loop invariant exists but its witness type is %s, expected bool"
        (P.term_to_string ty));
let while_cond_comp_typing = while_cond_comp_typing u nm ty inv inv_typing in
let (| res_typing , cond_pre_typing , x , post_typing |) =
  let open Metatheory in st_comp_typing_inversion (comp_typing_inversion while_cond_comp_typing)
in
let while_cond_hint:post_hint_for_env g = post_hint_from_comp_typing while_cond_comp_typing in
let (| cond , cond_comp , cond_typing |) =
  let ppname = mk_ppname_no_range "_while_c" in
  let r =
    check (push_context "check_while_condition" cond.range g)
      (comp_pre (comp_while_cond nm inv))
      cond_pre_typing
      (Some while_cond_hint)
      ppname
      cond
  in
  apply_checker_result_k r ppname
in
if eq_comp cond_comp (comp_while_cond nm inv)
then
  let while_body_comp_typing = while_body_comp_typing u nm ty inv inv_typing in
  let (| res_typing , body_pre_typing , x , post_typing |) =
    let open Metatheory in st_comp_typing_inversion (comp_typing_inversion while_body_comp_typing)
  in
  let while_post_hint:post_hint_for_env g = post_hint_from_comp_typing while_body_comp_typing in
  let (| body , body_comp , body_typing |) =
    let ppname = mk_ppname_no_range "_while_b" in
    let r =
      check (push_context "check_while_body" body.range g)
        (comp_pre (comp_while_body nm inv))
        body_pre_typing
        (Some while_post_hint)
        ppname
        body
    in
    apply_checker_result_k r ppname
  in
  if eq_comp body_comp (comp_while_body nm inv)
  then
    let d = T_While g inv cond body inv_typing cond_typing body_typing in
    prove_post_hint (try_frame_pre pre_typing (match_comp_res_with_post_hint d post_hint) res_ppname
      )
      post_hint
      t.range
  else
    fail g
      None
      (Printf.sprintf "Could not prove the inferred type of the while body matches the annotation\nInferred type = %s\nAnnotated type = %s\n"
          (P.comp_to_string body_comp)
          (P.comp_to_string (comp_while_body nm inv)))
else
  fail g
    None
    (Printf.sprintf "Could not prove that the inferred type of the while condition matches the annotation\nInferred type = %s\nAnnotated type = %s\n"
        (P.comp_to_string cond_comp)
        (P.comp_to_string (comp_while_cond nm inv)))
Pulse.Checker.While.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.While.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.tot_typing Pulse.Syntax.Base.tm_vprop Pulse.Typing.post_hint_opt Pulse.Syntax.Base.ppname Pulse.Syntax.Base.st_term Prims.b2t Pulse.Syntax.Base.uu___is_Tm_While Pulse.Syntax.Base.__proj__Mkst_term__item__term Pulse.Checker.Base.check_t Pulse.Checker.Pure.push_context Pulse.Syntax.Base.term_range Pulse.Syntax.Base.universe Pulse.Typing.universe_of Pulse.Syntax.Base.__proj__Mkst_comp__item__res Pulse.Syntax.Base.st_comp_of_comp Pulse.Typing.comp_while_cond Pulse.Syntax.Base.__proj__Mkst_comp__item__u Pulse.Syntax.Base.__proj__Mkst_comp__item__pre Pulse.Syntax.Base.var Pulse.Typing.fresh_wrt Pulse.Syntax.Naming.freevars Pulse.Syntax.Base.__proj__Mkst_comp__item__post Pulse.Typing.Env.push_binding Pulse.Syntax.Base.ppname_default Pulse.Syntax.Naming.open_term Pulse.Syntax.Base.comp_st Prims.l_and Prims.eq2 Pulse.Syntax.Base.vprop Pulse.Syntax.Base.comp_pre Pulse.Typing.comp_post_matches_hint FStar.Pervasives.Native.Some Pulse.Typing.post_hint_t Pulse.Typing.st_typing Pulse.Syntax.Base.__proj__Mkst_term__item__range Pulse.Syntax.Base.eq_comp Pulse.Typing.comp_while_body Pulse.Checker.Prover.prove_post_hint Pulse.Checker.Base.checker_result_t FStar.Pervasives.Native.None Pulse.Checker.Prover.try_frame_pre FStar.Pervasives.dtuple3 Pulse.Checker.Base.match_comp_res_with_post_hint Pulse.Typing.wtag Pulse.Syntax.Base.ctag Pulse.Syntax.Base.STT Pulse.Syntax.Base.Tm_While Pulse.Syntax.Base.Mkst_term'__Tm_While__payload Pulse.Typing.comp_while Pulse.Typing.T_While Prims.bool Pulse.Typing.Env.fail Pulse.Syntax.Base.range Prims.string FStar.Printf.sprintf Pulse.Syntax.Printer.comp_to_string Pulse.Typing.Combinators.st_typing_in_ctxt Pulse.Checker.Base.apply_checker_result_k Pulse.Syntax.Base.mk_ppname_no_range Pulse.Typing.post_hint_for_env Pulse.Checker.Base.post_hint_from_comp_typing FStar.Pervasives.dtuple4 Pulse.Typing.Metatheory.Base.st_comp_typing_inversion Pulse.Typing.Metatheory.Base.comp_typing_inversion Pulse.Typing.Metatheory.Base.comp_typing_u Pulse.Checker.While.while_body_comp_typing Pulse.Checker.While.while_cond_comp_typing Prims.unit Prims.op_BarBar Prims.op_Negation Pulse.Syntax.Base.eq_tm Pulse.Typing.tm_bool Pulse.Syntax.Base.eq_univ Pulse.Syntax.Pure.u0 Pulse.Syntax.Base.__proj__Mkppname__item__range Pulse.Syntax.Printer.term_to_string Pulse.Syntax.Base.term' Pulse.Syntax.Base.__proj__Mkterm__item__t Pulse.Syntax.Base.uu___is_Tm_ExistsSL Prims.dtuple2 Pulse.Checker.Pure.check_vprop Pulse.Syntax.Base.tm_exists_sl Pulse.Syntax.Base.Mkbinder Pulse.Syntax.Base.st_term'
module Pulse.Checker.While

open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Pure
open Pulse.Checker.Base
open Pulse.Checker.Prover

module T = FStar.Tactics.V2
module P = Pulse.Syntax.Printer
module Metatheory = Pulse.Typing.Metatheory

let while_cond_comp_typing (#g:env) (u:universe) (x:ppname) (ty:term) (inv_body:term)
                           (inv_typing:tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_vprop)
  : Metatheory.comp_typing_u g (comp_while_cond x inv_body)
  = Metatheory.admit_comp_typing g (comp_while_cond x inv_body)

let while_body_comp_typing (#g:env) (u:universe) (x:ppname) (ty:term) (inv_body:term)
                           (inv_typing:tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_vprop)
  : Metatheory.comp_typing_u g (comp_while_body x inv_body)
  = Metatheory.admit_comp_typing g (comp_while_body x inv_body)

#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 4"
let check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_While? t.term})
val check
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_While? t.term})
  (check:check_t)
  : T.Tac (checker_result_t g pre post_hint)

    g: Pulse.Typing.Env.env ->
    pre: Pulse.Syntax.Base.term ->
    pre_typing: Pulse.Typing.tot_typing g pre Pulse.Syntax.Base.tm_vprop ->
    post_hint: Pulse.Typing.post_hint_opt g ->
    res_ppname: Pulse.Syntax.Base.ppname ->
    t: Pulse.Syntax.Base.st_term{Tm_While? (Mkst_term?.term t)} ->
    check: Pulse.Checker.Base.check_t
  -> FStar.Tactics.Effect.Tac (Pulse.Checker.Base.checker_result_t g pre post_hint)