From 03d7ac6daeb069490a909a1c29ea5b5585d63c61 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 16 May 2017 18:09:52 -0400 Subject: Add Interp_compile --- src/Compilers/Named/CompileInterp.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src') diff --git a/src/Compilers/Named/CompileInterp.v b/src/Compilers/Named/CompileInterp.v index f87087e8e..713565ff6 100644 --- a/src/Compilers/Named/CompileInterp.v +++ b/src/Compilers/Named/CompileInterp.v @@ -36,6 +36,7 @@ Section language. Local Notation type := (type base_type_code). Local Notation exprf := (@exprf base_type_code op (fun _ => Name)). Local Notation expr := (@expr base_type_code op (fun _ => Name)). + Local Notation Expr := (@Expr base_type_code op). Local Notation wff := (@wff base_type_code op (fun _ => Name) interp_base_type). Local Notation wf := (@wf base_type_code op (fun _ => Name) interp_base_type). Local Notation nexprf := (@Named.exprf base_type_code op Name). @@ -194,4 +195,13 @@ Section language. : forall v, Named.interp (interp_op:=interp_op) (ctx:=ctx) f v = Some (interp interp_op e' v). Proof using ContextOk Name_dec base_type_dec. eapply interp_ocompile; eassumption. Qed. + + Lemma Interp_compile (ctx : Context) {t} (e : Expr t) (ls : list Name) + (Hwf : Wf e) + f + (Hls : name_list_unique ls) + (H : compile (e _) ls = Some f) + : forall v, Named.Interp (Context:=Context) (interp_op:=interp_op) f v + = Some (Interp interp_op e v). + Proof using ContextOk Name_dec base_type_dec. eapply interp_compile; eauto. Qed. End language. -- cgit v1.2.3