refactor val-spec AST to store externs as an assoc-list rather than a function (preparing for marshalling)

12 files changed, 58 insertions, 47 deletions

diff --git a/language/sail.ott b/language/sail.ott
index 59d51d68..5c8b6a01 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -943,8 +943,8 @@ val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::=
 
 val_spec_aux :: 'VS_' ::=
   {{ com value type specification }}
-  {{ ocaml  VS_val_spec of typschm * id * (string -> string option) * bool }}
-  {{ lem VS_val_spec of typschm * id * (string -> maybe string) * bool }}
+  {{ ocaml  VS_val_spec of typschm * id * (string * string) list * bool }}
+  {{ lem VS_val_spec of typschm * id * list (string * string) * bool }}
   | val typschm id                                  :: S :: val_spec
     {{ com specify the type of an upcoming definition }}
     {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }}
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 9966742e..3d13c5c3 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1488,3 +1488,13 @@ and locate_fexps : 'a. l -> 'a fexps -> 'a fexps = fun l (FES_aux (FES_Fexps (fe
 
 and locate_fexp : 'a. l -> 'a fexp -> 'a fexp = fun l (FE_aux (FE_Fexp (id, exp), (_, annot))) ->
   FE_aux (FE_Fexp (locate_id l id, locate l exp), (l, annot))
+
+
+let extern_assoc backend exts =
+  try
+    try
+      Some (List.assoc backend exts)
+    with Not_found ->
+      Some (List.assoc "_" exts)
+  with Not_found ->
+    None
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ea287190..54f18ae8 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -366,3 +366,6 @@ val locate_pat : l -> 'a pat -> 'a pat
 val locate_lexp : l -> 'a lexp -> 'a lexp
 
 val locate_typ : l -> typ -> typ
+
+
+val extern_assoc : string -> (string * string) list -> string option
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 36513ba1..36c60f2e 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1078,8 +1078,8 @@ let typschm_of_string order str =
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
-let extern_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false))
-let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> None), false))
+let extern_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, [("_", string_of_id id)], false))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, [], false))
 
 let val_spec_ids (Defs defs) =
   let val_spec_id (VS_aux (vs_aux, _)) =
@@ -1154,7 +1154,7 @@ let generate_undefineds vs_ids (Defs defs) =
   let undefined_td = function
     | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
-       [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false));
+       [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, [], false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             (mk_pat (P_lit (mk_lit L_unit)))
                             (if !opt_fast_undefined && List.length ids > 0 then
@@ -1164,7 +1164,7 @@ let generate_undefineds vs_ids (Defs defs) =
                                               [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
     | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
-       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             pat
                             (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
@@ -1212,7 +1212,7 @@ let generate_undefineds vs_ids (Defs defs) =
              (mk_exp (E_app (mk_id "internal_pick",
                              [mk_exp (E_list (List.map (make_constr typ_to_var) constr_args))]))) letbinds
        in
-       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                       pat
                       body]]
@@ -1248,7 +1248,7 @@ let generate_enum_functions vs_ids (Defs defs) =
   let rec gen_enums = function
     | DEF_type (TD_aux (TD_enum (id, _, elems, _), _)) as enum :: defs ->
        let enum_val_spec name quants typ =
-         mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts))
+         mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, [], !opt_enum_casts))
        in
        let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in
 
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 4828398f..2a1fae15 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -615,8 +615,8 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
  | _ -> failwith "Unsupported typedef"
 
 let get_externs (Defs defs) =
-  let extern_id (VS_aux (VS_val_spec (typschm, id, ext, _), _)) =
-    match ext "ocaml" with
+  let extern_id (VS_aux (VS_val_spec (typschm, id, exts, _), _)) =
+    match Ast_util.extern_assoc "ocaml" exts with
     | None -> []
     | Some ext -> [(id, mk_id ext)]
   in
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 3317c196..db8f9939 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -488,7 +488,7 @@ type_def_aux =  (* Type definition body *)
 
 type 
 val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id * (string -> string option) * bool
+   VS_val_spec of typschm * id * (string * string) list * bool
 
 
 type 
diff --git a/src/parser.mly b/src/parser.mly
index 070dee50..b2df5176 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1316,31 +1316,31 @@ let_def:
 
 externs:
   | id Colon String
-    { ([(string_of_id $1, $3)], None) }
+    { [(string_of_id $1, $3)] }
   | Under Colon String
-    { ([], Some $3) }
+    { [("_", $3)] }
   | id Colon String Comma externs
