From f30347427516e70bb720fc7ed1a08a4f055bae9e Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 12 Nov 2009 11:10:46 +0000 Subject: Repair interpretation of numeral for BigQ, add a printer (close #2160) on the way: - Added a testsuite output file - Try to avoid nasty unfolding (fix nfun ...) in type of I31. Idealy we would need a "Eval compute in" for the type of a inductive constructor - Stop opening Scopes for BigQ, BigN, BigZ by default The user should do some Open Scope. TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope (and so on for other operations), even with some Bind Scope around. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/syntax/numbers_syntax.ml | 61 ++++++++++++++++------------------------ 1 file changed, 24 insertions(+), 37 deletions(-) (limited to 'plugins/syntax') 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) -- cgit v1.2.3