(* definitions by functional composition.

    This file doesn't contain working code yet.
   It is a stub to be used later for the automatic generation of
   code.

 *)

(* primitive functions:
   unit, x1, x2, x3, x4, x5, x6, etc.

   The point of this file is to set up constants so that they
   can be automatically generated from the definitions into
   a form that the ocaml interval arithmetic verifier can use.

*)


let deriv_data6 = new_definition 
 `deriv_data6 p f (df1,df2,df3,df4,df5,df6) (x1,x2,x3,x4,x5,x6) <=>
   (derived_form p (\x1. f x1 x2 x3 x4 x5 x6) df1 x1 (:real) ) /\
   (derived_form p (\x2. f x1 x2 x3 x4 x5 x6) df2 x2 (:real) ) /\
   (derived_form p (\x3. f x1 x2 x3 x4 x5 x6) df3 x3 (:real) ) /\
   (derived_form p (\x4. f x1 x2 x3 x4 x5 x6) df4 x4 (:real) ) /\
   (derived_form p (\x5. f x1 x2 x3 x4 x5 x6) df5 x5 (:real) ) /\
   (derived_form p (\x6. f x1 x2 x3 x4 x5 x6) df6 x6 (:real) )`;;

let tf_primitive = 
[
"tf_x1";"tf_x2";"tf_x3";"tf_x4";"tf_x5";"tf_x6";"tf_unit";
"tf_delta_x";"tf_delta_x4";"tf_sol_x";"tf_dih_x";"tf_rad2_x";
]


let tf_compose = new_definition `tf_compose = ( o ):(B->C)->(A->B)->(A->C)`;;


let tf_plus = new_definition `tf_plus (f) 
  (g:real->real->real->real->real->real->real)  x1 x2 x3 x4 x5 x6 
  = f x1 x2 x3 x4 x5 x6 + g x1 x2 x3 x4 x5 x6`;;


let tf_scale = new_definition `tf_scale  
  (g:real->real->real->real->real->real->real) t  x1 x2 x3 x4 x5 x6 =
   (g x1 x2 x3 x4 x5 x6) * t`;;


let tf_product = new_definition `tf_product f 
  (g:real->real->real->real->real->real->real)  x1 x2 x3 x4 x5 x6
  = f x1 x2 x3 x4 x5 x6  * g x1 x2 x3 x4 x5 x6`;;


let tf_uni = new_definition `tf_uni
  (f:real->real)
    (g:real->real->real->real->real->real->real)  x1 x2 x3 x4 x5 x6 =
  f(g x1 x2 x3 x4 x5 x6)`;;


let tf_unit = new_definition `(tf_unit: real->real->real->real->real->real->real)
  x1 x2 x3 x4 x5 x6 = &1`;;


let tf_x1 = new_definition `(tf_x1: real->real->real->real->real->real->real)
  x1 x2 x3 x4 x5 x6 = x1`;;


let tf_x2 = new_definition `(tf_x2: real->real->real->real->real->real->real)
  x1 x2 x3 x4 x5 x6 = x2`;;


let tf_x3 = new_definition `(tf_x3: real->real->real->real->real->real->real)
  x1 x2 x3 x4 x5 x6 = x3`;;


let tf_x4 = new_definition `(tf_x4: real->real->real->real->real->real->real)
  x1 x2 x3 x4 x5 x6 = x4`;;


let tf_x5 = new_definition `(tf_x5: real->real->real->real->real->real->real)
  x1 x2 x3 x4 x5 x6 = x5`;;


let tf_x6 = new_definition `(tf_x6: real->real->real->real->real->real->real)
  x1 x2 x3 x4 x5 x6 = x6`;;


let tf_y1 = new_definition `tf_y1 = tf_uni sqrt tf_x1`;;


let tf_y2 = new_definition `tf_y2 = tf_uni sqrt tf_x2`;;


let tf_y3 = new_definition `tf_y3 = tf_uni sqrt tf_x3`;;


let tf_y4 = new_definition `tf_y4 = tf_uni sqrt tf_x4`;;


let tf_y5 = new_definition `tf_y5 = tf_uni sqrt tf_x5`;;


let tf_y6 = new_definition `tf_y6 = tf_uni sqrt tf_x6`;;


let tf_delta_x = new_definition `tf_delta_x = delta_x`;;
 


let tf_delta_x4 = new_definition `tf_delta_x4 = delta_x4`;;
 


let tf_delta4_squared_x = new_definition `tf_delta4_squared_x =
  tf_product tf_delta_x4 tf_delta_x4`;;


