diff options
Diffstat (limited to 'src/Experiments/NewPipeline/Language.v')
| -rw-r--r-- | src/Experiments/NewPipeline/Language.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index 6c31dd0d9..5fa3a25bd 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -104,12 +104,15 @@ Module Compilers. | arrow s d => @interp _ base_interp s -> @interp _ base_interp d end. - Fixpoint eqv {base_type} {base_interp : base_type -> Type} {t : type base_type} : relation (interp base_interp t) + Fixpoint related {base_type} {base_interp : base_type -> Type} (R : forall t, relation (base_interp t)) {t : type base_type} + : relation (interp base_interp t) := match t with - | base t => @eq (base_interp t) - | arrow s d => @eqv _ base_interp s ==> @eqv _ base_interp d + | base t => R t + | arrow s d => @related _ _ R s ==> @related _ _ R d end%signature. + Notation eqv := (@related _ _ (fun _ => eq)). + Fixpoint app_curried {base_type} {f : base_type -> Type} {t : type base_type} : interp f t -> for_each_lhs_of_arrow (interp f) t -> f (final_codomain t) := match t with |