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/BoundsPipeline.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/BoundsPipeline.v') diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index 1c6cec4c7..f0c161dc2 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -141,6 +141,7 @@ Module Pipeline. => fun 'tt 'tt => (false, nil, nil) | base.type.nat | base.type.bool + | base.type.zrange => fun _ _ => (false, nil, nil) | base.type.Z => fun a b @@ -153,6 +154,19 @@ Module Pipeline. then (false, nil, nil) else (false, nil, ((a, b)::nil)) end + | base.type.option A + => fun a b + => match a, b with + | None, None => (false, nil, nil) + | Some _, None => (false, nil, nil) + | None, Some _ => (true, nil, nil) + | Some None, Some None + | Some (Some _), Some None + | Some None, Some (Some _) + => (false, nil, nil) + | Some (Some a), Some (Some b) + => @find_too_loose_base_bounds A a b + end | base.type.prod A B => fun '(ra, rb) '(ra', rb') => let '(b1, lens1, ls1) := @find_too_loose_base_bounds A ra ra' in -- cgit v1.2.3