formal_ineqs/misc/vars.hl

   1 (* =========================================================== *)\r
   2 (* Commonly used variables and constants                       *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 module Misc_vars = struct\r
   8 \r
   9 (* bool variables *)\r
  10 let s_var_bool = `s:bool` and\r
  11         s1_var_bool = `s1:bool` and\r
  12         s2_var_bool = `s2:bool`;;\r
  13 \r
  14 (* num variables *)\r
  15 let n_var_num = `n:num` and\r
  16     m_var_num = `m:num` and\r
  17         t_var_num = `t:num` and\r
  18         p_var_num = `p:num` and\r
  19         q_var_num = `q:num` and\r
  20         k_var_num = `k:num` and\r
  21     e_var_num = `e:num` and\r
  22         e1_var_num = `e1:num` and\r
  23         e2_var_num = `e2:num` and\r
  24         r_var_num = `r:num` and\r
  25         r1_var_num = `r1:num` and\r
  26         r2_var_num = `r2:num` and\r
  27         n1_var_num = `n1:num` and\r
  28         n2_var_num = `n2:num` and\r
  29         m1_var_num = `m1:num` and\r
  30         m2_var_num = `m2:num` and\r
  31         x_var_num = `x:num` and\r
  32         y_var_num = `y:num` and\r
  33         i_var_num = `i:num` and\r
  34         j_var_num = `j:num`;;\r
  35 \r
  36 (* real variables *)\r
  37 let x_var_real = `x : real` and\r
  38     y_var_real = `y : real` and\r
  39         z_var_real = `z : real` and\r
  40     w_var_real = `w : real` and\r
  41         a_var_real = `a : real` and\r
  42         b_var_real = `b : real` and\r
  43         m_var_real = `m : real` and\r
  44         n_var_real = `n : real` and\r
  45         x1_var_real = `x1 : real` and\r
  46         x2_var_real = `x2 : real` and\r
  47         y1_var_real = `y1 : real` and\r
  48         y2_var_real = `y2 : real` and\r
  49         f1_var_real = `f1 : real` and\r
  50         f2_var_real = `f2 : real` and\r
  51     f_var_fun = `f : real->real` and\r
  52     g_var_fun = `g : real->real` and\r
  53     f1_var_fun = `f1 : real->real` and\r
  54     f2_var_fun = `f2 : real->real` and\r
  55     int_var = `int : real#real` and\r
  56     f_bounds_var = `f_bounds : real#real` and\r
  57     df_bounds_var = `df_bounds : real#real` and\r
  58     dd_bounds_var = `dd_bounds : real#real` and\r
  59     x_lo_var = `x_lo : real` and\r
  60     x_hi_var = `x_hi : real` and\r
  61         lo_var_real = `lo : real` and\r
  62         hi_var_real = `hi : real` and\r
  63     dd_var_real = `dd : real` and\r
  64     df_lo_var = `df_lo : real` and\r
  65     df_hi_var = `df_hi : real` and\r
  66     df_var_real = `df : real` and\r
  67     f_lo_var = `f_lo : real` and\r
  68     f_hi_var = `f_hi : real` and\r
  69         w1_var_real = `w1 : real` and\r
  70     w2_var_real = `w2 : real` and\r
  71     t_var_real = `t : real` and\r
  72     g_bounds_var = `g_bounds : real#real` and\r
  73     dg_bounds_var = `dg_bounds : real#real` and\r
  74     bounds_var = `bounds : real#real` and\r
  75     d_bounds_var = `d_bounds : real#real` and\r
  76     x0_var_real = `x0 : real` and\r
  77     z0_var_real = `z0 : real` and\r
  78     w0_var_real = `w0 : real` and\r
  79         error_var = `error : real` and\r
  80         d_bounds_list_var = `d_bounds_list : (real#real)list` and\r
  81         dd_bounds_list_var = `dd_bounds_list : ((real#real)list)list` and\r
  82         df_bounds_list_var = `df_bounds_list : (real#real)list` and\r
  83         dd_list_var = `dd_list : (real#real)list` and\r
  84         x_var_real_list = `x:(real)list` and\r
  85     y_var_real_list = `y:(real)list` and\r
  86     z_var_real_list = `z:(real)list` and\r
  87     w_var_real_list = `w:(real)list` and\r
  88     yw_var = `yw : (real#real)list` and\r
  89     xz_var = `xz : (real#real)list` and\r
  90     xz_pair_var = `xz : real#real` and\r
  91     yw_pair_var = `yw : real#real` and\r
  92         list_var_real_pair = `list : (real#real)list`;;\r
  93 \r
  94 (* bool constants *)\r
  95 let t_const = `T` and\r
  96     f_const = `F`;;\r
  97         \r
  98 (* num constants *)\r
  99 let zero_const = `_0` and\r
 100         zero_num = `0`;;\r
 101         \r
 102 (* num operations *)\r
 103 let add_op_num = `(+) : num->num->num` and\r
 104     sub_op_num = `(-) : num->num->num` and\r
 105     mul_op_num = `( * ) : num->num->num` and\r
 106         eq_op_num = `(=) : num->num->bool` and\r
 107     le_op_num = `(<=) : num->num->bool` and\r
 108         lt_op_num = `(<) : num->num->bool` and\r
 109     div_op_num = `(DIV): num->num->num` and\r
 110     pre_op_num = `PRE: num->num` and\r
 111     suc_op_num = `SUC : num->num`;;\r
 112 \r
 113 \r
 114 (* real constants *)\r
 115 let real_empty_list = `[]:(real)list`;; \r
 116 \r
 117 (* real operations *)\r
 118 let add_op_real = `(+) : real->real->real` and\r
 119     mul_op_real = `( * ) : real->real->real` and\r
 120     sub_op_real = `(-) : real->real->real` and\r
 121     div_op_real = `(/) :real->real->real` and\r
 122     inv_op_real = `inv : real->real` and\r
 123     neg_op_real = `(--) : real->real` and\r
 124     eq_op_real = `(=) : real->real->bool` and\r
 125     lt_op_real = `(<) : real->real->bool` and\r
 126         le_op_real = `(<=):real->real->bool` and\r
 127         ge_op_real = `(>=):real->real->bool` and\r
 128         amp_op_real = `(&) : num->real` and\r
 129         pow_op_real = `(pow) : real->num->real`;;\r
 130 \r
 131 (* types *)\r
 132 let real_ty = `:real` and\r
 133         real_list_ty = `:(real)list` and\r
 134         real_pair_ty = `:real#real` and\r
 135         real_pair_list_ty = `:(real#real)list` and\r
 136         num_type = `:num` and\r
 137         nty = `:N`;;\r
 138 \r
 139 \r
 140 (* Simple operations *)\r
 141 let mk_real_list tms = mk_list (tms, real_ty);;\r
 142 \r
 143 let mk_names n prefix = map (fun i -> prefix^(string_of_int i)) (1--n);;\r
 144 \r
 145 let mk_real_vars n prefix = map (C (curry mk_var) real_ty) (mk_names n prefix);;\r
 146 \r
 147  \r
 148 end;;\r