Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10

3 files changed, 49 insertions, 26 deletions

diff --git a/common/Behaviors.v b/common/Behaviors.v
index 023b33e2..1f7f6226 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -25,6 +25,7 @@ Require Import Integers.
 Require Import Smallstep.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 (** * Behaviors for program executions *)
 
diff --git a/common/Builtins0.v b/common/Builtins0.v
index 384dde1e..d1922297 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -142,17 +142,34 @@ Definition valty (t: typ) : Type :=
   | Tany32 | Tany64 => Empty_set (**r no clear semantic meaning *)
   end.
 
-(** We can inject and project between the numerical type [valty t] and the type [val]. *)
+Definition valretty (t: rettype) : Type :=
+  match t with
+  | Tret t => valty t
+  | Tint8signed => { n: int | n = Int.sign_ext 8 n }
+  | Tint8unsigned => { n: int | n = Int.zero_ext 8 n }
+  | Tint16signed => { n: int | n = Int.sign_ext 16 n }
+  | Tint16unsigned => { n: int | n = Int.zero_ext 16 n }
+  | Tvoid => unit
+  end.
+
+(** We can inject from the numerical type [valretty t] to the value type [val]. *)
 
-Definition inj_num (t: typ) : valty t -> val :=
+Definition inj_num (t: rettype) : valretty t -> val :=
   match t with
-  | Tint => Vint
-  | Tlong => Vlong
-  | Tfloat => Vfloat
-  | Tsingle => Vsingle
-  | Tany32 | Tany64 => fun _ => Vundef
+  | Tret Tint => Vint
+  | Tret Tlong => Vlong
+  | Tret Tfloat => Vfloat
+  | Tret Tsingle => Vsingle
+  | Tret (Tany32 | Tany64) => fun _ => Vundef
+  | Tint8signed => fun n => Vint (proj1_sig n)
+  | Tint8unsigned => fun n => Vint (proj1_sig n)
+  | Tint16signed => fun n => Vint (proj1_sig n)
+  | Tint16unsigned => fun n => Vint (proj1_sig n)
+  | Tvoid => fun _ => Vundef
   end.
 
+(** Conversely, we can project a value to the numerical type [valty t]. *)
+
 Definition proj_num {A: Type} (t: typ) (k0: A) (v: val): (valty t -> A) -> A :=
   match t with
   | Tint => fun k1 => match v with Vint n => k1 n | _ => k0 end
@@ -162,14 +179,15 @@ Definition proj_num {A: Type} (t: typ) (k0: A) (v: val): (valty t -> A) -> A :=
   | Tany32 | Tany64 => fun k1 => k0
   end.
 
-Lemma inj_num_wt: forall t x, Val.has_type (inj_num t x) t.
+Lemma inj_num_wt: forall t x, Val.has_rettype (inj_num t x) t.
 Proof.
-  destruct t; intros; exact I.
+  destruct t; intros; simpl; auto; try (apply proj2_sig).
+  destruct t; exact I.
 Qed.
 
 Lemma inj_num_inject: forall j t x, Val.inject j (inj_num t x) (inj_num t x).
 Proof.
-  destruct t; intros; constructor.
+  destruct t; intros; try constructor. destruct t; constructor.
 Qed.
 
 Lemma inj_num_opt_wt: forall t x, val_opt_has_rettype (option_map (inj_num t) x) t.
@@ -185,10 +203,13 @@ Qed.
 
 Lemma proj_num_wt:
   forall tres t k1 v,
-  (forall x, Val.has_type (k1 x) tres) ->
-  Val.has_type (proj_num t Vundef v k1) tres.
+  (forall x, Val.has_rettype (k1 x) tres) ->
+  Val.has_rettype (proj_num t Vundef v k1) tres.
 Proof.
-  intros. destruct t; simpl; destruct v; auto; exact I.
+  intros.
+  assert (U: Val.has_rettype Vundef tres).
+  { destruct tres; exact I. }
+  intros. destruct t; simpl; destruct v; auto.
 Qed.
 
 Lemma proj_num_inject:
