summaryrefslogtreecommitdiff
path: root/plugins/syntax/numbers_syntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/numbers_syntax.ml')
-rw-r--r--plugins/syntax/numbers_syntax.ml69
1 files changed, 35 insertions, 34 deletions
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 5d43b353..b990c0d2 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* 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 *)
@@ -9,18 +9,19 @@
(* digit-based syntax for int31, bigN bigZ and bigQ *)
open Bigint
-open Libnames
+open Names
+open Globnames
open Glob_term
(*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
-let make_dir l = Names.make_dirpath (List.map Names.id_of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (Names.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 make_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id)
-let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
+let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
+let make_mind_mpfile dir id = make_mind (MPfile (make_dir dir)) id
let make_mind_mpdot dir modname id =
- let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label modname)
+ let mp = MPdot (MPfile (make_dir dir), Label.make modname)
in make_mind mp id
@@ -82,9 +83,9 @@ exception Non_closed
(* parses a *non-negative* integer (from bigint.ml) into an int31
wraps modulo 2^31 *)
let int31_of_pos_bigint dloc n =
- let ref_construct = GRef (dloc, int31_construct) in
- let ref_0 = GRef (dloc, int31_0) in
- let ref_1 = GRef (dloc, int31_1) in
+ let ref_construct = GRef (dloc, int31_construct, None) in
+ let ref_0 = GRef (dloc, int31_0, None) in
+ let ref_1 = GRef (dloc, int31_1, None) in
let rec args counter n =
if counter <= 0 then
[]
@@ -95,7 +96,7 @@ let int31_of_pos_bigint dloc n =
GApp (dloc, ref_construct, List.rev (args 31 n))
let error_negative dloc =
- Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
+ Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
let interp_int31 dloc n =
if is_pos_or_zero n then
@@ -109,12 +110,12 @@ let bigint_of_int31 =
let rec args_parsing args cur =
match args with
| [] -> cur
- | (GRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
- | (GRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur))
+ | (GRef (_,b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+ | (GRef (_,b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
| _ -> raise Non_closed
in
function
- | GApp (_, GRef (_, c), args) when c=int31_construct -> args_parsing args zero
+ | GApp (_, GRef (_, c, _), args) when eq_gr c int31_construct -> args_parsing args zero
| _ -> raise Non_closed
let uninterp_int31 i =
@@ -127,7 +128,7 @@ let uninterp_int31 i =
let _ = Notation.declare_numeral_interpreter int31_scope
(int31_path, int31_module)
interp_int31
- ([GRef (Util.dummy_loc, int31_construct)],
+ ([GRef (Loc.ghost, int31_construct, None)],
uninterp_int31,
true)
@@ -158,16 +159,16 @@ let height bi =
(* n must be a non-negative integer (from bigint.ml) *)
let word_of_pos_bigint dloc hght n =
- let ref_W0 = GRef (dloc, zn2z_W0) in
- let ref_WW = GRef (dloc, zn2z_WW) in
+ let ref_W0 = GRef (dloc, zn2z_W0, None) in
+ let ref_WW = GRef (dloc, zn2z_WW, None) in
let rec decomp hgt n =
if hgt <= 0 then
int31_of_pos_bigint dloc n
else if equal n zero then
- GApp (dloc, ref_W0, [GHole (dloc, Evd.InternalHole)])
+ GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
else
let (h,l) = split_at hgt n in
- GApp (dloc, ref_WW, [GHole (dloc, Evd.InternalHole);
+ GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
decomp (hgt-1) h;
decomp (hgt-1) l])
in
@@ -175,7 +176,7 @@ let word_of_pos_bigint dloc hght n =
let bigN_of_pos_bigint dloc n =
let h = height n in
- let ref_constructor = GRef (dloc, bigN_constructor h) in
+ let ref_constructor = GRef (dloc, bigN_constructor h, None) in
let word = word_of_pos_bigint dloc h n in
let args =
if h < n_inlined then [word]
@@ -184,7 +185,7 @@ let bigN_of_pos_bigint dloc n =
GApp (dloc, ref_constructor, args)
let bigN_error_negative dloc =
- Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
+ Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
let interp_bigN dloc n =
if is_pos_or_zero n then
@@ -198,14 +199,14 @@ let interp_bigN dloc n =
let bigint_of_word =
let rec get_height rc =
match rc with
- | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
+ | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW ->
1+max (get_height lft) (get_height rght)
| _ -> 0
in
let rec transform hght rc =
match rc with
- | GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero
- | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW->
+ | GApp (_,GRef(_,c,_),_) when eq_gr c zn2z_W0-> zero
+ | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW->
let new_hght = hght-1 in
add (mult (rank new_hght)
(transform new_hght lft))
@@ -235,7 +236,7 @@ let uninterp_bigN rc =
let bigN_list_of_constructors =
let rec build i =
if i < n_inlined+1 then
- GRef (Util.dummy_loc, bigN_constructor i)::(build (i+1))
+ GRef (Loc.ghost, bigN_constructor i,None)::(build (i+1))
else
[]
in
@@ -252,8 +253,8 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
(*** Parsing for bigZ in digital notation ***)
let interp_bigZ dloc n =
- let ref_pos = GRef (dloc, bigZ_pos) in
- let ref_neg = GRef (dloc, bigZ_neg) in
+ let ref_pos = GRef (dloc, bigZ_pos, None) in
+ let ref_neg = GRef (dloc, bigZ_neg, None) in
if is_pos_or_zero n then
GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
else
@@ -261,8 +262,8 @@ let interp_bigZ dloc n =
(* pretty printing functions for bigZ *)
let bigint_of_bigZ = function
- | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
- | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_neg ->
+ | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+ | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_neg ->
let opp_val = bigint_of_bigN one_arg in
if equal opp_val zero then
raise Non_closed
@@ -281,19 +282,19 @@ let uninterp_bigZ rc =
let _ = Notation.declare_numeral_interpreter bigZ_scope
(bigZ_path, bigZ_module)
interp_bigZ
- ([GRef (Util.dummy_loc, bigZ_pos);
- GRef (Util.dummy_loc, bigZ_neg)],
+ ([GRef (Loc.ghost, bigZ_pos, None);
+ GRef (Loc.ghost, bigZ_neg, None)],
uninterp_bigZ,
true)
(*** Parsing for bigQ in digital notation ***)
let interp_bigQ dloc n =
- let ref_z = GRef (dloc, bigQ_z) in
+ let ref_z = GRef (dloc, bigQ_z, None) in
GApp (dloc, ref_z, [interp_bigZ dloc n])
let uninterp_bigQ rc =
try match rc with
- | GApp (_, GRef(_,c), [one_arg]) when c = bigQ_z ->
+ | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigQ_z ->
Some (bigint_of_bigZ one_arg)
| _ -> None (* we don't pretty-print yet fractions *)
with Non_closed -> None
@@ -302,5 +303,5 @@ let uninterp_bigQ rc =
let _ = Notation.declare_numeral_interpreter bigQ_scope
(bigQ_path, bigQ_module)
interp_bigQ
- ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
+ ([GRef (Loc.ghost, bigQ_z, None)], uninterp_bigQ,
true)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 23:31:00 +0000