From 4107ed987a8a89246a11e548b171d948ed216103 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 12 Jun 2017 15:33:01 -0400 Subject: Add CompileInterpSideConditions.v --- src/Compilers/Named/CompileInterpSideConditions.v | 253 ++++++++++++++++++++++ src/Compilers/Named/InterpSideConditions.v | 90 ++++---- 2 files changed, 299 insertions(+), 44 deletions(-) create mode 100644 src/Compilers/Named/CompileInterpSideConditions.v (limited to 'src') diff --git a/src/Compilers/Named/CompileInterpSideConditions.v b/src/Compilers/Named/CompileInterpSideConditions.v new file mode 100644 index 000000000..da8e1d8b2 --- /dev/null +++ b/src/Compilers/Named/CompileInterpSideConditions.v @@ -0,0 +1,253 @@ +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.NameUtil. +Require Import Crypto.Compilers.Named.NameUtilProperties. +Require Import Crypto.Compilers.Named.ContextDefinitions. +Require Import Crypto.Compilers.Named.ContextProperties. +Require Import Crypto.Compilers.Named.ContextProperties.NameUtil. +Require Import Crypto.Compilers.Named.InterpSideConditions. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.InterpSideConditions. +Require Import Crypto.Compilers.Named.Compile. +Require Import Crypto.Util.PointedProp. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeBy. + +Section language. + Context {base_type_code} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + {Name : Type} + {interp_base_type : base_type_code -> Type} + {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst} + {base_type_dec : DecidableRel (@eq base_type_code)} + {Name_dec : DecidableRel (@eq Name)} + {interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop} + {Context : @Context base_type_code Name interp_base_type} + {ContextOk : ContextOk Context}. + + Local Notation flat_type := (flat_type base_type_code). + 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). + Local Notation nexpr := (@Named.expr base_type_code op Name). + Local Notation ocompilef := (@ocompilef base_type_code op Name). + Local Notation ocompile := (@ocompile base_type_code op Name). + Local Notation compilef := (@compilef base_type_code op Name). + Local Notation compile := (@compile base_type_code op Name). + + Lemma interpf_side_conditions_gen_ocompilef (ctx : Context) {t} (e : exprf t) e' (ls : list (option Name)) + G + (Hwf : wff G e e') + (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb t ctx n = Some x) + v + (H : ocompilef e ls = Some v) + (Hls : oname_list_unique ls) + (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In (Some n) ls -> False) + : Named.interpf_side_conditions_gen interp_op interped_op_side_conditions ctx v + = Some (interpf_side_conditions_gen interp_op interped_op_side_conditions e'). + Proof using ContextOk Name_dec base_type_dec. + revert dependent ctx; revert dependent ls; induction Hwf; + repeat first [ progress intros + | progress subst + | progress inversion_option + | apply (f_equal (@Some _)) + | apply (f_equal2 (@pair _ _)) + | apply (f_equal2 and_pointed_Prop) + | apply (f_equal (@interp_op _ _ _)) + | solve [ eauto ] + | progress simpl in * + | progress unfold option_map, LetIn.Let_In in * + | progress break_innermost_match_step + | progress break_match_hyps + | progress destruct_head' or + | progress inversion_prod + | progress specialize_by_assumption + | progress specialize_by auto using oname_list_unique_nil + | match goal with + | [ H : forall x, oname_list_unique ?ls -> _ |- _ ] + => specialize (fun pf x => H x pf) + | [ H : context[snd (split_onames _ _)] |- _ ] + => rewrite snd_split_onames_skipn in H + | [ H : oname_list_unique (List.skipn _ _) -> _ |- _ ] + => specialize (fun pf => H (@oname_list_unique_skipn _ _ _ pf)) + | [ IH : forall v ls, ocompilef ?e ls = Some v -> _, H : ocompilef ?e ?ls' = Some ?v' |- _ ] + => specialize (IH _ _ H) + | [ IH : forall x1 x2 v ls, ocompilef (?e x1) ls = Some v -> _, H : ocompilef (?e ?x1') ?ls' = Some ?v' |- _ ] + => specialize (fun x2 => IH _ x2 _ _ H) + | [ H : context[List.In _ (_ ++ _)] |- _ ] + => rewrite List.in_app_iff in H + | [ H : forall ctx, _ -> Named.interpf_side_conditions_gen _ _ _ ?e = Some _, H' : context[Named.interpf_side_conditions_gen _ _ _ ?e] |- _ ] + => rewrite H in H' by assumption + | [ H : forall x2 ctx, _ -> Named.interpf_side_conditions_gen _ _ _ ?e = Some _ |- Named.interpf_side_conditions_gen _ _ _ ?e = Some _ ] + => apply H; clear H + | [ H : forall x2, _ -> forall ctx, _ -> Named.interpf_side_conditions_gen _ _ _ ?e = Some _ |- Named.interpf_side_conditions_gen _ _ _ ?e = Some _ ] + => apply H; clear H + | [ H : forall x2 ctx, _ -> Named.interpf_side_conditions_gen _ _ _ ?e = Some _, H' : context[Named.interpf_side_conditions_gen _ _ _ ?e] |- _ ] + => erewrite H in H'; clear H + | [ H : forall x2, _ -> forall ctx, _ -> Named.interpf_side_conditions_gen _ _ _ ?e = Some _, H' : context[Named.interpf_side_conditions_gen _ _ _ ?e] |- _ ] + => erewrite H in H'; clear H + end ]; + repeat match goal with + | _ => erewrite lookupb_extend by assumption + | [ |- context[find_Name_and_val ?tdec ?ndec ?a ?b ?c ?d ?default] ] + => lazymatch default with None => fail | _ => idtac end; + rewrite (find_Name_and_val_split tdec ndec (default:=default)) + | [ H : _ |- _ ] => erewrite H by eassumption + | _ => progress unfold dec in * + | _ => progress break_innermost_match_step + | _ => progress subst + | _ => progress destruct_head' and + | _ => congruence + | [ H : List.In _ (flatten_binding_list _ _) |- _ ] + => erewrite <- (flatten_binding_list_find_Name_and_val_unique _ _) in H; + [ | | apply path_prod_uncurried; split; [ eassumption | simpl; reflexivity ] ]; + [ | solve [ eauto using oname_list_unique_firstn, oname_list_unique_skipn ] ] + | [ H : _ |- _ ] + => first [ erewrite find_Name_and_val_wrong_type in H by eassumption + | rewrite find_Name_and_val_different in H by assumption + | rewrite snd_split_onames_skipn in H ] + | _ => solve [ eauto using In_skipn, In_firstn + | eapply split_onames_find_Name_Some_unique; [ | apply path_prod; simpl | ]; eauto ] + | [ H : find_Name_and_val _ _ ?t ?n ?N ?V None = Some _, H' : List.In (Some ?n) (List.skipn _ ?ls) |- False ] + => eapply find_Name_and_val_find_Name_Some, split_onames_find_Name_Some_unique in H; + [ | | apply path_prod_uncurried; split; [ eassumption | simpl; reflexivity ] ]; + [ | solve [ eauto using oname_list_unique_firstn, oname_list_unique_skipn ] ] + | [ H : List.In (existT _ ?t (?n, _)%core) ?G, + H' : List.In (Some ?n) (List.skipn _ ?ls), + IH : forall t' n' x', List.In (existT _ t' (n', x')%core) ?G -> List.In (Some n') ?ls -> False + |- False ] + => apply (IH _ _ _ H); clear IH H + | [ H : List.In (existT _ ?t (?n, _)%core) ?G, + H' : find_Name _ ?n ?N = Some ?t', + IH : forall t' n' x', List.In (existT _ t' (n', x')%core) ?G -> List.In (Some n') ?ls -> False + |- _ ] + => exfalso; apply (IH _ _ _ H); clear IH H + | [ H : List.In (existT _ ?t (?n, ?v')%core) ?G, + H' : lookupb ?ctx ?x = Some ?v, + IH : forall t' n' x', List.In (existT _ t' (n', x')%core) ?G -> lookupb ?ctx n' = Some x' + |- _ ] + => assert (v = v') by (pose proof (IH _ _ _ H); congruence); + (subst v || subst v') + | [ H : List.In (existT _ ?t (?n, ?v')%core) ?G, + H' : lookupb ?ctx ?x = _, + IH : forall t' n' x', List.In (existT _ t' (n', x')%core) ?G -> lookupb ?ctx n' = Some x' + |- _ ] + => pose proof (IH _ _ _ H); congruence + end. + Qed. + + Lemma interpf_side_conditions_ocompilef (ctx : Context) {t} (e : exprf t) e' (ls : list (option Name)) + G + (Hwf : wff G e e') + (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb t ctx n = Some x) + v + (H : ocompilef e ls = Some v) + (Hls : oname_list_unique ls) + (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In (Some n) ls -> False) + : Named.interpf_side_conditions interp_op interped_op_side_conditions ctx v + = Some (interpf_side_conditions interp_op interped_op_side_conditions e'). + Proof using ContextOk Name_dec base_type_dec. + unfold Named.interpf_side_conditions; erewrite interpf_side_conditions_gen_ocompilef by eassumption. + reflexivity. + Qed. + + Lemma interp_side_conditions_ocompile (ctx : Context) {t} (e : expr t) e' (ls : list (option Name)) + (Hwf : wf e e') + f + (Hls : oname_list_unique ls) + (H : ocompile e ls = Some f) + : forall v, Named.interp_side_conditions interp_op interped_op_side_conditions ctx f v + = Some (interp_side_conditions interp_op interped_op_side_conditions e' v). + Proof using ContextOk Name_dec base_type_dec. + revert H; destruct Hwf; + repeat first [ progress simpl in * + | progress unfold option_map, Named.interp in * + | congruence + | progress break_innermost_match + | progress inversion_option + | progress subst + | progress intros ]. + eapply interpf_side_conditions_ocompilef; + [ eauto | | eassumption + | inversion_prod; subst; rewrite snd_split_onames_skipn; eauto using oname_list_unique_skipn + |intros ???; erewrite <- (flatten_binding_list_find_Name_and_val_unique _ _) by eassumption; + let H := fresh in + intro H; apply find_Name_and_val_find_Name_Some in H; + eapply split_onames_find_Name_Some_unique in H; [ | eassumption.. ]; + intuition ]. + { intros ???. + repeat first [ solve [ auto ] + | rewrite (lookupb_extend _ _ _) + | progress subst + | progress break_innermost_match + | erewrite <- (flatten_binding_list_find_Name_and_val_unique _ _) by eassumption + | congruence + | match goal with + | [ |- context[find_Name_and_val ?tdec ?ndec ?a ?b ?c ?d ?default] ] + => lazymatch default with None => fail | _ => idtac end; + rewrite (find_Name_and_val_split tdec ndec (default:=default)) + | [ H : _ |- _ ] => first [ erewrite find_Name_and_val_wrong_type in H by eassumption + | erewrite find_Name_and_val_different in H by eassumption ] + end + | progress intros ]. } + Qed. + + Lemma interpf_side_conditions_gen_compilef (ctx : Context) {t} (e : exprf t) e' (ls : list Name) + G + (Hwf : wff G e e') + (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb t ctx n = Some x) + v + (H : compilef e ls = Some v) + (Hls : name_list_unique ls) + (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In n ls -> False) + : Named.interpf_side_conditions_gen interp_op interped_op_side_conditions ctx v + = Some (interpf_side_conditions_gen interp_op interped_op_side_conditions e'). + Proof using ContextOk Name_dec base_type_dec. + eapply interpf_side_conditions_gen_ocompilef; try eassumption. + setoid_rewrite List.in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst. + eauto. + Qed. + + Lemma interpf_side_conditions_compilef (ctx : Context) {t} (e : exprf t) e' (ls : list Name) + G + (Hwf : wff G e e') + (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb t ctx n = Some x) + v + (H : compilef e ls = Some v) + (Hls : name_list_unique ls) + (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In n ls -> False) + : Named.interpf_side_conditions interp_op interped_op_side_conditions ctx v + = Some (interpf_side_conditions interp_op interped_op_side_conditions e'). + Proof using ContextOk Name_dec base_type_dec. + unfold Named.interpf_side_conditions; erewrite interpf_side_conditions_gen_compilef by eassumption. + reflexivity. + Qed. + + Lemma interp_side_conditions_compile (ctx : Context) {t} (e : expr t) e' (ls : list Name) + (Hwf : wf e e') + f + (Hls : name_list_unique ls) + (H : compile e ls = Some f) + : forall v, Named.interp_side_conditions interp_op interped_op_side_conditions ctx f v + = Some (interp_side_conditions interp_op interped_op_side_conditions e' v). + Proof using ContextOk Name_dec base_type_dec. eapply interp_side_conditions_ocompile; eassumption. Qed. + + Lemma InterpSideConditions_compile {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.InterpSideConditions (Context:=Context) interp_op interped_op_side_conditions f v + = Some (InterpSideConditions interp_op interped_op_side_conditions e v). + Proof using ContextOk Name_dec base_type_dec. eapply interp_side_conditions_compile; eauto. Qed. +End language. diff --git a/src/Compilers/Named/InterpSideConditions.v b/src/Compilers/Named/InterpSideConditions.v index a2f965435..bd90eac23 100644 --- a/src/Compilers/Named/InterpSideConditions.v +++ b/src/Compilers/Named/InterpSideConditions.v @@ -4,49 +4,51 @@ Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Util.PointedProp. Require Import Crypto.Util.Notations. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type} - {interp_base_type : base_type_code -> Type} - {Context : Context Name interp_base_type} - (interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d) - (interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop). +Module Export Named. + Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + {Name : Type} + {interp_base_type : base_type_code -> Type} + {Context : Context Name interp_base_type} + (interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d) + (interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop). - Local Notation exprf := (@exprf base_type_code op Name). - Local Notation expr := (@expr base_type_code op Name). + Local Notation exprf := (@exprf base_type_code op Name). + Local Notation expr := (@expr base_type_code op Name). - Fixpoint interpf_side_conditions_gen {t} (ctx : Context) (e : exprf t) - : option (pointed_Prop * interp_flat_type interp_base_type t) - := match e with - | TT => Some (trivial, tt) - | Var t' x => option_map (fun v => (trivial, v)) (lookupb t' ctx x) - | Op t1 tR opc args - => match @interpf_side_conditions_gen _ ctx args with - | Some (args_cond, argsv) - => Some (args_cond /\ interped_op_side_conditions _ _ opc argsv, interp_op _ _ opc argsv) - | None => None - end - | LetIn _ n ex _ eC - => match @interpf_side_conditions_gen _ ctx ex with - | Some (x_cond, x) - => match @interpf_side_conditions_gen _ (extend ctx n x) eC with - | Some (c_cond, cv) - => Some (x_cond /\ c_cond, cv) - | None => None - end - | None => None - end - | Pair _ ex _ ey - => match @interpf_side_conditions_gen _ ctx ex, @interpf_side_conditions_gen _ ctx ey with - | Some (x_cond, xv), Some (y_cond, yv) => Some (x_cond /\ y_cond, (xv, yv)) - | None, _ | _, None => None - end - end%pointed_prop. - Definition interpf_side_conditions {t} ctx e : option pointed_Prop - := option_map (@fst _ _) (@interpf_side_conditions_gen t ctx e). - Definition interp_side_conditions {t} ctx (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop - := fun x => interpf_side_conditions (extend ctx (Abs_name e) x) (invert_Abs e). - Definition InterpSideConditions {t} (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop - := interp_side_conditions empty e. -End language. + Fixpoint interpf_side_conditions_gen {t} (ctx : Context) (e : exprf t) + : option (pointed_Prop * interp_flat_type interp_base_type t) + := match e with + | TT => Some (trivial, tt) + | Var t' x => option_map (fun v => (trivial, v)) (lookupb t' ctx x) + | Op t1 tR opc args + => match @interpf_side_conditions_gen _ ctx args with + | Some (args_cond, argsv) + => Some (args_cond /\ interped_op_side_conditions _ _ opc argsv, interp_op _ _ opc argsv) + | None => None + end + | LetIn _ n ex _ eC + => match @interpf_side_conditions_gen _ ctx ex with + | Some (x_cond, x) + => match @interpf_side_conditions_gen _ (extend ctx n x) eC with + | Some (c_cond, cv) + => Some (x_cond /\ c_cond, cv) + | None => None + end + | None => None + end + | Pair _ ex _ ey + => match @interpf_side_conditions_gen _ ctx ex, @interpf_side_conditions_gen _ ctx ey with + | Some (x_cond, xv), Some (y_cond, yv) => Some (x_cond /\ y_cond, (xv, yv)) + | None, _ | _, None => None + end + end%pointed_prop. + Definition interpf_side_conditions {t} ctx e : option pointed_Prop + := option_map (@fst _ _) (@interpf_side_conditions_gen t ctx e). + Definition interp_side_conditions {t} ctx (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop + := fun x => interpf_side_conditions (extend ctx (Abs_name e) x) (invert_Abs e). + Definition InterpSideConditions {t} (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop + := interp_side_conditions empty e. + End language. +End Named. -- cgit v1.2.3