diff options
Diffstat (limited to 'src/Compilers/Named')
44 files changed, 0 insertions, 4542 deletions
diff --git a/src/Compilers/Named/AListContext.v b/src/Compilers/Named/AListContext.v deleted file mode 100644 index ffc8355ee..000000000 --- a/src/Compilers/Named/AListContext.v +++ /dev/null @@ -1,143 +0,0 @@ -(** * Context made from an associative list, without modules *) -Require Import Coq.Bool.Sumbool. -Require Import Coq.Lists.List. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Equality. - -Local Open Scope list_scope. -Section ctx. - Context (key : Type) - (key_beq : key -> key -> bool) - (key_bl : forall k1 k2, key_beq k1 k2 = true -> k1 = k2) - (key_lb : forall k1 k2, k1 = k2 -> key_beq k1 k2 = true) - base_type_code (var : base_type_code -> Type) - (base_type_code_beq : base_type_code -> base_type_code -> bool) - (base_type_code_bl_transparent : forall x y, base_type_code_beq x y = true -> x = y) - (base_type_code_lb : forall x y, x = y -> base_type_code_beq x y = true). - - Definition var_cast {a b} (x : var a) : option (var b) - := match Sumbool.sumbool_of_bool (base_type_code_beq a b), Sumbool.sumbool_of_bool (base_type_code_beq b b) with - | left pf, left pf' => match eq_trans (base_type_code_bl_transparent _ _ pf) (eq_sym (base_type_code_bl_transparent _ _ pf')) with - | eq_refl => Some x - end - | right _, _ | _, right _ => None - end. - - Fixpoint find (k : key) (xs : list (key * { t : _ & var t })) {struct xs} - : option { t : _ & var t } - := match xs with - | nil => None - | k'x :: xs' => - if key_beq k (fst k'x) - then Some (snd k'x) - else find k xs' - end. - - Fixpoint remove (k : key) (xs : list (key * { t : _ & var t })) {struct xs} - : list (key * { t : _ & var t }) - := match xs with - | nil => nil - | k'x :: xs' => - if key_beq k (fst k'x) - then remove k xs' - else k'x :: remove k xs' - end. - - Definition add (k : key) (x : { t : _ & var t }) (xs : list (key * { t : _ & var t })) - : list (key * { t : _ & var t }) - := (k, x) :: xs. - - Lemma find_remove_neq k k' xs (H : k <> k') - : find k (remove k' xs) = find k xs. - Proof. - induction xs as [|x xs IHxs]; [ reflexivity | simpl ]. - break_innermost_match; - repeat match goal with - | [ H : key_beq _ _ = true |- _ ] => apply key_bl in H - | [ H : context[key_beq ?x ?x] |- _ ] => rewrite (key_lb x x) in H by reflexivity - | [ |- context[key_beq ?x ?x] ] => rewrite (key_lb x x) by reflexivity - | [ H : ?x = false |- context[?x] ] => rewrite H - | _ => congruence - | _ => assumption - | _ => progress subst - | _ => progress simpl - end. - Qed. - - Lemma find_remove_same k xs - : find k (remove k xs) = None. - Proof. - induction xs as [|x xs IHxs]; [ reflexivity | simpl ]. - break_innermost_match; - repeat match goal with - | [ H : key_beq _ _ = true |- _ ] => apply key_bl in H - | [ H : context[key_beq ?x ?x] |- _ ] => rewrite (key_lb x x) in H by reflexivity - | [ |- context[key_beq ?x ?x] ] => rewrite (key_lb x x) by reflexivity - | [ H : ?x = false |- context[?x] ] => rewrite H - | _ => congruence - | _ => assumption - | _ => progress subst - | _ => progress simpl - end. - Qed. - - Lemma find_remove_nbeq k k' xs (H : key_beq k k' = false) - : find k (remove k' xs) = find k xs. - Proof. - rewrite find_remove_neq; [ reflexivity | intro; subst ]. - rewrite key_lb in H by reflexivity; congruence. - Qed. - - Lemma find_remove_beq k k' xs (H : key_beq k k' = true) - : find k (remove k' xs) = None. - Proof. - apply key_bl in H; subst. - rewrite find_remove_same; reflexivity. - Qed. - - Definition AListContext : @Context base_type_code key var - := {| ContextT := list (key * { t : _ & var t }); - lookupb t ctx n - := match find n ctx with - | Some (existT t' v) - => var_cast v - | None => None - end; - extendb t ctx n v - := add n (existT _ t v) ctx; - removeb t ctx n - := remove n ctx; - empty := nil |}. - - Lemma length_extendb (ctx : AListContext) k t v - : length (@extendb _ _ _ AListContext t ctx k v) = S (length ctx). - Proof. reflexivity. Qed. - - Lemma AListContextOk : @ContextOk base_type_code key var AListContext. - Proof using base_type_code_lb key_bl key_lb. - split; - repeat first [ reflexivity - | progress simpl in * - | progress intros - | rewrite find_remove_nbeq by eassumption - | rewrite find_remove_beq by eassumption - | rewrite find_remove_neq by congruence - | rewrite find_remove_same by congruence - | match goal with - | [ |- context[key_beq ?x ?y] ] - => destruct (key_beq x y) eqn:? - | [ H : key_beq ?x ?y = true |- _ ] - => apply key_bl in H - end - | break_innermost_match_step - | progress unfold var_cast - | rewrite key_lb in * by reflexivity - | rewrite base_type_code_lb in * by reflexivity - | rewrite concat_pV - | congruence - | break_innermost_match_hyps_step - | progress unfold var_cast in * ]. - Qed. -End ctx. diff --git a/src/Compilers/Named/Compile.v b/src/Compilers/Named/Compile.v deleted file mode 100644 index bee71cea5..000000000 --- a/src/Compilers/Named/Compile.v +++ /dev/null @@ -1,59 +0,0 @@ -(** * PHOAS → Named Representation of Gallina *) -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.NameUtil. -Require Import Crypto.Compilers.Syntax. - -Local Notation eta x := (fst x, snd x). - -Local Open Scope ctype_scope. -Local Open Scope nexpr_scope. -Local Open Scope expr_scope. -Section language. - Context (base_type_code : Type) - (op : flat_type base_type_code -> flat_type base_type_code -> Type) - (Name : Type). - - 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 nexprf := (@Named.exprf base_type_code op Name). - Local Notation nexpr := (@Named.expr base_type_code op Name). - - Fixpoint ocompilef {t} (e : exprf t) (ls : list (option Name)) {struct e} - : option (nexprf t) - := match e in @Syntax.exprf _ _ _ t return option (nexprf t) with - | TT => Some Named.TT - | Var _ x => Some (Named.Var x) - | Op _ _ op args => option_map (Named.Op op) (@ocompilef _ args ls) - | LetIn tx ex _ eC - => match @ocompilef _ ex nil, split_onames tx ls with - | Some x, (Some n, ls')%core - => option_map (fun C => Named.LetIn tx n x C) (@ocompilef _ (eC n) ls') - | _, _ => None - end - | Pair _ ex _ ey => match @ocompilef _ ex nil, @ocompilef _ ey nil with - | Some x, Some y => Some (Named.Pair x y) - | _, _ => None - end - end. - - Definition ocompile {t} (e : expr t) (ls : list (option Name)) - : option (nexpr t) - := match e in @Syntax.expr _ _ _ t return option (nexpr t) with - | Abs src _ f - => match split_onames src ls with - | (Some n, ls')%core - => option_map (Named.Abs n) (@ocompilef _ (f n) ls') - | _ => None - end - end. - - Definition compilef {t} (e : exprf t) (ls : list Name) := @ocompilef t e (List.map (@Some _) ls). - Definition compile {t} (e : expr t) (ls : list Name) := @ocompile t e (List.map (@Some _) ls). -End language. - -Global Arguments ocompilef {_ _ _ _} e ls. -Global Arguments ocompile {_ _ _ _} e ls. -Global Arguments compilef {_ _ _ _} e ls. -Global Arguments compile {_ _ _ _} e ls. diff --git a/src/Compilers/Named/CompileInterp.v b/src/Compilers/Named/CompileInterp.v deleted file mode 100644 index 20a536ddc..000000000 --- a/src/Compilers/Named/CompileInterp.v +++ /dev/null @@ -1,207 +0,0 @@ -(** * PHOAS → Named Representation of Gallina *) -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.Syntax. -Require Import Crypto.Compilers.Wf. -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. - -Local Open Scope ctype_scope. -Local Open Scope nexpr_scope. -Local Open Scope expr_scope. -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)} - {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_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 (interp_op:=interp_op) (ctx:=ctx) v - = Some (interpf interp_op 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_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 ?e = Some _, H' : context[Named.interpf ?e] |- _ ] - => rewrite H in H' by assumption - | [ H : forall x2 ctx, _ -> Named.interpf ?e = Some _ |- Named.interpf ?e = Some _ ] - => apply H; clear H - | [ H : forall x2, _ -> forall ctx, _ -> Named.interpf ?e = Some _ |- Named.interpf ?e = Some _ ] - => apply 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 - end. - Qed. - - Lemma interp_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 (interp_op:=interp_op) (ctx:=ctx) f v - = Some (interp interp_op 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_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_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 (interp_op:=interp_op) (ctx:=ctx) v - = Some (interpf interp_op e'). - Proof using ContextOk Name_dec base_type_dec. - eapply interpf_ocompilef; try eassumption. - setoid_rewrite List.in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst. - eauto. - Qed. - - Lemma interp_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 (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 {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. diff --git a/src/Compilers/Named/CompileInterpSideConditions.v b/src/Compilers/Named/CompileInterpSideConditions.v deleted file mode 100644 index da8e1d8b2..000000000 --- a/src/Compilers/Named/CompileInterpSideConditions.v +++ /dev/null @@ -1,253 +0,0 @@ -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/CompileProperties.v b/src/Compilers/Named/CompileProperties.v deleted file mode 100644 index 9803946b2..000000000 --- a/src/Compilers/Named/CompileProperties.v +++ /dev/null @@ -1,74 +0,0 @@ -Require Import Coq.omega.Omega. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.NameUtil. -Require Import Crypto.Compilers.Named.NameUtilProperties. -Require Import Crypto.Compilers.Named.Compile. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.CountLets. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.ListUtil. - -Local Notation eta x := (fst x, snd x). - -Local Open Scope ctype_scope. -Local Open Scope nexpr_scope. -Local Open Scope expr_scope. -Section language. - Context (base_type_code : Type) - (op : flat_type base_type_code -> flat_type base_type_code -> Type) - (Name : Type) - (dummy : base_type_code -> Name). - - Local Notation flat_type := (flat_type base_type_code). - Local Notation type := (type base_type_code). - Local Notation exprft := (@exprf base_type_code op (fun _ => unit)). - Local Notation exprt := (@expr base_type_code op (fun _ => unit)). - Local Notation exprf := (@exprf base_type_code op (fun _ => Name)). - Local Notation expr := (@expr base_type_code op (fun _ => Name)). - Local Notation nexprf := (@Named.exprf base_type_code op Name). - Local Notation nexpr := (@Named.expr base_type_code op Name). - - Lemma compilef_count_let_bindersf_enough {t} - (e1 : exprf t) (e2 : exprft t) - G - (Hwf : wff G e1 e2) - : forall (ls1 : list Name) - (He : compilef e1 ls1 <> None) - (ls2 : list Name) - (Hls : List.length ls2 >= count_let_bindersf dummy e1), - compilef e1 ls2 <> None. - Proof. - unfold compilef; induction Hwf; - repeat first [ progress simpl in * - | progress cbv [option_map] in * - | progress subst - | progress inversion_prod - | congruence - | omega - | progress break_innermost_match_step - | progress break_match_hyps - | progress intros - | progress specialize_by congruence - | match goal with - | [ H : forall ls1, ocompilef ?e _ <> None -> _, H' : ocompilef ?e (List.map _ ?ls') = Some _ |- _ ] - => specialize (H ls'); rewrite H' in H - | [ H : forall ls1, ocompilef ?e _ <> None -> _, H' : ocompilef ?e nil = Some _ |- _ ] - => specialize (H nil); simpl in H; rewrite H' in H - | [ H : forall v ls1, ocompilef (?e v) _ <> None -> _, H' : ocompilef (?e ?v') _ = Some _ |- _ ] - => specialize (H v') - | [ H : forall ls1, List.length ls1 >= ?k -> _, H' : List.length _ >= ?k |- _ ] - => specialize (H _ H') - | [ H : context[snd (split_onames _ _)] |- _ ] - => rewrite snd_split_onames_skipn in H - | [ H : context[List.skipn _ (List.map _ _)] |- _] - => rewrite skipn_map in H - | [ H : fst (split_onames ?t (List.map _ ?ls)) = None |- _ ] - => rewrite split_onames_split_names in H - | [ H : fst (split_names _ _) = None |- _ ] - => apply length_fst_split_names_None_iff in H - end ]. - Abort. -End language. diff --git a/src/Compilers/Named/CompileWf.v b/src/Compilers/Named/CompileWf.v deleted file mode 100644 index 3ccff8d58..000000000 --- a/src/Compilers/Named/CompileWf.v +++ /dev/null @@ -1,254 +0,0 @@ -(** * PHOAS → Named Representation of Gallina *) -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Wf. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.ContextProperties.NameUtil. -Require Import Crypto.Compilers.Named.NameUtil. -Require Import Crypto.Compilers.Named.NameUtilProperties. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.Named.Compile. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.DestructHead. - -Local Open Scope ctype_scope. -Local Open Scope nexpr_scope. -Local Open Scope expr_scope. -Section language. - Context {base_type_code var} {var' : base_type_code -> Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type} - {base_type_dec : DecidableRel (@eq base_type_code)} - {Name_dec : DecidableRel (@eq Name)} - {Context : @Context base_type_code Name var} - {ContextOk : ContextOk Context} - {make_var' : forall t, var t -> var' t} (* probably only needed because I was clumsy in the proof method *). - - 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 wff := (@wff base_type_code op (fun _ => Name) var'). - Local Notation wf := (@wf base_type_code op (fun _ => Name) var'). - Local Notation nexprf := (@Named.exprf base_type_code op Name). - Local Notation nexpr := (@Named.expr base_type_code op Name). - Local Notation nwff := (@Named.wff base_type_code Name op var Context). - Local Notation nwf := (@Named.wf base_type_code Name op var Context). - 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). - - Local Ltac finish_with_var' := - (* FIXME: clean this up *) - lazymatch goal with - | [ H : find_Name_and_val _ _ ?b ?n ?i ?v None = Some _ - |- find_Name_and_val _ _ ?b ?n ?i _ None <> None ] - => (is_evar v; - let T := type of v in - let H := fresh in - assert (H : { k : T | k = v })); - [ - | let H' := fresh in - let H'' := fresh in - intro H'; - let T := match type of H with ?T = _ => T end in - assert (H'' : T <> None) by congruence; apply H''; revert H'; - rewrite <- !find_Name_and_val_None_iff; - tauto ] - end; - match goal with - | [ v : interp_flat_type _ ?t |- @sig (interp_flat_type _ ?t) _ ] - => exists (SmartMap.SmartVarfMap make_var' v) - end; - reflexivity. - - Lemma wff_ocompilef (ctx : Context) G - (HG : forall t n v, - List.In (existT _ t (n, v)%core) G -> lookupb t ctx n <> None) - {t} (e : exprf t) e' (ls : list (option Name)) - (Hwf : wff G e e') - 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) - : prop_of_option (nwff ctx v). - Proof using ContextOk Name_dec base_type_dec make_var'. - revert dependent ctx; revert dependent ls; induction Hwf; - repeat first [ progress intros - | progress subst - | progress inversion_option - | solve [ auto ] - | progress simpl in * - | progress unfold option_map in * - | progress break_innermost_match_step - | progress break_match_hyps - | progress autorewrite with push_prop_of_option in * - | progress specialize_by tauto - | progress specialize_by auto using oname_list_unique_nil - | solve [ unfold not in *; eauto using In_skipn, oname_list_unique_firstn, oname_list_unique_skipn ] - | progress destruct_head' or - | match goal with - | [ 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 (?e2 x1) ls = Some v -> _, H : ocompilef (?e2 ?x1') ?ls' = Some ?v' |- _ ] - => specialize (fun x2 => IH _ x2 _ _ H) - | [ HG : forall t n v, List.In _ _ -> _ = Some _, H : _ = None |- _ ] - => erewrite HG in H by eassumption - | [ |- _ /\ _ ] => split - | [ H : context[List.In _ (_ ++ _)] |- _ ] - => setoid_rewrite List.in_app_iff in H - | [ H : split_onames _ _ = (_, _)%core |- _ ] - => pose proof (f_equal (@fst _ _) H); - pose proof (f_equal (@snd _ _) H); - clear H - | [ H : context[snd (split_onames _ _)] |- _ ] - => rewrite snd_split_onames_skipn in H - | [ H : forall a, (forall x y z, _ \/ _ -> _) -> _ |- _ ] - => specialize (fun a pf1 pf2 - => H a (fun x y z pf - => match pf with - | or_introl pf' => pf1 x y z pf' - | or_intror pf' => pf2 x y z pf' - end)) - | [ H : forall a b, (forall x y z, _ \/ _ -> _) -> _ |- _ ] - => specialize (fun a b pf1 pf2 - => H a b (fun x y z pf - => match pf with - | or_introl pf' => pf1 x y z pf' - | or_intror pf' => pf2 x y z pf' - end)) - | [ H : forall a b c, (forall x y z, _ \/ _ -> _) -> _ |- _ ] - => specialize (fun a b c pf1 pf2 - => H a b c (fun x y z pf - => match pf with - | or_introl pf' => pf1 x y z pf' - | or_intror pf' => pf2 x y z pf' - end)) - | [ H : forall a b c d, (forall x y z, _ \/ _ -> _) -> _ |- _ ] - => specialize (fun a b c d pf1 pf2 - => H a b c d (fun x y z pf - => match pf with - | or_introl pf' => pf1 x y z pf' - | or_intror pf' => pf2 x y z pf' - end)) - | [ H : _ |- _ ] - => progress rewrite ?firstn_nil, ?skipn_nil, ?skipn_skipn in H - | [ H : List.In ?x (List.firstn ?a (List.skipn ?b ?ls)), H' : List.In ?x (List.skipn (?b + ?a) ?ls) |- False ] - => rewrite firstn_skipn_add in H; apply In_skipn in H - | [ H : ?T |- prop_of_option (nwff _ ?v) ] - => eapply 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 - end. - finish_with_var'. - Qed. - - Lemma wf_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) - : nwf ctx f. - Proof using ContextOk Name_dec base_type_dec make_var'. - 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 ]. - intro; simpl. - eapply wff_ocompilef; - [ | solve [ 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 - | eassumption - | 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 ]. - finish_with_var'. } - Qed. - - Lemma wff_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 <> None) - 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) - : prop_of_option (nwff ctx v). - Proof using ContextOk Name_dec base_type_dec make_var'. - eapply wff_ocompilef; try eassumption. - setoid_rewrite List.in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst. - eauto. - Qed. - - Lemma wf_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) - : nwf ctx f. - Proof using ContextOk Name_dec base_type_dec make_var'. eapply wf_ocompile; eassumption. Qed. -End language. diff --git a/src/Compilers/Named/Context.v b/src/Compilers/Named/Context.v deleted file mode 100644 index fd84e5b94..000000000 --- a/src/Compilers/Named/Context.v +++ /dev/null @@ -1,65 +0,0 @@ -(** * Contexts for Named Representation of Gallina *) -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Util.Notations. - -Record Context {base_type_code} (Name : Type) (var : base_type_code -> Type) := - { ContextT : Type; - lookupb : forall {t : base_type_code}, ContextT -> Name -> option (var t); - extendb : forall {t : base_type_code}, ContextT -> Name -> var t -> ContextT; - removeb : base_type_code -> ContextT -> Name -> ContextT; - empty : ContextT }. -Coercion ContextT : Context >-> Sortclass. -Arguments ContextT {_ _ _ _}, {_ _ _} _. -Arguments lookupb {_ _ _ _ _} _ _, {_ _ _ _} _ _ _. -Arguments extendb {_ _ _ _} [_] _ _ _. -Arguments removeb {_ _ _ _} _ _ _. -Arguments empty {_ _ _ _}. - -Section language. - Context {base_type_code : Type} - {Name : Type} - {var : base_type_code -> Type} - {Context : Context Name var}. - - Local Notation flat_type := (flat_type base_type_code). - - Fixpoint extend {t : flat_type} (ctx : Context) - (n : interp_flat_type (fun _ => Name) t) (v : interp_flat_type var t) - : Context - := match t return interp_flat_type (fun _ => Name) t -> interp_flat_type var t -> Context with - | Tbase t => fun n v => extendb ctx n v - | Unit => fun _ _ => ctx - | Prod A B => fun n v : interp_flat_type _ A * interp_flat_type _ B - => let ctx := @extend A ctx (fst n) (fst v) in - let ctx := @extend B ctx (snd n) (snd v) in - ctx - end n v. - - Fixpoint remove {t : flat_type} (ctx : Context) - (n : interp_flat_type (fun _ => Name) t) - : Context - := match t return interp_flat_type (fun _ => Name) t -> Context with - | Tbase t => fun n => removeb t ctx n - | Unit => fun _ => ctx - | Prod A B => fun n : interp_flat_type _ A * interp_flat_type _ B - => let ctx := @remove A ctx (fst n) in - let ctx := @remove B ctx (snd n) in - ctx - end n. - - Definition lookup {t} (ctx : Context) - : interp_flat_type (fun _ => Name) t -> option (interp_flat_type var t) - := smart_interp_flat_map - (g := fun t => option (interp_flat_type var t)) - (fun t v => lookupb ctx v) - (Some tt) - (fun A B x y => match x, y with - | Some x', Some y' => Some (x', y')%core - | _, _ => None - end). -End language. - -Global Arguments extend {_ _ _ _} {_} ctx _ _. -Global Arguments remove {_ _ _ _} {_} ctx _. -Global Arguments lookup {_ _ _ _} {_} ctx _, {_ _ _ _} _ ctx _. diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v deleted file mode 100644 index 1b57e5b51..000000000 --- a/src/Compilers/Named/ContextDefinitions.v +++ /dev/null @@ -1,67 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Decidable. - -Section with_context. - Context {base_type_code Name var} (Context : @Context base_type_code Name var) - (base_type_code_dec : DecidableRel (@eq base_type_code)) - (Name_dec : DecidableRel (@eq Name)). - - Fixpoint find_Name n - {T : flat_type base_type_code} - : interp_flat_type (fun _ => Name) T -> option base_type_code - := match T with - | Tbase t' => fun n' : Name => if dec (n = n') then Some t' else None - | Unit => fun _ => None - | Prod A B - => fun ab : interp_flat_type _ A * interp_flat_type _ B - => match @find_Name n B (snd ab), @find_Name n A (fst ab) with - | Some tb, _ => Some tb - | None, Some ta => Some ta - | None, None => None - end - end. - - Fixpoint find_Name_and_val {var'} t (n : Name) - {T : flat_type base_type_code} - : interp_flat_type (fun _ => Name) T -> interp_flat_type var' T -> option (var' t) -> option (var' t) - := match T with - | Tbase t' => fun (n' : Name) v default - => if dec (n = n') - then cast_if_eq t' t v - else default - | Unit => fun _ _ default => default - | Prod A B - => fun (ab : interp_flat_type _ A * interp_flat_type _ B) - (a'b' : interp_flat_type _ A * interp_flat_type _ B) - default - => @find_Name_and_val - var' t n B (snd ab) (snd a'b') - (@find_Name_and_val - var' t n A (fst ab) (fst a'b') - default) - end. - - Class ContextOk := - { lookupb_extendb_same - : forall (ctx : Context) n t v, lookupb t (extendb ctx n (t:=t) v) n = Some v; - lookupb_extendb_different - : forall (ctx : Context) n n' t t' v, n <> n' -> lookupb t' (extendb ctx n (t:=t) v) n' - = lookupb t' ctx n'; - lookupb_extendb_wrong_type - : forall (ctx : Context) n t t' v, t <> t' -> lookupb t' (extendb ctx n (t:=t) v) n = None; - lookupb_removeb_different - : forall (ctx : Context) n n' t t', n <> n' -> lookupb t' (removeb t ctx n) n' - = lookupb t' ctx n'; - lookupb_removeb_same - : forall (ctx : Context) n t t', lookupb t' (removeb t ctx n) n = None; - lookupb_empty - : forall n t, lookupb t (@empty _ _ _ Context) n = None; - - lookupb_unique_type - : forall (ctx : Context) n t t', lookupb t' ctx n <> None -> lookupb t ctx n <> None -> t = t' }. - - Definition context_equiv (a b : Context) - := forall n t, lookupb t a n = lookupb t b n. -End with_context. diff --git a/src/Compilers/Named/ContextOn.v b/src/Compilers/Named/ContextOn.v deleted file mode 100644 index 17d8690fc..000000000 --- a/src/Compilers/Named/ContextOn.v +++ /dev/null @@ -1,24 +0,0 @@ -(** * Transfer [Context] across an injection *) -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.ContextDefinitions. - -Section language. - Context {base_type_code Name1 Name2 : Type} - (f : Name2 -> Name1) - (f_inj : forall x y, f x = f y -> x = y) - {var : base_type_code -> Type}. - - Definition ContextOn (Ctx : Context Name1 var) : Context Name2 var - := {| ContextT := Ctx; - lookupb t ctx n := lookupb t ctx (f n); - extendb t ctx n v := extendb ctx (f n) v; - removeb t ctx n := removeb t ctx (f n); - empty := empty |}. - - Lemma ContextOnOk {Ctx} (COk : ContextOk Ctx) : ContextOk (ContextOn Ctx). - Proof. - unfold ContextOn in *; split; intros; try eapply COk; eauto. - Qed. -End language. - -Arguments ContextOnOk {_ _ _ f} f_inj {_ _} COk. diff --git a/src/Compilers/Named/ContextProperties.v b/src/Compilers/Named/ContextProperties.v deleted file mode 100644 index 782fc9a54..000000000 --- a/src/Compilers/Named/ContextProperties.v +++ /dev/null @@ -1,181 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.ContextProperties.Tactics. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Tactics.BreakMatch. - -Section with_context. - Context {base_type_code} - (base_type_code_dec : DecidableRel (@eq base_type_code)) - {Name} - (Name_dec : DecidableRel (@eq Name)) - {var} (Context : @Context base_type_code Name var) - (ContextOk : ContextOk Context). - - Local Notation find_Name := (@find_Name base_type_code Name Name_dec). - Local Notation find_Name_and_val := (@find_Name_and_val base_type_code Name base_type_code_dec Name_dec). - - Lemma lookupb_eq_cast - : forall (ctx : Context) n t t' (pf : t = t'), - lookupb t' ctx n = option_map (fun v => eq_rect _ var v _ pf) (lookupb t ctx n). - Proof. - intros; subst; edestruct lookupb; reflexivity. - Defined. - Lemma lookupb_extendb_eq - : forall (ctx : Context) n t t' (pf : t = t') v, - lookupb t' (extendb ctx n (t:=t) v) n = Some (eq_rect _ var v _ pf). - Proof. - intros; subst; apply lookupb_extendb_same; assumption. - Defined. - - Lemma lookupb_extendb_full (ctx : Context) n n' t t' v - : lookupb t' (extendb ctx n (t:=t) v) n' - = match dec (n = n'), dec (t = t') with - | left _, left pf - => Some (eq_rect _ var v _ pf) - | left _, _ - => None - | right _, _ - => lookupb t' ctx n' - end. - Proof using ContextOk. - break_innermost_match; subst; simpl. - { apply lookupb_extendb_same; assumption. } - { apply lookupb_extendb_wrong_type; assumption. } - { apply lookupb_extendb_different; assumption. } - Qed. - - Lemma lookupb_extend (ctx : Context) - T N t n v - : lookupb t (extend ctx N (t:=T) v) n - = find_Name_and_val t n N v (lookupb t ctx n). - Proof using ContextOk. revert ctx; induction T; t. Qed. - - Lemma lookupb_remove (ctx : Context) - T N t n - : lookupb t (remove ctx N) n - = match @find_Name n T N with - | Some _ => None - | None => lookupb t ctx n - end. - Proof using ContextOk. revert ctx; induction T; t. Qed. - - Lemma lookupb_remove_not_in (ctx : Context) - T N t n - (H : @find_Name n T N = None) - : lookupb t (remove ctx N) n = lookupb t ctx n. - Proof using ContextOk. rewrite lookupb_remove, H; reflexivity. Qed. - - Lemma lookupb_remove_in (ctx : Context) - T N t n - (H : @find_Name n T N <> None) - : lookupb t (remove ctx N) n = None. - Proof using ContextOk. rewrite lookupb_remove; break_match; congruence. Qed. - - Lemma find_Name_and_val_Some_None - {var' var''} - {t n T N} - {x : interp_flat_type var' T} - {y : interp_flat_type var'' T} - {default default' v} - (H0 : @find_Name_and_val var' t n T N x default = Some v) - (H1 : @find_Name_and_val var'' t n T N y default' = None) - : default = Some v /\ default' = None. - Proof using Type. - revert dependent default; revert dependent default'; induction T; t. - Qed. - - Lemma find_Name_and_val_default_to_None - {var'} - {t n T N} - {x : interp_flat_type var' T} - {default} - (H : @find_Name n T N <> None) - : @find_Name_and_val var' t n T N x default - = @find_Name_and_val var' t n T N x None. - Proof using Type. revert default; induction T; t. Qed. - Hint Rewrite @find_Name_and_val_default_to_None using congruence : ctx_db. - - Lemma find_Name_and_val_different - {var'} - {t n T N} - {x : interp_flat_type var' T} - {default} - (H : @find_Name n T N = None) - : @find_Name_and_val var' t n T N x default = default. - Proof using Type. revert default; induction T; t. Qed. - Hint Rewrite @find_Name_and_val_different using assumption : ctx_db. - - Lemma find_Name_and_val_wrong_type_iff - {var'} - {t t' n T N} - {x : interp_flat_type var' T} - {default} - (H : @find_Name n T N = Some t') - : t <> t' - <-> @find_Name_and_val var' t n T N x default = None. - Proof using Type. split; revert default; induction T; t. Qed. - Lemma find_Name_and_val_wrong_type - {var'} - {t t' n T N} - {x : interp_flat_type var' T} - {default} - (H : @find_Name n T N = Some t') - (Ht : t <> t') - : @find_Name_and_val var' t n T N x default = None. - Proof using Type. eapply find_Name_and_val_wrong_type_iff; eassumption. Qed. - Hint Rewrite @find_Name_and_val_wrong_type using congruence : ctx_db. - - Lemma find_Name_find_Name_and_val_wrong {var' n t' T V N} - : find_Name n N = Some t' - -> @find_Name_and_val var' t' n T N V None = None - -> False. - Proof using Type. induction T; t. Qed. - - Lemma find_Name_and_val_None_iff - {var'} - {t n T N} - {x : interp_flat_type var' T} - {default} - : (@find_Name n T N <> Some t - /\ (@find_Name n T N <> None \/ default = None)) - <-> @find_Name_and_val var' t n T N x default = None. - Proof using Type. - destruct (@find_Name n T N) eqn:?; unfold not; t; - try solve [ eapply find_Name_and_val_wrong_type; [ eassumption | congruence ] - | eapply find_Name_find_Name_and_val_wrong; eassumption - | left; congruence ]. - Qed. - - Lemma find_Name_and_val_split - {var' t n T N V default} - : @find_Name_and_val var' t n T N V default - = match @find_Name n T N with - | Some t' => if dec (t = t') - then @find_Name_and_val var' t n T N V None - else None - | None => default - end. - Proof using Type. - t; erewrite find_Name_and_val_wrong_type by solve [ eassumption | congruence ]; reflexivity. - Qed. - Lemma find_Name_and_val_find_Name_Some - {var' t n T N V v} - (H : @find_Name_and_val var' t n T N V None = Some v) - : @find_Name n T N = Some t. - Proof using Type. - rewrite find_Name_and_val_split in H; break_match_hyps; subst; congruence. - Qed. -End with_context. - -Ltac find_Name_and_val_default_to_None_step := - match goal with - | [ H : context[find_Name_and_val ?tdec ?ndec _ _ _ _ ?default] |- _ ] - => lazymatch default with None => fail | _ => idtac end; - rewrite (find_Name_and_val_split tdec ndec (default:=default)) in H - | [ |- context[find_Name_and_val ?tdec ?ndec _ _ _ _ ?default] ] - => lazymatch default with None => fail | _ => idtac end; - rewrite (find_Name_and_val_split tdec ndec (default:=default)) - end. -Ltac find_Name_and_val_default_to_None := repeat find_Name_and_val_default_to_None_step. diff --git a/src/Compilers/Named/ContextProperties/NameUtil.v b/src/Compilers/Named/ContextProperties/NameUtil.v deleted file mode 100644 index 320d910f0..000000000 --- a/src/Compilers/Named/ContextProperties/NameUtil.v +++ /dev/null @@ -1,161 +0,0 @@ -Require Import Coq.omega.Omega. -Require Import Crypto.Util.FixCoqMistakes. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.NameUtil. -Require Import Crypto.Compilers.Named.NameUtilProperties. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.ContextProperties.Tactics. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. - -Section with_context. - Context {base_type_code Name var} (Context : @Context base_type_code Name var) - (base_type_code_dec : DecidableRel (@eq base_type_code)) - (Name_dec : DecidableRel (@eq Name)) - (ContextOk : ContextOk Context). - - Local Notation find_Name := (@find_Name base_type_code Name Name_dec). - Local Notation find_Name_and_val := (@find_Name_and_val base_type_code Name base_type_code_dec Name_dec). - - Hint Rewrite (@find_Name_and_val_default_to_None _ base_type_code_dec _ Name_dec) using congruence : ctx_db. - Hint Rewrite (@find_Name_and_val_different _ base_type_code_dec _ Name_dec) using assumption : ctx_db. - Hint Rewrite (@find_Name_and_val_wrong_type _ base_type_code_dec _ Name_dec) using congruence : ctx_db. - Hint Rewrite (@snd_split_onames_skipn base_type_code Name) : ctx_db. - - Local Ltac misc_oname_t_step := - match goal with - | [ H : oname_list_unique (List.skipn _ _) -> _ |- _ ] - => specialize (fun pf => H (@oname_list_unique_skipn _ _ _ pf)) - | [ H : ((_, _) = (_, _))%core -> _ |- _ ] - => specialize (fun a b => H (f_equal2 (@pair _ _) a b)) - | [ H : ?x = (_,_)%core -> _ |- _ ] - => rewrite (surjective_pairing x) in H; - specialize (fun a b => H (f_equal2 (@pair _ _) a b)) - end. - - Lemma split_onames_find_Name - {n T N ls ls'} - (H : split_onames _ ls = (Some N, ls')%core) - : (exists t, @find_Name n T N = Some t) - <-> List.In (Some n) (List.firstn (CountLets.count_pairs T) ls). - Proof using Type. - revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' H; - [ | | specialize (IHT1 (fst N) ls (snd (split_onames T1 ls))); - specialize (IHT2 (snd N) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ]; - repeat first [ misc_oname_t_step - | t_step - | progress split_iff - | progress specialize_by (eexists; eauto) - | solve [ eauto using In_skipn, In_firstn ] - | match goal with - | [ H : List.In ?x (List.firstn ?n ?ls) |- List.In ?x (List.firstn (?n + ?m) ?ls) ] - => apply (In_firstn n); rewrite firstn_firstn by omega - | [ H : _ |- _ ] => first [ rewrite firstn_skipn_add in H - | rewrite firstn_firstn in H by omega ] - | [ H : List.In ?x' (List.firstn (?n + ?m) ?ls) |- List.In ?x' (List.firstn ?m (List.skipn ?n ?ls)) ] - => apply (In_firstn_skipn_split n) in H - end ]. - Qed. - - Lemma split_onames_find_Name_Some_unique_iff - {n T N ls ls'} - (Hls : oname_list_unique ls) - (H : split_onames _ ls = (Some N, ls')%core) - : (exists t, @find_Name n T N = Some t) - <-> List.In (Some n) ls /\ ~List.In (Some n) ls'. - Proof using Type. - rewrite (split_onames_find_Name (ls':=ls') (ls:=ls)) by assumption. - rewrite (surjective_pairing (split_onames _ _)) in H. - rewrite fst_split_onames_firstn, snd_split_onames_skipn in H. - inversion_prod; subst. - split; [ split | intros [? ?] ]; eauto using In_firstn, oname_list_unique_specialize. - match goal with - | [ H : List.In (Some _) ?ls |- _ ] - => is_var ls; - eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto - end. - Qed. - - Lemma split_onames_find_Name_Some_unique - {t n T N ls ls'} - (Hls : oname_list_unique ls) - (H : split_onames _ ls = (Some N, ls')%core) - (Hfind : @find_Name n T N = Some t) - : List.In (Some n) ls /\ ~List.In (Some n) ls'. - Proof using Type. - eapply split_onames_find_Name_Some_unique_iff; eauto. - Qed. - - Lemma flatten_binding_list_find_Name_and_val_unique - {var' t n T N V v ls ls'} - (Hls : oname_list_unique ls) - (H : split_onames _ ls = (Some N, ls')%core) - : @find_Name_and_val var' t n T N V None = Some v - <-> List.In (existT (fun t => (Name * var' t)%type) t (n, v)) (Wf.flatten_binding_list N V). - Proof using Type. - revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' Hls H; - [ | | specialize (IHT1 (fst N) (fst V) ls (snd (split_onames T1 ls))); - specialize (IHT2 (snd N) (snd V) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ]; - repeat first [ find_Name_and_val_default_to_None_step - | progress simpl in * - | rewrite List.in_app_iff - | misc_oname_t_step - | t_step - | progress split_iff - | lazymatch goal with - | [ H : find_Name ?n ?x = Some ?t, H' : find_Name_and_val ?t' ?n ?X ?V None = Some ?v |- _ ] - => apply find_Name_and_val_find_Name_Some in H' - | [ H : find_Name ?n ?x = Some ?t, H' : find_Name ?n ?x' = Some ?t' |- _ ] - => let apply_in_tac H := - (eapply 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 ] ]) in - first [ constr_eq x x'; fail 1 - | apply_in_tac H; apply_in_tac H' ] - end ]. - Qed. - - Lemma fst_split_mnames__flatten_binding_list__find_Name - (MName : Type) (force : MName -> option Name) - {var' t n T N V v} {ls : list MName} - (Hs : fst (split_mnames force T ls) = Some N) - (HN : List.In (existT _ t (n, v)%core) (Wf.flatten_binding_list (var2:=var') N V)) - : find_Name n N = Some t. - Proof. - revert dependent ls; induction T; - [ | | specialize (IHT1 (fst N) (fst V)); - specialize (IHT2 (snd N) (snd V)) ]; - repeat first [ misc_oname_t_step - | t_step - | match goal with - | [ H : _ |- _ ] => first [ rewrite snd_split_mnames_skipn in H - | rewrite List.in_app_iff in H ] - | [ H : context[fst (split_mnames _ _ ?ls)] |- _ ] - => is_var ls; rewrite (@fst_split_mnames_firstn _ _ _ _ _ ls) in H - end ]. - Abort. - - Lemma fst_split_mnames__find_Name__flatten_binding_list - (MName : Type) (force : MName -> option Name) - {var' t n T N V v default} {ls : list MName} - (Hs : fst (split_mnames force T ls) = Some N) - (Hfind : find_Name n N = Some t) - (HN : List.In (existT _ t (n, v)%core) (Wf.flatten_binding_list N V)) - : @find_Name_and_val var' t n T N V default = Some v. - Proof. - revert default; revert dependent ls; induction T; - [ | | specialize (IHT1 (fst N) (fst V)); - specialize (IHT2 (snd N) (snd V)) ]; - repeat first [ find_Name_and_val_default_to_None_step - | rewrite List.in_app_iff in * - | t_step ]. - Abort. -End with_context. diff --git a/src/Compilers/Named/ContextProperties/Proper.v b/src/Compilers/Named/ContextProperties/Proper.v deleted file mode 100644 index 0c583e446..000000000 --- a/src/Compilers/Named/ContextProperties/Proper.v +++ /dev/null @@ -1,142 +0,0 @@ -Require Import Coq.Classes.Morphisms. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.RewriteHyp. -Require Import Crypto.Util.Tactics.DestructHead. - -Section with_context. - Context {base_type_code} - {base_type_code_dec : DecidableRel (@eq base_type_code)} - {Name} - {Name_dec : DecidableRel (@eq Name)} - {var} {Context : @Context base_type_code Name var} - {ContextOk : ContextOk Context}. - - Local Notation context_equiv := (@context_equiv base_type_code Name var Context). - Local Notation extendb := (@extendb base_type_code Name var Context). - Local Notation removeb := (@removeb base_type_code Name var Context). - Local Notation lookupb := (@lookupb base_type_code Name var Context). - Local Notation extend := (@extend base_type_code Name var Context). - Local Notation remove := (@remove base_type_code Name var Context). - Local Notation lookup := (@lookup base_type_code Name var Context). - - Global Instance context_equiv_Equivalence : Equivalence context_equiv | 10. - Proof. split; repeat intro; congruence. Qed. - Global Instance context_equiv_Reflexive : Reflexive context_equiv | 10 := _. - Global Instance context_equiv_Symmetric : Symmetric context_equiv | 10 := _. - Global Instance context_equiv_Transitive : Transitive context_equiv | 10 := _. - - Local Ltac proper_t n n' t t' := - destruct (dec (n = n')), (dec (t = t')); subst; - repeat first [ reflexivity - | rewrite lookupb_extendb_same by assumption - | rewrite lookupb_extendb_different by assumption - | rewrite lookupb_extendb_wrong_type by assumption - | rewrite lookupb_removeb_same by assumption - | rewrite lookupb_removeb_different by assumption - | solve [ auto ] ]. - - Global Instance extendb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10. - Proof. - intros t ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'. - Qed. - Global Instance removeb_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10. - Proof. - intros t ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'. - Qed. - Global Instance lookupb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10. - Proof. repeat intro; subst; auto. Qed. - - Local Ltac proper_t2 t := - let IHt1 := fresh "IHt1" in - let IHt2 := fresh "IHt2" in - induction t as [ | | ? IHt1 ? IHt2]; - simpl; - repeat match goal with - | [ |- context[fun a b => ?f a b] ] - => change (fun a b => f a b) with f - end; - [ try exact _ - | repeat intro; auto - | repeat intro; subst; - destruct_head_prod; - first [ eapply IHt2; [ eapply IHt1 | .. ]; auto - | idtac ] ]. - - Global Instance extend_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10. - Proof. intro t; proper_t2 t. Qed. - Global Instance remove_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10. - Proof. intro t; proper_t2 t. Qed. - - Global Instance lookup_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10. - Proof. - intro t; proper_t2 t. - repeat match goal with - | [ |- context G[lookup (?A * ?B) ?ctx (?na, ?nb)] ] - => let G' := context G[match lookup A ctx na, lookup B ctx nb with - | Some a, Some b => Some (a, b) - | _, _ => None - end] in - change G' - end. - break_innermost_match; - repeat match goal with - | _ => progress subst - | _ => progress inversion_option - | _ => reflexivity - | [ IHt2 : Proper _ (lookup t2), H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ] - => assert (x = y) - by (rewrite <- H, <- H'; first [ eapply IHt1 | eapply IHt2 ]; (assumption || reflexivity)); - clear H H' - end. - Qed. -End with_context. - -Section language. - Context {base_type_code} - {base_type_code_dec : DecidableRel (@eq base_type_code)} - {Name} - {Name_dec : DecidableRel (@eq Name)} - {op : flat_type base_type_code -> flat_type base_type_code -> 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} - {Context : @Context base_type_code Name interp_base_type} - {ContextOk : ContextOk Context}. - - Local Notation context_equiv := (@context_equiv base_type_code Name interp_base_type Context). - Local Notation interpf := (@interpf base_type_code interp_base_type op Name Context interp_op). - Local Notation interp := (@interp base_type_code interp_base_type op Name Context interp_op). - - Global Instance interpf_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@interpf t). - Proof. - intros c0 c1 Hc e e' ?; subst e'; revert c0 c1 Hc. - induction e; - repeat first [ progress subst - | reflexivity - | progress inversion_option - | progress simpl in * - | progress unfold LetIn.Let_In - | intros; eapply lookupb_Proper; (assumption || reflexivity) - | intros; eapply extendb_Proper; (assumption || reflexivity) - | intros; eapply lookup_Proper; (assumption || reflexivity) - | intros; eapply extend_Proper; (assumption || reflexivity) - | intros; erewrite_hyp *; [ | eassumption ] - | intros; erewrite_hyp *; [ reflexivity | ] - | break_innermost_match_step - | match goal with - | [ H : interpf _ = ?x, H' : interpf _ = ?y |- _ ] - => assert (x = y) by (rewrite <- H, <- H'; eauto); clear H H' - end ]. - Qed. - - Global Instance interp_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> eq) (@interp t). - Proof. - intros ??? e e' ????; subst e'; subst. - eapply interpf_Proper; [ eapply extend_Proper; auto | reflexivity ]. - Qed. -End language. diff --git a/src/Compilers/Named/ContextProperties/SmartMap.v b/src/Compilers/Named/ContextProperties/SmartMap.v deleted file mode 100644 index 2bfba38dc..000000000 --- a/src/Compilers/Named/ContextProperties/SmartMap.v +++ /dev/null @@ -1,299 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.ContextProperties.Tactics. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Tactics.BreakMatch. - -Section with_context. - Context {base_type_code Name var} (Context : @Context base_type_code Name var) - (base_type_code_dec : DecidableRel (@eq base_type_code)) - (Name_dec : DecidableRel (@eq Name)) - (ContextOk : ContextOk Context). - - Local Notation find_Name := (@find_Name base_type_code Name Name_dec). - Local Notation find_Name_and_val := (@find_Name_and_val base_type_code Name base_type_code_dec Name_dec). - - Hint Rewrite (@find_Name_and_val_default_to_None _ base_type_code_dec _ Name_dec) using congruence : ctx_db. - Hint Rewrite (@find_Name_and_val_different _ base_type_code_dec _ Name_dec) using assumption : ctx_db. - Hint Rewrite (@find_Name_and_val_wrong_type _ base_type_code_dec _ Name_dec) using congruence : ctx_db. - - Lemma find_Name_and_val_flatten_binding_list - {var' var'' t n T N V1 V2 v1 v2} - (H1 : @find_Name_and_val var' t n T N V1 None = Some v1) - (H2 : @find_Name_and_val var'' t n T N V2 None = Some v2) - : List.In (existT (fun t => (var' t * var'' t)%type) t (v1, v2)) (Wf.flatten_binding_list V1 V2). - Proof using Type. - induction T; - [ | | specialize (IHT1 (fst N) (fst V1) (fst V2)); - specialize (IHT2 (snd N) (snd V1) (snd V2)) ]; - repeat first [ find_Name_and_val_default_to_None_step - | rewrite List.in_app_iff - | t_step ]. - Qed. - - Lemma find_Name_SmartFlatTypeMapInterp2_None_iff {var' n f T V N} - : @find_Name n (SmartFlatTypeMap f (t:=T) V) - (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None - <-> find_Name n N = None. - Proof using Type. - split; - (induction T; - [ | | specialize (IHT1 (fst V) (fst N)); - specialize (IHT2 (snd V) (snd N)) ]); - t. - Qed. - Hint Rewrite @find_Name_SmartFlatTypeMapInterp2_None_iff : ctx_db. - Lemma find_Name_SmartFlatTypeMapInterp2_None {var' n f T V N} - : @find_Name n (SmartFlatTypeMap f (t:=T) V) - (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None - -> find_Name n N = None. - Proof using Type. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed. - Hint Rewrite @find_Name_SmartFlatTypeMapInterp2_None using eassumption : ctx_db. - Lemma find_Name_SmartFlatTypeMapInterp2_None' {var' n f T V N} - : find_Name n N = None - -> @find_Name n (SmartFlatTypeMap f (t:=T) V) - (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None. - Proof using Type. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed. - Lemma find_Name_SmartFlatTypeMapInterp2_None_Some_wrong {var' n f T V N v} - : @find_Name n (SmartFlatTypeMap f (t:=T) V) - (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None - -> find_Name n N = Some v - -> False. - Proof using Type. - intro; erewrite find_Name_SmartFlatTypeMapInterp2_None by eassumption; congruence. - Qed. - Local Hint Resolve @find_Name_SmartFlatTypeMapInterp2_None_Some_wrong. - - Lemma find_Name_SmartFlatTypeMapInterp2 {var' n f T V N} - : @find_Name n (SmartFlatTypeMap f (t:=T) V) - (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) - = match find_Name n N with - | Some t' => match find_Name_and_val t' n N V None with - | Some v => Some (f t' v) - | None => None - end - | None => None - end. - Proof using Type. - induction T; - [ | | specialize (IHT1 (fst V) (fst N)); - specialize (IHT2 (snd V) (snd N)) ]. - { t. } - { t. } - { repeat first [ fin_t_step - | inversion_step - | rewrite_lookupb_extendb_step - | misc_t_step - | refolder_t_step ]. - repeat match goal with - | [ |- context[match @find_Name ?n ?T ?N with _ => _ end] ] - => destruct (@find_Name n T N) eqn:? - | [ H : context[match @find_Name ?n ?T ?N with _ => _ end] |- _ ] - => destruct (@find_Name n T N) eqn:? - end; - repeat first [ fin_t_step - | rewriter_t_step - | fin_t_late_step ]. } - Qed. - - Lemma find_Name_and_val__SmartFlatTypeMapInterp2__SmartFlatTypeMapUnInterp__Some_Some_alt - {var' var'' var''' t b n f g T V N X v v'} - (Hfg - : forall (V : var' t) (X : var'' (f t V)) (H : f t V = f t b), - g t b (eq_rect (f t V) var'' X (f t b) H) = g t V X) - : @find_Name_and_val - var'' (f t b) n (SmartFlatTypeMap f (t:=T) V) - (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) X None = Some v - -> @find_Name_and_val - var''' t n T N (SmartFlatTypeMapUnInterp (f:=f) g X) None = Some v' - -> g t b v = v'. - Proof using Type. - induction T; - [ | | specialize (IHT1 (fst V) (fst N) (fst X)); - specialize (IHT2 (snd V) (snd N) (snd X)) ]; - repeat first [ find_Name_and_val_default_to_None_step - | t_step - | match goal with - | [ H : _ |- _ ] - => progress rewrite find_Name_and_val_different in H - by solve [ congruence - | apply find_Name_SmartFlatTypeMapInterp2_None'; assumption ] - end ]. - Qed. - - Lemma find_Name_and_val__SmartFlatTypeMapInterp2__SmartFlatTypeMapUnInterp__Some_Some - {var' var'' var''' t b n f g T V N X v v'} - : @find_Name_and_val - var'' (f t b) n (SmartFlatTypeMap f (t:=T) V) - (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) X None = Some v - -> @find_Name_and_val - _ t n T N V None = Some b - -> @find_Name_and_val - var''' t n T N (SmartFlatTypeMapUnInterp (f:=f) g X) None = Some v' - -> g t b v = v'. - Proof using Type. - induction T; - [ | | specialize (IHT1 (fst V) (fst N) (fst X)); - specialize (IHT2 (snd V) (snd N) (snd X)) ]; - repeat first [ find_Name_and_val_default_to_None_step - | t_step - | match goal with - | [ H : _ |- _ ] - => progress rewrite find_Name_and_val_different in H - by solve [ congruence - | apply find_Name_SmartFlatTypeMapInterp2_None'; assumption ] - end ]. - Qed. - - Lemma interp_flat_type_rel_pointwise__find_Name_and_val - {var' var'' t n T N x y R v0 v1} - (H0 : @find_Name_and_val var' t n T N x None = Some v0) - (H1 : @find_Name_and_val var'' t n T N y None = Some v1) - (HR : interp_flat_type_rel_pointwise R x y) - : R _ v0 v1. - Proof using Type. - induction T; - [ | | specialize (IHT1 (fst N) (fst x) (fst y)); - specialize (IHT2 (snd N) (snd x) (snd y)) ]; - repeat first [ find_Name_and_val_default_to_None_step - | t_step ]. - Qed. - - Lemma find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_Some - {var' var'' var''' f g} - {T} - {N : interp_flat_type (fun _ : base_type_code => Name) T} - {B : interp_flat_type var' T} - {V : interp_flat_type var'' (SmartFlatTypeMap (t:=T) f B)} - {n : Name} - {t : base_type_code} - {v : var''' t} - {b} - {h} {i : forall v, var'' (f _ (h v))} - (Hn : find_Name n N = Some t) - (Hf : find_Name_and_val t n N (SmartFlatTypeMapUnInterp2 g V) None = Some v) - (Hb : find_Name_and_val t n N B None = Some b) - (Hig : forall B V, - existT _ (h (g _ B V)) (i (g _ B V)) - = existT _ B V - :> { b : _ & var'' (f _ b)}) - (N' := SmartFlatTypeMapInterp2 (var'':=fun _ => Name) (f:=f) (fun _ _ n => n) _ N) - : b = h v /\ find_Name_and_val (f t (h v)) n N' V None = Some (i v). - Proof using Type. - induction T; - [ | | specialize (IHT1 (fst N) (fst B) (fst V)); - specialize (IHT2 (snd N) (snd B) (snd V)) ]; - repeat first [ find_Name_and_val_default_to_None_step - | lazymatch goal with - | [ H : context[find_Name ?n (@SmartFlatTypeMapInterp2 _ ?var' _ _ ?f _ ?T ?V ?N)] |- _ ] - => setoid_rewrite find_Name_SmartFlatTypeMapInterp2 in H - end - | t_step - | match goal with - | [ Hhg : forall B V, existT _ (?h (?g ?t B V)) _ = existT _ B _ |- context[?h (?g ?t ?B' ?V')] ] - => specialize (Hhg B' V'); generalize dependent (g t B' V') - end ]. - Qed. -End with_context. - -Section with_context2. - Context {base_type_code1 base_type_code2 Name var1 var2} - {Context1 : @Context base_type_code1 Name var1} - {Context2 : @Context base_type_code2 Name var2} - {base_type_code1_dec : DecidableRel (@eq base_type_code1)} - {base_type_code2_dec : DecidableRel (@eq base_type_code2)} - {Name_dec : DecidableRel (@eq Name)} - {Context1Ok : ContextOk Context1} - {Context2Ok : ContextOk Context2} - {f_base : base_type_code1 -> base_type_code2} - {cast_backb: forall t, var2 (f_base t) -> var1 t}. - - Let cast_back : forall t, interp_flat_type var2 (lift_flat_type _ t) -> interp_flat_type var1 t - := fun t => untransfer_interp_flat_type f_base cast_backb. - - Local Notation find_Name1 := (@find_Name base_type_code1 Name Name_dec). - Local Notation find_Name_and_val1 := (@find_Name_and_val base_type_code1 Name base_type_code1_dec Name_dec). - Local Notation find_Name2 := (@find_Name base_type_code2 Name Name_dec). - Local Notation find_Name_and_val2 := (@find_Name_and_val base_type_code2 Name base_type_code2_dec Name_dec). - - Lemma find_Name_transfer_interp_flat_type {T n N} - : find_Name2 - n - (transfer_interp_flat_type - f_base (fun _ (n : Name) => n) - N) - = option_map f_base (find_Name1 (T:=T) n N). - Proof. - induction T; simpl in *; - [ | | specialize (IHT1 (fst N)); - specialize (IHT2 (snd N)) ]; - repeat first [ reflexivity - | misc_t_step - | rewriter_t_step - | progress cbv [option_map] in * - | fin_t_late_step - | break_t_step ]. - Qed. - - Local Ltac t' := - repeat first [ reflexivity - | progress subst - | progress inversion_step - | progress intros - | progress simpl in * - | rewrite cast_if_eq_refl - | break_innermost_match_step - | break_innermost_match_hyps_step - | solve [ auto ] - | specializer_t_step - | symmetry; find_Name_and_val_default_to_None_step; symmetry; - rewrite find_Name_transfer_interp_flat_type - | find_Name_and_val_default_to_None_step; - match goal with - | [ H : ?x = None |- context[?x] ] => rewrite H - end - | progress cbv [option_map] in * - | congruence ]. - - Lemma find_Name_and_val_transfer_interp_flat_type {t T} {n : Name} {N' N} {default default'} - (H' : find_Name Name_dec n N = Some t) - : find_Name_and_val1 t n N (cast_back T N') default - = option_map - (cast_backb _) - (find_Name_and_val2 - (f_base t) n - (transfer_interp_flat_type - f_base - (fun _ (n : Name) => n) N) - N' - default'). - Proof. - revert default default'; induction T; intros; - [ | | specialize (IHT1 (fst N') (fst N)); - specialize (IHT2 (snd N') (snd N)) ]; - t'. - Qed. - - Lemma find_Name_and_val_transfer_interp_flat_type_None {t T} {n : Name} {N' N} {default'} - (H' : find_Name Name_dec n N = None) - : find_Name_and_val2 - (var':=var2) - (f_base t) n - (transfer_interp_flat_type - (t:=T) - f_base - (fun _ (n : Name) => n) N) - N' - default' - = default'. - Proof. - revert default'; induction T; intros; - [ | | specialize (IHT1 (fst N') (fst N)); - specialize (IHT2 (snd N') (snd N)) ]; - t'. - Qed. -End with_context2. diff --git a/src/Compilers/Named/ContextProperties/Tactics.v b/src/Compilers/Named/ContextProperties/Tactics.v deleted file mode 100644 index b7e11a769..000000000 --- a/src/Compilers/Named/ContextProperties/Tactics.v +++ /dev/null @@ -1,101 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.HProp. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. - -Ltac fin_t_step := - solve [ reflexivity ]. -Ltac fin_t_late_step := - solve [ tauto - | congruence - | eauto - | exfalso; unfold not in *; eauto ]. -Ltac inversion_step := - first [ progress subst - | match goal with - | [ H := _ |- _ ] => subst H - | [ H : ?x = ?y |- _ ] => subst x || subst y - end - | progress inversion_option - | progress inversion_sigma - | progress inversion_prod - | progress destruct_head' and - | progress eliminate_hprop_eq - | match goal with - | [ H : ?T, H' : ?T |- _ ] => clear H' - | [ H : ?x = ?x |- _ ] => clear H - end - | progress split_and ]. -Ltac rewrite_lookupb_extendb_step := - first [ rewrite lookupb_extendb_different by congruence - | rewrite lookupb_extendb_same - | rewrite lookupb_removeb_same - | rewrite lookupb_extendb_wrong_type by assumption - | rewrite lookupb_removeb_different by congruence ]. -Ltac specializer_t_step := - match goal with - | _ => progress specialize_by_assumption - | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) - | [ H : ?T, H' : ?T |- _ ] => clear H' - | [ H : forall v, Some _ = Some v -> _ |- _ ] - => specialize (H _ eq_refl) - | [ H : forall v, Some v = Some _ -> _ |- _ ] - => specialize (H _ eq_refl) - end. -Ltac misc_t_step := - first [ progress intros - | progress simpl in * ]. -Ltac break_t_step := - first [ progress break_innermost_match_step - | progress unfold cast_if_eq in * - | match goal with - | [ H : context[match _ with _ => _ end] |- _ ] - => revert H; progress break_innermost_match_step - | [ |- _ /\ _ ] => split - | [ |- _ <-> _ ] => split - | [ |- ~ _ ] => intro - end - | progress destruct_head' ex - | progress destruct_head' or ]. -Ltac refolder_t_step := - let myfold_in_star c := - (let c' := (eval cbv [interp_flat_type] in c) in - change c' with c in * ) in - first [ match goal with - | [ var : ?base_type_code -> Type |- _ ] - => progress myfold_in_star (@interp_flat_type base_type_code var) - | [ base_type_code : Type, Name : Type |- _ ] - => progress myfold_in_star (@interp_flat_type base_type_code (fun _ => Name)) - - end ]. -Ltac rewriter_t_step := - first [ match goal with - | [ H : _ |- _ ] => rewrite H by (assumption || congruence) - | [ H : _ |- _ ] => etransitivity; [ | rewrite H by (assumption || congruence); reflexivity ] - | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : ?x = ?a :> option _, H' : ?x = ?b :> option _ |- _ ] - => assert (a = b) - by (transitivity x; [ symmetry | ]; assumption); - clear H' - | _ => progress autorewrite with ctx_db in * - end ]. -Ltac t_step := - first [ fin_t_step - | inversion_step - | rewrite_lookupb_extendb_step - | specializer_t_step - | misc_t_step - | break_t_step - | refolder_t_step - | rewriter_t_step - | fin_t_late_step ]. -Ltac t := repeat t_step. diff --git a/src/Compilers/Named/CountLets.v b/src/Compilers/Named/CountLets.v deleted file mode 100644 index 1daa8a286..000000000 --- a/src/Compilers/Named/CountLets.v +++ /dev/null @@ -1,49 +0,0 @@ -(** * Counts how many binders there are *) -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.CountLets. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.SmartMap. - -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type}. - - Local Notation flat_type := (flat_type base_type_code). - Local Notation type := (type base_type_code). - - Local Notation count_pairs := (@count_pairs base_type_code). - - Local Notation exprf := (@Named.exprf base_type_code op Name). - Local Notation expr := (@Named.expr base_type_code op Name). - - Section gen. - Context (count_type_let : flat_type -> nat). - Context (count_type_abs : flat_type -> nat). - - Fixpoint count_lets_genf {t} (e : exprf t) : nat - := match e with - | LetIn tx _ _ _ eC - => count_type_let tx + @count_lets_genf _ eC - | Op _ _ _ e => @count_lets_genf _ e - | Pair _ ex _ ey => @count_lets_genf _ ex + @count_lets_genf _ ey - | _ => 0 - end. - Definition count_lets_gen {t} (e : expr t) : nat - := match e with - | Abs tx _ _ f => count_type_abs tx + @count_lets_genf _ f - end. - End gen. - - Definition count_let_bindersf {t} (e : exprf t) : nat - := count_lets_genf count_pairs e. - Definition count_letsf {t} (e : exprf t) : nat - := count_lets_genf (fun _ => 1) e. - Definition count_let_binders {t} (e : expr t) : nat - := count_lets_gen count_pairs (fun _ => 0) e. - Definition count_lets {t} (e : expr t) : nat - := count_lets_gen (fun _ => 1) (fun _ => 0) e. - Definition count_binders {t} (e : expr t) : nat - := count_lets_gen count_pairs count_pairs e. -End language. diff --git a/src/Compilers/Named/DeadCodeElimination.v b/src/Compilers/Named/DeadCodeElimination.v deleted file mode 100644 index 340c5dd0d..000000000 --- a/src/Compilers/Named/DeadCodeElimination.v +++ /dev/null @@ -1,54 +0,0 @@ -(** * PHOAS → Named Representation of Gallina *) -Require Import Coq.PArith.BinPos Coq.Lists.List. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Compile. -Require Import Crypto.Compilers.Named.RegisterAssign. -Require Import Crypto.Compilers.Named.PositiveContext. -Require Import Crypto.Compilers.Named.EstablishLiveness. -Require Import Crypto.Compilers.CountLets. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.LetIn. - -Local Notation eta x := (fst x, snd x). - -Local Open Scope ctype_scope. -Local Open Scope nexpr_scope. -Local Open Scope expr_scope. -Section language. - Context (base_type_code : Type) - (op : flat_type base_type_code -> flat_type base_type_code -> Type) - (Name : Type) - {base_type_code_beq : base_type_code -> base_type_code -> bool} - (base_type_code_bl : forall t1 t2, base_type_code_beq t1 t2 = true -> t1 = t2) - {Context : Context Name (fun _ : base_type_code => positive)}. - - 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 nexprf := (@Named.exprf base_type_code op Name). - Local Notation nexpr := (@Named.expr base_type_code op Name). - - Local Notation PContext var := (@PositiveContext base_type_code var base_type_code_beq base_type_code_bl). - - Definition EliminateDeadCode - {t} (e : @Named.expr base_type_code op _ t) (ls : list Name) - : option (nexpr t) - := Let_In (insert_dead_names (Context:=PositiveContext_nd) None e ls) (* help vm_compute by factoring this out *) - (fun names => register_reassign (InContext:=PContext _) (ReverseContext:=Context) Pos.eqb empty empty e names). - - Definition CompileAndEliminateDeadCode - {t} (e : Expr t) (ls : list Name) - : option (nexpr t) - := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in - match e with - | Some e => EliminateDeadCode e ls - | None => None - end. -End language. - -Global Arguments EliminateDeadCode {_ _ _ _ _ _ t} e ls. -Global Arguments CompileAndEliminateDeadCode {_ _ _ _ _ _ t} e ls. diff --git a/src/Compilers/Named/DeadCodeEliminationInterp.v b/src/Compilers/Named/DeadCodeEliminationInterp.v deleted file mode 100644 index f822e6e29..000000000 --- a/src/Compilers/Named/DeadCodeEliminationInterp.v +++ /dev/null @@ -1,67 +0,0 @@ -Require Import Coq.PArith.BinPos. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.PositiveContext. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.RegisterAssignInterp. -Require Import Crypto.Compilers.Named.DeadCodeElimination. -Require Import Crypto.Util.Decidable. - -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {interp_base_type : base_type_code -> Type} - {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d} - {Name : Type} - {InContext : Context Name (fun _ : base_type_code => BinNums.positive)} - {InContextOk : ContextOk InContext} - {Name_beq : Name -> Name -> bool} - {InterpContext : Context Name interp_base_type} - {InterpContextOk : ContextOk InterpContext} - {base_type_code_beq : base_type_code -> base_type_code -> bool} - (base_type_code_bl : forall t1 t2, base_type_code_beq t1 t2 = true -> t1 = t2) - (base_type_code_lb : forall t1 t2, t1 = t2 -> base_type_code_beq t1 t2 = true) - (Name_bl : forall n1 n2, Name_beq n1 n2 = true -> n1 = n2) - (Name_lb : forall n1 n2, n1 = n2 -> Name_beq n1 n2 = true). - - Local Notation EliminateDeadCode := (@EliminateDeadCode base_type_code op Name _ base_type_code_bl InContext). - Local Notation PContext var := (@PositiveContext base_type_code var base_type_code_beq base_type_code_bl). - - Local Instance Name_dec : DecidableRel (@eq Name) - := dec_rel_of_bool_dec_rel Name_beq Name_bl Name_lb. - Local Instance base_type_code_dec : DecidableRel (@eq base_type_code) - := dec_rel_of_bool_dec_rel base_type_code_beq base_type_code_bl base_type_code_lb. - - Lemma interp_EliminateDeadCode - t e new_names - (ctxi_interp : PContext _) - (ctxr_interp : InterpContext) - eout v1 v2 x - : @EliminateDeadCode t e new_names = Some eout - -> interp (interp_op:=interp_op) (ctx:=ctxr_interp) eout x = Some v1 - -> interp (interp_op:=interp_op) (ctx:=ctxi_interp) e x = Some v2 - -> v1 = v2. - Proof using InContextOk InterpContextOk Name_bl Name_lb base_type_code_lb. - eapply @interp_register_reassign; - first [ assumption - | apply @PositiveContextOk; assumption - | apply Peqb_true_eq - | apply Pos.eqb_eq - | exact _ - | intros *; rewrite !lookupb_empty by (try apply @PositiveContextOk; assumption); - congruence ]. - Qed. - - Lemma InterpEliminateDeadCode - t e new_names - eout - v1 v2 x - : @EliminateDeadCode t e new_names = Some eout - -> Interp (Context:=InterpContext) (interp_op:=interp_op) eout x = Some v1 - -> Interp (Context:=PContext _) (interp_op:=interp_op) e x = Some v2 - -> v1 = v2. - Proof using InContextOk InterpContextOk Name_bl Name_lb base_type_code_lb. - apply interp_EliminateDeadCode. - Qed. -End language. diff --git a/src/Compilers/Named/EstablishLiveness.v b/src/Compilers/Named/EstablishLiveness.v deleted file mode 100644 index 706327918..000000000 --- a/src/Compilers/Named/EstablishLiveness.v +++ /dev/null @@ -1,105 +0,0 @@ -(** * Compute a list of liveness values for each binding *) -Require Import Coq.Lists.List. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.CountLets. -Require Import Crypto.Util.ListUtil. - -Local Notation eta x := (fst x, snd x). - -Local Open Scope ctype_scope. -Delimit Scope nexpr_scope with nexpr. - -Inductive liveness := live | dead. -Fixpoint merge_liveness (ls1 ls2 : list liveness) := - match ls1, ls2 with - | cons x xs, cons y ys - => cons match x, y with - | live, _ - | _, live - => live - | dead, dead - => dead - end - (@merge_liveness xs ys) - | nil, ls - | ls, nil - => ls - end. - -Section language. - Context (base_type_code : Type) - (op : flat_type base_type_code -> flat_type base_type_code -> Type). - - Local Notation flat_type := (flat_type base_type_code). - Local Notation type := (type base_type_code). - Local Notation exprf := (@exprf base_type_code op). - Local Notation expr := (@expr base_type_code op). - - Section internal. - Context (Name : Type) - (OutName : Type) - {Context : Context Name (fun _ : base_type_code => list liveness)}. - - Definition compute_livenessf_step - (compute_livenessf : forall (ctx : Context) {t} (e : exprf Name t) (prefix : list liveness), list liveness) - (ctx : Context) - {t} (e : exprf Name t) (prefix : list liveness) - : list liveness - := match e with - | TT => prefix - | Var t' name => match lookup (Tbase t') ctx name with - | Some ls => ls - | _ => nil - end - | Op _ _ op args - => @compute_livenessf ctx _ args prefix - | LetIn tx n ex _ eC - => let lx := @compute_livenessf ctx _ ex prefix in - let lx := merge_liveness lx (prefix ++ repeat live (count_pairs tx)) in - let ctx := extend ctx n (SmartValf _ (fun _ => lx) tx) in - @compute_livenessf ctx _ eC (prefix ++ repeat dead (count_pairs tx)) - | Pair _ ex _ ey - => merge_liveness (@compute_livenessf ctx _ ex prefix) - (@compute_livenessf ctx _ ey prefix) - end. - - Fixpoint compute_livenessf ctx {t} e prefix - := @compute_livenessf_step (@compute_livenessf) ctx t e prefix. - - Definition compute_liveness (ctx : Context) - {t} (e : expr Name t) (prefix : list liveness) - : list liveness - := match e with - | Abs src _ n f - => let prefix := prefix ++ repeat live (count_pairs src) in - let ctx := extend (t:=src) ctx n (SmartValf _ (fun _ => prefix) src) in - compute_livenessf ctx f prefix - end. - - Section insert_dead. - Context (default_out : option OutName). - - Fixpoint insert_dead_names_gen (ls : list liveness) (lsn : list OutName) - : list (option OutName) - := match ls with - | nil => nil - | cons live xs - => match lsn with - | cons n lsn' => Some n :: @insert_dead_names_gen xs lsn' - | nil => default_out :: @insert_dead_names_gen xs nil - end - | cons dead xs - => None :: @insert_dead_names_gen xs lsn - end. - Definition insert_dead_names {t} (e : expr Name t) - := insert_dead_names_gen (compute_liveness empty e nil). - End insert_dead. - End internal. -End language. - -Global Arguments compute_livenessf {_ _ _ _} ctx {t} e prefix. -Global Arguments compute_liveness {_ _ _ _} ctx {t} e prefix. -Global Arguments insert_dead_names {_ _ _ _ _} default_out {t} e lsn. diff --git a/src/Compilers/Named/ExprInversion.v b/src/Compilers/Named/ExprInversion.v deleted file mode 100644 index 783341f26..000000000 --- a/src/Compilers/Named/ExprInversion.v +++ /dev/null @@ -1,21 +0,0 @@ -Require Import Crypto.Compilers.TypeInversion. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. - -Module Export Named. - Ltac invert_one_expr e := - preinvert_one_type e; - intros ? e; - destruct e; - try exact I. - - Ltac invert_expr_step := - match goal with - | [ e : Named.exprf _ _ _ (Tbase _) |- _ ] => invert_one_expr e - | [ e : Named.exprf _ _ _ (Prod _ _) |- _ ] => invert_one_expr e - | [ e : Named.exprf _ _ _ Unit |- _ ] => invert_one_expr e - | [ e : Named.expr _ _ _ (Arrow _ _) |- _ ] => invert_one_expr e - end. - - Ltac invert_expr := repeat invert_expr_step. -End Named. diff --git a/src/Compilers/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v deleted file mode 100644 index b69d78d09..000000000 --- a/src/Compilers/Named/FMapContext.v +++ /dev/null @@ -1,70 +0,0 @@ -Require Import Coq.Bool.Sumbool. -Require Import Coq.FSets.FMapInterface. -Require Import Coq.FSets.FMapFacts. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Equality. - -Module FMapContextFun (E : DecidableType) (W : WSfun E). - Module Import Properties := WProperties_fun E W. - Import F. - Section ctx. - Context (E_eq_l : forall x y, E.eq x y -> x = y) - base_type_code (var : base_type_code -> Type) - (base_type_code_beq : base_type_code -> base_type_code -> bool) - (base_type_code_bl_transparent : forall x y, base_type_code_beq x y = true -> x = y) - (base_type_code_lb : forall x y, x = y -> base_type_code_beq x y = true). - - Definition var_cast {a b} (x : var a) : option (var b) - := match Sumbool.sumbool_of_bool (base_type_code_beq a b), Sumbool.sumbool_of_bool (base_type_code_beq b b) with - | left pf, left pf' => match eq_trans (base_type_code_bl_transparent _ _ pf) (eq_sym (base_type_code_bl_transparent _ _ pf')) with - | eq_refl => Some x - end - | right _, _ | _, right _ => None - end. - Definition FMapContext : @Context base_type_code W.key var - := {| ContextT := W.t { t : _ & var t }; - lookupb t ctx n - := match W.find n ctx with - | Some (existT t' v) - => var_cast v - | None => None - end; - extendb t ctx n v - := W.add n (existT _ t v) ctx; - removeb t ctx n - := W.remove n ctx; - empty := W.empty _ |}. - Lemma FMapContextOk : @ContextOk base_type_code W.key var FMapContext. - Proof using E_eq_l base_type_code_lb. - split; - repeat first [ reflexivity - | progress simpl in * - | progress intros - | rewrite add_eq_o by reflexivity - | progress rewrite ?add_neq_o, ?remove_neq_o, ?remove_eq_o in * by intuition - | progress rewrite empty_o in * - | progress unfold var_cast - | progress break_innermost_match_step - | rewrite concat_pV - | congruence - | rewrite base_type_code_lb in * by reflexivity - | break_innermost_match_hyps_step - | progress unfold var_cast in * ]. - Qed. - End ctx. - - Section ctx_nd. - Context {base_type_code var : Type}. - - Definition FMapContext_nd : @Context base_type_code W.key (fun _ => var) - := {| ContextT := W.t var; - lookupb t ctx n := W.find n ctx; - extendb t ctx n v := W.add n v ctx; - removeb t ctx n := W.remove n ctx; - empty := W.empty _ |}. - End ctx_nd. -End FMapContextFun. - -Module FMapContext (W : WS) := FMapContextFun W.E W. diff --git a/src/Compilers/Named/GetNames.v b/src/Compilers/Named/GetNames.v deleted file mode 100644 index ce26b1bca..000000000 --- a/src/Compilers/Named/GetNames.v +++ /dev/null @@ -1,38 +0,0 @@ -Require Import Coq.Lists.List. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. - -Local Open Scope list_scope. - -Section language. - Context {base_type_code} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type}. - - Local Notation exprf := (@exprf base_type_code op Name). - Local Notation expr := (@expr base_type_code op Name). - - Fixpoint get_names_of_type {t} : interp_flat_type (fun _ : base_type_code => Name) t -> list Name - := match t with - | Tbase T => fun n => n::nil - | Unit => fun _ => nil - | Prod A B => fun ab : interp_flat_type _ A * interp_flat_type _ B - => @get_names_of_type _ (fst ab) ++ @get_names_of_type _ (snd ab) - end. - - Fixpoint get_namesf {t} (e : exprf t) : list Name - := match e with - | TT => nil - | Var _ x => x::nil - | Op _ _ opc args => @get_namesf _ args - | LetIn tx nx ex tC eC - => get_names_of_type nx ++ (* @get_namesf _ ex ++ *) @get_namesf _ eC - | Pair _ ex _ ey - => @get_namesf _ ex ++ @get_namesf _ ey - end. - - Fixpoint get_names {t} (e : expr t) : list Name - := match e with - | Abs _ _ n f => get_names_of_type n ++ get_namesf f - end. -End language. diff --git a/src/Compilers/Named/IdContext.v b/src/Compilers/Named/IdContext.v deleted file mode 100644 index d82740cb4..000000000 --- a/src/Compilers/Named/IdContext.v +++ /dev/null @@ -1,27 +0,0 @@ -Require Import Coq.Lists.List. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. - -Section language. - Context {base_type_code Name} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (Context : @Context base_type_code Name (fun _ => Name)). - - Fixpoint collect_binders {t} (e : Named.exprf base_type_code op Name t) - : list { t : flat_type base_type_code & interp_flat_type (fun _ => Name) t } - := match e with - | TT => nil - | Var t n => (existT _ (Tbase t) n) :: nil - | Op t1 tR opc args => @collect_binders _ args - | LetIn tx n ex tC eC - => (existT _ tx n) :: @collect_binders tx ex ++ @collect_binders tC eC - | Pair tx ex ty ey - => @collect_binders tx ex ++ @collect_binders ty ey - end%list. - Definition idcontext {t} (e : Named.exprf base_type_code op Name t) : Context - := List.fold_right - (fun v ctx => extend ctx (projT2 v) (projT2 v)) - empty - (collect_binders e). -End language. diff --git a/src/Compilers/Named/InterpSideConditions.v b/src/Compilers/Named/InterpSideConditions.v deleted file mode 100644 index bd90eac23..000000000 --- a/src/Compilers/Named/InterpSideConditions.v +++ /dev/null @@ -1,54 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Notations. - -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). - - 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. diff --git a/src/Compilers/Named/InterpSideConditionsInterp.v b/src/Compilers/Named/InterpSideConditionsInterp.v deleted file mode 100644 index 72bb9c9e0..000000000 --- a/src/Compilers/Named/InterpSideConditionsInterp.v +++ /dev/null @@ -1,45 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.InterpSideConditions. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Option. - -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). - - Lemma snd_interpf_side_conditions_gen_eq {t} {ctx : Context} {e} - : interpf (t:=t) (ctx:=ctx) (interp_op:=interp_op) e - = option_map (@snd _ _) (interpf_side_conditions_gen interp_op interped_op_side_conditions ctx e). - Proof. - revert ctx; induction e; intros; - repeat first [ reflexivity - | progress subst - | progress inversion_option - | progress unfold option_map, LetIn.Let_In in * - | break_innermost_match_step - | break_innermost_match_hyps_step - | progress simpl in * - | match goal with - | [ H : forall ctx, interpf ?e = _, H' : context[interpf ?e] |- _ ] - => rewrite H in H' - | [ H : forall ctx, interpf ?e = _ |- context[interpf ?e] ] - => rewrite H - end ]. - Qed. - Lemma snd_interpf_side_conditions_gen_Some {t} {ctx : Context} {e v} - : interpf (t:=t) (ctx:=ctx) (interp_op:=interp_op) e = Some v - <-> option_map (@snd _ _) (interpf_side_conditions_gen interp_op interped_op_side_conditions ctx e) = Some v. - Proof. rewrite snd_interpf_side_conditions_gen_eq; reflexivity. Qed. -End language. diff --git a/src/Compilers/Named/InterpretToPHOAS.v b/src/Compilers/Named/InterpretToPHOAS.v deleted file mode 100644 index 4e74fc59a..000000000 --- a/src/Compilers/Named/InterpretToPHOAS.v +++ /dev/null @@ -1,65 +0,0 @@ -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Wf. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Util.PointedProp. - -Local Notation eta_and x := (conj (let (a, b) := x in a) (let (a, b) := x in b)). - -Module Export Named. - Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type}. - Section with_var. - Context {var : base_type_code -> Type} - {Context : Context Name var} - (failb : forall t, @Syntax.exprf base_type_code op var (Tbase t)). - - Local Notation failf t (* : @Syntax.exprf base_type_code op var t*) - := (SmartPairf (SmartValf _ failb t)). - - Fixpoint interpf_to_phoas - (ctx : Context) - {t} (e : @Named.exprf base_type_code op Name t) - {struct e} - : @Syntax.exprf base_type_code op var t - := match e in Named.exprf _ _ _ t return @Syntax.exprf base_type_code op var t with - | Named.Var t' x - => match lookupb t' ctx x with - | Some v => Var v - | None => failf _ - end - | Named.TT => TT - | Named.Pair tx ex ty ey - => Pair (@interpf_to_phoas ctx tx ex) (@interpf_to_phoas ctx ty ey) - | Named.Op _ _ opc args - => Op opc (@interpf_to_phoas ctx _ args) - | Named.LetIn _ n ex _ eC - => LetIn (@interpf_to_phoas ctx _ ex) - (fun v - => @interpf_to_phoas (extend ctx n v) _ eC) - end. - - Definition interp_to_phoas - (ctx : Context) - {t} (e : @Named.expr base_type_code op Name t) - : @Syntax.expr base_type_code op var (domain t -> codomain t) - := Abs (fun v => interpf_to_phoas (extend ctx (Abs_name e) v) (invert_Abs e)). - End with_var. - - Section all. - Context {Context : forall var, @Context base_type_code Name var} - (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)). - Definition InterpToPHOAS_gen - (ctx : forall var, Context var) - {t} (e : @Named.expr base_type_code op Name t) - : @Syntax.Expr base_type_code op (domain t -> codomain t) - := fun var => interp_to_phoas (failb var) (ctx var) e. - - Definition InterpToPHOAS {t} e - := @InterpToPHOAS_gen (fun var => empty) t e. - End all. - End language. -End Named. diff --git a/src/Compilers/Named/InterpretToPHOASInterp.v b/src/Compilers/Named/InterpretToPHOASInterp.v deleted file mode 100644 index 7fe50c994..000000000 --- a/src/Compilers/Named/InterpretToPHOASInterp.v +++ /dev/null @@ -1,89 +0,0 @@ -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Wf. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.InterpretToPHOAS. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. - -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type} - {base_type_code_dec : DecidableRel (@eq base_type_code)} - {Name_dec : DecidableRel (@eq Name)} - {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}. - Section with_context. - Context {Context : Context Name interp_base_type} - {ContextOk : ContextOk Context} - (failb : forall t, @Syntax.exprf base_type_code op interp_base_type (Tbase t)). - - Lemma interpf_interpf_to_phoas - (ctx : Context) - {t} (e : @Named.exprf base_type_code op Name t) - (Hwf : prop_of_option (Named.wff ctx e)) - : Named.interpf (interp_op:=interp_op) (ctx:=ctx) e - = Some (Syntax.interpf interp_op (interpf_to_phoas failb ctx e)). - Proof using Type. - revert dependent ctx; induction e; - repeat first [ progress intros - | progress subst - | progress inversion_option - | progress destruct_head' and - | progress break_innermost_match_step - | progress unfold option_map, LetIn.Let_In in * - | apply (f_equal (@Some _)) - | apply (f_equal (@interp_op _ _ _)) - | progress simpl in * - | progress autorewrite with push_prop_of_option in * - | solve [ eauto | congruence | tauto ] - | match goal with - | [ H : forall ctx Hwf', Named.interpf ?e = Some _, Hwf : prop_of_option (Named.wff _ ?e) |- _ ] - => specialize (H _ Hwf) - | [ H : forall ctx Hwf, Named.interpf ?e = Some _ |- Named.interpf ?e = Some _ ] - => rewrite H by auto - end ]. - Qed. - - Lemma interp_interp_to_phoas - (ctx : Context) - {t} (e : @Named.expr base_type_code op Name t) - (Hwf : Named.wf ctx e) - v - : Named.interp (interp_op:=interp_op) (ctx:=ctx) e v - = Some (Syntax.interp interp_op (interp_to_phoas failb ctx e) v). - Proof using Type. - unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas; auto. - Qed. - End with_context. - - Section all. - Context {Context : forall var, @Context base_type_code Name var} - {ContextOk : forall var, ContextOk (Context var)} - (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)). - - Lemma Interp_InterpToPHOAS_gen - {ctx : forall var, Context var} - {t} (e : @Named.expr base_type_code op Name t) - (Hwf : forall var, Named.wf (ctx var) e) - v - : Named.interp (interp_op:=interp_op) (ctx:=ctx _) e v - = Some (Interp interp_op (InterpToPHOAS_gen failb ctx e) v). - Proof using Type. apply interp_interp_to_phoas; auto. Qed. - - Lemma Interp_InterpToPHOAS - {t} (e : @Named.expr base_type_code op Name t) - (Hwf : Named.Wf Context e) - v - : Named.Interp (Context:=Context _) (interp_op:=interp_op) e v - = Some (Interp interp_op (InterpToPHOAS (Context:=Context) failb e) v). - Proof using Type. apply interp_interp_to_phoas; auto. Qed. - End all. -End language. diff --git a/src/Compilers/Named/InterpretToPHOASWf.v b/src/Compilers/Named/InterpretToPHOASWf.v deleted file mode 100644 index d2b3f18d3..000000000 --- a/src/Compilers/Named/InterpretToPHOASWf.v +++ /dev/null @@ -1,139 +0,0 @@ -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Wf. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.ContextProperties.SmartMap. -Require Import Crypto.Compilers.Named.InterpretToPHOAS. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. - -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type} - {base_type_code_dec : DecidableRel (@eq base_type_code)} - {Name_dec : DecidableRel (@eq Name)}. - Section with_var. - Context {var1 var2 : base_type_code -> Type} - {Context1 : Context Name var1} - {Context2 : Context Name var2} - {Context1Ok : ContextOk Context1} - {Context2Ok : ContextOk Context2} - (failb1 : forall t, @Syntax.exprf base_type_code op var1 (Tbase t)) - (failb2 : forall t, @Syntax.exprf base_type_code op var2 (Tbase t)). - - Local Ltac t_step := - first [ progress intros - | progress unfold dec in * - | reflexivity - | progress subst - | progress inversion_option - | erewrite lookupb_extend by assumption - | rewrite <- !find_Name_and_val_None_iff - | progress break_innermost_match_step - | progress break_match_hyps - | solve [ eauto using find_Name_and_val_flatten_binding_list ] - | congruence - | tauto - | match goal with - | [ H : lookupb (extend _ _ _) _ = _ |- _ ] - => erewrite (lookupb_extend _ _ _) in H by assumption - | [ H : context[List.In _ (_ ++ _)] |- _ ] - => setoid_rewrite List.in_app_iff in H - | [ |- context[List.In _ (_ ++ _)] ] - => rewrite List.in_app_iff - | [ |- 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 : 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)) in H - | [ H : forall n t, lookupb _ n = None <-> lookupb _ n = None |- context[lookupb _ _ = None] ] - => rewrite H - | [ H : forall n t, lookupb _ n = None |- context[lookupb _ _ = None] ] - => rewrite H - end ]. - Local Ltac t := repeat t_step. - - Lemma wff_interpf_to_phoas - (ctx1 : Context1) (ctx2 : Context2) - {t} (e : @Named.exprf base_type_code op Name t) - (Hwf1 : prop_of_option (Named.wff ctx1 e)) - (Hwf2 : prop_of_option (Named.wff ctx2 e)) - G - (HG : forall n t v1 v2, - lookupb t ctx1 n = Some v1 - -> lookupb t ctx2 n = Some v2 - -> List.In (existT _ t (v1, v2)%core) G) - (Hctx1_ctx2 : forall n t, - lookupb t ctx1 n = None <-> lookupb t ctx2 n = None) - : wff G (interpf_to_phoas failb1 ctx1 e) (interpf_to_phoas failb2 ctx2 e). - Proof using Context1Ok Context2Ok Name_dec base_type_code_dec. - revert dependent G; revert dependent ctx1; revert dependent ctx2; induction e; - repeat first [ progress intros - | progress destruct_head' and - | progress break_innermost_match_step - | progress simpl in * - | progress autorewrite with push_prop_of_option in * - | solve [ eauto | tauto ] - | match goal with - | [ |- wff _ _ _ ] => constructor - end ]. - match goal with H : _ |- _ => eapply H end; t. - Qed. - - Lemma wf_interp_to_phoas_gen - (ctx1 : Context1) (ctx2 : Context2) - {t} (e : @Named.expr base_type_code op Name t) - (Hwf1 : Named.wf ctx1 e) - (Hwf2 : Named.wf ctx2 e) - (Hctx1 : forall n t, lookupb t ctx1 n = None) - (Hctx2 : forall n t, lookupb t ctx2 n = None) - : wf (interp_to_phoas failb1 ctx1 e) (interp_to_phoas failb2 ctx2 e). - Proof using Context1Ok Context2Ok Name_dec base_type_code_dec. - constructor; intros. - apply wff_interpf_to_phoas; t. - Qed. - - Lemma wf_interp_to_phoas - {t} (e : @Named.expr base_type_code op Name t) - (Hwf1 : Named.wf (Context:=Context1) empty e) - (Hwf2 : Named.wf (Context:=Context2) empty e) - : wf (interp_to_phoas (Context:=Context1) failb1 empty e) (interp_to_phoas (Context:=Context2) failb2 empty e). - Proof using Context1Ok Context2Ok Name_dec base_type_code_dec. - apply wf_interp_to_phoas_gen; auto using lookupb_empty. - Qed. - End with_var. - - Section all. - Context {Context : forall var, @Context base_type_code Name var} - {ContextOk : forall var, ContextOk (Context var)} - (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)). - - Lemma Wf_InterpToPHOAS_gen - {ctx : forall var, Context var} - {t} (e : @Named.expr base_type_code op Name t) - (Hctx : forall var n t, lookupb t (ctx var) n = None) - (Hwf : forall var, Named.wf (ctx var) e) - : Wf (InterpToPHOAS_gen failb ctx e). - Proof using ContextOk Name_dec base_type_code_dec. - intros ??; apply wf_interp_to_phoas_gen; auto. - Qed. - - Lemma Wf_InterpToPHOAS - {t} (e : @Named.expr base_type_code op Name t) - (Hwf : Named.Wf Context e) - : Wf (InterpToPHOAS (Context:=Context) failb e). - Proof using ContextOk Name_dec base_type_code_dec. - intros ??; apply wf_interp_to_phoas; auto. - Qed. - End all. -End language. - -Hint Resolve Wf_InterpToPHOAS : wf. diff --git a/src/Compilers/Named/MapCast.v b/src/Compilers/Named/MapCast.v deleted file mode 100644 index fddee84fa..000000000 --- a/src/Compilers/Named/MapCast.v +++ /dev/null @@ -1,72 +0,0 @@ -Require Import Coq.Bool.Sumbool. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. - -Local Open Scope nexpr_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type} - {interp_base_type_bounds : base_type_code -> Type} - (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst) - (pick_typeb : forall t, interp_base_type_bounds t -> base_type_code). - Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v). - Context (cast_op : forall t tR (opc : op t tR) args_bs, - op (pick_type args_bs) (pick_type (interp_op_bounds t tR opc args_bs))) - {BoundsContext : Context Name interp_base_type_bounds}. - - Fixpoint mapf_cast - (ctx : BoundsContext) - {t} (e : exprf base_type_code op Name t) - {struct e} - : option { bounds : interp_flat_type interp_base_type_bounds t - & exprf base_type_code op Name (pick_type bounds) } - := match e in exprf _ _ _ t return option { bounds : interp_flat_type interp_base_type_bounds t - & exprf base_type_code op Name (pick_type bounds) } with - | TT => Some (existT _ tt TT) - | Pair tx ex ty ey - => match @mapf_cast ctx _ ex, @mapf_cast ctx _ ey with - | Some (existT x_bs xv), Some (existT y_bs yv) - => Some (existT _ (x_bs, y_bs)%core (Pair xv yv)) - | None, _ | _, None => None - end - | Var t x - => option_map - (fun bounds => existT _ bounds (Var x)) - (lookupb (t:=t) ctx x) - | LetIn tx n ex tC eC - => match @mapf_cast ctx _ ex with - | Some (existT x_bounds ex') - => option_map - (fun eC' => let 'existT Cx_bounds C_expr := eC' in - existT _ Cx_bounds (LetIn (pick_type x_bounds) - (SmartFlatTypeMapInterp2 (t:=tx) (fun _ _ (n : Name) => n) x_bounds n) ex' C_expr)) - (@mapf_cast (extend (t:=tx) ctx n x_bounds) _ eC) - | None => None - end - | Op t tR opc args - => option_map - (fun args' - => let 'existT args_bounds argsv := args' in - existT _ - (interp_op_bounds _ _ _ args_bounds) - (Op (cast_op t tR opc args_bounds) argsv)) - (@mapf_cast ctx _ args) - end. - - Definition map_cast - (ctx : BoundsContext) - {t} (e : expr base_type_code op Name t) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - : option { output_bounds : interp_flat_type interp_base_type_bounds (codomain t) - & expr base_type_code op Name (Arrow (pick_type input_bounds) (pick_type output_bounds)) } - := option_map - (fun v => existT - _ - (projT1 v) - (Abs (SmartFlatTypeMapInterp2 (fun _ _ (n' : Name) => n') input_bounds (Abs_name e)) - (projT2 v))) - (mapf_cast (extend ctx (Abs_name e) input_bounds) (invert_Abs e)). -End language. diff --git a/src/Compilers/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v deleted file mode 100644 index c38eadd9c..000000000 --- a/src/Compilers/Named/MapCastInterp.v +++ /dev/null @@ -1,290 +0,0 @@ -Require Import Coq.Bool.Sumbool. -Require Import Coq.Logic.Eqdep_dec. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.ContextProperties.SmartMap. -Require Import Crypto.Compilers.Named.InterpSideConditions. -Require Import Crypto.Compilers.Named.InterpSideConditionsInterp. -Require Import Crypto.Compilers.Named.MapCast. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.RewriteHyp. - -Local Open Scope nexpr_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type} - {interp_base_type_bounds : base_type_code -> Type} - (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst) - (pick_typeb : forall t, interp_base_type_bounds t -> base_type_code). - Local Notation pick_type t v := (SmartFlatTypeMap pick_typeb (t:=t) v). - Context (cast_op : forall t tR (opc : op t tR) args_bs, - op (pick_type _ args_bs) (pick_type _ (interp_op_bounds t tR opc args_bs))) - {BoundsContext : Context Name interp_base_type_bounds} - (BoundsContextOk : ContextOk BoundsContext) - {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) - (interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop) - (cast_backb: forall t b, interp_base_type (pick_typeb t b) -> interp_base_type t). - Let cast_back : forall t b, interp_flat_type interp_base_type (@pick_type t b) -> interp_flat_type interp_base_type t - := fun t b => SmartFlatTypeMapUnInterp cast_backb. - Context {Context : Context Name interp_base_type} - (ContextOk : ContextOk Context) - (inboundsb : forall t, interp_base_type_bounds t -> interp_base_type t -> Prop). - Let inbounds : forall t, interp_flat_type interp_base_type_bounds t -> interp_flat_type interp_base_type t -> Prop - := fun t => interp_flat_type_rel_pointwise inboundsb (t:=t). - Context (interp_op_bounds_correct: - forall t tR opc bs - (v : interp_flat_type interp_base_type t) - (H : inbounds t bs v) - (Hside : to_prop (interped_op_side_conditions _ _ opc v)), - inbounds tR (interp_op_bounds t tR opc bs) (interp_op t tR opc v)) - (pull_cast_back: - forall t tR opc bs - (v : interp_flat_type interp_base_type (pick_type t bs)) - (H : inbounds t bs (cast_back t bs v)) - (Hside : to_prop (interped_op_side_conditions _ _ opc (cast_back t bs v))), - interp_op t tR opc (cast_back t bs v) - = - cast_back _ _ (interp_op _ _ (cast_op _ _ opc bs) v)) - (base_type_dec : DecidableRel (@eq base_type_code)) - (Name_dec : DecidableRel (@eq Name)). - - Local Notation mapf_cast := (@mapf_cast _ op Name _ interp_op_bounds pick_typeb cast_op BoundsContext). - Local Notation map_cast := (@map_cast _ op Name _ interp_op_bounds pick_typeb cast_op BoundsContext). - - Local Ltac handle_options_step := - match goal with - | _ => progress inversion_option - | [ H : ?x = Some _ |- context[?x] ] => rewrite H - | [ H : ?x = None |- context[?x] ] => rewrite H - | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : Some _ <> None \/ _ |- _ ] => clear H - | [ H : Some ?x <> Some ?y |- _ ] => assert (x <> y) by congruence; clear H - | [ H : None <> Some _ |- _ ] => clear H - | [ H : Some _ <> None |- _ ] => clear H - | [ H : ?x <> ?x \/ _ |- _ ] => destruct H; [ exfalso; apply H; reflexivity | ] - | [ H : _ \/ None = Some _ |- _ ] => destruct H; [ | exfalso; clear -H; congruence ] - | [ H : _ \/ Some _ = None |- _ ] => destruct H; [ | exfalso; clear -H; congruence ] - | [ H : ?x = Some ?y, H' : ?x = Some ?y' |- _ ] - => assert (y = y') by congruence; (subst y' || subst y) - | _ => progress simpl @option_map - end. - - Local Ltac handle_lookupb_step := - let do_eq_dec dec t t' := - first [ constr_eq t t'; fail 1 - | lazymatch goal with - | [ H : t = t' |- _ ] => fail 1 - | [ H : t <> t' |- _ ] => fail 1 - | [ H : t = t' -> False |- _ ] => fail 1 - | _ => destruct (dec t t') - end ] in - let do_type_dec := do_eq_dec base_type_dec in - match goal with - | _ => progress unfold dec in * - | _ => handle_options_step - (* preprocess *) - | [ H : context[lookupb (extend _ _ _) _] |- _ ] - => first [ rewrite (lookupb_extend base_type_dec Name_dec) in H by assumption - | setoid_rewrite (lookupb_extend base_type_dec Name_dec) in H; [ | assumption.. ] ] - | [ |- context[lookupb (extend _ _ _) _] ] - => first [ rewrite (fun C => lookupb_extend C base_type_dec Name_dec) by assumption - | setoid_rewrite (lookupb_extend base_type_dec Name_dec); [ | assumption.. ] ] - | _ => progress subst - (* handle multiple hypotheses *) - | [ H : find_Name _ ?n ?N = Some ?t', H'' : context[find_Name_and_val _ _ ?t ?n ?N ?x ?default] |- _ ] - => do_type_dec t t' - (* clear the default value *) - | [ H : context[find_Name_and_val ?tdec ?ndec ?t ?n (T:=?T) ?N ?V ?default] |- _ ] - => lazymatch default with None => fail | _ => idtac end; - rewrite find_Name_and_val_split in H - (* generic handlers *) - | [ H : find_Name _ ?n ?N = Some ?t', H' : ?t <> ?t', H'' : context[find_Name_and_val _ _ ?t ?n ?N ?x ?default] |- _ ] - => erewrite find_Name_and_val_wrong_type in H'' by eassumption - | [ H : context[find_Name _ _ (SmartFlatTypeMapInterp2 _ _ _)] |- _ ] - => rewrite find_Name_SmartFlatTypeMapInterp2 with (base_type_code_dec:=base_type_dec) in H - | [ H : find_Name_and_val _ _ _ _ _ _ _ = None |- _ ] - => apply find_Name_and_val_None_iff in H - (* destructers *) - | [ |- context[find_Name_and_val ?tdec ?ndec ?t ?n ?N ?V ?default] ] - => destruct (find_Name_and_val tdec ndec t n N V default) eqn:? - | [ H : context[match find_Name_and_val ?tdec ?ndec ?t ?n ?N ?V ?default with _ => _ end] |- _ ] - => destruct (find_Name_and_val tdec ndec t n N V default) eqn:? - | [ H : context[match find_Name ?ndec ?n ?N with _ => _ end] |- _ ] - => destruct (find_Name ndec n N) eqn:? - | [ H : context[match base_type_dec ?x ?y with _ => _ end] |- _ ] - => destruct (base_type_dec x y) - | [ H : context[match Name_dec ?x ?y with _ => _ end] |- _ ] - => destruct (Name_dec x y) - end. - - Local Ltac handle_exists_in_goal := - lazymatch goal with - | [ |- exists v, Some ?k = Some v /\ @?B v ] - => exists k; split; [ reflexivity | ] - | [ |- (exists v, None = Some v /\ @?B v) ] - => exfalso - | [ |- ?A /\ (exists v, Some ?k = Some v /\ @?B v) ] - => cut (A /\ B k); [ clear; solve [ intuition eauto ] | cbv beta ] - | [ |- ?A /\ (exists v, None = Some v /\ @?B v) ] - => exfalso - end. - Local Ltac handle_bounds_side_conditions_step := - match goal with - | [ H : interpf ?e = Some ?v, H' : interpf_side_conditions_gen _ _ _ ?e = Some (_, ?v')%core |- _ ] - => first [ constr_eq v v'; fail 1 - | assert (Some v = Some v') - by (erewrite <- H, snd_interpf_side_conditions_gen_eq, H'; reflexivity); - inversion_option; (subst v || subst v') ] - end. - Local Ltac fin_inbounds_cast_back_t_step := - match goal with - | [ |- inboundsb _ _ _ /\ _ ] - => split; [ eapply interp_flat_type_rel_pointwise__find_Name_and_val; eassumption | ] - | [ |- cast_backb _ _ _ = _ ] - => eapply find_Name_and_val__SmartFlatTypeMapInterp2__SmartFlatTypeMapUnInterp__Some_Some; [ | eassumption.. ] - end. - Local Ltac specializer_t_step := - match goal with - | [ H : ?T, H' : ?T |- _ ] => clear H - | [ H : forall x, Some _ = Some x -> _ |- _ ] => specialize (H _ eq_refl) - | [ H : ?x = Some _, IH : forall a b, ?x = Some _ -> _ |- _ ] - => specialize (IH _ _ H) - | [ H : ?x = Some _, IH : forall a, ?x = Some _ -> _ |- _ ] - => specialize (IH _ H) - | [ H : forall t n v, lookupb ?ctx n = _ -> _, H' : lookupb ?ctx ?n' = _ |- _ ] - => specialize (H _ _ _ H') - | _ => progress specialize_by auto - end. - - Local Ltac break_t_step := - first [ progress destruct_head'_ex - | progress destruct_head'_and ]. - - Local Ltac t_step := - first [ progress intros - | break_t_step - | handle_lookupb_step - | handle_exists_in_goal - | solve [ auto ] - | specializer_t_step - | fin_inbounds_cast_back_t_step - | handle_options_step - | handle_bounds_side_conditions_step ]. - Local Ltac t := repeat t_step. - - Local Ltac do_specialize_IHe := - repeat match goal with - | [ IH : context[interpf ?e], H' : interpf (ctx:=?ctx) ?e = _ |- _ ] - => let check_tac _ := (rewrite H' in IH) in - first [ specialize (IH ctx); check_tac () - | specialize (fun a => IH a ctx); check_tac () - | specialize (fun a b => IH a b ctx); check_tac () ] - | [ IH : context[mapf_cast _ ?e], H' : mapf_cast ?ctx ?e = _ |- _ ] - => let check_tac _ := (rewrite H' in IH) in - first [ specialize (IH ctx); check_tac () - | specialize (fun a => IH a ctx); check_tac () - | specialize (fun a b => IH a b ctx); check_tac () ] - | [ H : forall x y z, Some _ = Some _ -> _ |- _ ] - => first [ specialize (H _ _ _ eq_refl) - | specialize (fun x => H x _ _ eq_refl) ] - | [ H : forall x y, Some _ = Some _ -> _ |- _ ] - => first [ specialize (H _ _ eq_refl) - | specialize (fun x => H x _ eq_refl) ] - | _ => progress specialize_by_assumption - end. - - Lemma mapf_cast_correct - {t} (e:exprf base_type_code op Name t) - : forall - (oldValues:Context) - (newValues:Context) - (varBounds:BoundsContext) - {b} e' (He':mapf_cast varBounds e = Some (existT _ b e')) - (Hctx:forall {t} n v, - lookupb (t:=t) oldValues n = Some v - -> exists b, lookupb (t:=t) varBounds n = Some b - /\ @inboundsb _ b v - /\ exists v', lookupb (t:=pick_typeb t b) newValues n = Some v' - /\ cast_backb t b v' = v) - r (Hr:interpf (interp_op:=interp_op) (ctx:=oldValues) e = Some r) - r' (Hr':interpf (interp_op:=interp_op) (ctx:=newValues) e' = Some r') - (Hside : prop_of_option (interpf_side_conditions interp_op interped_op_side_conditions oldValues e)) - , interpf (interp_op:=interp_op_bounds) (ctx:=varBounds) e = Some b - /\ @inbounds _ b r /\ cast_back _ _ r' = r. - Proof using Type*. - induction e; simpl interpf; simpl mapf_cast; unfold option_map, cast_back in *; intros; - unfold interpf_side_conditions in *; simpl in Hside; - repeat (repeat handle_options_step; break_match_hyps; inversion_option; inversion_sigma; autorewrite with push_to_prop in *; simpl in *; unfold option_map in *; subst; try tauto). - { destruct (Hctx _ _ _ Hr) as [b' [Hb'[Hb'v[v'[Hv' Hv'v]]]]]; clear Hctx Hr; subst. - repeat match goal with - [H: ?e = Some ?x, G:?e = Some ?x' |- _] => - pose proof (eq_trans (eq_sym G) H); clear G; inversion_option; subst - end. - auto. } - { do_specialize_IHe. - repeat (handle_options_step || destruct_head_and || specialize_by_assumption). - subst; intuition eauto; try (symmetry; rewrite_hyp ?*; eauto); - repeat handle_bounds_side_conditions_step; auto. } - { cbv [LetIn.Let_In] in *. - do_specialize_IHe. - destruct_head'_and. - destruct IHe1 as [IHe1_eq IHe1]; rewrite_hyp *; try assumption. - { apply IHe2; clear IHe2; try reflexivity; [ | t ]. - intros ??? Hlookup. - let b := fresh "b" in - let H' := fresh "H'" in - match goal with |- exists b0, ?v = Some b0 /\ _ => destruct v as [b|] eqn:H' end; - [ exists b; split; [ reflexivity | ] | exfalso ]; - revert Hlookup H'; t. } } - { do_specialize_IHe. - t. } - Qed. - - Lemma map_cast_correct - {t} (e:expr base_type_code op Name t) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - : forall - (oldValues:Context) - (newValues:Context) - (varBounds:BoundsContext) - {b} e' (He':map_cast varBounds e input_bounds = Some (existT _ b e')) - (Hctx:forall {t} n v, - lookupb (t:=t) oldValues n = Some v - -> exists b, lookupb (t:=t) varBounds n = Some b - /\ @inboundsb _ b v - /\ exists v', lookupb (t:=pick_typeb t b) newValues n = Some v' - /\ cast_backb t b v' = v) - v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v) - r (Hr:interp (interp_op:=interp_op) (ctx:=oldValues) e v = Some r) - r' (Hr':interp (interp_op:=interp_op) (ctx:=newValues) e' v' = Some r') - (Hside : prop_of_option (interp_side_conditions interp_op interped_op_side_conditions oldValues e v)) - , interp (interp_op:=interp_op_bounds) (ctx:=varBounds) e input_bounds = Some b - /\ @inbounds _ b r /\ cast_back _ _ r' = r. - Proof using Type*. - unfold map_cast, option_map, interp; simpl; intros. - repeat first [ progress subst - | progress inversion_option - | progress inversion_sigma - | progress break_match_hyps - | progress destruct_head' sigT - | progress simpl in * ]. - eapply mapf_cast_correct; try eassumption. - t. - Qed. -End language. diff --git a/src/Compilers/Named/MapCastWf.v b/src/Compilers/Named/MapCastWf.v deleted file mode 100644 index eb141cad1..000000000 --- a/src/Compilers/Named/MapCastWf.v +++ /dev/null @@ -1,285 +0,0 @@ -Require Import Coq.Bool.Sumbool. -Require Import Coq.Logic.Eqdep_dec. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.ContextProperties.SmartMap. -Require Import Crypto.Compilers.Named.Wf. -Require Import Crypto.Compilers.Named.MapCast. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.DestructHead. - -Local Open Scope nexpr_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type} - {interp_base_type_bounds : base_type_code -> Type} - (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst) - (pick_typeb : forall t, interp_base_type_bounds t -> base_type_code). - Local Notation pick_type t v := (SmartFlatTypeMap pick_typeb (t:=t) v). - Context (cast_op : forall t tR (opc : op t tR) args_bs, - op (pick_type _ args_bs) (pick_type _ (interp_op_bounds t tR opc args_bs))) - {BoundsContext : Context Name interp_base_type_bounds} - (BoundsContextOk : ContextOk BoundsContext) - {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) - {FullContext : Context Name (fun t => { b : interp_base_type_bounds t & interp_base_type (pick_typeb t b) }%type)} - (FullContextOk : ContextOk FullContext) - {Context : Context Name interp_base_type} - (ContextOk : ContextOk Context) - (base_type_dec : DecidableRel (@eq base_type_code)) - (Name_dec : DecidableRel (@eq Name)). - - Local Notation mapf_cast := (@mapf_cast _ op Name _ interp_op_bounds pick_typeb cast_op BoundsContext). - Local Notation map_cast := (@map_cast _ op Name _ interp_op_bounds pick_typeb cast_op BoundsContext). - - Local Ltac handle_options_step := - match goal with - | _ => progress inversion_option - | [ H : ?x = Some _ |- context[?x] ] => rewrite H - | [ H : ?x = None |- context[?x] ] => rewrite H - | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : Some _ <> None \/ _ |- _ ] => clear H - | [ H : Some ?x <> Some ?y |- _ ] => assert (x <> y) by congruence; clear H - | [ H : None <> Some _ |- _ ] => clear H - | [ H : Some _ <> None |- _ ] => clear H - | [ H : ?x <> ?x \/ _ |- _ ] => destruct H; [ exfalso; apply H; reflexivity | ] - | [ H : _ \/ None = Some _ |- _ ] => destruct H; [ | exfalso; clear -H; congruence ] - | [ H : _ \/ Some _ = None |- _ ] => destruct H; [ | exfalso; clear -H; congruence ] - | [ H : ?x = Some ?y, H' : ?x = Some ?y' |- _ ] - => assert (y = y') by congruence; (subst y' || subst y) - | _ => progress simpl @option_map - | _ => progress unfold option_map in * - end. - - Local Ltac handle_lookupb_step_extra := fail. - Local Ltac handle_lookupb_step := - let do_eq_dec dec t t' := - first [ constr_eq t t'; fail 1 - | lazymatch goal with - | [ H : t = t' |- _ ] => fail 1 - | [ H : t <> t' |- _ ] => fail 1 - | [ H : t = t' -> False |- _ ] => fail 1 - | _ => destruct (dec t t') - end ] in - let do_type_dec := do_eq_dec base_type_dec in - match goal with - | _ => progress unfold dec in * - | _ => handle_options_step - (* preprocess *) - | [ H : context[lookupb (extend _ _ _) _] |- _ ] - => first [ rewrite (lookupb_extend base_type_dec Name_dec) in H by assumption - | setoid_rewrite (lookupb_extend base_type_dec Name_dec) in H; [ | assumption.. ] ] - | [ |- context[lookupb (extend _ _ _) _] ] - => first [ rewrite (lookupb_extend base_type_dec Name_dec) by assumption - | setoid_rewrite (lookupb_extend base_type_dec Name_dec); [ | assumption.. ] ] - | _ => progress subst - (* handle multiple hypotheses *) - | [ H : find_Name _ ?n ?N = Some ?t', H'' : context[find_Name_and_val _ _ ?t ?n ?N ?x ?default] |- _ ] - => do_type_dec t t' - (* clear the default value *) - | [ H : context[find_Name_and_val ?tdec ?ndec ?t ?n (T:=?T) ?N ?V ?default] |- _ ] - => lazymatch default with None => fail | _ => idtac end; - rewrite find_Name_and_val_split in H - (* generic handlers *) - | [ H : find_Name _ ?n ?N = Some ?t', H' : ?t <> ?t', H'' : context[find_Name_and_val _ _ ?t ?n ?N ?x ?default] |- _ ] - => erewrite find_Name_and_val_wrong_type in H'' by eassumption - | [ H : context[find_Name _ _ (SmartFlatTypeMapInterp2 _ _ _)] |- _ ] - => rewrite find_Name_SmartFlatTypeMapInterp2 with (base_type_code_dec:=base_type_dec) in H - | [ H : find_Name_and_val _ _ _ _ _ _ _ = None |- _ ] - => apply find_Name_and_val_None_iff in H - | _ => progress handle_lookupb_step_extra - (* destructers *) - | [ |- context[find_Name_and_val ?tdec ?ndec ?t ?n ?N ?V ?default] ] - => destruct (find_Name_and_val tdec ndec t n N V default) eqn:? - | [ H : context[match find_Name_and_val ?tdec ?ndec ?t ?n ?N ?V ?default with _ => _ end] |- _ ] - => destruct (find_Name_and_val tdec ndec t n N V default) eqn:? - | [ H : context[match find_Name ?ndec ?n ?N with _ => _ end] |- _ ] - => destruct (find_Name ndec n N) eqn:? - | [ H : context[match base_type_dec ?x ?y with _ => _ end] |- _ ] - => destruct (base_type_dec x y) - | [ H : context[match Name_dec ?x ?y with _ => _ end] |- _ ] - => destruct (Name_dec x y) - end. - - Local Ltac handle_exists_in_goal := - lazymatch goal with - | [ |- exists v, Some ?k = Some v /\ @?B v ] - => exists k; split; [ reflexivity | ] - | [ |- exists v, Some ?k = Some v ] - => exists k; reflexivity - | [ |- (exists v, None = Some v /\ @?B v) ] - => exfalso - | [ |- ?A /\ (exists v, Some ?k = Some v /\ @?B v) ] - => cut (A /\ B k); [ clear; solve [ intuition eauto ] | cbv beta ] - | [ |- ?A /\ (exists v, None = Some v /\ @?B v) ] - => exfalso - end. - Local Ltac specializer_t_step := - match goal with - | [ H : ?T, H' : ?T |- _ ] => clear H - | [ H : forall x, Some _ = Some x -> _ |- _ ] => specialize (H _ eq_refl) - | [ H : ?x = Some _, IH : forall a b c, ?x = Some _ -> _ |- _ ] - => specialize (IH _ _ _ H) - | [ H : ?x = Some _, IH : forall a b, ?x = Some _ -> _ |- _ ] - => specialize (IH _ _ H) - | [ H : ?x = Some _, IH : forall a, ?x = Some _ -> _ |- _ ] - => specialize (IH _ H) - | [ H : forall t n x y z, lookupb ?ctx n = _ -> _, H' : lookupb ?ctx ?n' = _ |- _ ] - => specialize (H _ _ _ _ _ H') - | [ H : forall t n x y, lookupb ?ctx n = _ -> _, H' : lookupb ?ctx ?n' = _ |- _ ] - => specialize (H _ _ _ _ H') - | [ H : forall t n v, lookupb ?ctx n = _ -> _, H' : lookupb ?ctx ?n' = _ |- _ ] - => specialize (H _ _ _ H') - | _ => progress specialize_by auto - end. - - Local Ltac break_t_step := - first [ progress subst - | progress destruct_head'_ex - | progress destruct_head'_and - | progress inversion_option - | progress inversion_prod - | progress inversion_sigma - | progress autorewrite with push_prop_of_option in * - | progress break_match_hyps ]. - - Local Ltac do_specialize_IHe_step := - match goal with - | [ IH : context[mapf_cast _ ?e], H' : mapf_cast ?ctx ?e = _ |- _ ] - => let check_tac _ := (rewrite H' in IH) in - first [ specialize (IH ctx); check_tac () - | specialize (fun a => IH a ctx); check_tac () - | specialize (fun a b => IH a b ctx); check_tac () ] - | [ H : forall x y z w, Some _ = Some _ -> _ |- _ ] - => first [ specialize (H _ _ _ _ eq_refl) - | specialize (fun x y => H x y _ _ eq_refl) ] - | [ H : forall x y z, Some _ = Some _ -> _ |- _ ] - => first [ specialize (H _ _ _ eq_refl) - | specialize (fun x => H x _ _ eq_refl) ] - | [ H : forall x y, Some _ = Some _ -> _ |- _ ] - => first [ specialize (H _ _ eq_refl) - | specialize (fun x => H x _ eq_refl) ] - | _ => progress specialize_by_assumption - | [ H : forall a b, prop_of_option (Named.wff a ?e) -> _, H' : prop_of_option (Named.wff _ ?e) |- _ ] - => specialize (fun b => H _ b H') - | [ H : forall b v, _ -> prop_of_option (Named.wff b ?e) |- prop_of_option (Named.wff ?ctx ?e) ] - => specialize (H ctx) - | [ H : forall b v, _ -> _ -> prop_of_option (Named.wff b ?e) |- prop_of_option (Named.wff ?ctx ?e) ] - => specialize (H ctx) - | [ H : forall a b, _ -> _ -> _ -> prop_of_option (Named.wff b ?e) |- prop_of_option (Named.wff ?ctx ?e) ] - => specialize (fun a => H a ctx) - | [ H : forall a b, prop_of_option (Named.wff a ?e) -> _, H' : forall v, prop_of_option (Named.wff _ ?e) |- _ ] - => specialize (fun b v => H _ b (H' v)) - end. - Ltac do_specialize_IHe := repeat do_specialize_IHe_step. - - Definition make_fContext_value {t} {b : interp_flat_type interp_base_type_bounds t} - (v : interp_flat_type interp_base_type (pick_type t b)) - : interp_flat_type - (fun t => { b : interp_base_type_bounds t & interp_base_type (pick_typeb t b)}) - t - := SmartFlatTypeMapUnInterp2 - (fun t b (v : interp_flat_type _ (Tbase _)) - => existT (fun b => interp_base_type (pick_typeb t b)) b v) - v. - - Local Ltac t_step := - first [ progress intros - | progress simpl in * - | break_t_step - | handle_lookupb_step - | handle_exists_in_goal - | apply conj - | solve [ auto | exfalso; auto ] - | specializer_t_step - | progress do_specialize_IHe - | match goal with - | [ IH : forall v, _ -> ?T, v' : interp_flat_type _ _ |- ?T ] - => apply (IH (make_fContext_value v')); clear IH - end ]. - Local Ltac t := repeat t_step. - - Lemma find_Name_and_val_make_fContext_value_Some {T} - {N : interp_flat_type (fun _ : base_type_code => Name) T} - {B : interp_flat_type interp_base_type_bounds T} - {V : interp_flat_type interp_base_type (pick_type T B)} - {n : Name} - {t : base_type_code} - {v : { b : interp_base_type_bounds t & interp_base_type (pick_typeb t b)}} - {b} - (Hn : find_Name Name_dec n N = Some t) - (Hf : find_Name_and_val base_type_dec Name_dec t n N (make_fContext_value V) None = Some v) - (Hb : find_Name_and_val base_type_dec Name_dec t n N B None = Some b) - (N' := SmartFlatTypeMapInterp2 (var'':=fun _ => Name) (f:=pick_typeb) (fun _ _ n => n) _ N) - : b = projT1 v /\ find_Name_and_val base_type_dec Name_dec (pick_typeb t (projT1 v)) n N' V None = Some (projT2 v). - Proof using Type. - eapply (find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_Some base_type_dec Name_dec (h:=@projT1 _ _) (i:=@projT2 _ _) (f:=pick_typeb) (g:=fun _ => existT _)); - auto. - Qed. - - Local Ltac handle_lookupb_step_extra ::= - lazymatch goal with - | [ H : find_Name _ ?n ?N = Some ?t, - H' : find_Name_and_val _ _ ?t ?n ?N (@make_fContext_value ?T ?B ?v) None = Some ?v', - H'' : find_Name_and_val _ _ ?t ?n ?N ?B None = Some _ - |- _ ] - => pose proof (find_Name_and_val_make_fContext_value_Some H H' H''); clear H' - end. - - Lemma wff_mapf_cast - {t} (e:exprf base_type_code op Name t) - : forall - (fValues:FullContext) - (newValues:Context) - (varBounds:BoundsContext) - {b} e' (He':mapf_cast varBounds e = Some (existT _ b e')) - (Hwf : prop_of_option (Named.wff fValues e)) - (Hctx:forall {t} n v, - lookupb (t:=t) fValues n = Some v - -> lookupb (t:=t) varBounds n = Some (projT1 v) - /\ lookupb (t:=pick_typeb t (projT1 v)) newValues n = Some (projT2 v)), - prop_of_option (Named.wff newValues e'). - Proof using BoundsContextOk ContextOk FullContextOk Name_dec base_type_dec. induction e; t. Qed. - - Lemma wf_map_cast - {t} (e:expr base_type_code op Name t) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - : forall - (fValues:FullContext) - (newValues:Context) - (varBounds:BoundsContext) - {b} e' (He':map_cast varBounds e input_bounds = Some (existT _ b e')) - (Hwf : Named.wf fValues e) - (Hctx:forall {t} n v, - lookupb (t:=t) fValues n = Some v - -> lookupb (t:=t) varBounds n = Some (projT1 v) - /\ lookupb (t:=pick_typeb t (projT1 v)) newValues n = Some (projT2 v)), - Named.wf newValues e'. - Proof using BoundsContextOk ContextOk FullContextOk Name_dec base_type_dec. - unfold Named.wf, map_cast, option_map, interp; simpl; intros. - repeat first [ progress subst - | progress inversion_option - | progress inversion_sigma - | progress break_match_hyps - | progress destruct_head' sigT - | progress simpl in * ]. - match goal with v : _ |- _ => specialize (Hwf (make_fContext_value v)) end. - eapply wff_mapf_cast; eauto; []. - t. - Qed. -End language. diff --git a/src/Compilers/Named/MapType.v b/src/Compilers/Named/MapType.v deleted file mode 100644 index 15b40f7b7..000000000 --- a/src/Compilers/Named/MapType.v +++ /dev/null @@ -1,59 +0,0 @@ -Require Import Coq.Bool.Sumbool. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. - -Local Open Scope nexpr_scope. -Section language. - Context {base_type_code1 base_type_code2 : Type} - {op1 : flat_type base_type_code1 -> flat_type base_type_code1 -> Type} - {op2 : flat_type base_type_code2 -> flat_type base_type_code2 -> Type} - {Name : Type} - (f_base : base_type_code1 -> base_type_code2) - (f_op : forall s d, - op1 s d - -> option (op2 (lift_flat_type f_base s) (lift_flat_type f_base d))). - - Fixpoint mapf_type - {t} (e : exprf base_type_code1 op1 Name t) - : option (exprf base_type_code2 op2 Name (lift_flat_type f_base t)) - := match e in exprf _ _ _ t return option (exprf _ _ _ (lift_flat_type f_base t)) with - | TT => Some TT - | Var t x => Some (Var x) - | Op t1 tR opc args - => let opc := f_op _ _ opc in - let args := @mapf_type _ args in - match opc, args with - | Some opc, Some args => Some (Op opc args) - | _, _ => None - end - | LetIn tx n ex tC eC - => let n := transfer_interp_flat_type f_base (fun _ (n : Name) => n) n in - let ex := @mapf_type _ ex in - let eC := @mapf_type _ eC in - match ex, eC with - | Some ex, Some eC - => Some (LetIn _ n ex eC) - | _, _ => None - end - | Pair tx ex ty ey - => let ex := @mapf_type _ ex in - let ey := @mapf_type _ ey in - match ex, ey with - | Some ex, Some ey - => Some (Pair ex ey) - | _, _ => None - end - end. - - Definition map_type - {t} (e : expr base_type_code1 op1 Name t) - : option (expr base_type_code2 op2 Name (Arrow (lift_flat_type f_base (domain t)) (lift_flat_type f_base (codomain t)))) - := let f := invert_Abs e in - let f := mapf_type f in - let n := Abs_name e in - let n := transfer_interp_flat_type f_base (fun _ (n : Name) => n) n in - option_map - (fun f => Abs n f) - f. -End language. diff --git a/src/Compilers/Named/NameUtil.v b/src/Compilers/Named/NameUtil.v deleted file mode 100644 index 8b099ffdf..000000000 --- a/src/Compilers/Named/NameUtil.v +++ /dev/null @@ -1,56 +0,0 @@ -Require Import Coq.Lists.List. -Require Import Crypto.Compilers.Syntax. - -Local Open Scope core_scope. -Local Notation eta x := (fst x, snd x). - -Section language. - Context {base_type_code : Type} - {Name : Type}. - - Section monad. - Context (MName : Type) (force : MName -> option Name). - Fixpoint split_mnames - (t : flat_type base_type_code) (ls : list MName) - : option (interp_flat_type (fun _ => Name) t) * list MName - := match t return option (@interp_flat_type base_type_code (fun _ => Name) t) * _ with - | Tbase _ - => match ls with - | cons n ls' - => match force n with - | Some n => (Some n, ls') - | None => (None, ls') - end - | nil => (None, nil) - end - | Unit => (Some tt, ls) - | Prod A B - => let '(a, ls) := eta (@split_mnames A ls) in - let '(b, ls) := eta (@split_mnames B ls) in - (match a, b with - | Some a', Some b' => Some (a', b') - | _, _ => None - end, - ls) - end. - Definition mname_list_unique (ls : list MName) : Prop - := forall k n, - List.In (Some n) (firstn k (List.map force ls)) - -> List.In (Some n) (skipn k (List.map force ls)) - -> False. - End monad. - Definition split_onames := @split_mnames (option Name) (fun x => x). - Definition split_names := @split_mnames Name (@Some _). - - Definition oname_list_unique (ls : list (option Name)) : Prop - := mname_list_unique (option Name) (fun x => x) ls. - Definition name_list_unique (ls : list Name) : Prop - := oname_list_unique (List.map (@Some Name) ls). -End language. - -Global Arguments split_mnames {_ _ MName} force _ _, {_ _} MName force _ _. -Global Arguments split_onames {_ _} _ _. -Global Arguments split_names {_ _} _ _. -Global Arguments mname_list_unique {_ MName} force ls, {_} MName force ls. -Global Arguments oname_list_unique {_} ls. -Global Arguments name_list_unique {_} ls. diff --git a/src/Compilers/Named/NameUtilProperties.v b/src/Compilers/Named/NameUtilProperties.v deleted file mode 100644 index 944d164f2..000000000 --- a/src/Compilers/Named/NameUtilProperties.v +++ /dev/null @@ -1,223 +0,0 @@ -Require Import Coq.omega.Omega. -Require Import Coq.Arith.Arith. -Require Import Coq.Lists.List. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.CountLets. -Require Import Crypto.Compilers.Named.NameUtil. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.RewriteHyp. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SpecializeBy. - -Local Open Scope core_scope. -Section language. - Context {base_type_code : Type} - {Name : Type}. - - Section monad. - Context (MName : Type) (force : MName -> option Name). - - Lemma split_mnames_firstn_skipn - (t : flat_type base_type_code) (ls : list MName) - : split_mnames force t ls - = (fst (split_mnames force t (firstn (count_pairs t) ls)), - skipn (count_pairs t) ls). - Proof using Type. - apply path_prod_uncurried; simpl. - revert ls; induction t; split; split_prod; - repeat first [ progress simpl in * - | progress intros - | rewrite <- skipn_skipn - | reflexivity - | progress break_innermost_match_step - | apply (f_equal2 (@pair _ _)) - | rewrite_hyp <- !* - | match goal with - | [ H : forall ls, snd (split_mnames _ _ _) = _, H' : context[snd (split_mnames _ _ _)] |- _ ] - => rewrite H in H' - | [ H : _ |- _ ] => first [ rewrite <- firstn_skipn_add in H ] - | [ H : forall ls', fst (split_mnames _ _ _) = _, H' : context[fst (split_mnames _ _ (skipn ?n ?ls))] |- _ ] - => rewrite (H (skipn n ls)) in H' - | [ H : forall ls', fst (split_mnames _ _ _) = _, H' : context[fst (split_mnames _ ?t (firstn (count_pairs ?t + ?n) ?ls))] |- _ ] - => rewrite (H (firstn (count_pairs t + n) ls)), firstn_firstn in H' by omega - | [ H : forall ls', fst (split_mnames _ _ _) = _, H' : context[fst (split_mnames _ ?t ?ls)] |- _ ] - => is_var ls; rewrite (H ls) in H' - | [ H : ?x = Some _, H' : ?x = None |- _ ] => congruence - | [ H : ?x = Some ?a, H' : ?x = Some ?b |- _ ] - => assert (a = b) by congruence; (subst a || subst b) - end ]. - Qed. - - Lemma snd_split_mnames_skipn - (t : flat_type base_type_code) (ls : list MName) - : snd (split_mnames force t ls) = skipn (count_pairs t) ls. - Proof using Type. rewrite split_mnames_firstn_skipn; reflexivity. Qed. - Lemma fst_split_mnames_firstn - (t : flat_type base_type_code) (ls : list MName) - : fst (split_mnames force t ls) = fst (split_mnames force t (firstn (count_pairs t) ls)). - Proof using Type. rewrite split_mnames_firstn_skipn at 1; reflexivity. Qed. - - Lemma mname_list_unique_firstn_skipn n ls - : mname_list_unique force ls - -> (mname_list_unique force (firstn n ls) - /\ mname_list_unique force (skipn n ls)). - Proof using Type. - unfold mname_list_unique; intro H; split; intros k N; - rewrite <- ?firstn_map, <- ?skipn_map, ?skipn_skipn, ?firstn_firstn_min, ?firstn_skipn_add; - intros; eapply H; try eassumption. - { apply Min.min_case_strong. - { match goal with H : _ |- _ => rewrite skipn_firstn in H end; - eauto using In_firstn. } - { intro; match goal with H : _ |- _ => rewrite skipn_all in H by (rewrite firstn_length; omega * ) end. - simpl in *; tauto. } } - { eauto using In_skipn. } - Qed. - Definition mname_list_unique_firstn n ls - : mname_list_unique force ls -> mname_list_unique force (firstn n ls) - := fun H => proj1 (@mname_list_unique_firstn_skipn n ls H). - Definition mname_list_unique_skipn n ls - : mname_list_unique force ls -> mname_list_unique force (skipn n ls) - := fun H => proj2 (@mname_list_unique_firstn_skipn n ls H). - Lemma mname_list_unique_nil - : mname_list_unique force nil. - Proof using Type. - unfold mname_list_unique; simpl; intros ??. - rewrite firstn_nil, skipn_nil; simpl; auto. - Qed. - End monad. - - Lemma split_onames_firstn_skipn - (t : flat_type base_type_code) (ls : list (option Name)) - : split_onames t ls - = (fst (split_onames t (firstn (count_pairs t) ls)), - skipn (count_pairs t) ls). - Proof using Type. apply split_mnames_firstn_skipn. Qed. - Lemma snd_split_onames_skipn - (t : flat_type base_type_code) (ls : list (option Name)) - : snd (split_onames t ls) = skipn (count_pairs t) ls. - Proof using Type. apply snd_split_mnames_skipn. Qed. - Lemma fst_split_onames_firstn - (t : flat_type base_type_code) (ls : list (option Name)) - : fst (split_onames t ls) = fst (split_onames t (firstn (count_pairs t) ls)). - Proof using Type. apply fst_split_mnames_firstn. Qed. - - Lemma oname_list_unique_firstn n (ls : list (option Name)) - : oname_list_unique ls -> oname_list_unique (firstn n ls). - Proof using Type. apply mname_list_unique_firstn. Qed. - Lemma oname_list_unique_skipn n (ls : list (option Name)) - : oname_list_unique ls -> oname_list_unique (skipn n ls). - Proof using Type. apply mname_list_unique_skipn. Qed. - Lemma oname_list_unique_specialize (ls : list (option Name)) - : oname_list_unique ls - -> forall k n, - List.In (Some n) (firstn k ls) - -> List.In (Some n) (skipn k ls) - -> False. - Proof using Type. - intros H k n; specialize (H k n). - rewrite map_id in H; assumption. - Qed. - Definition oname_list_unique_nil : oname_list_unique (@nil (option Name)) - := mname_list_unique_nil _ (fun x => x). - - - Lemma split_names_firstn_skipn - (t : flat_type base_type_code) (ls : list Name) - : split_names t ls - = (fst (split_names t (firstn (count_pairs t) ls)), - skipn (count_pairs t) ls). - Proof using Type. apply split_mnames_firstn_skipn. Qed. - Lemma snd_split_names_skipn - (t : flat_type base_type_code) (ls : list Name) - : snd (split_names t ls) = skipn (count_pairs t) ls. - Proof using Type. apply snd_split_mnames_skipn. Qed. - Lemma fst_split_names_firstn - (t : flat_type base_type_code) (ls : list Name) - : fst (split_names t ls) = fst (split_names t (firstn (count_pairs t) ls)). - Proof using Type. apply fst_split_mnames_firstn. Qed. - - Lemma name_list_unique_firstn n (ls : list Name) - : name_list_unique ls -> name_list_unique (firstn n ls). - Proof using Type. - unfold name_list_unique; intro H; apply oname_list_unique_firstn with (n:=n) in H. - rewrite <- firstn_map; assumption. - Qed. - Lemma name_list_unique_skipn n (ls : list Name) - : name_list_unique ls -> name_list_unique (skipn n ls). - Proof using Type. - unfold name_list_unique; intro H; apply oname_list_unique_skipn with (n:=n) in H. - rewrite <- skipn_map; assumption. - Qed. - Lemma name_list_unique_specialize (ls : list Name) - : name_list_unique ls - -> forall k n, - List.In n (firstn k ls) - -> List.In n (skipn k ls) - -> False. - Proof using Type. - intros H k n; specialize (H k n). - rewrite !map_id, !firstn_map, !skipn_map in H. - eauto using in_map. - Qed. - Definition name_list_unique_nil : name_list_unique nil - := mname_list_unique_nil _ (@Some Name). - - Lemma length_fst_split_names_Some_iff - (t : flat_type base_type_code) (ls : list Name) - : fst (split_names t ls) <> None <-> List.length ls >= count_pairs t. - Proof using Type. - revert ls; induction t; intros ls; - try solve [ destruct ls; simpl; intuition (omega || congruence) ]. - repeat first [ progress simpl in * - | progress break_innermost_match_step - | progress specialize_by congruence - | progress specialize_by omega - | rewrite snd_split_names_skipn in * - | progress intros - | congruence - | omega - | match goal with - | [ H : forall ls, fst (split_names ?t ls) <> None <-> _, H' : fst (split_names ?t ?ls') = _ |- _ ] - => specialize (H ls'); rewrite H' in H - | [ H : _ |- _ ] => rewrite skipn_length in H - end - | progress split_iff - | match goal with - | [ |- iff _ _ ] => split - end ]. - Qed. - - Lemma length_fst_split_names_None_iff - (t : flat_type base_type_code) (ls : list Name) - : fst (split_names t ls) = None <-> List.length ls < count_pairs t. - Proof using Type. - destruct (length_fst_split_names_Some_iff t ls). - destruct (le_lt_dec (count_pairs t) (List.length ls)); specialize_by omega; - destruct (fst (split_names t ls)); split; try intuition (congruence || omega). - Qed. - - Lemma split_onames_split_names (t : flat_type base_type_code) (ls : list Name) - : split_onames t (List.map Some ls) - = (fst (split_names t ls), List.map Some (snd (split_names t ls))). - Proof using Type. - revert ls; induction t; - try solve [ destruct ls; reflexivity ]. - repeat first [ progress simpl in * - | progress intros - | rewrite snd_split_names_skipn - | rewrite snd_split_onames_skipn - | rewrite skipn_map - | match goal with - | [ H : forall ls, split_onames ?t (map Some ls) = _ |- context[split_onames ?t (map Some ?ls')] ] - => specialize (H ls') - end - | break_innermost_match_step - | progress inversion_prod - | congruence ]. - Qed. -End language. diff --git a/src/Compilers/Named/PositiveContext.v b/src/Compilers/Named/PositiveContext.v deleted file mode 100644 index 7b57098de..000000000 --- a/src/Compilers/Named/PositiveContext.v +++ /dev/null @@ -1,8 +0,0 @@ -Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Compilers.Named.FMapContext. - -Module PositiveContext := FMapContext PositiveMap. -Notation PositiveContext := PositiveContext.FMapContext. -Notation PositiveContext_nd := PositiveContext.FMapContext_nd. -Definition PositiveContextOk := PositiveContext.FMapContextOk (fun x y pf => pf). -Global Existing Instance PositiveContextOk. diff --git a/src/Compilers/Named/PositiveContext/Defaults.v b/src/Compilers/Named/PositiveContext/Defaults.v deleted file mode 100644 index 066de61cb..000000000 --- a/src/Compilers/Named/PositiveContext/Defaults.v +++ /dev/null @@ -1,29 +0,0 @@ -Require Import Coq.Lists.List. -Require Import Coq.Numbers.BinNums. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.PositiveContext. -Require Import Crypto.Compilers.Named.CountLets. -Require Import Crypto.Compilers.CountLets. - -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type}. - Definition default_names_forf {var} (dummy : forall t, var t) {t} (e : exprf base_type_code op (var:=var) t) : list positive - := map BinPos.Pos.of_succ_nat (seq 0 (count_let_bindersf dummy e)). - Definition default_names_for {var} (dummy : forall t, var t) {t} (e : expr base_type_code op (var:=var) t) : list positive - := map BinPos.Pos.of_succ_nat (seq 0 (count_binders dummy e)). - Definition DefaultNamesFor {t} (e : Expr base_type_code op t) : list positive - := map BinPos.Pos.of_succ_nat (seq 0 (CountBinders e)). -End language. - -Module Named. - Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type}. - Definition default_names_forf {Name} {t} (e : Named.exprf base_type_code op Name t) : list positive - := map BinPos.Pos.of_succ_nat (seq 0 (Named.CountLets.count_let_bindersf e)). - Definition default_names_for {Name} {t} (e : Named.expr base_type_code op Name t) : list positive - := map BinPos.Pos.of_succ_nat (seq 0 (Named.CountLets.count_binders e)). - End language. -End Named. diff --git a/src/Compilers/Named/PositiveContext/DefaultsProperties.v b/src/Compilers/Named/PositiveContext/DefaultsProperties.v deleted file mode 100644 index 2b46de136..000000000 --- a/src/Compilers/Named/PositiveContext/DefaultsProperties.v +++ /dev/null @@ -1,38 +0,0 @@ -Require Import Coq.Lists.List. -Require Import Coq.Numbers.BinNums. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.PositiveContext. -Require Import Crypto.Compilers.CountLets. -Require Import Crypto.Compilers.Named.NameUtil. -Require Import Crypto.Compilers.Named.PositiveContext.Defaults. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.Tactics.DestructHead. - -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type}. - - Lemma name_list_unique_map_pos_of_succ_nat_seq a b - : name_list_unique (map BinPos.Pos.of_succ_nat (seq a b)). - Proof using Type. - unfold name_list_unique, oname_list_unique, mname_list_unique. - intros k n. - rewrite !map_map, firstn_map, skipn_map, firstn_seq, skipn_seq. - rewrite !in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst. - match goal with H : _ |- _ => apply Pnat.SuccNat2Pos.inj in H end; subst. - rewrite in_seq in *. - omega *. - Qed. - - Lemma name_list_unique_default_names_forf {var dummy t e} - : name_list_unique (@default_names_forf base_type_code op var dummy t e). - Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. - Lemma name_list_unique_default_names_for {var dummy t e} - : name_list_unique (@default_names_for base_type_code op var dummy t e). - Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. - Lemma name_list_unique_DefaultNamesFor {t e} - : name_list_unique (@DefaultNamesFor base_type_code op t e). - Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. -End language. diff --git a/src/Compilers/Named/RegisterAssign.v b/src/Compilers/Named/RegisterAssign.v deleted file mode 100644 index 0b6c9b7b9..000000000 --- a/src/Compilers/Named/RegisterAssign.v +++ /dev/null @@ -1,89 +0,0 @@ -(** * Reassign registers *) -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.PositiveContext. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.NameUtil. -Require Import Crypto.Util.Decidable. - -Local Notation eta x := (fst x, snd x). - -Local Open Scope ctype_scope. -Delimit Scope nexpr_scope with nexpr. -Section language. - Context (base_type_code : Type) - (op : flat_type base_type_code -> flat_type base_type_code -> Type). - - Local Notation flat_type := (flat_type base_type_code). - Local Notation type := (type base_type_code). - Local Notation exprf := (@exprf base_type_code op). - Local Notation expr := (@expr base_type_code op). - - Section internal. - Context (InName OutName : Type) - {InContext : Context InName (fun _ : base_type_code => OutName)} - {ReverseContext : Context OutName (fun _ : base_type_code => InName)} - (InName_beq : InName -> InName -> bool). - - Definition register_reassignf_step - (register_reassignf : forall (ctxi : InContext) (ctxr : ReverseContext) - {t} (e : exprf InName t) (new_names : list (option OutName)), - option (exprf OutName t)) - (ctxi : InContext) (ctxr : ReverseContext) - {t} (e : exprf InName t) (new_names : list (option OutName)) - : option (exprf OutName t) - := match e in Named.exprf _ _ _ t return option (exprf _ t) with - | TT => Some TT - | Var t' name => match lookupb t' ctxi name with - | Some new_name - => match lookupb t' ctxr new_name with - | Some name' - => if InName_beq name name' - then Some (Var new_name) - else None - | None => None - end - | None => None - end - | Op _ _ op args - => option_map (Op op) (@register_reassignf ctxi ctxr _ args new_names) - | LetIn tx n ex _ eC - => let '(n', new_names') := eta (split_onames tx new_names) in - match n', @register_reassignf ctxi ctxr _ ex nil with - | Some n', Some x - => let ctxi := extend ctxi n n' in - let ctxr := extend ctxr n' n in - option_map (LetIn tx n' x) (@register_reassignf ctxi ctxr _ eC new_names') - | _, _ - => let ctxi := remove ctxi n in - @register_reassignf ctxi ctxr _ eC new_names' - end - | Pair _ ex _ ey - => match @register_reassignf ctxi ctxr _ ex nil, @register_reassignf ctxi ctxr _ ey nil with - | Some x, Some y - => Some (Pair x y) - | _, _ => None - end - end. - Fixpoint register_reassignf ctxi ctxr {t} e new_names - := @register_reassignf_step (@register_reassignf) ctxi ctxr t e new_names. - - Definition register_reassign (ctxi : InContext) (ctxr : ReverseContext) - {t} (e : expr InName t) (new_names : list (option OutName)) - : option (expr OutName t) - := match e in Named.expr _ _ _ t return option (expr _ t) with - | Abs src _ n f - => let '(n', new_names') := eta (split_onames src new_names) in - match n' with - | Some n' - => let ctxi := extend (t:=src) ctxi n n' in - let ctxr := extend (t:=src) ctxr n' n in - option_map (Abs n') (register_reassignf ctxi ctxr f new_names') - | None => None - end - end. - End internal. -End language. - -Global Arguments register_reassign {_ _ _ _ _ _} _ ctxi ctxr {t} e _. -Global Arguments register_reassignf {_ _ _ _ _ _} _ ctxi ctxr {t} e _. diff --git a/src/Compilers/Named/RegisterAssignInterp.v b/src/Compilers/Named/RegisterAssignInterp.v deleted file mode 100644 index be0e9cace..000000000 --- a/src/Compilers/Named/RegisterAssignInterp.v +++ /dev/null @@ -1,239 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.RegisterAssign. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.HProp. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.DestructHead. - -Local Open Scope nexpr_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {interp_base_type : base_type_code -> Type} - {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d} - {InName OutName : Type} - {InContext : Context InName (fun _ : base_type_code => OutName)} - {ReverseContext : Context OutName (fun _ : base_type_code => InName)} - {InContextOk : ContextOk InContext} - {ReverseContextOk : ContextOk ReverseContext} - {InName_beq : InName -> InName -> bool} - {InterpInContext : Context InName interp_base_type} - {InterpOutContext : Context OutName interp_base_type} - {InterpInContextOk : ContextOk InterpInContext} - {InterpOutContextOk : ContextOk InterpOutContext} - {base_type_code_dec : DecidableRel (@eq base_type_code)} - {OutName_dec : DecidableRel (@eq OutName)} - (InName_bl : forall n1 n2, InName_beq n1 n2 = true -> n1 = n2) - (InName_lb : forall n1 n2, n1 = n2 -> InName_beq n1 n2 = true). - - Local Instance InName_dec : DecidableRel (@eq InName) - := dec_rel_of_bool_dec_rel InName_beq InName_bl InName_lb. - - Local Notation register_reassignf := (@register_reassignf base_type_code op InName OutName InContext ReverseContext InName_beq). - Local Notation register_reassign := (@register_reassign base_type_code op InName OutName InContext ReverseContext InName_beq). - - Local Ltac t_find T := - induction T; - repeat first [ progress subst - | progress inversion_option - | progress simpl in * - | break_innermost_match_step - | break_innermost_match_hyps_step - | progress destruct_head'_and - | repeat apply conj; congruence - | progress cbv [cast_if_eq] in * - | progress eliminate_hprop_eq - | solve [ eauto ] - | match goal with - | [ |- context[@find_Name_and_val ?base_type_code ?Name ?base_type_code_dec ?Name_dec ?var' ?t ?n ?T ?N ?V ?default] ] - => lazymatch default with - | None => fail - | _ => rewrite (@find_Name_and_val_split base_type_code base_type_code_dec Name Name_dec var' t n T N V default) - end - | [ H : context[@find_Name_and_val ?base_type_code ?Name ?base_type_code_dec ?Name_dec ?var' ?t ?n ?T ?N ?V ?default] |- _ ] - => lazymatch default with - | None => fail - | _ => rewrite (@find_Name_and_val_split base_type_code base_type_code_dec Name Name_dec var' t n T N V default) in H - end - | [ H : forall a b, find_Name_and_val _ _ _ _ _ _ _ = Some _ -> _ |- find_Name_and_val _ _ _ _ _ _ _ = Some _ -> _ ] - => let H' := fresh in intro H'; pose proof (H _ _ H') - | [ H : forall a b, find_Name_and_val _ _ _ _ _ _ _ = Some _ -> _, H' : find_Name_and_val _ _ _ _ _ _ _ = Some _ |- _ ] - => specialize (H _ _ H') - | [ H : ?x = Some ?a, H' : ?y = Some ?b |- _ ] - => assert (a = b) by congruence; progress subst - end ]. - - - Lemma find_Name_and_val_OutToIn t T NI NO n_in n_out - : find_Name_and_val base_type_code_dec OutName_dec (T:=T) t n_out NO NI None = Some n_in - -> find_Name InName_dec n_in NI <> None. - Proof using Type. t_find T. Qed. - Lemma find_Name_and_val_InToOut t T NI NO n_in n_out - : find_Name_and_val base_type_code_dec InName_dec (T:=T) t n_in NI NO None = Some n_out - -> find_Name OutName_dec n_out NO <> None. - Proof using Type. t_find T. Qed. - - Lemma lookupb_extend_helper {ctxi : InContext} {ctxr : ReverseContext} {t T NI NO n_in n_out} - (H0 : lookupb t (extend (t:=T) ctxi NI NO) n_in = Some n_out) - (H1 : lookupb t (extend (t:=T) ctxr NO NI) n_out = Some n_in) - : ((lookupb t ctxi n_in = Some n_out /\ lookupb t ctxr n_out = Some n_in) - /\ (find_Name _ n_in NI = None /\ find_Name _ n_out NO = None)) - \/ (find_Name_and_val _ _ t n_in NI NO None = Some n_out - /\ find_Name_and_val _ _ t n_out NO NI None = Some n_in). - Proof using InContextOk ReverseContextOk. - rewrite (@lookupb_extend base_type_code _ InName _) in H0 by assumption. - rewrite (@lookupb_extend base_type_code _ OutName _) in H1 by assumption. - repeat first [ progress subst - | match goal with - | [ H : find_Name_and_val _ _ _ _ _ _ ?x = _ |- _ ] - => lazymatch x with - | None => fail - | _ => rewrite find_Name_and_val_split in H - end - end - | break_innermost_match_hyps_step - | congruence - | solve [ auto - | exfalso; eapply find_Name_and_val_OutToIn; eassumption - | exfalso; eapply find_Name_and_val_InToOut; eassumption ] ]. - Qed. - - Lemma find_Name_and_val_same_val {var' t T n_in n_out NI NO V v1 v2} - (H0 : find_Name_and_val base_type_code_dec InName_dec t (T:=T) (var':=var') n_in NI V None = Some v1) - (H1 : find_Name_and_val base_type_code_dec OutName_dec t (T:=T) n_out NO V None = Some v2) - (H2 : find_Name_and_val base_type_code_dec InName_dec t n_in NI NO None = Some n_out) - (H3 : find_Name_and_val base_type_code_dec OutName_dec t n_out NO NI None = Some n_in) - : v1 = v2. - Proof using Type. - t_find T; - match goal with - | [ H : _ = None |- _ ] - => first [ eapply find_Name_and_val_OutToIn in H; [ | eassumption ] - | eapply find_Name_and_val_InToOut in H; [ | eassumption ] ]; - destruct H - end. - Qed. - - Lemma find_Name_and_val_same_oval {var' t T n_in n_out NI NO V} - (H2 : find_Name_and_val base_type_code_dec InName_dec t n_in NI NO None = Some n_out) - (H3 : find_Name_and_val base_type_code_dec OutName_dec t n_out NO NI None = Some n_in) - : find_Name_and_val base_type_code_dec InName_dec t (T:=T) (var':=var') n_in NI V None - = find_Name_and_val base_type_code_dec OutName_dec t (T:=T) n_out NO V None. - Proof using Type. - t_find T; - match goal with - | [ H : _ = None |- _ ] - => first [ eapply find_Name_and_val_OutToIn in H; [ | eassumption ] - | eapply find_Name_and_val_InToOut in H; [ | eassumption ] ]; - destruct H - end. - Qed. - - Local Ltac t := - repeat first [ reflexivity - | assumption - | progress subst - | progress inversion_option - | progress simpl in * - | progress intros * - | progress intros - | progress destruct_head'_and - | progress destruct_head'_or - | match goal with - | [ H : InName_beq _ _ = true |- _ ] => apply InName_bl in H - | [ H : _ = Some ?v1, H' : _ = Some ?v2 |- _ ] - => is_var v1; is_var v2; - assert (v1 = v2) by eauto; progress subst - | [ H : lookupb (extend _ _ _) _ = Some _, H' : lookupb (extend _ _ _) _ = Some _ |- _ ] - => pose proof (lookupb_extend_helper H H'); clear H H' - | [ H : find_Name_and_val _ _ _ _ _ _ ?x = _ |- _ ] - => lazymatch x with - | None => fail - | _ => rewrite find_Name_and_val_split in H - end - | [ |- context[@find_Name_and_val ?base_type_code ?Name ?base_type_code_dec ?Name_dec ?var' ?t ?n ?T ?N ?V ?default] ] - => lazymatch default with - | None => fail - | _ => rewrite (@find_Name_and_val_split base_type_code base_type_code_dec Name Name_dec var' t n T N V default) - end - | [ H : _ |- _ ] - => first [ rewrite (@lookupb_remove base_type_code InName _) in H - | rewrite (@lookupb_remove base_type_code OutName _) in H - | rewrite (@lookupb_extend base_type_code _ InName _) in H - | rewrite (@lookupb_extend base_type_code _ OutName _) in H - | rewrite find_Name_and_val_different in H by assumption ] - end - | break_innermost_match_step - | break_innermost_match_hyps_step - | progress cbv [option_map LetIn.Let_In] in * - | solve [ eauto using find_Name_and_val_same_val ] - | match goal with - | [ H : _ |- ?v1 = ?v2 ] - => is_var v1; is_var v2; - eapply H; [ | eassumption | eassumption | eassumption ]; clear H - end ]. - - Lemma interpf_register_reassignf - ctxi ctxr t e new_names - (ctxi_interp : InterpInContext) - (ctxr_interp : InterpOutContext) - eout - v1 v2 - : (forall t (n_in : InName) (n_out : OutName) v1 v2, - lookupb t ctxi n_in = Some n_out - -> lookupb t ctxr n_out = Some n_in - -> lookupb t ctxi_interp n_in = Some v1 - -> lookupb t ctxr_interp n_out = Some v2 - -> v1 = v2) - -> @register_reassignf ctxi ctxr t e new_names = Some eout - -> interpf (interp_op:=interp_op) (ctx:=ctxr_interp) eout = Some v1 - -> interpf (interp_op:=interp_op) (ctx:=ctxi_interp) e = Some v2 - -> v1 = v2. - Proof using InContextOk InName_bl InName_lb InterpInContextOk InterpOutContextOk OutName_dec ReverseContextOk base_type_code_dec. - revert ctxi ctxr new_names ctxi_interp ctxr_interp eout v1 v2. - induction e; t. - Qed. - - Lemma interp_register_reassign - ctxi ctxr t e new_names - (ctxi_interp : InterpInContext) - (ctxr_interp : InterpOutContext) - eout - v1 v2 x - : (forall t (n_in : InName) (n_out : OutName) v1 v2, - lookupb t ctxi n_in = Some n_out - -> lookupb t ctxr n_out = Some n_in - -> lookupb t ctxi_interp n_in = Some v1 - -> lookupb t ctxr_interp n_out = Some v2 - -> v1 = v2) - -> @register_reassign ctxi ctxr t e new_names = Some eout - -> interp (interp_op:=interp_op) (ctx:=ctxr_interp) eout x = Some v1 - -> interp (interp_op:=interp_op) (ctx:=ctxi_interp) e x = Some v2 - -> v1 = v2. - Proof using InContextOk InName_bl InName_lb InterpInContextOk InterpOutContextOk OutName_dec ReverseContextOk base_type_code_dec. - destruct e; unfold interp, register_reassign, option_map in *. - break_innermost_match; try congruence. - intros; inversion_option; subst; simpl in *. - eapply interpf_register_reassignf; [ | eassumption.. ]. - t. - Qed. - - Lemma Interp_register_reassign - t e new_names - eout - v1 v2 x - : @register_reassign empty empty t e new_names = Some eout - -> Interp (Context:=InterpOutContext) (interp_op:=interp_op) eout x = Some v1 - -> Interp (Context:=InterpInContext) (interp_op:=interp_op) e x = Some v2 - -> v1 = v2. - Proof using InContextOk InName_bl InName_lb InterpInContextOk InterpOutContextOk OutName_dec ReverseContextOk base_type_code_dec. - apply interp_register_reassign; intros *. - rewrite !lookupb_empty; congruence. - Qed. -End language. diff --git a/src/Compilers/Named/SmartMap.v b/src/Compilers/Named/SmartMap.v deleted file mode 100644 index 76b2eec58..000000000 --- a/src/Compilers/Named/SmartMap.v +++ /dev/null @@ -1,20 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Named.Syntax. - -Module Export Named. - Section language. - Context {base_type_code : Type} - {interp_base_type : base_type_code -> Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {Name : Type}. - - (** [SmartVar] is like [Var], except that it inserts - pair-projections and [Pair] as necessary to handle - [flat_type], and not just [base_type_code] *) - Definition SmartVar {t} : interp_flat_type (fun _ => Name) t -> @exprf base_type_code op Name t - := smart_interp_flat_map (f:=fun _ => Name) (g:=@exprf _ _ _) (fun t => Var) TT (fun A B x y => Pair x y). - End language. -End Named. - -Global Arguments SmartVar {_ _ _ _} _. diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v deleted file mode 100644 index 4cc4ccbf2..000000000 --- a/src/Compilers/Named/Syntax.v +++ /dev/null @@ -1,92 +0,0 @@ -(** * Named Representation of Gallina *) -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.LetIn. - -Local Open Scope ctype_scope. -Local Open Scope expr_scope. -Delimit Scope nexpr_scope with nexpr. -Module Export Named. - Section language. - Context (base_type_code : Type) - (interp_base_type : base_type_code -> Type) - (op : flat_type base_type_code -> flat_type base_type_code -> Type) - (Name : Type). - - Local Notation flat_type := (flat_type base_type_code). - Local Notation type := (type base_type_code). - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type_gen := interp_flat_type. - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - - Inductive exprf : flat_type -> Type := - | TT : exprf Unit - | Var {t : base_type_code} : Name -> exprf (Tbase t) - | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR - | LetIn : forall {tx}, interp_flat_type_gen (fun _ => Name) tx -> exprf tx -> forall {tC}, exprf tC -> exprf tC - | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2). - Bind Scope nexpr_scope with exprf. - Inductive expr : type -> Type := - | Abs {src dst} : interp_flat_type_gen (fun _ => Name) src -> exprf dst -> expr (Arrow src dst). - Bind Scope nexpr_scope with expr. - Definition Abs_name {t} (e : expr t) : interp_flat_type_gen (fun _ => Name) (domain t) - := match e with Abs _ _ n f => n end. - Definition invert_Abs {t} (e : expr t) : exprf (codomain t) - := match e with Abs _ _ n f => f end. - - Section with_val_context. - Context (Context : Context Name interp_base_type) - (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). - - Fixpoint interpf - {t} (ctx : Context) (e : exprf t) - : option (interp_flat_type t) - := match e in exprf t return option (interp_flat_type t) with - | Var t' x => lookupb t' ctx x - | TT => Some tt - | Pair _ ex _ ey - => match @interpf _ ctx ex, @interpf _ ctx ey with - | Some xv, Some yv => Some (xv, yv)%core - | None, _ | _, None => None - end - | Op _ _ opc args - => option_map (@interp_op _ _ opc) (@interpf _ ctx args) - | LetIn _ n ex _ eC - => match @interpf _ ctx ex with - | Some xv - => dlet x := xv in - @interpf _ (extend ctx n x) eC - | None => None - end - end. - - Definition interp {t} (ctx : Context) (e : expr t) - : interp_flat_type (domain t) -> option (interp_flat_type (codomain t)) - := fun v => @interpf _ (extend ctx (Abs_name e) v) (invert_Abs e). - - Definition Interp {t} (e : expr t) - : interp_flat_type (domain t) -> option (interp_flat_type (codomain t)) - := interp empty e. - End with_val_context. - End language. -End Named. - -Global Arguments TT {_ _ _}. -Global Arguments Var {_ _ _ _} _. -Global Arguments Op {_ _ _ _ _} _ _. -Global Arguments LetIn {_ _ _} _ _ _ {_} _. -Global Arguments Pair {_ _ _ _} _ {_} _. -Global Arguments Abs {_ _ _ _ _} _ _. -Global Arguments invert_Abs {_ _ _ _} _. -Global Arguments Abs_name {_ _ _ _} _. -Global Arguments interpf {_ _ _ _ _ interp_op t ctx} _. -Global Arguments interp {_ _ _ _ _ interp_op t ctx} _ _. -Global Arguments Interp {_ _ _ _ _ interp_op t} _ _. - -Notation "'nlet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope. -Notation "'nlet' x : tx := A 'in' b" := (LetIn tx%ctype x%core A%nexpr b%nexpr) : nexpr_scope. -Notation "'λn' x .. y , t" := (Abs x .. (Abs y t%nexpr) .. ) : nexpr_scope. -Notation "( x , y , .. , z )" := (Pair .. (Pair x%nexpr y%nexpr) .. z%nexpr) : nexpr_scope. -Notation "()" := TT : nexpr_scope. diff --git a/src/Compilers/Named/WeakListContext.v b/src/Compilers/Named/WeakListContext.v deleted file mode 100644 index f1c4a46e3..000000000 --- a/src/Compilers/Named/WeakListContext.v +++ /dev/null @@ -1,10 +0,0 @@ -(** * Context made from an associative list *) -Require Import Coq.FSets.FMapWeakList. -Require Import Coq.FSets.FMapInterface. -Require Import Crypto.Compilers.Named.FMapContext. - -Module WeakListContext (E : DecidableType). - Module WL := FMapWeakList.Make E. - Module Context := FMapContext WL. - Include Context. -End WeakListContext. diff --git a/src/Compilers/Named/Wf.v b/src/Compilers/Named/Wf.v deleted file mode 100644 index 79f620edb..000000000 --- a/src/Compilers/Named/Wf.v +++ /dev/null @@ -1,56 +0,0 @@ -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Util.PointedProp. - -Module Export Named. - Section language. - Context {base_type_code Name : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type}. - Section with_var. - Context {var} - (Context : @Context base_type_code Name var). - - Section gen. - Context (quantify : forall tx, (interp_flat_type var tx -> option pointed_Prop) -> option pointed_Prop). - - Fixpoint wff_gen (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop - := match e with - | TT => Some trivial - | Var t n => match lookupb t ctx n return bool with - | Some _ => true - | None => false - end - | Op _ _ op args => @wff_gen ctx _ args - | LetIn _ n ex _ eC => @wff_gen ctx _ ex - /\ quantify _ (fun v => @wff_gen (extend ctx n v) _ eC) - | Pair _ ex _ ey => @wff_gen ctx _ ex /\ @wff_gen ctx _ ey - end%option_pointed_prop. - End gen. - - Definition wff := wff_gen (fun tx f => inject (forall v, prop_of_option (f v))). - Definition wf (ctx : Context) {t} (e : @expr base_type_code op Name t) : Prop - := forall v, prop_of_option (@wff (extend ctx (Abs_name e) v) _ (invert_Abs e)). - End with_var. - - Section unit. - Context (Context : @Context base_type_code Name (fun _ => unit)). - - Local Notation TT := (SmartValf _ (fun _ => tt) _). - Definition wff_unit := wff_gen Context (fun tx f => f TT). - Definition wf_unit ctx {t} (e : @expr base_type_code op Name t) : option pointed_Prop - := @wff_unit (extend ctx (Abs_name e) TT) _ (invert_Abs e). - End unit. - - Definition Wf (Context : forall var, @Context base_type_code Name var) {t} (e : @expr base_type_code op Name t) - := forall var, wf (Context var) empty e. - End language. -End Named. - -Global Arguments wff_gen {_ _ _ _ _} quantify ctx {t} _. -Global Arguments wff_unit {_ _ _ _} ctx {t} _. -Global Arguments wf_unit {_ _ _ _} ctx {t} _. -Global Arguments wff {_ _ _ _ _} ctx {t} _. -Global Arguments wf {_ _ _ _ _} ctx {t} _. -Global Arguments Wf {_ _ _} Context {t} _. diff --git a/src/Compilers/Named/WfFromUnit.v b/src/Compilers/Named/WfFromUnit.v deleted file mode 100644 index e00a79274..000000000 --- a/src/Compilers/Named/WfFromUnit.v +++ /dev/null @@ -1,82 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.ContextProperties. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Wf. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Option. - -Section language. - Context {base_type_code Name : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {base_type_code_dec : DecidableRel (@eq base_type_code)} - {Name_dec : DecidableRel (@eq Name)}. - - Section with_var. - Context {var} - (uContext : @Context base_type_code Name (fun _ => unit)) - (uContextOk : ContextOk uContext) - (vContext : @Context base_type_code Name var) - (vContextOk : ContextOk vContext). - - Local Ltac t := - repeat first [ progress simpl in * - | progress intros - | progress subst - | progress inversion_option - | congruence - | tauto - | solve [ eauto ] - | break_innermost_match_step - | break_innermost_match_hyps_step - | progress destruct_head'_and - | progress autorewrite with push_prop_of_option push_eq_Some_trivial in * - | rewrite !(@lookupb_extend base_type_code _ Name _) by auto - | rewrite (@find_Name_and_val_split base_type_code _ Name _) with (default := lookupb _ _) - | match goal with - | [ H : ?x = Some _ |- _ ] - => assert (x = None) by (split_iff; eauto); congruence - | [ |- _ /\ _ ] => split - | [ H : _ |- prop_of_option _ ] => eapply H; [ | eassumption ]; clear H - | [ |- context[find_Name_and_val ?tdec ?ndec ?b _ _ _ _ = None] ] - => rewrite <- !(@find_Name_and_val_None_iff _ tdec _ ndec _ b) - end ]. - - Lemma wff_from_unit - (vctx : vContext) - (uctx : uContext) - (Hctx : forall t n, lookupb t vctx n = None <-> lookupb t uctx n = None) - {t} (e : @exprf base_type_code op Name t) - : wff_unit uctx e = Some trivial -> prop_of_option (wff vctx e). - Proof using Name_dec base_type_code_dec uContextOk vContextOk. - revert uctx vctx Hctx; induction e; t. - Qed. - - Lemma wf_from_unit - (vctx : vContext) - (uctx : uContext) - (Hctx : forall t n, lookupb t vctx n = None <-> lookupb t uctx n = None) - {t} (e : @expr base_type_code op Name t) - : wf_unit uctx e = Some trivial -> wf vctx e. - Proof using Name_dec base_type_code_dec uContextOk vContextOk. - intros H ?; revert H; apply wff_from_unit; t. - Qed. - End with_var. - - Lemma Wf_from_unit - (Context : forall var, @Context base_type_code Name var) - (ContextOk : forall var, ContextOk (Context var)) - {t} (e : @expr base_type_code op Name t) - : wf_unit (Context:=Context _) empty e = Some trivial -> Wf Context e. - Proof using Name_dec base_type_code_dec. - intros H ?; revert H; apply wf_from_unit; auto; intros. - rewrite !lookupb_empty by auto; tauto. - Qed. -End language. - -Hint Resolve wf_from_unit Wf_from_unit wff_from_unit : wf. diff --git a/src/Compilers/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v deleted file mode 100644 index e9cd8737c..000000000 --- a/src/Compilers/Named/WfInterp.v +++ /dev/null @@ -1,41 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Context. -Require Import Crypto.Compilers.Named.Syntax. -Require Import Crypto.Compilers.Named.Wf. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.DestructHead. - -Section language. - Context {base_type_code Name interp_base_type} - {op : flat_type base_type_code -> flat_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} - {Context : @Context base_type_code Name interp_base_type}. - - Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t} - (Hwf : prop_of_option (wff ctx e)) - : @interpf base_type_code interp_base_type op Name Context interp_op t ctx e <> None. - Proof using Type. - revert dependent ctx; induction e; - repeat first [ progress intros - | progress simpl in * - | progress unfold option_map, LetIn.Let_In in * - | congruence - | progress specialize_by_assumption - | progress destruct_head' and - | progress break_innermost_match_step - | progress break_match_hyps - | progress autorewrite with push_prop_of_option in * - | progress specialize_by auto - | solve [ intuition eauto ] ]. - Qed. - - Lemma wf_interp_not_None {ctx : Context} {t} {e : @expr base_type_code op Name t} - (Hwf : wf ctx e) - v - : @interp base_type_code interp_base_type op Name Context interp_op t ctx e v <> None. - Proof using Type. - destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto. - Qed. -End language. |