From ad3f1343356b2ac60da964922459105e3329af0e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 5 Apr 2019 20:24:08 -0400 Subject: Automate more of the rewriter, and factor out rule-specific things --- src/Language.v | 100 +++++++++++++++++++-------------------------------------- 1 file changed, 33 insertions(+), 67 deletions(-) (limited to 'src/Language.v') diff --git a/src/Language.v b/src/Language.v index 966cd3118..eb64e0f2e 100644 --- a/src/Language.v +++ b/src/Language.v @@ -3,6 +3,7 @@ Require Import Coq.FSets.FMapPositive. Require Import Coq.Bool.Bool. Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relation_Definitions. +Require Import Crypto.PreLanguage. Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. Require Import Crypto.Util.Option. @@ -18,8 +19,10 @@ Require Import Crypto.Util.Tactics.RunTacticAsConstr. Require Import Crypto.Util.Tactics.DebugPrint. Require Import Crypto.Util.Tactics.ConstrFail. Import Coq.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. +Export PreLanguage. Module Compilers. + Export PreLanguage. Local Set Boolean Equality Schemes. Local Set Decidable Equality Schemes. Module Reify. @@ -1012,27 +1015,9 @@ Module Compilers. Section gen. Context (cast_outside_of_range : zrange -> BinInt.Z -> BinInt.Z). - Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool - := ((Z.abs (lower r) fancy.interp (invert_Some (to_fancy idc)) end. End gen. - - Definition cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z. - Proof. exact v. Qed. End with_base. Notation Some := option_Some. Notation None := option_None. (** Interpret identifiers where [Z_cast] is an opaque identity function when the value is not inside the range *) - Notation interp := (@gen_interp cast_outside_of_range). + Notation interp := (@gen_interp ident.cast_outside_of_range). Notation LiteralUnit := (@Literal base.type.unit). Notation LiteralZ := (@Literal base.type.Z). Notation LiteralBool := (@Literal base.type.bool). Notation LiteralNat := (@Literal base.type.nat). Notation LiteralZRange := (@Literal base.type.zrange). - Definition literal {T} (v : T) := v. - Definition eagerly {T} (v : T) := v. - Definition gets_inlined (real_val : bool) {T} (v : T) : bool := real_val. (** TODO: MOVE ME? *) - Module Thunked. - Definition bool_rect P (t f : Datatypes.unit -> P) (b : bool) : P - := Datatypes.bool_rect (fun _ => P) (t tt) (f tt) b. - Definition list_rect {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P -> P) (ls : list A) : P - := Datatypes.list_rect (fun _ => P) (N tt) C ls. - Definition list_case {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P) (ls : list A) : P - := ListUtil.list_case (fun _ => P) (N tt) C ls. - Definition nat_rect P (O_case : unit -> P) (S_case : nat -> P -> P) (n : nat) : P - := Datatypes.nat_rect (fun _ => P) (O_case tt) S_case n. - Definition option_rect {A} P (S_case : A -> P) (N_case : unit -> P) (o : option A) : P - := Datatypes.option_rect (fun _ => P) S_case (N_case tt) o. - End Thunked. - Ltac require_primitive_const term := lazymatch term with | S ?n => require_primitive_const n @@ -1203,7 +1169,7 @@ Module Compilers. | Datatypes.None => idtac | ZRange.Build_zrange ?x ?y => require_primitive_const x; require_primitive_const y - | literal ?x => idtac + | ident.literal ?x => idtac | ?term => fail 0 "Not a known const:" term end. Ltac is_primitive_const term := @@ -1259,20 +1225,20 @@ Module Compilers. then_tac (@ident.pair rA rB) | @Datatypes.bool_rect ?T0 ?Ptrue ?Pfalse => lazymatch (eval cbv beta in T0) with - | fun _ => ?T => reify_rec (@Thunked.bool_rect T (fun _ : Datatypes.unit => Ptrue) (fun _ : Datatypes.unit => Pfalse)) + | fun _ => ?T => reify_rec (@ident.Thunked.bool_rect T (fun _ : Datatypes.unit => Ptrue) (fun _ : Datatypes.unit => Pfalse)) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.bool_rect T' Ptrue Pfalse) end - | @Thunked.bool_rect ?T + | @ident.Thunked.bool_rect ?T => let rT := base.reify T in then_tac (@ident.bool_rect rT) | @Datatypes.option_rect ?A ?T0 ?PSome ?PNone => lazymatch (eval cbv beta in T0) with - | fun _ => ?T => reify_rec (@Thunked.option_rect A T PSome (fun _ : Datatypes.unit => PNone)) + | fun _ => ?T => reify_rec (@ident.Thunked.option_rect A T PSome (fun _ : Datatypes.unit => PNone)) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.option_rect A T' PSome PNone) end - | @Thunked.option_rect ?A ?T + | @ident.Thunked.option_rect ?A ?T => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.option_rect rA rT) @@ -1297,7 +1263,7 @@ Module Compilers. | @Datatypes.nat_rect ?T0 ?P0 => lazymatch (eval cbv beta in T0) with | fun _ => _ -> _ => else_tac () - | fun _ => ?T => reify_rec (@Thunked.nat_rect T (fun _ : Datatypes.unit => P0)) + | fun _ => ?T => reify_rec (@ident.Thunked.nat_rect T (fun _ : Datatypes.unit => P0)) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.nat_rect T' P0) end @@ -1310,32 +1276,32 @@ Module Compilers. | T0 => else_tac () | ?T' => reify_rec (@Datatypes.nat_rect T') end - | @Thunked.nat_rect ?T + | @ident.Thunked.nat_rect ?T => let rT := base.reify T in then_tac (@ident.nat_rect rT) - | eagerly (@Datatypes.nat_rect) ?T0 ?P0 + | ident.eagerly (@Datatypes.nat_rect) ?T0 ?P0 => lazymatch (eval cbv beta in T0) with | fun _ => _ -> _ => else_tac () - | fun _ => ?T => reify_rec (eagerly (@Thunked.nat_rect) T (fun _ : Datatypes.unit => P0)) + | fun _ => ?T => reify_rec (ident.eagerly (@ident.Thunked.nat_rect) T (fun _ : Datatypes.unit => P0)) | T0 => else_tac () - | ?T' => reify_rec (eagerly (@Datatypes.nat_rect) T' P0) + | ?T' => reify_rec (ident.eagerly (@Datatypes.nat_rect) T' P0) end - | eagerly (@Datatypes.nat_rect) ?T0 + | ident.eagerly (@Datatypes.nat_rect) ?T0 => lazymatch (eval cbv beta in T0) with | (fun _ => ?P -> ?Q) => let rP := base.reify P in let rQ := base.reify Q in then_tac (@ident.eager_nat_rect_arrow rP rQ) | T0 => else_tac () - | ?T' => reify_rec (eagerly (@Datatypes.nat_rect) T') + | ?T' => reify_rec (ident.eagerly (@Datatypes.nat_rect) T') end - | eagerly (@Thunked.nat_rect) ?T + | ident.eagerly (@ident.Thunked.nat_rect) ?T => let rT := base.reify T in then_tac (@ident.eager_nat_rect rT) | @Datatypes.list_rect ?A ?T0 ?Pnil => lazymatch (eval cbv beta in T0) with | fun _ => _ -> _ => else_tac () - | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil)) + | fun _ => ?T => reify_rec (@ident.Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil)) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil) end @@ -1349,18 +1315,18 @@ Module Compilers. | T0 => else_tac () | ?T' => reify_rec (@Datatypes.list_rect A T') end - | @Thunked.list_rect ?A ?T + | @ident.Thunked.list_rect ?A ?T => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.list_rect rA rT) - | eagerly (@Datatypes.list_rect) ?A ?T0 ?Pnil + | ident.eagerly (@Datatypes.list_rect) ?A ?T0 ?Pnil => lazymatch (eval cbv beta in T0) with | fun _ => _ -> _ => else_tac () - | fun _ => ?T => reify_rec (eagerly (@Thunked.list_rect) A T (fun _ : Datatypes.unit => Pnil)) + | fun _ => ?T => reify_rec (ident.eagerly (@ident.Thunked.list_rect) A T (fun _ : Datatypes.unit => Pnil)) | T0 => else_tac () - | ?T' => reify_rec (eagerly (@Datatypes.list_rect) A T' Pnil) + | ?T' => reify_rec (ident.eagerly (@Datatypes.list_rect) A T' Pnil) end - | eagerly (@Datatypes.list_rect) ?A ?T0 + | ident.eagerly (@Datatypes.list_rect) ?A ?T0 => lazymatch (eval cbv beta in T0) with | (fun _ => ?P -> ?Q) => let rA := base.reify A in @@ -1368,19 +1334,19 @@ Module Compilers. let rQ := base.reify Q in then_tac (@ident.eager_list_rect_arrow rA rP rQ) | T0 => else_tac () - | ?T' => reify_rec (eagerly (@Datatypes.list_rect) A T') + | ?T' => reify_rec (ident.eagerly (@Datatypes.list_rect) A T') end - | eagerly (@Thunked.list_rect) ?A ?T + | ident.eagerly (@ident.Thunked.list_rect) ?A ?T => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.eager_list_rect rA rT) | @ListUtil.list_case ?A ?T0 ?Pnil => lazymatch (eval cbv beta in T0) with - | fun _ => ?T => reify_rec (@Thunked.list_case A T (fun _ : Datatypes.unit => Pnil)) + | fun _ => ?T => reify_rec (@ident.Thunked.list_case A T (fun _ : Datatypes.unit => Pnil)) | T0 => else_tac () | ?T' => reify_rec (@ListUtil.list_case A T' Pnil) end - | @Thunked.list_case ?A ?T + | @ident.Thunked.list_case ?A ?T => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.list_case rA rT) @@ -1479,9 +1445,9 @@ Module Compilers. => let rA := base.reify A in then_tac (@ident.None rA) | ZRange.Build_zrange => then_tac ident.Build_zrange - | eagerly (?f ?x) => reify_rec (eagerly f x) + | ident.eagerly (?f ?x) => reify_rec (ident.eagerly f x) | fancy.interp ?idc - => let ridc := (eval cbv [to_fancy] in (to_fancy idc)) in + => let ridc := (eval cbv [of_fancy] in (of_fancy idc)) in then_tac ridc | @gen_interp _ _ ?idc => then_tac idc | _ => else_tac () @@ -2047,4 +2013,4 @@ Module Compilers. := FromFlat (to_flat e). End GeneralizeVar. End Compilers. -Global Opaque Compilers.ident.cast. (* This should never be unfolded except in [LanguageWf] *) +Global Opaque ident.cast. (* This should never be unfolded except in [LanguageWf] *) -- cgit v1.2.3