-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathfloat32.v
96 lines (83 loc) · 4.79 KB
/
float32.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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
Set Implicit Arguments.
Unset Strict Implicit.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import List. Import ListNotations.
Require Import Reals Rpower.
Require Import Extraction.
Require Import MLCert.axioms MLCert.extraction_hs.
(*Axiomatized 32-bit floating point numbers, together with cardinality axioms.
Currently Haskell-only: OCaml's float is double-precision by default; nor does
the OCaml standard support a single-precision 32-bit FP type.*)
(*32-bit floating-point numbers*)
Axiom float32 : Type.
Axiom float32_finite : Finite.class_of float32.
Definition float32_finType : finType := Finite.Pack float32_finite.
Axiom float32_card : #|float32_finType| = 2^32.
Extract Constant float32 => "Prelude.Float".
(*Arrays of 32-bit floats, implemented as AxVec's*)
Definition float32_arr (n:nat) := AxVec n float32. (*size-indexed float32 arrays*)
Lemma float32_arr_finite : forall n:nat, Finite.class_of (float32_arr n).
Proof. move => n; rewrite /float32_arr; apply: (AxVec_finite n float32_finType). Defined.
Definition float32_arr_finType (n:nat) : finType :=
Finite.Pack (float32_arr_finite n) .
Lemma float32_arr_card : forall n, #|float32_arr_finType n| = 2^(n*32).
Proof. by move => n; move: (@AxVec_card n 32 float32_finType float32_card) => /= <-. Qed.
(*Axiomatized arithmetic expressions over float32's and float arrays*)
Axiom f32_0 : float32.
Axiom f32_1 : float32.
Axiom f32_opp : float32 -> float32.
Axiom f32_gt : float32 -> float32 -> bool.
Axiom f32_add : float32 -> float32 -> float32.
Axiom f32_mult : float32 -> float32 -> float32.
Axiom f32_div : float32 -> float32 -> float32.
Axiom f32_pow : float32 -> float32 -> float32.
Axiom f32_eq : float32 -> float32 -> bool.
Axiom f32_init : forall (n:nat)(init:float32), float32_arr n.
Axiom f32_map : forall (n:nat)(f:float32->float32)(a:float32_arr n), float32_arr n.
Axiom f32_mapM : forall (M:Type->Type)(n:nat)(f:float32->M float32)(a:float32_arr n), M (float32_arr n).
Axiom f32_map2 : forall (n:nat)(f:float32->float32->float32)(a b:float32_arr n), float32_arr n.
Axiom f32_fold2 : forall (T:Type)(n:nat)(t0:T)(f:float32->float32->T->T)(a1 a2:float32_arr n), T.
Axiom f32_get : forall (n:nat)(i:'I_n)(a:float32_arr n), float32.
Axiom f32_upd : forall (n:nat)(i:'I_n)(new:float32)(a:float32_arr n), float32_arr n.
Axiom f32_get_f32 : forall (n:nat)(f:float32)(a:float32_arr n), float32.
Axiom f32_upd_f32 : forall (n:nat)(f new:float32)(a:float32_arr n), float32_arr n.
Extract Constant f32_0 => "(0.0 :: Prelude.Float)".
Extract Constant f32_1 => "(1.0 :: Prelude.Float)".
Extract Constant f32_opp => "(\f -> - f)".
Extract Constant f32_gt => "(\f1 f2 -> (Prelude.>) f1 f2)".
Extract Constant f32_add => "(\f1 f2 -> (Prelude.+) f1 f2)".
Extract Constant f32_mult => "(\f1 f2 -> (Prelude.*) f1 f2)".
Extract Constant f32_div => "(\f1 f2 -> (Prelude./) f1 f2)".
Extract Constant f32_pow => "(\f1 f2 -> (Prelude.**) f1 f2)".
Extract Constant f32_eq => "(\f1 f2 -> (Prelude.==) f1 f2)".
Extract Constant f32_init =>
"(\n init -> case n of
O -> []
S n1 -> init : f32_init n1 init)".
Extract Constant f32_map => "(\_ f a -> Prelude.map f a)".
Extract Constant f32_mapM => "(\_ f a -> Prelude.mapM f a)".
Extract Constant f32_map2 => "(\_ f a1 a2 -> Prelude.map (\(x,y) -> f x y) (Prelude.zip a1 a2))".
Extract Constant f32_fold2 => "(\_ t f a1 a2 -> Prelude.foldl (\acc (x, y) -> f x y acc) t (Prelude.zip a1 a2))".
Extract Constant f32_get => "(\_ i a -> (if (eqn i O) then (Prelude.head a) else (let (S x) = i in (f32_get O x (Prelude.tail a)))))".
Extract Constant f32_upd => "(\_ i new a -> (if (eqn i O) then ([new] Prelude.++ (Prelude.tail a)) else (let (S x) = i in ([Prelude.head a] Prelude.++ (f32_upd O x new (Prelude.tail a))))))".
Extract Constant f32_get_f32 => "(\_ f a -> if (f == 0.0) then (Prelude.head a) else (f32_get_f32 O (f - 1.0) (Prelude.tail a)))".
Extract Constant f32_upd_f32 => "(\_ f new a -> (if (f == 0.0) then ([new] Prelude.++ (Prelude.tail a)) else ([Prelude.head a] Prelude.++ (f32_upd_f32 O (f - 1.0) new (Prelude.tail a))))".
(*Notation and derived operations*)
Notation "0" := (f32_0) : f32_scope.
Notation "1" := (f32_1) : f32_scope.
Notation "2" := (f32_add f32_1 f32_1) : f32_scope.
Infix ">" := (f32_gt) : f32_scope.
Infix "+" := (f32_add) : f32_scope.
Infix "*" := (f32_mult) : f32_scope.
Infix "/" := (f32_div) : f32_scope.
Infix "**" := (f32_pow) (at level 20, left associativity) : f32_scope.
Infix "==" := (f32_eq) : f32_scope.
Definition neg1 : float32 := f32_opp f32_1.
Definition float32_of_bool (b:bool) := if b then f32_1 else neg1.
Coercion float32_of_bool : bool >-> float32.
Section f32_definitions.
Open Scope f32_scope.
Definition f32_dot (n:nat) (a1 a2:float32_arr n) : float32 :=
f32_fold2 0 (fun x1 x2 sum => (x1 * x2) + sum) a1 a2.
End f32_definitions.