Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Some reflection/tactics updates #2918

Merged
merged 11 commits into from
May 7, 2023
Merged

Some reflection/tactics updates #2918

Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
913ab4c
smtencoding: some comments + nit on message
mtzguido May 1, 2023
bed1a44
print/tc: tweaking debug info to distinguish let/val
mtzguido May 7, 2023
dae0fbc
bug-reports: nit on Makefile
mtzguido May 1, 2023
f0a340a
reflection: nbe: bv.ppname is sealed
mtzguido Apr 30, 2023
33ff60c
reflection: exposing the sort of pattern variables as sealed
mtzguido Apr 30, 2023
688a2ab
examples: restore param
mtzguido Apr 30, 2023
e208429
remove Pat_wild
mtzguido Apr 30, 2023
12ff4e8
bump checked filed version
mtzguido May 1, 2023
901cde6
reflection/tactics: distinguish Tv_Unknown and Tv_Unsupp
mtzguido May 1, 2023
91092c8
fixing lib and examples
mtzguido May 1, 2023
3afca1b
snap
mtzguido May 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
reflection: nbe: bv.ppname is sealed
  • Loading branch information
@mtzguido
mtzguido committed May 7, 2023
commit f0a340a04af99e4c0824aaecfb70c24134db0292
4 changes: 2 additions & 2 deletions src/reflection/FStar.Reflection.NBEEmbeddings.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -583,13 +583,13 @@ let e_term_view = e_term_view_aq (0, [])

let e_bv_view =
let embed_bv_view cb (bvv:bv_view) : t =
mkConstruct ref_Mk_bv.fv [] [as_arg (embed e_string cb bvv.bv_ppname);
mkConstruct ref_Mk_bv.fv [] [as_arg (embed (e_sealed e_string) cb bvv.bv_ppname);
as_arg (embed e_int cb bvv.bv_index)]
in
let unembed_bv_view cb (t : t) : option bv_view =
match t.nbe_t with
| Construct (fv, _, [(idx, _); (nm, _)]) when S.fv_eq_lid fv ref_Mk_bv.lid ->
BU.bind_opt (unembed e_string cb nm) (fun nm ->
BU.bind_opt (unembed (e_sealed e_string) cb nm) (fun nm ->
BU.bind_opt (unembed e_int cb idx) (fun idx ->
Some <| { bv_ppname = nm ; bv_index = idx }))

Expand Down