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/UnderLets.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'src/UnderLets.v') diff --git a/src/UnderLets.v b/src/UnderLets.v index 522a8c4c7..34cecf322 100644 --- a/src/UnderLets.v +++ b/src/UnderLets.v @@ -108,6 +108,13 @@ Module Compilers. => splice x (fun x => @splice_list A B xs (fun xs => e (cons x xs))) end. + Definition splice_option {A B} (v : option (@UnderLets A)) (e : option A -> @UnderLets B) : @UnderLets B + := match v with + | None => e None + | Some x + => splice x (fun x => e (Some x)) + end. + Fixpoint to_expr {t} (x : @UnderLets (expr t)) : expr t := match x with | Base v => v @@ -127,6 +134,7 @@ Module Compilers. Bind Scope under_lets_scope with UnderLets.UnderLets. Notation "x <-- y ; f" := (UnderLets.splice y (fun x => f%under_lets)) : under_lets_scope. Notation "x <---- y ; f" := (UnderLets.splice_list y (fun x => f%under_lets)) : under_lets_scope. + Notation "x <----- y ; f" := (UnderLets.splice_option y (fun x => f%under_lets)) : under_lets_scope. End Notations. Section reify. @@ -183,6 +191,22 @@ Module Compilers. k | None => @default_reify_and_let_binds_base_cps _ e T k end + | base.type.option A + => fun e T k + => match reflect_option e with + | Some ls + => option_rect + _ + (fun x k + => @reify_and_let_binds_base_cps + A x _ + (fun xe + => k (#ident.Some @ xe)%expr)) + (fun k => k (#ident.None)%expr) + ls + k + | None => @default_reify_and_let_binds_base_cps _ e T k + end end%under_lets. Fixpoint let_bind_return {t} : expr t -> expr t -- cgit v1.2.3