From f06968e452cca8782e822d98bec9007404abcbbe Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Jan 2008 10:44:39 +0000 Subject: [PATCH] snopshot (working one!) --- components/acic_content/termAcicContent.ml | 3 +- components/acic_content/termAcicContent.mli | 2 + components/cic/libraryObjects.ml | 18 +++ components/cic/libraryObjects.mli | 4 +- components/content_pres/termContentPres.ml | 3 +- components/content_pres/termContentPres.mli | 2 + components/grafite_engine/grafiteSync.ml | 22 +++- components/grafite_engine/grafiteSync.mli | 10 ++ components/grafite_parser/grafiteParser.ml | 16 ++- components/grafite_parser/grafiteParser.mli | 4 + components/lexicon/cicNotation.ml | 4 + components/lexicon/cicNotation.mli | 7 + components/library/coercDb.ml | 4 + components/library/coercDb.mli | 4 + components/library/librarySync.ml | 23 ++++ components/library/librarySync.mli | 6 +- matita/.depend | 4 +- matita/.depend.opt | 4 +- matita/Makefile | 20 +-- matita/matitaEngine.ml | 94 +++++++------- matita/matitaEngine.mli | 3 +- matita/matitaExcPp.ml | 2 + matita/matitaScript.ml | 82 ++++++------ matita/matitaWiki.ml | 2 +- matita/matitacLib.ml | 66 +++++----- matita/matitaprover.ml | 135 -------------------- matita/matitaprover.mli | 29 ----- matita/tests/depends | 3 + matita/tests/push_pop_status.ma | 95 ++++++++++++++ matita/tests/push_pop_status_aux1.ma | 1 + matita/tests/push_pop_status_aux2.ma | 2 + 31 files changed, 349 insertions(+), 325 deletions(-) delete mode 100644 matita/matitaprover.ml delete mode 100644 matita/matitaprover.mli create mode 100644 matita/tests/push_pop_status.ma create mode 100644 matita/tests/push_pop_status_aux1.ma create mode 100644 matita/tests/push_pop_status_aux2.ma diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml index 681f3cd54..f6b1b68aa 100644 --- a/components/acic_content/termAcicContent.ml +++ b/components/acic_content/termAcicContent.ml @@ -376,8 +376,9 @@ let ast_of_acic ~output_type id_to_sort annterm = debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); ast, term_info.uri +let counter = ref ~-1 +let reset () = counter := ~-1;; let fresh_id = - let counter = ref ~-1 in fun () -> incr counter; !counter diff --git a/components/acic_content/termAcicContent.mli b/components/acic_content/termAcicContent.mli index def5b0a1b..4f366c9c2 100644 --- a/components/acic_content/termAcicContent.mli +++ b/components/acic_content/termAcicContent.mli @@ -68,3 +68,5 @@ val instantiate_appl_pattern: (string * Cic.term) list -> CicNotationPt.cic_appl_pattern -> Cic.term +(* hack. seee cicNotation for explanation *) +val reset: unit -> unit diff --git a/components/cic/libraryObjects.ml b/components/cic/libraryObjects.ml index 7e1dc626f..e402f4db2 100644 --- a/components/cic/libraryObjects.ml +++ b/components/cic/libraryObjects.ml @@ -80,7 +80,25 @@ let reset_defaults () = true_URIs_ref := default_true_URIs; false_URIs_ref := default_false_URIs; absurd_URIs_ref := default_absurd_URIs +;; + +let stack = ref [];; +let push () = + stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref)::!stack; + reset_defaults () +;; + +let pop () = + match !stack with + | [] -> raise (Failure "Unable to POP in libraryObjects.ml") + | (eq,t,f,a)::tl -> + stack := tl; + eq_URIs_ref := eq; + true_URIs_ref := t; + false_URIs_ref := f; + absurd_URIs_ref := a +;; (**** LOOKUP FUNCTIONS ****) let eq_URI () = diff --git a/components/cic/libraryObjects.mli b/components/cic/libraryObjects.mli index bb742f172..b4e19dff8 100644 --- a/components/cic/libraryObjects.mli +++ b/components/cic/libraryObjects.mli @@ -24,8 +24,10 @@ *) val set_default : string -> UriManager.uri list -> unit -val reset_defaults : unit -> unit +val reset_defaults : unit -> unit +val push: unit -> unit +val pop: unit -> unit val eq_URI : unit -> UriManager.uri option diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml index 2fccd4f64..d68b6a8b4 100644 --- a/components/content_pres/termContentPres.ml +++ b/components/content_pres/termContentPres.ml @@ -468,8 +468,9 @@ let fill_pos_info l1_pattern = l1_pattern in aux true l1_pattern *) +let counter = ref ~-1 +let reset () = counter := ~-1;; let fresh_id = - let counter = ref ~-1 in fun () -> incr counter; !counter diff --git a/components/content_pres/termContentPres.mli b/components/content_pres/termContentPres.mli index 5ff710036..77cda8a81 100644 --- a/components/content_pres/termContentPres.mli +++ b/components/content_pres/termContentPres.mli @@ -50,3 +50,5 @@ val instantiate_level2: CicNotationEnv.t -> CicNotationPt.term -> CicNotationPt.term +(* hack. seee cicNotation for explanation *) +val reset: unit -> unit diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml index b02481111..d318d11a7 100644 --- a/components/grafite_engine/grafiteSync.ml +++ b/components/grafite_engine/grafiteSync.ml @@ -133,10 +133,7 @@ let time_travel ~present ~past = List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove; List.iter LibrarySync.remove_obj objs_to_remove -let init baseuri = - LibrarySync.remove_all_coercions (); - LibraryObjects.reset_defaults (); - { +let initial_status baseuri = { GrafiteTypes.moo_content_rev = []; proof_status = GrafiteTypes.No_proof; (* options = GrafiteTypes.no_options; *) @@ -145,3 +142,20 @@ let init baseuri = universe = Universe.empty; baseuri = baseuri; } + + +let init baseuri = + LibrarySync.remove_all_coercions (); + LibraryObjects.reset_defaults (); + initial_status baseuri + ;; +let pop () = + LibrarySync.pop (); + LibraryObjects.pop () +;; + +let push () = + LibrarySync.push (); + LibraryObjects.push () +;; + diff --git a/components/grafite_engine/grafiteSync.mli b/components/grafite_engine/grafiteSync.mli index fbe1fc8db..f66c0e853 100644 --- a/components/grafite_engine/grafiteSync.mli +++ b/components/grafite_engine/grafiteSync.mli @@ -41,3 +41,13 @@ val time_travel: (* also resets the imperative part of the status *) val init: string -> GrafiteTypes.status + +(* + (* just an empty status, does not reset imperative + * part, use push/pop for that *) +val initial_status: string -> GrafiteTypes.status +*) + + (* preserve _only_ imperative parts of the status *) +val push: unit -> unit +val pop: unit -> unit diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index c948272ef..df18135ac 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -30,6 +30,8 @@ let set_callback f = out := f module Ast = CicNotationPt +exception NoInclusionPerformed of string (* full path *) + type 'a localized_option = LSome of 'a | LNone of GrafiteAst.loc @@ -41,6 +43,7 @@ type ast_statement = GrafiteAst.statement type statement = + ?never_include:bool -> include_paths:string list -> LexiconEngine.status -> LexiconEngine.status * ast_statement localized_option @@ -687,17 +690,18 @@ EXTEND ]; statement: [ [ ex = executable -> - fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex)) + fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex)) | com = comment -> - fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) + fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> - fun ~include_paths status -> + fun ?(never_include=false) ~include_paths status -> let _root, buri, fullpath, _rrelpath = Librarian.baseuri_of_script ~include_paths fname in let status = - LexiconEngine.eval_command status - (LexiconAst.Include (iloc,buri,mode,fullpath)) + if never_include then raise (NoInclusionPerformed fullpath) + else LexiconEngine.eval_command status + (LexiconAst.Include (iloc,buri,mode,fullpath)) in !out fname; status, @@ -706,7 +710,7 @@ EXTEND (loc,GrafiteAst.Command (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> - fun ~include_paths status -> + fun ?(never_include=false) ~include_paths status -> let status = LexiconEngine.eval_command status scom in status,LNone loc | EOI -> raise End_of_file diff --git a/components/grafite_parser/grafiteParser.mli b/components/grafite_parser/grafiteParser.mli index f8754df0c..47f0af02b 100644 --- a/components/grafite_parser/grafiteParser.mli +++ b/components/grafite_parser/grafiteParser.mli @@ -33,7 +33,11 @@ type ast_statement = CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement +exception NoInclusionPerformed of string (* full path *) + type statement = + ?never_include:bool -> + (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *) include_paths:string list -> LexiconEngine.status -> LexiconEngine.status * ast_statement localized_option diff --git a/components/lexicon/cicNotation.ml b/components/lexicon/cicNotation.ml index d514c0273..bea67a0b4 100644 --- a/components/lexicon/cicNotation.ml +++ b/components/lexicon/cicNotation.ml @@ -96,3 +96,7 @@ let set_active_notations ids = in TermAcicContent.set_active_interpretations interp_ids +let reset () = + TermContentPres.reset (); + TermAcicContent.reset () +;; diff --git a/components/lexicon/cicNotation.mli b/components/lexicon/cicNotation.mli index 00b34babe..81b01aa45 100644 --- a/components/lexicon/cicNotation.mli +++ b/components/lexicon/cicNotation.mli @@ -38,3 +38,10 @@ 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 +(* resets internal couenters. this is an hack used in matitaScript. + * if you are in the middle of a script (with an history you may use to undo + * with some notations id inside) and you want to compile an external file + * in an empty environment you need, after its compilation, to restore + * the previous environment (re-executing all notations commands) and this must + * produce the same ids as before, otherwise history is wrong. *) + val reset: unit -> unit diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml index 0ca40eb1c..80222ad34 100644 --- a/components/library/coercDb.ml +++ b/components/library/coercDb.ml @@ -190,3 +190,7 @@ let add_coercion (src,tgt,u,saturations) = db := (src,tgt,(u,1,saturations)::l)::tl @ rest ;; + +type coerc_db = (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list +let dump () = !db +let restore coerc_db = db := coerc_db diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli index e1afd61aa..3071aecc4 100644 --- a/components/library/coercDb.mli +++ b/components/library/coercDb.mli @@ -50,6 +50,10 @@ val to_list: unit -> (coerc_carr * coerc_carr * (UriManager.uri * int) list) list +type coerc_db +val dump: unit -> coerc_db +val restore: coerc_db -> unit + val add_coercion: coerc_carr * coerc_carr * UriManager.uri * int -> unit diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index c36d84c90..630b51be8 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -243,6 +243,29 @@ let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; CoercDb.remove_coercion (fun (_,_,_,_) -> true) +let stack = ref [];; + +let h2l h = + UriManager.UriHashtbl.fold + (fun k v acc -> (k,v) :: acc) h [] +;; + +let push () = + stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack; + remove_all_coercions () +;; + +let pop () = + match !stack with + | [] -> raise (Failure "Unable to POP from librarySync.ml") + | (db,h) :: tl -> + stack := tl; + remove_all_coercions (); + CoercDb.restore db; + List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v) + h +;; + let add_coercion ~add_composites refinement_toolkit uri arity saturations baseuri = diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli index d8e432e75..9dd3f5c3c 100644 --- a/components/library/librarySync.mli +++ b/components/library/librarySync.mli @@ -57,6 +57,8 @@ val add_coercion: (* coercions and the information that [uri] and the composites are coercion *) val remove_coercion: UriManager.uri -> unit -(* mh... *) +(* this is used when resetting, but the more gracefull push/pop can be used to + * suspend/resume an execution *) val remove_all_coercions: unit -> unit - +val push: unit -> unit +val pop: unit -> unit diff --git a/matita/.depend b/matita/.depend index 84e4f1d2e..3d42927cd 100644 --- a/matita/.depend +++ b/matita/.depend @@ -22,8 +22,8 @@ matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi matitaEngine.cmx: matitaEngine.cmi -matitaExcPp.cmo: matitaExcPp.cmi -matitaExcPp.cmx: matitaExcPp.cmi +matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi +matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ diff --git a/matita/.depend.opt b/matita/.depend.opt index d8ff0ac75..44da8ef2b 100644 --- a/matita/.depend.opt +++ b/matita/.depend.opt @@ -22,8 +22,8 @@ matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi matitaEngine.cmx: matitaEngine.cmi -matitaExcPp.cmo: matitaExcPp.cmi -matitaExcPp.cmx: matitaExcPp.cmi +matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi +matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ diff --git a/matita/Makefile b/matita/Makefile index 4e42f2c43..a9cf7141d 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -19,7 +19,7 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS) INSTALL_PROGRAMS= matita matitac INSTALL_PROGRAMS_LINKS_MATITA= -INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitaclean matitaprover matitawiki +INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitaclean matitawiki MATITA_FLAGS = -noprofile NODB=false @@ -31,13 +31,12 @@ MLI = \ lablGraphviz.mli \ matitaTypes.mli \ matitaMisc.mli \ + matitaEngine.mli \ matitaExcPp.mli \ matitaInit.mli \ - matitaEngine.mli \ applyTransformation.mli \ matitaAutoGui.mli \ matitacLib.mli \ - matitaprover.mli \ matitaGtkMisc.mli \ matitaScript.mli \ matitaMathView.mli \ @@ -46,13 +45,12 @@ MLI = \ CMLI = \ matitaTypes.mli \ matitaMisc.mli \ + matitaEngine.mli \ matitaExcPp.mli \ matitaInit.mli \ - matitaEngine.mli \ applyTransformation.mli \ matitacLib.mli \ matitaWiki.mli \ - matitaprover.mli \ $(NULL) MAINCMLI = \ matitadep.mli \ @@ -66,7 +64,7 @@ MAINCML = $(MAINCMLI:%.mli=%.ml) PROGRAMS_BYTE = \ matita matitac matitadep matitaclean \ - matitaprover matitawiki + matitawiki PROGRAMS = $(PROGRAMS_BYTE) PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) NOINST_PROGRAMS = dump_moo @@ -143,11 +141,6 @@ rottener.opt: rottener.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) clean-rottened: find . -type f -name "*.ma.*.rottened" -exec rm {} \; -matitaprover: matitac - $(H)test -f $@ || ln -s $< $@ -matitaprover.opt: matitac.opt - $(H)test -f $@ || ln -s $< $@ - matitadep: matitac $(H)test -f $@ || ln -s $< $@ matitadep.opt: matitac.opt @@ -345,11 +338,6 @@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \ $(STATIC_EXTRA_CLIBS) strip $@ -matitaprover.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml - $(STATIC_LINK) $(STATIC_CLIBS_PROVER) -- \ - $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \ - $(STATIC_EXTRA_CLIBS); - strip $@ matitadep.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ matitaclean.opt.static: matitac.opt.static diff --git a/matita/matitaEngine.ml b/matita/matitaEngine.ml index 7ca67976a..5f8a1b7a7 100644 --- a/matita/matitaEngine.ml +++ b/matita/matitaEngine.ml @@ -98,62 +98,66 @@ let eval_ast ?do_heavy_checks lexicon_status ((new_grafite_status,new_lexicon_status),None)::intermediate_states exception TryingToAdd of string +exception EnrichedWithLexiconStatus of exn * LexiconEngine.status let out = ref ignore let set_callback f = out := f -let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) +let eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb = let rec loop lexicon_status grafite_status statuses = let loop = - if first_statement_only then - fun _ _ statuses -> statuses - else - loop + if first_statement_only then fun _ _ statuses -> statuses + else loop in - if prompt then (print_string "matita> "; flush stdout); - let cont = - try - Some (GrafiteParser.parse_statement ~include_paths str lexicon_status) - with - End_of_file -> None - in - match cont with - | None -> statuses - | Some (lexicon_status,ast) -> - (match ast with - GrafiteParser.LNone _ -> - watch_statuses lexicon_status grafite_status ; - loop lexicon_status grafite_status - (((grafite_status,lexicon_status),None)::statuses) - | GrafiteParser.LSome ast -> - !out ast; - cb grafite_status ast; - let new_statuses = - eval_ast ?do_heavy_checks lexicon_status - grafite_status ("",0,ast) in - if enforce_no_new_aliases then - List.iter - (fun (_,alias) -> - match alias with - None -> () - | Some (k,((v,_) as value)) -> - let newtxt = - DisambiguatePp.pp_environment - (DisambiguateTypes.Environment.add k value - DisambiguateTypes.Environment.empty) - in - raise (TryingToAdd newtxt)) new_statuses; - let grafite_status,lexicon_status = - match new_statuses with - [] -> assert false - | (s,_)::_ -> s - in - watch_statuses lexicon_status grafite_status ; - loop lexicon_status grafite_status (new_statuses @ statuses)) + let stop,l,g,s = + try + let cont = + try + Some (GrafiteParser.parse_statement ~include_paths str lexicon_status) + with + End_of_file -> None + in + match cont with + | None -> true, lexicon_status, grafite_status, statuses + | Some (lexicon_status,ast) -> + (match ast with + GrafiteParser.LNone _ -> + watch_statuses lexicon_status grafite_status ; + false, lexicon_status, grafite_status, + (((grafite_status,lexicon_status),None)::statuses) + | GrafiteParser.LSome ast -> + !out ast; + cb grafite_status ast; + let new_statuses = + eval_ast ?do_heavy_checks lexicon_status + grafite_status ("",0,ast) in + if enforce_no_new_aliases then + List.iter + (fun (_,alias) -> + match alias with + None -> () + | Some (k,((v,_) as value)) -> + let newtxt = + DisambiguatePp.pp_environment + (DisambiguateTypes.Environment.add k value + DisambiguateTypes.Environment.empty) + in + raise (TryingToAdd newtxt)) new_statuses; + let grafite_status,lexicon_status = + match new_statuses with + [] -> assert false + | (s,_)::_ -> s + in + watch_statuses lexicon_status grafite_status ; + false, lexicon_status, grafite_status, (new_statuses @ statuses)) + with exn -> + raise (EnrichedWithLexiconStatus (exn, lexicon_status)) + in + if stop then s else loop l g s in loop lexicon_status grafite_status [] ;; diff --git a/matita/matitaEngine.mli b/matita/matitaEngine.mli index 1db991f51..bb4537d8d 100644 --- a/matita/matitaEngine.mli +++ b/matita/matitaEngine.mli @@ -39,12 +39,13 @@ val eval_ast : (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) +exception EnrichedWithLexiconStatus of exn * LexiconEngine.status + (* should be used only by the compiler since it looses the * disambiguation_context (text,prefix_len,_) *) val eval_from_stream : first_statement_only:bool -> include_paths:string list -> - ?prompt:bool -> ?do_heavy_checks:bool -> ?enforce_no_new_aliases:bool -> (* default true *) ?watch_statuses:(LexiconEngine.status -> GrafiteTypes.status -> unit) -> diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml index 14e7a0db8..24981af6b 100644 --- a/matita/matitaExcPp.ml +++ b/matita/matitaExcPp.ml @@ -147,6 +147,8 @@ let rec to_string = None, "Already defined: " ^ UriManager.string_of_uri s | CoercDb.EqCarrNotImplemented msg -> None, ("EqCarrNotImplemented: " ^ Lazy.force msg) + | MatitaEngine.EnrichedWithLexiconStatus (exn,_) -> + None, "EnrichedWithLexiconStatus "^snd(to_string exn) | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> let loc = match errorll with diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 1a7c86bb8..828002a8b 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -71,7 +71,7 @@ type guistuff = { ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } -let eval_with_engine guistuff lexicon_status grafite_status user_goal +let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt st = let module TAPp = GrafiteAstPp in @@ -102,36 +102,48 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal res,"",parsed_text_length ;; -let wrap_with_make include_paths g f x = +(* this function calls the parser in a way that it does not perform inclusions, + * so that we can ensure the inclusion is performed after the included file + * is compiled (if needed). matitac does not need that, since it compiles files + * in the good order, here files may be compiled on demand. *) +let wrap_with_make include_paths (f : GrafiteParser.statement) x = try - f x + f ~never_include:true ~include_paths x with - | LexiconEngine.IncludedFileNotCompiled (xfilename,mafilename) - | GrafiteEngine.IncludedFileNotCompiled (xfilename,mafilename) as exn -> - assert (Pcre.pmatch ~pat:"ma$" mafilename); - assert (Pcre.pmatch ~pat:"lexicon$" xfilename || - Pcre.pmatch ~pat:"mo$" xfilename ); - (* we know that someone was able to include the .ma, get the baseuri - * but was unable to get the compilation output 'xfilename' *) + | GrafiteParser.NoInclusionPerformed mafilename -> let root, buri, _, tgt = + try Librarian.baseuri_of_script ~include_paths mafilename + with Librarian.NoRootFor _ -> + HLog.error ("The included file '"^mafilename^"' has no root file,"); + HLog.error "please create it."; + raise (Failure ("No root file for "^mafilename)) + in + let initial_lexicon_status = + CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script + in + let b,x = try - Librarian.baseuri_of_script ~include_paths mafilename - with Librarian.NoRootFor _ -> raise exn + GrafiteSync.push (); + LexiconSync.time_travel ~present:x ~past:initial_lexicon_status; + let rc = MatitacLib.Make.make root [tgt] in + GrafiteSync.pop (); + CicNotation.reset (); + ignore(CicNotation2.load_notation ~include_paths:[] + BuildTimeConf.core_notation_script); + let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c) + initial_lexicon_status (List.rev + x.LexiconEngine.lexicon_content_rev) + in + rc,x + with + | exn -> + HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn)); + assert false in - if MatitacLib.Make.make root [tgt] then f x + if b then f ~include_paths x else raise (Failure ("Compiling: " ^ tgt)) ;; -let eval_with_engine include_paths - guistuff lexicon_status grafite_status user_goal - skipped_txt nonskipped_txt st -= - wrap_with_make include_paths guistuff - (eval_with_engine - guistuff lexicon_status grafite_status user_goal - skipped_txt nonskipped_txt) st -;; - let pp_eager_statement_ast = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) @@ -588,25 +600,6 @@ script ex loc let module MD = GrafiteDisambiguator in let module ML = MatitaMisc in try - begin - match ex with - | TA.Command (_,TA.Set (_,"baseuri",u)) -> - if Http_getter_storage.is_read_only u then - raise (ActionCancelled ("baseuri " ^ u ^ " is readonly")); - if not (Http_getter_storage.is_empty ~local:true u) then - (match - guistuff.ask_confirmation - ~title:"Baseuri redefinition" - ~message:( - "Baseuri " ^ u ^ " already exists.\n" ^ - "Do you want to redefine the corresponding "^ - "part of the library?") - with - | `YES -> LibraryClean.clean_baseuris [u] - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel) - | _ -> () - end; ignore (buffer#move_mark (`NAME "beginning_of_statement") ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars (Glib.Utf8.length skipped_txt))) ; @@ -632,9 +625,8 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; let ast = - wrap_with_make include_paths guistuff - (GrafiteParser.parse_statement - (Ulexing.from_utf8_string text) ~include_paths) lexicon_status + wrap_with_make include_paths + (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status in ast, text | `Ast (st, text) -> (lexicon_status, st), text diff --git a/matita/matitaWiki.ml b/matita/matitaWiki.ml index 08f683cbf..87e9a4417 100644 --- a/matita/matitaWiki.ml +++ b/matita/matitaWiki.ml @@ -170,7 +170,7 @@ let rec interactive_loop () = | _ -> () in run_script str - (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false + (MatitaEngine.eval_from_stream ~first_statement_only:true ~include_paths:(Lazy.force include_paths) ~watch_statuses) ; interactive_loop (Some (List.length !lexicon_status)) with diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 51834f6e7..5495a6f78 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -200,46 +200,47 @@ let rec compile options fname = LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; true) with - | End_of_file -> - HLog.error "End_of_file"; - pp_times fname false big_bang; - clean_exit baseuri false + (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *) | AttemptToInsertAnAlias lexicon_status -> + pp_times fname false big_bang; + LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; + clean_exit baseuri false + | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) -> + (match exn with + | Sys.Break -> HLog.error "user break!" + | GrafiteEngine.Macro (floc, f) -> + (try + match f (get_macro_context (Some grafite_status)) with + | _, GrafiteAst.Inline (_, style, suri, prefix) -> + let str = + ApplyTransformation.txt_of_inline_macro style suri prefix + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") in + (* the output of compilation is wrong in this way!! *) + !out str; ignore(compile options fname) + | _ -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error (sprintf "A macro has been found at %d-%d" x y) + with exn -> HLog.error (snd (MatitaExcPp.to_string exn))) + | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> + let (x, y) = HExtlib.loc_of_floc floc in + HLog.error (sprintf "Parse error at %d-%d: %s" x y err) + | exn -> HLog.error (snd (MatitaExcPp.to_string exn))); + LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status; pp_times fname false big_bang; - LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; clean_exit baseuri false + | End_of_file -> (* this is CSC stuff ... or can only happen on empty files *) + HLog.error "End_of_file"; + pp_times fname false big_bang; + clean_exit baseuri false | Sys.Break as exn -> if matita_debug then raise exn; HLog.error "user break!"; pp_times fname false big_bang; clean_exit baseuri false - | GrafiteEngine.Macro (floc, f) -> - (try - match f (get_macro_context (Some grafite_status)) with - | _, GrafiteAst.Inline (_, style, suri, prefix) -> - let str = - ApplyTransformation.txt_of_inline_macro style suri prefix - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") in - !out str; - compile options fname - | _ -> - let x, y = HExtlib.loc_of_floc floc in - HLog.error (sprintf "A macro has been found at %d-%d" x y); - pp_times fname false big_bang; - clean_exit baseuri false - with exn -> - HLog.error (snd (MatitaExcPp.to_string exn)); - pp_times fname false big_bang; - clean_exit baseuri false) - | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> - let (x, y) = HExtlib.loc_of_floc floc in - HLog.error (sprintf "Parse error at %d-%d: %s" x y err); - pp_times fname false big_bang; - clean_exit baseuri false | exn -> if matita_debug then raise exn; - HLog.error (snd (MatitaExcPp.to_string exn)); + HLog.error ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn)); pp_times fname false big_bang; clean_exit baseuri false ;; @@ -268,10 +269,7 @@ module F = let mtime_of_source_object s = try Some (Unix.stat s).Unix.st_mtime - with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> - None -(* max_float *) -(* raise (Failure ("Unable to stat a source file: " ^ s)) *) + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None ;; let mtime_of_target_object s = diff --git a/matita/matitaprover.ml b/matita/matitaprover.ml deleted file mode 100644 index 79ab7683b..000000000 --- a/matita/matitaprover.ml +++ /dev/null @@ -1,135 +0,0 @@ -(* Copyright (C) 2006, 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 raw_preamble buri = " -inductive eq (A:Type) (x:A) : A \\to Prop \\def refl_eq : eq A x x. - -theorem sym_eq : \\forall A:Type.\\forall x,y:A. eq A x y \\to eq A y x. -intros.elim H. apply refl_eq. -qed. - -theorem eq_elim_r: - \\forall A:Type.\\forall x:A. \\forall P: A \\to Prop. - P x \\to \\forall y:A. eq A y x \\to P y. -intros. elim (sym_eq ? ? ? H1).assumption. -qed. - -theorem trans_eq : - \\forall A:Type.\\forall x,y,z:A. eq A x y \\to eq A y z \\to eq A x z. -intros.elim H1.assumption. -qed. - -default \"equality\" - " ^ buri ^ "/eq.ind - " ^ buri ^ "/sym_eq.con - " ^ buri ^ "/trans_eq.con - " ^ buri ^ "/eq_ind.con - " ^ buri ^ "/eq_elim_r.con - " ^ buri ^ "/eq_f.con - " ^ buri ^ "/eq_f1.con. - -theorem eq_f: \\forall A,B:Type.\\forall f:A\\to B. - \\forall x,y:A. eq A x y \\to eq B (f x) (f y). -intros.elim H.reflexivity. -qed. - -theorem eq_f1: \\forall A,B:Type.\\forall f:A\\to B. - \\forall x,y:A. eq A x y \\to eq B (f y) (f x). -intros.elim H.reflexivity. -qed. - -inductive ex (A:Type) (P:A \\to Prop) : Prop \\def - ex_intro: \\forall x:A. P x \\to ex A P. -interpretation \"exists\" 'exists \\eta.x = - (" ^ buri ^ "/ex.ind#xpointer(1/1) _ x). - -notation < \"hvbox(\\exists ident i opt (: ty) break . p)\" - right associative with precedence 20 -for @{ 'exists ${default - @{\\lambda ${ident i} : $ty. $p)} - @{\\lambda ${ident i} . $p}}}. - -" -;; - -let p_to_ma ?timeout ~tptppath ~filename () = - let data = - Tptp2grafite.tptp2grafite ?timeout ~filename ~tptppath:tptppath - ~raw_preamble () - in - data -;; - -let main () = - let tptppath = ref "./" in - let timeout = ref 600 in - MatitaInit.add_cmdline_spec - ["-tptppath",Arg.String (fun s -> tptppath:= s), - "Where to find the Axioms/ and Problems/ directory"; - "-timeout", Arg.Int (fun x -> timeout := x), - "Timeout in seconds"]; - MatitaInit.parse_cmdline_and_configuration_file (); - Helm_registry.set_bool "matita.nodisk" true; - HLog.set_log_callback (fun _ _ -> ()); - let args = Helm_registry.get_list Helm_registry.string "matita.args" in - let inputfile = - match args with - | [file] -> file - | _ -> prerr_endline "You must specify exactly one .p file."; exit 1 - in - let data = - p_to_ma ~timeout:!timeout ~filename:inputfile ~tptppath:!tptppath () - in -(* prerr_endline data; *) - let is = Ulexing.from_utf8_string data in - let gs = GrafiteSync.init "cic:/TPTP/" in - let ls = - CicNotation2.load_notation ~include_paths:[] - BuildTimeConf.core_notation_script - in - Sys.catch_break true; - try - let _ = - MatitaEngine.eval_from_stream - ~first_statement_only:false - ~include_paths:[] - ~do_heavy_checks:false - ~prompt:false - ls gs is - (fun _ _ -> ()) -(* - (fun _ s -> - let pp_ast_statement = - GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj - in - prerr_endline (pp_ast_statement s)) -*) - in - exit 0 - with exn -> - prerr_endline (snd (MatitaExcPp.to_string exn)); - exit 1 -;; diff --git a/matita/matitaprover.mli b/matita/matitaprover.mli deleted file mode 100644 index e0b9cbf0b..000000000 --- a/matita/matitaprover.mli +++ /dev/null @@ -1,29 +0,0 @@ -(* Copyright (C) 2006, 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 main: unit -> unit - -val p_to_ma: ?timeout:int -> tptppath:string -> filename:string -> unit -> string - diff --git a/matita/tests/depends b/matita/tests/depends index 9ae9703ec..200a4088c 100644 --- a/matita/tests/depends +++ b/matita/tests/depends @@ -29,10 +29,13 @@ coercions_open.ma logic/equality.ma nat/nat.ma match_inference.ma hard_refine.ma coq.ma fix_betareduction.ma coq.ma +push_pop_status_aux1.ma +push_pop_status.ma push_pop_status_aux1.ma decl.ma nat/orders.ma nat/times.ma pullback.ma mysql_escaping.ma rewrite.ma coq.ma +push_pop_status_aux2.ma injection.ma coq.ma contradiction.ma coq.ma fold.ma coq.ma diff --git a/matita/tests/push_pop_status.ma b/matita/tests/push_pop_status.ma new file mode 100644 index 000000000..a885f4e9d --- /dev/null +++ b/matita/tests/push_pop_status.ma @@ -0,0 +1,95 @@ + +(* XXX coercions *) +axiom A: Type. +axiom B: Type. +axiom cAB: A -> B. +coercion cic:/matita/tests/push_pop_status/cAB.con. + +inductive eq (A:Type) (x:A) : A \to Prop \def + refl_eq : eq A x x. + +(* XXX notation *) +notation "hvbox(a break === b)" non associative with precedence 45 for @{ 'eqqq $a $b }. +interpretation "test" 'eqqq x y = (cic:/matita/tests/push_pop_status/eq.ind#xpointer(1/1) _ x y). + +theorem eq_rect': + \forall A. \forall x:A. \forall P: \forall y:A. x===y \to Type. + P ? (refl_eq ? x) \to \forall y:A. \forall p:x===y. P y p. + intros. + exact + (match p1 return \lambda y. \lambda p.P y p with + [refl_eq \Rightarrow p]). +qed. + +lemma sym_eq : \forall A:Type.\forall x,y:A. x===y \to y===x. +intros.elim H. apply refl_eq. +qed. + +lemma trans_eq : \forall A:Type.\forall x,y,z:A. x===y \to y===z \to x===z. +intros.elim H1.assumption. +qed. + +theorem eq_elim_r: + \forall A:Type.\forall x:A. \forall P: A \to Prop. + P x \to \forall y:A. y===x \to P y. +intros. elim (sym_eq ? ? ? H1).assumption. +qed. + +theorem eq_elim_r': + \forall A:Type.\forall x:A. \forall P: A \to Set. + P x \to \forall y:A. y===x \to P y. +intros. elim (sym_eq ? ? ? H).assumption. +qed. + +theorem eq_elim_r'': + \forall A:Type.\forall x:A. \forall P: A \to Type. + P x \to \forall y:A. y===x \to P y. +intros. elim (sym_eq ? ? ? H).assumption. +qed. + +theorem eq_f: \forall A,B:Type.\forall f:A\to B. +\forall x,y:A. x===y \to f x === f y. +intros.elim H.apply refl_eq. +qed. + +theorem eq_f': \forall A,B:Type.\forall f:A\to B. +\forall x,y:A. x===y \to f y === f x. +intros.elim H.apply refl_eq. +qed. + +(* XXX defaults *) +default "equality" + cic:/matita/tests/push_pop_status/eq.ind + cic:/matita/tests/push_pop_status/sym_eq.con + cic:/matita/tests/push_pop_status/trans_eq.con + cic:/matita/tests/push_pop_status/eq_ind.con + cic:/matita/tests/push_pop_status/eq_elim_r.con + cic:/matita/tests/push_pop_status/eq_rec.con + cic:/matita/tests/push_pop_status/eq_elim_r'.con + cic:/matita/tests/push_pop_status/eq_rect.con + cic:/matita/tests/push_pop_status/eq_elim_r''.con + cic:/matita/tests/push_pop_status/eq_f.con + cic:/matita/tests/push_pop_status/eq_f'.con. (* \x.sym (eq_f x) *) + +include "push_pop_status_aux1.ma". +(* include "push_pop_status_aux2.ma". *) + +(* XXX default *) +theorem prova: \forall x:A. eq A x x. +intros. reflexivity. +qed. + +(* XXX notation *) +theorem prova1: \forall x:A. x === x. +intros. apply refl_eq. +qed. + +(* XXX coercion *) +theorem pippo: A -> B. +intro a. +apply (a : B). +qed. + +definition X := b. + + diff --git a/matita/tests/push_pop_status_aux1.ma b/matita/tests/push_pop_status_aux1.ma new file mode 100644 index 000000000..80e9a2f63 --- /dev/null +++ b/matita/tests/push_pop_status_aux1.ma @@ -0,0 +1 @@ +axiom c : Type. diff --git a/matita/tests/push_pop_status_aux2.ma b/matita/tests/push_pop_status_aux2.ma new file mode 100644 index 000000000..4799d5ba1 --- /dev/null +++ b/matita/tests/push_pop_status_aux2.ma @@ -0,0 +1,2 @@ +axiom c : Type. +axiom x : c === c. -- 2.39.2