diff options
Diffstat (limited to 'common/AST.v')
-rw-r--r-- | common/AST.v | 57 |
1 files changed, 56 insertions, 1 deletions
diff --git a/common/AST.v b/common/AST.v index 415e90e2..0b524eb8 100644 --- a/common/AST.v +++ b/common/AST.v @@ -544,10 +544,65 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := End TRANSF_PARTIAL_FUNDEF. -(** * Arguments and results to builtin functions *) +(** * Register pairs *) Set Contextual Implicit. +(** In some intermediate languages (LTL, Mach), 64-bit integers can be + split into two 32-bit halves and held in a pair of registers. + Syntactically, this is captured by the type [rpair] below. *) + +Inductive rpair (A: Type) : Type := + | One (r: A) + | Twolong (rhi rlo: A). + +Definition typ_rpair (A: Type) (typ_of: A -> typ) (p: rpair A): typ := + match p with + | One r => typ_of r + | Twolong rhi rlo => Tlong + end. + +Definition map_rpair (A B: Type) (f: A -> B) (p: rpair A): rpair B := + match p with + | One r => One (f r) + | Twolong rhi rlo => Twolong (f rhi) (f rlo) + end. + +Definition regs_of_rpair (A: Type) (p: rpair A): list A := + match p with + | One r => r :: nil + | Twolong rhi rlo => rhi :: rlo :: nil + end. + +Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A := + match l with + | nil => nil + | p :: l => regs_of_rpair p ++ regs_of_rpairs l + end. + +Lemma in_regs_of_rpairs: + forall (A: Type) (x: A) p, In x (regs_of_rpair p) -> forall l, In p l -> In x (regs_of_rpairs l). +Proof. + induction l; simpl; intros. auto. apply in_app. destruct H0; auto. subst a. auto. +Qed. + +Lemma in_regs_of_rpairs_inv: + forall (A: Type) (x: A) l, In x (regs_of_rpairs l) -> exists p, In p l /\ In x (regs_of_rpair p). +Proof. + induction l; simpl; intros. contradiction. + rewrite in_app_iff in H; destruct H. + exists a; auto. + apply IHl in H. firstorder auto. +Qed. + +Definition forall_rpair (A: Type) (P: A -> Prop) (p: rpair A): Prop := + match p with + | One r => P r + | Twolong rhi rlo => P rhi /\ P rlo + end. + +(** * Arguments and results to builtin functions *) + Inductive builtin_arg (A: Type) : Type := | BA (x: A) | BA_int (n: int) |