1 (* definitions by functional composition.
3 This file doesn't contain working code yet.
4 It is a stub to be used later for the automatic generation of
9 (* primitive functions:
10 unit, x1, x2, x3, x4, x5, x6, etc.
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.
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) )`;;
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";
33 let tf_compose = new_definition `tf_compose = ( o ):(B->C)->(A->B)->(A->C)`;;
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`;;
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`;;
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`;;
47 let tf_uni = new_definition `tf_uni
49 (g:real->real->real->real->real->real->real) x1 x2 x3 x4 x5 x6 =
50 f(g x1 x2 x3 x4 x5 x6)`;;
52 let tf_unit = new_definition `(tf_unit: real->real->real->real->real->real->real)
53 x1 x2 x3 x4 x5 x6 = &1`;;
55 let tf_x1 = new_definition `(tf_x1: real->real->real->real->real->real->real)
56 x1 x2 x3 x4 x5 x6 = x1`;;
58 let tf_x2 = new_definition `(tf_x2: real->real->real->real->real->real->real)
59 x1 x2 x3 x4 x5 x6 = x2`;;
61 let tf_x3 = new_definition `(tf_x3: real->real->real->real->real->real->real)
62 x1 x2 x3 x4 x5 x6 = x3`;;
64 let tf_x4 = new_definition `(tf_x4: real->real->real->real->real->real->real)
65 x1 x2 x3 x4 x5 x6 = x4`;;
67 let tf_x5 = new_definition `(tf_x5: real->real->real->real->real->real->real)
68 x1 x2 x3 x4 x5 x6 = x5`;;
70 let tf_x6 = new_definition `(tf_x6: real->real->real->real->real->real->real)
71 x1 x2 x3 x4 x5 x6 = x6`;;
73 let tf_y1 = new_definition `tf_y1 = tf_uni sqrt tf_x1`;;
75 let tf_y2 = new_definition `tf_y2 = tf_uni sqrt tf_x2`;;
77 let tf_y3 = new_definition `tf_y3 = tf_uni sqrt tf_x3`;;
79 let tf_y4 = new_definition `tf_y4 = tf_uni sqrt tf_x4`;;
81 let tf_y5 = new_definition `tf_y5 = tf_uni sqrt tf_x5`;;
83 let tf_y6 = new_definition `tf_y6 = tf_uni sqrt tf_x6`;;
85 let tf_delta_x = new_definition `tf_delta_x = delta_x`;;
87 let tf_delta_x4 = new_definition `tf_delta_x4 = delta_x4`;;
89 let tf_delta4_squared_x = new_definition `tf_delta4_squared_x =
90 tf_product tf_delta_x4 tf_delta_x4`;;
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)`;;
98 let tf_vol_x = new_definition `tf_vol_x =
99 tf_scale (tf_uni sqrt tf_delta_x) i_one_twelfth`;;
101 let tf_sol_x = new_definition `tf_sol_x = sol_x`;;
103 let tf_rad2_x = new_definition `tf_rad2_x = rad2_x`;;
105 let tf_dih_x = new_definition `tf_dih_x = dih_x`;;
107 let tf_dih2_x = new_definition `tf_dih2_x = rotate2 tf_dih_x`;;
109 let tf_dih3_x = new_definition `tf_dih3_x = rotate3 tf_dih_x`;;
111 let tf_dih4_x = new_definition `tf_dih4_x = rotate4 tf_dih_x`;;
113 let tf_dih5_x = new_definition `tf_dih5_x = rotate5 tf_dih_x`;;
115 let tf_dih6_x = new_definition `tf_dih6_x = rotate6 tf_dih_x`;;
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`;;
120 let tf_ldih_x = new_definition `tf_ldih_x = tf_product
121 tf_lfun_sqrtx1_div2 tf_dih_x`;;
123 let tf_ldih2_x = new_definition `tf_ldih2_x = rotate2 tf_ldih_x`;;
125 let tf_ldih3_x = new_definition `tf_ldih3_x = rotate3 tf_ldih_x`;;
127 let tf_ldih5_x = new_definition `tf_ldih5_x = rotate5 tf_ldih_x`;;
129 let tf_ldih6_x = new_definition `tf_ldih6_x = rotate6 tf_ldih_x`;;
136 All of these need to be implemented in the compositional argument-free style.
138 Some might no longer be used: num2?, rat1?, rat2?, den2?, monomials?
140 Then treat the univariates in the same way....
145 rhazim,rhazim2,rhazim3,
146 gchi1_x,gchi2_x,gchi3_x,gchi4_x,gchi5_x,gchi6_x,
148 num1,num2,num_combo1,
154 halfbump_x1, halfbump_x4;
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.
162 static const taylorFunction eta2_126,eta2_135,eta2_234,eta2_456,
165 vol3f_x_sqrt2_lmplus,
171 asn797k,asnFnhk,lfun_y1,
172 acs_sqrt_x1_d4, acs_sqrt_x2_d4;
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,
220 gamma3f_x_vL_lfun, gamma3f_x_vL0,
221 gamma3f_x_v_lfun, gamma3f_x_v0,
254 // construct x1^n1 .. x6^n6;
255 static const taylorFunction monomial(int,int,int,int,int,int);
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&);
261 static const taylorFunction arclength_x1(const interval&,const interval&);
262 static const taylorFunction arclength_x2(const interval&,const interval&);
264 static const taylorFunction surfR126d(const interval&);
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);
270 static const taylorFunction delta_template_B_x(const interval& x15,const interval& x45,
271 const interval& x34,const interval& x12);
274 static const taylorFunction /* taylorSimplex:: */ taum_template_B_x(const interval& x15,
275 const interval& x45,const interval& x34,const interval& x12 );
277 static const taylorFunction /* taylorSimplex:: */ dih_hexall_x(const interval& x14, const interval& x12,
278 const interval & x23);
280 static const taylorFunction /* taylorSimplex:: */ dih1_hexall_x(const interval& x14, const interval& x12,
281 const interval & x23);
284 static const taylorFunction /* taylorSimplex:: */ upper_dih_hexall_x(const interval& x14, const interval& x12,
285 const interval & x23);
287 static const taylorFunction /* taylorSimplex:: */ delta_hexall_x(const interval& x14, const interval& x12,
288 const interval & x23);
290 static const taylorFunction /* taylorSimplex:: */ delta4_hexall_x(const interval& x14, const interval& x12,
291 const interval & x23);
294 static const taylorFunction /* taylorSimplex:: */ taum_hexall_x(const interval& x14, const interval& x12,
295 const interval & x23);
297 static const taylorFunction /* taylorSimplex:: */ eulerA_hexall_x(const interval& x14, const interval& x12,
298 const interval & x23);
300 static const taylorFunction /* taylorSimplex:: */ factor345_hexall_x(const interval& costheta);
302 static const taylorFunction /* taylorSimplex:: */ law_cosines_234_x(const interval& costheta);
304 static const taylorFunction /* taylorSimplex:: */ law_cosines_126_x(const interval& costheta);
306 static const taylorFunction /* taylorSimplex:: */ lindih(const interval& theta);
308 static const taylorFunction /* taylorSimplex:: */ delta_126_x(const interval& x3s, const interval& x4s, const interval& x5s);
310 static const taylorFunction /* taylorSimplex:: */ delta_234_x(const interval& x1s, const interval& x5s, const interval& x6s);
312 static const taylorFunction /* taylorSimplex:: */ delta_135_x(const interval& x2s, const interval& x4s, const interval& x6s);
314 static const taylorFunction /* taylorSimplex:: */ taum_sub1_x(const interval& x1s);
316 static const taylorFunction /* taylorSimplex:: */ delta_sub1_x(const interval& x1s);
318 static const taylorFunction /* taylorSimplex:: */ taum_sub246_x(const interval& x2s,const interval& x4s,const interval& x6s);
320 static const taylorFunction /* taylorSimplex:: */ taum_sub345_x(const interval& x3s,const interval& x4s,const interval& x5s);