From 6211f14a1283c359944a3dd44699ba2a1b53ddc2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 2 Apr 2017 01:08:42 -0400 Subject: Add PreDefinitions pipeline file --- src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v | 33 +++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v (limited to 'src/Reflection') diff --git a/src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v b/src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v new file mode 100644 index 000000000..beca8e9d5 --- /dev/null +++ b/src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v @@ -0,0 +1,33 @@ +(** * 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. +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. -- cgit v1.2.3