From b6264b814066b113e8c4ce3d88872c9d2ec3ac4c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 1 Mar 2025 17:28:40 -0800 Subject: [PATCH] Tactics.NamedView: guaranteeing that `pack` does not change top-level ctor --- tests/tactics/NamedViewCtor.fst | 12 ++++++++++++ ulib/FStar.Tactics.NamedView.fst | 9 +++++++-- ulib/FStar.Tactics.NamedView.fsti | 32 +++++++++++++++++++++++++++++++ 3 files changed, 51 insertions(+), 2 deletions(-) create mode 100644 tests/tactics/NamedViewCtor.fst diff --git a/tests/tactics/NamedViewCtor.fst b/tests/tactics/NamedViewCtor.fst new file mode 100644 index 00000000000..501c4f1db26 --- /dev/null +++ b/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)) diff --git a/ulib/FStar.Tactics.NamedView.fst b/ulib/FStar.Tactics.NamedView.fst index c7ccc8cf836..47bad023af2 100644 --- a/ulib/FStar.Tactics.NamedView.fst +++ b/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 diff --git a/ulib/FStar.Tactics.NamedView.fsti b/ulib/FStar.Tactics.NamedView.fsti index 6caf3674d3a..7f98389a2ca 100644 --- a/ulib/FStar.Tactics.NamedView.fsti +++ b/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