From 719844deb55f1566b3bc73d3e6e16f906aa72e62 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 2 Apr 2017 11:11:05 -0400 Subject: Remove the bits of the new reflective pipeline in master This way, we can keep all of new pipeline code together in the PR --- _CoqProject | 2 - src/Reflection/Z/Bounds/Pipeline/Glue.v | 149 ---------------------- src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v | 52 -------- src/Specific/IntegrationTest.v | 2 - 4 files changed, 205 deletions(-) delete mode 100644 src/Reflection/Z/Bounds/Pipeline/Glue.v delete mode 100644 src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v diff --git a/_CoqProject b/_CoqProject index 0fde396da..9dce03103 100644 --- a/_CoqProject +++ b/_CoqProject @@ -216,8 +216,6 @@ src/Reflection/Z/Syntax.v src/Reflection/Z/Bounds/Interpretation.v src/Reflection/Z/Bounds/MapCastByDeBruijn.v src/Reflection/Z/Bounds/Relax.v -src/Reflection/Z/Bounds/Pipeline/Glue.v -src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v src/Reflection/Z/Interpretations128/Relations.v src/Reflection/Z/Interpretations128/RelationsCombinations.v src/Reflection/Z/Interpretations64/Relations.v diff --git a/src/Reflection/Z/Bounds/Pipeline/Glue.v b/src/Reflection/Z/Bounds/Pipeline/Glue.v deleted file mode 100644 index 93986a42f..000000000 --- a/src/Reflection/Z/Bounds/Pipeline/Glue.v +++ /dev/null @@ -1,149 +0,0 @@ -(** * Reflective Pipeline: Glue Code *) -(** This file defines the tactics that transform a non-reflective goal - into a goal the that the reflective machinery can handle. *) -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.Reify. -Require Import Crypto.Reflection.Z.Syntax. -Require Import Crypto.Reflection.Z.Syntax.Util. -Require Import Crypto.Reflection.Z.Reify. -Require Import Crypto.Reflection.Z.Bounds.Interpretation. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Curry. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tuple. - -(** The [do_curry] tactic takes a goal of the form -<< -BoundedWordToZ (?f a b ... z) = F A B ... Z ->> - and turns it into a goal of the form -<< -BoundedWordToZ (f' (a, b, ..., z)) = F' (A, B, ..., Z) ->> - *) -Ltac do_curry := - lazymatch goal with - | [ |- ?BWtoZ ?f_bw = ?f_Z ] - => let f_bw := head f_bw in - let f_Z := head f_Z in - change_with_curried f_Z; - let f_bw_name := fresh f_bw in - set (f_bw_name := f_bw); - change_with_curried f_bw_name - end. -(** The [split_BoundedWordToZ] tactic takes a goal of the form -<< -BoundedWordToZ (f args) = F ARGS ->> - and splits it into a conjunction, one part about the computational - behavior, and another part about the boundedness. *) -Ltac count_tuple_length T := - lazymatch T with - | (?A * ?B)%type => let a := count_tuple_length A in - let b := count_tuple_length B in - (eval compute in (a + b)%nat) - | _ => constr:(1%nat) - end. -Ltac make_evar_for_first_projection := - lazymatch goal with - | [ |- @map ?N1 ?A ?B wordToZ (@proj1_sig _ ?P ?f) = ?fZ ?argsZ ] - => let T := type of argsZ in - let N := count_tuple_length T in - let map' := (eval compute in (@map N)) in - let proj1_sig' := (eval compute in @proj1_sig) in - let f1 := fresh f in - let f2 := fresh f in - let pf := fresh in - revert f; refine (_ : let f := exist P _ _ in _); - intro f; - pose (proj1_sig f) as f1; - pose (proj2_sig f : P f1) as f2; - change f with (exist _ f1 f2); - subst f; cbn [proj1_sig proj2_sig] in f1, f2 |- *; revert f2; - lazymatch goal with - | [ |- let f' := _ in @?P f' ] - => refine (let pf := _ in (proj2 pf : let f' := proj1 pf in P f')) - end - end. -Ltac split_BoundedWordToZ := - match goal with - | [ |- BoundedWordToZ _ _ _ ?x = _ ] - => revert x - end; - repeat match goal with - | [ |- context[BoundedWordToZ _ _ _ ?x] ] - => is_var x; - first [ clearbody x; fail 1 - | instantiate (1:=ltac:(destruct x)); destruct x ] - end; - cbv beta iota; intro; - unfold BoundedWordToZ; cbn [proj1_sig]; - make_evar_for_first_projection. -(** The [zrange_to_reflective] tactic takes a goal of the form -<< -is_bounded_by _ bounds (map wordToZ (?fW args)) /\ map wordToZ (?fW args) = fZ argsZ ->> - and uses [cut] and a small lemma to turn it into a goal that the - reflective machinery can handle. The goal left by this tactic - should be fully solvable by the reflective pipeline. *) - -Ltac const_tuple T val := - lazymatch T with - | (?A * ?B)%type => let a := const_tuple A val in - let b := const_tuple B val in - constr:((a, b)%core) - | _ => val - end. -Lemma adjust_goal_for_reflective {T P} (LHS RHS : T) - : P RHS /\ LHS = RHS -> P LHS /\ LHS = RHS. -Proof. intros [? ?]; subst; tauto. Qed. -Ltac adjust_goal_for_reflective := apply adjust_goal_for_reflective. -Ltac unmap_wordToZ_tuple term := - lazymatch term with - | (?x, ?y) => let x' := unmap_wordToZ_tuple x in - let y' := unmap_wordToZ_tuple y in - constr:((x', y')) - | map wordToZ ?x => x - end. -Ltac zrange_to_reflective_hyps_step := - match goal with - | [ H : @ZRange.is_bounded_by ?option_bit_width ?count ?bounds (Tuple.map wordToZ ?arg) |- _ ] - => let rT := constr:(Syntax.tuple (Tbase TZ) count) in - let is_bounded_by' := constr:(@Bounds.is_bounded_by rT) in - let map' := constr:(@cast_back_flat_const (@Bounds.interp_base_type) rT (fun _ => Bounds.bounds_to_base_type) bounds) in - (* we use [cut] and [abstract] rather than [change] to catch inefficiencies in conversion early, rather than allowing [Defined] to take forever *) - let H' := fresh H in - rename H into H'; - assert (H : is_bounded_by' bounds (map' arg)) by (clear -H'; abstract exact H'); - clear H'; move H at top - end. -Ltac zrange_to_reflective_hyps := repeat zrange_to_reflective_hyps_step. -Ltac zrange_to_reflective_goal := - lazymatch goal with - | [ |- @ZRange.is_bounded_by ?option_bit_width ?count ?bounds (Tuple.map wordToZ ?reified_f_evar) - /\ Tuple.map wordToZ ?reified_f_evar = ?f ?Zargs ] - => let T := type of f in - let f_domain := lazymatch T with ?A -> ?B => A end in - let T := (eval compute in T) in - let rT := reify_type T in - let is_bounded_by' := constr:(@Bounds.is_bounded_by (codomain rT)) in - let input_bounds := const_tuple f_domain bounds in - let map_t := constr:(fun t bs => @cast_back_flat_const (@Bounds.interp_base_type) t (fun _ => Bounds.bounds_to_base_type) bs) in - let map_output := constr:(map_t (codomain rT) bounds) in - let map_input := constr:(map_t (domain rT) input_bounds) in - let args := unmap_wordToZ_tuple Zargs in - (* we use [cut] and [abstract] rather than [change] to catch inefficiencies in conversion early, rather than allowing [Defined] to take forever *) - cut (is_bounded_by' bounds (map_output reified_f_evar) /\ map_output reified_f_evar = f (map_input args)); - [ generalize reified_f_evar; clear; clearbody f; let x := fresh in intros ? x; abstract exact x - | ]; - cbv beta - end; - adjust_goal_for_reflective. -Ltac zrange_to_reflective := zrange_to_reflective_hyps; zrange_to_reflective_goal. - -(** The tactic [refine_to_reflective_glue] is the public-facing one. *) -Ltac refine_to_reflective_glue := - do_curry; - split_BoundedWordToZ; - zrange_to_reflective. diff --git a/src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v b/src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v deleted file mode 100644 index 8102fe2ee..000000000 --- a/src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v +++ /dev/null @@ -1,52 +0,0 @@ -(** * Definitions which are used in the pipeline, but shouldn't be changed *) -(** *** Definition of the output type of the post-Wf pipeline *) -(** Do not change these definitions unless you're hacking on the - entire reflective pipeline tactic automation. *) -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.SmartMap. -Require Import Crypto.Reflection.Z.Syntax. -Require Import Crypto.Reflection.Z.Bounds.Interpretation. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Prod. -Local Notation pick_typeb := Bounds.bounds_to_base_type (only parsing). -Local Notation pick_type v := (SmartFlatTypeMap (fun _ => pick_typeb) v). - -Record ProcessedReflectivePackage - := { InputType : _; - input_expr : Expr base_type op InputType; - input_bounds : interp_flat_type Bounds.interp_base_type (domain InputType); - output_bounds :> interp_flat_type Bounds.interp_base_type (codomain InputType); - output_expr :> Expr base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }. - -Notation OutputType pkg - := (Arrow (pick_type (@input_bounds pkg)) (pick_type (@output_bounds pkg))) - (only parsing). - -Definition Build_ProcessedReflectivePackage_from_option_sigma - {t} (e : Expr base_type op t) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - (result : option { output_bounds : interp_flat_type Bounds.interp_base_type (codomain t) - & Expr base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }) - : option ProcessedReflectivePackage - := option_map - (fun be - => let 'existT b e' := be in - {| InputType := t ; input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |}) - result. - -Definition ProcessedReflectivePackage_to_sigT (x : ProcessedReflectivePackage) - : { InputType : _ - & Expr base_type op InputType - * { bounds : interp_flat_type Bounds.interp_base_type (domain InputType) - * interp_flat_type Bounds.interp_base_type (codomain InputType) - & Expr base_type op (Arrow (pick_type (fst bounds)) (pick_type (snd bounds))) } }%type - := let (a, b, c, d, e) := x in - existT _ a (b, (existT _ (c, d) e)). - -Ltac inversion_ProcessedReflectivePackage := - repeat match goal with - | [ H : _ = _ :> ProcessedReflectivePackage |- _ ] - => apply (f_equal ProcessedReflectivePackage_to_sigT) in H; - cbv [ProcessedReflectivePackage_to_sigT] in H - end; - inversion_sigma; inversion_prod. diff --git a/src/Specific/IntegrationTest.v b/src/Specific/IntegrationTest.v index 1e62937df..09280851a 100644 --- a/src/Specific/IntegrationTest.v +++ b/src/Specific/IntegrationTest.v @@ -10,8 +10,6 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. Import ListNotations. -Require Import Crypto.Reflection.Z.Bounds.Pipeline.Glue. - Section BoundedField25p5. Local Coercion Z.of_nat : nat >-> Z. -- cgit v1.2.3