formal_lp/old/formal_interval/interval_1d/line_interval.hl

   1 (* port of lineInterval.cc.
   2    Only the top section has been translated.  The rest should be
   3    automatically generated from HOL Light specs.
   4
   5    This impements basic operations on the type line,
   6    such as addition and scalar multiplication.
   7
   8  *)
   9
  10 flyspeck_needs "../formal_lp/formal_interval/interval_1d/interval.hl";;
  11
  12 module Line_interval = struct
  13
  14   open List;;
  15   open Interval;;
  16
  17
  18 (* general utilities *)
  19 (*  let iter6 = 0--5;;
  20
  21   let table f = map f iter6;;
  22
  23   let table2 f = map (fun i -> map (fun j-> f i j) iter6) iter6;;
  24
  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));;
  27
  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 );;
  30
  31   let mth2 a i j = mth (mth a i) j;;
  32
  33   let maxl xs = end_itlist max xs;;
  34
  35   let minl xs = end_itlist min xs;;
  36 *)
  37 (* line interval proper *)
  38
  39 (*
  40 let partial line i = mth line.df i ;;
  41 *)
  42
  43 let mk_line(f1,df1) = { f = f1; df = df1};;
  44
  45 let line_zero =
  46   let z = zero in
  47   mk_line(z,z);;
  48
  49 let line_unit =
  50   mk_line(one,zero);;
  51
  52 let lmul =
  53   let ( * ) = imul in
  54   let ( + ) = iadd in
  55   fun a b -> mk_line ( a.f * b.f, a.f * b.df + b.f * a.df );;
  56
  57 let smul =
  58   let ( * ) = imul in
  59   fun a b -> mk_line ( a.f * b, a.df * b )
  60
  61 let ldiv =
  62   let one = mk_interval(1.0,1.0) in
  63   let ( * ) = imul in
  64   let ( - ) = isub in
  65   let ( / ) = idiv in
  66   fun b a ->
  67     let r = one/a.f in
  68     let f = b.f * r in
  69     let r2 = r * r in
  70     mk_line ( f, (b.df * a.f - a.df * b.f) * r2 );;
  71
  72 let ladd =
  73   let ( + ) = iadd in
  74     fun b a ->
  75       mk_line(b.f + a.f, b.df + a.df);;
  76
  77 let lsub =
  78   let ( - ) = isub in
  79     fun b a ->
  80       mk_line(b.f - a.f, b.df - a.df);;
  81
  82 let lneg =
  83   let ineg = ineg in
  84     fun a ->
  85       mk_line(ineg a.f, ineg a.df);;
  86
  87 let lsqrt =
  88   let one = mk_interval(1.0,1.0) in
  89   let two = mk_interval(2.0,2.0) in
  90   let ( * ) = imul in
  91   let ( / ) = idiv in
  92   fun a ->
  93     let f = isqrt a.f in
  94     let rs = one / (two * f) in
  95       mk_line(f, a.df * rs);;
  96
  97 let latan = (* arctan (a/b) *)
  98   let one = mk_interval(1.0,1.0) in
  99   let ( * ) = imul in
 100   let ( + ) = iadd in
 101   let ( - ) = isub in
 102   let ( / ) = idiv in
 103   fun a b ->
 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));;
 107
 108
 109  end;;