-    { cons_fst (string_of_id $1, $3) $5 }
+    { (string_of_id $1, $3) :: $5 }
 
 val_spec_def:
   | Doc val_spec_def
     { doc_vs $1 $2 }
   | Val id Colon typschm
-    { mk_vs (VS_val_spec ($4, $2, (fun _ -> None), false)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($4, $2, [], false)) $startpos $endpos }
   | Val Cast id Colon typschm
-    { mk_vs (VS_val_spec ($5, $3, (fun _ -> None), true)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($5, $3, [], true)) $startpos $endpos }
   | Val id Eq String Colon typschm
-    { mk_vs (VS_val_spec ($6, $2, (fun _ -> Some $4), false)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($6, $2, [], false)) $startpos $endpos }
   | Val Cast id Eq String Colon typschm
-    { mk_vs (VS_val_spec ($7, $3, (fun _ -> Some $5), true)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($7, $3, [("_", $5)], true)) $startpos $endpos }
   | Val String Colon typschm
-    { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), (fun _ -> Some $2), false)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), [("_", $2)], false)) $startpos $endpos }
   | Val Cast String Colon typschm
-    { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), (fun _ -> Some $3), true)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), [("_", $3)], true)) $startpos $endpos }
   | Val id Eq Lcurly externs Rcurly Colon typschm
-    { mk_vs (VS_val_spec ($8, $2, (fun backend -> (assoc_opt backend $5)), false)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($8, $2, $5, false)) $startpos $endpos }
   | Val Cast id Eq Lcurly externs Rcurly Colon typschm
-    { mk_vs (VS_val_spec ($9, $3, (fun backend -> (assoc_opt backend $6)), true)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($9, $3, $6, true)) $startpos $endpos }
 
 register_def:
   | Register id Colon typ
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index f1726ce4..ccbde5cd 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2235,8 +2235,8 @@ let find_exc_typ defs =
 
 let find_unimplemented defs =
   let adjust_def unimplemented = function
-    | DEF_spec (VS_aux (VS_val_spec (_,id,ext,_),_)) -> begin
-      match ext "coq" with
+    | DEF_spec (VS_aux (VS_val_spec (_,id,exts,_),_)) -> begin
+      match Ast_util.extern_assoc "coq" exts with
       | Some _ -> unimplemented
       | None -> IdSet.add id unimplemented
     end
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 68825c8f..ba2b797b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1349,7 +1349,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
 
 let doc_spec_lem (VS_aux (valspec,annot)) =
   match valspec with
-  | VS_val_spec (typschm,id,ext,_) when ext "lem" = None ->
+  | VS_val_spec (typschm,id,exts,_) when Ast_util.extern_assoc "lem" exts = None ->
      (* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in
      if contains_t_pp_var typ then empty else *)
      doc_docstring_lem annot ^^
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 0b0a8305..179ef208 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -538,9 +538,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
 
 let doc_spec (VS_aux (v, annot)) =
   let doc_extern ext =
-    let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^
-      utf8string ("\"" ^ String.escaped id ^  "\"")) (ext b) in
-    let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"; "smt"; "interpreter"; "c"]) in
+    let docs = List.map (fun (backend, rep) -> string (backend ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped rep ^ "\"")) ext in
     if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs)
   in
   match v with
diff --git a/src/rewrites.ml b/src/rewrites.ml
index c470d906..f1d22720 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2212,7 +2212,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
       in
       let val_spec =
         VS_aux (VS_val_spec
-          (mk_typschm typquant fun_typ, id, (fun _ -> None), false),
+          (mk_typschm typquant fun_typ, id, [], false),
           (Parse_ast.Unknown, empty_tannot))
       in
       let fundef = FD_aux (FD_function (r_o, t_o, e_o, funcls), fdannot) in
@@ -3152,7 +3152,7 @@ let construct_toplevel_string_append_func env f_id pat =
                                                             ), unk)]
   in
   let fun_typ = (mk_typ (Typ_fn ([string_typ], option_typ, no_effect))) in
-  let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, (fun _ -> None), false), unkt) in
+  let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, [], false), unkt) in
   let new_val_spec, env = Type_check.check_val_spec env new_val_spec in
   let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
   let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
@@ -4345,10 +4345,10 @@ let rewrite_defs_realise_mappings (Defs defs) =
     let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), l) in
     let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), l) in
 
