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 "../port_interval/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 *)
39 let partial line i = mth line.df i ;;
41 let mk_line(f1,df1) = { f = f1; df =df1};;
45 mk_line(z,replicate z 6);;
48 mk_line(one,replicate zero 6);;
53 fun a b -> mk_line ( a.f * b.f, map (fun i -> a.f * mth b.df i + b.f * mth a.df i) iter6);;
57 fun a b -> mk_line ( a.f * b, map (fun x -> x * b) a.df);;
60 let one = mk_interval(1.0,1.0) in
68 mk_line ( f, map (fun i -> ((mth b.df i) * a.f - (mth a.df i) * b.f)* r2) iter6);;
73 mk_line(b.f + a.f, map (fun i -> mth b.df i + mth a.df i) iter6);;
78 mk_line(b.f - a.f, map (fun i -> mth b.df i - mth a.df i) iter6);;
83 mk_line(ineg a.f, map ineg a.df);;
86 let one = mk_interval(1.0,1.0) in
87 let two = mk_interval(2.0,2.0) in
92 let rs = one / (two * f) in
93 mk_line(f, map (fun i -> mth a.df i * rs) iter6);;
95 let latan = (* arctan (a/b) *)
96 let one = mk_interval(1.0,1.0) in
102 let f = iatan (a.f/b.f) in
103 let rden = one/ (a.f * a.f + b.f * b.f) in
104 mk_line(f, map (fun i -> rden * (mth a.df i * b.f - mth b.df i * a.f)) iter6);;