From e472fa65fc063eaa965e648f2826bd21fdf07339 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 16 Aug 2018 14:34:42 -0400 Subject: Add andb_each_lhs_of_arrow --- src/Experiments/NewPipeline/Language.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src') diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index 26fe9eac6..4d17d9afd 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -97,6 +97,12 @@ Module Compilers. | arrow s d => f s * @for_each_lhs_of_arrow _ f d end. + Fixpoint andb_each_lhs_of_arrow {base_type} (f : type base_type -> bool) (t : type base_type) : bool + := match t with + | base t => true + | arrow s d => andb (f s) (@andb_each_lhs_of_arrow _ f d) + end. + (** Denote [type]s into their interpretation in [Type]/[Set] *) Fixpoint interp {base_type} (base_interp : base_type -> Type) (t : type base_type) : Type := match t with @@ -173,6 +179,15 @@ Module Compilers. | arrow s d => fun x_xs y_ys => R s (fst x_xs) (fst y_ys) /\ @and_for_each_lhs_of_arrow _ f g R d (snd x_xs) (snd y_ys) end. + Definition is_base {base_type} (t : type base_type) : bool + := match t with + | type.base _ => true + | type.arrow _ _ => false + end. + + Definition is_not_higher_order {base_type} : type base_type -> bool + := andb_each_lhs_of_arrow is_base. + Section interpM. Context {base_type} (M : Type -> Type) (base_interp : base_type -> Type). (** half-monadic denotation function; denote [type]s into their -- cgit v1.2.3