propagate parser kinds for nlist to interpreter and front end

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 ->

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 ->

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'

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

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 ->