diff options
author | Jason Gross <jgross@mit.edu> | 2018-04-17 18:40:18 -0400 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2018-04-18 03:43:32 -0400 |
commit | bad2d2aaa49cc0ea7a77c24655204964a4f25d2b (patch) | |
tree | fa1c9aecfceae63f87f275d440ec5fa7e9cf2637 /src | |
parent | a90c2b5eeed88e611b241dc1a52cb94f92bb40e7 (diff) |
Also include the syntax tree in bounds analysis errors
This should fix #349 (or at least most of it).
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 3845c8781..63f176b37 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -5715,28 +5715,28 @@ Module Compilers. {s d} (E : Expr (s -> d)) (b_in : ZRange.type.option.interp s) (b_out : ZRange.type.option.interp d) - : Expr (s -> d) + ZRange.type.option.interp d + : Expr (s -> d) + (ZRange.type.option.interp d * Expr (s -> d)) := let b_computed := partial.bounds.expr.Extract E b_in in if ZRange.type.option.is_tighter_than b_computed b_out then @inl (Expr (s -> d)) _ (RelaxZRange.expr.Relax relax_zrange E) - else @inr _ (ZRange.type.option.interp d) b_computed. + else @inr _ (ZRange.type.option.interp d * Expr (s -> d)) (b_computed, E). Definition CheckPartialEvaluateWithBounds0 (relax_zrange : zrange -> option zrange) {t} (E : Expr t) (b_out : ZRange.type.option.interp t) - : Expr t + ZRange.type.option.interp t + : Expr t + (ZRange.type.option.interp t * Expr t) := let b_computed := partial.bounds.expr.Extract E in if ZRange.type.option.is_tighter_than b_computed b_out then @inl (Expr t) _ (RelaxZRange.expr.Relax relax_zrange E) - else @inr _ (ZRange.type.option.interp t) b_computed. + else @inr _ (ZRange.type.option.interp t * Expr t) (b_computed, E). Definition CheckedPartialEvaluateWithBounds1 (relax_zrange : zrange -> option zrange) {s d} (e : Expr (s -> d)) (b_in : ZRange.type.option.interp s) (b_out : ZRange.type.option.interp d) - : Expr (s -> d) + ZRange.type.option.interp d + : Expr (s -> d) + (ZRange.type.option.interp d * Expr (s -> d)) := let E := PartialEvaluateWithBounds1 e b_in in dlet_nd e := GeneralizeVar.ToFlat E in let E := GeneralizeVar.FromFlat e in @@ -5746,7 +5746,7 @@ Module Compilers. (relax_zrange : zrange -> option zrange) {t} (e : Expr t) (b_out : ZRange.type.option.interp t) - : Expr t + ZRange.type.option.interp t + : Expr t + (ZRange.type.option.interp t * Expr t) := let E := PartialEvaluate true e in dlet_nd e := GeneralizeVar.ToFlat E in let E := GeneralizeVar.FromFlat e in @@ -6542,9 +6542,9 @@ Module Pipeline. Inductive ErrorMessage := | Computed_bounds_are_not_tight_enough {t} (computed_bounds expected_bounds : ZRange.type.option.interp t) + {t'} (syntax_tree : Expr t') | Bounds_analysis_failed | Type_too_complicated_for_cps (t : type) - | Return_type_mismatch {T'} (found expected : T') | Value_not_le (descr : string) {T'} (lhs rhs : T') | Value_not_lt (descr : string) {T'} (lhs rhs : T') | Values_not_provably_distinct (descr : string) {T'} (lhs rhs : T') @@ -6600,8 +6600,8 @@ Module Pipeline. let E := CheckedPartialEvaluateWithBounds1 relax_zrange E arg_bounds out_bounds in match E with | inl E => Success E - | inr b - => Error (Computed_bounds_are_not_tight_enough b out_bounds) + | inr (b, E) + => Error (Computed_bounds_are_not_tight_enough b out_bounds E) end) | None => Error (Type_too_complicated_for_cps t) end. @@ -6626,7 +6626,7 @@ Module Pipeline. cbv [BoundsPipeline Let_In] in *; repeat match goal with | [ H : match ?x with _ => _ end = Success _ |- _ ] - => destruct x eqn:?; cbv beta iota in H; [ | congruence ]; + => destruct x eqn:?; cbv beta iota in H; [ | destruct_head'_prod; congruence ]; let H' := fresh in inversion H as [H']; clear H; rename H' into H end. |