diff options
Diffstat (limited to 'parsing/g_rsyntax.ml')
| -rw-r--r-- | parsing/g_rsyntax.ml | 117 |
1 files changed, 90 insertions, 27 deletions
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index 2c0e9da77..7596e1f8a 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -51,6 +51,7 @@ if m< 2 then [m] else let (x1,x2) = div2 m in x1::(list_ch x2) in list_ch n +let _ = if !Options.v7 then let r_of_int n dloc = let (a0,a1,plus,mult,_,_) = get_r_sign dloc in let list_ch = int_decomp n in @@ -62,23 +63,24 @@ let r_of_int n dloc = | 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 - +in let r_of_string s dloc = r_of_int (int_of_string s) dloc - +in let rsyntax_create name = let e = Pcoq.create_constr_entry (Pcoq.get_univ "rnatural") name in Pcoq.Gram.Unsafe.clear_entry e; e - +in let rnumber = rsyntax_create "rnumber" - +in let _ = Gram.extend rnumber None [None, None, [[Gramext.Stoken ("INT", "")], Gramext.action r_of_string]] +in () (**********************************************************************) (* Old ast printing *) @@ -86,6 +88,7 @@ let _ = exception Non_closed_number +let _ = if !Options.v7 then let int_of_r p = let (a0,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in let rec int_of_r_rec p = @@ -111,46 +114,47 @@ let int_of_r p = Some (int_of_r_rec p) with Non_closed_number -> None - +in let replace_plus p = let (_,_,_,_,astnrplus,_) = get_r_sign_ast dummy_loc in ope ("REXPR",[ope("APPLIST",[astnrplus;p])]) - +in let replace_mult p = let (_,_,_,_,_,astnrmult) = get_r_sign_ast dummy_loc in ope ("REXPR",[ope("APPLIST",[astnrmult;p])]) - +in 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) - +in 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) - +in 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) - +in 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) +in +let _ = Esyntax.Ppprim.add ("r_printer_odd", r_printer_odd) in +let _ = Esyntax.Ppprim.add ("r_printer_odd_outside", r_printer_odd_outside) in +let _ = Esyntax.Ppprim.add ("r_printer_even", r_printer_even) in let _ = Esyntax.Ppprim.add ("r_printer_even_outside", r_printer_even_outside) +in () (**********************************************************************) -(* Parsing Z via scopes *) +(* Parsing R via scopes *) (**********************************************************************) open Libnames @@ -169,6 +173,7 @@ let glob_Ropp = ConstRef (make_path rdefinitions "Ropp") let glob_Rplus = ConstRef (make_path rdefinitions "Rplus") let glob_Rmult = ConstRef (make_path rdefinitions "Rmult") +(* V7 *) let r_of_posint dloc n = let ref_R0 = RRef (dloc, glob_R0) in let ref_R1 = RRef (dloc, glob_R1) in @@ -191,10 +196,39 @@ let r_of_int2 dloc z = | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (int_of_string (bigint_to_string (POS n)))]) | POS n -> r_of_posint dloc (int_of_string (bigint_to_string z)) +(* V8 *) +let two = mult_2 one +let three = add_1 two +let four = mult_2 two + +(* Unary representation of strictly positive numbers *) +let rec small_r dloc n = + if is_one n then RRef (dloc, glob_R1) + else RApp(dloc,RRef (dloc,glob_Rplus), + [RRef (dloc, glob_R1);small_r dloc (sub_1 n)]) + +let r_of_posint dloc n = + let r1 = RRef (dloc, glob_R1) in + let r2 = small_r dloc two in + let rec r_of_pos n = + if less_than n four then small_r dloc n + else + let (q,r) = div2_with_rest n in + let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in + if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in + if is_nonzero n then r_of_pos n else RRef(dloc,glob_R0) + +let r_of_int 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 + (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) +let bignat_of_r = +if !Options.v7 then let rec bignat_of_r = function | 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 -> @@ -207,6 +241,35 @@ let rec bignat_of_r = function | RRef (_,a) when a = glob_R1 -> one | RRef (_,a) when a = glob_R0 -> zero | _ -> raise Non_closed_number +in bignat_of_r +else +(* for numbers > 1 *) +let rec bignat_of_pos = function + (* 1+1 *) + | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)]) + when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two + (* 1+1+1 *) + | RApp (_,RRef (_,p1), [RRef (_,o1); + RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])]) + when p1 = glob_Rplus & p2 = glob_Rplus & + o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three + (* (1+1)*b *) + | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult -> + if bignat_of_pos a <> two then raise Non_closed_number; + mult_2 (bignat_of_pos b) + (* 1+(1+1)*b *) + | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])]) + when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1 -> + if bignat_of_pos a <> two then raise Non_closed_number; + add_1 (mult_2 (bignat_of_pos b)) + | _ -> raise Non_closed_number +in +let bignat_of_r = function + | RRef (_,a) when a = glob_R0 -> zero + | RRef (_,a) when a = glob_R1 -> one + | r -> bignat_of_pos r +in +bignat_of_r let bigint_of_r = function | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> NEG (bignat_of_r a) @@ -220,7 +283,7 @@ let uninterp_r p = let _ = Symbols.declare_numeral_interpreter "R_scope" ["Coq";"Reals";"Rdefinitions"] - (r_of_int2,None) + ((if !Options.v7 then r_of_int2 else r_of_int),None) ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0); RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);RRef(dummy_loc,glob_R1)], uninterp_r, @@ -229,8 +292,7 @@ let _ = Symbols.declare_numeral_interpreter "R_scope" (***********************************************************************) (* Old ast printers via scope *) -exception Non_closed_number - +let _ = if !Options.v7 then let bignat_of_pos p = let (_,one,plus,_,_,_) = get_r_sign_ast dummy_loc in let rec transl = function @@ -239,35 +301,36 @@ let bignat_of_pos p = | a when alpha_eq(a,one) -> Bignat.one | _ -> raise Non_closed_number in transl p - +in let bignat_option_of_pos p = try Some (bignat_of_pos p) with Non_closed_number -> None - +in let r_printer_Rplus1 p = match bignat_option_of_pos p with | Some n -> Some (str (Bignat.to_string (add_1 n))) | None -> None - +in let r_printer_Ropp p = match bignat_option_of_pos p with | Some n -> Some (str "-" ++ str (Bignat.to_string n)) | None -> None - +in let r_printer_R1 _ = Some (int 1) - +in let r_printer_R0 _ = Some (int 0) - +in (* Declare pretty-printers for integers *) let _ = Esyntax.declare_primitive_printer "r_printer_Ropp" "R_scope" (r_printer_Ropp) -let _ = +in let _ = Esyntax.declare_primitive_printer "r_printer_Rplus1" "R_scope" (r_printer_Rplus1) -let _ = +in let _ = Esyntax.declare_primitive_printer "r_printer_R1" "R_scope" (r_printer_R1) -let _ = +in let _ = Esyntax.declare_primitive_printer "r_printer_R0" "R_scope" r_printer_R0 +in () |