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
(string * Cic.term) list -> CicNotationPt.cic_appl_pattern ->
Cic.term
+(* hack. seee cicNotation for explanation *)
+val reset: unit -> unit
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 () =
*)
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
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
CicNotationEnv.t -> CicNotationPt.term ->
CicNotationPt.term
+(* hack. seee cicNotation for explanation *)
+val reset: unit -> unit
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; *)
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 ()
+;;
+
(* 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
module Ast = CicNotationPt
+exception NoInclusionPerformed of string (* full path *)
+
type 'a localized_option =
LSome of 'a
| LNone of GrafiteAst.loc
GrafiteAst.statement
type statement =
+ ?never_include:bool ->
include_paths:string list ->
LexiconEngine.status ->
LexiconEngine.status * ast_statement localized_option
];
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,
(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
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
in
TermAcicContent.set_active_interpretations interp_ids
+let reset () =
+ TermContentPres.reset ();
+ TermAcicContent.reset ()
+;;
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
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
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
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
=
(* 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
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 \
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 \
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
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 \
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 \
PROGRAMS_BYTE = \
matita matitac matitadep matitaclean \
- matitaprover matitawiki
+ matitawiki
PROGRAMS = $(PROGRAMS_BYTE)
PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
NOINST_PROGRAMS = dump_moo
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
$(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
((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 []
;;
(* 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) ->
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
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
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)
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))) ;
| `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
| _ -> ()
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
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
;;
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 =
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
-
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
--- /dev/null
+
+(* 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.
+
+
--- /dev/null
+axiom c : Type.
--- /dev/null
+axiom c : Type.
+axiom x : c === c.
projects / helm.git / commitdiff