diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /plugins/syntax/z_syntax.ml | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'plugins/syntax/z_syntax.ml')
-rw-r--r-- | plugins/syntax/z_syntax.ml | 81 |
1 files changed, 39 insertions, 42 deletions
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index e6dcc35e..f8bce8f7 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: z_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pcoq open Pp open Util @@ -23,18 +21,19 @@ exception Non_closed_number (**********************************************************************) open Libnames -open Rawterm +open Glob_term + +let binnums = ["Coq";"Numbers";"BinNums"] + let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let positive_module = ["Coq";"NArith";"BinPos"] let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) -let positive_path = make_path positive_module "positive" +let positive_path = make_path binnums "positive" (* TODO: temporary hack *) let make_kn dir id = Libnames.encode_mind dir id -let positive_kn = - make_kn (make_dir positive_module) (id_of_string "positive") +let positive_kn = make_kn (make_dir binnums) (id_of_string "positive") let glob_positive = IndRef (positive_kn,0) let path_of_xI = ((positive_kn,0),1) let path_of_xO = ((positive_kn,0),2) @@ -44,13 +43,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat dloc x = - let ref_xI = RRef (dloc, glob_xI) in - let ref_xH = RRef (dloc, glob_xH) in - let ref_xO = RRef (dloc, glob_xO) in + let ref_xI = GRef (dloc, glob_xI) in + let ref_xH = GRef (dloc, glob_xH) in + let ref_xO = GRef (dloc, glob_xO) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> RApp (dloc, ref_xO,[pos_of q]) - | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q]) + | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) + | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -68,9 +67,9 @@ let interp_positive dloc n = (**********************************************************************) 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 + | GApp (_, GRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a) + | GApp (_, GRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (_, a) when a = glob_xH -> Bigint.one | _ -> raise Non_closed_number let uninterp_positive p = @@ -84,11 +83,11 @@ let uninterp_positive p = (************************************************************************) let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,positive_module) + (positive_path,binnums) interp_positive - ([RRef (dummy_loc, glob_xI); - RRef (dummy_loc, glob_xO); - RRef (dummy_loc, glob_xH)], + ([GRef (dummy_loc, glob_xI); + GRef (dummy_loc, glob_xO); + GRef (dummy_loc, glob_xH)], uninterp_positive, true) @@ -96,21 +95,20 @@ let _ = Notation.declare_numeral_interpreter "positive_scope" (* Parsing N via scopes *) (**********************************************************************) -let binnat_module = ["Coq";"NArith";"BinNat"] -let n_kn = make_kn (make_dir binnat_module) (id_of_string "N") +let n_kn = make_kn (make_dir binnums) (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_path = make_path binnums "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]) + GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n]) else - RRef (dloc, glob_N0) + GRef (dloc, glob_N0) let error_negative dloc = user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") @@ -124,8 +122,8 @@ let n_of_int dloc n = (**********************************************************************) 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 + | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a + | GRef (_, a) when a = glob_N0 -> Bigint.zero | _ -> raise Non_closed_number let uninterp_n p = @@ -136,10 +134,10 @@ let uninterp_n p = (* Declaring interpreters and uninterpreters for N *) let _ = Notation.declare_numeral_interpreter "N_scope" - (n_path,binnat_module) + (n_path,binnums) n_of_int - ([RRef (dummy_loc, glob_N0); - RRef (dummy_loc, glob_Npos)], + ([GRef (dummy_loc, glob_N0); + GRef (dummy_loc, glob_Npos)], uninterp_n, true) @@ -147,9 +145,8 @@ let _ = Notation.declare_numeral_interpreter "N_scope" (* 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 z_path = make_path binnums "Z" +let z_kn = make_kn (make_dir binnums) (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) @@ -162,18 +159,18 @@ 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]) + GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n]) else - RRef (dloc, glob_ZERO) + GRef (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 + | GApp (_, GRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a + | GApp (_, GRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (_, a) when a = glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number let uninterp_z p = @@ -185,10 +182,10 @@ let uninterp_z p = (* Declaring interpreters and uninterpreters for Z *) let _ = Notation.declare_numeral_interpreter "Z_scope" - (z_path,binint_module) + (z_path,binnums) z_of_int - ([RRef (dummy_loc, glob_ZERO); - RRef (dummy_loc, glob_POS); - RRef (dummy_loc, glob_NEG)], + ([GRef (dummy_loc, glob_ZERO); + GRef (dummy_loc, glob_POS); + GRef (dummy_loc, glob_NEG)], uninterp_z, true) |