Nouvelle interprétation des nombres réels

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 93 insertions, 44 deletions

diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index f7156d46dc..244c5d821d 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -26,8 +26,10 @@ let get_r_sign loc =
   in
   ((mkid (id_of_string "R0"),
     mkid (id_of_string "R1"),
-    mkid (id_of_string "Rplus"), 
-    mkid (id_of_string "NRplus")))
+    mkid (id_of_string "Rplus"),
+    mkid (id_of_string "Rmult"),
+    mkid (id_of_string "NRplus"),
+    mkid (id_of_string "NRmult")))
 
 let get_r_sign_ast loc =
   let mkid id =
@@ -36,19 +38,30 @@ let get_r_sign_ast loc =
   ((mkid (id_of_string "R0"),
     mkid (id_of_string "R1"),
     mkid (id_of_string "Rplus"), 
-    mkid (id_of_string "NRplus")))
+    mkid (id_of_string "Rmult"),
+    mkid (id_of_string "NRplus"),
+    mkid (id_of_string "NRmult")))
+
+let int_decomp n = 
+let div2 k = 
+let x = k mod 2 in
+let y = k - x in (x,y/2) in
+let rec list_ch m =
+if m< 2 then [m]
+else let (x1,x2) = div2 m in x1::(list_ch x2)
+in list_ch n
 
 let r_of_int n dloc =
