diff options
author | Jason Gross <jgross@mit.edu> | 2019-04-04 15:51:20 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-04-04 15:51:20 -0400 |
commit | e0c9b5f803e63a91922cc0724119d39da0f24379 (patch) | |
tree | e48031155ce78dd94d33761917ece57455fb59fd /src/RewriterRulesInterpGood.v | |
parent | bd34d676010ebf6dd4aa5076537f89572803dd3d (diff) |
Add UnderLets flat_map interp proofs,other changes
Also remove a rewrite rule using cast from the non-cast arith rules,
regenerate the .out files, add ident.gets_inlined for eventual use in
the rewriter, and generalize the rewrite rule lemmas over
cast_out_of_range so that we can actually make use of their proofs for
interp.
Diffstat (limited to 'src/RewriterRulesInterpGood.v')
-rw-r--r-- | src/RewriterRulesInterpGood.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index d30366220..c73867339 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -144,7 +144,7 @@ Module Compilers. | [ |- _ /\ _ ] => split; [ intros; exact I | ] end | progress cbn [eq_rect] in * ]; - cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp UnderLets.interp_related] in *. + cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp UnderLets.interp_related UnderLets.interp_related_gen] in *. Ltac recurse_interp_related_step := let do_replace v := @@ -350,7 +350,7 @@ Module Compilers. | ] | [ |- context[match _ with nil => _ | _ => _ end] ] => progress recursive_match_to_list_case_in_goal end - | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related type.related] in * + | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related UnderLets.interp_related_gen type.related] in * | progress cbv [Compile.option_bind' respectful expr.interp_related] in * | progress fold (@type.interp _ base.interp) | progress fold (@base.interp) |