1 (* port of lineInterval.cc.
2 Only the top section has been translated. The rest should be
3 automatically generated from HOL Light specs.
5 This impements basic operations on the type line,
6 such as addition and scalar multiplication.
10 flyspeck_needs "../formal_lp/formal_interval/interval_1d/interval.hl";;
12 module Line_interval = struct
18 (* general utilities *)
21 let table f = map f iter6;;
23 let table2 f = map (fun i -> map (fun j-> f i j) iter6) iter6;;
25 let rth m x i = if (i >=0) && (i < m) then List.nth x i else
26 failwith (Printf.sprintf "index %d not in 0..%d" i (m-1));;
28 let mth x i = if (i >=0) && (i < 6) then List.nth x i else
29 failwith (Printf.sprintf "index %d not in 0..6" i );;
31 let mth2 a i j = mth (mth a i) j;;
33 let maxl xs = end_itlist max xs;;
35 let minl xs = end_itlist min xs;;
37 (* line interval proper *)
40 let partial line i = mth line.df i ;;
43 let mk_line(f1,df1) = { f = f1; df = df1};;
55 fun a b -> mk_line ( a.f * b.f, a.f * b.df + b.f * a.df );;
59 fun a b -> mk_line ( a.f * b, a.df * b )
62 let one = mk_interval(1.0,1.0) in
70 mk_line ( f, (b.df * a.f - a.df * b.f) * r2 );;
75 mk_line(b.f + a.f, b.df + a.df);;
80 mk_line(b.f - a.f, b.df - a.df);;
85 mk_line(ineg a.f, ineg a.df);;
88 let one = mk_interval(1.0,1.0) in
89 let two = mk_interval(2.0,2.0) in
94 let rs = one / (two * f) in
95 mk_line(f, a.df * rs);;
97 let latan = (* arctan (a/b) *)
98 let one = mk_interval(1.0,1.0) in
104 let f = iatan (a.f/b.f) in
105 let rden = one/ (a.f * a.f + b.f * b.f) in
106 mk_line(f, rden * (a.df * b.f - b.df * a.f));;