Replace Ctypes.typelist by list Ctypes.type

It makes the Coq and OCaml codes more legible, and avoids some typelist/list
conversions.

cfrontend/C2C.ml

@@ -311,9 +311,8 @@ let make_builtin_memcpy args =
       if not (Z.eq (Z.modulo sz1 al1) Z.zero) then
         error "alignment argument of '__builtin_memcpy_aligned' must be a divisor of the size";
       (* Issue #28: must decay array types to pointer types *)
-      Ebuiltin( AST.EF_memcpy(sz1, al1),
-               Tcons(typeconv(typeof dst),
-                     Tcons(typeconv(typeof src), Tnil)),
+      Ebuiltin(AST.EF_memcpy(sz1, al1),
+               [typeconv(typeof dst); typeconv(typeof src)],
                Econs(dst, Econs(src, Enil)), Tvoid)
   | _ ->
     assert false
@@ -328,7 +327,7 @@ let va_list_ptr e =
 
 let make_builtin_va_arg_by_val helper ty ty_ret arg =
   let ty_fun =
-    Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret,  AST.cc_default) in
+    Tfunction([Tpointer(Tvoid, noattr)], ty_ret,  AST.cc_default) in
   Ecast
     (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
            Econs(va_list_ptr arg, Enil),
@@ -337,7 +336,7 @@ let make_builtin_va_arg_by_val helper ty ty_ret arg =
 
 let make_builtin_va_arg_by_ref helper ty arg =
   let ty_fun =
-    Tfunction(Tcons(Tpointer(Tvoid, noattr), Tcons(Ctyping.size_t, Tnil)),
+    Tfunction([Tpointer(Tvoid, noattr); Ctyping.size_t],
               Tpointer(Tvoid, noattr),  AST.cc_default) in
   let ty_ptr =
     Tpointer(ty, noattr) in
@@ -464,7 +463,7 @@ let rec convertTyp env ?bitwidth t =
   | C.TFun(tres, targs, va, a) ->
       checkFunctionType env tres targs;
       Tfunction(begin match targs with
-                | None -> Tnil
+                | None -> []
                 | Some tl -> convertParams env tl
                 end,
                 convertTyp env tres,
@@ -493,8 +492,8 @@ let rec convertTyp env ?bitwidth t =
       convertIkind ik (convertAttr a)
 
 and convertParams env = function
-    | [] -> Tnil
-    | (id, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem)
+    | [] -> []
+    | (id, ty) :: rem -> convertTyp env ty :: convertParams env rem
 
 (* Convert types for the arguments to a function call.  The types for
    fixed arguments are taken from the function prototype.  The types
@@ -504,12 +503,12 @@ and convertParams env = function
 
 let rec convertTypArgs env tl el =
   match tl, el with
-  | _, [] -> Tnil
+  | _, [] -> []
   | [], e1 :: el ->
-      Tcons(convertTyp env (Cutil.default_argument_conversion env e1.etyp),
-            convertTypArgs env [] el)
+      convertTyp env (Cutil.default_argument_conversion env e1.etyp) ::
+      convertTypArgs env [] el
   | (id, t1) :: tl, e1 :: el ->
-      Tcons(convertTyp env t1, convertTypArgs env tl el)
+      convertTyp env t1 :: convertTypArgs env tl el
 
 (* Convert types for the arguments to inline asm statements and to
    the special built-in functions __builtin_annot, __builtin_ais_annot_
@@ -520,10 +519,10 @@ let rec convertTypArgs env tl el =
    and avoid inserting compiled code to convert the arguments. *)
 
 let rec convertTypAnnotArgs env = function
-  | [] -> Tnil
+  | [] -> []
   | e1 :: el ->
-      Tcons(convertTyp env (Cutil.unary_conversion env e1.etyp),
-            convertTypAnnotArgs env el)
+      convertTyp env (Cutil.unary_conversion env e1.etyp) ::
+      convertTypAnnotArgs env el
 
 let convertField env sid f =
   let id = intern_string f.fld_name
@@ -893,7 +892,7 @@ let rec convertExpr env e =
           let targ = convertTyp env
                          (Cutil.default_argument_conversion env arg.etyp) in
           Ebuiltin(AST.EF_annot_val(P.of_int 1,coqstring_of_camlstring txt, typ_of_type targ),
-                   Tcons(targ, Tnil), convertExprList env [arg],
+                   [targ], convertExprList env [arg],
                    convertTyp env e.etyp)
       | _ ->
           error "argument 1 of '__builtin_annot_intval' must be a string literal";
@@ -936,9 +935,8 @@ let rec convertExpr env e =
   | C.ECall({edesc = C.EVar {name = "__builtin_va_copy"}}, [arg1; arg2]) ->
       let dst = convertExpr env arg1 in
       let src = convertExpr env arg2 in
-      Ebuiltin( AST.EF_memcpy(Z.of_uint CBuiltins.size_va_list, Z.of_uint 4),
-               Tcons(Tpointer(Tvoid, noattr),
-                 Tcons(Tpointer(Tvoid, noattr), Tnil)),
+      Ebuiltin(AST.EF_memcpy(Z.of_uint CBuiltins.size_va_list, Z.of_uint 4),
+               [Tpointer(Tvoid, noattr); Tpointer(Tvoid, noattr)],
                Econs(va_list_ptr dst, Econs(va_list_ptr src, Enil)),
                Tvoid)
 
@@ -1363,8 +1361,6 @@ let helper_functions () = [
 ]
 
 let helper_function_declaration (name, tyres, tyargs) =
-  let tyargs =
-    List.fold_right (fun t tl -> Tcons(t, tl)) tyargs Tnil in
   let ef =
     AST.EF_runtime(coqstring_of_camlstring name,
                    signature_of_type tyargs tyres AST.cc_default) in

cfrontend/Cexec.v

@@ -717,10 +717,10 @@ Section EXPRS.
 Variable e: env.
 Variable w: world.
 
-Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) (m: mem) : option (list val) :=
+Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: list type) (m: mem) : option (list val) :=
   match vtl, tl with
-  | nil, Tnil => Some nil
-  | (v1,t1)::vtl, Tcons t1' tl =>
+  | nil, nil => Some nil
+  | (v1,t1)::vtl, t1'::tl =>
       do v <- sem_cast v1 t1 t1' m; do vl <- sem_cast_arguments vtl tl m; Some(v::vl)
   | _, _ => None
   end.
@@ -2308,7 +2308,7 @@ Definition do_initial_state (p: program): option (genv * state) :=
   do m0 <- Genv.init_mem p;
   do b <- Genv.find_symbol ge p.(prog_main);
   do f <- Genv.find_funct_ptr ge b;
-  check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s cc_default));
+  check (type_eq (type_of_fundef f) (Tfunction nil type_int32s cc_default));
   Some (ge, Callstate f nil Kstop m0).
 
 Definition at_final_state (S: state): option int :=

cfrontend/Clight.v

@@ -98,7 +98,7 @@ Inductive statement : Type :=
   | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *)
   | Sset : ident -> expr -> statement   (**r assignment [tempvar = rvalue] *)
   | Scall: option ident -> expr -> list expr -> statement (**r function call *)
-  | Sbuiltin: option ident -> external_function -> typelist -> list expr -> statement (**r builtin invocation *)
+  | Sbuiltin: option ident -> external_function -> list type -> list expr -> statement (**r builtin invocation *)
   | Ssequence : statement -> statement -> statement  (**r sequence *)
   | Sifthenelse : expr  -> statement -> statement -> statement (**r conditional *)
   | Sloop: statement -> statement -> statement (**r infinite loop *)
@@ -440,14 +440,14 @@ Combined Scheme eval_expr_lvalue_ind from eval_expr_ind2, eval_lvalue_ind2.
   and produces the list of cast values [vl].  It is used to
   evaluate the arguments of function calls. *)
 
