From 827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 21 Dec 2005 13:49:21 +0000 Subject: [PATCH] Huge reorganization of matita and ocaml. Modified Files in matita: .depend configure.ac matita.ml matitaEngine.ml matitaEngine.mli matitaExcPp.ml matitaGui.ml matitaGui.mli matitaInit.ml matitaInit.mli matitaMathView.ml matitaScript.ml matitaScript.mli matitacLib.ml matitaclean.ml matitadep.ml Modified Files in ocaml: .cvsignore Makefile.in clusters.dot daemons.dot patch_deps.sh METAS/meta.helm-grafite.src METAS/meta.helm-grafite_parser.src cic/cic.ml cic_disambiguation/disambiguate.ml cic_disambiguation/disambiguateTypes.ml cic_disambiguation/disambiguateTypes.mli extlib/hExtlib.ml extlib/hExtlib.mli grafite/.depend grafite/Makefile grafite/grafiteAst.ml grafite/grafiteAstPp.ml grafite/grafiteAstPp.mli grafite/grafiteMarshal.ml grafite2/.depend grafite2/Makefile grafite_parser/.depend grafite_parser/Makefile grafite_parser/cicNotation2.ml grafite_parser/cicNotation2.mli grafite_parser/grafiteDisambiguate.ml grafite_parser/grafiteDisambiguate.mli grafite_parser/grafiteParser.ml grafite_parser/grafiteParser.mli grafite_parser/test_dep.ml grafite_parser/test_parser.ml library/libraryClean.ml library/libraryMisc.ml library/libraryMisc.mli library/libraryNoDb.ml library/libraryNoDb.mli library/librarySync.ml tactics/.depend tactics/equalityTactics.mli tactics/proofEngineHelpers.ml tactics/proofEngineTypes.ml tactics/proofEngineTypes.mli tactics/reductionTactics.mli tactics/tactics.mli Added Files in ocaml: METAS/meta.helm-grafite_engine.src METAS/meta.helm-lexicon.src grafite_engine/.cvsignore grafite_engine/.depend grafite_engine/Makefile grafite_engine/grafiteEngine.ml grafite_engine/grafiteEngine.mli grafite_engine/grafiteMisc.ml grafite_engine/grafiteMisc.mli grafite_engine/grafiteSync.ml grafite_engine/grafiteSync.mli grafite_engine/grafiteTypes.ml grafite_engine/grafiteTypes.mli grafite_parser/dependenciesParser.ml grafite_parser/dependenciesParser.mli grafite_parser/grafiteDisambiguator.ml grafite_parser/grafiteDisambiguator.mli lexicon/.cvsignore lexicon/.depend lexicon/Makefile lexicon/cicNotation.ml lexicon/cicNotation.mli lexicon/disambiguatePp.ml lexicon/disambiguatePp.mli lexicon/lexiconAst.ml lexicon/lexiconAstPp.ml lexicon/lexiconAstPp.mli lexicon/lexiconEngine.ml lexicon/lexiconEngine.mli lexicon/lexiconMarshal.ml lexicon/lexiconMarshal.mli lexicon/lexiconSync.ml lexicon/lexiconSync.mli Removed Files in ocaml: METAS/meta.helm-grafite2.src grafite/cicNotation.ml grafite/cicNotation.mli grafite2/disambiguatePp.ml grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml grafite2/grafiteMisc.mli grafite2/grafiteTypes.ml grafite2/grafiteTypes.mli grafite2/matitaSync.ml grafite2/matitaSync.mli grafite_parser/grafiteParserMisc.ml grafite_parser/grafiteParserMisc.mli grafite_parser/matitaDisambiguator.ml grafite_parser/matitaDisambiguator.mli --- helm/ocaml/.cvsignore | 4 + helm/ocaml/METAS/meta.helm-grafite.src | 2 +- helm/ocaml/METAS/meta.helm-grafite2.src | 5 - helm/ocaml/METAS/meta.helm-grafite_engine.src | 5 + helm/ocaml/METAS/meta.helm-grafite_parser.src | 2 +- helm/ocaml/METAS/meta.helm-lexicon.src | 4 + helm/ocaml/Makefile.in | 9 +- helm/ocaml/cic/cic.ml | 4 + helm/ocaml/cic_disambiguation/disambiguate.ml | 4 +- .../cic_disambiguation/disambiguateTypes.ml | 11 - .../cic_disambiguation/disambiguateTypes.mli | 3 - helm/ocaml/clusters.dot | 11 +- helm/ocaml/daemons.dot | 3 +- helm/ocaml/extlib/hExtlib.ml | 10 + helm/ocaml/extlib/hExtlib.mli | 3 + helm/ocaml/grafite/.depend | 3 - helm/ocaml/grafite/Makefile | 1 - helm/ocaml/grafite/grafiteAst.ml | 34 +-- helm/ocaml/grafite/grafiteAstPp.ml | 46 --- helm/ocaml/grafite/grafiteAstPp.mli | 3 - helm/ocaml/grafite/grafiteMarshal.ml | 14 - helm/ocaml/grafite2/.depend | 14 +- helm/ocaml/grafite2/Makefile | 3 +- helm/ocaml/grafite_engine/.cvsignore | 5 + helm/ocaml/grafite_engine/.depend | 12 + helm/ocaml/grafite_engine/Makefile | 12 + .../grafiteEngine.ml | 220 ++++++-------- .../grafiteEngine.mli | 9 +- .../grafiteMisc.ml | 0 .../grafiteMisc.mli | 0 helm/ocaml/grafite_engine/grafiteSync.ml | 72 +++++ helm/ocaml/grafite_engine/grafiteSync.mli | 38 +++ .../grafiteTypes.ml | 35 +-- .../grafiteTypes.mli | 5 - helm/ocaml/grafite_parser/.depend | 16 +- helm/ocaml/grafite_parser/Makefile | 4 +- helm/ocaml/grafite_parser/cicNotation2.ml | 58 ++-- helm/ocaml/grafite_parser/cicNotation2.mli | 10 +- .../grafite_parser/dependenciesParser.ml | 90 ++++++ .../grafite_parser/dependenciesParser.mli | 39 +++ .../grafite_parser/grafiteDisambiguate.ml | 287 +++++++++--------- .../grafite_parser/grafiteDisambiguate.mli | 18 +- ...sambiguator.ml => grafiteDisambiguator.ml} | 0 ...mbiguator.mli => grafiteDisambiguator.mli} | 0 helm/ocaml/grafite_parser/grafiteParser.ml | 84 ++--- helm/ocaml/grafite_parser/grafiteParser.mli | 16 +- .../ocaml/grafite_parser/grafiteParserMisc.ml | 80 ----- helm/ocaml/grafite_parser/test_dep.ml | 4 +- helm/ocaml/grafite_parser/test_parser.ml | 106 +++---- helm/ocaml/lexicon/.cvsignore | 7 + helm/ocaml/lexicon/.depend | 20 ++ helm/ocaml/lexicon/Makefile | 17 ++ .../ocaml/{grafite => lexicon}/cicNotation.ml | 8 +- .../{grafite => lexicon}/cicNotation.mli | 3 +- .../{grafite2 => lexicon}/disambiguatePp.ml | 8 +- .../{grafite2 => lexicon}/disambiguatePp.mli | 2 +- helm/ocaml/lexicon/lexiconAst.ml | 53 ++++ helm/ocaml/lexicon/lexiconAstPp.ml | 82 +++++ .../lexiconAstPp.mli} | 9 +- helm/ocaml/lexicon/lexiconEngine.ml | 149 +++++++++ helm/ocaml/lexicon/lexiconEngine.mli | 40 +++ helm/ocaml/lexicon/lexiconMarshal.ml | 96 ++++++ helm/ocaml/lexicon/lexiconMarshal.mli | 37 +++ .../matitaSync.ml => lexicon/lexiconSync.ml} | 103 +------ .../lexiconSync.mli} | 24 +- helm/ocaml/library/libraryClean.ml | 26 +- helm/ocaml/library/libraryMisc.ml | 4 + helm/ocaml/library/libraryMisc.mli | 2 +- helm/ocaml/library/libraryNoDb.ml | 20 +- helm/ocaml/library/libraryNoDb.mli | 1 - helm/ocaml/library/librarySync.ml | 2 +- helm/ocaml/patch_deps.sh | 5 +- helm/ocaml/tactics/.depend | 1 + helm/ocaml/tactics/equalityTactics.mli | 2 +- helm/ocaml/tactics/proofEngineHelpers.ml | 2 +- helm/ocaml/tactics/proofEngineTypes.ml | 6 +- helm/ocaml/tactics/proofEngineTypes.mli | 8 +- helm/ocaml/tactics/reductionTactics.mli | 6 +- helm/ocaml/tactics/tactics.mli | 8 +- 79 files changed, 1292 insertions(+), 877 deletions(-) delete mode 100644 helm/ocaml/METAS/meta.helm-grafite2.src create mode 100644 helm/ocaml/METAS/meta.helm-grafite_engine.src create mode 100644 helm/ocaml/METAS/meta.helm-lexicon.src create mode 100644 helm/ocaml/grafite_engine/.cvsignore create mode 100644 helm/ocaml/grafite_engine/.depend create mode 100644 helm/ocaml/grafite_engine/Makefile rename helm/ocaml/{grafite2 => grafite_engine}/grafiteEngine.ml (80%) rename helm/ocaml/{grafite2 => grafite_engine}/grafiteEngine.mli (87%) rename helm/ocaml/{grafite2 => grafite_engine}/grafiteMisc.ml (100%) rename helm/ocaml/{grafite2 => grafite_engine}/grafiteMisc.mli (100%) create mode 100644 helm/ocaml/grafite_engine/grafiteSync.ml create mode 100644 helm/ocaml/grafite_engine/grafiteSync.mli rename helm/ocaml/{grafite2 => grafite_engine}/grafiteTypes.ml (84%) rename helm/ocaml/{grafite2 => grafite_engine}/grafiteTypes.mli (88%) create mode 100644 helm/ocaml/grafite_parser/dependenciesParser.ml create mode 100644 helm/ocaml/grafite_parser/dependenciesParser.mli rename helm/ocaml/grafite_parser/{matitaDisambiguator.ml => grafiteDisambiguator.ml} (100%) rename helm/ocaml/grafite_parser/{matitaDisambiguator.mli => grafiteDisambiguator.mli} (100%) delete mode 100644 helm/ocaml/grafite_parser/grafiteParserMisc.ml create mode 100644 helm/ocaml/lexicon/.cvsignore create mode 100644 helm/ocaml/lexicon/.depend create mode 100644 helm/ocaml/lexicon/Makefile rename helm/ocaml/{grafite => lexicon}/cicNotation.ml (96%) rename helm/ocaml/{grafite => lexicon}/cicNotation.mli (93%) rename helm/ocaml/{grafite2 => lexicon}/disambiguatePp.ml (88%) rename helm/ocaml/{grafite2 => lexicon}/disambiguatePp.mli (97%) create mode 100644 helm/ocaml/lexicon/lexiconAst.ml create mode 100644 helm/ocaml/lexicon/lexiconAstPp.ml rename helm/ocaml/{grafite_parser/grafiteParserMisc.mli => lexicon/lexiconAstPp.mli} (78%) create mode 100644 helm/ocaml/lexicon/lexiconEngine.ml create mode 100644 helm/ocaml/lexicon/lexiconEngine.mli create mode 100644 helm/ocaml/lexicon/lexiconMarshal.ml create mode 100644 helm/ocaml/lexicon/lexiconMarshal.mli rename helm/ocaml/{grafite2/matitaSync.ml => lexicon/lexiconSync.ml} (53%) rename helm/ocaml/{grafite2/matitaSync.mli => lexicon/lexiconSync.mli} (68%) diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore index 4c1a00d01..391243bb0 100644 --- a/helm/ocaml/.cvsignore +++ b/helm/ocaml/.cvsignore @@ -9,3 +9,7 @@ libraries.ps libraries-complete.ps .dep.dot .alldep.dot +.clustersdep.dot +.extdep.dot +libraries-clusters.ps +libraries-ext.ps diff --git a/helm/ocaml/METAS/meta.helm-grafite.src b/helm/ocaml/METAS/meta.helm-grafite.src index 847d6e333..0ae4a09d3 100644 --- a/helm/ocaml/METAS/meta.helm-grafite.src +++ b/helm/ocaml/METAS/meta.helm-grafite.src @@ -1,4 +1,4 @@ -requires="helm-content_pres" +requires="helm-cic" version="0.0.1" archive(byte)="grafite.cma" archive(native)="grafite.cmxa" diff --git a/helm/ocaml/METAS/meta.helm-grafite2.src b/helm/ocaml/METAS/meta.helm-grafite2.src deleted file mode 100644 index 058167e4a..000000000 --- a/helm/ocaml/METAS/meta.helm-grafite2.src +++ /dev/null @@ -1,5 +0,0 @@ -requires="helm-library helm-grafite helm-tactics helm-cic_disambiguation" -version="0.0.1" -archive(byte)="grafite2.cma" -archive(native)="grafite2.cmxa" -linkopts="" diff --git a/helm/ocaml/METAS/meta.helm-grafite_engine.src b/helm/ocaml/METAS/meta.helm-grafite_engine.src new file mode 100644 index 000000000..c7203724c --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-grafite_engine.src @@ -0,0 +1,5 @@ +requires="helm-library helm-grafite helm-tactics" +version="0.0.1" +archive(byte)="grafite_engine.cma" +archive(native)="grafite_engine.cmxa" +linkopts="" diff --git a/helm/ocaml/METAS/meta.helm-grafite_parser.src b/helm/ocaml/METAS/meta.helm-grafite_parser.src index cba4c171b..d921b5588 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 ulex" +requires="helm-lexicon helm-grafite ulex" version="0.0.1" archive(byte)="grafite_parser.cma" archive(native)="grafite_parser.cmxa" diff --git a/helm/ocaml/METAS/meta.helm-lexicon.src b/helm/ocaml/METAS/meta.helm-lexicon.src new file mode 100644 index 000000000..35ab5dd36 --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-lexicon.src @@ -0,0 +1,4 @@ +requires="helm-content_pres helm-cic_disambiguation camlp4.gramlib" +version="0.0.1" +archive(byte)="lexicon.cma" +archive(native)="lexicon.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 3dabc3ad4..0c2d49411 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -25,7 +25,8 @@ MODULES = \ tactics \ paramodulation \ cic_disambiguation \ - grafite2 \ + lexicon \ + grafite_engine \ grafite_parser \ $(NULL) @@ -89,14 +90,20 @@ METAS/META.helm-%: METAS/meta.helm-%.src .extdep.dot: .dep.dot ./patch_deps.sh $< $@ +.clustersdep.dot: .dep.dot + USE_CLUSTERS=yes ./patch_deps.sh $< $@ libraries.ps: .dep.dot dot -Tps -o $@ $< libraries-ext.ps: .extdep.dot dot -Tps -o $@ $< +libraries-clusters.ps: .clustersdep.dot + dot -Tps -o $@ $< libraries-complete.ps: .alldep.dot dot -Tps -o $@ $< +ps: libraries.ps libraries-ext.ps libraries-clusters.ps + tags: TAGS .PHONY: TAGS TAGS: diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 4b4e0fed9..6e200cc31 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -216,6 +216,10 @@ and annhypothesis = and anncontext = annhypothesis list ;; +type lazy_term = + context -> metasenv -> CicUniv.universe_graph -> + term * metasenv * CicUniv.universe_graph + type anntarget = Object of annobj (* if annobj is a Constant, this is its type *) | ConstantBody of annobj diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 2ab3b3706..689460973 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -409,7 +409,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast | None -> Cic.Implicit annotation | Some term -> aux ~localize loc context term in - aux ~localize:true dummy_floc context ast + aux ~localize:true HExtlib.dummy_floc context ast let interpretate_path ~context path = let localization_tbl = Cic.CicHash.create 23 in @@ -536,7 +536,7 @@ let rev_uniq = (* "aux" keeps domain in reverse order and doesn't care about duplicates. * Domain item more in deep in the list will be processed first. *) -let rec domain_rev_of_term ?(loc = dummy_floc) context = function +let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> domain_rev_of_term ~loc context term | CicNotationPt.AttributedTerm (_, term) -> diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index c22f08ed7..fda6779e2 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -115,14 +115,3 @@ let string_of_domain_item = function let string_of_domain dom = String.concat "; " (List.map string_of_domain_item dom) - -let floc_of_loc (loc_begin, loc_end) = - let floc_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = loc_begin } - in - let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in - (floc_begin, floc_end) - -let dummy_floc = floc_of_loc (-1, -1) - diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index 48ae7880d..4f4b3c3ec 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -94,6 +94,3 @@ type script_entry = | Comment of CicNotationPt.location * string type script = CicNotationPt.location * script_entry list *) - -val dummy_floc: Lexing.position * Lexing.position - diff --git a/helm/ocaml/clusters.dot b/helm/ocaml/clusters.dot index 7872df240..3d22c6479 100644 --- a/helm/ocaml/clusters.dot +++ b/helm/ocaml/clusters.dot @@ -10,10 +10,10 @@ style = "filled"; color = "white" acic_content; - cic_acic; cic_disambiguation; content_pres; - grafite; + grafite_parser; + lexicon; } subgraph cluster_partially { label = "Partially specified terms"; @@ -24,6 +24,8 @@ cic_unification; tactics; paramodulation; + grafite; + grafite_engine; } subgraph cluster_fully { label = "Fully specified terms"; @@ -37,6 +39,8 @@ metadata; urimanager; whelp; + library; + cic_acic; } subgraph cluster_utilities { label = "Utilities"; @@ -48,6 +52,7 @@ hgdome; hmysql; registry; -// utf8_macros; + utf8_macros; xml; + logger; } diff --git a/helm/ocaml/daemons.dot b/helm/ocaml/daemons.dot index 5b7d0c330..93c122d8a 100644 --- a/helm/ocaml/daemons.dot +++ b/helm/ocaml/daemons.dot @@ -16,5 +16,4 @@ Matita -> hgdome; ProofChecker -> cic_proof_checking; Uwobo -> content_pres; - Whelp -> cic_disambiguation; - Whelp -> content_pres; + Whelp -> grafite_parser; diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index 99e6609ec..979b0c519 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -321,6 +321,16 @@ let loc_of_floc = function | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> (loc_begin, loc_end) +let floc_of_loc (loc_begin, loc_end) = + let floc_begin = + { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; + Lexing.pos_cnum = loc_begin } + in + let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in + (floc_begin, floc_end) + +let dummy_floc = floc_of_loc (-1, -1) + let raise_localized_exception ~offset floc exn = let (x, y) = loc_of_floc floc in let x = offset + x in diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli index c0538bfab..aed9b2406 100644 --- a/helm/ocaml/extlib/hExtlib.mli +++ b/helm/ocaml/extlib/hExtlib.mli @@ -88,5 +88,8 @@ val set_profiling_printings : (unit -> bool) -> unit exception Localized of Token.flocation * exn val loc_of_floc: Token.flocation -> int * int +val floc_of_loc: int * int -> Token.flocation + +val dummy_floc: Lexing.position * Lexing.position val raise_localized_exception: offset:int -> Token.flocation -> exn -> 'a diff --git a/helm/ocaml/grafite/.depend b/helm/ocaml/grafite/.depend index a6c70afc7..dc225e221 100644 --- a/helm/ocaml/grafite/.depend +++ b/helm/ocaml/grafite/.depend @@ -1,9 +1,6 @@ grafiteAstPp.cmi: grafiteAst.cmo -cicNotation.cmi: grafiteAst.cmo grafiteMarshal.cmi: grafiteAst.cmo grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.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 b16d7b7dd..182cd4561 100644 --- a/helm/ocaml/grafite/Makefile +++ b/helm/ocaml/grafite/Makefile @@ -3,7 +3,6 @@ PREDICATES = INTERFACE_FILES = \ grafiteAstPp.mli \ - cicNotation.mli \ grafiteMarshal.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml index 810e54140..12063745f 100644 --- a/helm/ocaml/grafite/grafiteAst.ml +++ b/helm/ocaml/grafite/grafiteAst.ml @@ -25,7 +25,7 @@ type direction = [ `LeftToRight | `RightToLeft ] -type loc = CicNotationPt.location +type loc = Token.flocation type ('term, 'lazy_term, 'ident) pattern = 'lazy_term option * ('ident * 'term) list * 'term option @@ -108,11 +108,6 @@ type 'term macro = | Search_pat of loc * search_kind * string (* searches with string pattern *) | Search_term of loc * search_kind * 'term (* searches with term pattern *) -type alias_spec = - | Ident_alias of string * string (* identifier, uri *) - | Symbol_alias of string * int * string (* name, instance no, description *) - | Number_alias of int * string (* instance no, description *) - (** To be increased each time the command type below changes, used for "safe" * marshalling *) let magic = 5 @@ -123,28 +118,8 @@ type 'obj command = | Set of loc * string * string | Drop of loc | Qed of loc - (** name. - * Name is needed when theorem was started without providing a name - *) | Coercion of loc * UriManager.uri * bool (* add composites *) - | Alias of loc * alias_spec - (** parameters, name, type, fields *) | Obj of loc * 'obj - | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc * - int * CicNotationPt.term - (* direction, l1 pattern, associativity, precedence, l2 pattern *) - | Interpretation of loc * - string * (string * CicNotationPt.argument_pattern list) * - CicNotationPt.cic_appl_pattern - (* description (i.e. id), symbol, arg pattern, appl pattern *) - - (* DEBUGGING *) - | Dump of loc (* dump grammar on stdout *) - (* DEBUGGING *) - | Render of loc * UriManager.uri (* render library object *) - -(* composed magic: term + command magics. No need to change this value *) -let magic = magic + 10000 * CicNotationPt.magic type ('term, 'lazy_term, 'reduction, 'ident) tactical = | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic @@ -188,10 +163,3 @@ type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment = type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement = | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment - - (* statements meaningful for matitadep *) -type dependency = - | IncludeDep of string - | BaseuriDep of string - | UriDep of UriManager.uri - diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml index 7be8c816e..6f927ee13 100644 --- a/helm/ocaml/grafite/grafiteAstPp.ml +++ b/helm/ocaml/grafite/grafiteAstPp.ml @@ -170,25 +170,6 @@ let pp_macro ~term_pp = function | Print (_, name) -> sprintf "Print \"%s\"" name | Quit _ -> "Quit" -let pp_alias = function - | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri - | Symbol_alias (symb, instance, desc) -> - sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" - symb instance desc - | Number_alias (instance,desc) -> - sprintf "alias num (instance %d) = \"%s\"" instance desc - -let pp_argument_pattern = function - | CicNotationPt.IdentArg (eta_depth, name) -> - let eta_buf = Buffer.create 5 in - for i = 1 to eta_depth do - Buffer.add_string eta_buf "\\eta." - done; - sprintf "%s%s" (Buffer.contents eta_buf) name - -let pp_l1_pattern = CicNotationPp.pp_term -let pp_l2_pattern = CicNotationPp.pp_term - let pp_associativity = function | Gramext.LeftA -> "left associative" | Gramext.RightA -> "right associative" @@ -201,24 +182,10 @@ let pp_dir_opt = function | Some `LeftToRight -> "> " | Some `RightToLeft -> "< " -let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = - sprintf "interpretation \"%s\" '%s %s = %s" - dsc symbol - (String.concat " " (List.map pp_argument_pattern arg_patterns)) - (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern) - let pp_default what uris = sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_notation dir_opt l1_pattern assoc prec l2_pattern = - sprintf "notation %s\"%s\" %s %s for %s" - (pp_dir_opt dir_opt) - (pp_l1_pattern l1_pattern) - (pp_associativity assoc) - (pp_precedence prec) - (pp_l2_pattern l2_pattern) - let pp_coercion uri do_composites = sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri) (if do_composites then "compounds" else "no compounds") @@ -229,16 +196,9 @@ let pp_command ~obj_pp = function | Drop _ -> "drop" | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites - | Alias (_,s) -> pp_alias s | Obj (_,obj) -> obj_pp obj | Default (_,what,uris) -> pp_default what uris - | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> - pp_interpretation dsc symbol arg_patterns cic_appl_pattern - | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> - pp_notation dir_opt l1_pattern assoc prec l2_pattern - | Render _ - | Dump _ -> assert false (* ZACK: debugging *) let rec pp_tactical ~term_pp ~lazy_term_pp = let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in @@ -289,9 +249,3 @@ let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = function | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex | Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c - -let pp_dependency = function - | IncludeDep str -> "include \"" ^ str ^ "\"" - | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\"" - | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\"" - diff --git a/helm/ocaml/grafite/grafiteAstPp.mli b/helm/ocaml/grafite/grafiteAstPp.mli index 80d2174f7..f9b3b37cc 100644 --- a/helm/ocaml/grafite/grafiteAstPp.mli +++ b/helm/ocaml/grafite/grafiteAstPp.mli @@ -43,9 +43,6 @@ val pp_reduction_kind: val pp_command: obj_pp:('obj -> string) -> 'obj GrafiteAst.command -> string val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string -val pp_alias: GrafiteAst.alias_spec -> string -val pp_dependency: GrafiteAst.dependency -> string - val pp_comment: term_pp:('term -> string) -> lazy_term_pp:('lazy_term -> string) -> diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml index bf02e91ac..0c4488091 100644 --- a/helm/ocaml/grafite/grafiteMarshal.ml +++ b/helm/ocaml/grafite/grafiteMarshal.ml @@ -38,22 +38,8 @@ let rehash_cmd_uris = | GrafiteAst.Default (loc, name, uris) -> let uris = List.map rehash_uri uris in GrafiteAst.Default (loc, name, uris) - | GrafiteAst.Interpretation (loc, dsc, args, cic_appl_pattern) -> - let rec aux = - function - | CicNotationPt.UriPattern uri -> - CicNotationPt.UriPattern (rehash_uri uri) - | CicNotationPt.ApplPattern args -> - CicNotationPt.ApplPattern (List.map aux args) - | CicNotationPt.VarPattern _ - | CicNotationPt.ImplicitPattern as pat -> pat - in - let appl_pattern = aux cic_appl_pattern in - GrafiteAst.Interpretation (loc, dsc, args, appl_pattern) | GrafiteAst.Coercion (loc, uri, close) -> GrafiteAst.Coercion (loc, rehash_uri uri, close) - | GrafiteAst.Notation _ - | GrafiteAst.Alias _ as cmd -> cmd | cmd -> prerr_endline "Found a command not expected in a .moo:"; let obj_pp _ = assert false in diff --git a/helm/ocaml/grafite2/.depend b/helm/ocaml/grafite2/.depend index 28de95ab3..eaea866c1 100644 --- a/helm/ocaml/grafite2/.depend +++ b/helm/ocaml/grafite2/.depend @@ -1,14 +1,10 @@ -matitaSync.cmi: grafiteTypes.cmi +grafiteSync.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi grafiteTypes.cmo: grafiteTypes.cmi grafiteTypes.cmx: grafiteTypes.cmi -disambiguatePp.cmo: disambiguatePp.cmi -disambiguatePp.cmx: disambiguatePp.cmi -matitaSync.cmo: grafiteTypes.cmi disambiguatePp.cmi matitaSync.cmi -matitaSync.cmx: grafiteTypes.cmx disambiguatePp.cmx matitaSync.cmi +grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi +grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi grafiteMisc.cmo: grafiteMisc.cmi grafiteMisc.cmx: grafiteMisc.cmi -grafiteEngine.cmo: matitaSync.cmi grafiteTypes.cmi grafiteMisc.cmi \ - grafiteEngine.cmi -grafiteEngine.cmx: matitaSync.cmx grafiteTypes.cmx grafiteMisc.cmx \ - grafiteEngine.cmi +grafiteEngine.cmo: grafiteTypes.cmi grafiteMisc.cmi grafiteEngine.cmi +grafiteEngine.cmx: grafiteTypes.cmx grafiteMisc.cmx grafiteEngine.cmi diff --git a/helm/ocaml/grafite2/Makefile b/helm/ocaml/grafite2/Makefile index 5a8d64fad..7fac4b296 100644 --- a/helm/ocaml/grafite2/Makefile +++ b/helm/ocaml/grafite2/Makefile @@ -3,8 +3,7 @@ PREDICATES = INTERFACE_FILES = \ grafiteTypes.mli \ - disambiguatePp.mli \ - matitaSync.mli \ + grafiteSync.mli \ grafiteMisc.mli \ grafiteEngine.mli \ $(NULL) diff --git a/helm/ocaml/grafite_engine/.cvsignore b/helm/ocaml/grafite_engine/.cvsignore new file mode 100644 index 000000000..8697eb7ee --- /dev/null +++ b/helm/ocaml/grafite_engine/.cvsignore @@ -0,0 +1,5 @@ +*.cm[iaox] +*.cmxa +test_dep +test_parser +print_grammar diff --git a/helm/ocaml/grafite_engine/.depend b/helm/ocaml/grafite_engine/.depend new file mode 100644 index 000000000..d0e9a3a86 --- /dev/null +++ b/helm/ocaml/grafite_engine/.depend @@ -0,0 +1,12 @@ +grafiteSync.cmi: grafiteTypes.cmi +grafiteEngine.cmi: grafiteTypes.cmi +grafiteTypes.cmo: grafiteTypes.cmi +grafiteTypes.cmx: grafiteTypes.cmi +grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi +grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi +grafiteMisc.cmo: grafiteMisc.cmi +grafiteMisc.cmx: grafiteMisc.cmi +grafiteEngine.cmo: grafiteTypes.cmi grafiteSync.cmi grafiteMisc.cmi \ + grafiteEngine.cmi +grafiteEngine.cmx: grafiteTypes.cmx grafiteSync.cmx grafiteMisc.cmx \ + grafiteEngine.cmi diff --git a/helm/ocaml/grafite_engine/Makefile b/helm/ocaml/grafite_engine/Makefile new file mode 100644 index 000000000..e72acd29c --- /dev/null +++ b/helm/ocaml/grafite_engine/Makefile @@ -0,0 +1,12 @@ +PACKAGE = grafite_engine +PREDICATES = + +INTERFACE_FILES = \ + grafiteTypes.mli \ + grafiteSync.mli \ + grafiteMisc.mli \ + grafiteEngine.mli \ + $(NULL) +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +include ../Makefile.common diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml similarity index 80% rename from helm/ocaml/grafite2/grafiteEngine.ml rename to helm/ocaml/grafite_engine/grafiteEngine.ml index 4a851e77b..c820986b3 100644 --- a/helm/ocaml/grafite2/grafiteEngine.ml +++ b/helm/ocaml/grafite_engine/grafiteEngine.ml @@ -25,7 +25,6 @@ exception Drop exception IncludedFileNotCompiled of string (* file name *) -exception MetadataNotFound of string (* file name *) type options = { do_heavy_checks: bool ; @@ -273,13 +272,13 @@ let apply_tactic ~disambiguate_tactic tactic (status, goal) = let starting_metasenv = GrafiteTypes.get_proof_metasenv status in let before = List.map (fun g, _, _ -> g) starting_metasenv in (* prerr_endline "disambiguate"; *) - let status_ref, tactic = disambiguate_tactic status goal tactic in - let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv !status_ref in - let proof = GrafiteTypes.get_current_proof !status_ref in + let status, tactic = disambiguate_tactic status goal tactic in + let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv status in + let proof = GrafiteTypes.get_current_proof status in let proof_status = proof, goal in let needs_reordering, always_opens_a_goal = classify_tactic tactic in let tactic = tactic_of_ast tactic in - (* apply tactic will change the status pointed by status_ref ... *) + (* apply tactic will change the lexicon_status ... *) (* prerr_endline "apply_tactic bassa"; *) let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in let after = ProofEngineTypes.goals_of_proof proof in @@ -307,11 +306,11 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos proof, opened_goals in let incomplete_proof = - match !status_ref.GrafiteTypes.proof_status with + match status.GrafiteTypes.proof_status with | GrafiteTypes.Incomplete_proof p -> p | _ -> assert false in - { !status_ref with GrafiteTypes.proof_status = + { status with GrafiteTypes.proof_status = GrafiteTypes.Incomplete_proof { incomplete_proof with GrafiteTypes.proof = proof } }, opened_goals, closed_goals @@ -319,13 +318,12 @@ 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 -> ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> - GrafiteTypes.status ref * - (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + GrafiteTypes.status * + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> disambiguate_command: (GrafiteTypes.status -> @@ -336,29 +334,27 @@ type eval_ast = ?clean_baseuri:bool -> GrafiteTypes.status -> ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> - GrafiteTypes.status + GrafiteTypes.status * UriManager.uri list } type 'a eval_command = {ec_go: 'term 'obj. - baseuri_of_script:(string -> string) -> disambiguate_command: (GrafiteTypes.status -> 'obj GrafiteAst.command -> GrafiteTypes.status * Cic.obj GrafiteAst.command) -> options -> GrafiteTypes.status -> 'obj GrafiteAst.command -> - GrafiteTypes.status + GrafiteTypes.status * UriManager.uri list } type 'a eval_executable = {ee_go: 'term 'lazy_term 'reduction 'obj 'ident. - baseuri_of_script:(string -> string) -> disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> - GrafiteTypes.status ref * - (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + GrafiteTypes.status * + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> disambiguate_command: (GrafiteTypes.status -> @@ -367,21 +363,24 @@ type 'a eval_executable = options -> GrafiteTypes.status -> - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code -> GrafiteTypes.status + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code -> + GrafiteTypes.status * UriManager.uri list } -type 'a eval_from_moo = { efm_go: GrafiteTypes.status ref -> string -> unit } +type 'a eval_from_moo = + { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } let coercion_moo_statement_of uri = - GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, uri, false) + GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false) let eval_coercion status ~add_composites uri = let basedir = Helm_registry.get "matita.basedir" in - let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in + let status,compounds = + GrafiteSync.add_coercion ~basedir ~add_composites status uri in let moo_content = coercion_moo_statement_of uri in let status = GrafiteTypes.add_moo_content [moo_content] status in - let status = MatitaSync.add_coercion status uri compounds in - {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + compounds let eval_tactical ~disambiguate_tactic status tac = let apply_tactic = apply_tactic ~disambiguate_tactic in @@ -394,7 +393,7 @@ let eval_tactical ~disambiguate_tactic status tac = type tactic = input_status -> output_status - let id_tactic = apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) + let id_tactic = apply_tactic (GrafiteAst.IdTac HExtlib.dummy_floc) let mk_tactic tac = tac let apply_tactic tac = tac let goals (_, opened, closed) = opened, closed @@ -462,7 +461,7 @@ let add_coercions_of_record_to_moo obj lemmas status = let attributes = CicUtil.attributes_of_obj obj in let is_record = function `Class (`Record att) -> Some att | _-> None in match HExtlib.list_findopt is_record attributes with - | None -> status + | None -> status,[] | Some fields -> let is_a_coercion uri = try @@ -506,70 +505,51 @@ let add_coercions_of_record_to_moo obj lemmas status = (fun u -> prerr_endline (UriManager.string_of_uri u)) coercions; let status = GrafiteTypes.add_moo_content moo_content status in + let basedir = Helm_registry.get "matita.basedir" in List.fold_left - (fun status uri -> - MatitaSync.add_coercion status uri []) - status coercions + (fun (status,lemmas) uri -> + let status,new_lemmas = + GrafiteSync.add_coercion ~basedir ~add_composites:true status uri + in + status,new_lemmas@lemmas + ) (status,[]) coercions let add_obj uri obj status = let basedir = Helm_registry.get "matita.basedir" in - let lemmas = LibrarySync.add_obj uri obj basedir in - let status = - {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects} in - let status = MatitaSync.add_obj uri obj lemmas status in + let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in status, lemmas -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 = - { status with - GrafiteTypes.notation_ids = - notation_ids' @ status.GrafiteTypes.notation_ids } in - let basedir = Helm_registry.get "matita.basedir" in +let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> + let status,cmd = disambiguate_command status cmd in + let basedir = Helm_registry.get "matita.basedir" in + let status,uris = match cmd with | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; - GrafiteTypes.add_moo_content [cmd] status - | GrafiteAst.Include (loc, path) -> - let baseuri = baseuri_of_script path in + GrafiteTypes.add_moo_content [cmd] status,[] + | GrafiteAst.Include (loc, baseuri) -> 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 = - if Helm_registry.get_bool "db.nodb" then - if not (Sys.file_exists metadatapath) then - raise (MetadataNotFound metadatapath) - else - GrafiteTypes.add_metadata - (LibraryNoDb.load_metadata ~fname:metadatapath) status - else - status - in - let status = ref status in - eval_from_moo.efm_go status moopath; - !status + let status = eval_from_moo.efm_go status moopath in + status,[] | GrafiteAst.Set (loc, name, value) -> - let status = - if name = "baseuri" then begin - let value = - let v = Http_getter_misc.strip_trailing_slash value in - try - ignore (String.index v ' '); - raise (GrafiteTypes.Command_error "baseuri can't contain spaces") - with Not_found -> v - in - if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin - HLog.warn ("baseuri " ^ value ^ " is not empty"); - HLog.message ("cleaning baseuri " ^ value); - LibraryClean.clean_baseuris ~basedir [value] - end; - GrafiteTypes.add_metadata [LibraryNoDb.Baseuri value] status - end else - status - in - GrafiteTypes.set_option status name value + if name = "baseuri" then begin + let value = + let v = Http_getter_misc.strip_trailing_slash value in + try + ignore (String.index v ' '); + raise (GrafiteTypes.Command_error "baseuri can't contain spaces") + with Not_found -> v + in + if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin + HLog.warn ("baseuri " ^ value ^ " is not empty"); + HLog.message ("cleaning baseuri " ^ value); + LibraryClean.clean_baseuris ~basedir [value]; + end; + end; + GrafiteTypes.set_option status name value,[] | GrafiteAst.Drop loc -> raise Drop | GrafiteAst.Qed loc -> let uri, metasenv, bo, ty = @@ -590,44 +570,11 @@ let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opt "Proof not completed! metasenv is not empty!"); let name = UriManager.name_of_uri uri in let obj = Cic.Constant (name,Some bo,ty,[],[]) in - let status, _lemmas = add_obj uri obj status in - (* should we assert lemmas = [] ? *) - {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} + let status, lemmas = add_obj uri obj status in + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + uri::lemmas | GrafiteAst.Coercion (loc, uri, add_composites) -> eval_coercion status ~add_composites uri - | GrafiteAst.Alias (loc, spec) -> - let diff = - (*CSC: Warning: this code should be factorized with the corresponding - code in DisambiguatePp *) - match spec 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 - MatitaSync.set_proof_aliases status diff - | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *) - | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *) - | GrafiteAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm -> - let status = GrafiteTypes.add_moo_content [stm] status in - let uris = - List.map - (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri)) - (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern) - in - let diff = - [DisambiguateTypes.Symbol (symbol, 0), - DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] - in - let status = MatitaSync.set_proof_aliases status diff in - let status = GrafiteTypes.add_metadata uris status in - status - | GrafiteAst.Notation _ as stm -> GrafiteTypes.add_moo_content [stm] status | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -682,26 +629,34 @@ let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opt let initial_stack = Continuationals.Stack.of_metasenv metasenv in { status with GrafiteTypes.proof_status = GrafiteTypes.Incomplete_proof - { GrafiteTypes.proof = initial_proof; stack = initial_stack } } + { GrafiteTypes.proof = initial_proof; stack = initial_stack } }, + [] | _ -> if metasenv <> [] then raise (GrafiteTypes.Command_error ( "metasenv not empty while giving a definition with body: " ^ CicMetaSubst.ppmetasenv [] metasenv)); let status, lemmas = add_obj uri obj status in - let status = add_coercions_of_record_to_moo obj lemmas status in - {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} + let status,new_lemmas = + add_coercions_of_record_to_moo obj lemmas status + in + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + uri::new_lemmas@lemmas + in + match status.GrafiteTypes.proof_status with + GrafiteTypes.Intermediate _ -> + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris + | _ -> status,uris -} and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex -> +} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex -> match ex with | GrafiteAst.Tactical (_, tac, None) -> - eval_tactical ~disambiguate_tactic status tac + eval_tactical ~disambiguate_tactic status tac,[] | GrafiteAst.Tactical (_, tac, Some punct) -> let status = eval_tactical ~disambiguate_tactic status tac in - eval_tactical ~disambiguate_tactic status punct + eval_tactical ~disambiguate_tactic status punct,[] | GrafiteAst.Command (_, cmd) -> - eval_command.ec_go ~baseuri_of_script ~disambiguate_command - opts status cmd + eval_command.ec_go ~disambiguate_command opts status cmd | GrafiteAst.Macro (_, mac) -> (*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO raise (Command_error @@ -711,23 +666,24 @@ let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opt } and eval_from_moo = {efm_go = fun status fname -> let ast_of_cmd cmd = - GrafiteAst.Executable (DisambiguateTypes.dummy_floc, - GrafiteAst.Command (DisambiguateTypes.dummy_floc, + GrafiteAst.Executable (HExtlib.dummy_floc, + GrafiteAst.Command (HExtlib.dummy_floc, cmd)) in let moo = GrafiteMarshal.load_moo fname in - List.iter - (fun ast -> + List.fold_left + (fun status ast -> 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) + let status,lemmas = + eval_ast.ea_go + ~disambiguate_tactic:(fun status _ tactic -> status,tactic) ~disambiguate_command:(fun status cmd -> status,cmd) - !status ast) - moo -} and eval_ast = {ea_go = fun ~baseuri_of_script ~disambiguate_tactic - ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status + status ast + in + assert (lemmas=[]); + status) + status moo +} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status st -> let opts = { @@ -736,9 +692,9 @@ let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opt in match st with | GrafiteAst.Executable (_,ex) -> - eval_executable.ee_go ~baseuri_of_script ~disambiguate_tactic + eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command opts status ex - | GrafiteAst.Comment (_,c) -> eval_comment status c + | GrafiteAst.Comment (_,c) -> eval_comment status c,[] } let eval_ast = eval_ast.ea_go diff --git a/helm/ocaml/grafite2/grafiteEngine.mli b/helm/ocaml/grafite_engine/grafiteEngine.mli similarity index 87% rename from helm/ocaml/grafite2/grafiteEngine.mli rename to helm/ocaml/grafite_engine/grafiteEngine.mli index ccdc306c2..4043e8072 100644 --- a/helm/ocaml/grafite2/grafiteEngine.mli +++ b/helm/ocaml/grafite_engine/grafiteEngine.mli @@ -27,14 +27,12 @@ exception Drop exception IncludedFileNotCompiled of string val eval_ast : - baseuri_of_script:(string -> string) -> - disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> - GrafiteTypes.status ref * - (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + GrafiteTypes.status * + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> disambiguate_command: (GrafiteTypes.status -> @@ -45,4 +43,5 @@ val eval_ast : ?clean_baseuri:bool -> GrafiteTypes.status -> ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> - GrafiteTypes.status + (* the new status and generated objects, if any *) + GrafiteTypes.status * UriManager.uri list diff --git a/helm/ocaml/grafite2/grafiteMisc.ml b/helm/ocaml/grafite_engine/grafiteMisc.ml similarity index 100% rename from helm/ocaml/grafite2/grafiteMisc.ml rename to helm/ocaml/grafite_engine/grafiteMisc.ml diff --git a/helm/ocaml/grafite2/grafiteMisc.mli b/helm/ocaml/grafite_engine/grafiteMisc.mli similarity index 100% rename from helm/ocaml/grafite2/grafiteMisc.mli rename to helm/ocaml/grafite_engine/grafiteMisc.mli diff --git a/helm/ocaml/grafite_engine/grafiteSync.ml b/helm/ocaml/grafite_engine/grafiteSync.ml new file mode 100644 index 000000000..853a827c0 --- /dev/null +++ b/helm/ocaml/grafite_engine/grafiteSync.ml @@ -0,0 +1,72 @@ +(* 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/ + *) + +open Printf + +let add_obj ~basedir uri obj status = + let lemmas = LibrarySync.add_obj uri obj basedir in + {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects}, + lemmas + +let add_coercion ~basedir ~add_composites status uri = + let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in + {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions}, + compounds + +module OrderedUri = +struct + type t = UriManager.uri * string + let compare (u1, _) (u2, _) = UriManager.compare u1 u2 +end + +module UriSet = Set.Make (OrderedUri) + + (** @return l2 \ l1 *) +let uri_list_diff l2 l1 = + let module S = UriManager.UriSet in + let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in + let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in + let diff = S.diff s2 s1 in + S.fold (fun uri uris -> uri :: uris) diff [] + +let time_travel ~present ~past = + let objs_to_remove = + uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in + let coercions_to_remove = + uri_list_diff present.GrafiteTypes.coercions past.GrafiteTypes.coercions + in + List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove; + List.iter LibrarySync.remove_obj objs_to_remove + +let init () = + LibrarySync.remove_all_coercions (); + LibraryObjects.reset_defaults (); + { + GrafiteTypes.moo_content_rev = []; + proof_status = GrafiteTypes.No_proof; + options = GrafiteTypes.no_options; + objects = []; + coercions = []; + } diff --git a/helm/ocaml/grafite_engine/grafiteSync.mli b/helm/ocaml/grafite_engine/grafiteSync.mli new file mode 100644 index 000000000..ce3c04250 --- /dev/null +++ b/helm/ocaml/grafite_engine/grafiteSync.mli @@ -0,0 +1,38 @@ +(* 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/ + *) + +val add_obj: + basedir:string -> UriManager.uri -> Cic.obj -> GrafiteTypes.status -> + GrafiteTypes.status * UriManager.uri list + +val add_coercion: + basedir:string -> add_composites:bool -> GrafiteTypes.status -> + UriManager.uri -> GrafiteTypes.status * UriManager.uri list + +val time_travel: + present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit + + (* also resets the imperative part of the status *) +val init: unit -> GrafiteTypes.status diff --git a/helm/ocaml/grafite2/grafiteTypes.ml b/helm/ocaml/grafite_engine/grafiteTypes.ml similarity index 84% rename from helm/ocaml/grafite2/grafiteTypes.ml rename to helm/ocaml/grafite_engine/grafiteTypes.ml index c73e8bd3c..a13cc074e 100644 --- a/helm/ocaml/grafite2/grafiteTypes.ml +++ b/helm/ocaml/grafite_engine/grafiteTypes.ml @@ -50,15 +50,11 @@ type options = option_value StringMap.t let no_options = StringMap.empty type status = { - aliases: DisambiguateTypes.environment; - multi_aliases: DisambiguateTypes.multiple_environment; moo_content_rev: GrafiteMarshal.moo; - metadata: LibraryNoDb.metadata list; proof_status: proof_status; options: options; objects: UriManager.uri list; coercions: UriManager.uri list; - notation_ids: CicNotation.notation_id list; } let get_current_proof status = @@ -97,7 +93,9 @@ let set_metasenv metasenv status = Incomplete_proof { incomplete_proof with proof = (uri, metasenv, proof, ty) } | Intermediate _ -> Intermediate metasenv - | Proof _ -> assert false + | Proof (_, metasenv', _, _) -> + assert (metasenv = metasenv'); + status.proof_status in { status with proof_status = proof_status } @@ -122,12 +120,9 @@ let add_moo_content cmds status = (fun cmd acc -> (* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *) match cmd with - | GrafiteAst.Interpretation _ | GrafiteAst.Default _ -> if List.mem cmd content then acc else cmd :: acc - | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *) - cmd :: (List.filter ((<>) cmd) acc) | _ -> cmd :: acc) cmds content in @@ -175,30 +170,6 @@ let get_string_option status name = let qualify status name = get_string_option status "baseuri" ^ "/" ^ name -let add_metadata new_metadata status = - if Helm_registry.get_bool "db.nodb" then - let metadata = status.metadata in - let metadata' = - List.fold_left - (fun acc m -> - match m with - | LibraryNoDb.Dependency buri -> - let is_self = (* self dependency *) - try - get_string_option status "baseuri" = buri - with Option_error _ -> false (* baseuri not yet set *) - in - if is_self (* duplicate *) - || List.exists (LibraryNoDb.eq_metadata m) metadata - then acc - else m :: acc - | _ -> m :: acc) - metadata new_metadata - in - { status with metadata = metadata' } - else - status - let dump_status status = HLog.message "status.aliases:\n"; HLog.message "status.proof_status:"; diff --git a/helm/ocaml/grafite2/grafiteTypes.mli b/helm/ocaml/grafite_engine/grafiteTypes.mli similarity index 88% rename from helm/ocaml/grafite2/grafiteTypes.mli rename to helm/ocaml/grafite_engine/grafiteTypes.mli index 361a00825..70089623b 100644 --- a/helm/ocaml/grafite2/grafiteTypes.mli +++ b/helm/ocaml/grafite_engine/grafiteTypes.mli @@ -45,22 +45,17 @@ type options val no_options: options type status = { - aliases: DisambiguateTypes.environment; (** disambiguation aliases *) - multi_aliases: DisambiguateTypes.multiple_environment; moo_content_rev: GrafiteMarshal.moo; - metadata: LibraryNoDb.metadata list; proof_status: proof_status; (** logical status *) options: options; objects: UriManager.uri list; (** in-scope objects *) coercions: UriManager.uri list; (** defined coercions *) - notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) } val dump_status : status -> unit (** list is not reversed, head command will be the first emitted *) val add_moo_content: GrafiteMarshal.ast_command list -> status -> status -val add_metadata: LibraryNoDb.metadata list -> status -> status val get_option : status -> string -> option_value val get_string_option : status -> string -> string diff --git a/helm/ocaml/grafite_parser/.depend b/helm/ocaml/grafite_parser/.depend index 0694143fc..360429635 100644 --- a/helm/ocaml/grafite_parser/.depend +++ b/helm/ocaml/grafite_parser/.depend @@ -1,10 +1,10 @@ -grafiteParser.cmo: grafiteParser.cmi -grafiteParser.cmx: grafiteParser.cmi +dependenciesParser.cmo: dependenciesParser.cmi +dependenciesParser.cmx: dependenciesParser.cmi +grafiteParser.cmo: dependenciesParser.cmi grafiteParser.cmi +grafiteParser.cmx: dependenciesParser.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: grafiteParser.cmi grafiteParserMisc.cmi -grafiteParserMisc.cmx: grafiteParser.cmx grafiteParserMisc.cmi +grafiteDisambiguator.cmo: grafiteDisambiguator.cmi +grafiteDisambiguator.cmx: grafiteDisambiguator.cmi +grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi diff --git a/helm/ocaml/grafite_parser/Makefile b/helm/ocaml/grafite_parser/Makefile index d569dd41d..4b04b597e 100644 --- a/helm/ocaml/grafite_parser/Makefile +++ b/helm/ocaml/grafite_parser/Makefile @@ -2,11 +2,11 @@ PACKAGE = grafite_parser PREDICATES = INTERFACE_FILES = \ + dependenciesParser.mli \ grafiteParser.mli \ cicNotation2.mli \ - matitaDisambiguator.mli \ + grafiteDisambiguator.mli \ grafiteDisambiguate.mli \ - grafiteParserMisc.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/grafite_parser/cicNotation2.ml b/helm/ocaml/grafite_parser/cicNotation2.ml index 2ce3f012f..f978f2971 100644 --- a/helm/ocaml/grafite_parser/cicNotation2.ml +++ b/helm/ocaml/grafite_parser/cicNotation2.ml @@ -23,47 +23,25 @@ * http://helm.cs.unibo.it/ *) -let load_notation fname = +let load_notation ~include_paths fname = let ic = open_in fname in let lexbuf = Ulexing.from_utf8_channel ic in + let status = ref LexiconSync.init 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 + while true do + status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status) + done; + assert false + with End_of_file -> close_in ic; !status +let parse_environment ~include_paths str = + let lexbuf = Ulexing.from_utf8_string str in + let status = ref LexiconSync.init in + try + while true do + status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status) + done; + assert false + with End_of_file -> + !status.LexiconEngine.aliases, + !status.LexiconEngine.multi_aliases diff --git a/helm/ocaml/grafite_parser/cicNotation2.mli b/helm/ocaml/grafite_parser/cicNotation2.mli index 2d8c4b3c8..00f184b3b 100644 --- a/helm/ocaml/grafite_parser/cicNotation2.mli +++ b/helm/ocaml/grafite_parser/cicNotation2.mli @@ -23,9 +23,13 @@ * http://helm.cs.unibo.it/ *) +(** Note: notation is also loaded, but it cannot be undone since the + notation_ids part of the status is thrown away; + so far this function is useful only in Whelp *) val parse_environment: - string -> - DisambiguateTypes.environment * DisambiguateTypes.multiple_environment + include_paths:string list -> + string -> + DisambiguateTypes.environment * DisambiguateTypes.multiple_environment (** @param fname file from which load notation *) -val load_notation: string -> unit +val load_notation: include_paths:string list -> string -> LexiconEngine.status diff --git a/helm/ocaml/grafite_parser/dependenciesParser.ml b/helm/ocaml/grafite_parser/dependenciesParser.ml new file mode 100644 index 000000000..74805cfa7 --- /dev/null +++ b/helm/ocaml/grafite_parser/dependenciesParser.ml @@ -0,0 +1,90 @@ +(* 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/ + *) + +exception UnableToInclude of string + + (* statements meaningful for matitadep *) +type dependency = + | IncludeDep of string + | BaseuriDep of string + | UriDep of UriManager.uri + +let pp_dependency = function + | IncludeDep str -> "include \"" ^ str ^ "\"" + | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\"" + | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\"" + +let parse_dependencies lexbuf = + let tok_stream,_ = + CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf) + in + let rec parse acc = + (parser + | [< '("URI", u) >] -> + parse (UriDep (UriManager.uri_of_string u) :: acc) + | [< '("IDENT", "include"); '("QSTRING", fname) >] -> + parse (IncludeDep fname :: acc) + | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] -> + parse (BaseuriDep baseuri :: acc) + | [< '("EOI", _) >] -> acc + | [< 'tok >] -> parse acc + | [< >] -> acc) tok_stream + in + List.rev (parse []) + +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 ic = open_in file in + let istream = Ulexing.from_utf8_channel ic in + let rec find_baseuri = + function + [] -> failwith ("No baseuri defined in " ^ file) + | BaseuriDep s::_ -> s + | _::tl -> find_baseuri tl in + let buri = find_baseuri (parse_dependencies istream) in + let uri = Http_getter_misc.strip_trailing_slash buri in + if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then + HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); + (try + ignore(Http_getter.resolve uri) + with + | Http_getter_types.Unresolvable_URI _ -> + HLog.error (file ^ " sets an unresolvable baseuri: " ^ buri) + | Http_getter_types.Key_not_found _ -> ()); + uri diff --git a/helm/ocaml/grafite_parser/dependenciesParser.mli b/helm/ocaml/grafite_parser/dependenciesParser.mli new file mode 100644 index 000000000..882d45fb8 --- /dev/null +++ b/helm/ocaml/grafite_parser/dependenciesParser.mli @@ -0,0 +1,39 @@ +(* 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/ + *) + +exception UnableToInclude of string + + (* statements meaningful for matitadep *) +type dependency = + | IncludeDep of string + | BaseuriDep of string + | UriDep of UriManager.uri + +val pp_dependency: dependency -> string + + (** @raise End_of_file *) +val parse_dependencies: Ulexing.lexbuf -> dependency list + +val baseuri_of_script : include_paths:string list -> string -> string diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml index e6cc064a5..da7294478 100644 --- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml @@ -23,51 +23,46 @@ * http://helm.cs.unibo.it/ *) -open GrafiteTypes +exception BaseUriNotSetYet let singleton = function | [x], _ -> x | _ -> assert false (** @param term not meaningful when context is given *) -let disambiguate_term ?context status_ref goal term = - let status = !status_ref in - let context = - match context with - | Some c -> c - | None -> GrafiteTypes.get_proof_context status goal - in +let disambiguate_term lexicon_status_ref context metasenv term = + let lexicon_status = !lexicon_status_ref in let (diff, metasenv, cic, _) = singleton - (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) - ~aliases:status.aliases ~universe:(Some status.multi_aliases) - ~context ~metasenv:(GrafiteTypes.get_proof_metasenv status) term) + (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) + ~aliases:lexicon_status.LexiconEngine.aliases + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~context ~metasenv term) in - let status = GrafiteTypes.set_metasenv metasenv status in - let status = MatitaSync.set_proof_aliases status diff in - status_ref := status; - cic + let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in + lexicon_status_ref := lexicon_status; + metasenv,cic (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term * rationale: lazy_term will be invoked in different context to obtain a term, * each invocation will disambiguate the term and can add aliases. Once all * disambiguations have been performed, the first returned function can be * used to obtain the resulting aliases *) -let disambiguate_lazy_term status_ref term = +let disambiguate_lazy_term lexicon_status_ref term = (fun context metasenv ugraph -> - let status = !status_ref in + let lexicon_status = !lexicon_status_ref in let (diff, metasenv, cic, ugraph) = singleton - (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) - ~initial_ugraph:ugraph ~aliases:status.aliases - ~universe:(Some status.multi_aliases) ~context ~metasenv term) - in - let status = GrafiteTypes.set_metasenv metasenv status in - let status = MatitaSync.set_proof_aliases status diff in - status_ref := status; + (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) + ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~context ~metasenv + term) in + let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in + lexicon_status_ref := lexicon_status; cic, metasenv, ugraph) -let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) = +let disambiguate_pattern lexicon_status_ref (wanted, hyp_paths, goal_path) = let interp path = Disambiguate.interpretate_path [] path in let goal_path = HExtlib.map_option interp goal_path in let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in @@ -75,14 +70,14 @@ let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) = match wanted with None -> None | Some wanted -> - let wanted = disambiguate_lazy_term status_ref wanted in + let wanted = disambiguate_lazy_term lexicon_status_ref wanted in Some wanted in (wanted, hyp_paths, goal_path) -let disambiguate_reduction_kind aliases_ref = function +let disambiguate_reduction_kind lexicon_status_ref = function | `Unfold (Some t) -> - let t = disambiguate_lazy_term aliases_ref t in + let t = disambiguate_lazy_term lexicon_status_ref t in `Unfold (Some t) | `Normalize | `Reduce @@ -90,164 +85,176 @@ let disambiguate_reduction_kind aliases_ref = function | `Unfold None | `Whd as kind -> kind -let disambiguate_tactic status goal tactic = - let status_ref = ref status in - let tactic = - match tactic with +let disambiguate_tactic lexicon_status_ref context metasenv tactic = + let disambiguate_term = disambiguate_term lexicon_status_ref in + let disambiguate_pattern = disambiguate_pattern lexicon_status_ref in + let disambiguate_reduction_kind = disambiguate_reduction_kind lexicon_status_ref in + let disambiguate_lazy_term = disambiguate_lazy_term lexicon_status_ref in + match tactic with | GrafiteAst.Absurd (loc, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Absurd (loc, cic) + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Absurd (loc, cic) | GrafiteAst.Apply (loc, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Apply (loc, cic) - | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Apply (loc, cic) + | GrafiteAst.Assumption loc -> + metasenv,GrafiteAst.Assumption loc | GrafiteAst.Auto (loc,depth,width,paramodulation,full) -> - GrafiteAst.Auto (loc,depth,width,paramodulation,full) + metasenv,GrafiteAst.Auto (loc,depth,width,paramodulation,full) | GrafiteAst.Change (loc, pattern, with_what) -> - let with_what = disambiguate_lazy_term status_ref with_what in - let pattern = disambiguate_pattern status_ref pattern in - GrafiteAst.Change (loc, pattern, with_what) - | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id) - | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id) + let with_what = disambiguate_lazy_term with_what in + let pattern = disambiguate_pattern pattern in + metasenv,GrafiteAst.Change (loc, pattern, with_what) + | GrafiteAst.Clear (loc,id) -> + metasenv,GrafiteAst.Clear (loc,id) + | GrafiteAst.ClearBody (loc,id) -> + metasenv,GrafiteAst.ClearBody (loc,id) | GrafiteAst.Compare (loc,term) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.Compare (loc,term) - | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n) - | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Compare (loc,term) + | GrafiteAst.Constructor (loc,n) -> + metasenv,GrafiteAst.Constructor (loc,n) + | GrafiteAst.Contradiction loc -> + metasenv,GrafiteAst.Contradiction loc | GrafiteAst.Cut (loc, ident, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Cut (loc, ident, cic) - | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Cut (loc, ident, cic) + | GrafiteAst.DecideEquality loc -> + metasenv,GrafiteAst.DecideEquality loc | GrafiteAst.Decompose (loc, types, what, names) -> - let disambiguate types = function + let disambiguate (metasenv,types) = function | GrafiteAst.Type _ -> assert false | GrafiteAst.Ident id -> - (match disambiguate_term status_ref goal - (CicNotationPt.Ident (id, None)) - with - | Cic.MutInd (uri, tyno, _) -> - (GrafiteAst.Type (uri, tyno) :: types) - | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]]))) + (match + disambiguate_term context metasenv + (CicNotationPt.Ident(id, None)) + with + | metasenv,Cic.MutInd (uri, tyno, _) -> + metasenv,(GrafiteAst.Type (uri, tyno) :: types) + | _ -> + raise (GrafiteDisambiguator.DisambiguationError + (0,[[None,lazy "Decompose works only on inductive types"]]))) + in + let metasenv,types = + List.fold_left disambiguate (metasenv,[]) types in - let types = List.fold_left disambiguate [] types in - GrafiteAst.Decompose (loc, types, what, names) + metasenv,GrafiteAst.Decompose (loc, types, what, names) | GrafiteAst.Discriminate (loc,term) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.Discriminate(loc,term) + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Discriminate(loc,term) | GrafiteAst.Exact (loc, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Exact (loc, cic) + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Exact (loc, cic) | GrafiteAst.Elim (loc, what, Some using, depth, idents) -> - let what = disambiguate_term status_ref goal what in - let using = disambiguate_term status_ref goal using in - GrafiteAst.Elim (loc, what, Some using, depth, idents) + let metasenv,what = disambiguate_term context metasenv what in + let metasenv,using = disambiguate_term context metasenv using in + metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents) | GrafiteAst.Elim (loc, what, None, depth, idents) -> - let what = disambiguate_term status_ref goal what in - GrafiteAst.Elim (loc, what, None, depth, idents) + let metasenv,what = disambiguate_term context metasenv what in + metasenv,GrafiteAst.Elim (loc, what, None, depth, idents) | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> - let what = disambiguate_term status_ref goal what in - let using = disambiguate_term status_ref goal using in - GrafiteAst.ElimType (loc, what, Some using, depth, idents) + let metasenv,what = disambiguate_term context metasenv what in + let metasenv,using = disambiguate_term context metasenv using in + metasenv,GrafiteAst.ElimType (loc, what, Some using, depth, idents) | GrafiteAst.ElimType (loc, what, None, depth, idents) -> - let what = disambiguate_term status_ref goal what in - GrafiteAst.ElimType (loc, what, None, depth, idents) - | GrafiteAst.Exists loc -> GrafiteAst.Exists loc - | GrafiteAst.Fail loc -> GrafiteAst.Fail loc + let metasenv,what = disambiguate_term context metasenv what in + metasenv,GrafiteAst.ElimType (loc, what, None, depth, idents) + | GrafiteAst.Exists loc -> + metasenv,GrafiteAst.Exists loc + | GrafiteAst.Fail loc -> + metasenv,GrafiteAst.Fail loc | GrafiteAst.Fold (loc,red_kind, term, pattern) -> - let pattern = disambiguate_pattern status_ref pattern in - let term = disambiguate_lazy_term status_ref term in - let red_kind = disambiguate_reduction_kind status_ref red_kind in - GrafiteAst.Fold (loc, red_kind, term, pattern) + let pattern = disambiguate_pattern pattern in + let term = disambiguate_lazy_term term in + let red_kind = disambiguate_reduction_kind red_kind in + metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern) | GrafiteAst.FwdSimpl (loc, hyp, names) -> - GrafiteAst.FwdSimpl (loc, hyp, names) - | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc + metasenv,GrafiteAst.FwdSimpl (loc, hyp, names) + | GrafiteAst.Fourier loc -> + metasenv,GrafiteAst.Fourier loc | GrafiteAst.Generalize (loc,pattern,ident) -> - let pattern = disambiguate_pattern status_ref pattern in - GrafiteAst.Generalize (loc,pattern,ident) - | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g) - | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc + let pattern = disambiguate_pattern pattern in + metasenv,GrafiteAst.Generalize (loc,pattern,ident) + | GrafiteAst.Goal (loc, g) -> + metasenv,GrafiteAst.Goal (loc, g) + | GrafiteAst.IdTac loc -> + metasenv,GrafiteAst.IdTac loc | GrafiteAst.Injection (loc, term) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.Injection (loc,term) - | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names) + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Injection (loc,term) + | GrafiteAst.Intros (loc, num, names) -> + metasenv,GrafiteAst.Intros (loc, num, names) | GrafiteAst.Inversion (loc, term) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.Inversion (loc, term) + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Inversion (loc, term) | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> let f term to_what = - let term = disambiguate_term status_ref goal term in + let metasenv,term = disambiguate_term context metasenv term in term :: to_what in let to_what = List.fold_right f to_what [] in - let what = disambiguate_term status_ref goal what in - GrafiteAst.LApply (loc, depth, to_what, what, ident) - | GrafiteAst.Left loc -> GrafiteAst.Left loc + let metasenv,what = disambiguate_term context metasenv what in + metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident) + | GrafiteAst.Left loc -> + metasenv,GrafiteAst.Left loc | GrafiteAst.LetIn (loc, term, name) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.LetIn (loc,term,name) + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.LetIn (loc,term,name) | GrafiteAst.Reduce (loc, red_kind, pattern) -> - let pattern = disambiguate_pattern status_ref pattern in - let red_kind = disambiguate_reduction_kind status_ref red_kind in - GrafiteAst.Reduce(loc, red_kind, pattern) - | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc + let pattern = disambiguate_pattern pattern in + let red_kind = disambiguate_reduction_kind red_kind in + metasenv,GrafiteAst.Reduce(loc, red_kind, pattern) + | GrafiteAst.Reflexivity loc -> + metasenv,GrafiteAst.Reflexivity loc | GrafiteAst.Replace (loc, pattern, with_what) -> - let pattern = disambiguate_pattern status_ref pattern in - let with_what = disambiguate_lazy_term status_ref with_what in - GrafiteAst.Replace (loc, pattern, with_what) + let pattern = disambiguate_pattern pattern in + let with_what = disambiguate_lazy_term with_what in + metasenv,GrafiteAst.Replace (loc, pattern, with_what) | GrafiteAst.Rewrite (loc, dir, t, pattern) -> - let term = disambiguate_term status_ref goal t in - let pattern = disambiguate_pattern status_ref pattern in - GrafiteAst.Rewrite (loc, dir, term, pattern) - | GrafiteAst.Right loc -> GrafiteAst.Right loc - | GrafiteAst.Ring loc -> GrafiteAst.Ring loc - | GrafiteAst.Split loc -> GrafiteAst.Split loc - | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc + let metasenv,term = disambiguate_term context metasenv t in + let pattern = disambiguate_pattern pattern in + metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern) + | GrafiteAst.Right loc -> + metasenv,GrafiteAst.Right loc + | GrafiteAst.Ring loc -> + metasenv,GrafiteAst.Ring loc + | GrafiteAst.Split loc -> + metasenv,GrafiteAst.Split loc + | GrafiteAst.Symmetry loc -> + metasenv,GrafiteAst.Symmetry loc | GrafiteAst.Transitivity (loc, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Transitivity (loc, cic) - in - status_ref, tactic + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Transitivity (loc, cic) -let disambiguate_obj status obj = +let disambiguate_obj lexicon_status ~baseuri metasenv obj = let uri = match obj with | CicNotationPt.Inductive (_,(name,_,_,_)::_) | CicNotationPt.Record (_,name,_,_) -> - Some (UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ".ind")) + (match baseuri with + | Some baseuri -> + Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind")) + | None -> raise BaseUriNotSetYet) | CicNotationPt.Inductive _ -> assert false | CicNotationPt.Theorem _ -> None in let (diff, metasenv, cic, _) = singleton - (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ()) - ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj) - in - let proof_status = - match status.proof_status with - | No_proof -> Intermediate metasenv - | Incomplete_proof _ - | Proof _ -> - raise (GrafiteTypes.Command_error "imbricated proofs not allowed") - | Intermediate _ -> assert false - in - let status = { status with proof_status = proof_status } in - let status = MatitaSync.set_proof_aliases status diff in - status, cic + (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ()) + ~aliases:lexicon_status.LexiconEngine.aliases + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri obj) in + let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in + lexicon_status, metasenv, cic -let disambiguate_command status = +let disambiguate_command lexicon_status ~baseuri metasenv = function - | GrafiteAst.Alias _ | GrafiteAst.Coercion _ | GrafiteAst.Default _ | GrafiteAst.Drop _ - | GrafiteAst.Dump _ | GrafiteAst.Include _ - | GrafiteAst.Interpretation _ - | GrafiteAst.Notation _ | GrafiteAst.Qed _ - | GrafiteAst.Render _ | GrafiteAst.Set _ as cmd -> - status,cmd + lexicon_status,metasenv,cmd | GrafiteAst.Obj (loc,obj) -> - let status,obj = disambiguate_obj status obj in - status, GrafiteAst.Obj (loc,obj) - + let lexicon_status,metasenv,obj = + disambiguate_obj lexicon_status ~baseuri metasenv obj in + lexicon_status, metasenv, GrafiteAst.Obj (loc,obj) diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli index 379b65c1e..9944825e6 100644 --- a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli @@ -23,15 +23,19 @@ * http://helm.cs.unibo.it/ *) +exception BaseUriNotSetYet + val disambiguate_tactic: - GrafiteTypes.status -> - ProofEngineTypes.goal -> + LexiconEngine.status ref -> + Cic.context -> + Cic.metasenv -> (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic -> - GrafiteTypes.status ref * - (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic + Cic.metasenv * + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic val disambiguate_command: - GrafiteTypes.status -> + LexiconEngine.status -> + baseuri:string option -> + Cic.metasenv -> CicNotationPt.obj GrafiteAst.command -> - GrafiteTypes.status * Cic.obj GrafiteAst.command - + LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.ml b/helm/ocaml/grafite_parser/grafiteDisambiguator.ml similarity index 100% rename from helm/ocaml/grafite_parser/matitaDisambiguator.ml rename to helm/ocaml/grafite_parser/grafiteDisambiguator.ml diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.mli b/helm/ocaml/grafite_parser/grafiteDisambiguator.mli similarity index 100% rename from helm/ocaml/grafite_parser/matitaDisambiguator.mli rename to helm/ocaml/grafite_parser/grafiteDisambiguator.mli diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml index 5b9cea37a..d32eb3265 100644 --- a/helm/ocaml/grafite_parser/grafiteParser.ml +++ b/helm/ocaml/grafite_parser/grafiteParser.ml @@ -27,10 +27,17 @@ open Printf module Ast = CicNotationPt +type 'a localized_option = + LSome of 'a + | LNone of Token.flocation + type statement = - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, - CicNotationPt.obj, string) - GrafiteAst.statement + include_paths:string list -> + LexiconEngine.status -> + LexiconEngine.status * + (CicNotationPt.term, CicNotationPt.term, + CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + GrafiteAst.statement localized_option let grammar = CicNotationParser.level2_ast_grammar @@ -353,7 +360,7 @@ EXTEND if (try ignore (UriManager.uri_of_string uri); true with UriManager.IllFormedUri _ -> false) then - GrafiteAst.Ident_alias (id, uri) + LexiconAst.Ident_alias (id, uri) else raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri))) @@ -366,14 +373,14 @@ EXTEND let instance = match instance with Some i -> i | None -> 0 in - GrafiteAst.Symbol_alias (symbol, instance, dsc) + LexiconAst.Symbol_alias (symbol, instance, dsc) | IDENT "num"; instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; SYMBOL "="; dsc = QSTRING -> let instance = match instance with Some i -> i | None -> 0 in - GrafiteAst.Number_alias (instance, dsc) + LexiconAst.Number_alias (instance, dsc) ] ]; argument: [ @@ -439,7 +446,12 @@ EXTEND (s, args, t) ] ]; - command: [ [ + + include_command: [ [ + IDENT "include" ; path = QSTRING -> loc,path + ]]; + + grafite_command: [ [ IDENT "set"; n = QSTRING; v = QSTRING -> GrafiteAst.Set (loc, n, v) | IDENT "drop" -> GrafiteAst.Drop loc @@ -480,27 +492,23 @@ EXTEND GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) | IDENT "coercion" ; suri = URI -> GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true) - | IDENT "alias" ; spec = alias_spec -> - GrafiteAst.Alias (loc, spec) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) - | IDENT "include" ; path = QSTRING -> - GrafiteAst.Include (loc,path) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> let uris = List.map UriManager.uri_of_string uris in GrafiteAst.Default (loc,what,uris) + ]]; + lexicon_command: [ [ + IDENT "alias" ; spec = alias_spec -> + LexiconAst.Alias (loc, spec) | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation -> - GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2) + LexiconAst.Notation (loc, dir, l1, assoc, prec, l2) | IDENT "interpretation"; id = QSTRING; (symbol, args, l3) = interpretation -> - GrafiteAst.Interpretation (loc, id, (symbol, args), l3) - - | IDENT "dump" -> GrafiteAst.Dump loc - | IDENT "render"; u = URI -> - GrafiteAst.Render (loc, UriManager.uri_of_string u) + LexiconAst.Interpretation (loc, id, (symbol, args), l3) ]]; executable: [ - [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) + [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) | tac = tactical; punct = punctuation_tactical -> GrafiteAst.Tactical (loc, tac, Some punct) | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None) @@ -515,8 +523,25 @@ EXTEND ] ]; statement: [ - [ ex = executable -> GrafiteAst.Executable (loc,ex) - | com = comment -> GrafiteAst.Comment (loc, com) + [ ex = executable -> + fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex)) + | com = comment -> + fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) + | (iloc,fname) = include_command ; SYMBOL "." -> + fun ~include_paths status -> + let path = DependenciesParser.baseuri_of_script ~include_paths fname in + let status = + LexiconEngine.eval_command status (LexiconAst.Include (iloc,path)) + in + status, + LSome + (GrafiteAst.Executable + (loc,GrafiteAst.Command + (loc,GrafiteAst.Include (iloc,path)))) + | scom = lexicon_command ; SYMBOL "." -> + fun ~include_paths status -> + let status = LexiconEngine.eval_command status scom in + status,LNone loc | EOI -> raise End_of_file ] ]; @@ -536,22 +561,3 @@ let exc_located_wrapper f = let parse_statement lexbuf = exc_located_wrapper (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf))) - -let parse_dependencies lexbuf = - let tok_stream,_ = - CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf) - in - let rec parse acc = - (parser - | [< '("URI", u) >] -> - parse (GrafiteAst.UriDep (UriManager.uri_of_string u) :: acc) - | [< '("IDENT", "include"); '("QSTRING", fname) >] -> - parse (GrafiteAst.IncludeDep fname :: acc) - | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] -> - parse (GrafiteAst.BaseuriDep baseuri :: acc) - | [< '("EOI", _) >] -> acc - | [< 'tok >] -> parse acc - | [< >] -> acc) tok_stream - in - List.rev (parse []) - diff --git a/helm/ocaml/grafite_parser/grafiteParser.mli b/helm/ocaml/grafite_parser/grafiteParser.mli index 7b33c6e42..6a1980011 100644 --- a/helm/ocaml/grafite_parser/grafiteParser.mli +++ b/helm/ocaml/grafite_parser/grafiteParser.mli @@ -23,15 +23,19 @@ * http://helm.cs.unibo.it/ *) +type 'a localized_option = + LSome of 'a + | LNone of Token.flocation + type statement = - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, - CicNotationPt.obj, string) - GrafiteAst.statement + include_paths:string list -> + LexiconEngine.status -> + LexiconEngine.status * + (CicNotationPt.term, CicNotationPt.term, + CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + GrafiteAst.statement localized_option val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) - (** @raise End_of_file *) -val parse_dependencies: Ulexing.lexbuf -> GrafiteAst.dependency list - val statement: statement Grammar.Entry.e diff --git a/helm/ocaml/grafite_parser/grafiteParserMisc.ml b/helm/ocaml/grafite_parser/grafiteParserMisc.ml deleted file mode 100644 index 1b77da7cb..000000000 --- a/helm/ocaml/grafite_parser/grafiteParserMisc.ml +++ /dev/null @@ -1,80 +0,0 @@ -(* 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/test_dep.ml b/helm/ocaml/grafite_parser/test_dep.ml index a2c7e392e..90fdcd3b5 100644 --- a/helm/ocaml/grafite_parser/test_dep.ml +++ b/helm/ocaml/grafite_parser/test_dep.ml @@ -32,7 +32,7 @@ let _ = in Arg.parse [] open_file usage; let deps = - GrafiteParser.parse_dependencies (Ulexing.from_utf8_channel !ic) + DependenciesParser.parse_dependencies (Ulexing.from_utf8_channel !ic) in - List.iter (fun dep -> print_endline (GrafiteAstPp.pp_dependency dep)) deps + List.iter (fun dep -> print_endline (DependenciesParser.pp_dependency dep)) deps diff --git a/helm/ocaml/grafite_parser/test_parser.ml b/helm/ocaml/grafite_parser/test_parser.ml index 76463f814..3b5c8f375 100644 --- a/helm/ocaml/grafite_parser/test_parser.ml +++ b/helm/ocaml/grafite_parser/test_parser.ml @@ -62,76 +62,47 @@ let process_stream istream = let char_count = ref 0 in let module P = CicNotationPt in let module G = GrafiteAst in + let status = + ref + (CicNotation2.load_notation + ~include_paths:[] (Helm_registry.get "notation.core_file")) + in try while true do try - let statement = GrafiteParser.parse_statement istream in - let floc = extract_loc statement in - let (_, y) = HExtlib.loc_of_floc floc in - char_count := y + !char_count; - match statement with -(* | G.Executable (_, G.Macro (_, G.Check (_, - P.AttributedTerm (_, P.Ident _)))) -> - prerr_endline "mega hack"; - (match !last_rule_id with - | None -> () - | Some id -> - prerr_endline "removing last notation rule ..."; - CicNotationParser.delete id) *) - | G.Executable (_, G.Macro (_, G.Check (_, t))) -> - prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); - let t' = TermContentPres.pp_ast t in - prerr_endline (sprintf "rendered ast: %s" - (CicNotationPp.pp_term t')); - let tbl = Hashtbl.create 0 in - dump_xml t' tbl "out.xml" - | G.Executable (_, G.Command (_, - G.Notation (_, dir, l1, associativity, precedence, l2))) -> - prerr_endline "notation"; - prerr_endline (sprintf "l1: %s" (CicNotationPp.pp_term l1)); - prerr_endline (sprintf "l2: %s" (CicNotationPp.pp_term l2)); - prerr_endline (sprintf "prec: %s" (pp_precedence precedence)); - prerr_endline (sprintf "assoc: %s" (pp_associativity associativity)); - let keywords = CicNotationUtil.keywords_of_term l1 in - if keywords <> [] then - prerr_endline (sprintf "keywords: %s" - (String.concat " " keywords)); - if dir <> Some `RightToLeft then - ignore - (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> TermContentPres.instantiate_level2 env l2)); -(* last_rule_id := Some rule_id; *) - if dir <> Some `LeftToRight then - ignore (TermContentPres.add_pretty_printer - ?precedence ?associativity l2 l1) - | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) -> - prerr_endline "interpretation"; - prerr_endline (sprintf "dsc: %s" id); - ignore (TermAcicContent.add_interpretation id l2 l3); - flush stdout - | G.Executable (_, G.Command (_, G.Dump _)) -> - CicNotationParser.print_l2_pattern (); print_newline () - | G.Executable (_, G.Command (_, G.Render (_, uri))) -> - let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - let annobj, _, _, id_to_sort, _, _, _ = - Cic2acic.acic_object_of_cic_object obj - in - let annterm = - match annobj with - | Cic.AConstant (_, _, _, _, ty, _, _) - | Cic.AVariable (_, _, _, ty, _, _) -> ty - | _ -> assert false - in - let t, id_to_uri = - TermAcicContent.ast_of_acic id_to_sort annterm - in - prerr_endline "Raw AST"; - prerr_endline (CicNotationPp.pp_term t); - let t' = TermContentPres.pp_ast t in - prerr_endline "Rendered AST"; - prerr_endline (CicNotationPp.pp_term t'); - dump_xml t' id_to_uri "out.xml" - | _ -> prerr_endline "Unsupported statement" + match + GrafiteParser.parse_statement ~include_paths:[] istream !status + with + newstatus, GrafiteParser.LNone _ -> status := newstatus + | newstatus, GrafiteParser.LSome statement -> + status := newstatus; + let floc = extract_loc statement in + let (_, y) = HExtlib.loc_of_floc floc in + char_count := y + !char_count; + match statement with + (* | G.Executable (_, G.Macro (_, G.Check (_, + P.AttributedTerm (_, P.Ident _)))) -> + prerr_endline "mega hack"; + (match !last_rule_id with + | None -> () + | Some id -> + prerr_endline "removing last notation rule ..."; + CicNotationParser.delete id) *) + | G.Executable (_, G.Macro (_, G.Check (_, t))) -> + prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); + let t' = TermContentPres.pp_ast t in + prerr_endline (sprintf "rendered ast: %s" + (CicNotationPp.pp_term t')); + let tbl = Hashtbl.create 0 in + dump_xml t' tbl "out.xml" + | statement -> + prerr_endline + ("Unsupported statement: " ^ + GrafiteAstPp.pp_statement + ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:(fun _ -> "_lazy_term_here_") + ~obj_pp:(fun _ -> "_obj_here_") + statement) with | End_of_file -> raise End_of_file | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) -> @@ -154,7 +125,6 @@ let _ = let usage = "" in Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; print_endline "Loading builtin notation ..."; - CicNotation2.load_notation (Helm_registry.get "notation.core_file"); print_endline "done."; flush stdout; process_stream (Ulexing.from_utf8_channel stdin) diff --git a/helm/ocaml/lexicon/.cvsignore b/helm/ocaml/lexicon/.cvsignore new file mode 100644 index 000000000..f83e2a8d0 --- /dev/null +++ b/helm/ocaml/lexicon/.cvsignore @@ -0,0 +1,7 @@ +*.cmi +*.cma +*.cmo +*.cmx +*.cmxa +*.o +*.a diff --git a/helm/ocaml/lexicon/.depend b/helm/ocaml/lexicon/.depend new file mode 100644 index 000000000..452167c72 --- /dev/null +++ b/helm/ocaml/lexicon/.depend @@ -0,0 +1,20 @@ +lexiconAstPp.cmi: lexiconAst.cmo +disambiguatePp.cmi: lexiconAst.cmo +lexiconMarshal.cmi: lexiconAst.cmo +cicNotation.cmi: lexiconAst.cmo +lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi +lexiconSync.cmi: lexiconEngine.cmi +lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi +lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi +disambiguatePp.cmo: lexiconAstPp.cmi lexiconAst.cmo disambiguatePp.cmi +disambiguatePp.cmx: lexiconAstPp.cmx lexiconAst.cmx disambiguatePp.cmi +lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi +lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi +cicNotation.cmo: lexiconAst.cmo cicNotation.cmi +cicNotation.cmx: lexiconAst.cmx cicNotation.cmi +lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmo disambiguatePp.cmi \ + cicNotation.cmi lexiconEngine.cmi +lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx disambiguatePp.cmx \ + cicNotation.cmx lexiconEngine.cmi +lexiconSync.cmo: lexiconEngine.cmi cicNotation.cmi lexiconSync.cmi +lexiconSync.cmx: lexiconEngine.cmx cicNotation.cmx lexiconSync.cmi diff --git a/helm/ocaml/lexicon/Makefile b/helm/ocaml/lexicon/Makefile new file mode 100644 index 000000000..0e9c09526 --- /dev/null +++ b/helm/ocaml/lexicon/Makefile @@ -0,0 +1,17 @@ +PACKAGE = lexicon +PREDICATES = + +INTERFACE_FILES = \ + lexiconAstPp.mli \ + disambiguatePp.mli \ + lexiconMarshal.mli \ + cicNotation.mli \ + lexiconEngine.mli \ + lexiconSync.mli \ + $(NULL) +IMPLEMENTATION_FILES = \ + lexiconAst.ml \ + $(INTERFACE_FILES:%.mli=%.ml) + + +include ../Makefile.common diff --git a/helm/ocaml/grafite/cicNotation.ml b/helm/ocaml/lexicon/cicNotation.ml similarity index 96% rename from helm/ocaml/grafite/cicNotation.ml rename to helm/ocaml/lexicon/cicNotation.ml index 9500a8e11..0d48ea06d 100644 --- a/helm/ocaml/grafite/cicNotation.ml +++ b/helm/ocaml/lexicon/cicNotation.ml @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -open GrafiteAst +open LexiconAst type notation_id = | RuleId of CicNotationParser.rule_id @@ -50,11 +50,11 @@ let process_notation st = else [] in - st, rule_id @ pp_id + rule_id @ pp_id | Interpretation (loc, dsc, l2, l3) -> let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in - st, [ InterpretationId interp_id ] - | st -> st, [] + [InterpretationId interp_id] + | st -> [] let remove_notation = function | RuleId id -> CicNotationParser.delete id diff --git a/helm/ocaml/grafite/cicNotation.mli b/helm/ocaml/lexicon/cicNotation.mli similarity index 93% rename from helm/ocaml/grafite/cicNotation.mli rename to helm/ocaml/lexicon/cicNotation.mli index 9eb98c1d3..944438df8 100644 --- a/helm/ocaml/grafite/cicNotation.mli +++ b/helm/ocaml/lexicon/cicNotation.mli @@ -25,8 +25,7 @@ type notation_id -val process_notation: - 'obj GrafiteAst.command -> 'obj GrafiteAst.command * notation_id list +val process_notation: LexiconAst.command -> notation_id list val remove_notation: notation_id -> unit diff --git a/helm/ocaml/grafite2/disambiguatePp.ml b/helm/ocaml/lexicon/disambiguatePp.ml similarity index 88% rename from helm/ocaml/grafite2/disambiguatePp.ml rename to helm/ocaml/lexicon/disambiguatePp.ml index 733179589..a54e67506 100644 --- a/helm/ocaml/grafite2/disambiguatePp.ml +++ b/helm/ocaml/lexicon/disambiguatePp.ml @@ -27,9 +27,9 @@ open DisambiguateTypes let alias_of_domain_and_codomain_items domain_item (dsc,_) = match domain_item with - Id id -> GrafiteAst.Ident_alias (id, dsc) - | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc) - | Num i -> GrafiteAst.Number_alias (i, dsc) + Id id -> LexiconAst.Ident_alias (id, dsc) + | Symbol (symb, i) -> LexiconAst.Symbol_alias (symb, i, dsc) + | Num i -> LexiconAst.Number_alias (i, dsc) let aliases_of_environment env = Environment.fold @@ -46,6 +46,6 @@ let aliases_of_domain_and_codomain_items_list l = let pp_environment env = let aliases = aliases_of_environment env in let strings = - List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases + List.map (fun alias -> LexiconAstPp.pp_alias alias ^ ".") aliases in String.concat "\n" (List.sort compare strings) diff --git a/helm/ocaml/grafite2/disambiguatePp.mli b/helm/ocaml/lexicon/disambiguatePp.mli similarity index 97% rename from helm/ocaml/grafite2/disambiguatePp.mli rename to helm/ocaml/lexicon/disambiguatePp.mli index 516dfee17..e8d9b94a4 100644 --- a/helm/ocaml/grafite2/disambiguatePp.mli +++ b/helm/ocaml/lexicon/disambiguatePp.mli @@ -25,6 +25,6 @@ val aliases_of_domain_and_codomain_items_list: (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> - GrafiteAst.alias_spec list + LexiconAst.alias_spec list val pp_environment: DisambiguateTypes.environment -> string diff --git a/helm/ocaml/lexicon/lexiconAst.ml b/helm/ocaml/lexicon/lexiconAst.ml new file mode 100644 index 000000000..13135744e --- /dev/null +++ b/helm/ocaml/lexicon/lexiconAst.ml @@ -0,0 +1,53 @@ +(* 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/ + *) + +type direction = [ `LeftToRight | `RightToLeft ] + +type loc = Token.flocation + +type alias_spec = + | Ident_alias of string * string (* identifier, uri *) + | Symbol_alias of string * int * string (* name, instance no, description *) + | Number_alias of int * string (* instance no, description *) + +(** To be increased each time the command type below changes, used for "safe" + * marshalling *) +let magic = 5 + +type command = + | Include of loc * string + | Alias of loc * alias_spec + (** parameters, name, type, fields *) + | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc * + int * CicNotationPt.term + (* direction, l1 pattern, associativity, precedence, l2 pattern *) + | Interpretation of loc * + string * (string * CicNotationPt.argument_pattern list) * + CicNotationPt.cic_appl_pattern + (* description (i.e. id), symbol, arg pattern, appl pattern *) + +(* composed magic: term + command magics. No need to change this value *) +let magic = magic + 10000 * CicNotationPt.magic + diff --git a/helm/ocaml/lexicon/lexiconAstPp.ml b/helm/ocaml/lexicon/lexiconAstPp.ml new file mode 100644 index 000000000..57d22d6b4 --- /dev/null +++ b/helm/ocaml/lexicon/lexiconAstPp.ml @@ -0,0 +1,82 @@ +(* 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/ + *) + +open Printf + +open LexiconAst + +let pp_l1_pattern = CicNotationPp.pp_term +let pp_l2_pattern = CicNotationPp.pp_term + +let pp_alias = function + | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri + | Symbol_alias (symb, instance, desc) -> + sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" + symb instance desc + | Number_alias (instance,desc) -> + sprintf "alias num (instance %d) = \"%s\"" instance desc + +let pp_associativity = function + | Gramext.LeftA -> "left associative" + | Gramext.RightA -> "right associative" + | Gramext.NonA -> "non associative" + +let pp_precedence i = sprintf "with precedence %d" i + +let pp_argument_pattern = function + | CicNotationPt.IdentArg (eta_depth, name) -> + let eta_buf = Buffer.create 5 in + for i = 1 to eta_depth do + Buffer.add_string eta_buf "\\eta." + done; + sprintf "%s%s" (Buffer.contents eta_buf) name + +let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = + sprintf "interpretation \"%s\" '%s %s = %s" + dsc symbol + (String.concat " " (List.map pp_argument_pattern arg_patterns)) + (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern) + +let pp_dir_opt = function + | None -> "" + | Some `LeftToRight -> "> " + | Some `RightToLeft -> "< " + +let pp_notation dir_opt l1_pattern assoc prec l2_pattern = + sprintf "notation %s\"%s\" %s %s for %s" + (pp_dir_opt dir_opt) + (pp_l1_pattern l1_pattern) + (pp_associativity assoc) + (pp_precedence prec) + (pp_l2_pattern l2_pattern) + +let pp_command = function + | Include (_,path) -> "include " ^ path + | Alias (_,s) -> pp_alias s + | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> + pp_interpretation dsc symbol arg_patterns cic_appl_pattern + | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> + pp_notation dir_opt l1_pattern assoc prec l2_pattern + diff --git a/helm/ocaml/grafite_parser/grafiteParserMisc.mli b/helm/ocaml/lexicon/lexiconAstPp.mli similarity index 78% rename from helm/ocaml/grafite_parser/grafiteParserMisc.mli rename to helm/ocaml/lexicon/lexiconAstPp.mli index 74f60ec04..b7ad59f3c 100644 --- a/helm/ocaml/grafite_parser/grafiteParserMisc.mli +++ b/helm/ocaml/lexicon/lexiconAstPp.mli @@ -1,4 +1,4 @@ -(* Copyright (C) 2004-2005, HELM Team. +(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,10 +23,7 @@ * http://helm.cs.unibo.it/ *) -exception UnableToInclude of string +val pp_command: LexiconAst.command -> string -val baseuri_of_baseuri_decl : - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> - string option +val pp_alias: LexiconAst.alias_spec -> string -val baseuri_of_script : include_paths:string list -> string -> string diff --git a/helm/ocaml/lexicon/lexiconEngine.ml b/helm/ocaml/lexicon/lexiconEngine.ml new file mode 100644 index 000000000..ff186b131 --- /dev/null +++ b/helm/ocaml/lexicon/lexiconEngine.ml @@ -0,0 +1,149 @@ +(* 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 IncludedFileNotCompiled of string (* file name *) +exception MetadataNotFound of string (* file name *) + +type status = { + aliases: DisambiguateTypes.environment; (** disambiguation aliases *) + multi_aliases: DisambiguateTypes.multiple_environment; + lexicon_content_rev: LexiconMarshal.lexicon; + notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) + metadata: LibraryNoDb.metadata list; +} + +let add_lexicon_content cmds status = + let content = status.lexicon_content_rev in + let content' = + List.fold_right + (fun cmd acc -> cmd :: (List.filter ((<>) cmd) acc)) + cmds content + in +(* prerr_endline ("new lexicon content: " ^ String.concat " " (List.map + LexiconAstPp.pp_command content')); *) + { status with lexicon_content_rev = content' } + +let add_metadata new_metadata status = + if Helm_registry.get_bool "db.nodb" then + let metadata = status.metadata in + let metadata' = + List.fold_left + (fun acc m -> + match m with + | LibraryNoDb.Dependency buri -> + if List.exists (LibraryNoDb.eq_metadata m) metadata + then acc + else m :: acc + | _ -> m :: acc) + metadata new_metadata + in + { status with metadata = metadata' } + else + status + +let set_proof_aliases status new_aliases = + let commands_of_aliases = + List.map + (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias)) + in + let deps_of_aliases = + HExtlib.filter_map + (function + | LexiconAst.Ident_alias (_, suri) -> + let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in + Some (LibraryNoDb.Dependency buri) + | _ -> None) + in + let aliases = + List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) + status.aliases new_aliases in + let multi_aliases = + List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) + status.multi_aliases new_aliases in + let new_status = + { status with multi_aliases = multi_aliases ; aliases = aliases} + in + if new_aliases = [] then + new_status + else + let aliases = + DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases + in + let status = add_lexicon_content (commands_of_aliases aliases) new_status in + let status = add_metadata (deps_of_aliases aliases) status in + status + +let rec eval_command status cmd = + let notation_ids' = CicNotation.process_notation cmd in + let status = + { status with notation_ids = notation_ids' @ status.notation_ids } in + let basedir = Helm_registry.get "matita.basedir" in + match cmd with + | LexiconAst.Include (loc, baseuri) -> + let lexiconpath = LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri in + if not (Sys.file_exists lexiconpath) then + raise (IncludedFileNotCompiled lexiconpath); + let lexicon = LexiconMarshal.load_lexicon lexiconpath in + let status = List.fold_left eval_command status lexicon in + if Helm_registry.get_bool "db.nodb" then + let metadatapath = baseuri ^ ".metadata" in + if not (Sys.file_exists metadatapath) then + raise (MetadataNotFound metadatapath) + else + add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status + else + status + | LexiconAst.Alias (loc, spec) -> + let diff = + (*CSC: Warning: this code should be factorized with the corresponding + code in DisambiguatePp *) + match spec with + | LexiconAst.Ident_alias (id,uri) -> + [DisambiguateTypes.Id id, + (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))] + | LexiconAst.Symbol_alias (symb, instance, desc) -> + [DisambiguateTypes.Symbol (symb,instance), + DisambiguateChoices.lookup_symbol_by_dsc symb desc] + | LexiconAst.Number_alias (instance,desc) -> + [DisambiguateTypes.Num instance, + DisambiguateChoices.lookup_num_by_dsc desc] + in + set_proof_aliases status diff + | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm -> + let status = add_lexicon_content [stm] status in + let uris = + List.map + (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri)) + (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern) + in + let diff = + [DisambiguateTypes.Symbol (symbol, 0), + DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] + in + let status = set_proof_aliases status diff in + let status = add_metadata uris status in + status + | LexiconAst.Notation _ as stm -> add_lexicon_content [stm] status + diff --git a/helm/ocaml/lexicon/lexiconEngine.mli b/helm/ocaml/lexicon/lexiconEngine.mli new file mode 100644 index 000000000..a2232fe28 --- /dev/null +++ b/helm/ocaml/lexicon/lexiconEngine.mli @@ -0,0 +1,40 @@ +(* 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/ + *) + + +type status = { + aliases: DisambiguateTypes.environment; (** disambiguation aliases *) + multi_aliases: DisambiguateTypes.multiple_environment; + lexicon_content_rev: LexiconMarshal.lexicon; + notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) + metadata: LibraryNoDb.metadata list; +} + +val eval_command : status -> LexiconAst.command -> status + +val set_proof_aliases: + status -> + (DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) list -> + status diff --git a/helm/ocaml/lexicon/lexiconMarshal.ml b/helm/ocaml/lexicon/lexiconMarshal.ml new file mode 100644 index 000000000..bd87a9521 --- /dev/null +++ b/helm/ocaml/lexicon/lexiconMarshal.ml @@ -0,0 +1,96 @@ +(* 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/ + *) + +exception Checksum_failure of string +exception Corrupt_lexicon of string +exception Version_mismatch of string + +type lexicon = LexiconAst.command list + +let marshal_flags = [] + +let rehash_cmd_uris = + let rehash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in + function + | LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) -> + let rec aux = + function + | CicNotationPt.UriPattern uri -> + CicNotationPt.UriPattern (rehash_uri uri) + | CicNotationPt.ApplPattern args -> + CicNotationPt.ApplPattern (List.map aux args) + | CicNotationPt.VarPattern _ + | CicNotationPt.ImplicitPattern as pat -> pat + in + let appl_pattern = aux cic_appl_pattern in + LexiconAst.Interpretation (loc, dsc, args, appl_pattern) + | LexiconAst.Notation _ + | LexiconAst.Alias _ as cmd -> cmd + | cmd -> + prerr_endline "Found a command not expected in a .lexicon:"; + prerr_endline (LexiconAstPp.pp_command cmd); + assert false + +(** .lexicon file format + * - an integer -- magic number -- denoting the version of the dumped data + * structure. Different magic numbers stand for incompatible data structures + * - an integer -- checksum -- denoting the hash value (computed with + * Hashtbl.hash) of the string representation of the dumped data structur + * - marshalled data: list of LexiconAst.command + *) + +let save_lexicon ~fname lexicon = + let ensure_path_exists path = + let dir = Filename.dirname path in + HExtlib.mkdir dir + in + ensure_path_exists fname; + let oc = open_out fname in + let marshalled = Marshal.to_string (List.rev lexicon) marshal_flags in + let checksum = Hashtbl.hash marshalled in + output_binary_int oc LexiconAst.magic; + output_binary_int oc checksum; + output_string oc marshalled; + close_out oc + +let load_lexicon ~fname = + let ic = open_in fname in + HExtlib.finally + (fun () -> close_in ic) + (fun () -> + try + let lexicon_magic = input_binary_int ic in + if lexicon_magic <> LexiconAst.magic then raise (Version_mismatch fname); + let lexicon_checksum = input_binary_int ic in + let marshalled = HExtlib.input_all ic in + let checksum = Hashtbl.hash marshalled in + if checksum <> lexicon_checksum then raise (Checksum_failure fname); + let (lexicon:lexicon) = + Marshal.from_string marshalled 0 + in + List.map rehash_cmd_uris lexicon + with End_of_file -> raise (Corrupt_lexicon fname)) + () + diff --git a/helm/ocaml/lexicon/lexiconMarshal.mli b/helm/ocaml/lexicon/lexiconMarshal.mli new file mode 100644 index 000000000..9ef291842 --- /dev/null +++ b/helm/ocaml/lexicon/lexiconMarshal.mli @@ -0,0 +1,37 @@ +(* 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/ + *) + + (** name of the corrupt .lexicon file *) +exception Checksum_failure of string +exception Corrupt_lexicon of string +exception Version_mismatch of string + +type lexicon = LexiconAst.command list + +val save_lexicon: fname:string -> lexicon -> unit + + (** @raise Corrupt_lexicon *) +val load_lexicon: fname:string -> lexicon + diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/lexicon/lexiconSync.ml similarity index 53% rename from helm/ocaml/grafite2/matitaSync.ml rename to helm/ocaml/lexicon/lexiconSync.ml index ee5d84278..b6d2270fe 100644 --- a/helm/ocaml/grafite2/matitaSync.ml +++ b/helm/ocaml/lexicon/lexiconSync.ml @@ -23,16 +23,12 @@ * http://helm.cs.unibo.it/ *) -open Printf - -open GrafiteTypes - let alias_diff ~from status = let module Map = DisambiguateTypes.Environment in Map.fold (fun domain_item (description1,_ as codomain_item) acc -> try - let description2,_ = Map.find domain_item from.aliases in + let description2,_ = Map.find domain_item from.LexiconEngine.aliases in if description1 <> description2 then (domain_item,codomain_item)::acc else @@ -40,44 +36,12 @@ let alias_diff ~from status = with Not_found -> (domain_item,codomain_item)::acc) - status.aliases [] + status.LexiconEngine.aliases [] let alias_diff = let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status -let set_proof_aliases status new_aliases = - let commands_of_aliases = - List.map - (fun alias -> GrafiteAst.Alias (DisambiguateTypes.dummy_floc, alias)) - in - let deps_of_aliases = - HExtlib.filter_map - (function - | GrafiteAst.Ident_alias (_, suri) -> - let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in - Some (LibraryNoDb.Dependency buri) - | _ -> None) - in - let aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) - status.aliases new_aliases in - let multi_aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) - status.multi_aliases new_aliases in - let new_status = - { status with multi_aliases = multi_aliases ; aliases = aliases} - in - if new_aliases = [] then - new_status - else - let aliases = - DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases - in - let status = add_moo_content (commands_of_aliases aliases) new_status in - let status = add_metadata (deps_of_aliases aliases) status in - status - (** given a uri and a type list (the contructors types) builds a list of pairs * (name,uri) that is used to generate automatic aliases **) let extract_alias types uri = @@ -99,12 +63,12 @@ let build_aliases = let add_aliases_for_inductive_def status types uri = let aliases = build_aliases (extract_alias types uri) in - set_proof_aliases status aliases + LexiconEngine.set_proof_aliases status aliases let add_alias_for_constant status uri = let name = UriManager.name_of_uri uri in let new_env = build_aliases [(name,uri)] in - set_proof_aliases status new_env + LexiconEngine.set_proof_aliases status new_env let add_aliases_for_object status uri = function @@ -114,41 +78,20 @@ let add_aliases_for_object status uri = | Cic.Variable _ | Cic.CurrentProof _ -> assert false -let add_obj uri obj lemmas status = - List.fold_left add_alias_for_constant - (add_aliases_for_object status uri obj) lemmas - -let add_obj = - let profiler = HExtlib.profile "add_obj" in - fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status - -let add_coercion status uri compounds = - let status = {status with coercions = uri :: status.coercions} in - List.fold_left add_alias_for_constant status compounds +let add_aliases_for_objs = + List.fold_left + (fun status uri -> + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + add_aliases_for_object status uri obj) -module OrderedUri = -struct - type t = UriManager.uri * string - let compare (u1, _) (u2, _) = UriManager.compare u1 u2 -end - module OrderedId = struct type t = CicNotation.notation_id let compare = Pervasives.compare end -module UriSet = Set.Make (OrderedUri) module IdSet = Set.Make (OrderedId) - (** @return l2 \ l1 *) -let uri_list_diff l2 l1 = - let module S = UriManager.UriSet in - let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in - let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in - let diff = S.diff s2 s1 in - S.fold (fun uri uris -> uri :: uris) diff [] - (** @return l2 \ l1 *) let id_list_diff l2 l1 = let module S = IdSet in @@ -158,31 +101,17 @@ let id_list_diff l2 l1 = S.fold (fun uri uris -> uri :: uris) diff [] let time_travel ~present ~past = - let objs_to_remove = uri_list_diff present.objects past.objects in - let coercions_to_remove = uri_list_diff present.coercions past.coercions in let notation_to_remove = - id_list_diff present.notation_ids past.notation_ids + id_list_diff present.LexiconEngine.notation_ids + past.LexiconEngine.notation_ids in - let debug_list = ref [] in - List.iter - (fun uri -> LibrarySync.remove_coercion uri) - coercions_to_remove; - List.iter LibrarySync.remove_obj objs_to_remove; - List.iter CicNotation.remove_notation notation_to_remove + List.iter CicNotation.remove_notation notation_to_remove -let init () = - LibrarySync.remove_all_coercions (); - LibraryObjects.reset_defaults (); +let init = { - aliases = DisambiguateTypes.Environment.empty; + LexiconEngine.aliases = DisambiguateTypes.Environment.empty; multi_aliases = DisambiguateTypes.Environment.empty; - moo_content_rev = []; - metadata = []; - proof_status = No_proof; - options = no_options; - objects = []; - coercions = []; + lexicon_content_rev = []; notation_ids = []; + metadata = []; } - - diff --git a/helm/ocaml/grafite2/matitaSync.mli b/helm/ocaml/lexicon/lexiconSync.mli similarity index 68% rename from helm/ocaml/grafite2/matitaSync.mli rename to helm/ocaml/lexicon/lexiconSync.mli index bc744f862..62d8b97f5 100644 --- a/helm/ocaml/grafite2/matitaSync.mli +++ b/helm/ocaml/lexicon/lexiconSync.mli @@ -23,32 +23,18 @@ * http://helm.cs.unibo.it/ *) -val add_obj: - UriManager.uri -> Cic.obj -> UriManager.uri list -> - GrafiteTypes.status -> GrafiteTypes.status - -val add_coercion: - GrafiteTypes.status -> UriManager.uri -> UriManager.uri list -> - GrafiteTypes.status +val add_aliases_for_objs: + LexiconEngine.status -> UriManager.uri list -> LexiconEngine.status val time_travel: - present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit + present:LexiconEngine.status -> past:LexiconEngine.status -> unit (** perform a diff between the aliases contained in two statuses, assuming * that the second one can only have more aliases than the first one * @return the list of aliases that should be added to aliases of from in * order to be equal to aliases of the second argument *) val alias_diff: - from:GrafiteTypes.status -> GrafiteTypes.status -> + from:LexiconEngine.status -> LexiconEngine.status -> (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list - (** set the proof aliases enriching the moo_content *) -val set_proof_aliases : - GrafiteTypes.status -> - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> - GrafiteTypes.status - - (* also resets the imperative part of the status *) -val init: unit -> GrafiteTypes.status - - +val init: LexiconEngine.status diff --git a/helm/ocaml/library/libraryClean.ml b/helm/ocaml/library/libraryClean.ml index 00f2c4ef0..5da9507fc 100644 --- a/helm/ocaml/library/libraryClean.ml +++ b/helm/ocaml/library/libraryClean.ml @@ -145,7 +145,7 @@ let moo_root_dir = lazy ( String.sub url 7 (String.length url - 7) (* remove heading "file:///" *) ) -let close_nodb buris = +let close_nodb ~basedir buris = let rev_deps = Hashtbl.create 97 in let all_moos = HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo") @@ -154,19 +154,17 @@ let close_nodb buris = List.iter (fun path -> let metadata = LibraryNoDb.load_metadata ~fname:path in - let baseuri_of_current_moo = - let rec aux = function - | [] -> assert false - | LibraryNoDb.Baseuri buri::_ -> buri - | _ :: tl -> aux tl - in - aux metadata + let baseuri_of_current_moo = + let dirname = Filename.chop_extension (Filename.dirname path) in + let basedirlen = String.length basedir in + assert (String.sub dirname 0 basedirlen = basedir); + "cic:" ^ + String.sub dirname basedirlen (String.length dirname - basedirlen) ^ + Filename.basename path in let deps = HExtlib.filter_map - (function - | LibraryNoDb.Dependency buri -> Some buri - | _ -> None ) + (function LibraryNoDb.Dependency buri -> Some buri) metadata in List.iter @@ -198,7 +196,7 @@ let clean_baseuris ?(verbose=true) ~basedir buris = List.iter debug_prerr buris; let l = if Helm_registry.get_bool "db.nodb" then - close_nodb buris + close_nodb ~basedir buris else close_db [] buris in @@ -209,7 +207,9 @@ let clean_baseuris ?(verbose=true) ~basedir buris = List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; List.iter (fun buri -> - HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri)) + HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri); + HExtlib.safe_remove (LibraryMisc.metadata_file_of_baseuri basedir buri); + HExtlib.safe_remove (LibraryMisc.lexicon_file_of_baseuri basedir buri)) (HExtlib.list_uniq (List.fast_sort Pervasives.compare (List.map (UriManager.buri_of_uri) l))); List.iter diff --git a/helm/ocaml/library/libraryMisc.ml b/helm/ocaml/library/libraryMisc.ml index e953859b6..7911789e2 100644 --- a/helm/ocaml/library/libraryMisc.ml +++ b/helm/ocaml/library/libraryMisc.ml @@ -27,6 +27,10 @@ let obj_file_of_baseuri ~basedir ~baseuri = let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in path ^ ".moo" +let lexicon_file_of_baseuri ~basedir ~baseuri = + let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in + path ^ ".lexicon" + let metadata_file_of_baseuri ~basedir ~baseuri = let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in path ^ ".metadata" diff --git a/helm/ocaml/library/libraryMisc.mli b/helm/ocaml/library/libraryMisc.mli index 03a4742c5..e4d07faf7 100644 --- a/helm/ocaml/library/libraryMisc.mli +++ b/helm/ocaml/library/libraryMisc.mli @@ -24,5 +24,5 @@ *) val obj_file_of_baseuri: basedir:string -> baseuri:string -> string +val lexicon_file_of_baseuri: basedir:string -> baseuri:string -> string val metadata_file_of_baseuri: basedir:string -> baseuri:string -> string - diff --git a/helm/ocaml/library/libraryNoDb.ml b/helm/ocaml/library/libraryNoDb.ml index 12a2e96da..0a03a4a7e 100644 --- a/helm/ocaml/library/libraryNoDb.ml +++ b/helm/ocaml/library/libraryNoDb.ml @@ -33,7 +33,6 @@ let magic = 1 type metadata = | Dependency of string (* baseuri without trailing slash *) - | Baseuri of string let eq_metadata (m1:metadata) (m2:metadata) = m1 = m2 @@ -48,13 +47,18 @@ let marshal_flags = [] *) let save_metadata ~fname metadata = - let oc = open_out fname in - let marshalled = Marshal.to_string metadata marshal_flags in - let checksum = Hashtbl.hash marshalled in - output_binary_int oc magic; - output_binary_int oc checksum; - output_string oc marshalled; - close_out oc + let ensure_path_exists path = + let dir = Filename.dirname path in + HExtlib.mkdir dir + in + ensure_path_exists fname; + let oc = open_out fname in + let marshalled = Marshal.to_string metadata marshal_flags in + let checksum = Hashtbl.hash marshalled in + output_binary_int oc magic; + output_binary_int oc checksum; + output_string oc marshalled; + close_out oc let load_metadata ~fname = let ic = open_in fname in diff --git a/helm/ocaml/library/libraryNoDb.mli b/helm/ocaml/library/libraryNoDb.mli index 33b1b1eb3..1521f456f 100644 --- a/helm/ocaml/library/libraryNoDb.mli +++ b/helm/ocaml/library/libraryNoDb.mli @@ -27,7 +27,6 @@ * support their format *) type metadata = | Dependency of string (* baseuri without trailing slash *) - | Baseuri of string val eq_metadata: metadata -> metadata -> bool diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index 2690349bc..1ccc9d30f 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -251,7 +251,7 @@ let generate_elimination_principles ~basedir uri = List.iter remove_single_obj !uris; raise exn -(* COERICONS ***********************************************************) +(* COERCIONS ***********************************************************) let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; diff --git a/helm/ocaml/patch_deps.sh b/helm/ocaml/patch_deps.sh index 2abbbeab1..cd9f09c89 100755 --- a/helm/ocaml/patch_deps.sh +++ b/helm/ocaml/patch_deps.sh @@ -1,7 +1,10 @@ #!/bin/sh # script args: source_file target_file -use_clusters='yes' +use_clusters='no' +if [ ! -z "$USE_CLUSTERS" ]; then + use_clusters=$USE_CLUSTERS +fi # args: file snippet # file will be modified in place diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 5d1ceb1d0..95131ecf4 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -17,6 +17,7 @@ ring.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi +tactics.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli index 895a799dc..1d60ae149 100644 --- a/helm/ocaml/tactics/equalityTactics.mli +++ b/helm/ocaml/tactics/equalityTactics.mli @@ -33,7 +33,7 @@ val rewrite_simpl_tac: val replace_tac: pattern:ProofEngineTypes.lazy_pattern -> - with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic + with_what:Cic.lazy_term -> ProofEngineTypes.tactic val reflexivity_tac: ProofEngineTypes.tactic val symmetry_tac: ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index bb0603056..bb6390bdc 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -475,7 +475,7 @@ exception Fail of string Lazy.t * @raise Bad_pattern * *) let select ~metasenv ~ugraph ~conjecture:(_,context,ty) - ~(pattern: (Cic.term, ProofEngineTypes.lazy_term) ProofEngineTypes.pattern) + ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern) = let what, hyp_patterns, goal_pattern = pattern in let find_pattern_for name = diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 6e532a807..7497da7ed 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -58,10 +58,6 @@ let mk_tactic t = t type reduction = Cic.context -> Cic.term -> Cic.term -type lazy_term = - Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> - Cic.term * Cic.metasenv * CicUniv.universe_graph - let const_lazy_term t = (fun _ metasenv ugraph -> t, metasenv, ugraph) @@ -75,7 +71,7 @@ let const_lazy_reduction red = type ('term, 'lazy_term) pattern = 'lazy_term option * (string * 'term) list * 'term option -type lazy_pattern = (Cic.term, lazy_term) pattern +type lazy_pattern = (Cic.term, Cic.lazy_term) pattern let conclusion_pattern t = let t' = diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli index d50707f73..4396ea78f 100644 --- a/helm/ocaml/tactics/proofEngineTypes.mli +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -46,11 +46,7 @@ val mk_tactic: (status -> proof * goal list) -> tactic type reduction = Cic.context -> Cic.term -> Cic.term -type lazy_term = - Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> - Cic.term * Cic.metasenv * CicUniv.universe_graph - -val const_lazy_term: Cic.term -> lazy_term +val const_lazy_term: Cic.term -> Cic.lazy_term type lazy_reduction = Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> @@ -62,7 +58,7 @@ val const_lazy_reduction: reduction -> lazy_reduction type ('term, 'lazy_term) pattern = 'lazy_term option * (string * 'term) list * 'term option -type lazy_pattern = (Cic.term, lazy_term) pattern +type lazy_pattern = (Cic.term, Cic.lazy_term) pattern (** conclusion_pattern [t] returns the pattern (t,[],%) *) val conclusion_pattern : Cic.term option -> lazy_pattern diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index 153cb6f28..16e2bc23c 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -30,18 +30,18 @@ val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tac (* The default of term is the thesis of the goal to be prooved *) val unfold_tac: - ProofEngineTypes.lazy_term option -> + Cic.lazy_term option -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val change_tac: pattern:ProofEngineTypes.lazy_pattern -> - ProofEngineTypes.lazy_term -> + Cic.lazy_term -> ProofEngineTypes.tactic val fold_tac: reduction:ProofEngineTypes.lazy_reduction -> - term:ProofEngineTypes.lazy_term -> + term:Cic.lazy_term -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 519a7407d..25e479b47 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -9,7 +9,7 @@ val auto : ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic val change : pattern:ProofEngineTypes.lazy_pattern -> - ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic + Cic.lazy_term -> ProofEngineTypes.tactic val clear : hyp:string -> ProofEngineTypes.tactic val clearbody : hyp:string -> ProofEngineTypes.tactic val compare : term:Cic.term -> ProofEngineTypes.tactic @@ -38,7 +38,7 @@ val exists : ProofEngineTypes.tactic val fail : ProofEngineTypes.tactic val fold : reduction:ProofEngineTypes.lazy_reduction -> - term:ProofEngineTypes.lazy_term -> + term:Cic.lazy_term -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val fourier : ProofEngineTypes.tactic val fwd_simpl : @@ -68,7 +68,7 @@ val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic val replace : pattern:ProofEngineTypes.lazy_pattern -> - with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic + with_what:Cic.lazy_term -> ProofEngineTypes.tactic val rewrite : direction:[ `LeftToRight | `RightToLeft ] -> pattern:ProofEngineTypes.lazy_pattern -> @@ -85,6 +85,6 @@ val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic val unfold : - ProofEngineTypes.lazy_term option -> + Cic.lazy_term option -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -- 2.39.2