port_interval/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 "../port_interval/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 let partial line i = mth line.df i ;;
  40
  41 let mk_line(f1,df1) = { f = f1; df =df1};;
  42
  43 let line_zero =
  44   let z = zero in
  45   mk_line(z,replicate z 6);;
  46
  47 let line_unit =
  48   mk_line(one,replicate zero 6);;
  49
  50 let lmul =
  51   let ( * ) = imul in
  52   let ( + ) = iadd in
  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);;
  54
  55 let smul =
  56   let ( * ) = imul in
  57   fun a b -> mk_line ( a.f * b, map (fun x -> x * b) a.df);;
  58
  59 let ldiv =
  60   let one = mk_interval(1.0,1.0) in
  61   let ( * ) = imul in
  62   let ( - ) = isub in
  63   let ( / ) = idiv in
  64   fun b a ->
  65     let r = one/a.f in
  66     let f = b.f * r in
  67     let r2 = r * r in
  68     mk_line ( f, map (fun i -> ((mth b.df i) * a.f - (mth a.df i) * b.f)* r2) iter6);;
  69
  70 let ladd =
  71   let ( + ) = iadd in
  72     fun b a ->
  73       mk_line(b.f + a.f, map (fun i -> mth b.df i + mth a.df i) iter6);;
  74
  75 let lsub =
  76   let ( - ) = isub in
  77     fun b a ->
  78       mk_line(b.f - a.f, map (fun i -> mth b.df i - mth a.df i) iter6);;
  79
  80 let lneg =
  81   let ineg = ineg in
  82     fun a ->
  83       mk_line(ineg a.f, map ineg a.df);;
  84
  85 let lsqrt =
  86   let one = mk_interval(1.0,1.0) in
  87   let two = mk_interval(2.0,2.0) in
  88   let ( * ) = imul in
  89   let ( / ) = idiv in
  90   fun a ->
  91     let f = isqrt a.f in
  92     let rs = one / (two * f) in
  93       mk_line(f, map (fun i -> mth a.df i * rs) iter6);;
  94
  95 let latan = (* arctan (a/b) *)
  96   let one = mk_interval(1.0,1.0) in
  97   let ( * ) = imul in
  98   let ( + ) = iadd in
  99   let ( - ) = isub in
 100   let ( / ) = idiv in
 101   fun a b ->
 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);;
 105
 106
 107  end;;