diff options
-rw-r--r-- | plugins/syntax/numbers_syntax.ml | 61 | ||||
-rw-r--r-- | test-suite/output/NumbersSyntax.out | 56 | ||||
-rw-r--r-- | test-suite/output/NumbersSyntax.v | 46 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 18 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 12 | ||||
-rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 12 |
10 files changed, 161 insertions, 62 deletions
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 21b7115b6..4375d5e0f 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -14,23 +14,22 @@ open Bigint open Libnames open Rawterm -(*** Constants for locating the int31 and bigN ***) - - +(*** 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) -(* copied on g_zsyntax.ml, where it is said to be a temporary hack*) -(* takes a path an identifier in the form of a string list and a string, - returns a kernel_name *) -let make_kn dir id = Libnames.encode_mind (make_dir dir) (Names.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_mpdot dir modname id = + let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label modname) + in make_mind mp id (* int31 stuff *) let int31_module = ["Coq"; "Numbers"; "Cyclic"; "Int31"; "Int31"] let int31_path = make_path int31_module "int31" -let int31_id = make_kn int31_module +let int31_id = make_mind_mpfile int31_module let int31_scope = "int31_scope" let int31_construct = ConstructRef ((int31_id "int31",0),1) @@ -42,18 +41,14 @@ let int31_1 = ConstructRef ((int31_id "digits",0),2) (* bigN stuff*) let zn2z_module = ["Coq"; "Numbers"; "Cyclic"; "DoubleCyclic"; "DoubleType"] let zn2z_path = make_path zn2z_module "zn2z" -let zn2z_id = make_kn zn2z_module +let zn2z_id = make_mind_mpfile zn2z_module let zn2z_W0 = ConstructRef ((zn2z_id "zn2z",0),1) let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2) let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN" ] let bigN_path = make_path (bigN_module@["BigN"]) "t" -(* big ugly hack *) -let bigN_id id = let kn = - ((Names.MPdot ((Names.MPfile (make_dir bigN_module)), - Names.mk_label "BigN")), - [], Names.id_of_string id) in (Obj.magic (kn,kn) : Names.mutual_inductive) +let bigN_t = make_mind_mpdot bigN_module "BigN" "t_" let bigN_scope = "bigN_scope" (* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *) @@ -71,7 +66,7 @@ let bigN_constructor = 2*(to_int quo) in fun i -> - ConstructRef ((bigN_id "t_",0), + ConstructRef ((bigN_t,0), if less_than i n_inlined then (to_int i)+1 else @@ -81,25 +76,20 @@ let bigN_constructor = (*bigZ stuff*) let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ] let bigZ_path = make_path (bigZ_module@["BigZ"]) "t" -(* big ugly hack bis *) -let bigZ_id id = let kn = ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)), - Names.mk_label "BigZ")), - [], Names.id_of_string id) in (Obj.magic (kn,kn): Names.mutual_inductive) +let bigZ_t = make_mind_mpdot bigZ_module "BigZ" "t_" let bigZ_scope = "bigZ_scope" -let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1) -let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2) +let bigZ_pos = ConstructRef ((bigZ_t,0),1) +let bigZ_neg = ConstructRef ((bigZ_t,0),2) (*bigQ stuff*) let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"] -let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"] let bigQ_path = make_path (bigQ_module@["BigQ"]) "t" -(* big ugly hack bis *) -let bigQ_id = make_kn qmake_module +let bigQ_t = make_mind_mpdot bigQ_module "BigQ" "t_" let bigQ_scope = "bigQ_scope" -let bigQ_z = ConstructRef ((bigQ_id "q_type",0),1) +let bigQ_z = ConstructRef ((bigQ_t,0),1) (*** Definition of the Non_closed exception, used in the pretty printing ***) @@ -311,7 +301,7 @@ let uninterp_bigZ rc = with Non_closed -> None -(* Actually declares the interpreter for bigN *) +(* Actually declares the interpreter for bigZ *) let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ @@ -323,21 +313,18 @@ let _ = Notation.declare_numeral_interpreter bigZ_scope (*** Parsing for bigQ in digital notation ***) let interp_bigQ dloc n = let ref_z = RRef (dloc, bigQ_z) in - let ref_pos = RRef (dloc, bigZ_pos) in - let ref_neg = RRef (dloc, bigZ_neg) in - if is_pos_or_zero n then - RApp (dloc, ref_z, - [RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])]) - else - RApp (dloc, ref_z, - [RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])]) - -let uninterp_bigQ rc = None + RApp (dloc, ref_z, [interp_bigZ dloc n]) +let uninterp_bigQ rc = + try match rc with + | RApp (_, RRef(_,c), [one_arg]) when c = bigQ_z -> + Some (bigint_of_bigZ one_arg) + | _ -> None (* we don't pretty-print yet fractions *) + with Non_closed -> None (* Actually declares the interpreter for bigQ *) let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([], uninterp_bigQ, + ([RRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ, true) diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out new file mode 100644 index 000000000..1a8f4eff1 --- /dev/null +++ b/test-suite/output/NumbersSyntax.out @@ -0,0 +1,56 @@ +I31 + : digits31 int31 +2 + : int31 +660865024 + : int31 +2 + 2 + : int31 +2 + 2 + : int31 + = 4 + : int31 + = 710436486 + : int31 +2 + : BigN.t_ +1000000000000000000 + : BigN.t_ +2 + 2 + : BigN.t_ +2 + 2 + : BigN.t_ + = 4 + : BigN.t_ + = 37151199385380486 + : BigN.t_ +2 + : BigZ.t_ +-1000000000000000000 + : BigZ.t_ +2 + 2 + : BigZ.t_ +2 + 2 + : BigZ.t_ + = 4 + : BigZ.t_ + = 37151199385380486 + : BigZ.t_ +2 + : BigQ.t_ +-1000000000000000000 + : BigQ.t_ +2 + 2 + : bigQ +2 + 2 + : bigQ + = 4 + : bigQ + = 37151199385380486 + : bigQ +BigQ.Qq 6562%bigZ 456%bigN + : BigQ.t_ + = BigQ.Qq 3281%bigZ 228%bigN + : bigQ + = BigQ.Qq 1%bigZ 10000%bigN + : bigQ diff --git a/test-suite/output/NumbersSyntax.v b/test-suite/output/NumbersSyntax.v new file mode 100644 index 000000000..3f6a40bcb --- /dev/null +++ b/test-suite/output/NumbersSyntax.v @@ -0,0 +1,46 @@ + +Require Import BigQ. + +Open Scope int31_scope. +Check I31. (* Would be nice to have I31 : digits->digits->...->int31 + For the moment, I31 : digits31 int31, which is better + than (fix nfun .....) size int31 *) +Check 2. +Check 1000000000000000000. (* = 660865024, after modulo 2^31 *) +Check (add31 2 2). +Check (2+2). +Eval compute in 2+2. +Eval compute in 65675757 * 565675998. +Close Scope int31_scope. + +Open Scope bigN_scope. +Check 2. +Check 1000000000000000000. +Check (BigN.add 2 2). +Check (2+2). +Eval compute in 2+2. +Eval compute in 65675757 * 565675998. +Close Scope bigN_scope. + +Open Scope bigZ_scope. +Check 2. +Check -1000000000000000000. +Check (BigZ.add 2 2). +Check (2+2). +Eval compute in 2+2. +Eval compute in 65675757 * 565675998. +Close Scope bigN_scope. + +Open Scope bigQ_scope. +Check 2. +Check -1000000000000000000. +Check (BigQ.add 2 2). +Check (2+2). +Eval compute in 2+2. +Eval compute in 65675757 * 565675998. +(* fractions *) +Check (BigQ.Qq 6562%bigZ 456%bigN). + (* Having to say %bigZ and %bigN is a BUG! *) +Eval compute in (BigQ.red (BigQ.Qq 6562%bigZ 456%bigN)). +Eval compute in (1/10000). +Close Scope bigQ_scope. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 67d15b499..7d795cf50 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -24,8 +24,8 @@ Require Import BigNumPrelude. Require Import CyclicAxioms. Require Import ROmega. -Open Scope nat_scope. -Open Scope int31_scope. +Local Open Scope nat_scope. +Local Open Scope int31_scope. Section Basics. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 1168e7fd6..23c2c36a2 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -40,7 +40,9 @@ Inductive digits : Type := D0 | D1. (** The type [int31] has a unique constructor [I31] that expects 31 arguments of type [digits]. *) -Inductive int31 : Type := I31 : nfun digits size int31. +Definition digits31 t := Eval compute in nfun digits size t. + +Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault @@ -50,7 +52,7 @@ Register int31 as int31 type in "coq_int31" by True. Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. -Open Scope int31_scope. +Local Open Scope int31_scope. (** * Constants *) diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 6e8ca37ca..2e7604b0d 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -46,11 +46,11 @@ Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope. Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope. Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. -Open Scope bigZ_scope. +Local Open Scope bigZ_scope. (** Some additional results about [BigZ] *) -Theorem spec_to_Z: forall n:bigZ, +Theorem spec_to_Z: forall n : bigZ, BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z. Proof. intros n; case n; simpl; intros p; diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index e2be10ad9..d3f4776a6 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -19,15 +19,15 @@ Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig. Delimit Scope NumScope with Num. Bind Scope NumScope with Z.t. Local Open Scope NumScope. -Notation "[ x ]" := (Z.to_Z x) : NumScope. -Infix "==" := Z.eq (at level 70) : NumScope. -Notation "0" := Z.zero : NumScope. -Infix "+" := Z.add : NumScope. -Infix "-" := Z.sub : NumScope. -Infix "*" := Z.mul : NumScope. -Notation "- x" := (Z.opp x) : NumScope. -Infix "<=" := Z.le : NumScope. -Infix "<" := Z.lt : NumScope. +Local Notation "[ x ]" := (Z.to_Z x) : NumScope. +Local Infix "==" := Z.eq (at level 70) : NumScope. +Local Notation "0" := Z.zero : NumScope. +Local Infix "+" := Z.add : NumScope. +Local Infix "-" := Z.sub : NumScope. +Local Infix "*" := Z.mul : NumScope. +Local Notation "- x" := (Z.opp x) : NumScope. +Local Infix "<=" := Z.le : NumScope. +Local Infix "<" := Z.lt : NumScope. Hint Rewrite Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 4cc867898..ba457ffb8 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -51,11 +51,11 @@ Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. -Open Scope bigN_scope. +Local Open Scope bigN_scope. (** Example of reasoning about [BigN] *) -Theorem succ_pred: forall q:bigN, +Theorem succ_pred: forall q : bigN, 0 < q -> BigN.succ (BigN.pred q) == q. Proof. intros; apply succ_pred. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 2b199858f..49e7d7256 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -20,12 +20,12 @@ Module NSig_NAxioms (N:NType) <: NAxiomsSig. Delimit Scope NumScope with Num. Bind Scope NumScope with N.t. Local Open Scope NumScope. -Notation "[ x ]" := (N.to_Z x) : NumScope. -Infix "==" := N.eq (at level 70) : NumScope. -Notation "0" := N.zero : NumScope. -Infix "+" := N.add : NumScope. -Infix "-" := N.sub : NumScope. -Infix "*" := N.mul : NumScope. +Local Notation "[ x ]" := (N.to_Z x) : NumScope. +Local Infix "==" := N.eq (at level 70) : NumScope. +Local Notation "0" := N.zero : NumScope. +Local Infix "+" := N.add : NumScope. +Local Infix "-" := N.sub : NumScope. +Local Infix "*" := N.mul : NumScope. Hint Rewrite N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub : num. diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 38542c12b..eb0237f4a 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -10,7 +10,8 @@ (*i $Id$ i*) -Require Import Field Qfield BigN BigZ QSig QMake. +Require Export BigZ. +Require Import Field Qfield QSig QMake. (** We choose for BigQ an implemention with multiple representation of 0: 0, 1/0, 2/0 etc. @@ -43,6 +44,13 @@ Notation bigQ := BigQ.t. Delimit Scope bigQ_scope with bigQ. Bind Scope bigQ_scope with bigQ. Bind Scope bigQ_scope with BigQ.t. +Bind Scope bigQ_scope with BigQ.t_. + +(** BUG: the previous Bind Scope don't seem to work, and idem with BigN/BigZ. + For instance "Check (BigQ.opp 10)" fails when bigQ_scope is closed. + (whereas "Check (Int31.add31 10 10)" is ok). Something with modules ? + Adding an Arguments Scope helps, but this isn't a satisfactory solution. +*) Infix "+" := BigQ.add : bigQ_scope. Infix "-" := BigQ.sub : bigQ_scope. @@ -58,7 +66,7 @@ Notation "x > y" := (BigQ.lt y x)(only parsing) : bigQ_scope. Notation "x >= y" := (BigQ.le y x)(only parsing) : bigQ_scope. Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope. -Open Scope bigQ_scope. +Local Open Scope bigQ_scope. (** [BigQ] is a setoid *) |