Module IntPromotion

Require Import Coqlib.
Require Import Op.
Require Import Values.
Require Import IntPromotionCommon.
Require Import ZIntervalDomain.

Definition promote_operation (op : operation) (args : list ival) : op_promotion := op_prom_None.
Definition promote_condition (cond : condition) (args : list ival) : cond_promotion := cond_prom_None.


Lemma promote_operation_sound F V ge sp m op args iargs
  (MATCH : list_forall2 vmatch args iargs):
  sound_op_promotion (@promotable_op F V ge sp m) op (promote_operation op iargs) args.

Lemma promote_condition_sound m cond args iargs
  (MATCH : list_forall2 vmatch args iargs):
  sound_cond_promotion (@promotable_cond m) cond (promote_condition cond iargs) args.

Global Opaque promote_operation promote_condition.