-  let (a0,a1,plus,_) = get_r_sign dloc in
-  let rec mk_r n =
-    if n <= 0 then
-      a0
-    else if n = 1 then 
-      a1
-    else
-      mkAppC (plus, [a1; mk_r (n-1)])
-  in 
-  mk_r n
+  let (a0,a1,plus,mult,_,_) = get_r_sign dloc in
+  let list_ch = int_decomp n in
+  let a2 = mkAppC (plus, [a1; a1]) in
+  let rec mk_r l =
+    match l with
+    | [] -> failwith "Error r_of_int"
+    | [a] -> if a=1 then a1 else a0
+    | a::[b] -> if a==1 then mkAppC (plus, [a1; a2]) else a2
+    | a::l' -> if a=1 then mkAppC (plus, [a1; mkAppC (mult, [a2; mk_r l'])]) else mkAppC (mult, [a2; mk_r l'])
+  in mk_r list_ch
 
 let r_of_string s dloc = 
   r_of_int (int_of_string s) dloc
@@ -67,39 +80,68 @@ let _ =
 
 exception Non_closed_number
 
-let rec int_of_r_rec a1 plus p =
-  match p with
-    | Node (_,"APPLIST", [b; a; c]) when alpha_eq(b,plus) && 
-                                         alpha_eq(a,a1) ->
-        (int_of_r_rec a1 plus c)+1
-    | a when alpha_eq(a,a1) -> 1  
-    | _ -> raise Non_closed_number
-          
 let int_of_r p =
-  let (_,a1,plus,_) = get_r_sign_ast dummy_loc in
+  let (a0,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
+  let rec int_of_r_rec p = 
+    match p with
+  | Node (_,"APPLIST", [b;a;c]) when alpha_eq(b,plus) & alpha_eq(a,a1) & alpha_eq(c,a1) -> 2
+  | Node (_,"APPLIST", [b;a;c]) when alpha_eq(b,plus) & alpha_eq(a,a1) ->
+      (match c with
+      |	Node (_,"APPLIST", [e;d;f]) when alpha_eq(e,mult) -> 1 + int_of_r_rec c
+      |	Node (_,"APPLIST", [e;d;f]) when alpha_eq(e,plus) & alpha_eq(d,a1) & alpha_eq(f,a1) -> 3
+      |	_ -> raise Non_closed_number)
+  | Node (_,"APPLIST", [b;a;c]) when alpha_eq(b,mult) ->
+      (match a with
+      |	Node (_,"APPLIST", [e;d;f]) when alpha_eq(e,plus) & alpha_eq(d,a1) & alpha_eq(f,a1) ->
+	  (match c with
+	  | g when alpha_eq(g,a1) -> raise Non_closed_number
+	  | g when alpha_eq(g,a0) -> raise Non_closed_number
+	  | _ -> 2 * int_of_r_rec c)
+      |	_ -> raise Non_closed_number)
+  | a when alpha_eq(a,a0) -> 0
+  | a when alpha_eq(a,a1) -> 1
+  | _ -> raise Non_closed_number in
   try 
-    Some (int_of_r_rec a1 plus p)
+    Some (int_of_r_rec p)
   with
     Non_closed_number -> None
 
 let replace_plus p = 
-  let (_,a1,_,astnr) = get_r_sign_ast dummy_loc in
-     ope ("REXPR",[ope("APPLIST", [astnr; a1; p])]) 
+  let (_,_,_,_,astnrplus,_) = get_r_sign_ast dummy_loc in
+  ope ("REXPR",[ope("APPLIST",[astnrplus;p])])
+
+let replace_mult p = 
+  let (_,_,_,_,_,astnrmult) = get_r_sign_ast dummy_loc in
+  ope ("REXPR",[ope("APPLIST",[astnrmult;p])])
 
-let r_printer std_pr p =
-  let (_,a1,plus,_) = get_r_sign dummy_loc in
-  match (int_of_r p) with
-    | Some i -> str (string_of_int (i+1))
+let rec r_printer_odd std_pr p =
+  let (_,a1,plus,_,_,_) = get_r_sign_ast dummy_loc in
+  match (int_of_r (ope("APPLIST",[plus;a1;p]))) with
+    | Some i -> str (string_of_int i)
     | None -> std_pr (replace_plus p)
 
-let r_printer_outside std_pr p =
-  let (_,a1,plus,_) = get_r_sign dummy_loc in
-  match (int_of_r p) with
-    | Some i -> str "``" ++ str (string_of_int (i+1)) ++ str "``"
+let rec r_printer_odd_outside std_pr p =
+  let (_,a1,plus,_,_,_) = get_r_sign_ast dummy_loc in
+  match (int_of_r (ope("APPLIST",[plus;a1;p]))) with
+    | Some i -> str"``" ++ str (string_of_int i) ++ str"``"
     | None -> std_pr (replace_plus p)
 
-let _ = Esyntax.Ppprim.add ("r_printer", r_printer)
-let _ = Esyntax.Ppprim.add ("r_printer_outside", r_printer_outside)
+let rec r_printer_even std_pr p =
+  let (_,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
+  match (int_of_r (ope("APPLIST",[mult;(ope("APPLIST",[plus;a1;a1]));p]))) with
+    | Some i -> str (string_of_int i)
+    | None -> std_pr (replace_mult p)
+
+let rec r_printer_even_outside std_pr p =
+  let (_,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
+  match (int_of_r (ope("APPLIST",[mult;(ope("APPLIST",[plus;a1;a1]));p]))) with
+    | Some i -> str"``" ++ str (string_of_int i) ++ str"``"
+    | None -> std_pr (replace_mult p)
+
+let _ = Esyntax.Ppprim.add ("r_printer_odd", r_printer_odd)
+let _ = Esyntax.Ppprim.add ("r_printer_odd_outside", r_printer_odd_outside)
+let _ = Esyntax.Ppprim.add ("r_printer_even", r_printer_even)
+let _ = Esyntax.Ppprim.add ("r_printer_even_outside", r_printer_even_outside)
 
 (**********************************************************************)
 (* Parsing Z via scopes                                               *)
@@ -119,6 +161,7 @@ let glob_R1 = ConstRef (make_path rdefinitions "R1")
 let glob_R0 = ConstRef (make_path rdefinitions "R0")
 let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
 let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
+let glob_Rmult = ConstRef (make_path rdefinitions "Rmult")
 
 let r_of_posint dloc n =
   if is_nonzero n then begin
@@ -140,20 +183,26 @@ let r_of_posint dloc n =
   else
     RRef (dloc, glob_R0)
 
-let r_of_int dloc z =
+let r_of_int2 dloc z =
   match z with
   | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
-  | POS n -> r_of_posint dloc n 
+  | POS n -> r_of_posint dloc n
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
 let rec bignat_of_r = function
-  | RApp (_,RRef (_,p), [RRef (_,o); a]) when p = glob_Rplus & o = glob_R1
-      -> add_1 (bignat_of_r a)
-  | RRef (_,a) when a = glob_R1 -> Bignat.one
-  | RRef (_,a) when a = glob_R0 -> Bignat.zero
+  | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)]) when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> add_1 one
+  | RApp (_,RRef (_,p), [RRef (_,o); RApp (_,RRef (_,p2),_) as a]) when p = glob_Rplus & o = glob_R1 -> 
+      if p2 = glob_Rmult then add_1 (bignat_of_r a)
+      else (match a with 
+      |	RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)]) when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> add_1 (add_1 one)
+      |	_ -> raise Non_closed_number)
+  | RApp (_,RRef (_,p), [RApp (_,RRef (_,o1), [RRef (_,o2); RRef (_,o3)]); RRef (_,q)]) when p = glob_Rmult & o1 = glob_Rplus & o2 = glob_R1 & o3 = glob_R1 & q = glob_R1 -> raise Non_closed_number 
+  | RApp (_,RRef (_,p), [RApp (_,RRef (_,o1), [RRef (_,o2); RRef (_,o3)]); a]) when p = glob_Rmult & o1 = glob_Rplus & o2 = glob_R1 & o3 = glob_R1 -> mult_2 (bignat_of_r a) 
+  | RRef (_,a) when a = glob_R1 -> one
+  | RRef (_,a) when a = glob_R0 -> zero
   | _ -> raise Non_closed_number
 
 let bigint_of_r = function
@@ -168,9 +217,9 @@ let uninterp_r p =
 
 let _ = Symbols.declare_numeral_interpreter "R_scope"
   ["Coq";"Reals";"Rsyntax"]
-  (r_of_int,None)
+  (r_of_int2,None)
   ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
-    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_R1)],
+    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);RRef(dummy_loc,glob_R1)],
     uninterp_r,
     None)
 
@@ -180,7 +229,7 @@ let _ = Symbols.declare_numeral_interpreter "R_scope"
 exception Non_closed_number
 
 let bignat_of_pos p =
-  let (_,one,plus,_) = get_r_sign_ast dummy_loc in
+  let (_,one,plus,_,_,_) = get_r_sign_ast dummy_loc in
   let rec transl = function
     | Node (_,"APPLIST",[p; o; a]) when alpha_eq(p,plus) & alpha_eq(o,one)
         -> add_1(transl a)