From e4dac24479752b7d2645c9ba9dc23b73051f0f9e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 26 May 2020 17:33:45 +0100 Subject: Working on automation --- src/translation/HTLgenspec.v | 110 +++++++++++++++++++------------------------ 1 file changed, 48 insertions(+), 62 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 06ed68d..9c46b48 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -237,6 +237,37 @@ Proof. monadInv H; constructor. Qed. +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g; try discriminate + end. + +Ltac inv_add_instr' H := + match type of H with + | ?f _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H + end; repeat unfold_match H; inversion H. + +Ltac inv_add_instr := + match goal with + | H: context[add_instr_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_instr _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_branch_instr _ _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_branch_instr _ _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + end. + +Ltac destruct_optional := + match goal with H: option ?r |- _ => destruct H end. + Lemma iter_expand_instr_spec : forall l fin rtrn s s' i x, HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i -> @@ -250,87 +281,42 @@ Proof. destruct (peq pc pc1). + subst. - destruct instr1 eqn:?; try discriminate. - - * unfold add_instr in EQ. - destruct (check_empty_node_datapath s1 pc1); try discriminate. - destruct (check_empty_node_controllogic s1 pc1); try discriminate. - inversion EQ. - econstructor. - destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. + destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor. - destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - - inversion H1. inversion H7. rewrite H. apply tr_instr_Inop. + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + * inversion H1. inversion H7. rewrite H. apply tr_instr_Inop. eapply in_map with (f := fst) in H7. simpl in H7. contradiction. - * monadInv EQ. - inv_incr. - unfold add_instr in EQ2. - destruct (check_empty_node_datapath s0 pc1); try discriminate. - destruct (check_empty_node_controllogic s0 pc1); try discriminate. - inversion EQ2. - econstructor. - destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - - destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - - inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor. + * inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor. eapply translate_instr_tr_op. apply EQ1. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. - * monadInv EQ. - inv_incr. - unfold add_branch_instr in EQ2. - destruct (check_empty_node_datapath s0 pc1); try discriminate. - destruct (check_empty_node_controllogic s0 pc1); try discriminate. - inversion EQ2. - - econstructor. - destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - - inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. - apply EQ1. - + * inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. apply EQ1. eapply in_map with (f := fst) in H7. simpl in H7. contradiction. - * destruct o3 eqn:?. - unfold add_instr_skip in EQ. - destruct (check_empty_node_datapath s1 pc1); try discriminate. - destruct (check_empty_node_controllogic s1 pc1); try discriminate. - inversion EQ. - - econstructor. - destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - - inversion H1. inversion H7. constructor. - + * inversion H1. inversion H7. constructor. eapply in_map with (f := fst) in H7. simpl in H7. contradiction. - unfold add_instr_skip in EQ. - destruct (check_empty_node_datapath s1 pc1); try discriminate. - destruct (check_empty_node_controllogic s1 pc1); try discriminate. - inversion EQ. - - econstructor. - destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. - - inversion H1. inversion H7. apply constructor. - + * inversion H1. inversion H7. constructor. eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + eapply IHl. apply EQ0. assumption. -- cgit