From c9fad7cd7bdc4e79fb06a1d39abfa0d5471623e5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Sep 2021 14:00:41 +0200 Subject: Avoid `Global Set Asymmetric Patterns` (#408) Instead, add `Set Asymmetric Patterns` to the files that need it, or use `Arguments` to make inductive types work better with symmetric patterns. Closes: #403 --- common/Behaviors.v | 1 + common/Linking.v | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'common') 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/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]. *) -- cgit From 2a6991362fc6716a4f1eee5b083eace3a67923ed Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 6 Sep 2021 18:02:56 +0200 Subject: For numerical builtins, support return types that are small integer types --- common/Builtins0.v | 72 +++++++++++++++++++++++++++++++++++------------------- 1 file changed, 47 insertions(+), 25 deletions(-) (limited to 'common') 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 => -- cgit