From 86b6048ef8747297d92771722364ac9ec7566c62 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Mon, 21 Oct 2024 11:55:32 -0700 Subject: [PATCH] propagate parser kinds for nlist to interpreter and front end --- src/3d/InterpreterTarget.fst | 14 +++++++++++--- src/3d/Target.fst | 10 +++++++--- src/3d/Target.fsti | 2 +- src/3d/TranslateForInterpreter.fst | 11 ++++++++--- src/3d/prelude/EverParse3d.Interpreter.fst | 22 +++++++++++----------- 5 files changed, 38 insertions(+), 21 deletions(-) diff --git a/src/3d/InterpreterTarget.fst b/src/3d/InterpreterTarget.fst index e8ad14486..c16df15c8 100644 --- a/src/3d/InterpreterTarget.fst +++ b/src/3d/InterpreterTarget.fst @@ -860,11 +860,19 @@ let rec print_typ (mname:string) (t:typ) | None -> false, n | Some m -> true, (T.Constant m, snd n) in - Printf.sprintf "(T_nlist \"%s\" %b %b %s %s)" + let n_is_const = + if is_const + then + match fst n with + | T.Constant (A.Int _ n) -> Printf.sprintf "(Some %d)" n + | _ -> "None" + else "None" + in + Printf.sprintf "(T_nlist \"%s\" %s %s %b %s)" fn - is_const - fixed_size (T.print_expr mname n) + n_is_const + fixed_size (print_typ mname t) | T_at_most fn n t -> diff --git a/src/3d/Target.fst b/src/3d/Target.fst index c0c9c7d9e..f1a94d9e5 100644 --- a/src/3d/Target.fst +++ b/src/3d/Target.fst @@ -69,7 +69,7 @@ let rec parser_kind_eq k k' = match k.pk_kind, k'.pk_kind with | PK_return, PK_return -> true | PK_impos, PK_impos -> true - | PK_list, PK_list -> true + | PK_list k0 n0, PK_list k1 n1 -> parser_kind_eq k0 k1 && n0=n1 | PK_t_at_most, PK_t_at_most -> true | PK_t_exact, PK_t_exact -> true | PK_base hd1, PK_base hd2 -> A.(hd1.v = hd2.v) @@ -454,8 +454,12 @@ let rec print_kind (mname:string) (k:parser_kind) : Tot string = Printf.sprintf "%skind_%s" (maybe_mname_prefix mname hd) (print_ident hd) - | PK_list -> - "kind_nlist" + | PK_list k0 n -> + Printf.sprintf "(kind_nlist %s %s)" + (print_kind mname k0) + (match n with + | None -> "None" + | Some n -> Printf.sprintf "(Some %d)" n) | PK_t_at_most -> "kind_t_at_most" | PK_t_exact -> diff --git a/src/3d/Target.fsti b/src/3d/Target.fsti index fc954c510..f20de5c14 100644 --- a/src/3d/Target.fsti +++ b/src/3d/Target.fsti @@ -182,7 +182,7 @@ type parser_kind' = | PK_return | PK_impos | PK_base : hd:A.ident -> parser_kind' - | PK_list : parser_kind' + | PK_list : elt_kind:parser_kind -> option nat -> parser_kind' | PK_t_at_most: parser_kind' | PK_t_exact : parser_kind' | PK_filter : k:parser_kind -> parser_kind' diff --git a/src/3d/TranslateForInterpreter.fst b/src/3d/TranslateForInterpreter.fst index 393e70051..c09e0353c 100644 --- a/src/3d/TranslateForInterpreter.fst +++ b/src/3d/TranslateForInterpreter.fst @@ -128,8 +128,8 @@ let pk_base id nz wk = T.({ pk_weak_kind = wk; pk_nz = nz }) -let pk_list = T.({ - pk_kind = PK_list; +let pk_list k0 n = T.({ + pk_kind = PK_list k0 n; pk_weak_kind = WeakKindStrongPrefix; pk_nz = false }) @@ -493,7 +493,12 @@ let rec parse_typ (env:global_env) | T.T_nlist telt e -> let pt = parse_typ env typename (extend_fieldname "element") telt in let t_size_constant = is_compile_time_fixed_size env telt in - mk_parser pk_list + let n_is_const = + match T.as_constant e with + | Some (A.Int _ n) -> if n >= 0 then Some n else None + | _ -> None + in + mk_parser (pk_list pt.p_kind n_is_const) t typename fieldname diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst index a5645625e..47211b536 100644 --- a/src/3d/prelude/EverParse3d.Interpreter.fst +++ b/src/3d/prelude/EverParse3d.Interpreter.fst @@ -927,11 +927,11 @@ type typ fieldname:string -> #wk:_ -> #pk:P.parser_kind true wk -> #i:_ -> #l:_ -> #d:_ -> #b:_ -> #ha:_ -> - n_is_constant:bool -> - payload_is_constant_size:bool -> n:U32.t -> + n_is_constant:option nat { P.memoizes_n_as_const n_is_constant n } -> + payload_is_constant_size:bool -> t:typ pk i d l ha b -> - typ P.kind_nlist i d l ha false + typ (P.kind_nlist pk n_is_constant) i d l ha false | T_at_most: fieldname:string -> @@ -1036,7 +1036,7 @@ let rec as_type | T_with_dep_action _ i _ -> dtyp_as_type i - | T_nlist _ _ _ n t -> + | T_nlist _fn n _n_is_const _plconst t -> P.nlist n (as_type t) | T_at_most _ n t -> @@ -1125,8 +1125,8 @@ let rec as_parser //assert_norm (as_type g (T_with_comment t c) == as_type g t); as_parser t - | T_nlist _ _ _ n t -> - P.parse_nlist n (as_parser t) + | T_nlist _fn n n_is_const _plconst t -> + P.parse_nlist n n_is_const (as_parser t) | T_at_most _ n t -> P.parse_t_at_most n (as_parser t) @@ -1333,17 +1333,17 @@ let rec as_validator assert_norm (as_parser (T_with_comment fn t c) == as_parser t); A.validate_with_comment c (as_validator typename t) - | T_nlist fn n_is_const payload_is_constant_size n t -> - assert_norm (as_type (T_nlist fn n_is_const payload_is_constant_size n t) == P.nlist n (as_type t)); - assert_norm (as_parser (T_nlist fn n_is_const payload_is_constant_size n t) == P.parse_nlist n (as_parser t)); + | T_nlist fn n n_is_const payload_is_constant_size t -> + assert_norm (as_type (T_nlist fn n n_is_const payload_is_constant_size t) == P.nlist n (as_type t)); + assert_norm (as_parser (T_nlist fn n n_is_const payload_is_constant_size t) == P.parse_nlist n n_is_const (as_parser t)); if ha then ( A.validate_with_error_handler typename fn - (A.validate_nlist n (as_validator typename t)) + (A.validate_nlist n n_is_const (as_validator typename t)) ) else ( A.validate_with_error_handler typename fn - (A.validate_nlist_constant_size_without_actions n_is_const payload_is_constant_size n (as_validator typename t)) + (A.validate_nlist_constant_size_without_actions n n_is_const payload_is_constant_size (as_validator typename t)) ) | T_at_most fn n t ->