-Inductive eval_exprlist: list expr -> typelist -> list val -> Prop :=
+Inductive eval_exprlist: list expr -> list type -> list val -> Prop :=
   | eval_Enil:
-      eval_exprlist nil Tnil nil
+      eval_exprlist nil nil nil
   | eval_Econs:   forall a bl ty tyl v1 v2 vl,
       eval_expr a v1 ->
       sem_cast v1 (typeof a) ty m = Some v2 ->
       eval_exprlist bl tyl vl ->
-      eval_exprlist (a :: bl) (Tcons ty tyl) (v2 :: vl).
+      eval_exprlist (a :: bl) (ty :: tyl) (v2 :: vl).
 
 End EXPR.
 
@@ -687,7 +687,7 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
+      type_of_fundef f = Tfunction nil type_int32s cc_default ->
       initial_state p (Callstate f nil Kstop m0).
 
 (** A final state is a [Returnstate] with an empty continuation. *)

cfrontend/ClightBigstep.v

@@ -255,7 +255,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
+      type_of_fundef f = Tfunction nil type_int32s cc_default ->
       eval_funcall ge m0 f nil t m1 (Vint r) ->
       bigstep_program_terminates p t r.
 
@@ -265,7 +265,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
+      type_of_fundef f = Tfunction nil type_int32s cc_default ->
       evalinf_funcall ge m0 f nil t ->
       bigstep_program_diverges p t.
 

