formal_lp/old/formal_interval/interval_m/line_interval.hl

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