From f5ed7d87fddab66267f2a8242d31c205a0e24a4a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Feb 2017 16:27:32 -0500 Subject: Generalize BoundByCast a bit The rules for handling | / & vs >> are different; we can truncate early on | / &, but not on >> --- src/Reflection/BoundByCast.v | 14 +++++++++----- src/Reflection/MultiSizeTest2.v | 4 ++-- 2 files changed, 11 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/Reflection/BoundByCast.v b/src/Reflection/BoundByCast.v index fc2e6d11c..fb7b4b576 100644 --- a/src/Reflection/BoundByCast.v +++ b/src/Reflection/BoundByCast.v @@ -22,7 +22,7 @@ Section language. (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) (is_cast : forall src dst, op src dst -> bool) (is_const : forall src dst, op src dst -> bool) - (genericize_op : forall src dst (opc : op src dst) (new_bounded_type : base_type_code), + (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) (failf : forall var t, @exprf base_type_code op var (Tbase t)). Local Infix "<=?" := base_type_leb : expr_scope. @@ -169,10 +169,15 @@ Section language. => let output_bounds := interp_op_bounds _ _ opc2 input_bounds in let input_ts := SmartVarfMap bound_base_type input_bounds in let output_ts := SmartVarfMap bound_base_type output_bounds in - let new_type := flat_type_max (t:=Prod _ _) (input_ts, output_ts)%core in - let new_opc := option_map (genericize_op _ _ opc1) new_type in + let new_type_in := flat_type_max input_ts in + let new_type_out := flat_type_max output_ts in + let new_opc := match new_type_in, new_type_out with + | Some new_type_in, Some new_type_out + => genericize_op _ _ opc1 new_type_in new_type_out + | None, _ | _, None => None + end in match new_opc with - | Some (Some (existT _ new_opc)) + | Some (existT _ new_opc) => match SmartCast _ _, SmartCast _ _ with | Some SmartCast_args, Some SmartCast_result => LetIn args @@ -183,7 +188,6 @@ Section language. | _, None => Op opc1 args end - | Some None | None => Op opc1 args end. diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v index ec69d4c7b..49629cf58 100644 --- a/src/Reflection/MultiSizeTest2.v +++ b/src/Reflection/MultiSizeTest2.v @@ -46,10 +46,10 @@ Definition is_cast src dst (opc : op src dst) : bool Definition is_const src dst (opc : op src dst) : bool := match opc with Const _ _ => true | _ => false end. -Definition genericize_op src dst (opc : op src dst) (new_t : base_type) +Definition genericize_op src dst (opc : op src dst) (new_t_in new_t_out : base_type) : option { src'dst' : _ & op (fst src'dst') (snd src'dst') } := match opc with - | Plus _ => Some (existT _ (_, _) (Plus new_t)) + | Plus _ => Some (existT _ (_, _) (Plus (base_type_max base_type_leb new_t_in new_t_out))) | Const _ _ | Cast _ _ => None -- cgit v1.2.3