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

EverParse3d.InputStream.Base: do not use typeclasses for extra_t #117

Merged
merged 2 commits into from
Dec 4, 2023
Merged

EverParse3d.InputStream.Base: do not use typeclasses for extra_t #117

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e82664f
nit: use `instance val`
mtzguido Dec 2, 2023
7431735
EverParse3d.InputStream.Base: do not use typeclasses for extra_t
mtzguido Dec 2, 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
12 changes: 6 additions & 6 deletions src/3d/prelude/EverParse3d.Actions.Base.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ let input_buffer_t = EverParse3d.InputStream.All.t
let action
p inv l on_success a
=
(# [tcresolve ()] I.extra_t #input_buffer_t) ->
(# [EverParse3d.Util.solve_from_ctx ()] I.extra_t #input_buffer_t) ->
ctxt: app_ctxt ->
sl: input_buffer_t ->
pos: LPE.pos_t ->
Expand Down Expand Up @@ -160,7 +160,7 @@ let error_handler =

inline_for_extraction noextract
let validate_with_action_t' (#k:LP.parser_kind) (#t:Type) (p:LP.parser k t) (inv:slice_inv) (l:eloc) (allow_reading:bool) =
(# [tcresolve ()] I.extra_t #input_buffer_t) ->
(# [EverParse3d.Util.solve_from_ctx ()] I.extra_t #input_buffer_t) ->
(ctxt: app_ctxt) ->
(error_handler_fn : error_handler) ->
(sl: input_buffer_t) ->
Expand Down Expand Up @@ -216,7 +216,7 @@ let leaf_reader
(p: parser k t)
: Tot Type
=
(# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t ) ->
(# [EverParse3d.Util.solve_from_ctx ()] _extra_t : I.extra_t #input_buffer_t ) ->
(sl: input_buffer_t) ->
(pos: LPE.pos_t) ->
Stack t
Expand Down Expand Up @@ -825,7 +825,7 @@ let validate_list_inv
inline_for_extraction
noextract
let validate_list_body
(# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t )
(# [EverParse3d.Util.solve_from_ctx ()] _extra_t : I.extra_t #input_buffer_t )
(#k:LP.parser_kind)
#t
(#p:LP.parser k t)
Expand Down Expand Up @@ -860,7 +860,7 @@ let validate_list_body
inline_for_extraction
noextract
let validate_list'
(# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t )
(# [EverParse3d.Util.solve_from_ctx ()] _extra_t : I.extra_t #input_buffer_t )
(#k:LP.parser_kind)
#t
(#p:LP.parser k t)
Expand Down Expand Up @@ -1505,7 +1505,7 @@ let validate_list_up_to_inv

inline_for_extraction
let validate_list_up_to_body
(# [FStar.Tactics.Typeclasses.tcresolve ()] _extra_t : I.extra_t #input_buffer_t )
(# [EverParse3d.Util.solve_from_ctx ()] _extra_t : I.extra_t #input_buffer_t )
(#k: parser_kind true WeakKindStrongPrefix)
(#t: eqtype)
(#p: parser k t)
Expand Down
3 changes: 1 addition & 2 deletions src/3d/prelude/EverParse3d.InputStream.All.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ inline_for_extraction
noextract
val t : Type0

[@@FStar.Tactics.Typeclasses.tcinstance]
inline_for_extraction
noextract
val inst : input_stream_inst t
instance val inst : input_stream_inst t
12 changes: 6 additions & 6 deletions src/3d/prelude/EverParse3d.InputStream.Base.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ class input_stream_inst (t: Type) : Type = {
extra_t: Type0;

has:
(# [FStar.Tactics.Typeclasses.tcresolve () ] extra_t ) ->
(# [EverParse3d.Util.solve_from_ctx () ] extra_t ) ->
(x: t) ->
(len: tlen x) ->
(pos: LPE.pos_t) ->
Expand All @@ -77,7 +77,7 @@ class input_stream_inst (t: Type) : Type = {
));

read:
(# [FStar.Tactics.Typeclasses.tcresolve ()] extra_t ) ->
(# [EverParse3d.Util.solve_from_ctx ()] extra_t ) ->
(t': Type0) ->
(k: LP.parser_kind) ->
(p: LP.parser k t') ->
Expand Down Expand Up @@ -107,7 +107,7 @@ class input_stream_inst (t: Type) : Type = {
));

skip:
(# [FStar.Tactics.Typeclasses.tcresolve ()] extra_t ) ->
(# [EverParse3d.Util.solve_from_ctx ()] extra_t ) ->
(x: t) ->
(pos: LPE.pos_t) ->
(n: U64.t) ->
Expand All @@ -125,7 +125,7 @@ class input_stream_inst (t: Type) : Type = {
));

skip_if_success:
(# [FStar.Tactics.Typeclasses.tcresolve ()] extra_t ) ->
(# [EverParse3d.Util.solve_from_ctx ()] extra_t ) ->
(x: t) ->
(pos: LPE.pos_t) ->
(res: U64.t) ->
Expand All @@ -145,7 +145,7 @@ class input_stream_inst (t: Type) : Type = {
));

empty:
(# [FStar.Tactics.Typeclasses.tcresolve ()] extra_t ) ->
(# [EverParse3d.Util.solve_from_ctx ()] extra_t ) ->
(x: t) ->
(len: tlen x) ->
(pos: LPE.pos_t) ->
Expand Down Expand Up @@ -233,7 +233,7 @@ let length_all #t (#_: input_stream_inst t) (x: t) : GTot nat = U64.v (len_all x

let preserved'
(#t: Type)
(# [FStar.Tactics.Typeclasses.tcresolve ()] inst : input_stream_inst t)
(# [EverParse3d.Util.solve_from_ctx ()] inst : input_stream_inst t)
(x: t)
(l: B.loc)
(h: HS.mem)
Expand Down
8 changes: 8 additions & 0 deletions src/3d/prelude/EverParse3d.Util.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
module EverParse3d.Util

open FStar.Tactics.V2

let solve_from_ctx () : Tac unit =
ignore (intros ());
let bs = vars_of_env (cur_env ()) in
first (map (fun (b:binding) () -> exact b) bs)
3 changes: 1 addition & 2 deletions src/3d/prelude/buffer/EverParse3d.InputStream.Buffer.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ inline_for_extraction
noextract
val t : Type0

[@@ FStar.Tactics.Typeclasses.tcinstance]
noextract
inline_for_extraction
val inst : input_stream_inst t
instance val inst : input_stream_inst t
14 changes: 7 additions & 7 deletions src/3d/prelude/extern/EverParse3d.InputStream.Extern.Base.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ val preserved:
val extra_t: Type0

val has:
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
(x: t) ->
(n: U64.t) ->
HST.Stack bool
Expand All @@ -71,7 +71,7 @@ val has:
))

val read:
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
(x: t) ->
(n: U64.t) ->
(dst: B.buffer U8.t) ->
Expand All @@ -96,7 +96,7 @@ val read:

noextract [@@noextract_to "krml"]
let peep_pre
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t)
(x: t)
(n: U64.t)
(h: HS.mem)
Expand All @@ -107,7 +107,7 @@ let peep_pre

noextract [@@noextract_to "krml"]
let peep_post
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t)
(x: t)
(n: U64.t)
(h: HS.mem)
Expand All @@ -127,7 +127,7 @@ let peep_post
end

val peep:
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
(x: t) ->
(n: U64.t) ->
HST.Stack (B.buffer U8.t)
Expand All @@ -139,7 +139,7 @@ val peep:
))

val skip:
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
(x: t) ->
(n: U64.t) ->
HST.Stack unit
Expand All @@ -152,7 +152,7 @@ val skip:
))

val empty:
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: extra_t) ->
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: extra_t) ->
(x: t) ->
HST.Stack U64.t
(requires (fun h -> live x h))
Expand Down
26 changes: 13 additions & 13 deletions src/3d/prelude/extern/EverParse3d.InputStream.Extern.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ open LowStar.BufferOps
inline_for_extraction
noextract
let has
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(_: unit)
(position: LPE.pos_t)
Expand All @@ -137,7 +137,7 @@ let has
inline_for_extraction
noextract
let read0
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(position: LPE.pos_t)
(n: U64.t)
Expand Down Expand Up @@ -183,7 +183,7 @@ module LP = LowParse.Low.Base
inline_for_extraction
noextract
let read
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(t': Type0)
(k: LP.parser_kind)
(p: LP.parser k t')
Expand Down Expand Up @@ -245,7 +245,7 @@ let read

noextract [@@noextract_to "krml"]
let peep_pre'
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(position: LPE.pos_t)
(h: HS.mem)
Expand All @@ -257,7 +257,7 @@ let peep_pre'
noextract [@@noextract_to "krml"]
unfold
let peep_post'
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(position: LPE.pos_t)
(n: U64.t)
Expand All @@ -279,7 +279,7 @@ let peep_post'

noextract [@@noextract_to "krml"]
let peep0_pre'
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(position: LPE.pos_t)
(n: U64.t)
Expand All @@ -292,7 +292,7 @@ let peep0_pre'
// #restart-solver

let peep_post_extract_concl
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: Aux.t)
(n: U64.t)
(h: HS.mem)
Expand All @@ -316,7 +316,7 @@ let peep_post_extract_concl
= ()

let peep0_exit // this is the crucial lemma for peep to work
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(position: LPE.pos_t)
(n: U64.t)
Expand Down Expand Up @@ -350,7 +350,7 @@ let peep0_exit // this is the crucial lemma for peep to work
inline_for_extraction
noextract
let peep0
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(position: LPE.pos_t)
(n: U64.t)
Expand All @@ -363,7 +363,7 @@ let peep0
inline_for_extraction
noextract
let peep
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(position: LPE.pos_t)
(n: U64.t)
Expand All @@ -385,7 +385,7 @@ let peep
inline_for_extraction
noextract
let skip
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(position: LPE.pos_t)
(n: U64.t)
Expand All @@ -410,7 +410,7 @@ let skip
inline_for_extraction
noextract
let skip_if_success
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(pos: LPE.pos_t)
(res: U64.t)
Expand All @@ -436,7 +436,7 @@ let skip_if_success
inline_for_extraction
noextract
let empty
(#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
(#[EverParse3d.Util.solve_from_ctx ()] _extra_t: Aux.extra_t)
(x: t)
(_: unit)
(position: LPE.pos_t)
Expand Down
Loading