Update from HH
[Flyspeck/.git] / port_interval / types.hl
1
2
3 exception Unstable;;  (* generally thrown when there is a divide by zero *)
4
5 exception Fatal;;  (* generally indicates an uncorrected bug *)
6
7 (* represents a closed interval [lo,hi] of the real line *)
8
9 type interval = {
10   lo : float;
11   hi : float;
12 };;
13
14 (* represents a function u:real->real, its derivative du, and 2nd derivative *)
15
16 type univariate = {
17   u : interval -> interval;
18   du : interval -> interval;
19   ddu : interval -> interval;
20 };;
21
22 (* represents the value f of function of six variables at some point y.
23    and the value df of its six partial derivatives, evaluated at the same point y.
24    The length of the list df should always be 6.
25 *)
26
27 type line = {
28   f : interval;
29   df : (interval) list;
30 };;
31
32 (*
33   represents approximation data for a function f on a rectangular domain [x,z].
34   l gives the value and partial derivatives of f at some point y in the domain.
35   dd gives interval bounds on the second derivatives over the entire domain.
36   w i is an upper bound on widths (z i - y i) and (y i - x i).
37 *)
38
39 type taylor_interval = {
40   l : line;
41   w : float list;
42   dd : interval list list;
43 };;
44
45
46