port_interval/compose.hl

   1 (* definitions by functional composition.
   2
   3     This file doesn't contain working code yet.
   4    It is a stub to be used later for the automatic generation of
   5    code.
   6
   7  *)
   8
   9 (* primitive functions:
  10    unit, x1, x2, x3, x4, x5, x6, etc.
  11
  12    The point of this file is to set up constants so that they
  13    can be automatically generated from the definitions into
  14    a form that the ocaml interval arithmetic verifier can use.
  15
  16 *)
  17
  18 let deriv_data6 = new_definition
  19  `deriv_data6 p f (df1,df2,df3,df4,df5,df6) (x1,x2,x3,x4,x5,x6) <=>
  20    (derived_form p (\x1. f x1 x2 x3 x4 x5 x6) df1 x1 (:real) ) /\
  21    (derived_form p (\x2. f x1 x2 x3 x4 x5 x6) df2 x2 (:real) ) /\
  22    (derived_form p (\x3. f x1 x2 x3 x4 x5 x6) df3 x3 (:real) ) /\
  23    (derived_form p (\x4. f x1 x2 x3 x4 x5 x6) df4 x4 (:real) ) /\
  24    (derived_form p (\x5. f x1 x2 x3 x4 x5 x6) df5 x5 (:real) ) /\
  25    (derived_form p (\x6. f x1 x2 x3 x4 x5 x6) df6 x6 (:real) )`;;
  26
  27 let tf_primitive =
  28 [
  29 "tf_x1";"tf_x2";"tf_x3";"tf_x4";"tf_x5";"tf_x6";"tf_unit";
  30 "tf_delta_x";"tf_delta_x4";"tf_sol_x";"tf_dih_x";"tf_rad2_x";
  31 ]
  32
  33 let tf_compose = new_definition `tf_compose = ( o ):(B->C)->(A->B)->(A->C)`;;
  34
  35 let tf_plus = new_definition `tf_plus (f)
  36   (g:real->real->real->real->real->real->real)  x1 x2 x3 x4 x5 x6
  37   = f x1 x2 x3 x4 x5 x6 + g x1 x2 x3 x4 x5 x6`;;
  38
  39 let tf_scale = new_definition `tf_scale
  40   (g:real->real->real->real->real->real->real) t  x1 x2 x3 x4 x5 x6 =
  41    (g x1 x2 x3 x4 x5 x6) * t`;;
  42
  43 let tf_product = new_definition `tf_product f
  44   (g:real->real->real->real->real->real->real)  x1 x2 x3 x4 x5 x6
  45   = f x1 x2 x3 x4 x5 x6  * g x1 x2 x3 x4 x5 x6`;;
  46
  47 let tf_uni = new_definition `tf_uni
  48   (f:real->real)
  49     (g:real->real->real->real->real->real->real)  x1 x2 x3 x4 x5 x6 =
  50   f(g x1 x2 x3 x4 x5 x6)`;;
  51
  52 let tf_unit = new_definition `(tf_unit: real->real->real->real->real->real->real)
  53   x1 x2 x3 x4 x5 x6 = &1`;;
  54
  55 let tf_x1 = new_definition `(tf_x1: real->real->real->real->real->real->real)
  56   x1 x2 x3 x4 x5 x6 = x1`;;
  57
  58 let tf_x2 = new_definition `(tf_x2: real->real->real->real->real->real->real)
  59   x1 x2 x3 x4 x5 x6 = x2`;;
  60
  61 let tf_x3 = new_definition `(tf_x3: real->real->real->real->real->real->real)
  62   x1 x2 x3 x4 x5 x6 = x3`;;
  63
  64 let tf_x4 = new_definition `(tf_x4: real->real->real->real->real->real->real)
  65   x1 x2 x3 x4 x5 x6 = x4`;;
  66
  67 let tf_x5 = new_definition `(tf_x5: real->real->real->real->real->real->real)
  68   x1 x2 x3 x4 x5 x6 = x5`;;
  69
  70 let tf_x6 = new_definition `(tf_x6: real->real->real->real->real->real->real)
  71   x1 x2 x3 x4 x5 x6 = x6`;;
  72
  73 let tf_y1 = new_definition `tf_y1 = tf_uni sqrt tf_x1`;;
  74
  75 let tf_y2 = new_definition `tf_y2 = tf_uni sqrt tf_x2`;;
  76
  77 let tf_y3 = new_definition `tf_y3 = tf_uni sqrt tf_x3`;;
  78
  79 let tf_y4 = new_definition `tf_y4 = tf_uni sqrt tf_x4`;;
  80
  81 let tf_y5 = new_definition `tf_y5 = tf_uni sqrt tf_x5`;;
  82
  83 let tf_y6 = new_definition `tf_y6 = tf_uni sqrt tf_x6`;;
  84
  85 let tf_delta_x = new_definition `tf_delta_x = delta_x`;;
  86
  87 let tf_delta_x4 = new_definition `tf_delta_x4 = delta_x4`;;
  88
  89 let tf_delta4_squared_x = new_definition `tf_delta4_squared_x =
  90   tf_product tf_delta_x4 tf_delta_x4`;;
  91
  92 let i_one_twelfth = new_definition `i_one_twelfth = &1 / &12`;;
  93 let i_half = new_definition `i_half = &1 / &2`;;
  94 let i_mone = new_definition `i_mone = -- &1`;;
  95 let i_mhalf = new_definition `i_mhalf = -- &1 / &2`;;
  96 let i_c1 = new_definition `i_c1 = &1 / (h0 - &1)`;;
  97
  98 let tf_vol_x = new_definition `tf_vol_x =
  99   tf_scale (tf_uni sqrt tf_delta_x) i_one_twelfth`;;
 100
 101 let tf_sol_x = new_definition `tf_sol_x = sol_x`;;
 102
 103 let tf_rad2_x = new_definition `tf_rad2_x = rad2_x`;;
 104
 105 let tf_dih_x = new_definition `tf_dih_x = dih_x`;;
 106
 107 let tf_dih2_x = new_definition `tf_dih2_x = rotate2 tf_dih_x`;;
 108
 109 let tf_dih3_x = new_definition `tf_dih3_x = rotate3 tf_dih_x`;;
 110
 111 let tf_dih4_x = new_definition `tf_dih4_x = rotate4 tf_dih_x`;;
 112
 113 let tf_dih5_x = new_definition `tf_dih5_x = rotate5 tf_dih_x`;;
 114
 115 let tf_dih6_x = new_definition `tf_dih6_x = rotate6 tf_dih_x`;;
 116
 117 let tf_lfun_sqrtx1_div2 = new_definition `tf_lfun_sqrtx1_div2 =
 118   tf_scale ( tf_plus (tf_scale tf_unit h0) (tf_scale tf_y1 i_mhalf))  i_c1`;;
 119
 120 let tf_ldih_x = new_definition `tf_ldih_x = tf_product
 121   tf_lfun_sqrtx1_div2 tf_dih_x`;;
 122
 123 let tf_ldih2_x = new_definition `tf_ldih2_x = rotate2 tf_ldih_x`;;
 124
 125 let tf_ldih3_x = new_definition `tf_ldih3_x = rotate3 tf_ldih_x`;;
 126
 127 let tf_ldih5_x = new_definition `tf_ldih5_x = rotate5 tf_ldih_x`;;
 128
 129 let tf_ldih6_x = new_definition `tf_ldih6_x = rotate6 tf_ldih_x`;;
 130
 131
 132
 133 (*
 134
 135   FINISH:
 136   All of these need to be implemented in the compositional argument-free style.
 137
 138   Some might no longer be used: num2?, rat1?, rat2?, den2?, monomials?
 139
 140   Then treat the univariates in the same way....
 141
 142           upper_dih,
 143           eulerA_x,
 144
 145           rhazim,rhazim2,rhazim3,
 146           gchi1_x,gchi2_x,gchi3_x,gchi4_x,gchi5_x,gchi6_x,
 147           x1cube,x1square,
 148           num1,num2,num_combo1,
 149           rat1,rat2,den2,
 150           edge_flat2_x,
 151           edge_flat_x,
 152           flat_term_x,
 153           taum_x,
 154           halfbump_x1, halfbump_x4;
 155
 156         //////////
 157         // functions on an upright,flat,or quasiregular:
 158         // circumradius squared of the four faces of a simplex:
 159         // The circumradius squared of the face (ijk) of a simplex is eta2_ijk;
 160         // Miscellaneous functions.
 161         //
 162         static const taylorFunction eta2_126,eta2_135,eta2_234,eta2_456,
 163           vol3_x_sqrt,
 164           vol3f_x_lfun,
 165           vol3f_x_sqrt2_lmplus,
 166           arclength_x_123,
 167           arclength_x_234,
 168           arclength_x_126,
 169           arclength_x_345,
 170           norm2hhx,
 171           asn797k,asnFnhk,lfun_y1,
 172           acs_sqrt_x1_d4,         acs_sqrt_x2_d4;
 173
 174         static const taylorFunction
 175           sol_euler_x_div_sqrtdelta,
 176           sol_euler345_x_div_sqrtdelta,
 177           sol_euler156_x_div_sqrtdelta,
 178           sol_euler246_x_div_sqrtdelta,
 179           dih_x_div_sqrtdelta_posbranch,
 180           dih2_x_div_sqrtdelta_posbranch,
 181           dih3_x_div_sqrtdelta_posbranch,
 182           dih4_x_div_sqrtdelta_posbranch,
 183           dih5_x_div_sqrtdelta_posbranch,
 184           dih6_x_div_sqrtdelta_posbranch,
 185           ldih_x_div_sqrtdelta_posbranch,
 186           ldih2_x_div_sqrtdelta_posbranch,
 187           ldih3_x_div_sqrtdelta_posbranch,
 188           ldih4_x_div_sqrtdelta_posbranch,
 189           ldih5_x_div_sqrtdelta_posbranch,
 190           ldih6_x_div_sqrtdelta_posbranch,
 191           surf_x,
 192           vol3r_126_x,
 193
 194           dih_x_126_s2,
 195           dih2_x_126_s2,
 196           dih3_x_126_s2,
 197           dih4_x_126_s2,
 198           dih5_x_126_s2,
 199           dih6_x_126_s2,
 200           ldih_x_126_s2,
 201           ldih2_x_126_s2,
 202           ldih6_x_126_s2,
 203           dih_x_135_s2,
 204           dih2_x_135_s2,
 205           dih3_x_135_s2,
 206           dih4_x_135_s2,
 207           dih5_x_135_s2,
 208           dih6_x_135_s2,
 209           ldih_x_135_s2,
 210           ldih3_x_135_s2,
 211           ldih5_x_135_s2,
 212
 213           delta_x_135_s2,
 214           delta_x_126_s2,
 215
 216           vol3_x_135_s2,
 217
 218           gamma3f_x_vLR_lfun,
 219           gamma3f_x_vLR0,
 220           gamma3f_x_vL_lfun,  gamma3f_x_vL0,
 221           gamma3f_x_v_lfun,  gamma3f_x_v0,
 222
 223
 224           // dec 29 , 2010:
 225
 226           ldih_x_126_n,
 227           ldih2_x_126_n,
 228           ldih6_x_126_n,
 229           ldih_x_135_n,
 230           ldih3_x_135_n,
 231           ldih5_x_135_n,
 232
 233           gamma3f_126_x_s_n,
 234           gamma3f_135_x_s_n,
 235           gamma3f_vLR_x_nlfun,
 236           gamma3f_vLR_x_n0,
 237           gamma3f_vL_x_nlfun,
 238           gamma3f_vL_x_n0,
 239
 240           // may 2011:
 241           tau_lowform_x,
 242           tau_residual_x,
 243           delta_y_LC,
 244           euler_3flat_x,
 245           euler_2flat_x,
 246           euler_1flat_x,
 247           taum_3flat_x,
 248           taum_2flat_x,
 249           taum_1flat_x,
 250           delta_pent_x,
 251
 252           ;
 253
 254         // construct x1^n1 .. x6^n6;
 255         static const taylorFunction monomial(int,int,int,int,int,int);
 256
 257         static const taylorFunction taum_x1(const interval&,const interval&);
 258         static const taylorFunction taum_x2(const interval&,const interval&);
 259         static const taylorFunction taum_x1_x2(const interval&);
 260
 261         static const taylorFunction arclength_x1(const interval&,const interval&);
 262         static const taylorFunction arclength_x2(const interval&,const interval&);
 263
 264         static const taylorFunction surfR126d(const interval&);
 265
 266         static const taylorFunction dih_template_B_x(const interval& x15,const interval& x45,
 267                                         const interval& x34,const interval& x12,
 268                                              const interval& x25);
 269
 270         static const taylorFunction delta_template_B_x(const interval& x15,const interval& x45,
 271                                         const interval& x34,const interval& x12);
 272
 273
 274         static const taylorFunction /* taylorSimplex:: */ taum_template_B_x(const interval& x15,
 275                                                                      const interval& x45,const interval& x34,const interval& x12   );
 276
 277         static const taylorFunction /* taylorSimplex:: */ dih_hexall_x(const interval& x14, const interval& x12,
 278                                                                 const interval & x23);
 279
 280         static const taylorFunction /* taylorSimplex:: */ dih1_hexall_x(const interval& x14, const interval& x12,
 281                                                                 const interval & x23);
 282
 283
 284         static const taylorFunction /* taylorSimplex:: */ upper_dih_hexall_x(const interval& x14, const interval& x12,
 285                                                                 const interval & x23);
 286
 287         static const taylorFunction /* taylorSimplex:: */ delta_hexall_x(const interval& x14, const interval& x12,
 288                                                                 const interval & x23);
 289
 290         static const taylorFunction /* taylorSimplex:: */ delta4_hexall_x(const interval& x14, const interval& x12,
 291                                                                 const interval & x23);
 292
 293
 294         static const taylorFunction /* taylorSimplex:: */ taum_hexall_x(const interval& x14, const interval& x12,
 295                                                                 const interval & x23);
 296
 297         static const taylorFunction /* taylorSimplex:: */ eulerA_hexall_x(const interval& x14, const interval& x12,
 298                                                                 const interval & x23);
 299
 300         static const taylorFunction /* taylorSimplex:: */ factor345_hexall_x(const interval& costheta);
 301
 302         static const taylorFunction /* taylorSimplex:: */ law_cosines_234_x(const interval& costheta);
 303
 304         static const taylorFunction /* taylorSimplex:: */ law_cosines_126_x(const interval& costheta);
 305
 306         static const taylorFunction /* taylorSimplex:: */ lindih(const interval& theta);
 307
 308         static const taylorFunction /* taylorSimplex:: */ delta_126_x(const interval& x3s, const interval& x4s, const interval& x5s);
 309
 310         static const taylorFunction /* taylorSimplex:: */ delta_234_x(const interval& x1s, const interval& x5s, const interval& x6s);
 311
 312         static const taylorFunction /* taylorSimplex:: */ delta_135_x(const interval& x2s, const interval& x4s, const interval& x6s);
 313
 314         static const taylorFunction /* taylorSimplex:: */ taum_sub1_x(const interval& x1s);
 315
 316         static const taylorFunction /* taylorSimplex:: */ delta_sub1_x(const interval& x1s);
 317
 318         static const taylorFunction /* taylorSimplex:: */ taum_sub246_x(const interval& x2s,const interval& x4s,const interval& x6s);
 319
 320         static const taylorFunction /* taylorSimplex:: */ taum_sub345_x(const interval& x3s,const interval& x4s,const interval& x5s);
 321
 322
 323 };
 324 *)