blob: 05037456263d1c0af319080db1b7e567800b09b9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Util.Notations.
Local Open Scope expr_scope.
Section language.
Context {base_type_code : Type}
(base_type_beq : base_type_code -> base_type_code -> bool)
(base_type_leb : base_type_code -> base_type_code -> bool).
Local Infix "<=?" := base_type_leb : expr_scope.
Local Infix "=?" := base_type_beq : expr_scope.
Definition base_type_min (a b : base_type_code) : base_type_code
:= if a <=? b then a else b.
Definition base_type_max (a b : base_type_code) : base_type_code
:= if a <=? b then b else a.
Section gen.
Context (join : base_type_code -> base_type_code -> base_type_code).
Fixpoint flat_type_join {t : flat_type base_type_code}
: interp_flat_type (fun _ => base_type_code) t -> option base_type_code
:= match t with
| Tbase _ => fun v => Some v
| Unit => fun _ => None
| Prod A B
=> fun v => match @flat_type_join A (fst v), @flat_type_join B (snd v) with
| Some a, Some b => Some (join a b)
| Some a, None => Some a
| None, Some b => Some b
| None, None => None
end
end.
End gen.
Definition flat_type_min {t} := @flat_type_join base_type_min t.
Definition flat_type_max {t} := @flat_type_join base_type_max t.
End language.
|