let i_one_twelfth = new_definition `i_one_twelfth = &1 / &12`;;
let i_half = new_definition `i_half = &1 / &2`;;
let i_mone = new_definition `i_mone = -- &1`;;
let i_mhalf = new_definition `i_mhalf = -- &1 / &2`;;
let i_c1 = new_definition `i_c1 = &1 / (h0 - &1)`;;


let tf_vol_x = new_definition `tf_vol_x = 
  tf_scale (tf_uni sqrt tf_delta_x) i_one_twelfth`;;


let tf_sol_x = new_definition `tf_sol_x = sol_x`;;
 


let tf_rad2_x = new_definition `tf_rad2_x = rad2_x`;;


let tf_dih_x = new_definition `tf_dih_x = dih_x`;;
 


let tf_dih2_x = new_definition `tf_dih2_x = rotate2 tf_dih_x`;;


let tf_dih3_x = new_definition `tf_dih3_x = rotate3 tf_dih_x`;;


let tf_dih4_x = new_definition `tf_dih4_x = rotate4 tf_dih_x`;;


let tf_dih5_x = new_definition `tf_dih5_x = rotate5 tf_dih_x`;;


let tf_dih6_x = new_definition `tf_dih6_x = rotate6 tf_dih_x`;;


let tf_lfun_sqrtx1_div2 = new_definition `tf_lfun_sqrtx1_div2 = 
  tf_scale ( tf_plus (tf_scale tf_unit h0) (tf_scale tf_y1 i_mhalf))  i_c1`;;
 


let tf_ldih_x = new_definition `tf_ldih_x = tf_product
  tf_lfun_sqrtx1_div2 tf_dih_x`;;


let tf_ldih2_x = new_definition `tf_ldih2_x = rotate2 tf_ldih_x`;;


let tf_ldih3_x = new_definition `tf_ldih3_x = rotate3 tf_ldih_x`;;


let tf_ldih5_x = new_definition `tf_ldih5_x = rotate5 tf_ldih_x`;;


let tf_ldih6_x = new_definition `tf_ldih6_x = rotate6 tf_ldih_x`;;



