diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Inline.v | 12 | ||||
| -rw-r--r-- | src/Compilers/InlineWf.v | 6 |
2 files changed, 16 insertions, 2 deletions
diff --git a/src/Compilers/Inline.v b/src/Compilers/Inline.v index e4946adde..bd39b48a0 100644 --- a/src/Compilers/Inline.v +++ b/src/Compilers/Inline.v @@ -21,13 +21,20 @@ Section language. Inductive inline_directive : flat_type -> Type := | default_inline {t} (e : @exprf var t) : inline_directive t | inline {t} (e : interp_flat_type (fun t => @exprf var (Tbase t)) t) : inline_directive t - | no_inline {t} (e : @exprf var t) : inline_directive t. + | no_inline {t} (e : @exprf var t) : inline_directive t + | partial_inline + {tx tC} + (ex : @exprf var tx) + (eC : interp_flat_type var tx -> interp_flat_type (fun t => @exprf var (Tbase t)) tC) + : inline_directive tC. Definition exprf_of_inline_directive {t} (v : inline_directive t) : @exprf var t := match v with | default_inline t e => e | inline t e => SmartPairf e | no_inline t e => e + | partial_inline _ _ ex eC + => LetIn ex (fun x => SmartPairf (eC x)) end. Context (postprocess : forall {t}, @exprf var t -> inline_directive t). @@ -45,6 +52,8 @@ Section language. | no_inline _ ex => fun eC => LetIn ex (fun x => eC (SmartVarVarf x)) | inline _ ex => fun eC => eC ex + | partial_inline _ _ ex eC' + => fun eC => LetIn ex (fun x => eC (eC' x)) end (fun x => @inline_const_genf _ (eC x)) | Var _ x => x | TT => TT @@ -86,6 +95,7 @@ Global Arguments inline_directive {_} _ _ _, {_ _ _} _. Global Arguments no_inline {_ _ _ _} _. Global Arguments inline {_ _ _ _} _. Global Arguments default_inline {_ _ _ _} _. +Global Arguments partial_inline {_ _ _ _ _} ex eC. Global Arguments inline_const_genf {_ _ _} postprocess {_} _. Global Arguments inline_const_gen {_ _ _} postprocess {_} _. Global Arguments InlineConstGen {_ _} postprocess {_} _ var. diff --git a/src/Compilers/InlineWf.v b/src/Compilers/InlineWf.v index 84bf07fb7..a9fc959d0 100644 --- a/src/Compilers/InlineWf.v +++ b/src/Compilers/InlineWf.v @@ -33,10 +33,12 @@ Section language. | default_inline _ _, default_inline _ _ | no_inline _ _, no_inline _ _ | inline _ _, inline _ _ + | partial_inline _ _ _ _, partial_inline _ _ _ _ => True | default_inline _ _, _ | no_inline _ _, _ | inline _ _, _ + | partial_inline _ _ _ _, _ => False end) x y). @@ -118,7 +120,7 @@ Section language. | _ => progress inversion_sigma | _ => progress inversion_prod | _ => progress destruct_head' and - | _ => inversion_wf_step; progress subst + | _ => inversion_wf_step; destruct_head' sig; progress subst | _ => progress specialize_by_assumption | _ => progress break_match | _ => progress invert_inline_directive @@ -150,6 +152,8 @@ Section language. intros; destruct_head or; t_fin. } { match goal with H : _ |- _ => apply H end. intros; destruct_head or; t_fin. } + { match goal with H : _ |- _ => apply H end. + intros; destruct_head or; t_fin. } Qed. Lemma wff_postprocess_for_const is_const G t |