val add_knot (g : env)  (rng : R.range)
             (d : decl)
: Tac decl
let add_knot (g : env) (rng : R.range)
             (d : decl{FnDecl? d.d})
: Tac decl
=
  let FnDecl { id; isrec; bs; comp; meas; body } = d.d in
  if Nil? bs then
    fail g (Some d.range) "main: FnDecl does not have binders";
  (* NB: bs and comp are open *)
  let r_res = elab_comp comp in
  let elab_b (qbv : option qualifier & binder & bv) : Tot Tactics.NamedView.binder =
    let q, b, bv = qbv in
    {
      uniq = bv.bv_index;
      ppname = b.binder_ppname.name;
      sort = elab_term b.binder_ty;
      qual = elab_qual q;
      attrs = [];
    }
  in
  debug_main g
    (fun _ -> Printf.sprintf "add_knot: bs = %s\n"
              (string_of_list (fun (_, b,_) -> P.binder_to_string b) bs));

  (* for
       fn rec f (x1:t1) ... (xn:tn) :
         requires pre
         returns x:a
         ensures post

    we elab into

       let  f (x1:t1) ... (xn:tn)
              (f : (x1':t1) -> ... -> (xn':tn) -> stt a pre post)
              : stt a pre post

    without any sort of termination check. Now, for

       ghost fn rec f (x1:t1) ... (xn:tn) :
         requires pre
         returns x:a
         ensures post
         measure meas

    we must elab into

       let  f (x1:t1) ... (xn:tn)
              (f : (x1':t1) -> ... -> (xn':tn){meas' << meas} -> stt a pre post)
              : stt a pre post

    so we need to add the measure refinement. Since `meas` is an
    open term (wrt x1...xn), we must substitute it to create meas',
    subtituting x1' for x1, ..., xn' for xn

  *)
  (* Desugaring added a recursive knot argument at the end *)
  let bs, b_knot = splitlast bs in
  (* freshen *)
  let r_bs0 = List.Tot.map elab_b bs in
  let freshen_binder (b:T.binder) : T.binder =
    { b with uniq = 10000 + b.uniq
           ; ppname = map_seal b.ppname (fun s -> s ^ "'") }
  in
  let r_bs = map freshen_binder r_bs0 in
  let binder_to_r_namedv (b:T.binder) : R.namedv =
    R.pack_namedv {
      uniq = b.uniq;
      sort = seal b.sort;
      ppname = b.ppname;
    }
  in
  let prime_subst = map2 (fun (b1 b2 : T.binder) ->
                      R.NT (binder_to_r_namedv b1)
                            (binder_to_term b2)) r_bs0 r_bs in
  let r_bs =
    (* If ghost/atomic, we need to add a decreases refinement on the last arg *)
    if C_STAtomic? comp || C_STGhost? comp then (
      if None? meas then (
        let open FStar.Stubs.Pprint in
        let open Pulse.PP in
        fail_doc g (Some d.range) [
          text "'ghost' and 'atomic' recursive functions require a 'decreases' clause"]
      );
      let init, last = splitlast r_bs in
      let last : FStar.Tactics.NamedView.binder = last in
      let last =
        (* add a refinement to last *)
        let b' : simple_binder = {
          uniq = last.uniq;
          ppname = last.ppname;
          sort = last.sort;
          qual = Q_Explicit;
          attrs = [];
        }
        in
        let meas = Some?.v meas in
        let meas = elab_term meas in
        let meas' = R.subst_term prime_subst meas in
        let ref = `(`#meas' << `#meas) in
        (* TODO: this is not always printed *)
        let ref = (`labeled range_0 "Could not prove termination" (`#ref)) in
        { last with
            sort = (pack (Tv_Refine b' ref))
        }
      in
      init @ [last]
    ) else
      r_bs
  in
  let r_res = R.subst_term prime_subst r_res in
  let r_ty = FStar.Tactics.V2.SyntaxHelpers.mk_tot_arr r_bs r_res in
  // let open FStar.Stubs.Pprint in
  // let open Pulse.PP in
  // warn_doc g (Some d.range) [
  //   text "r_ty (type of the knot binder) =" ^/^ pp r_ty
  // ];
  if R.Tv_Unknown? (inspect_ln r_ty) then
    fail g (Some d.range) "error: r_ty is Tv_unknown in add_knot?";
  let b_knot =
    let s, rng = inspect_ident id in
    let b = mk_binder s rng (tm_fstar r_ty rng) in
    let bv = {
      bv_index = b_knot._3.bv_index;
      bv_ppname = { name = seal s; range = rng }
    } in
    let q = None in
    (q, b, bv)
  in
  let id' =
    let s, rng = inspect_ident id in
    pack_ident ("__recaux_" ^ s, rng)
  in
  let bs' = bs @ [b_knot] in

  (* NB: body and comp unchanged, they are already shifted properly
     (we dropped one binder and added one) *)
  { d with d =
    FnDecl { id=id'; isrec=false; bs=bs'; comp; meas=None; body }
  }
val add_knot (g : env)  (rng : R.range)
             (d : decl)
: Tac decl
let add_knot (g: env) (rng: R.range) (d: decl{FnDecl? d.d}) : Tac decl =
let FnDecl { id = id ; isrec = isrec ; bs = bs ; comp = comp ; meas = meas ; body = body } = d.d in
if Nil? bs then fail g (Some d.range) "main: FnDecl does not have binders";
let r_res = elab_comp comp in
let elab_b (qbv: option qualifier & binder & bv) : Tot Tactics.NamedView.binder =
  let q, b, bv = qbv in
  {
    uniq = bv.bv_index;
    ppname = b.binder_ppname.name;
    sort = elab_term b.binder_ty;
    qual = elab_qual q;
    attrs = []
  }
in
debug_main g
  (fun _ ->
      Printf.sprintf "add_knot: bs = %s\n"
        (string_of_list (fun (_, b, _) -> P.binder_to_string b) bs));
let bs, b_knot = splitlast bs in
let r_bs0 = List.Tot.map elab_b bs in
let freshen_binder (b: T.binder) : T.binder =
  { b with uniq = 10000 + b.uniq; ppname = map_seal b.ppname (fun s -> s ^ "'") }
in
let r_bs = map freshen_binder r_bs0 in
let binder_to_r_namedv (b: T.binder) : R.namedv =
  R.pack_namedv ({ uniq = b.uniq; sort = seal b.sort; ppname = b.ppname })
in
let prime_subst =
  map2 (fun (b1: T.binder) (b2: T.binder) -> R.NT (binder_to_r_namedv b1) (binder_to_term b2))
    r_bs0
    r_bs
in
let r_bs =
  if C_STAtomic? comp || C_STGhost? comp
  then
    (if None? meas
      then
        (let open FStar.Stubs.Pprint in
          let open Pulse.PP in
          fail_doc g
            (Some d.range)
            [text "'ghost' and 'atomic' recursive functions require a 'decreases' clause"]);
      let init, last = splitlast r_bs in
      let last:FStar.Tactics.NamedView.binder = last in
      let last =
        let b':simple_binder =
          {
            uniq = last.uniq;
            ppname = last.ppname;
            sort = last.sort;
            qual = Q_Explicit;
            attrs = []
          }
        in
        let meas = Some?.v meas in
        let meas = elab_term meas in
        let meas' = R.subst_term prime_subst meas in
        let ref = `((`#meas') << (`#meas)) in
        let ref = (`labeled range_0 "Could not prove termination" (`#ref)) in
        { last with sort = (pack (Tv_Refine b' ref)) }
      in
      init @ [last])
  else r_bs
in
let r_res = R.subst_term prime_subst r_res in
let r_ty = FStar.Tactics.V2.SyntaxHelpers.mk_tot_arr r_bs r_res in
if R.Tv_Unknown? (inspect_ln r_ty)
then fail g (Some d.range) "error: r_ty is Tv_unknown in add_knot?";
let b_knot =
  let s, rng = inspect_ident id in
  let b = mk_binder s rng (tm_fstar r_ty rng) in
  let bv = { bv_index = b_knot._3.bv_index; bv_ppname = { name = seal s; range = rng } } in
  let q = None in
  (q, b, bv)
in
let id' =
  let s, rng = inspect_ident id in
  pack_ident ("__recaux_" ^ s, rng)
in
let bs' = bs @ [b_knot] in
{ d with d = FnDecl ({ id = id'; isrec = false; bs = bs'; comp = comp; meas = None; body = body }) }
Pulse.Recursion.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.PP.fst.checked prims.fst.checked FStar.Tactics.V2.SyntaxHelpers.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.NamedView.fsti.checked FStar.Stubs.Pprint.fsti.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.Recursion.fst
Pulse.Typing.Env.env FStar.Range.range Pulse.Syntax.Base.decl Prims.b2t Pulse.Syntax.Base.uu___is_FnDecl Pulse.Syntax.Base.__proj__Mkdecl__item__d FStar.Reflection.Types.ident Prims.bool Prims.list FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier Pulse.Syntax.Base.binder Pulse.Syntax.Base.bv Pulse.Syntax.Base.comp Pulse.Syntax.Base.term Prims.l_imp FStar.Pervasives.Native.uu___is_Some Pulse.Syntax.Base.st_term Pulse.Syntax.Base.Mkdecl Pulse.Syntax.Base.FnDecl Pulse.Syntax.Base.Mkdecl'__FnDecl__payload FStar.Pervasives.Native.None Pulse.Syntax.Base.__proj__Mkdecl__item__range FStar.List.Tot.Base.op_At Prims.Cons Prims.Nil Prims.string FStar.Reflection.V2.Builtins.pack_ident FStar.Pervasives.Native.Mktuple2 Prims.op_Hat FStar.Reflection.V2.Data.ident_view Prims.precedes FStar.Reflection.V2.Builtins.inspect_ident FStar.Pervasives.Native.Mktuple3 Pulse.Syntax.Base.Mkbv Pulse.Syntax.Base.__proj__Mkbv__item__bv_index FStar.Pervasives.Native.__proj__Mktuple3__item___3 Pulse.Syntax.Base.Mkppname FStar.Sealed.seal Pulse.Syntax.Base.mk_binder Pulse.Syntax.Base.tm_fstar Prims.unit FStar.Reflection.V2.Data.uu___is_Tv_Unknown FStar.Reflection.V2.Builtins.inspect_ln Pulse.Typing.Env.fail FStar.Pervasives.Native.Some Pulse.Syntax.Base.range FStar.Tactics.NamedView.term FStar.Tactics.V2.SyntaxHelpers.mk_tot_arr FStar.Reflection.Types.term FStar.Reflection.V2.Builtins.subst_term FStar.Tactics.NamedView.binder Prims.op_BarBar Pulse.Syntax.Base.uu___is_C_STAtomic Pulse.Syntax.Base.uu___is_C_STGhost FStar.Tactics.NamedView.Mkbinder FStar.Tactics.NamedView.__proj__Mkbinder__item__uniq FStar.Tactics.NamedView.__proj__Mkbinder__item__ppname FStar.Tactics.NamedView.pack FStar.Tactics.NamedView.Tv_Refine FStar.Tactics.NamedView.__proj__Mkbinder__item__qual FStar.Tactics.NamedView.__proj__Mkbinder__item__attrs Pulse.Elaborate.Pure.elab_term FStar.Pervasives.Native.__proj__Some__item__v FStar.Tactics.NamedView.simple_binder FStar.Tactics.NamedView.__proj__Mkbinder__item__sort FStar.Reflection.V2.Data.Q_Explicit FStar.Pervasives.Native.tuple2 Pulse.Recursion.splitlast FStar.Pervasives.Native.uu___is_None Pulse.Typing.Env.fail_doc FStar.Stubs.Pprint.document Pulse.PP.text FStar.Stubs.Syntax.Syntax.subst_elt Pulse.Recursion.map2 FStar.Stubs.Syntax.Syntax.NT FStar.Tactics.V2.SyntaxCoercions.binder_to_term FStar.Reflection.Types.namedv FStar.Reflection.V2.Builtins.pack_namedv FStar.Reflection.V2.Data.Mknamedv_view FStar.Reflection.Types.typ FStar.List.Tot.Base.map Prims.op_Addition FStar.Sealed.map_seal Pulse.Recursion.debug_main FStar.Printf.sprintf FStar.Tactics.Util.string_of_list Pulse.Syntax.Printer.binder_to_string Pulse.Syntax.Base.__proj__Mkppname__item__name Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ppname Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ty Pulse.Elaborate.Pure.elab_qual Pulse.Elaborate.Pure.elab_comp Prims.uu___is_Nil Pulse.Syntax.Base.decl'
module Pulse.Recursion

module R = FStar.Reflection.V2
module RT = FStar.Reflection.Typing
module T = FStar.Tactics.V2
open FStar.Tactics.V2
module RU = Pulse.RuntimeUtils

open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing
module P = Pulse.Syntax.Printer

exception Splitlast_empty

let rec splitlast #a (l : list a) : Tac (list a & a) =
  match l with
  | [] -> raise Splitlast_empty
  | [x] -> [], x
  | x::xs ->
    let init, last = splitlast xs in
    x::init, last

 exception Map2_length_mismatch

let rec map2 #a #b #c (f : a -> b -> Tac c) (xs : list a) (ys : list b) : Tac (list c) =
  match xs, ys with
  | [], [] -> []
  | x::xx, y::yy -> f x y :: map2 f xx yy
  | _ -> raise Map2_length_mismatch

let debug_main g (s: unit -> Tac string) : Tac unit =
  if RU.debug_at_level (fstar_env g) "pulse.main"
  then print (s ())
  else ()

let add_knot (g : env) (rng : R.range)
             (d : decl{FnDecl? d.d})
val add_knot (g : env)  (rng : R.range)
             (d : decl)
: Tac decl
g: Pulse.Typing.Env.env -> rng: FStar.Range.range -> d: Pulse.Syntax.Base.decl
  -> FStar.Tactics.Effect.Tac Pulse.Syntax.Base.decl