(* =========================================================== *)
(* Commonly used variables and constants                       *)
(* Author: Alexey Solovyev                                     *)
(* Date: 2012-10-27                                            *)
(* =========================================================== *)

module Misc_vars = struct

(* bool variables *)
let s_var_bool = `s:bool` and
        s1_var_bool = `s1:bool` and
        s2_var_bool = `s2:bool`;;

(* num variables *)
let n_var_num = `n:num` and
    m_var_num = `m:num` and
        k_var_num = `k:num` and
    e_var_num = `e:num` and
        e1_var_num = `e1:num` and
        e2_var_num = `e2:num` and
        r_var_num = `r:num` and
        r1_var_num = `r1:num` and
        r2_var_num = `r2:num` and
        n1_var_num = `n1:num` and
        n2_var_num = `n2:num` and
        m1_var_num = `m1:num` and
        m2_var_num = `m2:num` and
        x_var_num = `x:num` and
        y_var_num = `y:num` and
        i_var_num = `i:num` and
        j_var_num = `j:num`;;

(* real variables *)
let x_var_real = `x : real` and
    y_var_real = `y : real` and
        z_var_real = `z : real` and
    w_var_real = `w : real` and
        a_var_real = `a : real` and
        b_var_real = `b : real` and
        m_var_real = `m : real` and
        n_var_real = `n : real` and
        x1_var_real = `x1 : real` and
        x2_var_real = `x2 : real` and
        y1_var_real = `y1 : real` and
        y2_var_real = `y2 : real` and
        f1_var_real = `f1 : real` and
        f2_var_real = `f2 : real` and
    f_var_fun = `f : real->real` and
    g_var_fun = `g : real->real` and
    f1_var_fun = `f1 : real->real` and
    f2_var_fun = `f2 : real->real` and
    int_var = `int : real#real` and
    f_bounds_var = `f_bounds : real#real` and
    df_bounds_var = `df_bounds : real#real` and
    dd_bounds_var = `dd_bounds : real#real` and
    x_lo_var = `x_lo : real` and
    x_hi_var = `x_hi : real` and
        lo_var_real = `lo : real` and
        hi_var_real = `hi : real` and
    dd_var_real = `dd : real` and
    df_lo_var = `df_lo : real` and
    df_hi_var = `df_hi : real` and
    df_var_real = `df : real` and
    f_lo_var = `f_lo : real` and
    f_hi_var = `f_hi : real` and
        w1_var_real = `w1 : real` and
    w2_var_real = `w2 : real` and
    t_var_real = `t : real` and
    g_bounds_var = `g_bounds : real#real` and
    dg_bounds_var = `dg_bounds : real#real` and
    bounds_var = `bounds : real#real` and
    d_bounds_var = `d_bounds : real#real` and
    x0_var_real = `x0 : real` and
    z0_var_real = `z0 : real` and
    w0_var_real = `w0 : real` and
        error_var = `error : real` and
        d_bounds_list_var = `d_bounds_list : (real#real)list` and
        dd_bounds_list_var = `dd_bounds_list : ((real#real)list)list` and
        df_bounds_list_var = `df_bounds_list : (real#real)list` and
        dd_list_var = `dd_list : (real#real)list` and
        x_var_real_list = `x:(real)list` and
    y_var_real_list = `y:(real)list` and
    z_var_real_list = `z:(real)list` and
    w_var_real_list = `w:(real)list` and
    yw_var = `yw : (real#real)list` and
    xz_var = `xz : (real#real)list` and
    xz_pair_var = `xz : real#real` and
    yw_pair_var = `yw : real#real` and
        list_var_real_pair = `list : (real#real)list`;;

(* bool constants *)
let t_const = `T` and
    f_const = `F`;;

(* num constants *)
let zero_const = `_0`;;

(* num operations *)
let add_op_num = `(+) : num->num->num` and
    sub_op_num = `(-) : num->num->num` and
    mul_op_num = `( * ) : num->num->num` and
    le_op_num = `(<=) : num->num->bool` and
        lt_op_num = `(<) : num->num->bool` and
    div_op_num = `(DIV): num->num->num` and
    pre_op_num = `PRE: num->num` and
    suc_op_num = `SUC : num->num`;;


(* real constants *)
let real_empty_list = `[]:(real)list`;;

(* real operations *)
let add_op_real = `(+) : real->real->real` and
    mul_op_real = `( * ) : real->real->real` and
    sub_op_real = `(-) : real->real->real` and
    div_op_real = `(/) :real->real->real` and
    inv_op_real = `inv : real->real` and
    neg_op_real = `(--) : real->real` and
    eq_op_real = `(=) : real->real->bool` and
    lt_op_real = `(<) : real->real->bool` and
        le_op_real = `(<=):real->real->bool` and
        amp_op_real = `(&) : num->real` and
        pow_op_real = `(pow) : real->num->real`;;

(* types *)
let real_ty = `:real` and
        real_list_ty = `:(real)list` and
        real_pair_ty = `:real#real` and
        real_pair_list_ty = `:(real#real)list` and
        nty = `:N`;;


(* Simple operations *)
let mk_real_list tms = mk_list (tms, real_ty);;

let mk_names n prefix = map (fun i -> prefix^(string_of_int i)) (1--n);;

let mk_real_vars n prefix = map (C (curry mk_var) real_ty) (mk_names n prefix);;


end;;