(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* RApp (dloc, ref_xO,[pos_of q],[Term.Expl]) | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q],[Term.Expl]) | (q,true) -> ref_xH in pos_of x let error_non_positive dloc = user_err_loc (dloc, "interp_positive", str "Only strictly positive numbers in type \"positive\"") let interp_positive dloc n = if is_strictly_pos n then pos_of_bignat dloc n else error_non_positive dloc (**********************************************************************) (* Printing positive via scopes *) (**********************************************************************) let rec bignat_of_pos = function | RApp (_, RRef (_,b),[a],_) when b = glob_xO -> mult_2(bignat_of_pos a) | RApp (_, RRef (_,b),[a],_) when b = glob_xI -> add_1(mult_2(bignat_of_pos a)) | RRef (_, a) when a = glob_xH -> Bigint.one | _ -> raise Non_closed_number let uninterp_positive p = try Some (bignat_of_pos p) with Non_closed_number -> None (************************************************************************) (* Declaring interpreters and uninterpreters for positive *) (************************************************************************) let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,positive_module) interp_positive ([RRef (dummy_loc, glob_xI); RRef (dummy_loc, glob_xO); RRef (dummy_loc, glob_xH)], uninterp_positive, true) (**********************************************************************) (* Parsing N via scopes *) (**********************************************************************) let binnat_module = ["Coq";"NArith";"BinNat"] let n_kn = make_kn (make_dir binnat_module) (id_of_string "N") let glob_n = IndRef (n_kn,0) let path_of_N0 = ((n_kn,0),1) let path_of_Npos = ((n_kn,0),2) let glob_N0 = ConstructRef path_of_N0 let glob_Npos = ConstructRef path_of_Npos let n_path = make_path binnat_module "N" let n_of_binnat dloc pos_or_neg n = if n <> zero then RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n],[Term.Expl]) else RRef (dloc, glob_N0) let error_negative dloc = user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\"") let n_of_int dloc n = if is_pos_or_zero n then n_of_binnat dloc true n else error_negative dloc (**********************************************************************) (* Printing N via scopes *) (**********************************************************************) let bignat_of_n = function | RApp (_, RRef (_,b),[a],_) when b = glob_Npos -> bignat_of_pos a | RRef (_, a) when a = glob_N0 -> Bigint.zero | _ -> raise Non_closed_number let uninterp_n p = try Some (bignat_of_n p) with Non_closed_number -> None (************************************************************************) (* Declaring interpreters and uninterpreters for N *) let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnat_module) n_of_int ([RRef (dummy_loc, glob_N0); RRef (dummy_loc, glob_Npos)], uninterp_n, true) (**********************************************************************) (* Parsing Z via scopes *) (**********************************************************************) let binint_module = ["Coq";"ZArith";"BinInt"] let z_path = make_path binint_module "Z" let z_kn = make_kn (make_dir binint_module) (id_of_string "Z") let glob_z = IndRef (z_kn,0) let path_of_ZERO = ((z_kn,0),1) let path_of_POS = ((z_kn,0),2) let path_of_NEG = ((z_kn,0),3) let glob_ZERO = ConstructRef path_of_ZERO let glob_POS = ConstructRef path_of_POS let glob_NEG = ConstructRef path_of_NEG let z_of_int dloc n = if n <> zero then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n],[Term.Expl]) else RRef (dloc, glob_ZERO) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) let bigint_of_z = function | RApp (_, RRef (_,b),[a],_) when b = glob_POS -> bignat_of_pos a | RApp (_, RRef (_,b),[a],_) when b = glob_NEG -> Bigint.neg (bignat_of_pos a) | RRef (_, a) when a = glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number let uninterp_z p = try Some (bigint_of_z p) with Non_closed_number -> None (************************************************************************) (* Declaring interpreters and uninterpreters for Z *) let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binint_module) z_of_int ([RRef (dummy_loc, glob_ZERO); RRef (dummy_loc, glob_POS); RRef (dummy_loc, glob_NEG)], uninterp_z, true)