summaryrefslogtreecommitdiff
path: root/plugins/syntax/z_syntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/z_syntax.ml')
-rw-r--r--plugins/syntax/z_syntax.ml72
1 files changed, 35 insertions, 37 deletions
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 4025893d..e3721362 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -1,17 +1,15 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pcoq
open Pp
+open Errors
open Util
open Names
-open Topconstr
-open Libnames
open Bigint
exception Non_closed_number
@@ -20,20 +18,20 @@ exception Non_closed_number
(* Parsing positive via scopes *)
(**********************************************************************)
-open Libnames
+open Globnames
open Glob_term
let binnums = ["Coq";"Numbers";"BinNums"]
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
let positive_path = make_path binnums "positive"
(* TODO: temporary hack *)
-let make_kn dir id = Libnames.encode_mind dir id
+let make_kn dir id = Globnames.encode_mind dir id
-let positive_kn = make_kn (make_dir binnums) (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)
@@ -43,13 +41,13 @@ let glob_xO = ConstructRef path_of_xO
let glob_xH = ConstructRef path_of_xH
let pos_of_bignat dloc x =
- 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 ref_xI = GRef (dloc, glob_xI, None) in
+ let ref_xH = GRef (dloc, glob_xH, None) in
+ let ref_xO = GRef (dloc, glob_xO, None) in
let rec pos_of x =
match div2_with_rest x with
| (q,false) -> GApp (dloc, ref_xO,[pos_of q])
- | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q])
+ | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q])
| (q,true) -> ref_xH
in
pos_of x
@@ -67,9 +65,9 @@ let interp_positive dloc n =
(**********************************************************************)
let rec bignat_of_pos = function
- | 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
+ | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+ | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+ | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
| _ -> raise Non_closed_number
let uninterp_positive p =
@@ -85,9 +83,9 @@ let uninterp_positive p =
let _ = Notation.declare_numeral_interpreter "positive_scope"
(positive_path,binnums)
interp_positive
- ([GRef (dummy_loc, glob_xI);
- GRef (dummy_loc, glob_xO);
- GRef (dummy_loc, glob_xH)],
+ ([GRef (Loc.ghost, glob_xI, None);
+ GRef (Loc.ghost, glob_xO, None);
+ GRef (Loc.ghost, glob_xH, None)],
uninterp_positive,
true)
@@ -95,7 +93,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
(* Parsing N via scopes *)
(**********************************************************************)
-let n_kn = make_kn (make_dir binnums) (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)
@@ -105,10 +103,10 @@ let glob_Npos = ConstructRef path_of_Npos
let n_path = make_path binnums "N"
let n_of_binnat dloc pos_or_neg n =
- if n <> zero then
- GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n])
+ if not (Bigint.equal n zero) then
+ GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n])
else
- GRef (dloc, glob_N0)
+ GRef (dloc, glob_N0, None)
let error_negative dloc =
user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
@@ -122,8 +120,8 @@ let n_of_int dloc n =
(**********************************************************************)
let bignat_of_n = function
- | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
- | GRef (_, a) when a = glob_N0 -> Bigint.zero
+ | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
+ | GRef (_, a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
| _ -> raise Non_closed_number
let uninterp_n p =
@@ -136,8 +134,8 @@ let uninterp_n p =
let _ = Notation.declare_numeral_interpreter "N_scope"
(n_path,binnums)
n_of_int
- ([GRef (dummy_loc, glob_N0);
- GRef (dummy_loc, glob_Npos)],
+ ([GRef (Loc.ghost, glob_N0, None);
+ GRef (Loc.ghost, glob_Npos, None)],
uninterp_n,
true)
@@ -146,7 +144,7 @@ let _ = Notation.declare_numeral_interpreter "N_scope"
(**********************************************************************)
let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (id_of_string "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)
@@ -156,21 +154,21 @@ let glob_POS = ConstructRef path_of_POS
let glob_NEG = ConstructRef path_of_NEG
let z_of_int dloc n =
- if n <> zero then
+ if not (Bigint.equal n zero) then
let sgn, n =
if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
- GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n])
+ GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n])
else
- GRef (dloc, glob_ZERO)
+ GRef (dloc, glob_ZERO, None)
(**********************************************************************)
(* Printing Z via scopes *)
(**********************************************************************)
let bigint_of_z = function
- | 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
+ | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+ | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+ | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
| _ -> raise Non_closed_number
let uninterp_z p =
@@ -184,8 +182,8 @@ let uninterp_z p =
let _ = Notation.declare_numeral_interpreter "Z_scope"
(z_path,binnums)
z_of_int
- ([GRef (dummy_loc, glob_ZERO);
- GRef (dummy_loc, glob_POS);
- GRef (dummy_loc, glob_NEG)],
+ ([GRef (Loc.ghost, glob_ZERO, None);
+ GRef (Loc.ghost, glob_POS, None);
+ GRef (Loc.ghost, glob_NEG, None)],
uninterp_z,
true)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 19:11:29 +0000