Jib: Refactor initializers

The init instruction used to just have the form:
```
ctyp id = cval
```
which was always equivalent to:
```
ctyp id
id = cval
```

However this doesn't work with some C and C++ constructs where we want
to generate something that is only valid as an initializer, i.e.
```C
const_sail_string[] = {"Hello", "World"};
```

To fix this the init instruction has the form
```
ctyp id = init
```
where `init` can either be a plain cval as before or a special initializer
form that can't be split into two instructions. Before this patch we just had
to hope that the cval that compiled into an initializer wouldn't be constant
propagated, but with this that is statically guaranteed.

language/jib.ott

@@ -138,7 +138,6 @@ cval :: 'V_' ::=
   | cval nat0 nat1                                  :: :: tuple_member
   | op ( cval0 , ... , cvaln )                      :: :: call
   | cval . id                                       :: :: field
-  | string0 . ... . stringn                         :: :: config_key
 
 % Note that init / clear are sometimes referred to as create / kill
 
@@ -225,12 +224,16 @@ creturn :: 'CR_' ::=
   | clexp                     :: :: one
   | ( clexp0 , ... , clexpn ) :: :: multi
 
+init :: 'Init_' ::=
+  | cval                             :: :: cval
+  | json_key string0 . ... . stringn :: :: json_key
+
 instr :: 'I_' ::=
   {{ aux _ iannot }}
 % The following are the minimal set of instructions output by
 % Jib_compile.ml.
   | ctyp name                                      :: :: decl
-  | ctyp name = cval                               :: :: init
+  | ctyp name = init                               :: :: init
   | jump ( cval ) string                           :: :: jump
   | goto string                                    :: :: goto
   | string :                                       :: :: label

src/lib/jib_compile.ml

@@ -648,7 +648,7 @@ module Make (C : CONFIG) = struct
     in
     let key_name = ngensym () in
     let args = [V_lit (VL_int (Big_int.of_int (List.length key)), CT_fint 64); V_id (key_name, CT_json_key)] in
-    let key_init = [iinit l CT_json_key key_name (V_config_key key)] in
+    let key_init = [ijson_key l key_name key] in
 
     let config_extract ctyp ~validate ~extract =
       let json = ngensym () in

src/lib/jib_optimize.ml

@@ -151,7 +151,6 @@ let rec cval_subst id subst = function
   | V_ctor_unwrap (cval, ctor, ctyp) -> V_ctor_unwrap (cval_subst id subst cval, ctor, ctyp)
   | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> (field, cval_subst id subst cval)) fields, ctyp)
   | V_tuple (members, ctyp) -> V_tuple (List.map (cval_subst id subst) members, ctyp)
-  | V_config_key parts -> V_config_key parts
 
 let rec cval_map_id f = function
   | V_id (id, ctyp) -> V_id (f id, ctyp)
@@ -164,7 +163,6 @@ let rec cval_map_id f = function
   | V_ctor_unwrap (cval, ctor, ctyp) -> V_ctor_unwrap (cval_map_id f cval, ctor, ctyp)
   | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> (field, cval_map_id f cval)) fields, ctyp)
   | V_tuple (members, ctyp) -> V_tuple (List.map (cval_map_id f) members, ctyp)
-  | V_config_key parts -> V_config_key parts
 
 module Remove_undefined = struct
   open Jib
@@ -242,10 +240,13 @@ end
 
 let remove_functions_to_references = Jib_visitor.visit_instrs (new Remove_functions_to_references.visitor)
 
