diff options
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/Z/FoldTypes.v | 17 | ||||
| -rw-r--r-- | src/Reflection/Z/Syntax/Util.v | 3 |
2 files changed, 20 insertions, 0 deletions
diff --git a/src/Reflection/Z/FoldTypes.v b/src/Reflection/Z/FoldTypes.v new file mode 100644 index 000000000..776f000f5 --- /dev/null +++ b/src/Reflection/Z/FoldTypes.v @@ -0,0 +1,17 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.Reflection.Z.Syntax.Util. +Require Import Crypto.Reflection.FoldTypes. + +Section min_or_max. + Context (f : base_type -> base_type -> base_type) + (init : base_type). + + Definition TypeFold {t} (e : Expr base_type op t) : base_type + := TypeFold (fun t => t) f init e. +End min_or_max. + +Definition MaxTypeUsed {t} (e : Expr base_type op t) : base_type + := TypeFold base_type_max (TWord 0) e. +Definition MinTypeUsed {t} (e : Expr base_type op t) : base_type + := TypeFold base_type_min TZ e. diff --git a/src/Reflection/Z/Syntax/Util.v b/src/Reflection/Z/Syntax/Util.v index 8e9102101..24fe5b331 100644 --- a/src/Reflection/Z/Syntax/Util.v +++ b/src/Reflection/Z/Syntax/Util.v @@ -35,8 +35,11 @@ Definition base_type_leb (v1 v2 : base_type) : bool end. Definition base_type_min := base_type_min base_type_leb. +Definition base_type_max := base_type_max base_type_leb. Global Arguments base_type_min !_ !_ / . +Global Arguments base_type_max !_ !_ / . Global Arguments TypeUtil.base_type_min _ _ _ / _. +Global Arguments TypeUtil.base_type_max _ _ _ / _. Definition Castb {var} A A' (v : exprf base_type op (var:=var) (Tbase A)) : exprf base_type op (var:=var) (Tbase A') |