formal_ineqs/verifier/interval_m/line_interval.ml

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