+let init_subst id subst init =
+  match init with Init_cval cval -> Init_cval (cval_subst id subst cval) | Init_json_key _ -> init
+
 let rec instrs_subst id subst = function
   | I_aux (I_decl (_, id'), _) :: _ as instrs when Name.compare id id' = 0 -> instrs
-  | I_aux (I_init (ctyp, id', cval), aux) :: rest when Name.compare id id' = 0 ->
-      I_aux (I_init (ctyp, id', cval_subst id subst cval), aux) :: rest
+  | I_aux (I_init (ctyp, id', init), aux) :: rest when Name.compare id id' = 0 ->
+      I_aux (I_init (ctyp, id', init_subst id subst init), aux) :: rest
   | I_aux (I_reset (_, id'), _) :: _ as instrs when Name.compare id id' = 0 -> instrs
   | I_aux (I_reinit (ctyp, id', cval), aux) :: rest when Name.compare id id' = 0 ->
       I_aux (I_reinit (ctyp, id', cval_subst id subst cval), aux) :: rest
@@ -254,7 +255,7 @@ let rec instrs_subst id subst = function
       let instr =
         match instr with
         | I_decl (ctyp, id') -> I_decl (ctyp, id')
-        | I_init (ctyp, id', cval) -> I_init (ctyp, id', cval_subst id subst cval)
+        | I_init (ctyp, id', init) -> I_init (ctyp, id', init_subst id subst init)
         | I_jump (cval, label) -> I_jump (cval_subst id subst cval, label)
         | I_goto label -> I_goto label
         | I_label label -> I_label label
@@ -335,7 +336,7 @@ let inline cdefs should_inline instrs =
   let fix_substs =
     let f = cval_map_id (ssa_name (-1)) in
     function
-    | I_aux (I_init (ctyp, id, cval), aux) -> I_aux (I_init (ctyp, id, f cval), aux)
+    | I_aux (I_init (ctyp, id, Init_cval cval), aux) -> I_aux (I_init (ctyp, id, Init_cval (f cval)), aux)
     | I_aux (I_jump (cval, label), aux) -> I_aux (I_jump (f cval, label), aux)
     | I_aux (I_funcall (clexp, extern, function_id, args), aux) ->
         I_aux (I_funcall (clexp, extern, function_id, List.map f args), aux)
@@ -504,7 +505,6 @@ let remove_tuples cdefs ctx =
     | V_id (id, ctyp) -> V_id (id, ctyp)
     | V_member (id, ctyp) -> V_member (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
-    | V_config_key parts -> V_config_key parts
     | V_ctor_kind (cval, ctor, ctyp) -> V_ctor_kind (fix_cval cval, ctor, ctyp)
     | V_ctor_unwrap (cval, ctor, ctyp) -> V_ctor_unwrap (fix_cval cval, ctor, ctyp)
     | V_tuple_member (cval, _, n) ->
@@ -547,10 +547,11 @@ let remove_tuples cdefs ctx =
     | CR_one clexp -> CR_one (fix_clexp clexp)
     | CR_multi clexps -> CR_multi (List.map fix_clexp clexps)
   in
+  let fix_init = function Init_cval cval -> Init_cval (fix_cval cval) | Init_json_key parts -> Init_json_key parts in
   let rec fix_instr_aux = function
     | I_funcall (creturn, extern, id, args) -> I_funcall (fix_creturn creturn, extern, id, List.map fix_cval args)
     | I_copy (clexp, cval) -> I_copy (fix_clexp clexp, fix_cval cval)
-    | I_init (ctyp, id, cval) -> I_init (ctyp, id, fix_cval cval)
+    | I_init (ctyp, id, init) -> I_init (ctyp, id, fix_init init)
     | I_reinit (ctyp, id, cval) -> I_reinit (ctyp, id, fix_cval cval)
     | I_jump (cval, label) -> I_jump (fix_cval cval, label)
     | I_throw cval -> I_throw (fix_cval cval)

src/lib/jib_ssa.ml

@@ -541,7 +541,6 @@ let rename_variables globals graph root children =
         )
     | V_member (id, ctyp) -> V_member (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
-    | V_config_key parts -> V_config_key parts
     | V_call (id, fs) -> V_call (id, List.map fold_cval fs)
     | V_field (f, field) -> V_field (fold_cval f, field)
     | V_tuple_member (f, len, n) -> V_tuple_member (fold_cval f, len, n)
@@ -551,6 +550,11 @@ let rename_variables globals graph root children =
     | V_tuple (members, ctyp) -> V_tuple (List.map fold_cval members, ctyp)
   in
 
+  let fold_init = function
+    | Init_cval cval -> Init_cval (fold_cval cval)
+    | Init_json_key parts -> Init_json_key parts
+  in
+
   let rec fold_clexp rmw = function
     | CL_id (id, ctyp) when rmw ->
         let i = top_stack id in
@@ -588,12 +592,12 @@ let rename_variables globals graph root children =
           counts := NameMap.add id i !counts;
           push_stack id i;
           I_decl (ctyp, ssa_name i id)
-      | I_init (ctyp, id, cval) ->
-          let cval = fold_cval cval in
+      | I_init (ctyp, id, init) ->
+          let init = fold_init init in
           let i = get_count id + 1 in
           counts := NameMap.add id i !counts;
           push_stack id i;
-          I_init (ctyp, ssa_name i id, cval)
+          I_init (ctyp, ssa_name i id, init)
       | instr -> instr
     in
     I_aux (aux, annot)

src/lib/jib_util.ml

@@ -76,7 +76,9 @@ let idecl l ctyp id = I_aux (I_decl (ctyp, id), (instr_number (), l))
 
 let ireset l ctyp id = I_aux (I_reset (ctyp, id), (instr_number (), l))
 
-let iinit l ctyp id cval = I_aux (I_init (ctyp, id, cval), (instr_number (), l))
+let iinit l ctyp id cval = I_aux (I_init (ctyp, id, Init_cval cval), (instr_number (), l))
+
+let ijson_key l id parts = I_aux (I_init (CT_json_key, id, Init_json_key parts), (instr_number (), l))
 
 let iif l cval then_instrs else_instrs ctyp = I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l))
 
@@ -333,7 +335,6 @@ let rec string_of_cval = function
       | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Struct without struct type found"
     end
   | V_tuple (members, _) -> "(" ^ Util.string_of_list ", " string_of_cval members ^ ")"
-  | V_config_key parts -> "config " ^ String.concat "." parts
 
 let rec string_of_clexp = function
   | CL_id (id, ctyp) -> string_of_name id
@@ -347,14 +348,18 @@ let string_of_creturn = function
   | CR_one clexp -> string_of_clexp clexp
   | CR_multi clexps -> "(" ^ Util.string_of_list ", " string_of_clexp clexps ^ ")"
 
+let string_of_init = function
+  | Init_cval cval -> string_of_cval cval
+  | Init_json_key parts -> Util.string_of_list "." (fun part -> "\"" ^ part ^ "\"") parts
+
 let rec doc_instr (I_aux (aux, _)) =
   let open Printf in
   let instr s = twice space ^^ string s in
   match aux with
   | I_decl (ctyp, id) -> ksprintf instr "%s : %s" (string_of_name id) (string_of_ctyp ctyp)
   | I_reset (ctyp, id) -> ksprintf instr "reset %s : %s" (string_of_name id) (string_of_ctyp ctyp)
-  | I_init (ctyp, id, cval) ->
-      ksprintf instr "%s : %s = %s" (string_of_name id) (string_of_ctyp ctyp) (string_of_cval cval)
+  | I_init (ctyp, id, init) ->
+      ksprintf instr "%s : %s = %s" (string_of_name id) (string_of_ctyp ctyp) (string_of_init init)
   | I_reinit (ctyp, id, cval) ->
       ksprintf instr "reinit %s : %s = %s" (string_of_name id) (string_of_ctyp ctyp) (string_of_cval cval)
   | I_clear (ctyp, id) -> ksprintf instr "clear %s : %s" (string_of_name id) (string_of_ctyp ctyp)
@@ -663,7 +668,7 @@ let rec is_polymorphic = function
 
 let rec cval_deps = function
   | V_id (id, _) -> NameSet.singleton id
-  | V_lit _ | V_member _ | V_config_key _ -> NameSet.empty
+  | V_lit _ | V_member _ -> NameSet.empty
   | V_field (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval
   | V_call (_, cvals) | V_tuple (cvals, _) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals)
   | V_ctor_kind (cval, _, _) -> cval_deps cval
@@ -688,11 +693,14 @@ let creturn_deps = function
         )
         (NameSet.empty, NameSet.empty) clexps
 
+let init_deps = function Init_cval cval -> cval_deps cval | Init_json_key _ -> NameSet.empty
+
 (* Return the direct, read/write dependencies of a single instruction *)
 let instr_deps = function
   | I_decl (_, id) -> (NameSet.empty, NameSet.singleton id)
   | I_reset (_, id) -> (NameSet.empty, NameSet.singleton id)
-  | I_init (_, id, cval) | I_reinit (_, id, cval) -> (cval_deps cval, NameSet.singleton id)
+  | I_init (_, id, init) -> (init_deps init, NameSet.singleton id)
+  | I_reinit (_, id, cval) -> (cval_deps cval, NameSet.singleton id)
   | I_if (cval, _, _, _) -> (cval_deps cval, NameSet.empty)
   | I_jump (cval, _) -> (cval_deps cval, NameSet.empty)
   | I_funcall (creturn, _, _, cvals) ->
@@ -754,7 +762,6 @@ let rec map_cval_ctyp f = function
   | V_id (id, ctyp) -> V_id (id, f ctyp)
   | V_member (id, ctyp) -> V_member (id, f ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, f ctyp)
-  | V_config_key parts -> V_config_key parts
   | V_ctor_kind (cval, (id, unifiers), ctyp) -> V_ctor_kind (map_cval_ctyp f cval, (id, List.map f unifiers), f ctyp)
   | V_ctor_unwrap (cval, (id, unifiers), ctyp) -> V_ctor_unwrap (map_cval_ctyp f cval, (id, List.map f unifiers), f ctyp)
   | V_tuple_member (cval, i, j) -> V_tuple_member (map_cval_ctyp f cval, i, j)
@@ -767,11 +774,14 @@ let map_creturn_ctyp f = function
   | CR_one clexp -> CR_one (map_clexp_ctyp f clexp)
   | CR_multi clexps -> CR_multi (List.map (map_clexp_ctyp f) clexps)
 
+let map_init_ctyp f init =
+  match init with Init_cval cval -> Init_cval (map_cval_ctyp f cval) | Init_json_key _ -> init
+
 let rec map_instr_ctyp f (I_aux (instr, aux)) =
   let instr =
     match instr with
     | I_decl (ctyp, id) -> I_decl (f ctyp, id)
-    | I_init (ctyp, id, cval) -> I_init (f ctyp, id, map_cval_ctyp f cval)
+    | I_init (ctyp, id, init) -> I_init (f ctyp, id, map_init_ctyp f init)
     | I_if (cval, then_instrs, else_instrs, ctyp) ->
         I_if
           ( map_cval_ctyp f cval,
@@ -1038,7 +1048,6 @@ and cval_ctyp = function
   | V_struct (_, ctyp) -> ctyp
   | V_tuple (_, ctyp) -> ctyp
   | V_call (op, vs) -> infer_call op vs
-  | V_config_key _ -> CT_json_key
 
 let rec clexp_ctyp = function
   | CL_id (_, ctyp) -> ctyp
@@ -1066,10 +1075,13 @@ let rec clexp_ctyp = function
 
 let creturn_ctyp = function CR_one clexp -> clexp_ctyp clexp | CR_multi clexps -> CT_tup (List.map clexp_ctyp clexps)
 
+let init_ctyps = function Init_cval cval -> CTSet.singleton (cval_ctyp cval) | Init_json_key _ -> CTSet.empty
+
 let rec instr_ctyps (I_aux (instr, aux)) =
   match instr with
   | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) | I_undefined ctyp -> CTSet.singleton ctyp
-  | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> CTSet.add ctyp (CTSet.singleton (cval_ctyp cval))
+  | I_init (ctyp, _, init) -> CTSet.add ctyp (init_ctyps init)
+  | I_reinit (ctyp, _, cval) -> CTSet.add ctyp (CTSet.singleton (cval_ctyp cval))
   | I_if (cval, instrs1, instrs2, ctyp) ->
       CTSet.union (instrs_ctyps instrs1) (instrs_ctyps instrs2) |> CTSet.add (cval_ctyp cval) |> CTSet.add ctyp
   | I_funcall (creturn, _, (_, ctyps), cvals) ->

src/lib/jib_util.mli

@@ -60,6 +60,7 @@ val symbol_generator : string -> (unit -> id) * (unit -> unit)
 val idecl : l -> ctyp -> name -> instr
 val ireset : l -> ctyp -> name -> instr
 val iinit : l -> ctyp -> name -> cval -> instr
+val ijson_key : l -> name -> string list -> instr
 val iif : l -> cval -> instr list -> instr list -> ctyp -> instr
 val ifuncall : l -> clexp -> id * ctyp list -> cval list -> instr
 val ifuncall_multi : l -> clexp list -> id * ctyp list -> cval list -> instr

src/lib/jib_visitor.ml

@@ -164,7 +164,6 @@ let rec visit_cval vis outer_cval =
         let cval' = visit_cval vis cval in
         let id' = visit_id vis id in
         if cval == cval' && id == id' then no_change else V_field (cval', id')
-    | V_config_key _ -> no_change
   in
   do_visit vis (vis#vcval outer_cval) aux outer_cval
 
@@ -175,18 +174,25 @@ and visit_field vis ((id, cval) as field) =
 
 and visit_cvals vis cvals = map_no_copy (visit_cval vis) cvals
 
+let visit_init vis no_change =
+  match no_change with
+  | Init_cval cval ->
+      let cval' = visit_cval vis cval in
+      if cval == cval' then no_change else Init_cval cval'
+  | Init_json_key _ -> no_change
+
 let rec visit_instr vis outer_instr =
   let aux vis no_change =
     match no_change with
     | I_aux (I_decl (ctyp, name), aux) ->
         let ctyp' = visit_ctyp vis ctyp in
         let name' = visit_name vis name in
         if ctyp == ctyp' && name == name' then no_change else I_aux (I_decl (ctyp', name'), aux)
-    | I_aux (I_init (ctyp, name, cval), aux) ->
+    | I_aux (I_init (ctyp, name, init), aux) ->
         let ctyp' = visit_ctyp vis ctyp in
         let name' = visit_name vis name in
-        let cval' = visit_cval vis cval in
-        if ctyp == ctyp' && name == name' && cval == cval' then no_change else I_aux (I_init (ctyp', name', cval'), aux)
+        let init' = visit_init vis init in
+        if ctyp == ctyp' && name == name' && init == init' then no_change else I_aux (I_init (ctyp', name', init'), aux)
     | I_aux (I_jump (cval, label), aux) ->
         let cval' = visit_cval vis cval in
         if cval == cval' then no_change else I_aux (I_jump (cval', label), aux)

src/lib/smt_gen.ml

@@ -427,10 +427,6 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
         | V_tuple _ | V_tuple_member _ ->
             let* l = current_location in
             Reporting.unreachable l __POS__ "Found tuple value, which should have been removed before SMT generation"
-        | V_config_key _ ->
-            let* l = current_location in
-            Reporting.unreachable l __POS__
-              "Found config key value, which should have been removed before SMT generation"
       )
 
   (* [bvzeint esz cval] (BitVector Zero Extend INTeger), takes a cval

src/sail_c_backend/c_backend.ml

@@ -716,7 +716,7 @@ let hoist_allocations recursive_functions = function
             cleanups := iclear ctyp hid :: !cleanups;
             let instrs = instrs_rename decl_id hid instrs in
             I_aux (I_reset (ctyp, hid), annot) :: hoist instrs
-        | I_aux (I_init (ctyp, decl_id, cval), annot) :: instrs when hoist_ctyp ctyp ->
+        | I_aux (I_init (ctyp, decl_id, Init_cval cval), annot) :: instrs when hoist_ctyp ctyp ->
             let hid = hoist_id () in
             decls := idecl (snd annot) ctyp hid :: !decls;
             cleanups := iclear ctyp hid :: !cleanups;
@@ -973,8 +973,6 @@ let rec sgen_cval = function
       Printf.sprintf "{%s}"
         (Util.string_of_list ", " (fun (field, cval) -> zencode_id field ^ " = " ^ sgen_cval cval) fields)
   | V_ctor_unwrap (f, ctor, _) -> Printf.sprintf "%s.variants.%s" (sgen_cval f) (sgen_uid ctor)
-  | V_config_key parts ->
-      Printf.sprintf "(const_sail_string[]){%s}" (Util.string_of_list ", " (fun part -> "\"" ^ part ^ "\"") parts)
   | V_tuple _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for a tuple literal"
 
 and sgen_call op cvals =
@@ -1324,11 +1322,14 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
       else string (Printf.sprintf "  %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp l x) c_args)
   | I_clear (ctyp, _) when is_stack_ctyp ctyp -> empty
   | I_clear (ctyp, id) -> sail_kill ~prefix:"  " ~suffix:";" (sgen_ctyp_name ctyp) "&%s" (sgen_name id)
-  | I_init (CT_json_key, id, V_config_key parts) ->
-      ksprintf string "  sail_config_key %s = {%s};" (sgen_name id)
-        (Util.string_of_list ", " (fun part -> "\"" ^ part ^ "\"") parts)
-  | I_init (ctyp, id, cval) ->
-      codegen_instr fid ctx (idecl l ctyp id) ^^ hardline ^^ codegen_conversion l (CL_id (id, ctyp)) cval
+  | I_init (ctyp, id, init) -> (
+      match init with
+      | Init_cval cval ->
+          codegen_instr fid ctx (idecl l ctyp id) ^^ hardline ^^ codegen_conversion l (CL_id (id, ctyp)) cval
+      | Init_json_key parts ->
+          ksprintf string "  sail_config_key %s = {%s};" (sgen_name id)
+            (Util.string_of_list ", " (fun part -> "\"" ^ part ^ "\"") parts)
+    )
   | I_reinit (ctyp, id, cval) ->
       codegen_instr fid ctx (ireset l ctyp id) ^^ hardline ^^ codegen_conversion l (CL_id (id, ctyp)) cval
   | I_reset (ctyp, id) when is_stack_ctyp ctyp -> string (Printf.sprintf "  %s %s;" (sgen_ctyp ctyp) (sgen_name id))

src/sail_smt_backend/jib_smt.ml

@@ -585,7 +585,7 @@ module Make (Config : CONFIG) = struct
               singleton (define_const id ret_ctyp (Fn (zencode_id function_id, smt_args)))
         )
         else failwith ("Unrecognised function " ^ string_of_id function_id)
-    | I_init (ctyp, id, cval) | I_copy (CL_id (id, ctyp), cval) ->
+    | I_init (ctyp, id, Init_cval cval) | I_copy (CL_id (id, ctyp), cval) ->
         let* smt = Smt.smt_cval cval in
         let* smt = Smt.smt_conversion ~into:ctyp ~from:(cval_ctyp cval) smt in
         singleton (define_const id ctyp smt)

src/sail_sv_backend/jib_sv.ml

@@ -1279,9 +1279,13 @@ module Make (Config : CONFIG) = struct
     match aux with
     | I_comment str -> wrap (SVS_comment str)
     | I_decl (ctyp, id) -> wrap (SVS_var (id, ctyp, None))
-    | I_init (ctyp, id, cval) ->
-        let* value = Smt.smt_cval cval in
-        wrap (SVS_var (id, ctyp, Some value))
+    | I_init (ctyp, id, init) -> (
+        match init with
+        | Init_cval cval ->
+            let* value = Smt.smt_cval cval in
+            wrap (SVS_var (id, ctyp, Some value))
+        | Init_json_key _ -> Reporting.unreachable l __POS__ "Json key found in SV backend"
+      )
     | I_return cval ->
         let* value = Smt.smt_cval cval in
         wrap (SVS_return value)
@@ -2482,7 +2486,7 @@ module Make (Config : CONFIG) = struct
         (fun (decls, others) instr ->
           match instr with
           | I_aux (I_decl (ctyp, id), (_, l)) -> (idecl l ctyp id :: decls, others)
-          | I_aux (I_init (ctyp, id, cval), (_, l)) ->
+          | I_aux (I_init (ctyp, id, Init_cval cval), (_, l)) ->
               (idecl l ctyp id :: decls, icopy l (CL_id (id, ctyp)) cval :: others)
           | other -> (decls, other :: others)
         )