cfrontend/Cop.v

@@ -1003,7 +1003,7 @@ Definition sem_cmp (c:comparison)
 (** ** Function applications *)
 
 Inductive classify_fun_cases : Type :=
-  | fun_case_f (targs: typelist) (tres: type) (cc: calling_convention) (**r (pointer to) function *)
+  | fun_case_f (targs: list type) (tres: type) (cc: calling_convention) (**r (pointer to) function *)
   | fun_default.
 
 Definition classify_fun (ty: type) :=

cfrontend/Csem.v

@@ -191,12 +191,12 @@ Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement :=
 
 (** Extract the values from a list of function arguments *)
 
-Inductive cast_arguments (m: mem): exprlist -> typelist -> list val -> Prop :=
+Inductive cast_arguments (m: mem): exprlist -> list type -> list val -> Prop :=
   | cast_args_nil:
-      cast_arguments m Enil Tnil nil
+      cast_arguments m Enil nil nil
   | cast_args_cons: forall v ty el targ1 targs v1 vl,
       sem_cast v ty targ1 m = Some v1 -> cast_arguments m el targs vl ->
-      cast_arguments m (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl).
+      cast_arguments m (Econs (Eval v ty) el) (targ1 :: targs) (v1 :: vl).
 
 (** ** Reduction semantics for expressions *)
 
@@ -832,7 +832,7 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
+      type_of_fundef f = Tfunction nil type_int32s cc_default ->
       initial_state p (Callstate f nil Kstop m0).
 
 (** A final state is a [Returnstate] with an empty continuation. *)

cfrontend/Cshmgen.v

@@ -578,36 +578,36 @@ with transl_lvalue (ce: composite_env) (a: Clight.expr) {struct a} : res (expr *
    casted to the corresponding types in [tyl].
    Used for function applications. *)
 
-Fixpoint transl_arglist (ce: composite_env) (al: list Clight.expr) (tyl: typelist)
+Fixpoint transl_arglist (ce: composite_env) (al: list Clight.expr) (tyl: list type)
                          {struct al}: res (list expr) :=
   match al, tyl with
-  | nil, Tnil => OK nil
-  | a1 :: a2, Tcons ty1 ty2 =>
+  | nil, nil => OK nil
+  | a1 :: a2, ty1 :: ty2 =>
       do ta1 <- transl_expr ce a1;
       do ta1' <- make_cast (typeof a1) ty1 ta1;
       do ta2 <- transl_arglist ce a2 ty2;
       OK (ta1' :: ta2)
-  | a1 :: a2, Tnil =>
+  | a1 :: a2, nil =>
       (* Tolerance for calls to K&R or variadic functions *)
       do ta1 <- transl_expr ce a1;
       do ta1' <- make_cast (typeof a1) (default_argument_conversion (typeof a1)) ta1;
-      do ta2 <- transl_arglist ce a2 Tnil;
+      do ta2 <- transl_arglist ce a2 nil;
       OK (ta1' :: ta2)
   | _, _ =>
       Error(msg "Cshmgen.transl_arglist: arity mismatch")
   end.
 
 (** Compute the argument signature that corresponds to a function application. *)
 
-Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist)
+Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: list type)
                             {struct al}: list AST.typ :=
   match al, tyl with
   | nil, _ => nil
-  | a1 :: a2, Tcons ty1 ty2 =>
+  | a1 :: a2, cons ty1 ty2 =>
       typ_of_type ty1 :: typlist_of_arglist a2 ty2
-  | a1 :: a2, Tnil =>
+  | a1 :: a2, nil =>
       (* Tolerance for calls to K&R or variadic functions *)
