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

Implementing map_seal and bind_seal primitive operators #3074

Merged
merged 11 commits into from
Nov 1, 2023
Merged

Implementing map_seal and bind_seal primitive operators #3074

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
7ea5df0
Syntax: Embeddings: better error
mtzguido Oct 30, 2023
38efb18
Syntax: Embeddings: sealed values should not be lazy
mtzguido Oct 30, 2023
f3f41cd
NBETerm: add set_type for embeddings
mtzguido Oct 30, 2023
f9095a4
Pervasives: add norm_debug step to trigger debugging
mtzguido Oct 30, 2023
362490c
Normalizer: allow for renormalization after primitive steps
mtzguido Oct 30, 2023
cdb4067
Normalizer: implement map_seal/bind_seal steps
mtzguido Oct 30, 2023
3282ad7
Add a test for map_seal/bind_seal
mtzguido Oct 30, 2023
5a368dd
snap
mtzguido Oct 30, 2023
7e7c05c
expected output
mtzguido Oct 30, 2023
01f0101
Merge branch 'master' of gh:FStarLang/FStar into guido_misc
mtzguido Oct 30, 2023
924c9f9
Merge branch 'master' into map_seal
mtzguido Nov 1, 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
NBETerm: add set_type for embeddings
  • Loading branch information
@mtzguido
mtzguido committed Oct 30, 2023
commit f3f41cd9f53905b33414808eb5922e6e9d90be93
1 change: 1 addition & 0 deletions src/typechecker/FStar.TypeChecker.NBETerm.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -219,6 +219,7 @@ let translate_cb cbs t = cbs.translate t
let embed (e:embedding 'a) (cb:nbe_cbs) (x:'a) : t = e.em cb x
let unembed (e:embedding 'a) (cb:nbe_cbs) (trm:t) : option 'a = e.un cb trm
let type_of (e:embedding 'a) : t = e.typ
let set_type (ty:t) (e:embedding 'a) : embedding 'a = { e with typ = ty }


let mk_emb em un typ et = {em = em; un = un; typ = typ; emb_typ=et}
Expand Down
1 change: 1 addition & 0 deletions src/typechecker/FStar.TypeChecker.NBETerm.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,6 +253,7 @@ val embed : embedding 'a -> nbe_cbs -> 'a -> t
val unembed : embedding 'a -> nbe_cbs -> t -> option 'a
val lazy_unembed_lazy_kind (#a:Type) (k:lazy_kind) (x:t) : option a
val type_of : embedding 'a -> t
val set_type : t -> embedding 'a -> embedding 'a

val e_bool : embedding bool
val e_string : embedding string
Expand Down