diff options
-rw-r--r-- | src/Reflection/Relations.v | 43 |
1 files changed, 34 insertions, 9 deletions
diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v index bc8b58f35..d0a513c0c 100644 --- a/src/Reflection/Relations.v +++ b/src/Reflection/Relations.v @@ -85,18 +85,41 @@ Section language. Context (P : Type) (and : P -> P -> P) (True : P) - (R : forall t, interp_base_type1 t -> interp_base_type2 t -> P). + (False : P). + Section hetero. + Context (R : forall t1 t2, interp_base_type1 t1 -> interp_base_type2 t2 -> P). - Fixpoint interp_flat_type_rel_pointwise2_gen_Prop (t : flat_type) - : interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> P - := match t with - | Syntax.Tbase t => R t - | Unit => fun _ _ => True - | Prod x y => fun a b => and (interp_flat_type_rel_pointwise2_gen_Prop x (fst a) (fst b)) - (interp_flat_type_rel_pointwise2_gen_Prop y (snd a) (snd b)) - end. + Fixpoint interp_flat_type_rel_pointwise2_hetero_gen_Prop (t1 t2 : flat_type) + : interp_flat_type interp_base_type1 t1 -> interp_flat_type interp_base_type2 t2 -> P + := match t1, t2 with + | Syntax.Tbase t1, Syntax.Tbase t2 => R t1 t2 + | Unit, Unit => fun _ _ => True + | Prod x1 y1, Prod x2 y2 + => fun a b => and (interp_flat_type_rel_pointwise2_hetero_gen_Prop x1 x2 (fst a) (fst b)) + (interp_flat_type_rel_pointwise2_hetero_gen_Prop y1 y2 (snd a) (snd b)) + | Syntax.Tbase _, _ + | Unit, _ + | Prod _ _, _ + => fun _ _ => False + end. + End hetero. + Section homogenous. + Context (R : forall t, interp_base_type1 t -> interp_base_type2 t -> P). + + Fixpoint interp_flat_type_rel_pointwise2_gen_Prop (t : flat_type) + : interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> P + := match t with + | Syntax.Tbase t => R t + | Unit => fun _ _ => True + | Prod x y => fun a b => and (interp_flat_type_rel_pointwise2_gen_Prop x (fst a) (fst b)) + (interp_flat_type_rel_pointwise2_gen_Prop y (snd a) (snd b)) + end. + End homogenous. End gen_prop. + Definition interp_flat_type_rel_pointwise2_hetero + := @interp_flat_type_rel_pointwise2_hetero_gen_Prop Prop and True False. + Definition interp_flat_type_rel_pointwise2 := @interp_flat_type_rel_pointwise2_gen_Prop Prop and True. @@ -140,6 +163,8 @@ Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _. Global Arguments interp_type_gen_rel_pointwise2_hetero {_ _ _ _ _} Rsrc Rdst {t} _ _. Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _. Global Arguments interp_flat_type_rel_pointwise2_gen_Prop {_ _ _ P} and True R {t} _ _. +Global Arguments interp_flat_type_rel_pointwise2_hetero_gen_Prop {_ _ _ P} and True False R {t1 t2} _ _. +Global Arguments interp_flat_type_rel_pointwise2_hetero {_ _ _} R {t1 t2} _ _. Global Arguments interp_flat_type_rel_pointwise2 {_ _ _} R {t} _ _. Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _. Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _. |