source: extracted/floats.ml @ 2620

Last change on this file since 2620 was 2620, checked in by campbell, 7 years ago

Sufficient hacking to run the extracted Clight semantics.

File size: 1.8 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Coqlib
30
31open Arithmetic
32
33open Char
34
35open String
36
37open Vector
38
39open FoldStuff
40
41open BitVector
42
43open Extranat
44
45open Integers
46
47type float (* AXIOM TO BE REALIZED *)
48(*
49(** val fzero : float **)
50let fzero =
51  failwith "AXIOM TO BE REALIZED"
52
53(** val fone : float **)
54let fone =
55  failwith "AXIOM TO BE REALIZED"
56
57(** val fneg : float -> float **)
58let fneg =
59  failwith "AXIOM TO BE REALIZED"
60
61(** val fabs : float -> float **)
62let fabs =
63  failwith "AXIOM TO BE REALIZED"
64
65(** val singleoffloat : float -> float **)
66let singleoffloat =
67  failwith "AXIOM TO BE REALIZED"
68
69(** val intoffloat : Nat.nat -> float -> BitVector.bitVector **)
70let intoffloat =
71  failwith "AXIOM TO BE REALIZED"
72
73(** val intuoffloat : Nat.nat -> float -> BitVector.bitVector **)
74let intuoffloat =
75  failwith "AXIOM TO BE REALIZED"
76
77(** val floatofint : Nat.nat -> BitVector.bitVector -> float **)
78let floatofint =
79  failwith "AXIOM TO BE REALIZED"
80
81(** val floatofintu : Nat.nat -> BitVector.bitVector -> float **)
82let floatofintu =
83  failwith "AXIOM TO BE REALIZED"
84
85(** val fadd : float -> float -> float **)
86let fadd =
87  failwith "AXIOM TO BE REALIZED"
88
89(** val fsub : float -> float -> float **)
90let fsub =
91  failwith "AXIOM TO BE REALIZED"
92
93(** val fmul : float -> float -> float **)
94let fmul =
95  failwith "AXIOM TO BE REALIZED"
96
97(** val fdiv : float -> float -> float **)
98let fdiv =
99  failwith "AXIOM TO BE REALIZED"
100
101(** val fcmp : Integers.comparison -> float -> float -> Bool.bool **)
102let fcmp =
103  failwith "AXIOM TO BE REALIZED"
104
105(** val eq_dec0 : float -> float -> (__, __) Types.sum **)
106let eq_dec0 =
107  failwith "AXIOM TO BE REALIZED"
108*)
Note: See TracBrowser for help on using the repository browser.