diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-27 17:53:43 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-27 17:53:43 +0000 |
commit | 7f2c52bcf588abfcbf30530bae240244229304a4 (patch) | |
tree | 6a74c2b13c24e66076177d51e188724c06ef0720 | |
parent | 999ac2c4c2bb6c7397c88ee1b6f39bdb43eaecb1 (diff) |
Parsing files for numerals (+ ascii/string) moved into plugins
Idea: make coqtop more independant of the standard library.
In the future, we can imagine loading the syntax for numerals right
after their definition. For the moment, it is easier to stay lazy
and load the syntax plugins slightly before the definitions.
After this commit, the main (sole ?) references to theories/
from the core ml files are in Coqlib (but many parts of coqlib
are only used by plugins), and it mainly concerns Init
(+ Logic/JMeq and maybe a few others).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
21 files changed, 35 insertions, 12 deletions
diff --git a/Makefile.common b/Makefile.common index b17d37195..5a2817e41 100644 --- a/Makefile.common +++ b/Makefile.common @@ -69,7 +69,7 @@ SRCDIRS:=\ omega romega micromega quote ring dp \ setoid_ring xml extraction interface fourier \ cc funind firstorder field subtac \ - rtauto groebner ) + rtauto groebner syntax) # Order is relevent here because kernel and checker contain files # with the same name @@ -176,17 +176,24 @@ FOCMA:=plugins/firstorder/ground_plugin.cma CCCMA:=plugins/cc/cc_plugin.cma SUBTACCMA:=plugins/subtac/subtac_plugin.cma RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma +NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma +OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ + z_syntax_plugin.cma \ + numbers_syntax_plugin.cma \ + r_syntax_plugin.cma \ + ascii_syntax_plugin.cma \ + string_syntax_plugin.cma ) PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ - $(FUNINDCMA) $(GBCMA) + $(FUNINDCMA) $(GBCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ - $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) + $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINS:=$(PLUGINSCMA) PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index 03fb9c629..3eb27abbb 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -4,10 +4,4 @@ G_prim G_proofs G_tactic G_ltac -G_natsyntax -G_zsyntax -G_rsyntax -G_ascii_syntax -G_string_syntax G_decl_mode -G_intsyntax diff --git a/parsing/g_ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index f9ca94ff6..f9ca94ff6 100644 --- a/parsing/g_ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib new file mode 100644 index 000000000..54b5815c5 --- /dev/null +++ b/plugins/syntax/ascii_syntax_plugin.mllib @@ -0,0 +1,2 @@ +Ascii_syntax +Ascii_syntax_mod diff --git a/parsing/g_natsyntax.ml b/plugins/syntax/nat_syntax.ml index c62c81377..c62c81377 100644 --- a/parsing/g_natsyntax.ml +++ b/plugins/syntax/nat_syntax.ml diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib new file mode 100644 index 000000000..35af24819 --- /dev/null +++ b/plugins/syntax/nat_syntax_plugin.mllib @@ -0,0 +1,2 @@ +Nat_syntax +Nat_syntax_mod diff --git a/parsing/g_intsyntax.ml b/plugins/syntax/numbers_syntax.ml index 7cef2fac0..94e4c103a 100644 --- a/parsing/g_intsyntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -205,7 +205,7 @@ let bigN_of_pos_bigint dloc n = let result h word = RApp (dloc, ref_constructor h, if less_than h n_inlined then [word] else - [G_natsyntax.nat_of_int dloc (sub h n_inlined); + [Nat_syntax.nat_of_int dloc (sub h n_inlined); word]) in let hght = height n in diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib new file mode 100644 index 000000000..060f47c1f --- /dev/null +++ b/plugins/syntax/numbers_syntax_plugin.mllib @@ -0,0 +1,2 @@ +Numbers_syntax +Numbers_syntax_mod diff --git a/parsing/g_rsyntax.ml b/plugins/syntax/r_syntax.ml index 4a5972cc7..4a5972cc7 100644 --- a/parsing/g_rsyntax.ml +++ b/plugins/syntax/r_syntax.ml diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib new file mode 100644 index 000000000..b9ea91db3 --- /dev/null +++ b/plugins/syntax/r_syntax_plugin.mllib @@ -0,0 +1,2 @@ +R_syntax +R_syntax_mod diff --git a/parsing/g_string_syntax.ml b/plugins/syntax/string_syntax.ml index a936485d9..d1c263dc8 100644 --- a/parsing/g_string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -14,7 +14,7 @@ open Names open Pcoq open Libnames open Topconstr -open G_ascii_syntax +open Ascii_syntax open Rawterm open Coqlib diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib new file mode 100644 index 000000000..f73c447c8 --- /dev/null +++ b/plugins/syntax/string_syntax_plugin.mllib @@ -0,0 +1,2 @@ +String_syntax +String_syntax_mod diff --git a/parsing/g_zsyntax.ml b/plugins/syntax/z_syntax.ml index bfbe54c28..bfbe54c28 100644 --- a/parsing/g_zsyntax.ml +++ b/plugins/syntax/z_syntax.ml diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib new file mode 100644 index 000000000..cabaef820 --- /dev/null +++ b/plugins/syntax/z_syntax_plugin.mllib @@ -0,0 +1,2 @@ +Z_syntax +Z_syntax_mod diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 73e4924aa..2194b93a3 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -12,6 +12,8 @@ Set Implicit Arguments. Require Import Notations. Require Import Logic. +Declare ML Module "nat_syntax_plugin". + (** [unit] is a singleton datatype with sole inhabitant [tt] *) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 84de55e24..685c72470 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -15,7 +15,8 @@ Require Export Specif. Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. -(* Initially available plugins *) +(* Initially available plugins + (+ nat_syntax_plugin loaded in Datatypes) *) Declare ML Module "extraction_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 209eb5497..076bceba4 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -10,6 +10,8 @@ Unset Boxed Definitions. +Declare ML Module "z_syntax_plugin". + (**********************************************************************) (** Binary positive numbers *) diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 633cc8423..d890d9287 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -21,6 +21,8 @@ Require Export ZArith. Require Export Znumtheory. Require Export Zpow_facts. +Declare ML Module "numbers_syntax_plugin". + (* *** Nota Bene *** All results that were general enough has been moved in ZArith. Only remain here specialized lemmas and compatibility elements. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 63b8928fb..897d5c710 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -12,6 +12,7 @@ (** Definitions for the axiomatization *) (*********************************************************) +Declare ML Module "r_syntax_plugin". Require Export ZArith_base. Parameter R : Set. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 1f10f2aff..5a2cc9695 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -13,6 +13,7 @@ Require Import Bool. Require Import BinPos. +Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 59edf8187..7d6696b78 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -13,6 +13,7 @@ Require Import Arith. Require Import Ascii. +Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) |