From a696aae5ea794cd43fd3d83d37a0345d2a1387b3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Dec 2005 14:09:31 +0000 Subject: [PATCH] 1. Several files in grafite that should be in grafite_parser moved there. 2. grafiteEngine is now generalized over the function baseuri_of_script (that associates the baseuri to a .ma file). This function is used to execute the Include statement. However, it seems to me that this shows a problem in the architecture (since the only possible implementation of the function involves using the grafie_parser right now). Modified Files in ocaml: METAS/meta.helm-grafite_parser.src grafite/.depend grafite/Makefile grafite/cicNotation.ml grafite/cicNotation.mli grafite2/disambiguatePp.ml grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml grafite2/grafiteMisc.mli grafite_parser/.depend grafite_parser/Makefile Modified Files in matita: matitaEngine.ml matitaEngine.mli matitaGui.ml matitaInit.ml matitaScript.ml matitacLib.ml matitaclean.ml matitadep.ml Added Files in ocaml: grafite_parser/cicNotation2.ml grafite_parser/cicNotation2.mli grafite_parser/grafiteParser.ml grafite_parser/grafiteParser.mli grafite_parser/grafiteParserMisc.ml grafite_parser/grafiteParserMisc.mli grafite_parser/print_grammar.ml grafite_parser/test_dep.ml grafite_parser/test_parser.ml Removed Files in ocaml: grafite/grafiteParser.ml grafite/grafiteParser.mli grafite/print_grammar.ml grafite/test_dep.ml grafite/test_parser.ml --- helm/ocaml/METAS/meta.helm-grafite_parser.src | 2 +- helm/ocaml/grafite/.depend | 11 +-- helm/ocaml/grafite/Makefile | 43 ---------- helm/ocaml/grafite/cicNotation.ml | 11 --- helm/ocaml/grafite/cicNotation.mli | 3 - helm/ocaml/grafite2/disambiguatePp.ml | 32 -------- helm/ocaml/grafite2/disambiguatePp.mli | 4 - helm/ocaml/grafite2/grafiteEngine.ml | 44 ++++------ helm/ocaml/grafite2/grafiteEngine.mli | 4 +- helm/ocaml/grafite2/grafiteMisc.ml | 48 ----------- helm/ocaml/grafite2/grafiteMisc.mli | 9 --- helm/ocaml/grafite_parser/.depend | 6 ++ helm/ocaml/grafite_parser/Makefile | 32 ++++++++ helm/ocaml/grafite_parser/cicNotation2.ml | 69 ++++++++++++++++ helm/ocaml/grafite_parser/cicNotation2.mli | 31 +++++++ .../grafiteParser.ml | 0 .../grafiteParser.mli | 0 .../ocaml/grafite_parser/grafiteParserMisc.ml | 80 +++++++++++++++++++ .../grafite_parser/grafiteParserMisc.mli | 32 ++++++++ .../print_grammar.ml | 0 .../{grafite => grafite_parser}/test_dep.ml | 0 .../test_parser.ml | 2 +- 22 files changed, 274 insertions(+), 189 deletions(-) create mode 100644 helm/ocaml/grafite_parser/cicNotation2.ml create mode 100644 helm/ocaml/grafite_parser/cicNotation2.mli rename helm/ocaml/{grafite => grafite_parser}/grafiteParser.ml (100%) rename helm/ocaml/{grafite => grafite_parser}/grafiteParser.mli (100%) create mode 100644 helm/ocaml/grafite_parser/grafiteParserMisc.ml create mode 100644 helm/ocaml/grafite_parser/grafiteParserMisc.mli rename helm/ocaml/{grafite => grafite_parser}/print_grammar.ml (100%) rename helm/ocaml/{grafite => grafite_parser}/test_dep.ml (100%) rename helm/ocaml/{grafite => grafite_parser}/test_parser.ml (98%) diff --git a/helm/ocaml/METAS/meta.helm-grafite_parser.src b/helm/ocaml/METAS/meta.helm-grafite_parser.src index 389007b5b..cba4c171b 100644 --- a/helm/ocaml/METAS/meta.helm-grafite_parser.src +++ b/helm/ocaml/METAS/meta.helm-grafite_parser.src @@ -1,4 +1,4 @@ -requires="helm-grafite2" +requires="helm-grafite2 ulex" version="0.0.1" archive(byte)="grafite_parser.cma" archive(native)="grafite_parser.cmxa" diff --git a/helm/ocaml/grafite/.depend b/helm/ocaml/grafite/.depend index c5774b069..a6c70afc7 100644 --- a/helm/ocaml/grafite/.depend +++ b/helm/ocaml/grafite/.depend @@ -1,12 +1,9 @@ grafiteAstPp.cmi: grafiteAst.cmo -grafiteParser.cmi: grafiteAst.cmo cicNotation.cmi: grafiteAst.cmo grafiteMarshal.cmi: grafiteAst.cmo grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi -grafiteParser.cmo: grafiteAst.cmo grafiteParser.cmi -grafiteParser.cmx: grafiteAst.cmx grafiteParser.cmi -cicNotation.cmo: grafiteParser.cmi grafiteAst.cmo cicNotation.cmi -cicNotation.cmx: grafiteParser.cmx grafiteAst.cmx cicNotation.cmi -grafiteMarshal.cmo: grafiteAst.cmo grafiteMarshal.cmi -grafiteMarshal.cmx: grafiteAst.cmx grafiteMarshal.cmi +cicNotation.cmo: grafiteAst.cmo cicNotation.cmi +cicNotation.cmx: grafiteAst.cmx cicNotation.cmi +grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi +grafiteMarshal.cmx: grafiteAstPp.cmx grafiteAst.cmx grafiteMarshal.cmi diff --git a/helm/ocaml/grafite/Makefile b/helm/ocaml/grafite/Makefile index 0ce510b20..b16d7b7dd 100644 --- a/helm/ocaml/grafite/Makefile +++ b/helm/ocaml/grafite/Makefile @@ -3,7 +3,6 @@ PREDICATES = INTERFACE_FILES = \ grafiteAstPp.mli \ - grafiteParser.mli \ cicNotation.mli \ grafiteMarshal.mli \ $(NULL) @@ -11,47 +10,5 @@ IMPLEMENTATION_FILES = \ grafiteAst.ml \ $(INTERFACE_FILES:%.mli=%.ml) -all: test_parser print_grammar test_dep -clean: clean_tests - -# cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as -# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by -# "_loc" occurrences -MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" -grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -# -# -grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) -grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) - -clean_tests: - rm -f test_parser{,.opt} test_dep{,.opt} print_grammar{,.opt} - -LOCAL_LINKOPTS = -package helm-grafite -linkpkg -test: test_parser print_grammar test_dep -test_parser: test_parser.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -print_grammar: print_grammar.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -test_dep: test_dep.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< include ../Makefile.common - -# cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as -# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by -# "_loc" occurrences -UTF8DIR := $(shell $(OCAMLFIND) query helm-utf8_macros) -ULEXDIR := $(shell $(OCAMLFIND) query ulex) -MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" -cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationLexer.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -# - diff --git a/helm/ocaml/grafite/cicNotation.ml b/helm/ocaml/grafite/cicNotation.ml index 30dd5f4d1..9500a8e11 100644 --- a/helm/ocaml/grafite/cicNotation.ml +++ b/helm/ocaml/grafite/cicNotation.ml @@ -61,17 +61,6 @@ let remove_notation = function | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id | InterpretationId id -> TermAcicContent.remove_interpretation id -let load_notation fname = - let ic = open_in fname in - let lexbuf = Ulexing.from_utf8_channel ic in - try - while true do - match GrafiteParser.parse_statement lexbuf with - | Executable (_, Command (_, cmd)) -> ignore (process_notation cmd) - | _ -> () - done - with End_of_file -> close_in ic - let get_all_notations () = List.map (fun (interp_id, dsc) -> diff --git a/helm/ocaml/grafite/cicNotation.mli b/helm/ocaml/grafite/cicNotation.mli index 1c6e95385..41b775562 100644 --- a/helm/ocaml/grafite/cicNotation.mli +++ b/helm/ocaml/grafite/cicNotation.mli @@ -30,9 +30,6 @@ val process_notation: val remove_notation: notation_id -> unit -(** @param fname file from which load notation *) -val load_notation: string -> unit - (** {2 Notation enabling/disabling} * Right now, only disabling of notation during pretty printing is supporting. * If it is useful to disable it also for the input phase is still to be diff --git a/helm/ocaml/grafite2/disambiguatePp.ml b/helm/ocaml/grafite2/disambiguatePp.ml index c3a48e409..733179589 100644 --- a/helm/ocaml/grafite2/disambiguatePp.ml +++ b/helm/ocaml/grafite2/disambiguatePp.ml @@ -25,38 +25,6 @@ open DisambiguateTypes -let parse_environment str = - let stream = Ulexing.from_utf8_string str in - let environment = ref Environment.empty in - let multiple_environment = ref Environment.empty in - try - while true do - let alias = - match GrafiteParser.parse_statement stream with - GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias))) - -> alias - | _ -> assert false in - let key,value = - (*CSC: Warning: this code should be factorized with the corresponding - code in MatitaEngine *) - match alias with - GrafiteAst.Ident_alias (id,uri) -> - Id id, - (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) - | GrafiteAst.Symbol_alias (symb,instance,desc) -> - Symbol (symb,instance), - DisambiguateChoices.lookup_symbol_by_dsc symb desc - | GrafiteAst.Number_alias (instance,desc) -> - Num instance, - DisambiguateChoices.lookup_num_by_dsc desc - in - environment := Environment.add key value !environment; - multiple_environment := Environment.cons key value !multiple_environment; - done; - assert false - with End_of_file -> - !environment, !multiple_environment - let alias_of_domain_and_codomain_items domain_item (dsc,_) = match domain_item with Id id -> GrafiteAst.Ident_alias (id, dsc) diff --git a/helm/ocaml/grafite2/disambiguatePp.mli b/helm/ocaml/grafite2/disambiguatePp.mli index 69b6e8451..516dfee17 100644 --- a/helm/ocaml/grafite2/disambiguatePp.mli +++ b/helm/ocaml/grafite2/disambiguatePp.mli @@ -23,10 +23,6 @@ * http://helm.cs.unibo.it/ *) -val parse_environment: - string -> - DisambiguateTypes.environment * DisambiguateTypes.multiple_environment - val aliases_of_domain_and_codomain_items_list: (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> GrafiteAst.alias_spec list diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml index 70fb767a8..00470b9fc 100644 --- a/helm/ocaml/grafite2/grafiteEngine.ml +++ b/helm/ocaml/grafite2/grafiteEngine.ml @@ -24,13 +24,11 @@ *) exception Drop -exception UnableToInclude of string exception IncludedFileNotCompiled of string (* file name *) exception MetadataNotFound of string (* file name *) type options = { do_heavy_checks: bool ; - include_paths: string list ; clean_baseuri: bool } @@ -319,6 +317,7 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos type eval_ast = {ea_go: 'term 'lazy_term 'reduction 'obj 'ident. + baseuri_of_script:(string -> string) -> disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> @@ -332,7 +331,6 @@ type eval_ast = GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> ?do_heavy_checks:bool -> - ?include_paths:string list -> ?clean_baseuri:bool -> GrafiteTypes.status -> ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> @@ -341,6 +339,7 @@ type eval_ast = type 'a eval_command = {ec_go: 'term 'obj. + baseuri_of_script:(string -> string) -> disambiguate_command: (GrafiteTypes.status -> ('term,'obj) GrafiteAst.command -> @@ -351,6 +350,7 @@ type 'a eval_command = type 'a eval_executable = {ee_go: 'term 'lazy_term 'reduction 'obj 'ident. + baseuri_of_script:(string -> string) -> disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> @@ -446,23 +446,9 @@ let eval_tactical ~disambiguate_tactic status tac = in status -let make_absolute paths path = - let rec aux = function - | [] -> ignore (Unix.stat path); path - | p :: tl -> - let path = p ^ "/" ^ path in - try - ignore (Unix.stat path); path - with Unix.Unix_error _ -> aux tl - in - try - aux paths - with Unix.Unix_error _ -> raise (UnableToInclude path) -;; - let eval_comment status c = status -let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> +let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opts status cmd -> let status,cmd = disambiguate_command status cmd in let cmd,notation_ids' = CicNotation.process_notation cmd in let status = @@ -475,10 +461,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status | GrafiteAst.Include (loc, path) -> - let absolute_path = make_absolute opts.include_paths path in - let moopath = GrafiteMisc.obj_file_of_script ~basedir absolute_path in - let metadatapath = - GrafiteMisc.metadata_file_of_script ~basedir absolute_path in + let baseuri = baseuri_of_script path in + let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in + let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in if not (Sys.file_exists moopath) then raise (IncludedFileNotCompiled moopath); let status = @@ -634,7 +619,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> MatitaSync.add_obj uri obj {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} -} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex -> +} and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex -> match ex with | GrafiteAst.Tactical (_, tac, None) -> eval_tactical ~disambiguate_tactic status tac @@ -642,7 +627,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> let status = eval_tactical ~disambiguate_tactic status tac in eval_tactical ~disambiguate_tactic status punct | GrafiteAst.Command (_, cmd) -> - eval_command.ec_go ~disambiguate_command opts status cmd + eval_command.ec_go ~baseuri_of_script ~disambiguate_command + opts status cmd | GrafiteAst.Macro (_, mac) -> (*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO raise (Command_error @@ -662,21 +648,23 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> let ast = ast_of_cmd ast in status := eval_ast.ea_go + ~baseuri_of_script:(fun _ -> assert false) ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic) ~disambiguate_command:(fun status cmd -> status,cmd) !status ast) moo -} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command - ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st +} and eval_ast = {ea_go = fun ~baseuri_of_script ~disambiguate_tactic + ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status + st -> let opts = { do_heavy_checks = do_heavy_checks ; - include_paths = include_paths; clean_baseuri = clean_baseuri } in match st with | GrafiteAst.Executable (_,ex) -> - eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command opts status ex + eval_executable.ee_go ~baseuri_of_script ~disambiguate_tactic + ~disambiguate_command opts status ex | GrafiteAst.Comment (_,c) -> eval_comment status c } diff --git a/helm/ocaml/grafite2/grafiteEngine.mli b/helm/ocaml/grafite2/grafiteEngine.mli index efebbf048..e317060b5 100644 --- a/helm/ocaml/grafite2/grafiteEngine.mli +++ b/helm/ocaml/grafite2/grafiteEngine.mli @@ -24,10 +24,11 @@ *) exception Drop -exception UnableToInclude of string exception IncludedFileNotCompiled of string val eval_ast : + baseuri_of_script:(string -> string) -> + disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> @@ -41,7 +42,6 @@ val eval_ast : GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> ?do_heavy_checks:bool -> - ?include_paths:string list -> ?clean_baseuri:bool -> GrafiteTypes.status -> ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> diff --git a/helm/ocaml/grafite2/grafiteMisc.ml b/helm/ocaml/grafite2/grafiteMisc.ml index 8739b7a07..227cd382b 100644 --- a/helm/ocaml/grafite2/grafiteMisc.ml +++ b/helm/ocaml/grafite2/grafiteMisc.ml @@ -29,51 +29,3 @@ let is_empty buri = Http_getter_types.Ls_section _ -> true | Http_getter_types.Ls_object _ -> false) (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/")) - -let baseuri_of_baseuri_decl st = - match st with - | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) -> - Some buri - | _ -> None - -let baseuri_of_file file = - let uri = ref None in - let ic = open_in file in - let istream = Ulexing.from_utf8_channel ic in - (try - while true do - try - let stm = GrafiteParser.parse_statement istream in - match baseuri_of_baseuri_decl stm with - | Some buri -> - let u = Http_getter_misc.strip_trailing_slash buri in - if String.length u < 5 || String.sub u 0 5 <> "cic:/" then - HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); - (try - ignore(Http_getter.resolve u) - with - | Http_getter_types.Unresolvable_URI _ -> - HLog.error (file ^ " sets an unresolvable baseuri: "^buri) - | Http_getter_types.Key_not_found _ -> ()); - uri := Some u; - raise End_of_file - | None -> () - with - CicNotationParser.Parse_error err -> - HLog.error ("Unable to parse: " ^ file); - HLog.error ("Parse error: " ^ err); - () - done - with End_of_file -> close_in ic); - match !uri with - | Some uri -> uri - | None -> failwith ("No baseuri defined in " ^ file) - -let obj_file_of_script ~basedir f = - let baseuri = baseuri_of_file f in - LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri - -let metadata_file_of_script ~basedir f = - let baseuri = baseuri_of_file f in - LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri - diff --git a/helm/ocaml/grafite2/grafiteMisc.mli b/helm/ocaml/grafite2/grafiteMisc.mli index 9f1486b0b..833bb6360 100644 --- a/helm/ocaml/grafite2/grafiteMisc.mli +++ b/helm/ocaml/grafite2/grafiteMisc.mli @@ -23,14 +23,5 @@ * http://helm.cs.unibo.it/ *) -val baseuri_of_baseuri_decl : - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> - string option - (** check whether no objects are defined below a given baseuri *) val is_empty: string -> bool - -val baseuri_of_file : string -> string - -val obj_file_of_script : basedir:string -> string -> string -val metadata_file_of_script : basedir:string -> string -> string diff --git a/helm/ocaml/grafite_parser/.depend b/helm/ocaml/grafite_parser/.depend index 8baa095bc..6d2222906 100644 --- a/helm/ocaml/grafite_parser/.depend +++ b/helm/ocaml/grafite_parser/.depend @@ -1,4 +1,10 @@ +grafiteParser.cmo: grafiteParser.cmi +grafiteParser.cmx: grafiteParser.cmi +cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi +cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi matitaDisambiguator.cmo: matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaDisambiguator.cmi grafiteDisambiguate.cmo: matitaDisambiguator.cmi grafiteDisambiguate.cmi grafiteDisambiguate.cmx: matitaDisambiguator.cmx grafiteDisambiguate.cmi +grafiteParserMisc.cmo: grafiteParserMisc.cmi +grafiteParserMisc.cmx: grafiteParserMisc.cmi diff --git a/helm/ocaml/grafite_parser/Makefile b/helm/ocaml/grafite_parser/Makefile index afb05493e..d569dd41d 100644 --- a/helm/ocaml/grafite_parser/Makefile +++ b/helm/ocaml/grafite_parser/Makefile @@ -2,9 +2,41 @@ PACKAGE = grafite_parser PREDICATES = INTERFACE_FILES = \ + grafiteParser.mli \ + cicNotation2.mli \ matitaDisambiguator.mli \ grafiteDisambiguate.mli \ + grafiteParserMisc.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +all: test_parser print_grammar test_dep +clean: clean_tests + +# cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as +# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by +# "_loc" occurrences +UTF8DIR = $(shell $(OCAMLFIND) query helm-utf8_macros) +ULEXDIR = $(shell $(OCAMLFIND) query ulex) +MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" +grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +# +# +grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) +grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) + +clean_tests: + rm -f test_parser{,.opt} test_dep{,.opt} print_grammar{,.opt} + +LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg +test: test_parser print_grammar test_dep +test_parser: test_parser.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +print_grammar: print_grammar.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +test_dep: test_dep.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< + include ../Makefile.common diff --git a/helm/ocaml/grafite_parser/cicNotation2.ml b/helm/ocaml/grafite_parser/cicNotation2.ml new file mode 100644 index 000000000..2ce3f012f --- /dev/null +++ b/helm/ocaml/grafite_parser/cicNotation2.ml @@ -0,0 +1,69 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let load_notation fname = + let ic = open_in fname in + let lexbuf = Ulexing.from_utf8_channel ic in + try + while true do + match GrafiteParser.parse_statement lexbuf with + | GrafiteAst.Executable (_, GrafiteAst.Command (_, cmd)) -> + ignore (CicNotation.process_notation cmd) + | _ -> () + done + with End_of_file -> close_in ic + +let parse_environment str = + let stream = Ulexing.from_utf8_string str in + let environment = ref DisambiguateTypes.Environment.empty in + let multiple_environment = ref DisambiguateTypes.Environment.empty in + try + while true do + let alias = + match GrafiteParser.parse_statement stream with + GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias))) + -> alias + | _ -> assert false in + let key,value = + (*CSC: Warning: this code should be factorized with the corresponding + code in MatitaEngine *) + match alias with + GrafiteAst.Ident_alias (id,uri) -> + DisambiguateTypes.Id id, + (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) + | GrafiteAst.Symbol_alias (symb,instance,desc) -> + DisambiguateTypes.Symbol (symb,instance), + DisambiguateChoices.lookup_symbol_by_dsc symb desc + | GrafiteAst.Number_alias (instance,desc) -> + DisambiguateTypes.Num instance, + DisambiguateChoices.lookup_num_by_dsc desc + in + environment := DisambiguateTypes.Environment.add key value !environment; + multiple_environment := DisambiguateTypes.Environment.cons key value !multiple_environment; + done; + assert false + with End_of_file -> + !environment, !multiple_environment + diff --git a/helm/ocaml/grafite_parser/cicNotation2.mli b/helm/ocaml/grafite_parser/cicNotation2.mli new file mode 100644 index 000000000..2d8c4b3c8 --- /dev/null +++ b/helm/ocaml/grafite_parser/cicNotation2.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val parse_environment: + string -> + DisambiguateTypes.environment * DisambiguateTypes.multiple_environment + +(** @param fname file from which load notation *) +val load_notation: string -> unit diff --git a/helm/ocaml/grafite/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml similarity index 100% rename from helm/ocaml/grafite/grafiteParser.ml rename to helm/ocaml/grafite_parser/grafiteParser.ml diff --git a/helm/ocaml/grafite/grafiteParser.mli b/helm/ocaml/grafite_parser/grafiteParser.mli similarity index 100% rename from helm/ocaml/grafite/grafiteParser.mli rename to helm/ocaml/grafite_parser/grafiteParser.mli diff --git a/helm/ocaml/grafite_parser/grafiteParserMisc.ml b/helm/ocaml/grafite_parser/grafiteParserMisc.ml new file mode 100644 index 000000000..1b77da7cb --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteParserMisc.ml @@ -0,0 +1,80 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception UnableToInclude of string + +let baseuri_of_baseuri_decl st = + match st with + | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) -> + Some buri + | _ -> None + +let make_absolute paths path = + let rec aux = function + | [] -> ignore (Unix.stat path); path + | p :: tl -> + let path = p ^ "/" ^ path in + try + ignore (Unix.stat path); path + with Unix.Unix_error _ -> aux tl + in + try + aux paths + with Unix.Unix_error _ -> raise (UnableToInclude path) +;; + +let baseuri_of_script ~include_paths file = + let file = make_absolute include_paths file in + let uri = ref None in + let ic = open_in file in + let istream = Ulexing.from_utf8_channel ic in + (try + while true do + try + let stm = GrafiteParser.parse_statement istream in + match baseuri_of_baseuri_decl stm with + | Some buri -> + let u = Http_getter_misc.strip_trailing_slash buri in + if String.length u < 5 || String.sub u 0 5 <> "cic:/" then + HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); + (try + ignore(Http_getter.resolve u) + with + | Http_getter_types.Unresolvable_URI _ -> + HLog.error (file ^ " sets an unresolvable baseuri: "^buri) + | Http_getter_types.Key_not_found _ -> ()); + uri := Some u; + raise End_of_file + | None -> () + with + CicNotationParser.Parse_error err -> + HLog.error ("Unable to parse: " ^ file); + HLog.error ("Parse error: " ^ err); + () + done + with End_of_file -> close_in ic); + match !uri with + | Some uri -> uri + | None -> failwith ("No baseuri defined in " ^ file) diff --git a/helm/ocaml/grafite_parser/grafiteParserMisc.mli b/helm/ocaml/grafite_parser/grafiteParserMisc.mli new file mode 100644 index 000000000..74f60ec04 --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteParserMisc.mli @@ -0,0 +1,32 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception UnableToInclude of string + +val baseuri_of_baseuri_decl : + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + string option + +val baseuri_of_script : include_paths:string list -> string -> string diff --git a/helm/ocaml/grafite/print_grammar.ml b/helm/ocaml/grafite_parser/print_grammar.ml similarity index 100% rename from helm/ocaml/grafite/print_grammar.ml rename to helm/ocaml/grafite_parser/print_grammar.ml diff --git a/helm/ocaml/grafite/test_dep.ml b/helm/ocaml/grafite_parser/test_dep.ml similarity index 100% rename from helm/ocaml/grafite/test_dep.ml rename to helm/ocaml/grafite_parser/test_dep.ml diff --git a/helm/ocaml/grafite/test_parser.ml b/helm/ocaml/grafite_parser/test_parser.ml similarity index 98% rename from helm/ocaml/grafite/test_parser.ml rename to helm/ocaml/grafite_parser/test_parser.ml index d5edf50c9..76463f814 100644 --- a/helm/ocaml/grafite/test_parser.ml +++ b/helm/ocaml/grafite_parser/test_parser.ml @@ -154,7 +154,7 @@ let _ = let usage = "" in Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; print_endline "Loading builtin notation ..."; - CicNotation.load_notation (Helm_registry.get "notation.core_file"); + CicNotation2.load_notation (Helm_registry.get "notation.core_file"); print_endline "done."; flush stdout; process_stream (Ulexing.from_utf8_channel stdin) -- 2.39.2