From 0bbbdfede48aed7a74ac2fb95440256ed60fb6e8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Feb 2019 18:17:11 -0500 Subject: Add support for reifying `zrange` and `option` This is needed to reify statements for the rewriter. --- src/Rewriter.v | 27 +++++++++++++++++++-------- 1 file changed, 19 insertions(+), 8 deletions(-) (limited to 'src/Rewriter.v') diff --git a/src/Rewriter.v b/src/Rewriter.v index a79bcb18f..e23b65ae7 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -41,6 +41,7 @@ Module Compilers. | type.type_base t => type.type_base t | type.prod A B => type.prod (partial_subst A evar_map) (partial_subst B evar_map) | type.list A => type.list (partial_subst A evar_map) + | type.option A => type.option (partial_subst A evar_map) end. Fixpoint subst (ptype : type) (evar_map : EvarMap) : option Compilers.base.type @@ -52,6 +53,7 @@ Module Compilers. B' <- subst B evar_map; Some (Compilers.base.type.prod A' B')) | type.list A => option_map Compilers.base.type.list (subst A evar_map) + | type.option A => option_map Compilers.base.type.option (subst A evar_map) end%option. Fixpoint subst_default_relax P {t evm} : P t -> P (subst_default (relax t) evm) @@ -66,6 +68,8 @@ Module Compilers. v) | Compilers.base.type.list A => @subst_default_relax (fun t => P (Compilers.base.type.list t)) A evm + | Compilers.base.type.option A + => @subst_default_relax (fun t => P (Compilers.base.type.option t)) A evm end. Fixpoint var_types_of (t : type) : Set @@ -74,6 +78,7 @@ Module Compilers. | type.type_base _ => unit | type.prod A B => var_types_of A * var_types_of B | type.list A => var_types_of A + | type.option A => var_types_of A end%type. Fixpoint add_var_types_cps {t : type} (v : var_types_of t) (evm : EvarMap) : ~> EvarMap @@ -84,6 +89,7 @@ Module Compilers. | type.prod A B => fun '(a, b) => @add_var_types_cps A a evm _ (fun evm => @add_var_types_cps B b evm _ k) | type.list A => fun t => @add_var_types_cps A t evm _ k + | type.option A => fun t => @add_var_types_cps A t evm _ k | type.type_base _ => fun _ => k evm end v. @@ -102,9 +108,12 @@ Module Compilers. Some (a, b) | type.list A, Compilers.base.type.list A' => unify_extracted A A' + | type.option A, Compilers.base.type.option A' + => unify_extracted A A' | type.type_base _, _ | type.prod _ _, _ | type.list _, _ + | type.option _, _ => None end%option. End base. @@ -1231,6 +1240,7 @@ Module Compilers. b <- make_Literal_pattern B; Some ((#pattern.ident.pair @ a @ b)%pattern)) | pattern.base.type.list A => None + | pattern.base.type.option A => None end%option%cps. Fixpoint make_interp_rewrite_pattern {t} @@ -1272,6 +1282,7 @@ Module Compilers. with | pattern.base.type.var _ | pattern.base.type.list _ + | pattern.base.type.option _ => I | pattern.base.type.type_base t => fun f x => f x @@ -1937,13 +1948,13 @@ Module Compilers. Definition strip_literal_casts_dtree' := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 strip_literal_casts_rewrite_rules. Definition nbe_dtree : decision_tree - := Eval compute in invert_Some nbe_dtree'. + := Eval compute in Option.invert_Some nbe_dtree'. Definition arith_dtree : decision_tree - := Eval compute in invert_Some arith_dtree'. + := Eval compute in Option.invert_Some arith_dtree'. Definition arith_with_casts_dtree : decision_tree - := Eval compute in invert_Some arith_with_casts_dtree'. + := Eval compute in Option.invert_Some arith_with_casts_dtree'. Definition strip_literal_casts_dtree : decision_tree - := Eval compute in invert_Some strip_literal_casts_dtree'. + := Eval compute in Option.invert_Some strip_literal_casts_dtree'. Definition nbe_default_fuel := Eval compute in List.length nbe_rewrite_rules. Definition arith_default_fuel := Eval compute in List.length (arith_rewrite_rules 0%Z (* dummy val *)). @@ -2214,11 +2225,11 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) Definition fancy_dtree' := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_rewrite_rules. Definition fancy_dtree : decision_tree - := Eval compute in invert_Some fancy_dtree'. + := Eval compute in Option.invert_Some fancy_dtree'. Definition fancy_with_casts_dtree' := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_with_casts_rewrite_rules. Definition fancy_with_casts_dtree : decision_tree - := Eval compute in invert_Some fancy_with_casts_dtree'. + := Eval compute in Option.invert_Some fancy_with_casts_dtree'. Definition fancy_default_fuel := Eval compute in List.length fancy_rewrite_rules. Definition fancy_with_casts_default_fuel := Eval compute in List.length fancy_with_casts_rewrite_rules. Import PrimitiveHList. @@ -2255,8 +2266,8 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) Export Language.Compilers.defaults. Export PrimitiveSigma.Primitive. Notation "'llet' x := v 'in' f" := (Let_In v (fun x => f)). - Notation "x <- 'type.try_make_transport_cps' t1 t2 ; f" := (type.try_make_transport_cps t1 t2 (fun y => match y with Some x => f | None => None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x <- 'type.try_make_transport_cps' t1 t2 ; '/' f ']'"). - Notation "x <- 'base.try_make_transport_cps' t1 t2 ; f" := (base.try_make_transport_cps t1 t2 (fun y => match y with Some x => f | None => None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x <- 'base.try_make_transport_cps' t1 t2 ; '/' f ']'"). + Notation "x <- 'type.try_make_transport_cps' t1 t2 ; f" := (type.try_make_transport_cps t1 t2 (fun y => match y with Datatypes.Some x => f | Datatypes.None => Datatypes.None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x <- 'type.try_make_transport_cps' t1 t2 ; '/' f ']'"). + Notation "x <- 'base.try_make_transport_cps' t1 t2 ; f" := (base.try_make_transport_cps t1 t2 (fun y => match y with Datatypes.Some x => f | Datatypes.None => Datatypes.None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x <- 'base.try_make_transport_cps' t1 t2 ; '/' f ']'"). End RewriterPrintingNotations. Ltac make_rewrite_head1 rewrite_head0 pr2_rewrite_rules := -- cgit v1.2.3