diff options
Diffstat (limited to 'parsing/g_rsyntaxnew.ml')
| -rw-r--r-- | parsing/g_rsyntaxnew.ml | 113 |
1 files changed, 113 insertions, 0 deletions
diff --git a/parsing/g_rsyntaxnew.ml b/parsing/g_rsyntaxnew.ml new file mode 100644 index 000000000..081762ae3 --- /dev/null +++ b/parsing/g_rsyntaxnew.ml @@ -0,0 +1,113 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +open Coqast +open Ast +open Pp +open Util +open Names +open Pcoq +open Extend +open Topconstr +open Libnames + +(**********************************************************************) +(* Parsing R via scopes *) +(**********************************************************************) + +open Libnames +open Rawterm +open Bignat + +let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) +let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] + +(* TODO: temporary hack *) +let make_path dir id = Libnames.encode_kn dir (id_of_string id) + +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 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 *) +(**********************************************************************) + +exception Non_closed_number + +(* 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 + +let bignat_of_r = function + | RRef (_,a) when a = glob_R0 -> zero + | RRef (_,a) when a = glob_R1 -> one + | r -> bignat_of_pos r + +let bigint_of_r = function + | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> NEG (bignat_of_r a) + | a -> POS (bignat_of_r a) + +let uninterp_r p = + try + Some (bigint_of_r p) + with Non_closed_number -> + None + +let _ = Symbols.declare_numeral_interpreter "R_scope" + ["Coq";"Reals";"Rsyntax"] + (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, + None) |