-
Notifications
You must be signed in to change notification settings - Fork 0
/
ModRecFNToFN.v
28 lines (22 loc) · 846 Bytes
/
ModRecFNToFN.v
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
Require Import Kami.AllNotations FpuKami.Definitions String.
Section FNFromRecFN.
Variable name: string.
Variable expWidthMinus2 sigWidthMinus2: nat.
Local Notation "^ x" := (name ++ "#" ++ x)%string (at level 100).
Open Scope kami_expr.
Definition RecFNToFN_module :=
MODULE {
Rule ^"RecFNToFN" :=
Call input: RecFN expWidthMinus2 sigWidthMinus2 <- "input" ();
LET nf <- getNF_from_RecFN #input;
Call "nf" (#nf: _);
LET recfn <- getFN_from_NF #nf;
(* LET recfn: _ <- (getFN_from_RecFN #input); *)
Call "output" (#recfn: _);
Retv
}.
Close Scope kami_expr.
End FNFromRecFN.
Definition RecF16ToF16 := RecFNToFN_module "fpu" 6 6.
Definition RecF32ToF32 := RecFNToFN_module "fpu" 6 22.
Definition RecF64ToF64 := RecFNToFN_module "fpu" 9 51.