@@ -201,13 +222,14 @@ Proof.
 Qed.
 
 Lemma proj_num_opt_wt:
-  forall (tres: typ) t k0 k1 v,
+  forall tres t k0 k1 v,
   k0 = None \/ k0 = Some Vundef ->
   (forall x, val_opt_has_rettype (k1 x) tres) ->
   val_opt_has_rettype (proj_num t k0 v k1) tres.
 Proof.
   intros.
-  assert (val_opt_has_rettype k0 tres). { destruct H; subst k0; exact I. }
+  assert (val_opt_has_rettype k0 tres).
+  { destruct H; subst k0. exact I. hnf. destruct tres; exact I. }
   destruct t; simpl; destruct v; auto.
 Qed.
 
@@ -228,8 +250,8 @@ Qed.
  *)
 
 Program Definition mkbuiltin_n1t 
-    (targ1: typ) (tres: typ)
-    (f: valty targ1 -> valty tres) :=
+    (targ1: typ) (tres: rettype)
+    (f: valty targ1 -> valretty tres) :=
   mkbuiltin_v1t tres
     (fun v1 => proj_num targ1 Vundef v1 (fun x => inj_num tres (f x)))
     _ _.
@@ -241,8 +263,8 @@ Next Obligation.
 Qed.
 
 Program Definition mkbuiltin_n2t 
-    (targ1 targ2: typ) (tres: typ)
-    (f: valty targ1 -> valty targ2 -> valty tres) :=
+    (targ1 targ2: typ) (tres: rettype)
+    (f: valty targ1 -> valty targ2 -> valretty tres) :=
   mkbuiltin_v2t tres
     (fun v1 v2 =>
        proj_num targ1 Vundef v1 (fun x1 =>
@@ -256,8 +278,8 @@ Next Obligation.
 Qed.
 
 Program Definition mkbuiltin_n3t 
-    (targ1 targ2 targ3: typ) (tres: typ)
-    (f: valty targ1 -> valty targ2 -> valty targ3 -> valty tres) :=
+    (targ1 targ2 targ3: typ) (tres: rettype)
+    (f: valty targ1 -> valty targ2 -> valty targ3 -> valretty tres) :=
   mkbuiltin_v3t tres
     (fun v1 v2 v3 =>
        proj_num targ1 Vundef v1 (fun x1 =>
@@ -272,8 +294,8 @@ Next Obligation.
 Qed.
 
 Program Definition mkbuiltin_n1p
-    (targ1: typ) (tres: typ)
-    (f: valty targ1 -> option (valty tres)) :=
+    (targ1: typ) (tres: rettype)
+    (f: valty targ1 -> option (valretty tres)) :=
   mkbuiltin_v1p tres
     (fun v1 => proj_num targ1 None v1 (fun x => option_map (inj_num tres) (f x)))
     _ _.
@@ -285,8 +307,8 @@ Next Obligation.
 Qed.
 
 Program Definition mkbuiltin_n2p
-    (targ1 targ2: typ) (tres: typ)
-    (f: valty targ1 -> valty targ2 -> option (valty tres)) :=
+    (targ1 targ2: typ) (tres: rettype)
+    (f: valty targ1 -> valty targ2 -> option (valretty tres)) :=
   mkbuiltin_v2p tres
     (fun v1 v2 =>
       proj_num targ1 None v1 (fun x1 =>
diff --git a/common/Linking.v b/common/Linking.v
index 089f4fd2..d23b1028 100644
--- a/common/Linking.v
+++ b/common/Linking.v
@@ -869,7 +869,7 @@ Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope.
 Fixpoint compose_passes (l l': Language) (passes: Passes l l') : Pass l l' :=
   match passes in Passes l l' return Pass l l' with
   | pass_nil l => pass_identity l
-  | pass_cons l1 l2 l3 pass1 passes => pass_compose pass1 (compose_passes passes)
+  | pass_cons pass1 passes => pass_compose pass1 (compose_passes passes)
   end.
 
 (** Some more lemmas about [nlist_forall2]. *)