diff options
| -rw-r--r-- | _CoqProject | 16 | ||||
| -rw-r--r-- | src/Compilers/BoundByCast.v | 48 | ||||
| -rw-r--r-- | src/Compilers/BoundByCastInterp.v | 117 | ||||
| -rw-r--r-- | src/Compilers/BoundByCastWf.v | 47 | ||||
| -rw-r--r-- | src/Compilers/InlineCast.v | 90 | ||||
| -rw-r--r-- | src/Compilers/InlineCastInterp.v | 115 | ||||
| -rw-r--r-- | src/Compilers/InlineCastWf.v | 131 | ||||
| -rw-r--r-- | src/Compilers/MapCast.v | 105 | ||||
| -rw-r--r-- | src/Compilers/MapCastInterp.v | 291 | ||||
| -rw-r--r-- | src/Compilers/MapCastWf.v | 172 | ||||
| -rw-r--r-- | src/Compilers/MultiSizeTest2.v | 183 | ||||
| -rw-r--r-- | src/Compilers/SmartBound.v | 135 | ||||
| -rw-r--r-- | src/Compilers/SmartBoundInterp.v | 144 | ||||
| -rw-r--r-- | src/Compilers/SmartBoundWf.v | 140 | ||||
| -rw-r--r-- | src/Compilers/SmartCast.v | 41 | ||||
| -rw-r--r-- | src/Compilers/SmartCastInterp.v | 37 | ||||
| -rw-r--r-- | src/Compilers/SmartCastWf.v | 84 |
17 files changed, 0 insertions, 1896 deletions
diff --git a/_CoqProject b/_CoqProject index 5949f7239..36cddc8ab 100644 --- a/_CoqProject +++ b/_CoqProject @@ -22,9 +22,6 @@ src/Arithmetic/BarrettReduction/HAC.v src/Arithmetic/BarrettReduction/Wikipedia.v src/Arithmetic/MontgomeryReduction/Definition.v src/Arithmetic/MontgomeryReduction/Proofs.v -src/Compilers/BoundByCast.v -src/Compilers/BoundByCastInterp.v -src/Compilers/BoundByCastWf.v src/Compilers/CommonSubexpressionElimination.v src/Compilers/CommonSubexpressionEliminationDenote.v src/Compilers/CommonSubexpressionEliminationInterp.v @@ -40,9 +37,6 @@ src/Compilers/ExprInversion.v src/Compilers/FilterLive.v src/Compilers/FoldTypes.v src/Compilers/Inline.v -src/Compilers/InlineCast.v -src/Compilers/InlineCastInterp.v -src/Compilers/InlineCastWf.v src/Compilers/InlineInterp.v src/Compilers/InlineWf.v src/Compilers/InputSyntax.v @@ -55,26 +49,16 @@ src/Compilers/Linearize.v src/Compilers/LinearizeInterp.v src/Compilers/LinearizeWf.v src/Compilers/Map.v -src/Compilers/MapCast.v src/Compilers/MapCastByDeBruijn.v src/Compilers/MapCastByDeBruijnInterp.v src/Compilers/MapCastByDeBruijnWf.v -src/Compilers/MapCastInterp.v -src/Compilers/MapCastWf.v src/Compilers/MultiSizeTest.v -src/Compilers/MultiSizeTest2.v src/Compilers/Reify.v src/Compilers/Relations.v src/Compilers/RenameBinders.v src/Compilers/Rewriter.v src/Compilers/RewriterInterp.v src/Compilers/RewriterWf.v -src/Compilers/SmartBound.v -src/Compilers/SmartBoundInterp.v -src/Compilers/SmartBoundWf.v -src/Compilers/SmartCast.v -src/Compilers/SmartCastInterp.v -src/Compilers/SmartCastWf.v src/Compilers/SmartMap.v src/Compilers/Syntax.v src/Compilers/TestCase.v diff --git a/src/Compilers/BoundByCast.v b/src/Compilers/BoundByCast.v deleted file mode 100644 index 3a7bf143a..000000000 --- a/src/Compilers/BoundByCast.v +++ /dev/null @@ -1,48 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartBound. -Require Import Crypto.Compilers.InlineCast. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Compilers.Inline. -Require Import Crypto.Compilers.Linearize. -Require Import Crypto.Compilers.MapCast. -Require Import Crypto.Compilers.Eta. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> 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) - (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (is_cast : forall src dst, op src dst -> bool) - (is_const : forall src dst, op src dst -> bool) - (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), - option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) - (failf : forall var t, @exprf base_type_code op var (Tbase t)). - - Local Notation Expr := (@Expr base_type_code op). - - Definition Boundify {t1} (e1 : Expr t1) args2 - : Expr _ - := ExprEta - (InlineCast - _ base_type_bl_transparent base_type_leb Cast is_cast is_const - (Linearize - (SmartBound - _ - interp_op_bounds - bound_base_type - Cast - (@MapInterpCast - base_type_code interp_base_type_bounds - op (@interp_op_bounds) - (@failf) - (@bound_op _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast genericize_op) - t1 e1 args2) - args2))). -End language. diff --git a/src/Compilers/BoundByCastInterp.v b/src/Compilers/BoundByCastInterp.v deleted file mode 100644 index 77496659b..000000000 --- a/src/Compilers/BoundByCastInterp.v +++ /dev/null @@ -1,117 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.InterpWfRel. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.BoundByCast. -Require Import Crypto.Compilers.SmartBound. -Require Import Crypto.Compilers.SmartBoundInterp. -Require Import Crypto.Compilers.SmartBoundWf. -Require Import Crypto.Compilers.InlineCastInterp. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Compilers.InlineInterp. -Require Import Crypto.Compilers.LinearizeInterp. -Require Import Crypto.Compilers.LinearizeWf. -Require Import Crypto.Compilers.MapCastInterp. -Require Import Crypto.Compilers.MapCastWf. -Require Import Crypto.Compilers.EtaInterp. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (interp_base_type interp_base_type_bounds : 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) - (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) - (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (cast_val : forall A A', interp_base_type A -> interp_base_type A') - (is_cast : forall src dst, op src dst -> bool) - (is_const : forall src dst, op src dst -> bool) - (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), - option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) - (failf : forall var t, @exprf base_type_code op var (Tbase t)) - (bound_is_good : forall t, interp_base_type_bounds t -> Prop) - (is_bounded_by_base : forall t, interp_base_type t -> interp_base_type_bounds t -> Prop) - (interpf_Cast_id : forall A x, interpf interp_op (Cast _ A A x) = interpf interp_op x) - (interpf_cast : forall A A' e, interpf interp_op (Cast _ A A' e) = cast_val A A' (interpf interp_op e)) - (cast_val_squash : forall a b c v, - base_type_min base_type_leb b (base_type_min base_type_leb a c) = base_type_min base_type_leb a c - -> cast_val b c (cast_val a b v) = cast_val a c v) - (is_cast_correct : forall s d opc e, is_cast (Tbase s) (Tbase d) opc = true - -> interp_op _ _ opc (interpf interp_op e) - = interpf interp_op (Cast _ s d e)) - (wff_Cast : forall var1 var2 G A A' e1 e2, - wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)) - (strip_cast_val - : forall t x y, - is_bounded_by_base t y x -> - cast_val (bound_base_type t x) t (cast_val t (bound_base_type t x) y) = y). - Local Notation is_bounded_by (*{T} : interp_flat_type interp_base_type T -> interp_flat_type interp_base_type_bounds T -> Prop*) - := (interp_flat_type_rel_pointwise is_bounded_by_base). - Context (is_bounded_by_interp_op - : forall src dst opc sv1 sv2, - is_bounded_by sv1 sv2 -> - is_bounded_by (interp_op src dst opc sv1) (interp_op_bounds src dst opc sv2)). - Local Notation bounds_are_good - := (@interp_flat_type_rel_pointwise1 _ _ bound_is_good). - Local Notation bound_op := (@bound_op _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast genericize_op). - Local Notation G_invariant_holds G - := (forall t x x', - List.In (existT _ t (x, x')%core) G -> is_bounded_by_base t x x') - (only parsing). - Context (interpf_bound_op - : forall G t tR opc ein eout ebounds, - wff G ein ebounds - -> G_invariant_holds G - -> interpf interp_op ein = interpf interp_op eout - -> bounds_are_recursively_good interp_op_bounds bound_is_good ebounds - -> bounds_are_good (interp_op_bounds t tR opc (interpf interp_op_bounds ebounds)) - -> interpf interp_op (@bound_op interp_base_type t tR t tR opc opc eout (interpf interp_op_bounds ebounds)) - = interpf interp_op (Op opc ein)). - - Context (is_bounded_by_bound_op - : forall G t tR opc ein eout ebounds, - wff G ein ebounds - -> G_invariant_holds G - -> interpf interp_op ein = interpf interp_op eout - -> bounds_are_recursively_good interp_op_bounds bound_is_good ebounds - -> bounds_are_good (interp_op_bounds t tR opc (interpf interp_op_bounds ebounds)) - -> is_bounded_by - (interpf interp_op (@bound_op interp_base_type t tR t tR opc opc eout (interpf interp_op_bounds ebounds))) - (interpf interp_op_bounds (Op opc ebounds))). - - Local Notation Expr := (@Expr base_type_code op). - Local Notation Boundify := (@Boundify _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast is_cast is_const genericize_op failf). - Local Notation interpf_smart_unbound := (@interpf_smart_unbound _ interp_base_type_bounds bound_base_type interp_base_type cast_val). - - Lemma InterpBoundifyAndRel {t} - (e : Expr t) - (Hwf : Wf e) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - (output_bounds := Interp interp_op_bounds e input_bounds) - (e' := Boundify e input_bounds) - (Hgood : bounds_are_recursively_good - (@interp_op_bounds) bound_is_good - (invert_Abs (e _) input_bounds)) - : forall x, - is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds - -> is_bounded_by (Interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds - /\ interpf_smart_unbound _ (Interp interp_op e' x) - = Interp interp_op e (interpf_smart_unbound input_bounds x). - Proof using cast_val_squash interpf_Cast_id interpf_bound_op interpf_cast is_bounded_by_bound_op is_bounded_by_interp_op is_cast_correct strip_cast_val wff_Cast. - intros; subst e' output_bounds. - unfold Boundify. - erewrite InterpExprEta, InterpInlineCast, InterpLinearize by eauto with wf. - match goal with |- ?A /\ ?B => cut (A /\ (A -> B)); [ tauto | ] end. - split. - { apply interp_wf; auto. } - { intro Hbounded_out. - erewrite InterpSmartBound, InterpMapInterpCast by eauto with wf. - reflexivity. } - Qed. -End language. diff --git a/src/Compilers/BoundByCastWf.v b/src/Compilers/BoundByCastWf.v deleted file mode 100644 index d03ec1359..000000000 --- a/src/Compilers/BoundByCastWf.v +++ /dev/null @@ -1,47 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.BoundByCast. -Require Import Crypto.Compilers.EtaWf. -Require Import Crypto.Compilers.InlineCastWf. -Require Import Crypto.Compilers.LinearizeWf. -Require Import Crypto.Compilers.SmartBoundWf. -Require Import Crypto.Compilers.MapCastWf. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> 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) - (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (is_cast : forall src dst, op src dst -> bool) - (is_const : forall src dst, op src dst -> bool) - (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), - option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) - (failf : forall var t, @exprf base_type_code op var (Tbase t)) - (wff_Cast : forall var1 var2 G A A' e1 e2, - wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)). - - Local Notation Expr := (@Expr base_type_code op). - - Lemma Wf_Boundify {t1} (e1 : Expr t1) args2 - (Hwf : Wf e1) - : Wf (@Boundify - _ op _ interp_op_bounds - bound_base_type - _ base_type_bl_transparent - base_type_leb - Cast - is_cast is_const genericize_op - failf t1 e1 args2). - Proof using wff_Cast. - unfold Boundify; auto 7 with wf. - Qed. -End language. - -Hint Resolve Wf_Boundify : wf. diff --git a/src/Compilers/InlineCast.v b/src/Compilers/InlineCast.v deleted file mode 100644 index 675835760..000000000 --- a/src/Compilers/InlineCast.v +++ /dev/null @@ -1,90 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartCast. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.Inline. -Require Import Crypto.Util.Notations. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (is_cast : forall src dst, op src dst -> bool) - (is_const : forall src dst, op src dst -> bool). - Local Infix "<=?" := base_type_leb : expr_scope. - Local Infix "=?" := base_type_beq : expr_scope. - - Local Notation base_type_min := (base_type_min base_type_leb). - Local Notation SmartCast_base := (@SmartCast_base _ op _ base_type_bl_transparent Cast). - - Local Notation flat_type := (flat_type base_type_code). - Local Notation exprf := (@exprf base_type_code op). - Local Notation Expr := (@Expr base_type_code op). - - (** We can squash [a -> b -> c] into [a -> c] if [min a b c = min a - c], i.e., if the narrowest type we pass through in the original - case is the same as the narrowest type we pass through in the - new case. *) - Definition squash_cast {var} (a b c : base_type_code) - : @exprf var (Tbase a) -> @exprf var (Tbase c) - := if base_type_beq (base_type_min b (base_type_min a c)) (base_type_min a c) - then SmartCast_base - else fun x => Cast _ b c (Cast _ a b x). - Fixpoint maybe_push_cast {var t} (v : @exprf var t) : option (@exprf var t) - := match v in Syntax.exprf _ _ t return option (exprf t) with - | Var _ _ as v' - => Some v' - | Op t1 tR opc args - => match t1, tR return op t1 tR -> exprf t1 -> option (exprf tR) with - | Tbase b, Tbase c - => fun opc args - => if is_cast _ _ opc - then match @maybe_push_cast _ _ args with - | Some (Op t1 tR opc' args') - => match t1, tR return op t1 tR -> exprf t1 -> option (exprf (Tbase c)) with - | Tbase a, Tbase b - => fun opc' args' - => if is_cast _ _ opc' - then Some (squash_cast a b c args') - else None - | Unit, Tbase _ - => fun opc' args' - => if is_const _ _ opc' - then Some (SmartCast_base (Op opc' TT)) - else None - | _, _ => fun _ _ => None - end opc' args' - | Some (Var _ v as v') => Some (SmartCast_base v') - | Some _ => None - | None => None - end - else None - | Unit, _ - => fun opc args - => if is_const _ _ opc - then Some (Op opc TT) - else None - | _, _ - => fun _ _ => None - end opc args - | Pair _ _ _ _ - | LetIn _ _ _ _ - | TT - => None - end. - Definition push_cast {var t} : @exprf var t -> @inline_directive _ op var t - := match t with - | Tbase _ => fun v => match maybe_push_cast v with - | Some e => inline e - | None => default_inline v - end - | _ => default_inline - end. - - Definition InlineCast {t} (e : Expr t) : Expr t - := InlineConstGen (@push_cast) e. -End language. diff --git a/src/Compilers/InlineCastInterp.v b/src/Compilers/InlineCastInterp.v deleted file mode 100644 index 2b2e08b4d..000000000 --- a/src/Compilers/InlineCastInterp.v +++ /dev/null @@ -1,115 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.TypeInversion. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Compilers.InlineCast. -Require Import Crypto.Compilers.InlineInterp. -Require Import Crypto.Compilers.SmartCast. -Require Import Crypto.Compilers.SmartCastInterp. -Require Import Crypto.Compilers.Inline. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Notations. - -Local Open Scope expr_scope. -Local Open Scope ctype_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 src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst} - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (is_cast : forall src dst, op src dst -> bool) - (is_const : forall src dst, op src dst -> bool) - (interpf_Cast_id : forall A x, interpf interp_op (Cast _ A A x) = interpf interp_op x) - (cast_val : forall A A', interp_base_type A -> interp_base_type A') - (interpf_cast : forall A A' e, interpf interp_op (Cast _ A A' e) = cast_val A A' (interpf interp_op e)) - (cast_val_squash : forall a b c v, - base_type_min base_type_leb b (base_type_min base_type_leb a c) = base_type_min base_type_leb a c - -> cast_val b c (cast_val a b v) = cast_val a c v) - (is_cast_correct : forall s d opc e, is_cast (Tbase s) (Tbase d) opc = true - -> interp_op _ _ opc (interpf interp_op e) - = interpf interp_op (Cast _ s d e)). - - Local Notation SmartCast_base := (@SmartCast_base _ op _ base_type_bl_transparent Cast interp_base_type). - Local Notation squash_cast := (@squash_cast _ op _ base_type_bl_transparent base_type_leb Cast). - Local Notation maybe_push_cast := (@maybe_push_cast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const). - Local Notation push_cast := (@push_cast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const). - Local Notation InlineCast := (@InlineCast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const). - Local Notation base_type_min := (base_type_min base_type_leb). - - Lemma cast_val_id A (v : exprf _ _ (Tbase A)) - : cast_val A A (interpf interp_op v) = interpf interp_op v. - Proof using interpf_Cast_id interpf_cast. rewrite <- !interpf_cast, !interpf_Cast_id; reflexivity. Qed. - - Lemma interpf_squash_cast a b c e1 - : interpf interp_op (@squash_cast _ a b c e1) = interpf interp_op (Cast _ b c (Cast _ a b e1)). - Proof using cast_val_squash interpf_Cast_id interpf_cast. - unfold squash_cast; - repeat first [ progress break_innermost_match - | intro - | reflexivity - | progress subst - | match goal with H : base_type_beq _ _ = true |- _ => apply base_type_bl_transparent in H end - | rewrite !cast_val_id - | rewrite !interpf_SmartCast_base by assumption - | rewrite !interpf_Cast_id - | rewrite interpf_cast - | rewrite cast_val_squash by assumption ]. - Qed. - - Lemma interpf_maybe_push_cast t e e' - : @maybe_push_cast _ t e = Some e' - -> interpf interp_op e' = interpf interp_op e. - Proof using cast_val_squash interpf_Cast_id interpf_cast is_cast_correct. - revert e'; induction e; - repeat first [ reflexivity - | discriminate - | progress subst - | progress inversion_option - | progress break_innermost_match_step - | progress simpl in * - | intro - | rewrite !interpf_SmartCast_base by assumption - | setoid_rewrite interpf_SmartCast_base; [ | assumption.. ] - | erewrite is_cast_correct by eassumption - | progress change (fun t => interp_base_type t) with interp_base_type in * - | rewrite !interpf_cast - | rewrite !interpf_squash_cast - | match goal with - | [ H : forall x, Some _ = Some x -> _ |- _ ] - => specialize (H _ eq_refl) - | [ |- context[interpf (t:=Unit) interp_op ?e] ] - => destruct (interpf interp_op e) - | [ H : maybe_push_cast ?e = Some _, H' : _ = interpf interp_op ?e |- _ ] - => rewrite <- H'; clear e H H' - | [ H : context[match ?e with _ => _ end] |- _ ] - => invert_one_expr e - end ]. - Qed. - - Lemma interpf_exprf_of_push_cast t e - : interpf interp_op (exprf_of_inline_directive (@push_cast _ t e)) - = interpf interp_op e. - Proof using cast_val_squash interpf_Cast_id interpf_cast is_cast_correct. - unfold push_cast; break_innermost_match; simpl; try reflexivity. - match goal with H : _ |- _ => apply interpf_maybe_push_cast in H end. - assumption. - Qed. - - Local Hint Resolve interpf_exprf_of_push_cast. - - Lemma InterpInlineCast {t} e (Hwf : Wf e) - : forall x, - Interp interp_op (@InlineCast t e) x - = Interp interp_op e x. - Proof using cast_val_squash interpf_Cast_id interpf_cast is_cast_correct. apply InterpInlineConstGen; auto. Qed. -End language. - -Hint Rewrite @interpf_exprf_of_push_cast @InterpInlineCast using solve [ eassumption | eauto with wf ] : reflective_interp. diff --git a/src/Compilers/InlineCastWf.v b/src/Compilers/InlineCastWf.v deleted file mode 100644 index f2d3cc84f..000000000 --- a/src/Compilers/InlineCastWf.v +++ /dev/null @@ -1,131 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.TypeInversion. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Compilers.WfInversion. -Require Import Crypto.Compilers.InlineCast. -Require Import Crypto.Compilers.InlineWf. -Require Import Crypto.Compilers.SmartCast. -Require Import Crypto.Compilers.SmartCastWf. -Require Import Crypto.Compilers.Inline. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Notations. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (is_cast : forall src dst, op src dst -> bool) - (is_const : forall src dst, op src dst -> bool) - (wff_Cast : forall var1 var2 G A A' e1 e2, - wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)). - Local Infix "<=?" := base_type_leb : expr_scope. - Local Infix "=?" := base_type_beq : expr_scope. - - Local Notation SmartCast_base := (@SmartCast_base _ op _ base_type_bl_transparent Cast). - Local Notation squash_cast := (@squash_cast _ op _ base_type_bl_transparent base_type_leb Cast). - Local Notation maybe_push_cast := (@maybe_push_cast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const). - Local Notation push_cast := (@push_cast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const). - Local Notation InlineCast := (@InlineCast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const). - - Lemma wff_squash_cast var1 var2 a b c e1 e2 G - (Hwf : wff G e1 e2) - : wff G (@squash_cast var1 a b c e1) (@squash_cast var2 a b c e2). - Proof using wff_Cast. - unfold squash_cast; break_innermost_match; auto with wf. - Qed. - - Local Opaque InlineCast.squash_cast. - - Lemma wff_maybe_push_cast_match {var1 var2 t e1 e2 G} - (Hwf : wff G e1 e2) - : match @maybe_push_cast var1 t e1, @maybe_push_cast var2 t e2 with - | Some e1', Some e2' => wff G e1' e2' - | None, None => True - | Some _, None | None, Some _ => False - end. - Proof using wff_Cast. - induction Hwf; - repeat match goal with - | [ |- wff _ (squash_cast _ _ _ _) (squash_cast _ _ _ _) ] - => apply wff_squash_cast - | _ => progress subst - | _ => progress destruct_head' sig - | _ => progress destruct_head' and - | _ => progress inversion_option - | _ => progress simpl in * - | _ => congruence - | _ => progress break_innermost_match_step - | _ => intro - | [ H : forall e1 e2, Some _ = Some e1 -> _ |- _ ] - => specialize (fun e2 => H _ e2 eq_refl) - | [ H : forall e, Some _ = Some e -> _ |- _ ] - => specialize (H _ eq_refl) - | _ => solve [ auto with wf ] - | _ => progress inversion_wf_constr - | _ => progress inversion_flat_type - | [ H : context[match ?e with _ => _ end] |- _ ] => invert_one_expr e - | [ |- context[match ?e with _ => _ end] ] => invert_one_expr e - end. - Qed. - - Lemma wff_maybe_push_cast var1 var2 t e1 e2 G e1' e2' - (Hwf : wff G e1 e2) - : @maybe_push_cast var1 t e1 = Some e1' - -> @maybe_push_cast var2 t e2 = Some e2' - -> wff G e1' e2'. - Proof using wff_Cast. - intros H0 H1; eapply wff_maybe_push_cast_match in Hwf. - rewrite H0, H1 in Hwf; assumption. - Qed. - - Local Notation wff_inline_directive G x y := - (wff G (exprf_of_inline_directive x) (exprf_of_inline_directive y) - /\ (fun x' y' - => match x', y' with - | default_inline _ _, default_inline _ _ - | no_inline _ _, no_inline _ _ - | inline _ _, inline _ _ - => True - | default_inline _ _, _ - | no_inline _ _, _ - | inline _ _, _ - => False - end) x y). - - Lemma wff_push_cast var1 var2 t e1 e2 G - (Hwf : wff G e1 e2) - : wff_inline_directive G (@push_cast var1 t e1) (@push_cast var2 t e2). - Proof using wff_Cast. - pose proof (wff_maybe_push_cast_match Hwf). - unfold push_cast; destruct t; - break_innermost_match; - repeat first [ apply conj - | exact I - | progress simpl in * - | exfalso; assumption - | assumption ]. - Qed. - - Lemma wff_exprf_of_push_cast var1 var2 t e1 e2 G - (Hwf : wff G e1 e2) - : wff G - (exprf_of_inline_directive (@push_cast var1 t e1)) - (exprf_of_inline_directive (@push_cast var2 t e2)). - Proof using wff_Cast. apply wff_push_cast; assumption. Qed. - - Local Hint Resolve wff_push_cast. - - Lemma Wf_InlineCast {t} e (Hwf : Wf e) - : Wf (@InlineCast t e). - Proof using wff_Cast. apply Wf_InlineConstGen; auto. Qed. -End language. - -Hint Resolve Wf_InlineCast : wf. diff --git a/src/Compilers/MapCast.v b/src/Compilers/MapCast.v deleted file mode 100644 index 0cb453b00..000000000 --- a/src/Compilers/MapCast.v +++ /dev/null @@ -1,105 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Option. - -Local Open Scope ctype_scope. -Local Open Scope expr_scope. -Section language. - Context {base_type_code1 base_type_code2 : Type} - {interp_base_type2 : 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} - (interp_op2 : forall src dst, op2 src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst) - (failv : forall {var t}, @exprf base_type_code1 op1 var (Tbase t)). - Context (transfer_op : forall ovar src1 dst1 src2 dst2 - (opc1 : op1 src1 dst1) - (opc2 : op2 src2 dst2) - (args1' : @exprf base_type_code1 op1 ovar src1) - (args2 : interp_flat_type interp_base_type2 src2), - @exprf base_type_code1 op1 ovar dst1). - - - Section with_var. - Context {ovar : base_type_code1 -> Type}. - Local Notation SmartFail - := (SmartValf _ (@failv _)). - Local Notation failf t (* {t} : @exprf base_type_code1 op1 ovar t*) - := (SmartPairf (SmartFail t)). - - (** We only ever make use of this when [e1] and [e2] are the same - type, and, in fact, the same syntax tree instantiated to - different [var] arguments. However, if we make - [mapf_interp_cast] homogenous (force [t1] and [t2] to be - judgmentally equal), then we run into trouble in the recursive - calls in the [LetIn] and [Op] cases; we'd need to have - evidence that they are the same (such as a (transparent!) - well-foundedness proof), or a decider of type equality with - transparent proofs that we can cast across. - - Rather than asking for either of these, we take the simpler - route of allowing expression trees of different types, and - failing ([failf]) or falling back to default behavior (as in - the [TT] and [Var] cases) when things don't match. - - Allowing two different [base_type_code]s and [op] types is - unnecessary, and they could be collapsed. The extra - generalization costs little in lines-of-code, though, so I've - left it in. *) - Fixpoint mapf_interp_cast - {t1} (e1 : @exprf base_type_code1 op1 ovar t1) - {t2} (e2 : @exprf base_type_code2 op2 interp_base_type2 t2) - {struct e1} - : @exprf base_type_code1 op1 ovar t1 - := match e1 in exprf _ _ t1, e2 as e2 in exprf _ _ t2 - return exprf _ _ (var:=ovar) t1 with - | TT as e1', _ - | Var _ _ as e1', _ - => e1' - | Pair tx1 ex1 ty1 ey1, Pair tx2 ex2 ty2 ey2 - => Pair - (@mapf_interp_cast _ ex1 _ ex2) - (@mapf_interp_cast _ ey1 _ ey2) - | Op _ tR1 op1 args1, Op _ tR2 op2 args2 - => let args' := @mapf_interp_cast _ args1 _ args2 in - transfer_op _ _ _ _ _ op1 op2 args' (interpf interp_op2 args2) - | LetIn tx1 ex1 tC1 eC1, LetIn tx2 ex2 tC2 eC2 - => let ex' := @mapf_interp_cast _ ex1 _ ex2 in - let eC' := fun v' => @mapf_interp_cast _ (eC1 v') _ (eC2 (interpf interp_op2 ex2)) in - LetIn ex' eC' - | Op _ _ _ _, _ - | LetIn _ _ _ _, _ - | Pair _ _ _ _, _ - => @failf _ - end. - Arguments mapf_interp_cast {_} _ {_} _. (* 8.4 workaround for bad arguments *) - - Definition map_interp_cast - {t1} (e1 : @expr base_type_code1 op1 ovar t1) - {t2} (e2 : @expr base_type_code2 op2 interp_base_type2 t2) - (args2 : interp_flat_type interp_base_type2 (domain t2)) - : @expr base_type_code1 op1 ovar (Arrow (domain t1) (codomain t1)) - := let f1 := invert_Abs e1 in - let f2 := invert_Abs e2 in - Abs (fun x => @mapf_interp_cast _ (f1 x) _ (f2 args2)). - End with_var. -End language. - -Global Arguments mapf_interp_cast {_ _ _ _ _} interp_op2 failv transfer_op {ovar} {t1} e1 {t2} e2. -Global Arguments map_interp_cast {_ _ _ _ _} interp_op2 failv transfer_op {ovar} {t1} e1 {t2} e2 args2. - -Section homogenous. - Context {base_type_code : Type} - {interp_base_type2 : base_type_code -> Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (interp_op2 : forall src dst, op src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst) - (failv : forall {var t}, @exprf base_type_code op var (Tbase t)). - - Definition MapInterpCast - transfer_op - {t} (e : Expr base_type_code op t) (args : interp_flat_type interp_base_type2 (domain t)) - : Expr base_type_code op (Arrow (domain t) (codomain t)) - := fun var => map_interp_cast interp_op2 (@failv) transfer_op (e _) (e _) args. -End homogenous. diff --git a/src/Compilers/MapCastInterp.v b/src/Compilers/MapCastInterp.v deleted file mode 100644 index bbf4581b5..000000000 --- a/src/Compilers/MapCastInterp.v +++ /dev/null @@ -1,291 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Compilers.MapCast. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.WfProofs. -Require Import Crypto.Compilers.WfInversion. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.RewriteHyp. - -Local Open Scope ctype_scope. -Local Open Scope expr_scope. -Section language. - Context {base_type_code : Type} - {interp_base_type1 : base_type_code -> Type} - {interp_base_type2 : base_type_code -> Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (interp_op1 : forall src dst, op src dst -> interp_flat_type interp_base_type1 src -> interp_flat_type interp_base_type1 dst) - (interp_op2 : forall src dst, op src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst) - (failv : forall {var t}, @exprf base_type_code op var (Tbase t)). - Context (transfer_op : forall ovar src1 dst1 src2 dst2 - (opc1 : op src1 dst1) - (opc2 : op src2 dst2) - (args1' : @exprf base_type_code op ovar src1) - (args2 : interp_flat_type interp_base_type2 src2), - @exprf base_type_code op ovar dst1). - - Context (R' : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop). - Local Notation R x y := (interp_flat_type_rel_pointwise R' x y). - Section gen_Prop. - Context (P : Type) (and : P -> P -> P) (True : P). - Context (bound_is_good : forall t, interp_base_type2 t -> P). - Local Notation bounds_are_good - := (@interp_flat_type_rel_pointwise1_gen_Prop _ _ P and True bound_is_good _). - Fixpoint bounds_are_recursively_good_gen_Prop {t} (e : exprf base_type_code op t) : P - := match e with - | LetIn tx ex tC eC - => and (@bounds_are_recursively_good_gen_Prop tx ex) - (@bounds_are_recursively_good_gen_Prop tC (eC (interpf interp_op2 ex))) - | Op t1 tR opc args as e' - => and (@bounds_are_recursively_good_gen_Prop _ args) - (bounds_are_good (interpf interp_op2 e')) - | TT => True - | Var t v => bound_is_good _ v - | Pair tx ex ty ey - => and (@bounds_are_recursively_good_gen_Prop _ ex) - (@bounds_are_recursively_good_gen_Prop _ ey) - end. - End gen_Prop. - Definition bounds_are_recursively_goodb - := bounds_are_recursively_good_gen_Prop bool andb true. - Global Arguments bounds_are_recursively_goodb _ {_} !_ / . - Definition bounds_are_recursively_good - := @bounds_are_recursively_good_gen_Prop Prop and True. - Global Arguments bounds_are_recursively_good _ {_} !_ / . - Lemma bounds_are_recursively_good_iff_bool - R t x - : is_true (@bounds_are_recursively_goodb R t x) - <-> @bounds_are_recursively_good (fun t x => is_true (R t x)) t x. - Proof using Type. - unfold is_true. - clear; induction x; simpl in *; rewrite ?Bool.andb_true_iff; - try setoid_rewrite interp_flat_type_rel_pointwise1_gen_Prop_iff_bool; - rewrite_hyp ?*; intuition congruence. - Qed. - Definition bounds_are_recursively_good_gen_Prop_iff_bool - : forall R t x, - is_true (@bounds_are_recursively_good_gen_Prop bool _ _ R t x) - <-> @bounds_are_recursively_good_gen_Prop Prop _ _ (fun t x => is_true (R t x)) t x - := bounds_are_recursively_good_iff_bool. - - Context (bound_is_good : forall t, interp_base_type2 t -> Prop). - Local Notation bounds_are_good - := (@interp_flat_type_rel_pointwise1 _ _ bound_is_good). - Lemma bounds_are_good_when_recursively_good {t} e - : @bounds_are_recursively_good bound_is_good t e -> bounds_are_good (interpf interp_op2 e). - Proof using Type. - induction e; simpl; unfold LetIn.Let_In; intuition auto. - Qed. - Local Hint Resolve bounds_are_good_when_recursively_good. - - Local Notation G_invariant_holds G - := (forall t x x', - List.In (existT _ t (x, x')%core) G -> R' t x x') - (only parsing). - - Context (interpf_transfer_op - : forall G t tR opc ein eout ebounds, - wff G ein ebounds - -> G_invariant_holds G - -> interpf interp_op1 ein = interpf interp_op1 eout - -> bounds_are_recursively_good bound_is_good ebounds - -> bounds_are_good (interp_op2 t tR opc (interpf interp_op2 ebounds)) - -> interpf interp_op1 (transfer_op interp_base_type1 t tR t tR opc opc eout (interpf interp_op2 ebounds)) - = interpf interp_op1 (Op opc ein)). - - Context (R_transfer_op - : forall G t tR opc ein eout ebounds, - wff G ein ebounds - -> G_invariant_holds G - -> interpf interp_op1 ein = interpf interp_op1 eout - -> bounds_are_recursively_good bound_is_good ebounds - -> bounds_are_good (interp_op2 t tR opc (interpf interp_op2 ebounds)) - -> R (interpf interp_op1 (transfer_op interp_base_type1 t tR t tR opc opc eout (interpf interp_op2 ebounds))) - (interpf interp_op2 (Op opc ebounds))). - - Local Notation mapf_interp_cast - := (@mapf_interp_cast - base_type_code base_type_code interp_base_type2 - op op interp_op2 failv - transfer_op). - Local Notation map_interp_cast - := (@map_interp_cast - base_type_code base_type_code interp_base_type2 - op op interp_op2 failv - transfer_op). - Local Notation MapInterpCast - := (@MapInterpCast - base_type_code interp_base_type2 - op interp_op2 failv - transfer_op). - - (* Local *) Hint Resolve <- List.in_app_iff. - Local Hint Resolve (fun t T => @interp_flat_type_rel_pointwise_flatten_binding_list _ _ _ t T R'). - - Local Ltac break_t - := first [ progress subst - | progress inversion_wf - | progress invert_expr_subst - | progress inversion_sigma - | progress inversion_prod - | progress destruct_head sig - | progress destruct_head sigT - | progress destruct_head ex - | progress destruct_head and - | progress destruct_head prod - | progress split_and - | progress break_match_hyps ]. - - Local Ltac fin_False := - lazymatch goal with - | [ H : False |- _ ] => exfalso; assumption - end. - - Local Ltac fin_t0 := - solve [ constructor; eauto - | eauto - | auto - | hnf; auto ]. - - Local Ltac handle_list_t := - match goal with - | _ => progress cbv [LetIn.Let_In duplicate_types] in * - | [ H : List.In _ (_ ++ _) |- _ ] => apply List.in_app_or in H - | [ H : List.In _ (List.map _ _) |- _ ] - => rewrite List.in_map_iff in H - | _ => rewrite <- flatten_binding_list_flatten_binding_list2 - | [ H : appcontext[flatten_binding_list2] |- _ ] - => rewrite <- flatten_binding_list_flatten_binding_list2 in H - | [ H : context[flatten_binding_list (SmartVarfMap _ _) (SmartVarfMap _ _)] |- _ ] - => rewrite flatten_binding_list_SmartVarfMap in H - | [ H : context[flatten_binding_list2 (SmartVarfMap _ _) (SmartVarfMap _ _)] |- _ ] - => rewrite flatten_binding_list2_SmartVarfMap in H - | [ H : context[flatten_binding_list2 (SmartVarfMap _ _) _] |- _ ] - => rewrite flatten_binding_list2_SmartVarfMap1 in H - | [ H : context[flatten_binding_list2 _ (SmartVarfMap _ _)] |- _ ] - => rewrite flatten_binding_list2_SmartVarfMap2 in H - | _ => rewrite <- flatten_binding_list_flatten_binding_list2 - | _ => rewrite List.in_map_iff - | [ H : context[List.In _ (_ ++ _)] |- _ ] - => setoid_rewrite List.in_app_iff in H - end. - - Local Ltac wff_t := - match goal with - | [ |- wff _ _ _ ] => constructor - | [ H : _ |- wff _ (mapf_interp_cast _ _ _) (mapf_interp_cast _ _ _) ] - => eapply H; eauto; []; clear H - | _ => solve [ eauto using wff_in_impl_Proper ] - end. - - Local Ltac R_t := - match goal with - | [ |- R' _ _ _ ] => eapply interp_flat_type_rel_pointwise_flatten_binding_list; eauto - | [ H : forall x y, _ -> R _ _ |- R _ _ ] => apply H; eauto; [] - | [ H : forall x y, _ -> _ -> R _ _ |- R _ _ ] => apply H; eauto; [] - end. - - Local Ltac misc_t := - match goal with - | _ => progress specialize_by eauto - | [ |- exists _, _ ] - => eexists (existT _ _ _) - | [ |- _ /\ _ ] => split - | [ H : _ = _ |- _ ] => rewrite H - | [ H : ?x = _, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : forall x y, _ -> _ -> _ = _ |- interpf _ _ = interpf _ _ ] - => apply H - end. - - Local Ltac t_step := - first [ intro - | fin_False - | progress break_t - | fin_t0 - | progress simpl in * - | wff_t - | handle_list_t - | progress destruct_head' or - | misc_t - | R_t ]. - - Lemma interpf_mapf_interp_cast_and_rel - G - {t1} e1 ebounds - (Hgood : bounds_are_recursively_good bound_is_good ebounds) - (HG : G_invariant_holds G) - (Hwf : wff G e1 ebounds) - : interpf interp_op1 (@mapf_interp_cast interp_base_type1 t1 e1 t1 ebounds) - = interpf interp_op1 e1 - /\ R (interpf interp_op1 (@mapf_interp_cast interp_base_type1 t1 e1 t1 ebounds)) - (interpf interp_op2 ebounds). - Proof using R_transfer_op interpf_transfer_op. induction Hwf; repeat t_step. Qed. - - Local Hint Resolve interpf_mapf_interp_cast_and_rel. - - Lemma interpf_mapf_interp_cast - G - {t1} e1 ebounds - (Hgood : bounds_are_recursively_good bound_is_good ebounds) - (HG : G_invariant_holds G) - (Hwf : wff G e1 ebounds) - : interpf interp_op1 (@mapf_interp_cast interp_base_type1 t1 e1 t1 ebounds) - = interpf interp_op1 e1. - Proof using R_transfer_op interpf_transfer_op. eapply interpf_mapf_interp_cast_and_rel; eassumption. Qed. - - Lemma interp_map_interp_cast_and_rel - {t1} e1 ebounds - args2 - (Hgood : bounds_are_recursively_good bound_is_good (invert_Abs ebounds args2)) - (Hwf : wf e1 ebounds) - : forall x, - R x args2 - -> interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x - = interp interp_op1 e1 x - /\ R (interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x) - (interp interp_op2 ebounds args2). - Proof using R_transfer_op interpf_transfer_op. destruct Hwf; intros; eapply interpf_mapf_interp_cast_and_rel; eauto. Qed. - - Lemma interp_map_interp_cast - {t1} e1 ebounds - args2 - (Hgood : bounds_are_recursively_good bound_is_good (invert_Abs ebounds args2)) - (Hwf : wf e1 ebounds) - : forall x, - R x args2 - -> interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x - = interp interp_op1 e1 x. - Proof using R_transfer_op interpf_transfer_op. intros; eapply interp_map_interp_cast_and_rel; eassumption. Qed. - - Lemma InterpMapInterpCastAndRel - {t} e - args - (Hwf : Wf e) - (Hgood : bounds_are_recursively_good bound_is_good (invert_Abs (e interp_base_type2) args)) - : forall x, - R x args - -> Interp interp_op1 (@MapInterpCast t e args) x - = Interp interp_op1 e x - /\ R (Interp interp_op1 (@MapInterpCast t e args) x) - (Interp interp_op2 e args). - Proof using R_transfer_op interpf_transfer_op. apply interp_map_interp_cast_and_rel; auto. Qed. - - Lemma InterpMapInterpCast - {t} e - args - (Hwf : Wf e) - (Hgood : bounds_are_recursively_good bound_is_good (invert_Abs (e interp_base_type2) args)) - : forall x, - R x args - -> Interp interp_op1 (@MapInterpCast t e args) x - = Interp interp_op1 e x. - Proof using R_transfer_op interpf_transfer_op. apply interp_map_interp_cast; auto. Qed. -End language. diff --git a/src/Compilers/MapCastWf.v b/src/Compilers/MapCastWf.v deleted file mode 100644 index 2961b9426..000000000 --- a/src/Compilers/MapCastWf.v +++ /dev/null @@ -1,172 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Compilers.MapCast. -Require Import Crypto.Compilers.WfProofs. -Require Import Crypto.Compilers.WfInversion. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. - -Local Open Scope ctype_scope. -Local Open Scope expr_scope. -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} - (interp_op2 : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst) - (failv : forall {var t}, @exprf base_type_code op var (Tbase t)). - Context (transfer_op : forall ovar src1 dst1 src2 dst2 - (opc1 : op src1 dst1) - (opc2 : op src2 dst2) - (args1' : @exprf base_type_code op ovar src1) - (args2 : interp_flat_type interp_base_type src2), - @exprf base_type_code op ovar dst1). - - Local Notation interp_flat_type_ivarf_wff G a b - := (forall t x y, - List.In (existT _ t (x, y)%core) (flatten_binding_list a b) - -> wff G x y) - (only parsing). - - Section with_var. - Context {ovar1 ovar2 : base_type_code -> Type}. - - Context (wff_transfer_op - : forall G src1 dst1 src2 dst2 opc1 opc2 args1 args1' args2, - wff G (var1:=ovar1) (var2:=ovar2) args1 args1' - -> wff G - (@transfer_op ovar1 src1 dst1 src2 dst2 opc1 opc2 args1 args2) - (@transfer_op ovar2 src1 dst1 src2 dst2 opc1 opc2 args1' args2)). - Local Notation mapf_interp_cast - := (@mapf_interp_cast - base_type_code base_type_code interp_base_type - op op interp_op2 failv - transfer_op). - Local Notation map_interp_cast - := (@map_interp_cast - base_type_code base_type_code interp_base_type - op op interp_op2 failv - transfer_op). - - Local Notation G1eTf - := (fun t : base_type_code => interp_flat_type ovar1 (Tbase t) * interp_flat_type ovar2 (Tbase t))%type. - Local Notation G2eTf - := (fun t : base_type_code => ovar1 t * ovar2 t)%type. - Local Notation GbeTf - := (fun t : base_type_code => interp_flat_type ovar1 (Tbase t) * interp_base_type t)%type. - - (* Definition Gse_related' {t} (G1e : G1eTf t) (Gbe : GbeTf t) (G2e G2eTf t) : Prop - := fst G1e = fst Gbe /\ - - := exists (pf1 : projT1 G1e = projT1 G2e - - Definition Gse_related (G1e : sigT G1eTf) (G2e : sigT G2eTf) (G3e : sigT G3eTf) : Prop - := exists (pf1 : projT1 G1e = projT1 G2e - /\ - - Local Notation G3eT - := {t : base_type_code & - ((interp_flat_type ivarf1 (Tbase t) * interp_flat_type ivarf2 (Tbase t)) - * (ovar1 t * ovar2 t) - * interp_base_type t)%type }. - Local Notation G3T - := (list G3eT). - - Definition G3e_to_G1e - - *) - (* Local *) Hint Resolve <- List.in_app_iff. - - Local Ltac break_t - := first [ progress subst - | progress inversion_wf - | progress invert_expr_subst - | progress inversion_sigma - | progress inversion_prod - | progress destruct_head sig - | progress destruct_head sigT - | progress destruct_head ex - | progress destruct_head and - | progress destruct_head prod - | progress break_match_hyps ]. - - Lemma wff_mapf_interp_cast - G1 Gbounds - {t1} e1 e2 ebounds - (Hwf_bounds : wff Gbounds e1 ebounds) - (Hwf : wff G1 e1 e2) - : wff G1 - (@mapf_interp_cast ovar1 t1 e1 t1 ebounds) - (@mapf_interp_cast ovar2 t1 e2 t1 ebounds). - Proof using wff_transfer_op. - revert dependent Gbounds; revert ebounds; - induction Hwf; - repeat match goal with - | _ => solve [ exfalso; assumption ] - | _ => intro - | _ => progress break_t - | _ => solve [ constructor; eauto - | eauto - | auto - | hnf; auto ] - | _ => progress simpl in * - | [ H : List.In _ (_ ++ _) |- _ ] => apply List.in_app_or in H - | _ => progress destruct_head or - | [ |- wff _ _ _ ] => constructor - | [ H : _ |- wff _ (mapf_interp_cast _ _ _ _) (mapf_interp_cast _ _ _ _) ] - => eapply H; eauto; []; clear H - | _ => solve [ eauto using wff_SmartVarf, wff_in_impl_Proper ] - end. - Qed. - - Lemma wf_map_interp_cast - {t1} e1 e2 ebounds - args2 - (Hwf_bounds : wf e1 ebounds) - (Hwf : wf e1 e2) - : wf (@map_interp_cast ovar1 t1 e1 t1 ebounds args2) - (@map_interp_cast ovar2 t1 e2 t1 ebounds args2). - Proof using wff_transfer_op. - destruct Hwf; - repeat match goal with - | _ => solve [ constructor; eauto - | eauto using wff_mapf_interp_cast - | exfalso; assumption ] - | _ => intro - | _ => progress break_t - | [ |- wf _ _ ] => constructor - | _ => solve [ eauto using wff_SmartVarf, wff_in_impl_Proper ] - end. - Qed. - End with_var. - - Section gen. - Context (wff_transfer_op - : forall ovar1 ovar2 G src1 dst1 src2 dst2 opc1 opc2 e1 e2 args2, - wff G (var1:=ovar1) (var2:=ovar2) e1 e2 - -> wff G - (@transfer_op ovar1 src1 dst1 src2 dst2 opc1 opc2 e1 args2) - (@transfer_op ovar2 src1 dst1 src2 dst2 opc1 opc2 e2 args2)). - - Local Notation MapInterpCast - := (@MapInterpCast - base_type_code interp_base_type - op interp_op2 failv - transfer_op). - - Lemma Wf_MapInterpCast - {t} e - args - (Hwf : Wf e) - : Wf (@MapInterpCast t e args). - Proof using wff_transfer_op. - intros ??; apply wf_map_interp_cast; auto. - Qed. - End gen. -End language. - -Hint Resolve Wf_MapInterpCast : wf. diff --git a/src/Compilers/MultiSizeTest2.v b/src/Compilers/MultiSizeTest2.v deleted file mode 100644 index eac196510..000000000 --- a/src/Compilers/MultiSizeTest2.v +++ /dev/null @@ -1,183 +0,0 @@ -Require Import Coq.omega.Omega. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.BoundByCast. - -(** * Preliminaries: bounded and unbounded number types *) - -Definition bound8 := 256. - -Definition word8 := {n | n < bound8}. - -Definition bound9 := 512. - -Definition word9 := {n | n < bound9}. - - -(** * Expressions over unbounded words *) - -Inductive base_type := Nat | Word8 | Word9. -Scheme Equality for base_type. -Definition interp_base_type (t : base_type) - := match t with - | Nat => nat - | Word8 => word8 - | Word9 => word9 - end. -Definition interp_base_type_bounds (t : base_type) - := nat. -Definition base_type_leb (x y : base_type) : bool - := match x, y with - | Word8, _ => true - | _, Word8 => false - | Word9, _ => true - | _, Word9 => false - | Nat, Nat => true - end. -Local Notation TNat := (Tbase Nat). -Local Notation TWord8 := (Tbase Word8). -Local Notation TWord9 := (Tbase Word9). -Inductive op : flat_type base_type -> flat_type base_type -> Set := -| Const {t} (v : interp_base_type t) : op Unit (Tbase t) -| Plus (t : base_type) : op (Tbase t * Tbase t) (Tbase t) -| Cast (t1 t2 : base_type) : op (Tbase t1) (Tbase t2). - -Definition is_cast src dst (opc : op src dst) : bool - := match opc with Cast _ _ => true | _ => false end. -Definition is_const src dst (opc : op src dst) : bool - := match opc with Const _ _ => true | _ => false end. - -Definition genericize_op src dst (opc : op src dst) (new_t_in new_t_out : base_type) - : option { src'dst' : _ & op (fst src'dst') (snd src'dst') } - := match opc with - | Plus _ => Some (existT _ (_, _) (Plus (base_type_max base_type_leb new_t_in new_t_out))) - | Const _ _ - | Cast _ _ - => None - end. - -Definition Constf {var} {t} (v : interp_base_type t) : exprf base_type op (var:=var) (Tbase t) - := Op (Const v) TT. - -Theorem O_lt_S : forall n, O < S n. -Proof. - intros; omega. -Qed. - -Definition plus8 (a b : word8) : word8 := - let n := proj1_sig a + proj1_sig b in - match le_lt_dec bound8 n with - | left _ => exist _ O (O_lt_S _) - | right pf => exist _ n pf - end. - -Definition plus9 (a b : word9) : word9 := - let n := proj1_sig a + proj1_sig b in - match le_lt_dec bound9 n with - | left _ => exist _ O (O_lt_S _) - | right pf => exist _ n pf - end. - -Infix "+8" := plus8 (at level 50). -Infix "+9" := plus9 (at level 50). - -Definition unbound {t} : interp_base_type t -> nat := - match t with - | Nat => fun x => x - | Word8 => fun x => proj1_sig x - | Word9 => fun x => proj1_sig x - end. - -Definition bound {t} : nat -> interp_base_type t := - match t return nat -> interp_base_type t with - | Nat => fun x => x - | Word8 => fun x => - match le_lt_dec bound8 x with - | left _ => exist _ O (O_lt_S _) - | right pf => exist _ x pf - end - | Word9 => fun x => - match le_lt_dec bound9 x with - | left _ => exist _ O (O_lt_S _) - | right pf => exist _ x pf - end - end. - -Definition interp_op {src dst} (opc : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst - := match opc in op src dst return interp_flat_type _ src -> interp_flat_type _ dst with - | Const _ v => fun _ => v - | Plus Nat => fun xy => fst xy + snd xy - | Plus Word8 => fun xy => fst xy +8 snd xy - | Plus Word9 => fun xy => fst xy +9 snd xy - | Cast t1 t2 => fun x => bound (unbound x) - end. - -Definition interp_op_bounds {src dst} (opc : op src dst) : interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst - := match opc in op src dst return interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst with - | Const _ v => fun _ => unbound v - | Plus _ => fun xy => fst xy + snd xy - | Cast t1 t2 => fun x => x - end. - -Definition bound_type t (v : interp_base_type_bounds t) : base_type - := if lt_dec v bound8 - then Word8 - else if lt_dec v bound9 - then Word9 - else Nat. - -Definition failv t : interp_base_type t - := match t with - | Nat => 0 - | Word8 => exist _ 0 (O_lt_S _) - | Word9 => exist _ 0 (O_lt_S _) - end. - -Definition failf var t : @exprf base_type op var (Tbase t) - := Op (Const (failv t)) TT. - -Definition Boundify {t1} (e1 : Expr base_type op t1) args2 - : Expr _ _ _ - := @Boundify - base_type op interp_base_type_bounds (@interp_op_bounds) - bound_type base_type_beq internal_base_type_dec_bl - base_type_leb - (fun var A A' => Op (Cast A A')) - is_cast - is_const - genericize_op - (@failf) - t1 e1 args2. - -(** * Examples *) - -Example ex1 : Expr base_type op (Arrow Unit TNat) := fun var => - Abs (fun _ => - LetIn (Constf (t:=Nat) 127) (fun a : var Nat => - LetIn (Constf (t:=Nat) 63) (fun b : var Nat => - LetIn (Op (tR:=TNat) (Plus Nat) (Pair (Var a) (Var b))) (fun c : var Nat => - Op (Plus Nat) (Pair (Var c) (Var c)))))). - -(* -Example ex1f : Expr base_type op (Arrow (TNat * TNat) TNat) := fun var => - Abs (fun a0b0 : interp_flat_type _ (TNat * TNat) => - let a0 := fst a0b0 in let b0 := snd a0b0 in - LetIn (Var a0) (fun a : var Nat => - LetIn (Var b0) (fun b : var Nat => - LetIn (Op (tR:=TNat) (Plus Nat) (Pair (Var a) (Var b))) (fun c : var Nat => - Op (Plus Nat) (Pair (Var c) (Var c)))))). - -Eval compute in (Interp (@interp_op) ex1). -Eval cbv -[plus] in (Interp (@interp_op) ex1f). - -Notation e x := (exist _ x _). - -Definition ex1b := Boundify ex1 tt. -Eval compute in ex1b. - -Definition ex1fb := Boundify ex1f (63, 63)%core. -Eval compute in ex1fb. - -Definition ex1fb' := Boundify ex1f (64, 64)%core. -Eval compute in ex1fb'. -*)
\ No newline at end of file diff --git a/src/Compilers/SmartBound.v b/src/Compilers/SmartBound.v deleted file mode 100644 index 39fd34dd7..000000000 --- a/src/Compilers/SmartBound.v +++ /dev/null @@ -1,135 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.SmartCast. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Util.Notations. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> 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) - (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), - option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) - (failf : forall var t, @exprf base_type_code op var (Tbase t)). - Local Infix "<=?" := base_type_leb : expr_scope. - Local Infix "=?" := base_type_beq : expr_scope. - - Local Notation flat_type_max := (flat_type_max base_type_leb). - Local Notation SmartCast := (@SmartCast _ op _ base_type_bl_transparent Cast). - - 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). - Local Notation Expr := (@Expr base_type_code op). - - Definition bound_flat_type {t} : interp_flat_type interp_base_type_bounds t - -> flat_type - := @SmartFlatTypeMap _ interp_base_type_bounds (fun t v => bound_base_type t v) t. - Definition bound_type {t} - (e_bounds : interp_type interp_base_type_bounds t) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - : type - := Arrow (@bound_flat_type (domain t) input_bounds) - (@bound_flat_type (codomain t) (e_bounds input_bounds)). - Definition bound_op - ovar src1 dst1 src2 dst2 (opc1 : op src1 dst1) (opc2 : op src2 dst2) - : exprf (var:=ovar) src1 - -> interp_flat_type interp_base_type_bounds src2 - -> exprf (var:=ovar) dst1 - := fun args input_bounds - => let output_bounds := interp_op_bounds _ _ opc2 input_bounds in - let input_ts := SmartVarfMap bound_base_type input_bounds in - let output_ts := SmartVarfMap bound_base_type output_bounds in - let new_type_in := flat_type_max input_ts in - let new_type_out := flat_type_max output_ts in - let new_opc := match new_type_in, new_type_out with - | Some new_type_in, Some new_type_out - => genericize_op _ _ opc1 new_type_in new_type_out - | None, _ | _, None => None - end in - match new_opc with - | Some (existT _ new_opc) - => match SmartCast _ _, SmartCast _ _ with - | Some SmartCast_args, Some SmartCast_result - => LetIn args - (fun args - => LetIn (Op new_opc (SmartCast_args args)) - (fun opv => SmartCast_result opv)) - | None, _ - | _, None - => Op opc1 args - end - | None - => Op opc1 args - end. - - Section smart_bound. - Definition interpf_smart_bound_exprf {var t} - (e : interp_flat_type var t) (bounds : interp_flat_type interp_base_type_bounds t) - : interp_flat_type (fun t => exprf (var:=var) (Tbase t)) (bound_flat_type bounds) - := SmartFlatTypeMap2Interp2 - (f:=fun t v => Tbase _) - (fun t bs v => Cast _ t (bound_base_type t bs) (Var v)) - bounds e. - Definition interpf_smart_unbound_exprf {var t} - (bounds : interp_flat_type interp_base_type_bounds t) - (e : interp_flat_type (fun t => exprf (var:=var) (Tbase t)) (bound_flat_type bounds)) - : interp_flat_type (fun t => @exprf var (Tbase t)) t - := SmartFlatTypeMapUnInterp2 - (f:=fun t v => Tbase (bound_base_type t _)) - (fun t bs v => Cast _ (bound_base_type t bs) t v) - e. - - Definition interpf_smart_bound - {interp_base_type} - (cast_val : forall A A', interp_base_type A -> interp_base_type A') - {t} - (e : interp_flat_type interp_base_type t) - (bounds : interp_flat_type interp_base_type_bounds t) - : interp_flat_type interp_base_type (bound_flat_type bounds) - := SmartFlatTypeMap2Interp2 - (f:=fun t v => Tbase _) - (fun t bs v => cast_val t (bound_base_type t bs) v) - bounds e. - Definition interpf_smart_unbound - {interp_base_type} - (cast_val : forall A A', interp_base_type A -> interp_base_type A') - {t} - (bounds : interp_flat_type interp_base_type_bounds t) - (e : interp_flat_type interp_base_type (bound_flat_type bounds)) - : interp_flat_type interp_base_type t - := SmartFlatTypeMapUnInterp2 (f:=fun _ _ => Tbase _) (fun t b v => cast_val _ _ v) e. - - Definition smart_boundf {var t1} (e1 : exprf (var:=var) t1) (bounds : interp_flat_type interp_base_type_bounds t1) - : exprf (var:=var) (bound_flat_type bounds) - := LetIn e1 (fun e1' => SmartPairf (var:=var) (interpf_smart_bound_exprf e1' bounds)). - Definition smart_bound {var t1} (e1 : expr (var:=var) t1) - (e_bounds : interp_type interp_base_type_bounds t1) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t1)) - : expr (var:=var) (bound_type e_bounds input_bounds) - := Abs - (fun args - => LetIn - (SmartPairf (interpf_smart_unbound_exprf input_bounds (SmartVarfMap (fun _ => Var) args))) - (fun v => smart_boundf - (invert_Abs e1 v) - (e_bounds input_bounds))). - Definition SmartBound {t1} (e : Expr t1) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t1)) - : Expr (bound_type _ input_bounds) - := fun var => smart_bound (e var) (interp (@interp_op_bounds) (e _)) input_bounds. - End smart_bound. -End language. - -Global Arguments bound_flat_type _ _ _ !_ _ / . -Global Arguments bound_type _ _ _ !_ _ _ / . diff --git a/src/Compilers/SmartBoundInterp.v b/src/Compilers/SmartBoundInterp.v deleted file mode 100644 index bd43f36a8..000000000 --- a/src/Compilers/SmartBoundInterp.v +++ /dev/null @@ -1,144 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.InterpWfRel. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.SmartMap. -(*Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.BoundByCast.*) -Require Import Crypto.Compilers.SmartBound. -Require Import Crypto.Compilers.ExprInversion. -(*Require Import Crypto.Compilers.SmartBoundWf. -Require Import Crypto.Compilers.InlineCastInterp. -Require Import Crypto.Compilers.InlineInterp. -Require Import Crypto.Compilers.LinearizeInterp. -Require Import Crypto.Compilers.LinearizeWf. -Require Import Crypto.Compilers.MapCastInterp. -Require Import Crypto.Compilers.MapCastWf. -Require Import Crypto.Compilers.EtaInterp.*) -Require Import Crypto.Util.Tactics.DestructHead. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (interp_base_type interp_base_type_bounds : 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) - (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) - (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (cast_val : forall A A', interp_base_type A -> interp_base_type A') - (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), - option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) - (failf : forall var t, @exprf base_type_code op var (Tbase t)) - (is_bounded_by_base : forall t, interp_base_type t -> interp_base_type_bounds t -> Prop) - (interpf_cast : forall A A' e, interpf interp_op (Cast _ A A' e) = cast_val A A' (interpf interp_op e)) - (strip_cast_val - : forall t x y, - is_bounded_by_base t y x -> - cast_val (bound_base_type t x) t (cast_val t (bound_base_type t x) y) = y). -(* - (wff_Cast : forall var1 var2 G A A' e1 e2, - wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)).*) - - Local Notation is_bounded_by (*{T} : interp_flat_type interp_base_type T -> interp_flat_type interp_base_type_bounds T -> Prop*) - := (interp_flat_type_rel_pointwise is_bounded_by_base). - Context (is_bounded_by_interp_op - : forall src dst opc sv1 sv2, - is_bounded_by sv1 sv2 -> - is_bounded_by (interp_op src dst opc sv1) (interp_op_bounds src dst opc sv2)). - Local Notation Expr := (@Expr base_type_code op). - Local Notation expr := (@expr base_type_code op). - Local Notation exprf := (@exprf base_type_code op). - Local Notation SmartBound := (@SmartBound _ _ _ interp_op_bounds bound_base_type Cast). - Local Notation smart_bound := (@smart_bound _ _ interp_base_type_bounds bound_base_type Cast). - Local Notation interpf_smart_bound := (@interpf_smart_bound _ interp_base_type_bounds bound_base_type interp_base_type cast_val). - Local Notation interpf_smart_unbound := (@interpf_smart_unbound _ interp_base_type_bounds bound_base_type interp_base_type cast_val). - Local Notation interpf_smart_bound_exprf := (@interpf_smart_bound_exprf _ op interp_base_type_bounds bound_base_type Cast). - Local Notation interpf_smart_unbound_exprf := (@interpf_smart_unbound_exprf _ op interp_base_type_bounds bound_base_type Cast). - Local Notation bound_op := (@bound_op _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast genericize_op). - - Local Ltac t := - unfold SmartPairf, SmartBound.interpf_smart_bound, SmartBound.interpf_smart_bound_exprf; - repeat first [ reflexivity - | progress destruct_head' unit - | progress simpl in * - | rewrite !interpf_cast - | match goal with H : _ |- _ => setoid_rewrite H end ]. - Lemma interpf_SmartPairf_interpf_smart_bound_exprf - {t} e bounds - : interpf interp_op (SmartPairf (interpf_smart_bound_exprf (t:=t) e bounds)) - = interpf_smart_bound e bounds. - Proof using interpf_cast. clear -interpf_cast; induction t; t. Qed. - - Lemma interpf_SmartPairf_interpf_smart_unbound_exprf - {t} bounds e - : interpf interp_op (SmartPairf (interpf_smart_unbound_exprf (t:=t) bounds e)) - = interpf_smart_unbound bounds (SmartVarfMap (fun _ e => interpf interp_op e) e). - Proof using interpf_cast. clear -interpf_cast; induction t; t. Qed. - - Lemma interp_smart_bound_and_rel {t} - (e : expr t) (ebounds : expr t) - (Hwf : wf e ebounds) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - (output_bounds := interp interp_op_bounds ebounds input_bounds) - (e' := smart_bound e (interp interp_op_bounds ebounds) input_bounds) - : forall x, - is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds - -> is_bounded_by (interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds - /\ interpf_smart_unbound _ (interp interp_op e' x) - = interp interp_op e (interpf_smart_unbound input_bounds x). - Proof using interpf_cast is_bounded_by_interp_op strip_cast_val. - intros; subst e' output_bounds. - match goal with |- ?A /\ ?B => cut (A /\ (A -> B)); [ tauto | ] end. - split. - { apply interp_wf; auto. } - { intro Hbounded_out. - unfold smart_bound; simpl. - cbv [LetIn.Let_In]. - rewrite interpf_invert_Abs, interpf_SmartPairf_interpf_smart_bound_exprf, interpf_SmartPairf_interpf_smart_unbound_exprf, SmartVarfMap_compose; simpl. - rewrite SmartVarfMap_id. - setoid_rewrite SmartFlatTypeMapUnInterp2_SmartFlatTypeMap2Interp2. - etransitivity; [ | eapply SmartVarfMap2_snd_arg ]. - apply lift_interp_flat_type_rel_pointwise_f_eq2. - eauto using interp_flat_type_rel_pointwise_impl', interp_flat_type_rel_pointwise_always. } - Qed. - - Lemma InterpSmartBoundAndRel {t} - (e : Expr t) - (Hwf : Wf e) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - (output_bounds := Interp interp_op_bounds e input_bounds) - (e' := SmartBound e input_bounds) - (*(Hgood : bounds_are_recursively_good - (@interp_op_bounds) bound_is_good - (invert_Abs (e _) input_bounds))*) - : forall x, - is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds - -> is_bounded_by (Interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds - /\ interpf_smart_unbound _ (Interp interp_op e' x) - = Interp interp_op e (interpf_smart_unbound input_bounds x). - Proof using interpf_cast is_bounded_by_interp_op strip_cast_val. - apply interp_smart_bound_and_rel; auto. - Qed. - - Lemma InterpSmartBound {t} - (e : Expr t) - (Hwf : Wf e) - (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - (output_bounds := Interp interp_op_bounds e input_bounds) - (e' := SmartBound e input_bounds) - (*(Hgood : bounds_are_recursively_good - (@interp_op_bounds) bound_is_good - (invert_Abs (e _) input_bounds))*) - : forall x, - is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds - -> interpf_smart_unbound _ (Interp interp_op e' x) - = Interp interp_op e (interpf_smart_unbound input_bounds x). - Proof using interpf_cast is_bounded_by_interp_op strip_cast_val. - intros; eapply InterpSmartBoundAndRel; auto. - Qed. -End language. diff --git a/src/Compilers/SmartBoundWf.v b/src/Compilers/SmartBoundWf.v deleted file mode 100644 index ae7f2c81f..000000000 --- a/src/Compilers/SmartBoundWf.v +++ /dev/null @@ -1,140 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.TypeInversion. -Require Import Crypto.Compilers.ExprInversion. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.WfProofs. -Require Import Crypto.Compilers.SmartBound. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.SmartCastWf. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Notations. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> 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) - (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (base_type_leb : base_type_code -> base_type_code -> bool) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), - option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) - (failf : forall var t, @exprf base_type_code op var (Tbase t)) - (wff_Cast : forall var1 var2 G A A' e1 e2, - wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)). - - Local Notation Expr := (@Expr base_type_code op). - Local Notation SmartBound := (@SmartBound _ _ _ interp_op_bounds bound_base_type Cast). - Local Notation smart_bound := (@smart_bound _ _ interp_base_type_bounds bound_base_type Cast). - Local Notation interpf_smart_bound_exprf := (@interpf_smart_bound_exprf _ op interp_base_type_bounds bound_base_type Cast). - Local Notation interpf_smart_unbound_exprf := (@interpf_smart_unbound_exprf _ op interp_base_type_bounds bound_base_type Cast). - Local Notation bound_op := (@bound_op _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast genericize_op). - Local Notation wff_SmartCast_match := (@wff_SmartCast_match _ op _ base_type_bl_transparent Cast wff_Cast). - - Local Hint Resolve List.in_or_app wff_in_impl_Proper. - - Lemma wff_bound_op - ovar1 ovar2 G src1 dst1 src2 dst2 opc1 opc2 e1 e2 args2 - (Hwf : wff G (var1:=ovar1) (var2:=ovar2) e1 e2) - : wff G - (@bound_op ovar1 src1 dst1 src2 dst2 opc1 opc2 e1 args2) - (@bound_op ovar2 src1 dst1 src2 dst2 opc1 opc2 e2 args2). - Proof using wff_Cast. - unfold SmartBound.bound_op; - repeat first [ progress break_innermost_match - | assumption - | constructor - | intro - | eapply wff_in_impl_Proper; [ eapply wff_SmartCast; eassumption | ] - | match goal with - | [ H0 : SmartCast.SmartCast _ _ _ ?x ?y = Some _, H1 : SmartCast.SmartCast _ _ _ ?x ?y = None |- _ ] - => let H := fresh in - refine (let H := wff_SmartCast_match x y in _); - erewrite H0, H1 in H; exfalso; exact H - end - | solve [ auto ] ]. - Qed. - - Local Hint Resolve List.in_app_or List.in_or_app. - - Lemma wff_SmartPairf_interpf_smart_unbound_exprf var1 var2 t input_bounds x1 x2 - : wff (flatten_binding_list x1 x2) - (SmartPairf - (var:=var1) - (interpf_smart_unbound_exprf input_bounds - (SmartVarfMap (fun t => Var) x1))) - (SmartPairf - (var:=var2) - (t:=t) - (interpf_smart_unbound_exprf input_bounds - (SmartVarfMap (fun t => Var) x2))). - Proof using wff_Cast. - clear -wff_Cast. - unfold SmartPairf, SmartVarfMap, interpf_smart_unbound_exprf; induction t; - repeat match goal with - | _ => progress simpl in * - | [ |- wff _ (Cast _ _ _ _) (Cast _ _ _ _) ] - => apply wff_Cast - | [ |- wff _ _ _ ] - => constructor - | _ => solve [ auto with wf ] - | _ => eapply wff_in_impl_Proper; [ solve [ eauto ] | ] - | _ => intro - end. - Qed. - - Local Hint Resolve wff_SmartPairf_interpf_smart_unbound_exprf : wf. - - Lemma wff_SmartPairf_interpf_smart_bound_exprf var1 var2 t x1 x2 output_bounds - : wff (flatten_binding_list x1 x2) - (SmartPairf - (var:=var1) - (interpf_smart_bound_exprf (t:=t) x1 output_bounds)) - (SmartPairf - (var:=var2) - (interpf_smart_bound_exprf x2 output_bounds)). - Proof using wff_Cast. - clear -wff_Cast. - unfold SmartPairf, SmartVarfMap, interpf_smart_bound_exprf; induction t; - repeat match goal with - | _ => progress simpl in * - | [ |- wff _ (Cast _ _ _ _) (Cast _ _ _ _) ] - => apply wff_Cast - | [ |- wff _ _ _ ] - => constructor - | _ => solve [ auto with wf ] - | _ => eapply wff_in_impl_Proper; [ solve [ eauto ] | ] - | _ => intro - end. - Qed. - - Local Hint Resolve wff_SmartPairf_interpf_smart_bound_exprf : wf. - - Lemma wf_smart_bound {var1 var2 t1} e1 e2 e_bounds input_bounds - (Hwf : wf e1 e2) - : wf (@smart_bound var1 t1 e1 e_bounds input_bounds) - (@smart_bound var2 t1 e2 e_bounds input_bounds). - Proof using wff_Cast. - clear -wff_Cast Hwf. - destruct Hwf; unfold SmartBound.smart_bound. - repeat constructor; auto with wf; intros; - try (eapply wff_in_impl_Proper; [ solve [ eauto with wf ] | ]); - auto. - Qed. - - Lemma Wf_SmartBound {t1} e input_bounds - (Hwf : Wf e) - : Wf (@SmartBound t1 e input_bounds). - Proof using wff_Cast. - intros var1 var2; specialize (Hwf var1 var2). - unfold SmartBound.SmartBound. - apply wf_smart_bound; assumption. - Qed. -End language. - -Hint Resolve Wf_SmartBound wff_bound_op : wf. diff --git a/src/Compilers/SmartCast.v b/src/Compilers/SmartCast.v deleted file mode 100644 index 237907e9c..000000000 --- a/src/Compilers/SmartCast.v +++ /dev/null @@ -1,41 +0,0 @@ -Require Import Coq.Bool.Sumbool. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Util.Notations. - -Local Open Scope expr_scope. -Local Open Scope ctype_scope. -Section language. - Context {base_type_code : Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')). - - Local Notation exprf := (@exprf base_type_code op). - - Definition SmartCast_base {var A A'} (x : exprf (var:=var) (Tbase A)) - : exprf (var:=var) (Tbase A') - := match sumbool_of_bool (base_type_beq A A') with - | left pf => match base_type_bl_transparent _ _ pf with - | eq_refl => x - end - | right _ => Cast _ _ A' x - end. - - Fixpoint SmartCast {var} A B - : option (interp_flat_type var A -> exprf (var:=var) B) - := match A, B return option (interp_flat_type var A -> exprf (var:=var) B) with - | Tbase A, Tbase B => Some (fun v => SmartCast_base (Var (var:=var) v)) - | Prod A0 A1, Prod B0 B1 - => match @SmartCast _ A0 B0, @SmartCast _ A1 B1 with - | Some f, Some g => Some (fun xy => Pair (f (fst xy)) (g (snd xy))) - | _, _ => None - end - | Unit, Unit => Some (fun _ => TT) - | Tbase _, _ - | Prod _ _, _ - | Unit, _ - => None - end. -End language. diff --git a/src/Compilers/SmartCastInterp.v b/src/Compilers/SmartCastInterp.v deleted file mode 100644 index e755cd168..000000000 --- a/src/Compilers/SmartCastInterp.v +++ /dev/null @@ -1,37 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.SmartCast. -Require Import Crypto.Util.Notations. - -Local Open Scope expr_scope. -Local Open Scope ctype_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 src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst} - {base_type_beq : base_type_code -> base_type_code -> bool} - {base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y} - {Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')} - (interpf_Cast_id : forall A x, interpf interp_op (Cast _ A A x) = interpf interp_op x) - {cast_val : forall A A', interp_base_type A -> interp_base_type A'} - (interpf_cast : forall A A' e, interpf interp_op (Cast _ A A' e) = cast_val A A' (interpf interp_op e)). - - Local Notation exprf := (@exprf base_type_code op). - Local Notation SmartCast_base := (@SmartCast_base _ _ _ base_type_bl_transparent Cast). - Local Notation SmartCast := (@SmartCast _ _ _ base_type_bl_transparent Cast). - - Lemma interpf_SmartCast_base {A A'} (x : exprf (Tbase A)) - : interpf interp_op (SmartCast_base x) = interpf interp_op (Cast _ A A' x). - Proof using interpf_Cast_id. - clear dependent cast_val. - unfold SmartCast_base. - destruct (Sumbool.sumbool_of_bool (base_type_beq A A')) as [H|H]. - { destruct (base_type_bl_transparent A A' H). - rewrite interpf_Cast_id; reflexivity. } - { reflexivity. } - Qed. -End language. - -Hint Rewrite @interpf_SmartCast_base using solve [ eassumption | eauto ] : reflective_interp. diff --git a/src/Compilers/SmartCastWf.v b/src/Compilers/SmartCastWf.v deleted file mode 100644 index 8ff630b77..000000000 --- a/src/Compilers/SmartCastWf.v +++ /dev/null @@ -1,84 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.WfProofs. -Require Import Crypto.Compilers.TypeUtil. -Require Import Crypto.Compilers.SmartCast. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Notations. - -Local Open Scope expr_scope. -Local Open Scope ctype_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 src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst} - (base_type_beq : base_type_code -> base_type_code -> bool) - (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) - (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) - (wff_Cast : forall var1 var2 G A A' e1 e2, - wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)). - - Local Notation exprf := (@exprf base_type_code op). - Local Notation SmartCast_base := (@SmartCast_base _ _ _ base_type_bl_transparent Cast). - Local Notation SmartCast := (@SmartCast _ _ _ base_type_bl_transparent Cast). - - Lemma wff_SmartCast_base {var1 var2 A A'} G e1 e2 - (Hwf : wff (var1:=var1) (var2:=var2) G (t:=Tbase A) e1 e2) - : wff G (t:=Tbase A') (SmartCast_base e1) (SmartCast_base e2). - Proof using wff_Cast. - unfold SmartCast_base; destruct (Sumbool.sumbool_of_bool (base_type_beq A A')) as [H|H]. - { destruct (base_type_bl_transparent A A' H); assumption. } - { auto. } - Qed. - - Local Hint Resolve List.in_or_app wff_in_impl_Proper. - Local Hint Extern 1 => progress simpl. - - Lemma wff_SmartCast_match {var1 var2} A B - : match SmartCast A B, SmartCast A B with - | Some f1, Some f2 - => forall e1 e2, - wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2) (f1 e1) (f2 e2) - | None, None => True - | Some _, None | None, Some _ => False - end. - Proof using wff_Cast. - break_innermost_match; revert dependent B; induction A, B; - repeat match goal with - | _ => progress simpl in * - | _ => intro - | _ => progress subst - | _ => progress inversion_option - | [ |- wff _ (SmartCast_base _) (SmartCast_base _) ] - => apply wff_SmartCast_base - | _ => progress break_match_hyps - | _ => solve [ eauto with wf ] - | [ H : forall B f1 f2, SmartCast ?A B = Some f1 -> SmartCast ?A B = Some f2 -> _, - H' : SmartCast ?A ?Bv = Some _, H'' : SmartCast ?A ?Bv = Some _ |- _ ] - => specialize (H _ _ _ H' H'') - | [ |- wff _ (Pair _ _) (Pair _ _) ] => constructor - | [ |- wff _ _ _ ] => solve [ eauto with wf ] - end. - Qed. - - Lemma wff_SmartCast {var1 var2} A B f1 f2 - : SmartCast A B = Some f1 -> SmartCast A B = Some f2 - -> forall e1 e2, - wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2) (f1 e1) (f2 e2). - Proof using wff_Cast. - intros H1 H2; generalize (@wff_SmartCast_match var1 var2 A B). - rewrite H1, H2; trivial. - Qed. - - Lemma wff_SmartCast_app {var1 var2} G A B f1 f2 - : SmartCast A B = Some f1 -> SmartCast A B = Some f2 - -> forall e1 e2, - wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2 ++ G) (f1 e1) (f2 e2). - Proof using wff_Cast. - intros; eapply wff_in_impl_Proper; [ eapply wff_SmartCast; eassumption | auto ]. - Qed. -End language. - -Hint Resolve wff_SmartCast_base wff_SmartCast wff_SmartCast_app : wf. |