Tactics.NamedView: guaranteeing that pack does not change top-level…

… ctor

tests/tactics/NamedViewCtor.fst

@@ -0,0 +1,12 @@
+module NamedViewCtor
+
+open FStar.Tactics.V2
+module R = FStar.Reflection.V2
+
+let not_unsupp (tv:term_view{~(Tv_Unsupp? tv)}) : Tot unit =
+  let t = pack tv in
+  assert (~(R.Tv_Unsupp? (R.inspect_ln t)))
+
+let preserved (t1 t2 : term) : Tot unit =
+  let t = pack (Tv_App t1 (t2, Q_Explicit)) in
+  assert (R.Tv_App? (R.inspect_ln t))

ulib/FStar.Tactics.NamedView.fst

@@ -408,7 +408,7 @@ let close_match_returns_ascription (mra : match_returns_ascription) : R.match_re
   (b, (ct, topt, use_eq))
 
 private
-let open_view (tv:term_view) : Tac named_term_view =
+let open_view (tv:term_view) : Tac (tv':named_term_view{ctor_matches tv' tv}) =
   match tv with
   (* Nothing interesting *)
   | RD.Tv_Var v -> Tv_Var (R.inspect_namedv v)
@@ -454,7 +454,7 @@ let open_view (tv:term_view) : Tac named_term_view =
     Tv_Match scrutinee ret brs
 
 private
-let close_view (tv : named_term_view) : Tot term_view =
+let close_view (tv : named_term_view) : Tot (tv':term_view{ctor_matches tv tv'}) =
   match tv with
   (* Nothing interesting *)
   | Tv_Var v -> RD.Tv_Var (R.pack_namedv v)
@@ -517,6 +517,11 @@ let pack (tv:named_term_view) : Tot term =
   let tv = close_view tv in
   R.pack_ln tv
 
+let pack_ctor_matches (tv:named_term_view)
+  : Lemma (ctor_matches tv (RB.inspect_ln (pack tv)))
+          [SMTPat (pack tv)]
+  = R.inspect_pack_inv (close_view tv)
+
 private
 let open_univ_s (us : list R.univ_name) : Tac (list univ_name & subst_t) =
   let n = List.Tot.length us in

ulib/FStar.Tactics.NamedView.fsti

@@ -20,6 +20,7 @@ open FStar.Stubs.Reflection.Types
 open FStar.Stubs.Reflection.V2.Data
 module R = FStar.Stubs.Reflection.Types
 module RD = FStar.Stubs.Reflection.V2.Data
+module RB = FStar.Stubs.Reflection.V2.Builtins
 
 (* Re export the syntax types. Expose variables as their views, users do
 not need to pack/inspect these if they are using the named view. *)
@@ -111,6 +112,30 @@ type named_term_view =
   | Tv_Unknown  : named_term_view // An underscore: _
   | Tv_Unsupp : named_term_view // failed to inspect, not supported
 
+(* Relating constructors between old and new view. Both flavors of
+functions usually behave the same wrt the top-level constructor
+of the terms involved. *)
+let ctor_matches (v1:named_term_view) (v2:RD.term_view) : prop =
+  match v1, v2 with
+  | Tv_Var _             , RD.Tv_Var _             -> True
+  | Tv_BVar _            , RD.Tv_BVar _            -> True
+  | Tv_FVar _            , RD.Tv_FVar _            -> True
+  | Tv_UInst _ _         , RD.Tv_UInst _ _         -> True
+  | Tv_App _ _           , RD.Tv_App _ _           -> True
+  | Tv_Abs _ _           , RD.Tv_Abs _ _           -> True
+  | Tv_Arrow _ _         , RD.Tv_Arrow _ _         -> True
+  | Tv_Type _            , RD.Tv_Type _            -> True
+  | Tv_Refine _ _        , RD.Tv_Refine _ _        -> True
+  | Tv_Const _           , RD.Tv_Const _           -> True
+  | Tv_Uvar _ _          , RD.Tv_Uvar _ _          -> True
+  | Tv_Let _ _ _ _ _     , RD.Tv_Let _ _ _ _ _     -> True
+  | Tv_Match _ _ _       , RD.Tv_Match _ _ _       -> True
+  | Tv_AscribedT _ _ _ _ , RD.Tv_AscribedT _ _ _ _ -> True
+  | Tv_AscribedC _ _ _ _ , RD.Tv_AscribedC _ _ _ _ -> True
+  | Tv_Unknown           , RD.Tv_Unknown           -> True
+  | Tv_Unsupp            , RD.Tv_Unsupp            -> True
+  | _ -> False
+
 // Repeat from FStar.R.Data
 let notAscription (tv:named_term_view) : bool =
   not (Tv_AscribedT? tv) && not (Tv_AscribedC? tv)
@@ -187,12 +212,19 @@ val pack_universe (uv:named_universe_view) : Tot universe
 [@@plugin]
 val close_term (b:binder) (t:term) : Tot (R.binder & term)
 
+(* Note: this cannot guarantee that the returned view ctor_matches the
+  original term, since we compress the term which may resolve uvar. *)
 [@@plugin; coercion]
 val inspect (t:term) : Tac named_term_view
 
 [@@plugin; coercion]
 val pack (tv:named_term_view) : Tot term
 
+(* pack, however, does guarantee that. *)
+val pack_ctor_matches (tv:named_term_view)
+  : Lemma (ctor_matches tv (RB.inspect_ln (pack tv)))
+          [SMTPat (pack tv)]
+
 [@@plugin; coercion]
 val inspect_sigelt (s : sigelt) : Tac named_sigelt_view