-    let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
-    let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
-    let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
-    let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+    let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, [], false), (Parse_ast.Unknown,())) in
+    let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, [], false), (Parse_ast.Unknown,())) in
+    let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, [], false), (Parse_ast.Unknown,())) in
+    let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, [], false), (Parse_ast.Unknown,())) in
 
     let forwards_spec, env = Type_check.check_val_spec env forwards_spec in
     let backwards_spec, env = Type_check.check_val_spec env backwards_spec in
@@ -4382,7 +4382,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
     let string_defs =
       begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then
               let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
-              let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+              let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in
               let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
               let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
               let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
@@ -4392,7 +4392,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
             else
               if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then
                 let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
-                let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+                let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in
                 let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
                 let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
                 let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
diff --git a/src/type_check.ml b/src/type_check.ml
index cf1d8ef9..16690696 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -392,7 +392,7 @@ module Env : sig
   val add_overloads : id -> id list -> t -> t
   val get_overloads : id -> t -> id list
   val is_extern : id -> t -> string -> bool
-  val add_extern : id -> (string -> string option) -> t -> t
+  val add_extern : id -> (string * string) list -> t -> t
   val get_extern : id -> t -> string -> string
   val get_default_order : t -> order
   val set_default_order : order_aux -> t -> t
@@ -459,7 +459,7 @@ end = struct
       enums : IdSet.t Bindings.t;
       records : (typquant * (typ * id) list) Bindings.t;
       accessors : (typquant * typ) Bindings.t;
-      externs : (string -> string option) Bindings.t;
+      externs : (string * string) list Bindings.t;
       smt_ops : string Bindings.t;
       constraint_synonyms : (kid list * n_constraint) Bindings.t;
       casts : id list;
@@ -1073,7 +1073,7 @@ end = struct
     | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id)
 
   let is_extern id env backend =
-    try not (Bindings.find id env.externs backend = None) with
+    try not (Ast_util.extern_assoc backend (Bindings.find id env.externs) = None) with
     | Not_found -> false
     (* Bindings.mem id env.externs *)
 
@@ -1082,7 +1082,7 @@ end = struct
 
   let get_extern id env backend =
     try
-      match Bindings.find id env.externs backend with
+      match Ast_util.extern_assoc backend (Bindings.find id env.externs) with
       | Some ext -> ext
       | None -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id)
     with
@@ -4353,7 +4353,7 @@ let mk_val_spec env typq typ id =
     | Typ_aux (Typ_fn (_,_,eff),_) -> eff
     | _ -> no_effect
   in
-  DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, (fun _ -> None), false), (Parse_ast.Unknown, Some ((env,typ,eff),None))))
+  DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, [], false), (Parse_ast.Unknown, Some ((env,typ,eff),None))))
 
 let check_tannotopt env typq ret_typ = function
   | Typ_annot_opt_aux (Typ_annot_opt_none, _) -> ()
@@ -4449,16 +4449,16 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md
 let check_val_spec env (VS_aux (vs, (l, _))) =
   let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, Some ((env, typ, eff), None)))) in
   let vs, id, typq, typ, env = match vs with
-    | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, ext_opt, is_cast) ->
+    | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, exts, is_cast) ->
        typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm));
-       let env = match (ext_opt "smt", ext_opt "#") with
+       let env = match (Ast_util.extern_assoc "smt" exts, Ast_util.extern_assoc "#" exts) with
          | Some op, None -> Env.add_smt_op id op env
          | _, _ -> env
        in
-       let env = Env.add_extern id ext_opt env in
+       let env = Env.add_extern id exts env in
        let env = if is_cast then Env.add_cast id env else env in
        let typq, typ = expand_bind_synonyms ts_l env (typq, typ) in
-       let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in
+       let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, exts, is_cast) in
        (vs, id, typq, typ, env)
   in
   let eff =
@@ -4626,13 +4626,13 @@ let initial_env =
   (* |> Env.add_val_spec (mk_id "int")
    *      (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), Typ_aux (Typ_bidir (int_typ, string_typ), Parse_ast.Unknown)) *)
 
-  |> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "size_itself_int")
+  |> Env.add_extern (mk_id "size_itself_int") [("_", "size_itself_int")]
   |> Env.add_val_spec (mk_id "size_itself_int")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
                                   Parse_ast.Unknown)],Parse_ast.Unknown),
        function_typ [app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]]
          (atom_typ (nvar (mk_kid "n"))) no_effect)
-  |> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "make_the_value")
+  |> Env.add_extern (mk_id "make_the_value") [("_", "make_the_value")]
   |> Env.add_val_spec (mk_id "make_the_value")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
                                   Parse_ast.Unknown)],Parse_ast.Unknown),