Update from HH
[Flyspeck/.git] / 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 *)