formal_lp/old/formal_interval/m_verifier0.hl

   1 flyspeck_needs "../formal_lp/formal_interval/interval_m/verifier.hl";;
   2 flyspeck_needs "../formal_lp/formal_interval/eval_interval.hl";;
   3
   4 open Verifier;;
   5 open Interval;;
   6 open Line_interval;;
   7 open Taylor;;
   8 open Recurse;;
   9
  10 (****************************)
  11 (* Automatic conversion of formal interval functions into functions *)
  12
  13 let rec build_fun i_fun =
  14   match i_fun with
  15     | Int_var tm ->
  16         (try F_int_var (dest_small_numeral (rand tm))
  17          with Failure _ ->
  18            let name = (fst o dest_var) tm in
  19              F_int_var (int_of_string (String.sub name 1 (String.length name - 1))))
  20     | Int_const th ->
  21         let f1, f2 = (dest_pair o rand o concl) th in
  22         let int = mk_interval (float_of_float_tm f1, float_of_float_tm f2) in
  23           F_int_const int
  24     | Int_pow (n, f) -> F_int_pow (n, build_fun f)
  25     | Int_unary (op, f) ->
  26         let f' = build_fun f in
  27           if op = neg_op_real then F_int_neg f' else failwith ("Unsupported operator: "^string_of_term op)
  28     | Int_binary (op, f1, f2) ->
  29         let f1', f2' = build_fun f1, build_fun f2 in
  30           if op = add_op_real then F_int_add (f1',f2')
  31           else if op = sub_op_real then F_int_sub (f1',f2')
  32           else if op = mul_op_real then F_int_mul (f1',f2')
  33           else failwith ("Unsupported operator: "^string_of_term op)
  34     | _ -> failwith "Unsupported function";;
  35
  36
  37 let buildL pp lin_th =
  38   let funs = map (fst o dest_interval_arith) ((striplist dest_conj o rand o concl) lin_th) in
  39   let i_funs = map (eval_constants pp o build_interval_fun) funs in
  40   let fs = map build_fun i_funs @ (replicate (F_int_const zero) (8 - length funs + 1)) in
  41   let eval_fs = map eval_int_fun fs in
  42   let f, df = hd eval_fs, tl eval_fs in
  43     (fun i x z ->
  44       let vars = map2 (curry mk_interval) x z in
  45         if i = 0 then f vars else (List.nth df (i - 1)) vars),
  46     (fun x ->
  47       let vars = map (fun x -> mk_interval (x,x)) x in
  48         mk_line (f vars, map (fun df -> df vars) df));;
  49
  50 let buildL0 pp poly_tm =
  51   let lin_th = gen_lin_approx_poly_thm0 poly_tm in
  52     buildL pp lin_th;;
  53
  54 let buildDD pp second_th =
  55   let poly_tm = (lhand o rator o lhand o concl) second_th in
  56   let n = (get_dim o fst o dest_abs) poly_tm in
  57   let ns = 1--n in
  58   let funs = (striplist dest_conj o rand o snd o dest_forall o rand o concl) second_th in
  59   let i_funs = map (eval_constants pp o build_interval_fun o fst o dest_interval_arith) funs in
  60   let fs0 = map build_fun i_funs in
  61   let pad1 = replicate zero (8 - n) and
  62       pad2 = replicate zero 8 in
  63   let pad3 = replicate pad2 (8 - n) in
  64   let get_el dd i j =
  65     let i', j' = if j <= i then i, j else j, i in
  66     let index = (i' - 1) * i' / 2 + (j' - 1) in
  67       List.nth dd index in
  68   let eval_fs = map eval_int_fun fs0 in
  69     fun x z ->
  70       let ints = map2 (curry mk_interval) x z in
  71       let vals = map (fun f -> f ints) eval_fs in
  72         map (fun i -> map (fun j -> get_el vals i j) ns @ pad1) ns @ pad3;;
  73
  74
  75 let buildDD0 pp poly_tm =
  76   let second_th = gen_second_bounded_poly_thm0 poly_tm in
  77     buildDD pp second_th;;
  78
  79
  80 (******)
  81
  82 let build_taylor pp lin_th second_th =
  83   let f_df, lin = buildL pp lin_th and
  84       dd = buildDD pp second_th in
  85     Prim_a (make_primitiveA (f_df, lin, dd));;
  86
  87 let build_taylor0 pp poly_tm =
  88   build_taylor pp (gen_lin_approx_poly_thm0 poly_tm) (gen_second_bounded_poly_thm0 poly_tm);;