aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/FoldTypes.v
blob: 7b3059e438f3afbd652773cc74fd77f1649d8fb6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Syntax.Util.
Require Import Crypto.Compilers.FoldTypes.

Section min_or_max.
  Context (f : base_type -> base_type -> base_type)
          (init : base_type).

  Definition TypeFold {t} (e : Expr t) : base_type
    := TypeFold (fun t => t) f init e.
End min_or_max.

Definition MaxTypeUsed {t} (e : Expr t) : base_type
  := TypeFold base_type_max (TWord 0) e.
Definition MinTypeUsed {t} (e : Expr t) : base_type
  := TypeFold base_type_min TZ e.