From: Enrico Tassi Date: Mon, 15 Jun 2009 16:22:18 +0000 (+0000) Subject: EXPERIMENTAL COMMIT (by CSC,actuall :-) X-Git-Tag: make_still_working~3868 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c8de084e314e41f3dc2f605f6242283e930b803;p=helm.git EXPERIMENTAL COMMIT (by CSC,actuall :-) This commit partially implements (in NCicLibrary) serialization for NG. It creates several .matita/matita/.../foo.ng files that are ocaml dumps of closures (NRstatus.refiner_status -> NRstatus.refiner_status) to be applied to the current status. The test tests/ng_includeB.ma shows how unification hints are preserved. TODO: a) decompilation is implemented in NCicLibrary, but not called anywhere b) serialization of objects (and "query" db (and old to new cache??)) not implemented yet c) objects are removed from the library, but not from the environment! --- diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index efadc681e..f17459162 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 1e777ab83..9b454f294 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -471,8 +471,16 @@ let coercion_moo_statement_of (uri,arity, saturations,_) = (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations) let eval_unification_hint status t n = - (* XXX no undo *) - NCicUnifHint.add_user_provided_hint t n; + let aux status = + let hstatus = + NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n + in + { status with NRstatus.uhint_db = hstatus } in + let rstatus = aux (GrafiteTypes.get_rstatus status) in + let status = GrafiteTypes.set_rstatus rstatus status in + let dump = GrafiteTypes.get_dump status in + let dump = fun status -> aux (dump status) in + let status = GrafiteTypes.set_dump dump status in status,`Old [] ;; @@ -726,6 +734,10 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status raise (IncludedFileNotCompiled (moopath_rw,baseuri)) in let status = eval_from_moo.efm_go status moopath in + let rstatus = GrafiteTypes.get_rstatus status in + let rstatus = + NCicLibrary.require ~baseuri:(NUri.uri_of_string baseuri) rstatus in + let status = GrafiteTypes.set_rstatus rstatus status in (* debug let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in @@ -785,20 +797,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in let obj = uri,height,[],[],obj_kind in NCicTypeChecker.typecheck_obj obj; - NCicLibrary.add_obj uri obj; + let timestamp = NCicLibrary.add_obj uri obj in let objs = NCicElim.mk_elims obj in - let uris = - uri:: - List.map - (fun (uri,_,_,_,_) as obj -> + let timestamp,uris_rev = + List.fold_left + (fun (timestamp,uris_rev) (uri,_,_,_,_) as obj -> NCicTypeChecker.typecheck_obj obj; - NCicLibrary.add_obj uri obj; - uri - ) objs - in - {status with - GrafiteTypes.ng_status = - GrafiteTypes.CommandMode estatus },`New uris + let timestamp = NCicLibrary.add_obj uri obj in + timestamp,uri::uris_rev + ) (timestamp,[]) objs in + let uris = uri::List.rev uris_rev in + GrafiteTypes.set_library_db timestamp + {status with + GrafiteTypes.ng_status = + GrafiteTypes.CommandMode estatus },`New uris | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index a773ea401..60bfc6921 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -171,6 +171,7 @@ let time_travel ~present ~past = uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in List.iter LibrarySync.remove_obj objs_to_remove; CoercDb.restore past.GrafiteTypes.coercions; + NCicLibrary.time_travel (GrafiteTypes.get_library_db past) ;; let initial_status lexicon_status baseuri = { @@ -185,6 +186,8 @@ let initial_status lexicon_status baseuri = { NEstatus.rstatus = { NRstatus.uhint_db = NCicUnifHint.empty_db; NRstatus.coerc_db = NCicCoercion.empty_db; + NRstatus.library_db = NCicLibrary.time0; + NRstatus.dump = fun x -> x; }; } } diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 2ee136dfe..6a57c4a00 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -100,6 +100,48 @@ let get_estatus x = | CommandMode e -> e ;; +let set_estatus e x = + { x with ng_status = + match x.ng_status with + ProofMode t -> + ProofMode + {t with NTacStatus.istatus = + {t.NTacStatus.istatus with NTacStatus.estatus = e}} + | CommandMode _ -> CommandMode e} +;; + +let get_rstatus x = (get_estatus x).NEstatus.rstatus;; + +let get_hstatus x = (get_rstatus x).NRstatus.uhint_db;; + +let get_library_db x = (get_rstatus x).NRstatus.library_db;; + +let get_dump x = (get_rstatus x).NRstatus.dump;; + +let set_rstatus h x = + let estatus = get_estatus x in + set_estatus { estatus with NEstatus.rstatus = h } x +;; + +let set_hstatus h x = + let rstatus = get_rstatus x in + set_rstatus { rstatus with NRstatus.uhint_db = h} x +;; + +let set_library_db h x = + let rstatus = get_rstatus x in + set_rstatus { rstatus with NRstatus.library_db = h} x +;; + +let set_dump h x = + let estatus = get_estatus x in + set_estatus + { estatus with NEstatus.rstatus = + { estatus.NEstatus.rstatus with + NRstatus.dump = h}} + x +;; + let get_current_proof status = match status.proof_status with | Incomplete_proof { proof = p } -> p diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index c874d43f6..4d693ea6b 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -75,10 +75,19 @@ val get_proof_context : status -> int -> Cic.context val get_proof_conclusion : status -> int -> Cic.term val get_lexicon : status -> LexiconEngine.status val get_estatus : status -> NEstatus.extra_status +val get_rstatus : status -> NRstatus.refiner_status +val get_hstatus : status -> NCicUnifHint.db +val get_library_db : status -> NCicLibrary.timestamp +val get_dump : status -> (NRstatus.refiner_status -> NRstatus.refiner_status) val get_coercions: status -> NCicCoercion.db val set_stack: Continuationals.Stack.t -> status -> status val set_metasenv: Cic.metasenv -> status -> status val set_lexicon : LexiconEngine.status -> status -> status val set_coercions: NCicCoercion.db -> status -> status +val set_estatus : NEstatus.extra_status -> status -> status +val set_rstatus : NRstatus.refiner_status -> status -> status +val set_hstatus : NCicUnifHint.db -> status -> status +val set_library_db : NCicLibrary.timestamp -> status -> status +val set_dump : (NRstatus.refiner_status -> NRstatus.refiner_status) -> status -> status diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index e2d800157..8c988de2f 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -12,10 +12,19 @@ (* $Id$ *) exception ObjectNotFound of string Lazy.t +exception LibraryOutOfSync of string Lazy.t -let storage = ref [];; +type timestamp = + (NUri.uri * NCic.obj) list * + (NUri.uri * string * NReference.reference) list * + NCic.obj NUri.UriMap.t;; +let time0 = [],[],NUri.UriMap.empty;; +let storage = ref [];; let aliases = ref [];; +let cache = ref NUri.UriMap.empty;; + +let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;; let resolve name = try @@ -63,28 +72,56 @@ let add_obj u obj = (NReference.Ind (inductive,i,leftno))] ) il) in - aliases := references @ !aliases + aliases := references @ !aliases; + !storage,!aliases,!cache ;; -let cache = NUri.UriHash.create 313;; - let get_obj u = try List.assq u !storage with Not_found -> - try NUri.UriHash.find cache u + try NUri.UriMap.find u !cache with Not_found -> (* in the final implementation should get it from disk *) let ouri = NCic2OCic.ouri_of_nuri u in try let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in let l = OCic2NCic.convert_obj ouri o in - List.iter (fun (u,_,_,_,_ as o) -> - (* prerr_endline ("+"^NUri.string_of_uri u); *) - NUri.UriHash.add cache u o) l; + List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l; HExtlib.list_last l with CicEnvironment.Object_not_found u -> raise (ObjectNotFound (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u)))) ;; -let clear_cache () = NUri.UriHash.clear cache;; +let clear_cache () = cache := NUri.UriMap.empty;; + +let magic = 0;; + +let path_of_baseuri baseuri = + let uri = NUri.string_of_uri baseuri in + let path = String.sub uri 4 (String.length uri - 4) in + let path = Helm_registry.get "matita.basedir" ^ path in + let dirname = Filename.dirname path in + HExtlib.mkdir dirname; + path ^ ".ng" +;; + +let serialize ~baseuri dump = + let ch = open_out (path_of_baseuri baseuri) in + Marshal.to_channel ch (magic,dump) [Marshal.Closures]; + close_out ch +;; + +let require ~baseuri = + let ch = open_in (path_of_baseuri baseuri) in + let mmagic,dump = Marshal.from_channel ch in + close_in ch; + if mmagic <> magic then + raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library.")) + else + dump +;; + +let decompile ~baseuri = + Unix.unlink (path_of_baseuri baseuri) +;; diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index fe3262109..11a608e1d 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -12,12 +12,21 @@ (* $Id$ *) exception ObjectNotFound of string Lazy.t +exception LibraryOutOfSync of string Lazy.t -val add_obj: NUri.uri -> NCic.obj -> unit +type timestamp +val time0: timestamp + +val add_obj: NUri.uri -> NCic.obj -> timestamp val aliases_of: NUri.uri -> NReference.reference list val resolve: string -> NReference.reference list -val get_obj: NUri.uri -> NCic.obj +val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *) val clear_cache : unit -> unit +val time_travel: timestamp -> unit +val serialize: baseuri:NUri.uri -> ('status -> 'status) -> unit +val require: baseuri:NUri.uri -> 'status -> 'status +val decompile: baseuri:NUri.uri -> unit + (* EOF *) diff --git a/helm/software/components/ng_kernel/nUri.ml b/helm/software/components/ng_kernel/nUri.ml index e94ee9037..5d8107294 100644 --- a/helm/software/components/ng_kernel/nUri.ml +++ b/helm/software/components/ng_kernel/nUri.ml @@ -53,3 +53,4 @@ module HT = struct end;; module UriHash = Hashtbl.Make(HT);; +module UriMap = Map.Make(HT);; diff --git a/helm/software/components/ng_kernel/nUri.mli b/helm/software/components/ng_kernel/nUri.mli index 56b49ce88..323da90c3 100644 --- a/helm/software/components/ng_kernel/nUri.mli +++ b/helm/software/components/ng_kernel/nUri.mli @@ -20,4 +20,4 @@ val eq: uri -> uri -> bool val compare: uri -> uri -> int module UriHash: Hashtbl.S with type key = uri - +module UriMap: Map.S with type key = uri diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index ee4b6b3d3..632748f92 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -3,8 +3,8 @@ nCicMetaSubst.cmi: nCicCoercion.cmi: nCicUnifHint.cmi: nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi -nCicUnification.cmi: nCicUnifHint.cmi -nCicRefiner.cmi: nCicUnifHint.cmi +nCicUnification.cmi: nRstatus.cmi +nCicRefiner.cmi: nRstatus.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi @@ -15,7 +15,11 @@ nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi -nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi -nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi -nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicRefiner.cmi +nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ + nCicUnification.cmi +nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ + nCicUnification.cmi +nCicRefiner.cmo: nRstatus.cmi nCicUnification.cmi nCicMetaSubst.cmi \ + nCicCoercion.cmi nCicRefiner.cmi +nCicRefiner.cmx: nRstatus.cmx nCicUnification.cmx nCicMetaSubst.cmx \ + nCicCoercion.cmx nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 51f0482a5..bd7f72e70 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -273,7 +273,9 @@ let _ = (try let rdb = { NRstatus.uhint_db = NCicUnifHint.empty_db; - NRstatus.coerc_db = NCicCoercion.empty_db + NRstatus.coerc_db = NCicCoercion.empty_db; + NRstatus.library_db = NCicLibrary.time0; + NRstatus.dump = fun x -> x } in let metasenv, subst, bo, infty = NCicRefiner.typeof rdb [] [] [] bo None diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index 9bd934c3b..9532ba985 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -62,9 +62,7 @@ let index_hint hdb context t1 t2 precedence = let empty_db = DB.empty ;; -let user_db = ref empty_db ;; - -let add_user_provided_hint t precedence = +let add_user_provided_hint db t precedence = let u = UriManager.uri_of_string "cic:/foo/bar.con" in let c, a, b = let rec aux ctx = function @@ -80,7 +78,7 @@ let add_user_provided_hint t precedence = in aux [] (fst (OCic2NCic.convert_term u t)) in - user_db := index_hint !user_db c a b precedence + index_hint db c a b precedence ;; let db () = @@ -139,10 +137,13 @@ let db () = else []) [] (CoercDb.to_list (CoercDb.dump ())) in + prerr_endline "MISTERO"; + assert false (* ERA List.fold_left (fun db -> function | (ctx,b1,b2) -> index_hint db ctx b1 b2 0) !user_db (List.flatten hints) +*) ;; let saturate ?(delta=0) metasenv subst context ty goal_arity = diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index 7582c3df6..bb8bc6af1 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -16,7 +16,7 @@ type db val index_hint: db -> NCic.context -> NCic.term -> NCic.term -> int -> db -val add_user_provided_hint : Cic.term -> int -> unit +val add_user_provided_hint : db -> Cic.term -> int -> db val empty_db : db diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml index 02eee9837..0ef8755f4 100644 --- a/helm/software/components/ng_refiner/nRstatus.ml +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -14,5 +14,7 @@ type refiner_status = { coerc_db : NCicCoercion.db; uhint_db : NCicUnifHint.db; + library_db : NCicLibrary.timestamp; + dump: refiner_status -> refiner_status } diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli index 46634a679..6cf9ddd4f 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -14,4 +14,6 @@ type refiner_status = { coerc_db : NCicCoercion.db; uhint_db : NCicUnifHint.db; + library_db : NCicLibrary.timestamp; + dump: refiner_status -> refiner_status } diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index d701a50ae..3c7db84cd 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -88,7 +88,9 @@ let save_moo grafite_status = GrafiteMarshal.save_moo moo_fname grafite_status.GrafiteTypes.moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname - (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev + (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev; + NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri) + (GrafiteTypes.get_dump grafite_status) | _ -> clean_current_baseuri grafite_status ;; diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 1f880575e..eb115636f 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -222,11 +222,12 @@ let main () = | End_of_file -> () | GrafiteEngine.Drop -> clean_exit 1 ); - let proof_status,moo_content_rev,lexicon_content_rev = + let proof_status,moo_content_rev,lexicon_content_rev,dump = match !grafite_status with | s::_ -> s.proof_status, s.moo_content_rev, - (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev + (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev, + GrafiteTypes.get_dump s | _ -> assert false in if proof_status <> GrafiteTypes.No_proof then @@ -253,6 +254,7 @@ let main () = in GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; + NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri) dump; exit 0 end with diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index a4e879a36..7580ebf29 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -274,6 +274,8 @@ let compile atstart options fname = (* FG: we do not generate .moo when dumping .mma files *) GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; + NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri) + (GrafiteTypes.get_dump grafite_status) end; let tm = Unix.gmtime elapsed in let sec = string_of_int tm.Unix.tm_sec ^ "''" in diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends index ccbafd0cd..190d7bf6d 100644 --- a/helm/software/matita/tests/depends +++ b/helm/software/matita/tests/depends @@ -1,5 +1,5 @@ -TPTP/Veloci/GRP595-1.p.ma logic/equality.ma TPTP/Veloci/GRP570-1.p.ma logic/equality.ma +TPTP/Veloci/GRP595-1.p.ma logic/equality.ma dependent_guarded_bove_capretta.ma nat/nat.ma interactive/test5.ma TPTP/Veloci/SYN083-1.p.ma logic/equality.ma @@ -35,8 +35,8 @@ TPTP/Veloci/COL063-3.p.ma logic/equality.ma TPTP/Veloci/LCL112-2.p.ma logic/equality.ma formal_topology.ma logic/connectives.ma TPTP/Veloci/RNG023-7.p.ma logic/equality.ma -test2.ma coq.ma replace.ma coq.ma +test2.ma coq.ma TPTP/Veloci/COL064-7.p.ma logic/equality.ma TPTP/Veloci/BOO009-2.p.ma logic/equality.ma TPTP/Veloci/GRP510-1.p.ma logic/equality.ma @@ -86,8 +86,8 @@ letrec.ma TPTP/Veloci/BOO001-1.p.ma logic/equality.ma TPTP/Veloci/GRP160-1.p.ma logic/equality.ma TPTP/Veloci/GRP600-1.p.ma logic/equality.ma -TPTP/Veloci/GRP512-1.p.ma logic/equality.ma TPTP/Veloci/COL063-5.p.ma logic/equality.ma +TPTP/Veloci/GRP512-1.p.ma logic/equality.ma continuationals.ma coq.ma TPTP/Veloci/GRP490-1.p.ma logic/equality.ma TPTP/Veloci/BOO034-1.p.ma logic/equality.ma @@ -101,8 +101,8 @@ TPTP/Veloci/BOO009-4.p.ma logic/equality.ma TPTP/Veloci/LAT040-1.p.ma logic/equality.ma TPTP/Veloci/GRP578-1.p.ma logic/equality.ma change.ma coq.ma -TPTP/Veloci/BOO075-1.p.ma logic/equality.ma TPTP/Veloci/GRP168-1.p.ma logic/equality.ma +TPTP/Veloci/BOO075-1.p.ma logic/equality.ma TPTP/Veloci/GRP143-1.p.ma logic/equality.ma TPTP/Veloci/GRP586-1.p.ma logic/equality.ma TPTP/Veloci/GRP561-1.p.ma logic/equality.ma @@ -118,8 +118,8 @@ TPTP/Veloci/RNG007-4.p.ma logic/equality.ma TPTP/Veloci/GRP548-1.p.ma logic/equality.ma TPTP/Veloci/GRP182-3.p.ma logic/equality.ma TPTP/Veloci/COL048-1.p.ma logic/equality.ma -TPTP/Veloci/GRP189-2.p.ma logic/equality.ma TPTP/Veloci/BOO005-2.p.ma logic/equality.ma +TPTP/Veloci/GRP189-2.p.ma logic/equality.ma TPTP/Veloci/GRP556-1.p.ma logic/equality.ma TPTP/Veloci/GRP146-1.p.ma logic/equality.ma TPTP/Veloci/COL064-4.p.ma logic/equality.ma @@ -142,8 +142,8 @@ TPTP/Veloci/GRP580-1.p.ma logic/equality.ma TPTP/Veloci/COL062-3.p.ma logic/equality.ma TPTP/Veloci/GRP492-1.p.ma logic/equality.ma cut.ma coq.ma -TPTP/Veloci/COL018-1.p.ma logic/equality.ma TPTP/Veloci/LAT034-1.p.ma logic/equality.ma +TPTP/Veloci/COL018-1.p.ma logic/equality.ma tinycals.ma logic/connectives.ma coercions_contravariant.ma logic/equality.ma nat/nat.ma interactive/automatic_insertion.ma @@ -151,11 +151,11 @@ clearbody.ma coq.ma TPTP/Veloci/LCL134-1.p.ma logic/equality.ma TPTP/Veloci/COL060-2.p.ma logic/equality.ma TPTP/Veloci/BOO016-2.p.ma logic/equality.ma -TPTP/Veloci/GRP542-1.p.ma logic/equality.ma TPTP/Veloci/LAT039-2.p.ma logic/equality.ma -TPTP/Veloci/GRP157-1.p.ma logic/equality.ma +TPTP/Veloci/GRP542-1.p.ma logic/equality.ma TPTP/Veloci/GRP186-4.p.ma logic/equality.ma TPTP/Veloci/GRP454-1.p.ma logic/equality.ma +TPTP/Veloci/GRP157-1.p.ma logic/equality.ma TPTP/Veloci/GRP509-1.p.ma logic/equality.ma TPTP/Veloci/GRP550-1.p.ma logic/equality.ma ng_commands.ma nat/nat.ma ng_pts.ma @@ -166,22 +166,25 @@ TPTP/Veloci/GRP605-1.p.ma logic/equality.ma fguidi.ma logic/connectives.ma nat/nat.ma TPTP/Veloci/GRP583-1.p.ma logic/equality.ma TPTP/Veloci/GRP517-1.p.ma logic/equality.ma -TPTP/Veloci/COL083-1.p.ma logic/equality.ma -TPTP/Veloci/GRP495-1.p.ma logic/equality.ma TPTP/Veloci/GRP173-1.p.ma logic/equality.ma +TPTP/Veloci/GRP495-1.p.ma logic/equality.ma +TPTP/Veloci/COL083-1.p.ma logic/equality.ma coercions_propagation.ma logic/connectives.ma nat/orders.ma TPTP/Veloci/LAT045-1.p.ma logic/equality.ma TPTP/Veloci/GRP558-1.p.ma logic/equality.ma TPTP/Veloci/GRP010-4.p.ma logic/equality.ma interactive/test_instance.ma TPTP/Veloci/COL012-1.p.ma logic/equality.ma +ng_lexiconn.ma ng_pts.ma TPTP/Veloci/COL063-2.p.ma logic/equality.ma first.ma +ng_coercions.ma TPTP/Veloci/COL045-1.p.ma logic/equality.ma TPTP/Veloci/BOO005-4.p.ma logic/equality.ma interactive/test7.ma bad_induction.ma logic/equality.ma nat/nat.ma TPTP/Veloci/RNG023-6.p.ma logic/equality.ma +ng_include.ma nat/plus.ma ng_pts.ma color.ma logic/equality.ma nat/nat.ma TPTP/Veloci/COL064-6.p.ma logic/equality.ma metasenv_ordering.ma coq.ma @@ -192,8 +195,8 @@ TPTP/Veloci/LCL153-1.p.ma logic/equality.ma pullback.ma logic/equality.ma TPTP/Veloci/COL086-1.p.ma logic/equality.ma TPTP/Veloci/GRP151-1.p.ma logic/equality.ma -TPTP/Veloci/LCL161-1.p.ma logic/equality.ma TPTP/Veloci/GRP616-1.p.ma logic/equality.ma +TPTP/Veloci/LCL161-1.p.ma logic/equality.ma TPTP/Veloci/GRP023-2.p.ma logic/equality.ma TPTP/Veloci/GRP206-1.p.ma logic/equality.ma decompose.ma logic/connectives.ma @@ -208,8 +211,8 @@ dependent_type_inference.ma nat/nat.ma TPTP/Veloci/GRP456-1.p.ma logic/equality.ma TPTP/Veloci/GRP159-1.p.ma logic/equality.ma TPTP/Veloci/ROB030-1.p.ma logic/equality.ma -TPTP/Veloci/GRP577-1.p.ma logic/equality.ma TPTP/Veloci/GRP552-1.p.ma logic/equality.ma +TPTP/Veloci/GRP577-1.p.ma logic/equality.ma TPTP/Veloci/BOO013-2.p.ma logic/equality.ma rewrite.ma coq.ma bad_tests/auto.ma coq.ma @@ -222,16 +225,16 @@ TPTP/Veloci/GRP602-1.p.ma logic/equality.ma TPTP/Veloci/GRP514-1.p.ma logic/equality.ma TPTP/Veloci/LCL139-1.p.ma logic/equality.ma TPTP/Veloci/GRP547-1.p.ma logic/equality.ma -TPTP/Veloci/COL004-3.p.ma logic/equality.ma +TPTP/Veloci/GRP137-1.p.ma logic/equality.ma TPTP/Veloci/GRP459-1.p.ma logic/equality.ma TPTP/Veloci/BOO069-1.p.ma logic/equality.ma -TPTP/Veloci/GRP137-1.p.ma logic/equality.ma +TPTP/Veloci/COL004-3.p.ma logic/equality.ma TPTP/Veloci/GRP188-2.p.ma logic/equality.ma apply.ma coq.ma TPTP/Veloci/GRP467-1.p.ma logic/equality.ma TPTP/Veloci/GRP145-1.p.ma logic/equality.ma -TPTP/Veloci/COL063-4.p.ma logic/equality.ma TPTP/Veloci/LCL155-1.p.ma logic/equality.ma +TPTP/Veloci/COL063-4.p.ma logic/equality.ma TPTP/Veloci/GRP588-1.p.ma logic/equality.ma TPTP/Veloci/GRP153-1.p.ma logic/equality.ma paramodulation.ma coq.ma @@ -240,8 +243,8 @@ coercions_nonuniform.ma TPTP/Veloci/GRP161-1.p.ma logic/equality.ma TPTP/Veloci/COL064-8.p.ma logic/equality.ma TPTP/Veloci/LDA001-1.p.ma logic/equality.ma -TPTP/Veloci/BOO010-4.p.ma logic/equality.ma TPTP/Veloci/COL050-1.p.ma logic/equality.ma +TPTP/Veloci/BOO010-4.p.ma logic/equality.ma TPTP/Veloci/LCL110-2.p.ma logic/equality.ma TPTP/Veloci/GRP491-1.p.ma logic/equality.ma TPTP/Veloci/COL061-3.p.ma logic/equality.ma @@ -250,9 +253,9 @@ TPTP/Veloci/GRP613-1.p.ma logic/equality.ma compose.ma logic/equality.ma TPTP/Veloci/COL025-1.p.ma logic/equality.ma TPTP/Veloci/GRP115-1.p.ma logic/equality.ma -letrecand.ma nat/nat.ma unifhint.ma list/list.ma nat/nat.ma nat/plus.ma hard_refine.ma coq.ma +letrecand.ma nat/nat.ma paramodulation/group.ma coq.ma TPTP/Veloci/LCL158-1.p.ma logic/equality.ma TPTP/Veloci/LCL133-1.p.ma logic/equality.ma @@ -269,8 +272,8 @@ TPTP/Veloci/GRP599-1.p.ma logic/equality.ma TPTP/Veloci/GRP574-1.p.ma logic/equality.ma TPTP/Veloci/LDA007-3.p.ma logic/equality.ma unfold.ma coq.ma -TPTP/Veloci/GRP486-1.p.ma logic/equality.ma TPTP/Veloci/GRP189-1.p.ma logic/equality.ma +TPTP/Veloci/GRP486-1.p.ma logic/equality.ma TPTP/Veloci/BOO071-1.p.ma logic/equality.ma TPTP/Veloci/BOO013-4.p.ma logic/equality.ma TPTP/Veloci/GRP582-1.p.ma logic/equality.ma @@ -290,8 +293,9 @@ injection.ma coq.ma second.ma first.ma TPTP/Veloci/COL062-2.p.ma logic/equality.ma match_inference.ma -simpl.ma coq.ma unifhint_simple.ma logic/equality.ma +ng_includeB.ma ng_include.ma +simpl.ma coq.ma TPTP/Veloci/COL063-6.p.ma logic/equality.ma TPTP/Veloci/GRP142-1.p.ma logic/equality.ma third.ma first.ma second.ma diff --git a/helm/software/matita/tests/ng_include.ma b/helm/software/matita/tests/ng_include.ma new file mode 100644 index 000000000..4584afddc --- /dev/null +++ b/helm/software/matita/tests/ng_include.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ng_pts.ma". +include "nat/plus.ma". + +(* +ndefinition x ≝ O. +*) +(*ndefinition y ≝ cic:/matita/tests/ng_commands/x.def(1).*) + +axiom P: nat → Prop. + +unification hint 0 (∀n. P (0 + n) = P n) . + +ntheorem foo: ∀n. ∀H:(P (? + n) → Prop). ∀p:P n. H p. \ No newline at end of file diff --git a/helm/software/matita/tests/ng_includeB.ma b/helm/software/matita/tests/ng_includeB.ma new file mode 100644 index 000000000..f7e1e293e --- /dev/null +++ b/helm/software/matita/tests/ng_includeB.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ng_include.ma". + +ntheorem foo: ∀n. ∀H:(P (? + n) → Prop). ∀p:P n. H p.