(*

  FINISH:
  All of these need to be implemented in the compositional argument-free style.

  Some might no longer be used: num2?, rat1?, rat2?, den2?, monomials?

  Then treat the univariates in the same way....

	  upper_dih,
	  eulerA_x,

	  rhazim,rhazim2,rhazim3,
	  gchi1_x,gchi2_x,gchi3_x,gchi4_x,gchi5_x,gchi6_x,
	  x1cube,x1square,
	  num1,num2,num_combo1,
	  rat1,rat2,den2,
	  edge_flat2_x,
	  edge_flat_x,
	  flat_term_x,
	  taum_x,
	  halfbump_x1, halfbump_x4;

	//////////
	// functions on an upright,flat,or quasiregular:
	// circumradius squared of the four faces of a simplex:
	// The circumradius squared of the face (ijk) of a simplex is eta2_ijk;
	// Miscellaneous functions.
	//
	static const taylorFunction eta2_126,eta2_135,eta2_234,eta2_456,
	  vol3_x_sqrt,
	  vol3f_x_lfun,
	  vol3f_x_sqrt2_lmplus,
	  arclength_x_123,
	  arclength_x_234,
	  arclength_x_126,
	  arclength_x_345,
	  norm2hhx,
	  asn797k,asnFnhk,lfun_y1,
	  acs_sqrt_x1_d4,	  acs_sqrt_x2_d4;

	static const taylorFunction
	  sol_euler_x_div_sqrtdelta,
	  sol_euler345_x_div_sqrtdelta,
	  sol_euler156_x_div_sqrtdelta,
	  sol_euler246_x_div_sqrtdelta,
	  dih_x_div_sqrtdelta_posbranch,
	  dih2_x_div_sqrtdelta_posbranch,
	  dih3_x_div_sqrtdelta_posbranch,
	  dih4_x_div_sqrtdelta_posbranch,
	  dih5_x_div_sqrtdelta_posbranch,
	  dih6_x_div_sqrtdelta_posbranch,
	  ldih_x_div_sqrtdelta_posbranch,
	  ldih2_x_div_sqrtdelta_posbranch,
	  ldih3_x_div_sqrtdelta_posbranch,
	  ldih4_x_div_sqrtdelta_posbranch,
	  ldih5_x_div_sqrtdelta_posbranch,
	  ldih6_x_div_sqrtdelta_posbranch,
	  surf_x,
	  vol3r_126_x,

	  dih_x_126_s2,
	  dih2_x_126_s2,
	  dih3_x_126_s2,
	  dih4_x_126_s2,
	  dih5_x_126_s2,
	  dih6_x_126_s2,
	  ldih_x_126_s2,
	  ldih2_x_126_s2,
	  ldih6_x_126_s2,
	  dih_x_135_s2,
	  dih2_x_135_s2,
	  dih3_x_135_s2,
	  dih4_x_135_s2,
	  dih5_x_135_s2,
	  dih6_x_135_s2,
	  ldih_x_135_s2,
	  ldih3_x_135_s2,
	  ldih5_x_135_s2,

	  delta_x_135_s2,
	  delta_x_126_s2,

	  vol3_x_135_s2, 

	  gamma3f_x_vLR_lfun,
	  gamma3f_x_vLR0,
	  gamma3f_x_vL_lfun,  gamma3f_x_vL0,
	  gamma3f_x_v_lfun,  gamma3f_x_v0,


	  // dec 29 , 2010:

	  ldih_x_126_n,
	  ldih2_x_126_n,
	  ldih6_x_126_n,
	  ldih_x_135_n,
	  ldih3_x_135_n,
	  ldih5_x_135_n,

          gamma3f_126_x_s_n,
	  gamma3f_135_x_s_n,
	  gamma3f_vLR_x_nlfun,
	  gamma3f_vLR_x_n0,
	  gamma3f_vL_x_nlfun,
	  gamma3f_vL_x_n0,

	  // may 2011:
	  tau_lowform_x,
	  tau_residual_x,
	  delta_y_LC,
	  euler_3flat_x,
	  euler_2flat_x,
	  euler_1flat_x,
	  taum_3flat_x,
	  taum_2flat_x,
	  taum_1flat_x,
	  delta_pent_x,

	  ;

	// construct x1^n1 .. x6^n6;
	static const taylorFunction monomial(int,int,int,int,int,int);

	static const taylorFunction taum_x1(const interval&,const interval&);
	static const taylorFunction taum_x2(const interval&,const interval&);
	static const taylorFunction taum_x1_x2(const interval&);

	static const taylorFunction arclength_x1(const interval&,const interval&);
	static const taylorFunction arclength_x2(const interval&,const interval&);

	static const taylorFunction surfR126d(const interval&);

	static const taylorFunction dih_template_B_x(const interval& x15,const interval& x45,
					const interval& x34,const interval& x12, 
					     const interval& x25);

	static const taylorFunction delta_template_B_x(const interval& x15,const interval& x45,
					const interval& x34,const interval& x12);


	static const taylorFunction /* taylorSimplex:: */ taum_template_B_x(const interval& x15,
								     const interval& x45,const interval& x34,const interval& x12   );

	static const taylorFunction /* taylorSimplex:: */ dih_hexall_x(const interval& x14, const interval& x12,
								const interval & x23);

	static const taylorFunction /* taylorSimplex:: */ dih1_hexall_x(const interval& x14, const interval& x12,
								const interval & x23);


	static const taylorFunction /* taylorSimplex:: */ upper_dih_hexall_x(const interval& x14, const interval& x12,
								const interval & x23);

	static const taylorFunction /* taylorSimplex:: */ delta_hexall_x(const interval& x14, const interval& x12,
								const interval & x23);

	static const taylorFunction /* taylorSimplex:: */ delta4_hexall_x(const interval& x14, const interval& x12,
								const interval & x23);


	static const taylorFunction /* taylorSimplex:: */ taum_hexall_x(const interval& x14, const interval& x12,
								const interval & x23);

	static const taylorFunction /* taylorSimplex:: */ eulerA_hexall_x(const interval& x14, const interval& x12,
								const interval & x23);

	static const taylorFunction /* taylorSimplex:: */ factor345_hexall_x(const interval& costheta);

	static const taylorFunction /* taylorSimplex:: */ law_cosines_234_x(const interval& costheta);

	static const taylorFunction /* taylorSimplex:: */ law_cosines_126_x(const interval& costheta);

	static const taylorFunction /* taylorSimplex:: */ lindih(const interval& theta);

	static const taylorFunction /* taylorSimplex:: */ delta_126_x(const interval& x3s, const interval& x4s, const interval& x5s);

	static const taylorFunction /* taylorSimplex:: */ delta_234_x(const interval& x1s, const interval& x5s, const interval& x6s);

	static const taylorFunction /* taylorSimplex:: */ delta_135_x(const interval& x2s, const interval& x4s, const interval& x6s);

	static const taylorFunction /* taylorSimplex:: */ taum_sub1_x(const interval& x1s);

	static const taylorFunction /* taylorSimplex:: */ delta_sub1_x(const interval& x1s);

	static const taylorFunction /* taylorSimplex:: */ taum_sub246_x(const interval& x2s,const interval& x4s,const interval& x6s);

	static const taylorFunction /* taylorSimplex:: */ taum_sub345_x(const interval& x3s,const interval& x4s,const interval& x5s);


};
*)