-      typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil
+      typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 nil
   end.
 
 (** Translate a function call.

cfrontend/Cshmgenproof.v

@@ -41,30 +41,21 @@ Proof.
   eexact H.
 - intros. destruct f; simpl in H0.
 + monadInv H0. constructor; auto.
-+ destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H0.
++ destruct signature_eq; inv H0.
   constructor; auto.
 - intros; red; auto.
 Qed.
 
 (** * Properties of operations over types *)
 
-Remark transl_params_types:
-  forall params,
-  map typ_of_type (map snd params) = typlist_of_typelist (type_of_params params).
-Proof.
-  induction params; simpl. auto. destruct a as [id ty]; simpl. f_equal; auto.
-Qed.
-
 Lemma transl_fundef_sig1:
   forall ce f tf args res cc,
   match_fundef ce f tf ->
   classify_fun (type_of_fundef f) = fun_case_f args res cc ->
   funsig tf = signature_of_type args res cc.
 Proof.
   intros. inv H.
-- monadInv H1. simpl. inversion H0.
-  unfold signature_of_function, signature_of_type.
-  f_equal. apply transl_params_types.
+- monadInv H1. simpl. inversion H0. reflexivity.
 - simpl in H0. unfold funsig. congruence.
 Qed.
 
@@ -1940,7 +1931,7 @@ Proof.
   exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C).
   assert (D: Genv.find_symbol tge (AST.prog_main tprog) = Some b).
   { destruct TRANSL as (P & Q & R). rewrite Q. rewrite symbols_preserved. auto. }
-  assert (E: funsig tf = signature_of_type Tnil type_int32s cc_default).
+  assert (E: funsig tf = signature_of_type nil type_int32s cc_default).
   { eapply transl_fundef_sig2; eauto. }
   econstructor; split.
   econstructor; eauto. apply (Genv.init_mem_match TRANSL). eauto.

cfrontend/Cstrategy.v

@@ -140,13 +140,13 @@ with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_alignof: forall ty1 ty,
       eval_simple_rvalue (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))).
 
-Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop :=
+Inductive eval_simple_list: exprlist -> list type -> list val -> Prop :=
   | esrl_nil:
-      eval_simple_list Enil Tnil nil
+      eval_simple_list Enil nil nil
   | esrl_cons: forall r rl ty tyl v vl v',
       eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty m = Some v ->
       eval_simple_list rl tyl vl ->
-      eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl).
+      eval_simple_list (Econs r rl) (ty :: tyl) (v :: vl).
 
 Scheme eval_simple_rvalue_ind2 := Minimality for eval_simple_rvalue Sort Prop
   with eval_simple_lvalue_ind2 := Minimality for eval_simple_lvalue Sort Prop.
@@ -3032,7 +3032,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
+      type_of_fundef f = Tfunction nil type_int32s cc_default ->
       eval_funcall ge m0 f nil t m1 (Vint r) ->
       bigstep_program_terminates p t r.
 
@@ -3042,7 +3042,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
+      type_of_fundef f = Tfunction nil type_int32s cc_default ->
       evalinf_funcall ge m0 f nil t ->
       bigstep_program_diverges p t.
 

cfrontend/Csyntax.v

@@ -54,7 +54,7 @@ Inductive expr : Type :=
   | Ecomma (r1 r2: expr) (ty: type)       (**r sequence expression [r1, r2] *)
   | Ecall (r1: expr) (rargs: exprlist) (ty: type)
                                              (**r function call [r1(rargs)] *)
-  | Ebuiltin (ef: external_function) (tyargs: typelist) (rargs: exprlist) (ty: type)
+  | Ebuiltin (ef: external_function) (tyargs: list type) (rargs: exprlist) (ty: type)
                                                  (**r builtin function call *)
   | Eloc (b: block) (ofs: ptrofs) (bf: bitfield) (ty: type)
                        (**r memory location, result of evaluating a l-value *)
@@ -109,7 +109,7 @@ Definition Eselection (r1 r2 r3: expr) (ty: type) :=
   let t := typ_of_type ty in
   let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in
   Ebuiltin (EF_builtin "__builtin_sel"%string sg)
-           (Tcons type_bool (Tcons ty (Tcons ty Tnil)))
+           (type_bool :: ty :: ty :: nil)
            (Econs r1 (Econs r2 (Econs r3 Enil)))
            ty.