aboutsummaryrefslogtreecommitdiffhomepage
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.ml64
1 files changed, 32 insertions, 32 deletions
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 3ee64ba7e..e23852bf8 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -87,9 +87,9 @@ exception Non_closed
(* parses a *non-negative* integer (from bigint.ml) into an int31
wraps modulo 2^31 *)
let int31_of_pos_bigint ?loc n =
- let ref_construct = Loc.tag ?loc @@ GRef (int31_construct, None) in
- let ref_0 = Loc.tag ?loc @@ GRef (int31_0, None) in
- let ref_1 = Loc.tag ?loc @@ GRef (int31_1, None) in
+ let ref_construct = CAst.make ?loc @@ GRef (int31_construct, None) in
+ let ref_0 = CAst.make ?loc @@ GRef (int31_0, None) in
+ let ref_1 = CAst.make ?loc @@ GRef (int31_1, None) in
let rec args counter n =
if counter <= 0 then
[]
@@ -97,7 +97,7 @@ let int31_of_pos_bigint ?loc n =
let (q,r) = div2_with_rest n in
(if r then ref_1 else ref_0)::(args (counter-1) q)
in
- Loc.tag ?loc @@ GApp (ref_construct, List.rev (args 31 n))
+ CAst.make ?loc @@ GApp (ref_construct, List.rev (args 31 n))
let error_negative ?loc =
CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
@@ -114,12 +114,12 @@ let bigint_of_int31 =
let rec args_parsing args cur =
match args with
| [] -> 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))
+ | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+ | { CAst.v = 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 eq_gr c int31_construct -> args_parsing args zero
+ | { CAst.v = GApp ({ CAst.v = GRef (c, _)}, args) } when eq_gr c int31_construct -> args_parsing args zero
| _ -> raise Non_closed
let uninterp_int31 i =
@@ -132,7 +132,7 @@ let uninterp_int31 i =
let _ = Notation.declare_numeral_interpreter int31_scope
(int31_path, int31_module)
interp_int31
- ([Loc.tag @@ GRef (int31_construct, None)],
+ ([CAst.make @@ GRef (int31_construct, None)],
uninterp_int31,
true)
@@ -163,16 +163,16 @@ let height bi =
(* n must be a non-negative integer (from bigint.ml) *)
let word_of_pos_bigint ?loc hght n =
- let ref_W0 = Loc.tag ?loc @@ GRef (zn2z_W0, None) in
- let ref_WW = Loc.tag ?loc @@ GRef (zn2z_WW, None) in
+ let ref_W0 = CAst.make ?loc @@ GRef (zn2z_W0, None) in
+ let ref_WW = CAst.make ?loc @@ GRef (zn2z_WW, None) in
let rec decomp hgt n =
if hgt <= 0 then
int31_of_pos_bigint ?loc n
else if equal n zero then
- Loc.tag ?loc @@ GApp (ref_W0, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
+ CAst.make ?loc @@ GApp (ref_W0, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
else
let (h,l) = split_at hgt n in
- Loc.tag ?loc @@ GApp (ref_WW, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
+ CAst.make ?loc @@ GApp (ref_WW, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
decomp (hgt-1) h;
decomp (hgt-1) l])
in
@@ -180,13 +180,13 @@ let word_of_pos_bigint ?loc hght n =
let bigN_of_pos_bigint ?loc n =
let h = height n in
- let ref_constructor = Loc.tag ?loc @@ GRef (bigN_constructor h, None) in
+ let ref_constructor = CAst.make ?loc @@ GRef (bigN_constructor h, None) in
let word = word_of_pos_bigint ?loc h n in
let args =
if h < n_inlined then [word]
else [Nat_syntax_plugin.Nat_syntax.nat_of_int ?loc (of_int (h-n_inlined));word]
in
- Loc.tag ?loc @@ GApp (ref_constructor, args)
+ CAst.make ?loc @@ GApp (ref_constructor, args)
let bigN_error_negative ?loc =
CErrors.user_err ?loc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.")
@@ -203,14 +203,14 @@ let interp_bigN ?loc n =
let bigint_of_word =
let rec get_height rc =
match rc with
- | _, GApp ((_, GRef(c,_)), [_;lft;rght]) when eq_gr c zn2z_WW ->
+ | { CAst.v = GApp ({ CAst.v = 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 eq_gr c zn2z_W0-> zero
- | _, GApp ((_, GRef(c,_)), [_;lft;rght]) when eq_gr c zn2z_WW->
+ | { CAst.v = GApp ({ CAst.v = GRef(c,_)},_)} when eq_gr c zn2z_W0-> zero
+ | { CAst.v = GApp ({ CAst.v = 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))
@@ -223,8 +223,8 @@ let bigint_of_word =
let bigint_of_bigN rc =
match rc with
- | _, GApp (_,[one_arg]) -> bigint_of_word one_arg
- | _, GApp (_,[_;second_arg]) -> bigint_of_word second_arg
+ | { CAst.v = GApp (_,[one_arg]) } -> bigint_of_word one_arg
+ | { CAst.v = GApp (_,[_;second_arg]) } -> bigint_of_word second_arg
| _ -> raise Non_closed
let uninterp_bigN rc =
@@ -240,7 +240,7 @@ let uninterp_bigN rc =
let bigN_list_of_constructors =
let rec build i =
if i < n_inlined+1 then
- (Loc.tag @@ GRef (bigN_constructor i,None))::(build (i+1))
+ (CAst.make @@ GRef (bigN_constructor i,None))::(build (i+1))
else
[]
in
@@ -257,17 +257,17 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
(*** Parsing for bigZ in digital notation ***)
let interp_bigZ ?loc n =
- let ref_pos = Loc.tag ?loc @@ GRef (bigZ_pos, None) in
- let ref_neg = Loc.tag ?loc @@ GRef (bigZ_neg, None) in
+ let ref_pos = CAst.make ?loc @@ GRef (bigZ_pos, None) in
+ let ref_neg = CAst.make ?loc @@ GRef (bigZ_neg, None) in
if is_pos_or_zero n then
- Loc.tag ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n])
+ CAst.make ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n])
else
- Loc.tag ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)])
+ CAst.make ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)])
(* pretty printing functions for bigZ *)
let bigint_of_bigZ = function
- | _, 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 ->
+ | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+ | { CAst.v = GApp ({ CAst.v = 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
@@ -286,19 +286,19 @@ let uninterp_bigZ rc =
let _ = Notation.declare_numeral_interpreter bigZ_scope
(bigZ_path, bigZ_module)
interp_bigZ
- ([Loc.tag @@ GRef (bigZ_pos, None);
- Loc.tag @@ GRef (bigZ_neg, None)],
+ ([CAst.make @@ GRef (bigZ_pos, None);
+ CAst.make @@ GRef (bigZ_neg, None)],
uninterp_bigZ,
true)
(*** Parsing for bigQ in digital notation ***)
let interp_bigQ ?loc n =
- let ref_z = Loc.tag ?loc @@ GRef (bigQ_z, None) in
- Loc.tag ?loc @@ GApp (ref_z, [interp_bigZ ?loc n])
+ let ref_z = CAst.make ?loc @@ GRef (bigQ_z, None) in
+ CAst.make ?loc @@ GApp (ref_z, [interp_bigZ ?loc n])
let uninterp_bigQ rc =
try match rc with
- | _, GApp ((_, GRef(c,_)), [one_arg]) when eq_gr c bigQ_z ->
+ | { CAst.v = GApp ({ CAst.v = 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
@@ -307,5 +307,5 @@ let uninterp_bigQ rc =
let _ = Notation.declare_numeral_interpreter bigQ_scope
(bigQ_path, bigQ_module)
interp_bigQ
- ([Loc.tag @@ GRef (bigQ_z, None)], uninterp_bigQ,
+ ([CAst.make @@ GRef (bigQ_z, None)], uninterp_bigQ,
true)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 20:14:01 +0000