development/thales/chaff/external_arith.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* External Rational Number Operations                                                    *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-09-17                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 type mixed_term =
  11   | Ocaml_num of num
  12   | Ocaml_real of num
  13   | Hol_light of bool*term;; (* true if changed *)
  14
  15 (*
  16 type num =
  17 |       Int of int
  18 |       Big_int of Big_int.big_int
  19 |       Ratio of Ratio.ratio ///;;
  20
  21 let internalize_bool = function
  22   |  true -> `T`
  23   |  false -> `F`;;
  24 *)
  25
  26 let realize =
  27   let amp = `real_of_num` in
  28    fun x -> mk_comb (amp,x);;
  29
  30 let real_of_rat  =
  31   let real_div = `real_div` in
  32   let quot n d = mk_binop real_div (realize n) (realize d) in
  33     fun x ->
  34       let n = mk_numeral(Big_int (Ratio.numerator_ratio x)) in
  35       let d = mk_numeral(Big_int (Ratio.denominator_ratio x)) in
  36         quot n d;;
  37
  38 let term_of_mixed =
  39     function
  40   | Ocaml_real a ->
  41       (match a with
  42         | Big_int _ -> realize(mk_numeral a)
  43         | Int x -> realize (mk_small_numeral x)
  44         | Ratio x -> real_of_rat x)
  45   | Ocaml_num a ->
  46       (match a with
  47         | Big_int _ ->(mk_numeral a)
  48         | Int x ->  (mk_small_numeral x)
  49         | Ratio _ -> failwith "unnatural quotient")
  50   | Hol_light (changed,t) -> t;;
  51
  52 let dest_binop_from oplist t =
  53   let (h,y)= dest_comb t in
  54   let (op,x) = dest_comb h in
  55     if (mem op oplist) then (op,x,y) else failwith "op not found";;
  56
  57 let zero  = Int 0;;
  58
  59 let one = Int 1;;
  60
  61 let num_trunc_minus x y =  if ( y >/ x) then zero else x -/ y;;
  62
  63 let rat_div x y = if (y =/ zero) then zero else (x // y);;
  64
  65 let rat_inv x = if (x =/ zero) then zero else (one // x);;
  66
  67 let mk_cty ty = map (fun (a,b)-> (mk_mconst(a,ty),b));;
  68
  69 (*
  70 let real_rels = mk_cty `:real->real->bool`
  71  ["real_lt";"real_le";"=";"real_ge";"real_gt"];;
  72
  73 let num_rels = mk_cty `:num->num->bool`
  74   ["<=";"<";"=";">=";">="];;
  75 *)
  76
  77 let real_binop = mk_cty `:real->real->real`
  78  [("real_add",( +/ ));("real_sub", ( -/ ));("real_mul", ( */ ));("real_div",rat_div)];;
  79
  80 let num_binop = mk_cty `:num->num->num`
  81  [("+",( +/ ));("-",num_trunc_minus);("*", ( */ ))];;
  82
  83 let dec_op = mk_cty `:num->num->real`
  84  [("DECIMAL",( // ))];;
  85
  86 let numeral_op = mk_cty `:num->real` ["real_of_num",I];;
  87
  88 let real_unary = mk_cty `:real->real` [("real_neg",minus_num);("real_inv",rat_inv)];;
  89
  90 (*
  91 let lift (a,b) x  = function;;
  92 *)
  93
  94 let rec mixed_of_term arith = function
  95   | Var _ as u -> Hol_light (false,u)
  96   | Const _ as u -> Hol_light (false,u)
  97   | Abs(x,t) as u -> let t' = mixed_of_term false t in
  98       (match t' with
  99          | Hol_light (false,_) -> Hol_light (false,u)
 100          | _ -> Hol_light (true,mk_abs(x, term_of_mixed t')))
 101 (*
 102   | Const (h,y) as u -> Hol_lightu;;
 103       if (is_const h)
 104 *)
 105 ;;
 106
 107 type_of `DECIMAL`;;
 108 type_of `3`;;
 109 let mixedalize t = t;;
 110
 111 mk_numeral;;
 112 Int 3;;
 113
 114 Int 3;;
 115
 116 let v = Int 3 // Int 4;;
 117 let rec sqx n v = if (n = 0) then Int 1 else if (n=1) then v else (sqx (n-1) v)*/ (sqx (n-1) v);;
 118
 119 let vv = sqx 10 v;;