From 68e62a195d6228befb75b4e2edd59bc58b1cdb0c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 23 Sep 2003 15:12:46 +0000 Subject: [PATCH] Now mathql_generator compiles before mathql_interpreter. This feature, announced in my Ph.D. thesis, will allow the interpreter to interact with the generator. --- helm/ocaml/Makefile.in | 4 +-- helm/ocaml/mathql/.cvsignore | 2 +- helm/ocaml/mathql/.depend | 10 ++---- helm/ocaml/mathql/Makefile | 13 +++----- .../mQueryMisc.ml | 32 +++++++++++++------ .../mQueryMisc.mli | 23 +++++++------ helm/ocaml/mathql_generator/Makefile | 2 +- .../mathql_generator/cGLocateInductive.ml | 2 +- .../mathql_generator/cGMatchConclusion.ml | 4 +-- helm/ocaml/mathql_interpreter/.cvsignore | 2 +- helm/ocaml/mathql_interpreter/.depend | 16 ++++++---- helm/ocaml/mathql_interpreter/Makefile | 15 +++++---- .../mQueryTLexer.mll | 0 .../mQueryTParser.mly | 0 .../mQueryUtil.ml | 13 -------- .../mQueryUtil.mli | 5 --- 16 files changed, 71 insertions(+), 72 deletions(-) rename helm/ocaml/{mathql_interpreter => mathql}/mQueryMisc.ml (86%) rename helm/ocaml/{mathql_interpreter => mathql}/mQueryMisc.mli (86%) rename helm/ocaml/{mathql => mathql_interpreter}/mQueryTLexer.mll (100%) rename helm/ocaml/{mathql => mathql_interpreter}/mQueryTParser.mly (100%) rename helm/ocaml/{mathql => mathql_interpreter}/mQueryUtil.ml (94%) rename helm/ocaml/{mathql => mathql_interpreter}/mQueryUtil.mli (94%) diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 8eae88814..c0ef52ff8 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,8 +1,8 @@ # Warning: the modules must be in compilation order MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ cic_cache cic_proof_checking cic_textual_parser \ - tex_cic_textual_parser cic_unification mathql mathql_interpreter \ - mathql_generator cic_omdoc tactics cic_transformations + tex_cic_textual_parser cic_unification mathql mathql_generator \ + mathql_interpreter cic_omdoc tactics cic_transformations OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/mathql/.cvsignore b/helm/ocaml/mathql/.cvsignore index cd9b591e3..6b3eba302 100644 --- a/helm/ocaml/mathql/.cvsignore +++ b/helm/ocaml/mathql/.cvsignore @@ -1 +1 @@ -*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli +*.cm[iaox] *.cmxa diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend index 769e30c89..30dbaa280 100644 --- a/helm/ocaml/mathql/.depend +++ b/helm/ocaml/mathql/.depend @@ -1,8 +1,2 @@ -mQueryTParser.cmi: mathQL.cmo -mQueryUtil.cmi: mathQL.cmo -mQueryTParser.cmo: mathQL.cmo mQueryTParser.cmi -mQueryTParser.cmx: mathQL.cmx mQueryTParser.cmi -mQueryTLexer.cmo: mQueryTParser.cmi -mQueryTLexer.cmx: mQueryTParser.cmx -mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mathQL.cmo mQueryUtil.cmi -mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mathQL.cmx mQueryUtil.cmi +mQueryMisc.cmo: mQueryMisc.cmi +mQueryMisc.cmx: mQueryMisc.cmi diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile index 6d5481948..6554bf698 100644 --- a/helm/ocaml/mathql/Makefile +++ b/helm/ocaml/mathql/Makefile @@ -1,16 +1,13 @@ PACKAGE = mathql -REQUIRES = helm-urimanager +REQUIRES = helm-cic helm-cic_textual_parser PREDICATES = -INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli +INTERFACE_FILES = mQueryMisc.mli -IMPLEMENTATION_FILES = mathQL.ml mQueryTParser.ml mQueryTLexer.ml \ - mQueryUtil.ml +IMPLEMENTATION_FILES = mathQL.ml mQueryMisc.ml -EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi mQueryTLexer.cmi \ - mQueryTLexer.mll mQueryTParser.mly +EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi -EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ - mQueryTLexer.ml +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/mathql_interpreter/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml similarity index 86% rename from helm/ocaml/mathql_interpreter/mQueryMisc.ml rename to helm/ocaml/mathql/mQueryMisc.ml index cb6f92a21..0d8dcd5d9 100644 --- a/helm/ocaml/mathql_interpreter/mQueryMisc.ml +++ b/helm/ocaml/mathql/mQueryMisc.ml @@ -23,15 +23,16 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 15/01/2003 *) -(* *) -(* *) -(******************************************************************************) +(****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* Ferruccio Guidi *) +(* 15/01/2003 *) +(* *) +(* *) +(****************************************************************************) exception IllFormedUri of string;; @@ -109,3 +110,16 @@ let term_of_cic_textual_parser_uri uri = | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) ;; + +(* conversion functions *****************************************************) + +type uriref = UriManager.uri * (int list) + +let string_of_uriref (uri, fi) = + let module UM = UriManager in + let str = UM.string_of_uri uri in + let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in + match fi with + | [] -> str + | [t] -> str ^ xp t ^ ")" + | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" diff --git a/helm/ocaml/mathql_interpreter/mQueryMisc.mli b/helm/ocaml/mathql/mQueryMisc.mli similarity index 86% rename from helm/ocaml/mathql_interpreter/mQueryMisc.mli rename to helm/ocaml/mathql/mQueryMisc.mli index 7c0aa7468..6fb600dab 100644 --- a/helm/ocaml/mathql_interpreter/mQueryMisc.mli +++ b/helm/ocaml/mathql/mQueryMisc.mli @@ -23,15 +23,16 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 15/01/2003 *) -(* *) -(* *) -(******************************************************************************) +(****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* Ferruccio Guidi *) +(* 15/01/2003 *) +(* *) +(* *) +(****************************************************************************) exception IllFormedUri of string @@ -39,3 +40,7 @@ val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string + +type uriref = UriManager.uri * (int list) + +val string_of_uriref : uriref -> string diff --git a/helm/ocaml/mathql_generator/Makefile b/helm/ocaml/mathql_generator/Makefile index 3079a6643..a72f17ab2 100644 --- a/helm/ocaml/mathql_generator/Makefile +++ b/helm/ocaml/mathql_generator/Makefile @@ -1,7 +1,7 @@ PACKAGE = mathql_generator REQUIRES = helm-cic helm-cic_proof_checking helm-mathql - + PREDICATES = INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \ diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml index 032060fd3..c5734f242 100644 --- a/helm/ocaml/mathql_generator/cGLocateInductive.ml +++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml @@ -30,7 +30,7 @@ exception NotAnInductiveDefinition let get_constraints = function | Cic.MutInd (uri, t, _) -> - let uri = MQueryUtil.string_of_uriref (uri, [t]) in + let uri = MQueryMisc.string_of_uriref (uri, [t]) in let constr_obj = [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)] in diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml index 28639c8f7..bb87b461e 100644 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml @@ -43,7 +43,7 @@ let sort_entries entries = let levels_of_term metasenv context term = let module TC = CicTypeChecker in let module Red = CicReduction in - let module Util = MQueryUtil in + let module Misc = MQueryMisc in let degree t = let rec degree_aux = function | Cic.Sort _ -> 1 @@ -64,7 +64,7 @@ let levels_of_term metasenv context term = in let inspect_uri main l uri tc v term = let d = degree term in - entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l + entry_in (Misc.string_of_uriref (uri, tc), main, 2 * v + d - 1) l in let rec inspect_term main l v term = match term with Cic.Rel _ -> l diff --git a/helm/ocaml/mathql_interpreter/.cvsignore b/helm/ocaml/mathql_interpreter/.cvsignore index 6b3eba302..cd9b591e3 100644 --- a/helm/ocaml/mathql_interpreter/.cvsignore +++ b/helm/ocaml/mathql_interpreter/.cvsignore @@ -1 +1 @@ -*.cm[iaox] *.cmxa +*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 962eaf63a..7d9b3c625 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -1,21 +1,25 @@ mQIConn.cmi: mQIMap.cmi mQIProperty.cmi: mQIConn.cmi mQueryInterpreter.cmi: mQIConn.cmi -mQueryMisc.cmo: mQueryMisc.cmi -mQueryMisc.cmx: mQueryMisc.cmi +mQueryTParser.cmo: mQueryTParser.cmi +mQueryTParser.cmx: mQueryTParser.cmi +mQueryTLexer.cmo: mQueryTParser.cmi +mQueryTLexer.cmx: mQueryTParser.cmx +mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mQueryUtil.cmi +mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mQueryUtil.cmi mQIUtil.cmo: mQIUtil.cmi mQIUtil.cmx: mQIUtil.cmi mQIPostgres.cmo: mQIPostgres.cmi mQIPostgres.cmx: mQIPostgres.cmi -mQIMap.cmo: mQIMap.cmi -mQIMap.cmx: mQIMap.cmi +mQIMap.cmo: mQueryUtil.cmi mQIMap.cmi +mQIMap.cmx: mQueryUtil.cmx mQIMap.cmi mQIConn.cmo: mQIMap.cmi mQIPostgres.cmi mQIConn.cmi mQIConn.cmx: mQIMap.cmx mQIPostgres.cmx mQIConn.cmi mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIPostgres.cmi mQIUtil.cmi \ mQIProperty.cmi mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIPostgres.cmx mQIUtil.cmx \ mQIProperty.cmi -mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi \ +mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi mQueryUtil.cmi \ mQueryInterpreter.cmi -mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx \ +mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx mQueryUtil.cmx \ mQueryInterpreter.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index be32ff48c..88c66ac8e 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -1,17 +1,20 @@ PACKAGE = mathql_interpreter -REQUIRES = helm-cic helm-cic_textual_parser helm-mathql postgres +REQUIRES = helm-urimanager helm-mathql postgres #natile-galax PREDICATES = -INTERFACE_FILES = mQueryMisc.mli mQIUtil.mli \ +INTERFACE_FILES = mQueryUtil.mli mQIUtil.mli \ mQIPostgres.mli mQIMap.mli mQIConn.mli \ - mQIProperty.mli mQueryInterpreter.mli + mQIProperty.mli mQueryInterpreter.mli -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +IMPLEMENTATION_FILES = mQueryTParser.ml mQueryTLexer.ml \ + $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_INSTALL = mQueryTLexer.cmi \ + mQueryTLexer.mll mQueryTParser.mly -EXTRA_OBJECTS_TO_CLEAN = +EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ + mQueryTLexer.ml include ../Makefile.common diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll similarity index 100% rename from helm/ocaml/mathql/mQueryTLexer.mll rename to helm/ocaml/mathql_interpreter/mQueryTLexer.mll diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly similarity index 100% rename from helm/ocaml/mathql/mQueryTParser.mly rename to helm/ocaml/mathql_interpreter/mQueryTParser.mly diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql_interpreter/mQueryUtil.ml similarity index 94% rename from helm/ocaml/mathql/mQueryUtil.ml rename to helm/ocaml/mathql_interpreter/mQueryUtil.ml index 349c2ac55..30e6688ee 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql_interpreter/mQueryUtil.ml @@ -216,16 +216,3 @@ let list_meet f l1 l2 = end in aux (l1, l2) -(* conversion functions *****************************************************) - -type uriref = UriManager.uri * (int list) - -let string_of_uriref (uri, fi) = - let module UM = UriManager in - let str = UM.string_of_uri uri in - let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in - match fi with - | [] -> str - | [t] -> str ^ xp t ^ ")" - | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" - diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql_interpreter/mQueryUtil.mli similarity index 94% rename from helm/ocaml/mathql/mQueryUtil.mli rename to helm/ocaml/mathql_interpreter/mQueryUtil.mli index bb38dc91d..2a3c80b83 100644 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ b/helm/ocaml/mathql_interpreter/mQueryUtil.mli @@ -47,8 +47,3 @@ type 'a comparison = Lt val list_join : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list - - -type uriref = UriManager.uri * (int list) - -val string_of_uriref : uriref -> string -- 2.39.2