From: Claudio Sacerdoti Coen Date: Wed, 21 Dec 2005 13:49:21 +0000 (+0000) Subject: Huge reorganization of matita and ocaml. X-Git-Tag: make_still_working~7978 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8;p=helm.git 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 --- 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/cicNotation.ml b/helm/ocaml/grafite/cicNotation.ml deleted file mode 100644 index 9500a8e11..000000000 --- a/helm/ocaml/grafite/cicNotation.ml +++ /dev/null @@ -1,81 +0,0 @@ -(* 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 GrafiteAst - -type notation_id = - | RuleId of CicNotationParser.rule_id - | InterpretationId of TermAcicContent.interpretation_id - | PrettyPrinterId of TermContentPres.pretty_printer_id - -let process_notation st = - match st with - | Notation (loc, dir, l1, associativity, precedence, l2) -> - let rule_id = - if dir <> Some `RightToLeft then - [ RuleId (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> - CicNotationPt.AttributedTerm - (`Loc loc,TermContentPres.instantiate_level2 env l2))) ] - else - [] - in - let pp_id = - if dir <> Some `LeftToRight then - [ PrettyPrinterId - (TermContentPres.add_pretty_printer ?precedence ?associativity - l2 l1) ] - else - [] - in - st, 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, [] - -let remove_notation = function - | RuleId id -> CicNotationParser.delete id - | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id - | InterpretationId id -> TermAcicContent.remove_interpretation id - -let get_all_notations () = - List.map - (fun (interp_id, dsc) -> - InterpretationId interp_id, "interpretation: " ^ dsc) - (TermAcicContent.get_all_interpretations ()) - -let get_active_notations () = - List.map (fun id -> InterpretationId id) - (TermAcicContent.get_active_interpretations ()) - -let set_active_notations ids = - let interp_ids = - HExtlib.filter_map - (function InterpretationId interp_id -> Some interp_id | _ -> None) - ids - in - TermAcicContent.set_active_interpretations interp_ids - diff --git a/helm/ocaml/grafite/cicNotation.mli b/helm/ocaml/grafite/cicNotation.mli deleted file mode 100644 index 9eb98c1d3..000000000 --- a/helm/ocaml/grafite/cicNotation.mli +++ /dev/null @@ -1,41 +0,0 @@ -(* 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 notation_id - -val process_notation: - 'obj GrafiteAst.command -> 'obj GrafiteAst.command * notation_id list - -val remove_notation: notation_id -> unit - -(** {2 Notation enabling/disabling} - * Right now, only disabling of notation during pretty printing is supporting. - * If it is useful to disable it also for the input phase is still to be - * understood ... *) - -val get_all_notations: unit -> (notation_id * string) list (* id, dsc *) -val get_active_notations: unit -> notation_id list -val set_active_notations: notation_id list -> unit - 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/grafite2/disambiguatePp.ml b/helm/ocaml/grafite2/disambiguatePp.ml deleted file mode 100644 index 733179589..000000000 --- a/helm/ocaml/grafite2/disambiguatePp.ml +++ /dev/null @@ -1,51 +0,0 @@ -(* 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 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) - -let aliases_of_environment env = - Environment.fold - (fun domain_item codomain_item acc -> - alias_of_domain_and_codomain_items domain_item codomain_item::acc - ) env [] - -let aliases_of_domain_and_codomain_items_list l = - List.fold_left - (fun acc (domain_item,codomain_item) -> - alias_of_domain_and_codomain_items domain_item codomain_item::acc - ) [] l - -let pp_environment env = - let aliases = aliases_of_environment env in - let strings = - List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases - in - String.concat "\n" (List.sort compare strings) diff --git a/helm/ocaml/grafite2/disambiguatePp.mli b/helm/ocaml/grafite2/disambiguatePp.mli deleted file mode 100644 index 516dfee17..000000000 --- a/helm/ocaml/grafite2/disambiguatePp.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val aliases_of_domain_and_codomain_items_list: - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> - GrafiteAst.alias_spec list - -val pp_environment: DisambiguateTypes.environment -> string diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml deleted file mode 100644 index 4a851e77b..000000000 --- a/helm/ocaml/grafite2/grafiteEngine.ml +++ /dev/null @@ -1,744 +0,0 @@ -(* 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 Drop -exception IncludedFileNotCompiled of string (* file name *) -exception MetadataNotFound of string (* file name *) - -type options = { - do_heavy_checks: bool ; - clean_baseuri: bool -} - -(** create a ProofEngineTypes.mk_fresh_name_type function which uses given - * names as long as they are available, then it fallbacks to name generation - * using FreshNamesGenerator module *) -let namer_of names = - let len = List.length names in - let count = ref 0 in - fun metasenv context name ~typ -> - if !count < len then begin - let name = Cic.Name (List.nth names !count) in - incr count; - name - end else - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ - -let tactic_of_ast ast = - let module PET = ProofEngineTypes in - match ast with - | GrafiteAst.Absurd (_, term) -> Tactics.absurd term - | GrafiteAst.Apply (_, term) -> Tactics.apply term - | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width,paramodulation,full) -> - AutoTactic.auto_tac ?depth ?width ?paramodulation ?full - ~dbd:(LibraryDb.instance ()) () - | GrafiteAst.Change (_, pattern, with_what) -> - Tactics.change ~pattern with_what - | GrafiteAst.Clear (_,id) -> Tactics.clear id - | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id - | GrafiteAst.Contradiction _ -> Tactics.contradiction - | GrafiteAst.Compare (_, term) -> Tactics.compare term - | GrafiteAst.Constructor (_, n) -> Tactics.constructor n - | GrafiteAst.Cut (_, ident, term) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.cut ~mk_fresh_name_callback:(namer_of names) term - | GrafiteAst.DecideEquality _ -> Tactics.decide_equality - | GrafiteAst.Decompose (_, types, what, names) -> - let to_type = function - | GrafiteAst.Type (uri, typeno) -> uri, typeno - | GrafiteAst.Ident _ -> assert false - in - let user_types = List.rev_map to_type types in - let dbd = LibraryDb.instance () in - let mk_fresh_name_callback = namer_of names in - Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what - | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term - | GrafiteAst.Elim (_, what, using, depth, names) -> - Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) - what - | GrafiteAst.ElimType (_, what, using, depth, names) -> - Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) - what - | GrafiteAst.Exact (_, term) -> Tactics.exact term - | GrafiteAst.Exists _ -> Tactics.exists - | GrafiteAst.Fail _ -> Tactics.fail - | GrafiteAst.Fold (_, reduction_kind, term, pattern) -> - let reduction = - match reduction_kind with - | `Normalize -> - PET.const_lazy_reduction - (CicReduction.normalize ~delta:false ~subst:[]) - | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce - | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl - | `Unfold None -> - PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None) - | `Unfold (Some lazy_term) -> - (fun context metasenv ugraph -> - let what, metasenv, ugraph = lazy_term context metasenv ugraph in - ProofEngineReduction.unfold ~what, metasenv, ugraph) - | `Whd -> - PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[]) - in - Tactics.fold ~reduction ~term ~pattern - | GrafiteAst.Fourier _ -> Tactics.fourier - | GrafiteAst.FwdSimpl (_, hyp, names) -> - Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) - ~dbd:(LibraryDb.instance ()) hyp - | GrafiteAst.Generalize (_,pattern,ident) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern - | GrafiteAst.Goal (_, n) -> Tactics.set_goal n - | GrafiteAst.IdTac _ -> Tactics.id - | GrafiteAst.Injection (_,term) -> Tactics.injection term - | GrafiteAst.Intros (_, None, names) -> - PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () - | GrafiteAst.Intros (_, Some num, names) -> - PrimitiveTactics.intros_tac ~howmany:num - ~mk_fresh_name_callback:(namer_of names) () - | GrafiteAst.Inversion (_, term) -> - Tactics.inversion term - | GrafiteAst.LApply (_, how_many, to_what, what, ident) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many - ~to_what what - | GrafiteAst.Left _ -> Tactics.left - | GrafiteAst.LetIn (loc,term,name) -> - Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) - | GrafiteAst.Reduce (_, reduction_kind, pattern) -> - (match reduction_kind with - | `Normalize -> Tactics.normalize ~pattern - | `Reduce -> Tactics.reduce ~pattern - | `Simpl -> Tactics.simpl ~pattern - | `Unfold what -> Tactics.unfold ~pattern what - | `Whd -> Tactics.whd ~pattern) - | GrafiteAst.Reflexivity _ -> Tactics.reflexivity - | GrafiteAst.Replace (_, pattern, with_what) -> - Tactics.replace ~pattern ~with_what - | GrafiteAst.Rewrite (_, direction, t, pattern) -> - EqualityTactics.rewrite_tac ~direction ~pattern t - | GrafiteAst.Right _ -> Tactics.right - | GrafiteAst.Ring _ -> Tactics.ring - | GrafiteAst.Split _ -> Tactics.split - | GrafiteAst.Symmetry _ -> Tactics.symmetry - | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term - -(* maybe we only need special cases for apply and goal *) -let classify_tactic tactic = - match tactic with - (* tactics that can't close the goal (return a goal we want to "select") *) - | GrafiteAst.Rewrite _ - | GrafiteAst.Split _ - | GrafiteAst.Replace _ - | GrafiteAst.Reduce _ - | GrafiteAst.Injection _ - | GrafiteAst.IdTac _ - | GrafiteAst.Generalize _ - | GrafiteAst.Elim _ - | GrafiteAst.Cut _ - | GrafiteAst.Decompose _ -> true, true - (* tactics we don't want to reorder goals. I think only Goal needs this. *) - | GrafiteAst.Goal _ -> false, true - (* tactics like apply *) - | _ -> true, false - -let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= - let module PEH = ProofEngineHelpers in -(* let print_m name metasenv = - prerr_endline (">>>>> " ^ name); - prerr_endline (CicMetaSubst.ppmetasenv [] metasenv) - in *) - (* phase one calculates: - * new_goals_from_refine: goals added by refine - * head_goal: the first goal opened by ythe tactic - * other_goals: other goals opened by the tactic - *) - let new_goals_from_refine = PEH.compare_metasenvs start refine in - let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in - let head_goal, other_goals, goals = - match goals with - | [] -> None,[],goals - | hd::tl -> - (* assert (List.mem hd new_goals_from_tactic); - * invalidato dalla goal_tac - * *) - Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>) - hd) goals - in - let produced_goals = - match head_goal with - | None -> new_goals_from_refine @ other_goals - | Some x -> x :: new_goals_from_refine @ other_goals - in - (* extract the metas generated by refine and tactic *) - let metas_for_tactic_head = - match head_goal with - | None -> [] - | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in - let metas_for_tactic_goals = - List.map - (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic) - goals - in - let metas_for_refine_goals = - List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in - let produced_metas, goals = - let produced_metas = - if always_opens_a_goal then - metas_for_tactic_head @ metas_for_refine_goals @ - metas_for_tactic_goals - else begin -(* print_m "metas_for_refine_goals" metas_for_refine_goals; - print_m "metas_for_tactic_head" metas_for_tactic_head; - print_m "metas_for_tactic_goals" metas_for_tactic_goals; *) - metas_for_refine_goals @ metas_for_tactic_head @ - metas_for_tactic_goals - end - in - let goals = List.map (fun (metano, _, _) -> metano) produced_metas in - produced_metas, goals - in - (* residual metas, preserving the original order *) - let before, after = - let rec split e = - function - | [] -> [],[] - | (metano, _, _) :: tl when metano = e -> - [], List.map (fun (x,_,_) -> x) tl - | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a - in - let find n metasenv = - try - Some (List.find (fun (metano, _, _) -> metano = n) metasenv) - with Not_found -> None - in - let extract l = - List.fold_right - (fun n acc -> - match find n tactic with - | Some x -> x::acc - | None -> acc - ) l [] in - let before_l, after_l = split current_goal start in - let before_l = - List.filter (fun x -> not (List.mem x produced_goals)) before_l in - let after_l = - List.filter (fun x -> not (List.mem x produced_goals)) after_l in - let before = extract before_l in - let after = extract after_l in - before, after - in -(* |+ DEBUG CODE +| - print_m "BEGIN" start; - prerr_endline ("goal was: " ^ string_of_int current_goal); - prerr_endline ("and metas from refine are:"); - List.iter - (fun t -> prerr_string (" " ^ string_of_int t)) - new_goals_from_refine; - prerr_endline ""; - print_m "before" before; - print_m "metas_for_tactic_head" metas_for_tactic_head; - print_m "metas_for_refine_goals" metas_for_refine_goals; - print_m "metas_for_tactic_goals" metas_for_tactic_goals; - print_m "produced_metas" produced_metas; - print_m "after" after; -|+ FINE DEBUG CODE +| *) - before @ produced_metas @ after, goals - -let apply_tactic ~disambiguate_tactic tactic (status, goal) = -(* prerr_endline "apply_tactic"; *) -(* prerr_endline (Continuationals.Stack.pp (GrafiteTypes.get_stack status)); *) - 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 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 ... *) -(* prerr_endline "apply_tactic bassa"; *) - let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in - let after = ProofEngineTypes.goals_of_proof proof in - let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in -(* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before)); -prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after)); -prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *) -(* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals)); -prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *) - let proof, opened_goals = - if needs_reordering then begin - let uri, metasenv_after_tactic, t, ty = proof in -(* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *) - let reordered_metasenv, opened_goals = - reorder_metasenv - starting_metasenv - metasenv_after_refinement metasenv_after_tactic - opened goal always_opens_a_goal - in - let proof' = uri, reordered_metasenv, t, ty in -(* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *) - proof', opened_goals - end - else - proof, opened_goals - in - let incomplete_proof = - match !status_ref.GrafiteTypes.proof_status with - | GrafiteTypes.Incomplete_proof p -> p - | _ -> assert false - in - { !status_ref with GrafiteTypes.proof_status = - GrafiteTypes.Incomplete_proof - { incomplete_proof with GrafiteTypes.proof = proof } }, - opened_goals, closed_goals - -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) -> - - disambiguate_command: - (GrafiteTypes.status -> - 'obj GrafiteAst.command -> - GrafiteTypes.status * Cic.obj GrafiteAst.command) -> - - ?do_heavy_checks:bool -> - ?clean_baseuri:bool -> - GrafiteTypes.status -> - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> - GrafiteTypes.status - } - -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 - } - -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) -> - - disambiguate_command: - (GrafiteTypes.status -> - 'obj GrafiteAst.command -> - GrafiteTypes.status * Cic.obj GrafiteAst.command) -> - - options -> - GrafiteTypes.status -> - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code -> GrafiteTypes.status - } - -type 'a eval_from_moo = { efm_go: GrafiteTypes.status ref -> string -> unit } - -let coercion_moo_statement_of uri = - GrafiteAst.Coercion (DisambiguateTypes.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 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} - -let eval_tactical ~disambiguate_tactic status tac = - let apply_tactic = apply_tactic ~disambiguate_tactic in - let module MatitaStatus = - struct - type input_status = GrafiteTypes.status * ProofEngineTypes.goal - - type output_status = - GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list - - type tactic = input_status -> output_status - - let id_tactic = apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) - let mk_tactic tac = tac - let apply_tactic tac = tac - let goals (_, opened, closed) = opened, closed - let set_goals (opened, closed) (status, _, _) = (status, opened, closed) - let get_stack (status, _) = GrafiteTypes.get_stack status - - let set_stack stack (status, opened, closed) = - GrafiteTypes.set_stack stack status, opened, closed - - let inject (status, _) = (status, [], []) - let focus goal (status, _, _) = (status, goal) - end - in - let module MatitaTacticals = Tacticals.Make (MatitaStatus) in - let rec tactical_of_ast l tac = - match tac with - | GrafiteAst.Tactic (loc, tactic) -> - MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic)) - | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) - assert (l > 0); - MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals) - | GrafiteAst.Do (loc, n, tactical) -> - MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical) - | GrafiteAst.Repeat (loc, tactical) -> - MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical) - | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) - assert (l > 0); - MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical) - ~continuations:(List.map (tactical_of_ast (l+1)) tacticals) - | GrafiteAst.First (loc, tacticals) -> - MatitaTacticals.first - ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals) - | GrafiteAst.Try (loc, tactical) -> - MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical) - | GrafiteAst.Solve (loc, tacticals) -> - MatitaTacticals.solve_tactics - ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals) - - | GrafiteAst.Skip loc -> MatitaTacticals.skip - | GrafiteAst.Dot loc -> MatitaTacticals.dot - | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon - | GrafiteAst.Branch loc -> MatitaTacticals.branch - | GrafiteAst.Shift loc -> MatitaTacticals.shift - | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i - | GrafiteAst.Merge loc -> MatitaTacticals.merge - | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals - | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus - in - let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in - let status = (* is proof completed? *) - match status.GrafiteTypes.proof_status with - | GrafiteTypes.Incomplete_proof - { GrafiteTypes.stack = stack; proof = proof } - when Continuationals.Stack.is_empty stack -> - { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof } - | _ -> status - in - status - -let eval_comment status c = status - -(* since the record syntax allows to declare coercions, we have to put this - * information inside the moo *) -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 - | Some fields -> - let is_a_coercion uri = - try - let obj,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in - let attrs = CicUtil.attributes_of_obj obj in - List.mem (`Class `Projection) attrs - with Not_found -> assert false - in - (* looking at the fields we can know the 'wanted' coercions, but not the - * actually generated ones. So, only the intersection between the wanted - * and the actual should be in the moo as coercion, while everithing in - * lemmas should go as aliases *) - let wanted_coercions = - HExtlib.filter_map - (function - | (name,true) -> - Some - (UriManager.uri_of_string - (GrafiteTypes.qualify status name ^ ".con")) - | _ -> None) - fields - in - prerr_endline "wanted coercions:"; - List.iter - (fun u -> prerr_endline (UriManager.string_of_uri u)) - wanted_coercions; - let coercions, moo_content = - List.split - (HExtlib.filter_map - (fun uri -> - let is_a_wanted_coercion = - List.exists (UriManager.eq uri) wanted_coercions in - if is_a_coercion uri && is_a_wanted_coercion then - Some (uri, coercion_moo_statement_of uri) - else - None) - lemmas) - in - List.iter - (fun u -> prerr_endline (UriManager.string_of_uri u)) - coercions; - let status = GrafiteTypes.add_moo_content moo_content status in - List.fold_left - (fun status uri -> - MatitaSync.add_coercion status uri []) - 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 - 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 - 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 - 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 - | 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 - | GrafiteAst.Drop loc -> raise Drop - | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty = - match status.GrafiteTypes.proof_status with - | GrafiteTypes.Proof (Some uri, metasenv, body, ty) -> - uri, metasenv, body, ty - | GrafiteTypes.Proof (None, metasenv, body, ty) -> - raise (GrafiteTypes.Command_error - ("Someone allows to start a theorem without giving the "^ - "name/uri. This should be fixed!")) - | _-> - raise - (GrafiteTypes.Command_error "You can't Qed an incomplete theorem") - in - if metasenv <> [] then - raise - (GrafiteTypes.Command_error - "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} - | 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 - Cic.Constant (name,_,_,_,_) - | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name - | Cic.InductiveDefinition (types,_,_,_) -> - ".ind", - (match types with (name,_,_,_)::_ -> name | _ -> assert false) - | _ -> assert false in - let uri = - UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) - in - let metasenv = GrafiteTypes.get_proof_metasenv status in - match obj with - | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> - let name = UriManager.name_of_uri uri in - if not(CicPp.check name ty) then - HLog.error ("Bad name: " ^ name); - if opts.do_heavy_checks then - begin - let dbd = LibraryDb.instance () in - let similar = Whelp.match_term ~dbd ty in - let similar_len = List.length similar in - if similar_len> 30 then - (HLog.message - ("Duplicate check will compare your theorem with " ^ - string_of_int similar_len ^ - " theorems, this may take a while.")); - let convertible = - List.filter ( - fun u -> - let t = CicUtil.term_of_uri u in - let ty',g = - CicTypeChecker.type_of_aux' - metasenv' [] t CicUniv.empty_ugraph - in - fst(CicReduction.are_convertible [] ty' ty g)) - similar - in - (match convertible with - | [] -> () - | x::_ -> - HLog.warn - ("Theorem already proved: " ^ UriManager.string_of_uri x ^ - "\nPlease use a variant.")); - end; - assert (metasenv = metasenv'); - let goalno = - match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false - in - let initial_proof = (Some uri, metasenv, bo, ty) in - let initial_stack = Continuationals.Stack.of_metasenv metasenv in - { status with GrafiteTypes.proof_status = - GrafiteTypes.Incomplete_proof - { 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} - -} and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex -> - match ex with - | GrafiteAst.Tactical (_, tac, None) -> - eval_tactical ~disambiguate_tactic status tac - | GrafiteAst.Tactical (_, tac, Some punct) -> - let status = eval_tactical ~disambiguate_tactic status tac in - eval_tactical ~disambiguate_tactic status punct - | GrafiteAst.Command (_, cmd) -> - eval_command.ec_go ~baseuri_of_script ~disambiguate_command - opts status cmd - | GrafiteAst.Macro (_, mac) -> -(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO - raise (Command_error - (Printf.sprintf "The macro %s can't be in a script" - (GrafiteAstPp.pp_macro_ast mac))) -*) assert false - -} and eval_from_moo = {efm_go = fun status fname -> - let ast_of_cmd cmd = - GrafiteAst.Executable (DisambiguateTypes.dummy_floc, - GrafiteAst.Command (DisambiguateTypes.dummy_floc, - cmd)) - in - let moo = GrafiteMarshal.load_moo fname in - List.iter - (fun 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) - ~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 - st --> - let opts = { - do_heavy_checks = do_heavy_checks ; - clean_baseuri = clean_baseuri } - in - match st with - | GrafiteAst.Executable (_,ex) -> - eval_executable.ee_go ~baseuri_of_script ~disambiguate_tactic - ~disambiguate_command opts status ex - | 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/grafite2/grafiteEngine.mli deleted file mode 100644 index ccdc306c2..000000000 --- a/helm/ocaml/grafite2/grafiteEngine.mli +++ /dev/null @@ -1,48 +0,0 @@ -(* 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 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) -> - - disambiguate_command: - (GrafiteTypes.status -> - 'obj GrafiteAst.command -> - GrafiteTypes.status * Cic.obj GrafiteAst.command) -> - - ?do_heavy_checks:bool -> - ?clean_baseuri:bool -> - GrafiteTypes.status -> - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> - GrafiteTypes.status diff --git a/helm/ocaml/grafite2/grafiteMisc.ml b/helm/ocaml/grafite2/grafiteMisc.ml deleted file mode 100644 index 227cd382b..000000000 --- a/helm/ocaml/grafite2/grafiteMisc.ml +++ /dev/null @@ -1,31 +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/ - *) - -let is_empty buri = - List.for_all - (function - Http_getter_types.Ls_section _ -> true - | Http_getter_types.Ls_object _ -> false) - (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/")) diff --git a/helm/ocaml/grafite2/grafiteMisc.mli b/helm/ocaml/grafite2/grafiteMisc.mli deleted file mode 100644 index 833bb6360..000000000 --- a/helm/ocaml/grafite2/grafiteMisc.mli +++ /dev/null @@ -1,27 +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/ - *) - - (** check whether no objects are defined below a given baseuri *) -val is_empty: string -> bool diff --git a/helm/ocaml/grafite2/grafiteTypes.ml b/helm/ocaml/grafite2/grafiteTypes.ml deleted file mode 100644 index c73e8bd3c..000000000 --- a/helm/ocaml/grafite2/grafiteTypes.ml +++ /dev/null @@ -1,222 +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 Option_error of string * string -exception Statement_error of string -exception Command_error of string - -let command_error msg = raise (Command_error msg) - -type incomplete_proof = { - proof: ProofEngineTypes.proof; - stack: Continuationals.Stack.t; -} - -type proof_status = - | No_proof - | Incomplete_proof of incomplete_proof - | Proof of ProofEngineTypes.proof - | Intermediate of Cic.metasenv - (* Status in which the proof could be while it is being processed by the - * engine. No status entering/exiting the engine could be in it. *) - -module StringMap = Map.Make (String) -type option_value = - | String of string - | Int of int -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 = - match status.proof_status with - | Incomplete_proof { proof = p } -> p - | _ -> raise (Statement_error "no ongoing proof") - -let get_proof_metasenv status = - match status.proof_status with - | No_proof -> [] - | Proof (_, metasenv, _, _) - | Incomplete_proof { proof = (_, metasenv, _, _) } - | Intermediate metasenv -> - metasenv - -let get_stack status = - match status.proof_status with - | Incomplete_proof p -> p.stack - | Proof _ -> Continuationals.Stack.empty - | _ -> assert false - -let set_stack stack status = - match status.proof_status with - | Incomplete_proof p -> - { status with proof_status = Incomplete_proof { p with stack = stack } } - | Proof _ -> - assert (Continuationals.Stack.is_empty stack); - status - | _ -> assert false - -let set_metasenv metasenv status = - let proof_status = - match status.proof_status with - | No_proof -> Intermediate metasenv - | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) -> - Incomplete_proof - { incomplete_proof with proof = (uri, metasenv, proof, ty) } - | Intermediate _ -> Intermediate metasenv - | Proof _ -> assert false - in - { status with proof_status = proof_status } - -let get_proof_context status goal = - match status.proof_status with - | Incomplete_proof { proof = (_, metasenv, _, _) } -> - let (_, context, _) = CicUtil.lookup_meta goal metasenv in - context - | _ -> [] - -let get_proof_conclusion status goal = - match status.proof_status with - | Incomplete_proof { proof = (_, metasenv, _, _) } -> - let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in - conclusion - | _ -> raise (Statement_error "no ongoing proof") - -let add_moo_content cmds status = - let content = status.moo_content_rev in - let content' = - List.fold_right - (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 -(* prerr_endline ("new moo content: " ^ String.concat " " (List.map - GrafiteAstPp.pp_command content')); *) - { status with moo_content_rev = content' } - -let get_option status name = - try - StringMap.find name status.options - with Not_found -> raise (Option_error (name, "not found")) - -let set_option status name value = - let mangle_dir s = - let s = Str.global_replace (Str.regexp "//+") "/" s in - let s = Str.global_replace (Str.regexp "/$") "" s in - s - in - let types = [ "baseuri", (`String, mangle_dir); ] in - let ty_and_mangler = - try - List.assoc name types - with Not_found -> - command_error (Printf.sprintf "Unknown option \"%s\"" name) - in - let value = - match ty_and_mangler with - | `String, f -> String (f value) - | `Int, f -> - (try - Int (int_of_string (f value)) - with Failure _ -> - command_error (Printf.sprintf "Not an integer value \"%s\"" value)) - in - if StringMap.mem name status.options && name = "baseuri" then - command_error "Redefinition of 'baseuri' is forbidden." - else - { status with options = StringMap.add name value status.options } - - -let get_string_option status name = - match get_option status name with - | String s -> s - | _ -> raise (Option_error (name, "not a string value")) - -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:"; - HLog.message - (match status.proof_status with - | No_proof -> "no proof\n" - | Incomplete_proof _ -> "incomplete proof\n" - | Proof _ -> "proof\n" - | Intermediate _ -> "Intermediate\n"); - HLog.message "status.options\n"; - StringMap.iter (fun k v -> - let v = - match v with - | String s -> s - | Int i -> string_of_int i - in - HLog.message (k ^ "::=" ^ v)) status.options; - HLog.message "status.coercions\n"; - HLog.message "status.objects:\n"; - List.iter - (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects diff --git a/helm/ocaml/grafite2/grafiteTypes.mli b/helm/ocaml/grafite2/grafiteTypes.mli deleted file mode 100644 index 361a00825..000000000 --- a/helm/ocaml/grafite2/grafiteTypes.mli +++ /dev/null @@ -1,78 +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 Option_error of string * string -exception Statement_error of string -exception Command_error of string - -type incomplete_proof = { - proof: ProofEngineTypes.proof; - stack: Continuationals.Stack.t; -} - -type proof_status = - No_proof - | Incomplete_proof of incomplete_proof - | Proof of ProofEngineTypes.proof - | Intermediate of Cic.metasenv - -type option_value = - | String of string - | Int of int -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 -val set_option : status -> string -> string -> status - -val qualify: status -> string -> string - -val get_current_proof: status -> ProofEngineTypes.proof -val get_proof_metasenv: status -> Cic.metasenv -val get_stack: status -> Continuationals.Stack.t -val get_proof_context : status -> int -> Cic.context -val get_proof_conclusion : status -> int -> Cic.term - -val set_stack: Continuationals.Stack.t -> status -> status -val set_metasenv: Cic.metasenv -> status -> status diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/grafite2/matitaSync.ml deleted file mode 100644 index ee5d84278..000000000 --- a/helm/ocaml/grafite2/matitaSync.ml +++ /dev/null @@ -1,188 +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/ - *) - -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 - if description1 <> description2 then - (domain_item,codomain_item)::acc - else - acc - with - Not_found -> - (domain_item,codomain_item)::acc) - status.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 = - fst(List.fold_left ( - fun (acc,i) (name, _, _, cl) -> - (name, UriManager.uri_of_uriref uri i None) :: - (fst(List.fold_left ( - fun (acc,j) (name,_) -> - (((name,UriManager.uri_of_uriref uri i - (Some j)) :: acc) , j+1) - ) (acc,1) cl)),i+1 - ) ([],0) types) - -let build_aliases = - List.map - (fun (name,uri) -> - DisambiguateTypes.Id name, - (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri)) - -let add_aliases_for_inductive_def status types uri = - let aliases = build_aliases (extract_alias types uri) in - 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 - -let add_aliases_for_object status uri = - function - Cic.InductiveDefinition (types,_,_,_) -> - add_aliases_for_inductive_def status types uri - | Cic.Constant _ -> add_alias_for_constant 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 - -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 - 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.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 - 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 - -let init () = - LibrarySync.remove_all_coercions (); - LibraryObjects.reset_defaults (); - { - aliases = DisambiguateTypes.Environment.empty; - multi_aliases = DisambiguateTypes.Environment.empty; - moo_content_rev = []; - metadata = []; - proof_status = No_proof; - options = no_options; - objects = []; - coercions = []; - notation_ids = []; - } - - diff --git a/helm/ocaml/grafite2/matitaSync.mli b/helm/ocaml/grafite2/matitaSync.mli deleted file mode 100644 index bc744f862..000000000 --- a/helm/ocaml/grafite2/matitaSync.mli +++ /dev/null @@ -1,54 +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/ - *) - -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 time_travel: - present:GrafiteTypes.status -> past:GrafiteTypes.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 -> - (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 - - 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/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml new file mode 100644 index 000000000..c820986b3 --- /dev/null +++ b/helm/ocaml/grafite_engine/grafiteEngine.ml @@ -0,0 +1,700 @@ +(* 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 Drop +exception IncludedFileNotCompiled of string (* file name *) + +type options = { + do_heavy_checks: bool ; + clean_baseuri: bool +} + +(** create a ProofEngineTypes.mk_fresh_name_type function which uses given + * names as long as they are available, then it fallbacks to name generation + * using FreshNamesGenerator module *) +let namer_of names = + let len = List.length names in + let count = ref 0 in + fun metasenv context name ~typ -> + if !count < len then begin + let name = Cic.Name (List.nth names !count) in + incr count; + name + end else + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ + +let tactic_of_ast ast = + let module PET = ProofEngineTypes in + match ast with + | GrafiteAst.Absurd (_, term) -> Tactics.absurd term + | GrafiteAst.Apply (_, term) -> Tactics.apply term + | GrafiteAst.Assumption _ -> Tactics.assumption + | GrafiteAst.Auto (_,depth,width,paramodulation,full) -> + AutoTactic.auto_tac ?depth ?width ?paramodulation ?full + ~dbd:(LibraryDb.instance ()) () + | GrafiteAst.Change (_, pattern, with_what) -> + Tactics.change ~pattern with_what + | GrafiteAst.Clear (_,id) -> Tactics.clear id + | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id + | GrafiteAst.Contradiction _ -> Tactics.contradiction + | GrafiteAst.Compare (_, term) -> Tactics.compare term + | GrafiteAst.Constructor (_, n) -> Tactics.constructor n + | GrafiteAst.Cut (_, ident, term) -> + let names = match ident with None -> [] | Some id -> [id] in + Tactics.cut ~mk_fresh_name_callback:(namer_of names) term + | GrafiteAst.DecideEquality _ -> Tactics.decide_equality + | GrafiteAst.Decompose (_, types, what, names) -> + let to_type = function + | GrafiteAst.Type (uri, typeno) -> uri, typeno + | GrafiteAst.Ident _ -> assert false + in + let user_types = List.rev_map to_type types in + let dbd = LibraryDb.instance () in + let mk_fresh_name_callback = namer_of names in + Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what + | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term + | GrafiteAst.Elim (_, what, using, depth, names) -> + Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) + what + | GrafiteAst.ElimType (_, what, using, depth, names) -> + Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) + what + | GrafiteAst.Exact (_, term) -> Tactics.exact term + | GrafiteAst.Exists _ -> Tactics.exists + | GrafiteAst.Fail _ -> Tactics.fail + | GrafiteAst.Fold (_, reduction_kind, term, pattern) -> + let reduction = + match reduction_kind with + | `Normalize -> + PET.const_lazy_reduction + (CicReduction.normalize ~delta:false ~subst:[]) + | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce + | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl + | `Unfold None -> + PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None) + | `Unfold (Some lazy_term) -> + (fun context metasenv ugraph -> + let what, metasenv, ugraph = lazy_term context metasenv ugraph in + ProofEngineReduction.unfold ~what, metasenv, ugraph) + | `Whd -> + PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[]) + in + Tactics.fold ~reduction ~term ~pattern + | GrafiteAst.Fourier _ -> Tactics.fourier + | GrafiteAst.FwdSimpl (_, hyp, names) -> + Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) + ~dbd:(LibraryDb.instance ()) hyp + | GrafiteAst.Generalize (_,pattern,ident) -> + let names = match ident with None -> [] | Some id -> [id] in + Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern + | GrafiteAst.Goal (_, n) -> Tactics.set_goal n + | GrafiteAst.IdTac _ -> Tactics.id + | GrafiteAst.Injection (_,term) -> Tactics.injection term + | GrafiteAst.Intros (_, None, names) -> + PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () + | GrafiteAst.Intros (_, Some num, names) -> + PrimitiveTactics.intros_tac ~howmany:num + ~mk_fresh_name_callback:(namer_of names) () + | GrafiteAst.Inversion (_, term) -> + Tactics.inversion term + | GrafiteAst.LApply (_, how_many, to_what, what, ident) -> + let names = match ident with None -> [] | Some id -> [id] in + Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many + ~to_what what + | GrafiteAst.Left _ -> Tactics.left + | GrafiteAst.LetIn (loc,term,name) -> + Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) + | GrafiteAst.Reduce (_, reduction_kind, pattern) -> + (match reduction_kind with + | `Normalize -> Tactics.normalize ~pattern + | `Reduce -> Tactics.reduce ~pattern + | `Simpl -> Tactics.simpl ~pattern + | `Unfold what -> Tactics.unfold ~pattern what + | `Whd -> Tactics.whd ~pattern) + | GrafiteAst.Reflexivity _ -> Tactics.reflexivity + | GrafiteAst.Replace (_, pattern, with_what) -> + Tactics.replace ~pattern ~with_what + | GrafiteAst.Rewrite (_, direction, t, pattern) -> + EqualityTactics.rewrite_tac ~direction ~pattern t + | GrafiteAst.Right _ -> Tactics.right + | GrafiteAst.Ring _ -> Tactics.ring + | GrafiteAst.Split _ -> Tactics.split + | GrafiteAst.Symmetry _ -> Tactics.symmetry + | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term + +(* maybe we only need special cases for apply and goal *) +let classify_tactic tactic = + match tactic with + (* tactics that can't close the goal (return a goal we want to "select") *) + | GrafiteAst.Rewrite _ + | GrafiteAst.Split _ + | GrafiteAst.Replace _ + | GrafiteAst.Reduce _ + | GrafiteAst.Injection _ + | GrafiteAst.IdTac _ + | GrafiteAst.Generalize _ + | GrafiteAst.Elim _ + | GrafiteAst.Cut _ + | GrafiteAst.Decompose _ -> true, true + (* tactics we don't want to reorder goals. I think only Goal needs this. *) + | GrafiteAst.Goal _ -> false, true + (* tactics like apply *) + | _ -> true, false + +let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= + let module PEH = ProofEngineHelpers in +(* let print_m name metasenv = + prerr_endline (">>>>> " ^ name); + prerr_endline (CicMetaSubst.ppmetasenv [] metasenv) + in *) + (* phase one calculates: + * new_goals_from_refine: goals added by refine + * head_goal: the first goal opened by ythe tactic + * other_goals: other goals opened by the tactic + *) + let new_goals_from_refine = PEH.compare_metasenvs start refine in + let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in + let head_goal, other_goals, goals = + match goals with + | [] -> None,[],goals + | hd::tl -> + (* assert (List.mem hd new_goals_from_tactic); + * invalidato dalla goal_tac + * *) + Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>) + hd) goals + in + let produced_goals = + match head_goal with + | None -> new_goals_from_refine @ other_goals + | Some x -> x :: new_goals_from_refine @ other_goals + in + (* extract the metas generated by refine and tactic *) + let metas_for_tactic_head = + match head_goal with + | None -> [] + | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in + let metas_for_tactic_goals = + List.map + (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic) + goals + in + let metas_for_refine_goals = + List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in + let produced_metas, goals = + let produced_metas = + if always_opens_a_goal then + metas_for_tactic_head @ metas_for_refine_goals @ + metas_for_tactic_goals + else begin +(* print_m "metas_for_refine_goals" metas_for_refine_goals; + print_m "metas_for_tactic_head" metas_for_tactic_head; + print_m "metas_for_tactic_goals" metas_for_tactic_goals; *) + metas_for_refine_goals @ metas_for_tactic_head @ + metas_for_tactic_goals + end + in + let goals = List.map (fun (metano, _, _) -> metano) produced_metas in + produced_metas, goals + in + (* residual metas, preserving the original order *) + let before, after = + let rec split e = + function + | [] -> [],[] + | (metano, _, _) :: tl when metano = e -> + [], List.map (fun (x,_,_) -> x) tl + | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a + in + let find n metasenv = + try + Some (List.find (fun (metano, _, _) -> metano = n) metasenv) + with Not_found -> None + in + let extract l = + List.fold_right + (fun n acc -> + match find n tactic with + | Some x -> x::acc + | None -> acc + ) l [] in + let before_l, after_l = split current_goal start in + let before_l = + List.filter (fun x -> not (List.mem x produced_goals)) before_l in + let after_l = + List.filter (fun x -> not (List.mem x produced_goals)) after_l in + let before = extract before_l in + let after = extract after_l in + before, after + in +(* |+ DEBUG CODE +| + print_m "BEGIN" start; + prerr_endline ("goal was: " ^ string_of_int current_goal); + prerr_endline ("and metas from refine are:"); + List.iter + (fun t -> prerr_string (" " ^ string_of_int t)) + new_goals_from_refine; + prerr_endline ""; + print_m "before" before; + print_m "metas_for_tactic_head" metas_for_tactic_head; + print_m "metas_for_refine_goals" metas_for_refine_goals; + print_m "metas_for_tactic_goals" metas_for_tactic_goals; + print_m "produced_metas" produced_metas; + print_m "after" after; +|+ FINE DEBUG CODE +| *) + before @ produced_metas @ after, goals + +let apply_tactic ~disambiguate_tactic tactic (status, goal) = +(* prerr_endline "apply_tactic"; *) +(* prerr_endline (Continuationals.Stack.pp (GrafiteTypes.get_stack status)); *) + let starting_metasenv = GrafiteTypes.get_proof_metasenv status in + let before = List.map (fun g, _, _ -> g) starting_metasenv in +(* prerr_endline "disambiguate"; *) + 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 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 + let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in +(* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before)); +prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after)); +prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *) +(* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals)); +prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *) + let proof, opened_goals = + if needs_reordering then begin + let uri, metasenv_after_tactic, t, ty = proof in +(* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *) + let reordered_metasenv, opened_goals = + reorder_metasenv + starting_metasenv + metasenv_after_refinement metasenv_after_tactic + opened goal always_opens_a_goal + in + let proof' = uri, reordered_metasenv, t, ty in +(* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *) + proof', opened_goals + end + else + proof, opened_goals + in + let incomplete_proof = + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Incomplete_proof p -> p + | _ -> assert false + in + { status with GrafiteTypes.proof_status = + GrafiteTypes.Incomplete_proof + { incomplete_proof with GrafiteTypes.proof = proof } }, + opened_goals, closed_goals + +type eval_ast = + {ea_go: + 'term 'lazy_term 'reduction 'obj 'ident. + disambiguate_tactic: + (GrafiteTypes.status -> + ProofEngineTypes.goal -> + ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + GrafiteTypes.status * + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + + disambiguate_command: + (GrafiteTypes.status -> + 'obj GrafiteAst.command -> + GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + + ?do_heavy_checks:bool -> + ?clean_baseuri:bool -> + GrafiteTypes.status -> + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + GrafiteTypes.status * UriManager.uri list + } + +type 'a eval_command = + {ec_go: 'term 'obj. + disambiguate_command: + (GrafiteTypes.status -> + 'obj GrafiteAst.command -> + GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + options -> GrafiteTypes.status -> 'obj GrafiteAst.command -> + GrafiteTypes.status * UriManager.uri list + } + +type 'a eval_executable = + {ee_go: 'term 'lazy_term 'reduction 'obj 'ident. + disambiguate_tactic: + (GrafiteTypes.status -> + ProofEngineTypes.goal -> + ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + GrafiteTypes.status * + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + + disambiguate_command: + (GrafiteTypes.status -> + 'obj GrafiteAst.command -> + GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + + options -> + GrafiteTypes.status -> + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code -> + GrafiteTypes.status * UriManager.uri list + } + +type 'a eval_from_moo = + { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } + +let coercion_moo_statement_of uri = + GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false) + +let eval_coercion status ~add_composites uri = + let basedir = Helm_registry.get "matita.basedir" 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 + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + compounds + +let eval_tactical ~disambiguate_tactic status tac = + let apply_tactic = apply_tactic ~disambiguate_tactic in + let module MatitaStatus = + struct + type input_status = GrafiteTypes.status * ProofEngineTypes.goal + + type output_status = + GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list + + type tactic = input_status -> output_status + + 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 + let set_goals (opened, closed) (status, _, _) = (status, opened, closed) + let get_stack (status, _) = GrafiteTypes.get_stack status + + let set_stack stack (status, opened, closed) = + GrafiteTypes.set_stack stack status, opened, closed + + let inject (status, _) = (status, [], []) + let focus goal (status, _, _) = (status, goal) + end + in + let module MatitaTacticals = Tacticals.Make (MatitaStatus) in + let rec tactical_of_ast l tac = + match tac with + | GrafiteAst.Tactic (loc, tactic) -> + MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic)) + | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) + assert (l > 0); + MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals) + | GrafiteAst.Do (loc, n, tactical) -> + MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical) + | GrafiteAst.Repeat (loc, tactical) -> + MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical) + | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) + assert (l > 0); + MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical) + ~continuations:(List.map (tactical_of_ast (l+1)) tacticals) + | GrafiteAst.First (loc, tacticals) -> + MatitaTacticals.first + ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals) + | GrafiteAst.Try (loc, tactical) -> + MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical) + | GrafiteAst.Solve (loc, tacticals) -> + MatitaTacticals.solve_tactics + ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals) + + | GrafiteAst.Skip loc -> MatitaTacticals.skip + | GrafiteAst.Dot loc -> MatitaTacticals.dot + | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon + | GrafiteAst.Branch loc -> MatitaTacticals.branch + | GrafiteAst.Shift loc -> MatitaTacticals.shift + | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i + | GrafiteAst.Merge loc -> MatitaTacticals.merge + | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals + | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus + in + let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in + let status = (* is proof completed? *) + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Incomplete_proof + { GrafiteTypes.stack = stack; proof = proof } + when Continuationals.Stack.is_empty stack -> + { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof } + | _ -> status + in + status + +let eval_comment status c = status + +(* since the record syntax allows to declare coercions, we have to put this + * information inside the moo *) +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,[] + | Some fields -> + let is_a_coercion uri = + try + let obj,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in + let attrs = CicUtil.attributes_of_obj obj in + List.mem (`Class `Projection) attrs + with Not_found -> assert false + in + (* looking at the fields we can know the 'wanted' coercions, but not the + * actually generated ones. So, only the intersection between the wanted + * and the actual should be in the moo as coercion, while everithing in + * lemmas should go as aliases *) + let wanted_coercions = + HExtlib.filter_map + (function + | (name,true) -> + Some + (UriManager.uri_of_string + (GrafiteTypes.qualify status name ^ ".con")) + | _ -> None) + fields + in + prerr_endline "wanted coercions:"; + List.iter + (fun u -> prerr_endline (UriManager.string_of_uri u)) + wanted_coercions; + let coercions, moo_content = + List.split + (HExtlib.filter_map + (fun uri -> + let is_a_wanted_coercion = + List.exists (UriManager.eq uri) wanted_coercions in + if is_a_coercion uri && is_a_wanted_coercion then + Some (uri, coercion_moo_statement_of uri) + else + None) + lemmas) + in + List.iter + (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,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 status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in + status, lemmas + +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, 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 = eval_from_moo.efm_go status moopath in + status,[] + | GrafiteAst.Set (loc, 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 = + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Proof (Some uri, metasenv, body, ty) -> + uri, metasenv, body, ty + | GrafiteTypes.Proof (None, metasenv, body, ty) -> + raise (GrafiteTypes.Command_error + ("Someone allows to start a theorem without giving the "^ + "name/uri. This should be fixed!")) + | _-> + raise + (GrafiteTypes.Command_error "You can't Qed an incomplete theorem") + in + if metasenv <> [] then + raise + (GrafiteTypes.Command_error + "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 + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + uri::lemmas + | GrafiteAst.Coercion (loc, uri, add_composites) -> + eval_coercion status ~add_composites uri + | GrafiteAst.Obj (loc,obj) -> + let ext,name = + match obj with + Cic.Constant (name,_,_,_,_) + | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name + | Cic.InductiveDefinition (types,_,_,_) -> + ".ind", + (match types with (name,_,_,_)::_ -> name | _ -> assert false) + | _ -> assert false in + let uri = + UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) + in + let metasenv = GrafiteTypes.get_proof_metasenv status in + match obj with + | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> + let name = UriManager.name_of_uri uri in + if not(CicPp.check name ty) then + HLog.error ("Bad name: " ^ name); + if opts.do_heavy_checks then + begin + let dbd = LibraryDb.instance () in + let similar = Whelp.match_term ~dbd ty in + let similar_len = List.length similar in + if similar_len> 30 then + (HLog.message + ("Duplicate check will compare your theorem with " ^ + string_of_int similar_len ^ + " theorems, this may take a while.")); + let convertible = + List.filter ( + fun u -> + let t = CicUtil.term_of_uri u in + let ty',g = + CicTypeChecker.type_of_aux' + metasenv' [] t CicUniv.empty_ugraph + in + fst(CicReduction.are_convertible [] ty' ty g)) + similar + in + (match convertible with + | [] -> () + | x::_ -> + HLog.warn + ("Theorem already proved: " ^ UriManager.string_of_uri x ^ + "\nPlease use a variant.")); + end; + assert (metasenv = metasenv'); + let goalno = + match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false + in + let initial_proof = (Some uri, metasenv, bo, ty) in + let initial_stack = Continuationals.Stack.of_metasenv metasenv in + { status with GrafiteTypes.proof_status = + GrafiteTypes.Incomplete_proof + { 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,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 ~disambiguate_tactic ~disambiguate_command opts status ex -> + match ex with + | GrafiteAst.Tactical (_, tac, None) -> + 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,[] + | GrafiteAst.Command (_, cmd) -> + eval_command.ec_go ~disambiguate_command opts status cmd + | GrafiteAst.Macro (_, mac) -> +(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO + raise (Command_error + (Printf.sprintf "The macro %s can't be in a script" + (GrafiteAstPp.pp_macro_ast mac))) +*) assert false + +} and eval_from_moo = {efm_go = fun status fname -> + let ast_of_cmd cmd = + GrafiteAst.Executable (HExtlib.dummy_floc, + GrafiteAst.Command (HExtlib.dummy_floc, + cmd)) + in + let moo = GrafiteMarshal.load_moo fname in + List.fold_left + (fun status ast -> + let ast = ast_of_cmd ast in + let status,lemmas = + eval_ast.ea_go + ~disambiguate_tactic:(fun status _ tactic -> status,tactic) + ~disambiguate_command:(fun status cmd -> status,cmd) + 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 = { + do_heavy_checks = do_heavy_checks ; + clean_baseuri = clean_baseuri } + in + match st with + | GrafiteAst.Executable (_,ex) -> + eval_executable.ee_go ~disambiguate_tactic + ~disambiguate_command opts status ex + | GrafiteAst.Comment (_,c) -> eval_comment status c,[] +} + +let eval_ast = eval_ast.ea_go diff --git a/helm/ocaml/grafite_engine/grafiteEngine.mli b/helm/ocaml/grafite_engine/grafiteEngine.mli new file mode 100644 index 000000000..4043e8072 --- /dev/null +++ b/helm/ocaml/grafite_engine/grafiteEngine.mli @@ -0,0 +1,47 @@ +(* 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 Drop +exception IncludedFileNotCompiled of string + +val eval_ast : + disambiguate_tactic: + (GrafiteTypes.status -> + ProofEngineTypes.goal -> + ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + GrafiteTypes.status * + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + + disambiguate_command: + (GrafiteTypes.status -> + 'obj GrafiteAst.command -> + GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + + ?do_heavy_checks:bool -> + ?clean_baseuri:bool -> + GrafiteTypes.status -> + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + (* the new status and generated objects, if any *) + GrafiteTypes.status * UriManager.uri list diff --git a/helm/ocaml/grafite_engine/grafiteMisc.ml b/helm/ocaml/grafite_engine/grafiteMisc.ml new file mode 100644 index 000000000..227cd382b --- /dev/null +++ b/helm/ocaml/grafite_engine/grafiteMisc.ml @@ -0,0 +1,31 @@ +(* 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/ + *) + +let is_empty buri = + List.for_all + (function + Http_getter_types.Ls_section _ -> true + | Http_getter_types.Ls_object _ -> false) + (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/")) diff --git a/helm/ocaml/grafite_engine/grafiteMisc.mli b/helm/ocaml/grafite_engine/grafiteMisc.mli new file mode 100644 index 000000000..833bb6360 --- /dev/null +++ b/helm/ocaml/grafite_engine/grafiteMisc.mli @@ -0,0 +1,27 @@ +(* 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/ + *) + + (** check whether no objects are defined below a given baseuri *) +val is_empty: string -> bool 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/grafite_engine/grafiteTypes.ml b/helm/ocaml/grafite_engine/grafiteTypes.ml new file mode 100644 index 000000000..a13cc074e --- /dev/null +++ b/helm/ocaml/grafite_engine/grafiteTypes.ml @@ -0,0 +1,193 @@ +(* 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 Option_error of string * string +exception Statement_error of string +exception Command_error of string + +let command_error msg = raise (Command_error msg) + +type incomplete_proof = { + proof: ProofEngineTypes.proof; + stack: Continuationals.Stack.t; +} + +type proof_status = + | No_proof + | Incomplete_proof of incomplete_proof + | Proof of ProofEngineTypes.proof + | Intermediate of Cic.metasenv + (* Status in which the proof could be while it is being processed by the + * engine. No status entering/exiting the engine could be in it. *) + +module StringMap = Map.Make (String) +type option_value = + | String of string + | Int of int +type options = option_value StringMap.t +let no_options = StringMap.empty + +type status = { + moo_content_rev: GrafiteMarshal.moo; + proof_status: proof_status; + options: options; + objects: UriManager.uri list; + coercions: UriManager.uri list; +} + +let get_current_proof status = + match status.proof_status with + | Incomplete_proof { proof = p } -> p + | _ -> raise (Statement_error "no ongoing proof") + +let get_proof_metasenv status = + match status.proof_status with + | No_proof -> [] + | Proof (_, metasenv, _, _) + | Incomplete_proof { proof = (_, metasenv, _, _) } + | Intermediate metasenv -> + metasenv + +let get_stack status = + match status.proof_status with + | Incomplete_proof p -> p.stack + | Proof _ -> Continuationals.Stack.empty + | _ -> assert false + +let set_stack stack status = + match status.proof_status with + | Incomplete_proof p -> + { status with proof_status = Incomplete_proof { p with stack = stack } } + | Proof _ -> + assert (Continuationals.Stack.is_empty stack); + status + | _ -> assert false + +let set_metasenv metasenv status = + let proof_status = + match status.proof_status with + | No_proof -> Intermediate metasenv + | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) -> + Incomplete_proof + { incomplete_proof with proof = (uri, metasenv, proof, ty) } + | Intermediate _ -> Intermediate metasenv + | Proof (_, metasenv', _, _) -> + assert (metasenv = metasenv'); + status.proof_status + in + { status with proof_status = proof_status } + +let get_proof_context status goal = + match status.proof_status with + | Incomplete_proof { proof = (_, metasenv, _, _) } -> + let (_, context, _) = CicUtil.lookup_meta goal metasenv in + context + | _ -> [] + +let get_proof_conclusion status goal = + match status.proof_status with + | Incomplete_proof { proof = (_, metasenv, _, _) } -> + let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in + conclusion + | _ -> raise (Statement_error "no ongoing proof") + +let add_moo_content cmds status = + let content = status.moo_content_rev in + let content' = + List.fold_right + (fun cmd acc -> +(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *) + match cmd with + | GrafiteAst.Default _ -> + if List.mem cmd content then acc + else cmd :: acc + | _ -> cmd :: acc) + cmds content + in +(* prerr_endline ("new moo content: " ^ String.concat " " (List.map + GrafiteAstPp.pp_command content')); *) + { status with moo_content_rev = content' } + +let get_option status name = + try + StringMap.find name status.options + with Not_found -> raise (Option_error (name, "not found")) + +let set_option status name value = + let mangle_dir s = + let s = Str.global_replace (Str.regexp "//+") "/" s in + let s = Str.global_replace (Str.regexp "/$") "" s in + s + in + let types = [ "baseuri", (`String, mangle_dir); ] in + let ty_and_mangler = + try + List.assoc name types + with Not_found -> + command_error (Printf.sprintf "Unknown option \"%s\"" name) + in + let value = + match ty_and_mangler with + | `String, f -> String (f value) + | `Int, f -> + (try + Int (int_of_string (f value)) + with Failure _ -> + command_error (Printf.sprintf "Not an integer value \"%s\"" value)) + in + if StringMap.mem name status.options && name = "baseuri" then + command_error "Redefinition of 'baseuri' is forbidden." + else + { status with options = StringMap.add name value status.options } + + +let get_string_option status name = + match get_option status name with + | String s -> s + | _ -> raise (Option_error (name, "not a string value")) + +let qualify status name = get_string_option status "baseuri" ^ "/" ^ name + +let dump_status status = + HLog.message "status.aliases:\n"; + HLog.message "status.proof_status:"; + HLog.message + (match status.proof_status with + | No_proof -> "no proof\n" + | Incomplete_proof _ -> "incomplete proof\n" + | Proof _ -> "proof\n" + | Intermediate _ -> "Intermediate\n"); + HLog.message "status.options\n"; + StringMap.iter (fun k v -> + let v = + match v with + | String s -> s + | Int i -> string_of_int i + in + HLog.message (k ^ "::=" ^ v)) status.options; + HLog.message "status.coercions\n"; + HLog.message "status.objects:\n"; + List.iter + (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects diff --git a/helm/ocaml/grafite_engine/grafiteTypes.mli b/helm/ocaml/grafite_engine/grafiteTypes.mli new file mode 100644 index 000000000..70089623b --- /dev/null +++ b/helm/ocaml/grafite_engine/grafiteTypes.mli @@ -0,0 +1,73 @@ +(* 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 Option_error of string * string +exception Statement_error of string +exception Command_error of string + +type incomplete_proof = { + proof: ProofEngineTypes.proof; + stack: Continuationals.Stack.t; +} + +type proof_status = + No_proof + | Incomplete_proof of incomplete_proof + | Proof of ProofEngineTypes.proof + | Intermediate of Cic.metasenv + +type option_value = + | String of string + | Int of int +type options +val no_options: options + +type status = { + moo_content_rev: GrafiteMarshal.moo; + proof_status: proof_status; (** logical status *) + options: options; + objects: UriManager.uri list; (** in-scope objects *) + coercions: UriManager.uri list; (** defined coercions *) +} + +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 get_option : status -> string -> option_value +val get_string_option : status -> string -> string +val set_option : status -> string -> string -> status + +val qualify: status -> string -> string + +val get_current_proof: status -> ProofEngineTypes.proof +val get_proof_metasenv: status -> Cic.metasenv +val get_stack: status -> Continuationals.Stack.t +val get_proof_context : status -> int -> Cic.context +val get_proof_conclusion : status -> int -> Cic.term + +val set_stack: Continuationals.Stack.t -> status -> status +val set_metasenv: Cic.metasenv -> status -> status 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/grafiteDisambiguator.ml b/helm/ocaml/grafite_parser/grafiteDisambiguator.ml new file mode 100644 index 000000000..5258a4963 --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteDisambiguator.ml @@ -0,0 +1,176 @@ +(* 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 + +exception Ambiguous_input +(* the integer is an offset to be added to each location *) +exception DisambiguationError of + int * (Token.flocation option * string Lazy.t) list list + (** parameters are: option name, error message *) +exception Unbound_identifier of string + +type choose_uris_callback = + id:string -> UriManager.uri list -> UriManager.uri list + +type choose_interp_callback = (string * string) list list -> int list + +let mono_uris_callback ~id = + if Helm_registry.get_bool "matita.auto_disambiguation" then + function l -> l + else + raise Ambiguous_input + +let mono_interp_callback _ = raise Ambiguous_input + +let _choose_uris_callback = ref mono_uris_callback +let _choose_interp_callback = ref mono_interp_callback +let set_choose_uris_callback f = _choose_uris_callback := f +let set_choose_interp_callback f = _choose_interp_callback := f + +module Callbacks = + struct + let interactive_user_uri_choice ~selection_mode ?ok + ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = + !_choose_uris_callback ~id uris + + let interactive_interpretation_choice interp = + !_choose_interp_callback interp + + let input_or_locate_uri ~(title:string) ?id = + (* Zack: I try to avoid using this callback. I therefore assume that + * the presence of an identifier that can't be resolved via "locate" + * query is a syntax error *) + let msg = match id with Some id -> id | _ -> "_" in + raise (Unbound_identifier msg) + end + +module Disambiguator = Disambiguate.Make (Callbacks) + +(* implement module's API *) + +let disambiguate_thing ~aliases ~universe + ~(f:?fresh_instances:bool -> + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + 'a -> 'b) + ~(drop_aliases: 'b -> 'b) + ~(drop_aliases_and_clear_diff: 'b -> 'b) + (thing: 'a) += + assert (universe <> None); + let library = false, DisambiguateTypes.Environment.empty, None in + let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in + let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in + let passes = (* *) + [ (false, mono_aliases, false); + (false, multi_aliases, false); + (true, mono_aliases, false); + (true, multi_aliases, false); + (true, mono_aliases, true); + (true, multi_aliases, true); + (true, library, true); + ] + in + let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) = + CicRefine.insert_coercions := insert_coercions; + f ~fresh_instances ~aliases ~universe thing + in + let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = + if use_mono_aliases && not instances then + drop_aliases res + else if user_asked then + drop_aliases res (* one shot aliases *) + else + drop_aliases_and_clear_diff res + in + let rec aux errors = + function + | [ pass ] -> + (try + set_aliases pass (try_pass pass) + with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> + raise (DisambiguationError (offset, errors @ [newerrors]))) + | hd :: tl -> + (try + set_aliases hd (try_pass hd) + with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) -> + aux (errors @ [newerrors]) tl) + | [] -> assert false + in + let saved_insert_coercions = !CicRefine.insert_coercions in + try + let res = aux [] passes in + CicRefine.insert_coercions := saved_insert_coercions; + res + with exn -> + CicRefine.insert_coercions := saved_insert_coercions; + raise exn + +type disambiguator_thing = + { do_it : + 'a 'b. + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + f:(?fresh_instances:bool -> + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + 'a -> 'b * bool) -> + drop_aliases:('b * bool -> 'b * bool) -> + drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool + } + +let disambiguate_thing = + let profiler = HExtlib.profile "disambiguate_thing" in + { do_it = + fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing + -> profiler.HExtlib.profile + (disambiguate_thing ~aliases ~universe ~f ~drop_aliases + ~drop_aliases_and_clear_diff) thing + } + +let drop_aliases (choices, user_asked) = + (List.map (fun (d, a, b, c) -> d, a, b, c) choices), + user_asked + +let drop_aliases_and_clear_diff (choices, user_asked) = + (List.map (fun (_, a, b, c) -> [], a, b, c) choices), + user_asked + +let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph + ~aliases ~universe term + = + assert (fresh_instances = None); + let f = + Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph + in + disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases + ~drop_aliases_and_clear_diff term + +let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj = + assert (fresh_instances = None); + let f = Disambiguator.disambiguate_obj ~dbd ~uri in + disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases + ~drop_aliases_and_clear_diff obj diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguator.mli b/helm/ocaml/grafite_parser/grafiteDisambiguator.mli new file mode 100644 index 000000000..b7c85f6af --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteDisambiguator.mli @@ -0,0 +1,51 @@ +(* 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/ + *) + +(** raised when ambiguous input is found but not expected (e.g. in the batch + * compiler) *) +exception Ambiguous_input +(* the integer is an offset to be added to each location *) +exception DisambiguationError of + int * (Token.flocation option * string Lazy.t) list list + +type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list +type choose_interp_callback = (string * string) list list -> int list + +val set_choose_uris_callback: choose_uris_callback -> unit +val set_choose_interp_callback: choose_interp_callback -> unit + +(** @raise Ambiguous_input if called, default value for internal + * choose_uris_callback if not set otherwise with set_choose_uris_callback + * above *) +val mono_uris_callback: choose_uris_callback + +(** @raise Ambiguous_input if called, default value for internal + * choose_interp_callback if not set otherwise with set_choose_interp_callback + * above *) +val mono_interp_callback: choose_interp_callback + +(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) + +include Disambiguate.Disambiguator 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/grafiteParserMisc.mli b/helm/ocaml/grafite_parser/grafiteParserMisc.mli deleted file mode 100644 index 74f60ec04..000000000 --- a/helm/ocaml/grafite_parser/grafiteParserMisc.mli +++ /dev/null @@ -1,32 +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 - -val baseuri_of_baseuri_decl : - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> - string option - -val baseuri_of_script : include_paths:string list -> string -> string diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.ml b/helm/ocaml/grafite_parser/matitaDisambiguator.ml deleted file mode 100644 index 5258a4963..000000000 --- a/helm/ocaml/grafite_parser/matitaDisambiguator.ml +++ /dev/null @@ -1,176 +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/ - *) - -open Printf - -exception Ambiguous_input -(* the integer is an offset to be added to each location *) -exception DisambiguationError of - int * (Token.flocation option * string Lazy.t) list list - (** parameters are: option name, error message *) -exception Unbound_identifier of string - -type choose_uris_callback = - id:string -> UriManager.uri list -> UriManager.uri list - -type choose_interp_callback = (string * string) list list -> int list - -let mono_uris_callback ~id = - if Helm_registry.get_bool "matita.auto_disambiguation" then - function l -> l - else - raise Ambiguous_input - -let mono_interp_callback _ = raise Ambiguous_input - -let _choose_uris_callback = ref mono_uris_callback -let _choose_interp_callback = ref mono_interp_callback -let set_choose_uris_callback f = _choose_uris_callback := f -let set_choose_interp_callback f = _choose_interp_callback := f - -module Callbacks = - struct - let interactive_user_uri_choice ~selection_mode ?ok - ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = - !_choose_uris_callback ~id uris - - let interactive_interpretation_choice interp = - !_choose_interp_callback interp - - let input_or_locate_uri ~(title:string) ?id = - (* Zack: I try to avoid using this callback. I therefore assume that - * the presence of an identifier that can't be resolved via "locate" - * query is a syntax error *) - let msg = match id with Some id -> id | _ -> "_" in - raise (Unbound_identifier msg) - end - -module Disambiguator = Disambiguate.Make (Callbacks) - -(* implement module's API *) - -let disambiguate_thing ~aliases ~universe - ~(f:?fresh_instances:bool -> - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> - 'a -> 'b) - ~(drop_aliases: 'b -> 'b) - ~(drop_aliases_and_clear_diff: 'b -> 'b) - (thing: 'a) -= - assert (universe <> None); - let library = false, DisambiguateTypes.Environment.empty, None in - let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in - let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in - let passes = (* *) - [ (false, mono_aliases, false); - (false, multi_aliases, false); - (true, mono_aliases, false); - (true, multi_aliases, false); - (true, mono_aliases, true); - (true, multi_aliases, true); - (true, library, true); - ] - in - let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) = - CicRefine.insert_coercions := insert_coercions; - f ~fresh_instances ~aliases ~universe thing - in - let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = - if use_mono_aliases && not instances then - drop_aliases res - else if user_asked then - drop_aliases res (* one shot aliases *) - else - drop_aliases_and_clear_diff res - in - let rec aux errors = - function - | [ pass ] -> - (try - set_aliases pass (try_pass pass) - with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> - raise (DisambiguationError (offset, errors @ [newerrors]))) - | hd :: tl -> - (try - set_aliases hd (try_pass hd) - with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) -> - aux (errors @ [newerrors]) tl) - | [] -> assert false - in - let saved_insert_coercions = !CicRefine.insert_coercions in - try - let res = aux [] passes in - CicRefine.insert_coercions := saved_insert_coercions; - res - with exn -> - CicRefine.insert_coercions := saved_insert_coercions; - raise exn - -type disambiguator_thing = - { do_it : - 'a 'b. - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> - f:(?fresh_instances:bool -> - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> - 'a -> 'b * bool) -> - drop_aliases:('b * bool -> 'b * bool) -> - drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool - } - -let disambiguate_thing = - let profiler = HExtlib.profile "disambiguate_thing" in - { do_it = - fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing - -> profiler.HExtlib.profile - (disambiguate_thing ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff) thing - } - -let drop_aliases (choices, user_asked) = - (List.map (fun (d, a, b, c) -> d, a, b, c) choices), - user_asked - -let drop_aliases_and_clear_diff (choices, user_asked) = - (List.map (fun (_, a, b, c) -> [], a, b, c) choices), - user_asked - -let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph - ~aliases ~universe term - = - assert (fresh_instances = None); - let f = - Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph - in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff term - -let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj = - assert (fresh_instances = None); - let f = Disambiguator.disambiguate_obj ~dbd ~uri in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff obj diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.mli b/helm/ocaml/grafite_parser/matitaDisambiguator.mli deleted file mode 100644 index b7c85f6af..000000000 --- a/helm/ocaml/grafite_parser/matitaDisambiguator.mli +++ /dev/null @@ -1,51 +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/ - *) - -(** raised when ambiguous input is found but not expected (e.g. in the batch - * compiler) *) -exception Ambiguous_input -(* the integer is an offset to be added to each location *) -exception DisambiguationError of - int * (Token.flocation option * string Lazy.t) list list - -type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list -type choose_interp_callback = (string * string) list list -> int list - -val set_choose_uris_callback: choose_uris_callback -> unit -val set_choose_interp_callback: choose_interp_callback -> unit - -(** @raise Ambiguous_input if called, default value for internal - * choose_uris_callback if not set otherwise with set_choose_uris_callback - * above *) -val mono_uris_callback: choose_uris_callback - -(** @raise Ambiguous_input if called, default value for internal - * choose_interp_callback if not set otherwise with set_choose_interp_callback - * above *) -val mono_interp_callback: choose_interp_callback - -(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) - -include Disambiguate.Disambiguator 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/lexicon/cicNotation.ml b/helm/ocaml/lexicon/cicNotation.ml new file mode 100644 index 000000000..0d48ea06d --- /dev/null +++ b/helm/ocaml/lexicon/cicNotation.ml @@ -0,0 +1,81 @@ +(* 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 LexiconAst + +type notation_id = + | RuleId of CicNotationParser.rule_id + | InterpretationId of TermAcicContent.interpretation_id + | PrettyPrinterId of TermContentPres.pretty_printer_id + +let process_notation st = + match st with + | Notation (loc, dir, l1, associativity, precedence, l2) -> + let rule_id = + if dir <> Some `RightToLeft then + [ RuleId (CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> + CicNotationPt.AttributedTerm + (`Loc loc,TermContentPres.instantiate_level2 env l2))) ] + else + [] + in + let pp_id = + if dir <> Some `LeftToRight then + [ PrettyPrinterId + (TermContentPres.add_pretty_printer ?precedence ?associativity + l2 l1) ] + else + [] + in + rule_id @ pp_id + | Interpretation (loc, dsc, l2, l3) -> + let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in + [InterpretationId interp_id] + | st -> [] + +let remove_notation = function + | RuleId id -> CicNotationParser.delete id + | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id + | InterpretationId id -> TermAcicContent.remove_interpretation id + +let get_all_notations () = + List.map + (fun (interp_id, dsc) -> + InterpretationId interp_id, "interpretation: " ^ dsc) + (TermAcicContent.get_all_interpretations ()) + +let get_active_notations () = + List.map (fun id -> InterpretationId id) + (TermAcicContent.get_active_interpretations ()) + +let set_active_notations ids = + let interp_ids = + HExtlib.filter_map + (function InterpretationId interp_id -> Some interp_id | _ -> None) + ids + in + TermAcicContent.set_active_interpretations interp_ids + diff --git a/helm/ocaml/lexicon/cicNotation.mli b/helm/ocaml/lexicon/cicNotation.mli new file mode 100644 index 000000000..944438df8 --- /dev/null +++ b/helm/ocaml/lexicon/cicNotation.mli @@ -0,0 +1,40 @@ +(* 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 notation_id + +val process_notation: LexiconAst.command -> notation_id list + +val remove_notation: notation_id -> unit + +(** {2 Notation enabling/disabling} + * Right now, only disabling of notation during pretty printing is supporting. + * If it is useful to disable it also for the input phase is still to be + * understood ... *) + +val get_all_notations: unit -> (notation_id * string) list (* id, dsc *) +val get_active_notations: unit -> notation_id list +val set_active_notations: notation_id list -> unit + diff --git a/helm/ocaml/lexicon/disambiguatePp.ml b/helm/ocaml/lexicon/disambiguatePp.ml new file mode 100644 index 000000000..a54e67506 --- /dev/null +++ b/helm/ocaml/lexicon/disambiguatePp.ml @@ -0,0 +1,51 @@ +(* 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 DisambiguateTypes + +let alias_of_domain_and_codomain_items domain_item (dsc,_) = + match domain_item with + 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 + (fun domain_item codomain_item acc -> + alias_of_domain_and_codomain_items domain_item codomain_item::acc + ) env [] + +let aliases_of_domain_and_codomain_items_list l = + List.fold_left + (fun acc (domain_item,codomain_item) -> + alias_of_domain_and_codomain_items domain_item codomain_item::acc + ) [] l + +let pp_environment env = + let aliases = aliases_of_environment env in + let strings = + List.map (fun alias -> LexiconAstPp.pp_alias alias ^ ".") aliases + in + String.concat "\n" (List.sort compare strings) diff --git a/helm/ocaml/lexicon/disambiguatePp.mli b/helm/ocaml/lexicon/disambiguatePp.mli new file mode 100644 index 000000000..e8d9b94a4 --- /dev/null +++ b/helm/ocaml/lexicon/disambiguatePp.mli @@ -0,0 +1,30 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val aliases_of_domain_and_codomain_items_list: + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) 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/lexicon/lexiconAstPp.mli b/helm/ocaml/lexicon/lexiconAstPp.mli new file mode 100644 index 000000000..b7ad59f3c --- /dev/null +++ b/helm/ocaml/lexicon/lexiconAstPp.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val pp_command: LexiconAst.command -> string + +val pp_alias: LexiconAst.alias_spec -> 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/lexicon/lexiconSync.ml b/helm/ocaml/lexicon/lexiconSync.ml new file mode 100644 index 000000000..b6d2270fe --- /dev/null +++ b/helm/ocaml/lexicon/lexiconSync.ml @@ -0,0 +1,117 @@ +(* 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/ + *) + +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.LexiconEngine.aliases in + if description1 <> description2 then + (domain_item,codomain_item)::acc + else + acc + with + Not_found -> + (domain_item,codomain_item)::acc) + 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 + +(** 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 = + fst(List.fold_left ( + fun (acc,i) (name, _, _, cl) -> + (name, UriManager.uri_of_uriref uri i None) :: + (fst(List.fold_left ( + fun (acc,j) (name,_) -> + (((name,UriManager.uri_of_uriref uri i + (Some j)) :: acc) , j+1) + ) (acc,1) cl)),i+1 + ) ([],0) types) + +let build_aliases = + List.map + (fun (name,uri) -> + DisambiguateTypes.Id name, + (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri)) + +let add_aliases_for_inductive_def status types uri = + let aliases = build_aliases (extract_alias types uri) in + 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 + LexiconEngine.set_proof_aliases status new_env + +let add_aliases_for_object status uri = + function + Cic.InductiveDefinition (types,_,_,_) -> + add_aliases_for_inductive_def status types uri + | Cic.Constant _ -> add_alias_for_constant status uri + | Cic.Variable _ + | Cic.CurrentProof _ -> assert false + +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 OrderedId = +struct + type t = CicNotation.notation_id + let compare = Pervasives.compare +end + +module IdSet = Set.Make (OrderedId) + + (** @return l2 \ l1 *) +let id_list_diff l2 l1 = + let module S = IdSet 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 notation_to_remove = + id_list_diff present.LexiconEngine.notation_ids + past.LexiconEngine.notation_ids + in + List.iter CicNotation.remove_notation notation_to_remove + +let init = + { + LexiconEngine.aliases = DisambiguateTypes.Environment.empty; + multi_aliases = DisambiguateTypes.Environment.empty; + lexicon_content_rev = []; + notation_ids = []; + metadata = []; + } diff --git a/helm/ocaml/lexicon/lexiconSync.mli b/helm/ocaml/lexicon/lexiconSync.mli new file mode 100644 index 000000000..62d8b97f5 --- /dev/null +++ b/helm/ocaml/lexicon/lexiconSync.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/ + *) + +val add_aliases_for_objs: + LexiconEngine.status -> UriManager.uri list -> LexiconEngine.status + +val time_travel: + 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:LexiconEngine.status -> LexiconEngine.status -> + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list + +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