+content.cmi:
acic2content.cmi: content.cmi
content2cic.cmi: content.cmi
cicNotationUtil.cmi: cicNotationPt.cmx
cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi
acic2astMatcher.cmi: cicNotationPt.cmx
termAcicContent.cmi: cicNotationPt.cmx
+cicNotationPt.cmo:
+cicNotationPt.cmx:
content.cmo: content.cmi
content.cmx: content.cmi
acic2content.cmo: content.cmi acic2content.cmi
+proceduralHelpers.cmi:
+proceduralClassify.cmi:
+proceduralOptimizer.cmi:
+proceduralTypes.cmi:
+proceduralMode.cmi:
+proceduralConversion.cmi:
procedural1.cmi: proceduralTypes.cmi
procedural2.cmi: proceduralTypes.cmi
proceduralTeX.cmi: proceduralTypes.cmi
+acic2Procedural.cmi:
proceduralHelpers.cmo: proceduralHelpers.cmi
proceduralHelpers.cmx: proceduralHelpers.cmi
proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi
+extractor.cmo:
+extractor.cmx:
+extractor_manager.cmo:
+extractor_manager.cmx:
+table_creator.cmo:
+table_creator.cmx:
gallina8Parser.cmi: types.cmo
grafiteParser.cmi: types.cmo
grafite.cmi: types.cmo
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmo gallina8Parser.cmi
+cicUniv.cmi:
unshare.cmi: cic.cmx
deannotate.cmi: cic.cmx
cicParser.cmi: cic.cmx
cicUtil.cmi: cic.cmx
helmLibraryObjects.cmi: cic.cmx
+libraryObjects.cmi:
discrimination_tree.cmi: cic.cmx
path_indexing.cmi: cic.cmx
cicInspect.cmi: cic.cmx
+eta_fixing.cmi:
+doubleTypeInference.cmi:
+cic2acic.cmi:
cic2Xml.cmi: cic2acic.cmi
eta_fixing.cmo: eta_fixing.cmi
eta_fixing.cmx: eta_fixing.cmi
+cicDisambiguate.cmi:
+disambiguateChoices.cmi:
cicDisambiguate.cmo: cicDisambiguate.cmi
cicDisambiguate.cmx: cicDisambiguate.cmi
disambiguateChoices.cmo: disambiguateChoices.cmi
+cicExportation.cmi:
cicExportation.cmo: cicExportation.cmi
cicExportation.cmx: cicExportation.cmi
+cicLogger.cmi:
+cicEnvironment.cmi:
+cicPp.cmi:
+cicUnivUtils.cmi:
+cicSubstitution.cmi:
+cicMiniReduction.cmi:
+cicReduction.cmi:
+cicTypeChecker.cmi:
+freshNamesGenerator.cmi:
+cicDischarge.cmi:
cicLogger.cmo: cicLogger.cmi
cicLogger.cmx: cicLogger.cmi
cicEnvironment.cmo: cicEnvironment.cmi
+cicMetaSubst.cmi:
+cicMkImplicit.cmi:
+termUtil.cmi:
+coercGraph.cmi:
+cicUnification.cmi:
+cicReplace.cmi:
+cicRefine.cmi:
cicMetaSubst.cmo: cicMetaSubst.cmi
cicMetaSubst.cmx: cicMetaSubst.cmi
cicMkImplicit.cmo: cicMkImplicit.cmi
;;
let generate_dot_file () =
- let l = CoercDb.to_list () in
+ let l = CoercDb.to_list (CoercDb.dump ()) in
let module Pp = GraphvizPp.Dot in
let buf = Buffer.create 10240 in
let fmt = Format.formatter_of_buffer buf in
(* : carr -> (carr * uri option) where the option is always Some *)
let get_coercions_to carr =
- let l = CoercDb.to_list () in
+ let l = CoercDb.to_list (CoercDb.dump ()) in
let splat_coercion_to carr (src,tgt,cl) =
if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
in
(* : carr -> (carr * uri option) where the option is always Some *)
let get_coercions_from carr =
- let l = CoercDb.to_list () in
+ let l = CoercDb.to_list (CoercDb.dump ()) in
let splat_coercion_from carr (src,tgt,cl) =
if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
in
+renderingAttrs.cmi:
+cicNotationLexer.cmi:
+cicNotationParser.cmi:
+mpresentation.cmi:
+box.cmi:
+content2presMatcher.cmi:
termContentPres.cmi: cicNotationParser.cmi
boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
cicNotationPres.cmi: mpresentation.cmi box.cmi
+disambiguateTypes.cmi:
disambiguate.cmi: disambiguateTypes.cmi
multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
disambiguateTypes.cmo: disambiguateTypes.cmi
+http_getter_wget.cmi:
+http_getter_logger.cmi:
+http_getter_misc.cmi:
+http_getter_const.cmi:
http_getter_env.cmi: http_getter_types.cmx
+http_getter_storage.cmi:
http_getter_common.cmi: http_getter_types.cmx
http_getter.cmi: http_getter_types.cmx
+http_getter_types.cmo:
+http_getter_types.cmx:
http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi
http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi
http_getter_logger.cmo: http_getter_logger.cmi
+grafiteTypes.cmi:
grafiteSync.cmi: grafiteTypes.cmi
grafiteEngine.cmi: grafiteTypes.cmi
grafiteTypes.cmo: grafiteTypes.cmi
(match status.GrafiteTypes.ng_status with
| GrafiteTypes.ProofMode
{ NTacStatus.istatus =
- {NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } ->
+ { NTacStatus.pstatus = pstatus; estatus = estatus } } ->
let uri,height,menv,subst,obj_kind = pstatus in
if menv <> [] then
raise
in
{status with
GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode lexicon_status },`New uris
+ 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;
NCicEnvironment.add_constraint strict [false,u1] [false,u2];
status, `New [u1;u2]
| GrafiteAst.NObj (loc,obj) ->
- let lexicon_status =
+ let estatus =
match status.GrafiteTypes.ng_status with
| GrafiteTypes.ProofMode _ -> assert false
- | GrafiteTypes.CommandMode ls -> ls in
- let lexicon_status,obj =
- GrafiteDisambiguate.disambiguate_nobj lexicon_status
+ | GrafiteTypes.CommandMode es -> es
+ in
+ let estatus,obj =
+ GrafiteDisambiguate.disambiguate_nobj estatus
~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
let uri,height,nmenv,nsubst,nobj = obj in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
GrafiteTypes.ProofMode
(subst_metasenv_and_fix_names
{ NTacStatus.gstatus = ninitial_stack;
- istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}})
+ istatus = { NTacStatus.pstatus = obj; estatus = estatus}})
}
in
(match nmenv with
let lemmas =
LibrarySync.add_coercion ~add_composites ~pack_coercion_obj
uri arity saturations baseuri in
+ let status =
{ status with GrafiteTypes.coercions = CoercDb.dump () ;
- objects = lemmas @ status.GrafiteTypes.objects
- },
- lemmas
+ objects = lemmas @ status.GrafiteTypes.objects;
+ }
+ in
+ let db =
+ NCicCoercion.index_old_db (CoercDb.dump ())
+ (GrafiteTypes.get_coercions status)
+ in
+ let status = GrafiteTypes.set_coercions db status in
+ status, lemmas
let prefer_coercion s u =
CoercDb.prefer u;
coercions = CoercDb.empty_coerc_db;
automation_cache = AutomationCache.empty ();
baseuri = baseuri;
- ng_status = GrafiteTypes.CommandMode lexicon_status;
+ ng_status = GrafiteTypes.CommandMode {
+ NEstatus.lstatus = lexicon_status;
+ NEstatus.rstatus = {
+ NRstatus.uhint_db = NCicUnifHint.empty_db;
+ NRstatus.coerc_db = NCicCoercion.empty_db;
+ };
}
+}
let init baseuri =
type ng_status =
| ProofMode of NTacStatus.tac_status
- | CommandMode of LexiconEngine.status
+ | CommandMode of NEstatus.extra_status
type status = {
moo_content_rev: GrafiteMarshal.moo;
ng_status: ng_status;
}
+let get_lexicon x =
+ match x.ng_status with
+ | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.lstatus
+ | CommandMode e -> e.NEstatus.lstatus
+;;
+
+let set_lexicon new_lexicon_status new_grafite_status =
+ { new_grafite_status with ng_status =
+ match new_grafite_status.ng_status with
+ | CommandMode estatus ->
+ CommandMode
+ { estatus with NEstatus.lstatus = new_lexicon_status }
+ | ProofMode t ->
+ ProofMode
+ { t with NTacStatus.istatus =
+ { t.NTacStatus.istatus with NTacStatus.estatus =
+ { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.lstatus =
+ new_lexicon_status }}}}
+;;
+
+let set_coercions db new_grafite_status =
+ { new_grafite_status with ng_status =
+ match new_grafite_status.ng_status with
+ | CommandMode estatus ->
+ CommandMode
+ { estatus with NEstatus.rstatus =
+ { estatus.NEstatus.rstatus with NRstatus.coerc_db = db }}
+ | ProofMode t ->
+ ProofMode
+ { t with NTacStatus.istatus =
+ { t.NTacStatus.istatus with NTacStatus.estatus =
+ { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.rstatus =
+ { t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.rstatus with NRstatus.coerc_db = db
+ }}}}}
+;;
+
+let get_estatus x =
+ match x.ng_status with
+ | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
+ | CommandMode e -> e
+;;
+
let get_current_proof status =
match status.proof_status with
| Incomplete_proof { proof = p } -> p
List.iter
(fun u -> HLog.message (UriManager.string_of_uri u)) status.objects
+let get_coercions new_grafite_status =
+ let e = get_estatus new_grafite_status in
+ e.NEstatus.rstatus.NRstatus.coerc_db
+;;
+
type ng_status =
| ProofMode of NTacStatus.tac_status
- | CommandMode of LexiconEngine.status
+ | CommandMode of NEstatus.extra_status
type status = {
moo_content_rev: GrafiteMarshal.moo;
val get_stack: status -> Continuationals.Stack.t
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_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
+dependenciesParser.cmi:
+grafiteParser.cmi:
+cicNotation2.cmi:
+nEstatus.cmi:
+grafiteDisambiguate.cmi:
grafiteWalker.cmi: grafiteParser.cmi
+print_grammar.cmi:
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi
cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi
+nEstatus.cmo: nEstatus.cmi
+nEstatus.cmx: nEstatus.cmi
grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi
+dependenciesParser.cmi:
+grafiteParser.cmi:
+cicNotation2.cmi:
+nEstatus.cmi:
+grafiteDisambiguate.cmi: nEstatus.cmi
grafiteWalker.cmi: grafiteParser.cmi
+print_grammar.cmi:
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi
cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi
-grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
-grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
+nEstatus.cmo: nEstatus.cmi
+nEstatus.cmx: nEstatus.cmi
+grafiteDisambiguate.cmo: nEstatus.cmi grafiteDisambiguate.cmi
+grafiteDisambiguate.cmx: nEstatus.cmx grafiteDisambiguate.cmi
grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi
grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi
print_grammar.cmo: print_grammar.cmi
dependenciesParser.mli \
grafiteParser.mli \
cicNotation2.mli \
+ nEstatus.mli \
grafiteDisambiguate.mli \
grafiteWalker.mli \
print_grammar.mli \
metasenv,(*subst,*) cic
;;
-let disambiguate_nterm expty lexicon_status context metasenv subst thing
+let disambiguate_nterm expty estatus context metasenv subst thing
=
let diff, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
- ~coercion_db:(NCicCoercion.db ())
- ~aliases:lexicon_status.LexiconEngine.aliases
+ ~rdb:estatus.NEstatus.rstatus
+ ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
~expty
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases)
~lookup_in_library:nlookup_in_library
~mk_choice:ncic_mk_choice
~mk_implicit
~description_of_alias:LexiconAst.description_of_alias
~context ~metasenv ~subst thing)
in
- let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
- metasenv, subst, lexicon_status, cic
+ let lexicon_status =
+ LexiconEngine.set_proof_aliases estatus.NEstatus.lstatus diff in
+ metasenv, subst, { estatus with NEstatus.lstatus = lexicon_status }, cic
;;
| `Proof as t -> metasenv,t in
metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
-let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
+let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
let uri =
let baseuri =
match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
let _,g = CicTypeChecker.typecheck uri in
CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri))
graph l)
- graph (CoercDb.to_list ())
+ graph (CoercDb.to_list (CoercDb.dump ()))
in
ignore(CicUniv.do_rank graph);
(try
(match
NCicDisambiguate.disambiguate_obj
+ ~rdb:estatus.NEstatus.rstatus
~lookup_in_library:nlookup_in_library
~description_of_alias:LexiconAst.description_of_alias
~mk_choice:ncic_mk_choice
~mk_implicit
~uri:(OCic2NCic.nuri_of_ouri uri)
- ~coercion_db:(NCicCoercion.db ())
- ~aliases:lexicon_status.LexiconEngine.aliases
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
+ ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases)
(text,prefix_len,obj)
with
| [_,_,_,obj],_ ->
(* let time = Unix.gettimeofday () in *)
+ let lexicon_status = estatus.NEstatus.lstatus in
let (diff, metasenv, _, cic, _) =
singleton "third"
(CicDisambiguate.disambiguate_obj
~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~uri:(Some uri)
- (text,prefix_len,obj)) in
+ (text,prefix_len,obj))
+ in
(*
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
- lexicon_status, metasenv, cic
+ { estatus with NEstatus.lstatus = lexicon_status }, metasenv, cic
with
| Sys.Break as exn -> raise exn
raise exn
;;
-let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
+let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
let uri =
let baseuri =
match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
~mk_choice:ncic_mk_choice
~mk_implicit
~uri:(OCic2NCic.nuri_of_ouri uri)
- ~coercion_db:(NCicCoercion.db ())
- ~aliases:lexicon_status.LexiconEngine.aliases
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~rdb:estatus.NEstatus.rstatus
+ ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
+ ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases)
(text,prefix_len,obj)) in
- let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
- lexicon_status, cic
+ let lexicon_status =
+ LexiconEngine.set_proof_aliases estatus.NEstatus.lstatus diff in
+ { estatus with NEstatus.lstatus = lexicon_status }, cic
;;
-let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
+let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
match cmd with
- | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj)
+ | GrafiteAst.NObj(loc,obj) -> estatus, metasenv, GrafiteAst.NObj(loc,obj)
| GrafiteAst.Index(loc,key,uri) ->
- let lexicon_status_ref = ref lexicon_status in
+ let lexicon_status_ref = ref estatus.NEstatus.lstatus in
let disambiguate_term =
disambiguate_term None text prefix_len lexicon_status_ref [] in
let disambiguate_term_option metasenv =
metasenv, Some t
in
let metasenv,key = disambiguate_term_option metasenv key in
- !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
+ { estatus with NEstatus.lstatus = !lexicon_status_ref },
+ metasenv,GrafiteAst.Index(loc,key,uri)
| GrafiteAst.Select (loc,uri) ->
- lexicon_status, metasenv, GrafiteAst.Select(loc,uri)
+ estatus, metasenv, GrafiteAst.Select(loc,uri)
| GrafiteAst.Pump(loc,i) ->
- lexicon_status, metasenv, GrafiteAst.Pump(loc,i)
+ estatus, metasenv, GrafiteAst.Pump(loc,i)
| GrafiteAst.PreferCoercion (loc,t) ->
- let lexicon_status_ref = ref lexicon_status in
+ let lexicon_status_ref = ref estatus.NEstatus.lstatus in
let disambiguate_term =
disambiguate_term None text prefix_len lexicon_status_ref [] in
let metasenv,t = disambiguate_term metasenv t in
- !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t)
+ { estatus with NEstatus.lstatus = !lexicon_status_ref},
+ metasenv, GrafiteAst.PreferCoercion (loc,t)
| GrafiteAst.Coercion (loc,t,b,a,s) ->
- let lexicon_status_ref = ref lexicon_status in
+ let lexicon_status_ref = ref estatus.NEstatus.lstatus in
let disambiguate_term =
disambiguate_term None text prefix_len lexicon_status_ref [] in
let metasenv,t = disambiguate_term metasenv t in
- !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
+ { estatus with NEstatus.lstatus = !lexicon_status_ref },
+ metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
| GrafiteAst.Inverter (loc,n,indty,params) ->
- let lexicon_status_ref = ref lexicon_status in
- let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in
- let metasenv,indty = disambiguate_term metasenv indty in
- !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
+ let lexicon_status_ref = ref estatus.NEstatus.lstatus in
+ let disambiguate_term =
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
+ let metasenv,indty = disambiguate_term metasenv indty in
+ { estatus with NEstatus.lstatus = !lexicon_status_ref },
+ metasenv, GrafiteAst.Inverter (loc,n,indty,params)
| GrafiteAst.UnificationHint (loc, t, n) ->
- let lexicon_status_ref = ref lexicon_status in
+ let lexicon_status_ref = ref estatus.NEstatus.lstatus in
let disambiguate_term =
disambiguate_term None text prefix_len lexicon_status_ref [] in
let metasenv,t = disambiguate_term metasenv t in
- !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t,n)
+ { estatus with NEstatus.lstatus = !lexicon_status_ref },
+ metasenv, GrafiteAst.UnificationHint (loc,t,n)
| GrafiteAst.Default _
| GrafiteAst.Drop _
| GrafiteAst.Include _
| GrafiteAst.NQed _
| GrafiteAst.NUnivConstraint _
| GrafiteAst.Set _ as cmd ->
- lexicon_status,metasenv,cmd
+ estatus,metasenv,cmd
| GrafiteAst.Obj (loc,obj) ->
- let lexicon_status,metasenv,obj =
- disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
- lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
+ let estatus,metasenv,obj =
+ disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj)in
+ estatus, metasenv, GrafiteAst.Obj (loc,obj)
| GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
- let lexicon_status_ref = ref lexicon_status in
+ let lexicon_status_ref = ref estatus.NEstatus.lstatus in
let disambiguate_term =
disambiguate_term None text prefix_len lexicon_status_ref [] in
let disambiguate_term_option metasenv =
let metasenv,refl = disambiguate_term_option metasenv refl in
let metasenv,sym = disambiguate_term_option metasenv sym in
let metasenv,trans = disambiguate_term_option metasenv trans in
- !lexicon_status_ref, metasenv,
+ { estatus with NEstatus.lstatus = !lexicon_status_ref }, metasenv,
GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
let disambiguate_macro
Cic.metasenv * lazy_tactic
val disambiguate_command:
- LexiconEngine.status ->
+ NEstatus.extra_status ->
?baseuri:string ->
Cic.metasenv ->
((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
- LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
+ NEstatus.extra_status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
val disambiguate_macro:
LexiconEngine.status ref ->
Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro
val disambiguate_nterm :
- NCic.term option -> LexiconEngine.status ->
+ NCic.term option ->
+ NEstatus.extra_status ->
NCic.context -> NCic.metasenv -> NCic.substitution ->
CicNotationPt.term Disambiguate.disambiguator_input ->
- NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term
+ NCic.metasenv * NCic.substitution * NEstatus.extra_status * NCic.term
val disambiguate_nobj :
- LexiconEngine.status -> ?baseuri:string ->
+ NEstatus.extra_status ->
+ ?baseuri:string ->
(CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
- LexiconEngine.status * NCic.obj
+ NEstatus.extra_status * NCic.obj
type pattern =
CicNotationPt.term Disambiguate.disambiguator_input option *
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+type extra_status = {
+ lstatus : LexiconEngine.status;
+ rstatus : NRstatus.refiner_status;
+}
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+type extra_status = {
+ lstatus : LexiconEngine.status;
+ rstatus : NRstatus.refiner_status;
+}
+
+domMisc.cmi:
+xml2Gdome.cmi:
domMisc.cmo: domMisc.cmi
domMisc.cmx: domMisc.cmi
xml2Gdome.cmo: xml2Gdome.cmi
+hSql.cmi:
+hSqlite3.cmo:
+hSqlite3.cmx:
+hMysql.cmo:
+hMysql.cmx:
hSql.cmo: hSqlite3.cmx hMysql.cmx hSql.cmi
hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi
cicNotation.cmi: lexiconAst.cmx
lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi
lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx
+lexiconAst.cmo:
+lexiconAst.cmx:
lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi
lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi
lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi
+librarian.cmi:
+libraryMisc.cmi:
+libraryDb.cmi:
+coercDb.cmi:
cicCoercion.cmi: coercDb.cmi
+librarySync.cmi:
+cicElim.cmi:
+cicRecord.cmi:
+cicFix.cmi:
+libraryClean.cmi:
librarian.cmo: librarian.cmi
librarian.cmx: librarian.cmi
libraryMisc.cmo: libraryMisc.cmi
| _, _ -> false
;;
-let to_list () =
- List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) !db
+let to_list db =
+ List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db
;;
let rec myfilter p = function
(* takes a term in whnf ~delta:false and a desired ariety *)
val coerc_carr_of_term: Cic.term -> int -> coerc_carr
-val to_list:
- unit ->
- (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
-
type coerc_db
val empty_coerc_db : coerc_db
val dump: unit -> coerc_db
val restore: coerc_db -> unit
+val to_list:
+ coerc_db ->
+ (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
+
(* src carr, tgt carr, uri, saturations, coerced position
* invariant:
* if the constant pointed by uri has n argments
)
ul)
- (CoercDb.to_list ())
+ (CoercDb.to_list (CoercDb.dump ()))
in
let cpos = no_args - arity - saturations - 1 in
if not add_composites then
+helmLogger.cmi:
helmLogger.cmo: helmLogger.cmi
helmLogger.cmx: helmLogger.cmi
+sqlStatements.cmi:
+metadataTypes.cmi:
metadataExtractor.cmi: metadataTypes.cmi
metadataPp.cmi: metadataTypes.cmi
metadataConstraints.cmi: metadataTypes.cmi
+nCicDisambiguate.cmi:
nCicDisambiguate.cmo: nCicDisambiguate.cmi
nCicDisambiguate.cmx: nCicDisambiguate.cmi
;;
let refine_term
- metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl=
+ metasenv subst context uri ~rdb ~use_coercions term expty _ ~localization_tbl=
assert (uri=None);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
(NCicPp.ppterm ~metasenv ~subst ~context term)));
(*assert false*) HExtlib.dummy_floc
in
let metasenv, subst, term, _ =
- NCicRefiner.typeof
- (NCicUnifHint.db ())
- ~look_for_coercion:(
- if use_coercions then
- NCicCoercion.look_for_coercion coercion_db
- else (fun _ _ _ _ _ -> []))
+ NCicRefiner.typeof
+ { rdb with NRstatus.coerc_db =
+ if use_coercions then rdb.NRstatus.coerc_db
+ else NCicCoercion.empty_db }
metasenv subst context term expty ~localise
in
Disambiguate.Ok (term, metasenv, subst, ())
;;
let refine_obj
- ~coercion_db metasenv subst context _uri
+ ~rdb metasenv subst context _uri
~use_coercions obj _ _ugraph ~localization_tbl
=
assert (metasenv=[]);
try
let obj =
NCicRefiner.typeof_obj
- (NCicUnifHint.db ())
- ~look_for_coercion:(
- if use_coercions then
- NCicCoercion.look_for_coercion coercion_db
- else (fun _ _ _ _ _ -> []))
+ { rdb with NRstatus.coerc_db =
+ if use_coercions then rdb.NRstatus.coerc_db
+ else NCicCoercion.empty_db }
obj ~localise
in
Disambiguate.Ok (obj, [], [], ())
let disambiguate_term ~context ~metasenv ~subst ~expty
~mk_implicit ~description_of_alias ~mk_choice
- ~aliases ~universe ~coercion_db ~lookup_in_library
+ ~aliases ~universe ~rdb ~lookup_in_library
(text,prefix_len,term)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
- ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term)
+ ~refine_thing:(refine_term ~rdb) (text,prefix_len,term)
~mk_localization_tbl ~expty ~subst
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
let disambiguate_obj
~mk_implicit ~description_of_alias ~mk_choice
- ~aliases ~universe ~coercion_db ~lookup_in_library ~uri
+ ~aliases ~universe ~rdb ~lookup_in_library ~uri
(text,prefix_len,obj)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
~interpretate_thing:(interpretate_obj ~mk_choice)
- ~refine_thing:(refine_obj ~coercion_db)
+ ~refine_thing:(refine_obj ~rdb)
(text,prefix_len,obj)
~mk_localization_tbl ~expty:None
in
mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
aliases:'alias DisambiguateTypes.Environment.t ->
universe:'alias list DisambiguateTypes.Environment.t option ->
- coercion_db:NCicCoercion.db ->
+ rdb:NRstatus.refiner_status ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) ->
aliases:'a DisambiguateTypes.Environment.t ->
universe:'a list DisambiguateTypes.Environment.t option ->
- coercion_db:NCicCoercion.db ->
+ rdb:NRstatus.refiner_status ->
lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key -> 'a list) ->
+nUri.cmi:
nReference.cmi: nUri.cmi
nCicUtils.cmi: nCic.cmx
nCicSubstitution.cmi: nCic.cmx
nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx
nCicReduction.cmi: nCic.cmx
nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx
-nCicUntrusted.cmi: nCic.cmx
+nCicUntrusted.cmi: nUri.cmi nCic.cmx
nCic.cmo: nUri.cmi nReference.cmi
nCic.cmx: nUri.cmx nReference.cmx
nUri.cmo: nUri.cmi
nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \
nCic.cmx nCicTypeChecker.cmi
-nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicReduction.cmi nCic.cmx nCicUntrusted.cmi
-nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicReduction.cmx nCic.cmx nCicUntrusted.cmi
+nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicTypeChecker.cmi \
+ nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \
+ nCicUntrusted.cmi
+nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicTypeChecker.cmx \
+ nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
+ nCicUntrusted.cmi
+nDiscriminationTree.cmi:
+nCicMetaSubst.cmi:
+nCicCoercion.cmi:
+nCicUnifHint.cmi:
+nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi
nCicUnification.cmi: nCicUnifHint.cmi
nCicRefiner.cmi: nCicUnifHint.cmi
nDiscriminationTree.cmo: nDiscriminationTree.cmi
nCicCoercion.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicCoercion.cmi
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
-nCicUnification.cmi: nCicUnifHint.cmi
-nCicRefiner.cmi: nCicUnifHint.cmi
+nDiscriminationTree.cmi:
+nCicMetaSubst.cmi:
+nCicCoercion.cmi:
+nCicUnifHint.cmi:
+nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi
+nCicUnification.cmi: nRstatus.cmi
+nCicRefiner.cmi: nRstatus.cmi
nDiscriminationTree.cmo: nDiscriminationTree.cmi
nDiscriminationTree.cmx: nDiscriminationTree.cmi
nCicMetaSubst.cmo: nCicMetaSubst.cmi
nCicCoercion.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicCoercion.cmi
nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi
nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.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
+nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi
+nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.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
nCicMetaSubst.mli \
nCicCoercion.mli \
nCicUnifHint.mli \
+ nRstatus.mli \
nCicUnification.mli \
nCicRefiner.mli
prerr_endline ("start: " ^ NUri.string_of_uri u);
let bo = curryfy [] bo in
(try
+ let rdb = {
+ NRstatus.uhint_db = NCicUnifHint.empty_db;
+ NRstatus.coerc_db = NCicCoercion.empty_db
+ } in
let metasenv, subst, bo, infty =
- NCicRefiner.typeof
- ~look_for_coercion:(fun _ _ _ _ _ -> [])
- NCicUnifHint.empty_db [] [] [] bo None
+ NCicRefiner.typeof rdb [] [] [] bo None
in
let metasenv, subst =
try
- NCicUnification.unify NCicUnifHint.empty_db metasenv subst [] infty ty
+ NCicUnification.unify rdb metasenv subst [] infty ty
with
| NCicUnification.Uncertain msg
| NCicUnification.UnificationFailure msg
db_src, db_tgt
;;
-let db () =
+let index_old_db odb db =
List.fold_left
(fun db (_,tgt,clist) ->
List.fold_left
(fun db (uri,_,arg) ->
+ try
let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
let src, tgt =
NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
assert false
in
- index_coercion db c src tgt arity arg)
+ index_coercion db c src tgt arity arg
+ with
+ | NCicEnvironment.BadDependency _
+ | NCicTypeChecker.TypeCheckerFailure _ -> db)
db clist)
- (DB.empty,DB.empty) (CoercDb.to_list ())
+ db (CoercDb.to_list odb)
;;
let empty_db = (DB.empty,DB.empty) ;;
val index_coercion:
db -> NCic.term -> NCic.term -> NCic.term -> int -> int -> db
- (* gets the old imperative coercion DB *)
-val db : unit -> db
+ (* gets the old imperative coercion DB (list format) *)
+val index_old_db: CoercDb.coerc_db -> db -> db
val empty_db : db
;;
-let check_allowed_sort_elimination hdb localise r orig =
+let check_allowed_sort_elimination rdb localise r orig =
let mkapp he arg =
match he with
| C.Appl l -> C.Appl (l @ [arg])
NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type
in
let metasenv, subst =
- try NCicUnification.unify hdb metasenv subst context
+ try NCicUnification.unify rdb metasenv subst context
arity2 (C.Prod (name, so1, meta))
with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
"expected %s, found %s" (* XXX localizzare meglio *)
| C.Sort _ (* , t ==?== C.Prod _ *) ->
let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
let metasenv, subst =
- try NCicUnification.unify hdb metasenv subst context
+ try NCicUnification.unify rdb metasenv subst context
arity2 (C.Prod ("_", ind, meta))
with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
"expected %s, found %s" (* XXX localizzare meglio *)
aux
;;
-let rec typeof hdb
+let rec typeof rdb
?(localise=fun _ -> Stdpp.dummy_loc)
- ~look_for_coercion metasenv subst context term expty
+ metasenv subst context term expty
=
let force_ty skip_lambda metasenv subst context orig t infty expty =
(*D*)inside 'F'; try let rc =
(NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
try
let metasenv, subst =
- NCicUnification.unify hdb metasenv subst context infty expty
+ NCicUnification.unify rdb metasenv subst context infty expty
in
metasenv, subst, t, expty
with exc ->
- try_coercions hdb ~look_for_coercion ~localise
+ try_coercions rdb ~localise
metasenv subst context t orig infty expty true exc)
| None -> metasenv, subst, t, infty
(*D*)in outside(); rc with exc -> outside (); raise exc
| C.Prod (name,(s as orig_s),(t as orig_t)) ->
let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
let metasenv, subst, s, s1 =
- force_to_sort hdb ~look_for_coercion
+ force_to_sort rdb
metasenv subst context s orig_s localise s1 in
let context1 = (name,(C.Decl s))::context in
let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
let metasenv, subst, t, s2 =
- force_to_sort hdb ~look_for_coercion
+ force_to_sort rdb
metasenv subst context1 t orig_t localise s2 in
let metasenv, subst, s, t, ty =
sort_of_prod localise metasenv subst
let metasenv, subst, s, ty_s =
typeof_aux metasenv subst context None s in
let metasenv, subst, s, _ =
- force_to_sort hdb ~look_for_coercion
+ force_to_sort rdb
metasenv subst context s orig_s localise ty_s in
let (metasenv,subst), exp_ty_t =
match exp_s with
| Some exp_s ->
- (try NCicUnification.unify hdb metasenv subst context s exp_s,exp_ty_t
+ (try NCicUnification.unify rdb metasenv subst context s exp_s,exp_ty_t
with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
"Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
let metasenv, subst, ty, ty_ty =
typeof_aux metasenv subst context None ty in
let metasenv, subst, ty, _ =
- force_to_sort hdb ~look_for_coercion
+ force_to_sort rdb
metasenv subst context ty orig_ty localise ty_ty in
let metasenv, subst, t, _ =
typeof_aux metasenv subst context (Some ty) t in
let metasenv, subst, he, ty_he =
typeof_aux metasenv subst context None he in
let metasenv, subst, t, ty =
- eat_prods hdb ~localise ~look_for_coercion
+ eat_prods rdb ~localise
metasenv subst context orig_he he ty_he args
in
let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in
let metasenv,metanoouttype,newouttype,metaoutsort =
NCicMetaSubst.mk_meta metasenv context `Term in
let metasenv,subst =
- NCicUnification.unify hdb metasenv subst context outsort metaoutsort in
+ NCicUnification.unify rdb metasenv subst context outsort metaoutsort in
let metasenv =
List.filter (function (j,_) -> j <> metanoouttype) metasenv in
let subst =
let metasenv, subst, ind, ind_ty =
typeof_aux metasenv subst context None ind in
let metasenv, subst =
- check_allowed_sort_elimination hdb localise r orig_term metasenv subst
+ check_allowed_sort_elimination rdb localise r orig_term metasenv subst
context ind ind_ty outsort
in
(* let's check if the type of branches are right *)
match expty with
| None -> metasenv, subst
| Some expty ->
- NCicUnification.unify hdb metasenv subst context resty expty
+ NCicUnification.unify rdb metasenv subst context resty expty
in
*)
let _, metasenv, subst, pl =
in
typeof_aux metasenv subst context expty term
-and try_coercions hdb
- ~localise ~look_for_coercion
+and try_coercions rdb
+ ~localise
metasenv subst context t orig_t infty expty perform_unification exc
=
(* we try with a coercion *)
NCicPp.ppterm ~metasenv ~subst ~context meta ^ " === " ^
NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
let metasenv, subst =
- NCicUnification.unify hdb metasenv subst context meta t
+ NCicUnification.unify rdb metasenv subst context meta t
in
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n"));
let metasenv, subst =
if perform_unification then
- NCicUnification.unify hdb metasenv subst context newtype expty
+ NCicUnification.unify rdb metasenv subst context newtype expty
else metasenv, subst
in
metasenv, subst, newterm, newtype
| NCicUnification.Uncertain _ as exc -> first exc tl
in
first exc
- (look_for_coercion metasenv subst context infty expty)
+ (NCicCoercion.look_for_coercion
+ rdb.NRstatus.coerc_db metasenv subst context infty expty)
-and force_to_sort hdb
- ~look_for_coercion metasenv subst context t orig_t localise ty
-=
+and force_to_sort rdb metasenv subst context t orig_t localise ty =
match NCicReduction.whd ~subst context ty with
| C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty ->
metasenv, subst, t, ty
metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
| C.Sort _ as ty -> metasenv, subst, t, ty
| ty ->
- try_coercions hdb ~localise ~look_for_coercion metasenv subst context
+ try_coercions rdb ~localise metasenv subst context
t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false
(Uncertain (lazy (localise orig_t,
"The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
with NCicUtils.Subst_not_found _ -> aux 'M')
| _ -> aux 'H'
-and eat_prods hdb
- ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args
+and eat_prods rdb
+ ~localise metasenv subst context orig_he he ty_he args
=
(*D*)inside 'E'; try let rc =
let rec aux metasenv subst args_so_far he ty_he = function
match NCicReduction.whd ~subst context ty_he with
| C.Prod (_,s,t) ->
let metasenv, subst, arg, _ =
- typeof hdb ~look_for_coercion ~localise
+ typeof rdb ~localise
metasenv subst context arg (Some s) in
let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
aux metasenv subst (arg :: args_so_far) he t tl
| C.Meta _
| C.Appl (C.Meta _ :: _) as t ->
let metasenv, subst, arg, ty_arg =
- typeof hdb ~look_for_coercion ~localise
+ typeof rdb ~localise
metasenv subst context arg None in
let name = guess_name subst context ty_arg in
let metasenv, _, meta, _ =
let flex_prod = C.Prod (name, ty_arg, meta) in
(* next line grants that ty_args is a type *)
let metasenv,subst, flex_prod, _ =
- typeof hdb ~look_for_coercion ~localise metasenv subst
+ typeof rdb ~localise metasenv subst
context flex_prod None in
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^
NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
let metasenv, subst =
- try NCicUnification.unify hdb metasenv subst context t flex_prod
+ try NCicUnification.unify rdb metasenv subst context t flex_prod
with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
("The term %s has an inferred type %s, but is applied to the" ^^
" argument %s of type %s")
(List.length args) (List.length args_so_far))))
| ty ->
let metasenv, subst, newhead, newheadty =
- try_coercions hdb ~localise ~look_for_coercion metasenv subst context
+ try_coercions rdb ~localise metasenv subst context
(NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
(NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
false
;;
-let typeof_obj hdb
- ?(localise=fun _ -> Stdpp.dummy_loc)
- ~look_for_coercion (uri,height,metasenv,subst,obj)
+let typeof_obj
+ rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
=
prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj));
let check_type metasenv subst context (ty as orig_ty) = (* XXX fattorizza *)
let metasenv, subst, ty, sort =
- typeof hdb ~localise ~look_for_coercion metasenv subst context ty None
+ typeof rdb ~localise metasenv subst context ty None
in
let metasenv, subst, ty, sort =
- force_to_sort hdb ~look_for_coercion
- metasenv subst context ty orig_ty localise sort
+ force_to_sort rdb metasenv subst context ty orig_ty localise sort
in
metasenv, subst, ty, sort
in
match bo with
| Some bo ->
let metasenv, subst, bo, ty =
- typeof hdb ~localise ~look_for_coercion
- metasenv subst [] bo (Some ty)
+ typeof rdb ~localise metasenv subst [] bo (Some ty)
in
let height = (* XXX recalculate *) height in
metasenv, subst, Some bo, ty, height
List.fold_left
(fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
let metasenv, subst, dbo, ty =
- typeof hdb ~localise ~look_for_coercion
- metasenv subst types dbo (Some ty)
+ typeof rdb ~localise metasenv subst types dbo (Some ty)
in
metasenv, subst, (relevance,name,k,ty,dbo)::fl)
(metasenv, subst, []) rev_fl
match item1,item2 with
(n1,C.Decl ty1),(n2,C.Decl ty2) ->
if n1 = n2 then
- NCicUnification.unify hdb ~test_eq_only:true metasenv
+ NCicUnification.unify rdb ~test_eq_only:true metasenv
subst context ty1 ty2,true
else
(metasenv,subst),false
| (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
if n1 = n2 then
let metasenv,subst =
- NCicUnification.unify hdb ~test_eq_only:true metasenv
+ NCicUnification.unify rdb ~test_eq_only:true metasenv
subst context ty1 ty2
in
- NCicUnification.unify hdb ~test_eq_only:true metasenv
+ NCicUnification.unify rdb ~test_eq_only:true metasenv
subst context bo1 bo2,true
else
(metasenv,subst),false
exception AssertFailure of string Lazy.t;;
val typeof :
- NCicUnifHint.db ->
+ NRstatus.refiner_status ->
?localise:(NCic.term -> Stdpp.location) ->
- look_for_coercion:(
- NCic.metasenv -> NCic.substitution -> NCic.context ->
- (* inferred type, expected type *)
- NCic.term -> NCic.term ->
- (* enriched metasenv, new term, its type, metavriable to
- * be unified with the old term *)
- (NCic.metasenv * NCic.term * NCic.term * NCic.term) list
- ) ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term option -> (* term, expected type *)
NCic.metasenv * NCic.substitution * NCic.term * NCic.term
(* menv, subst,refined term, type *)
val typeof_obj :
- NCicUnifHint.db ->
+ NRstatus.refiner_status ->
?localise:(NCic.term -> Stdpp.location) ->
- look_for_coercion:(
- NCic.metasenv -> NCic.substitution -> NCic.context ->
- (* inferred type, expected type *)
- NCic.term -> NCic.term ->
- (* enriched metasenv, new term, its type, metavriable to
- * be unified with the old term *)
- (NCic.metasenv * NCic.term * NCic.term * NCic.term) list
- ) ->
NCic.obj -> NCic.obj
if List.length l > 1 then
combine mk_hint l
else [])
- [] (CoercDb.to_list ())
+ [] (CoercDb.to_list (CoercDb.dump ()))
in
List.fold_left
(fun db -> function
val index_hint:
db -> NCic.context -> NCic.term -> NCic.term -> int -> db
- (* gets the old imperative coercion DB *)
-val db : unit -> db
val add_user_provided_hint : Cic.term -> int -> unit
val empty_db : db
in
mk_lambda context 0 argsty
-and instantiate hdb test_eq_only metasenv subst context n lc t swap =
+and instantiate rdb test_eq_only metasenv subst context n lc t swap =
(*D*) inside 'I'; try let rc =
pp (lazy(string_of_int n ^ " :=?= "^
NCicPp.ppterm ~metasenv ~subst ~context t));
let unify test_eq_only m s c t1 t2 =
- if swap then unify hdb test_eq_only m s c t2 t1
- else unify hdb test_eq_only m s c t1 t2
+ if swap then unify rdb test_eq_only m s c t2 t1
+ else unify rdb test_eq_only m s c t1 t2
in
let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
let metasenv, subst, t =
metasenv, subst
(*D*) in outside(); rc with exn -> outside (); raise exn
-and unify hdb test_eq_only metasenv subst context t1 t2 =
+and unify rdb test_eq_only metasenv subst context t1 t2 =
(*D*) inside 'U'; try let rc =
let fo_unif test_eq_only metasenv subst t1 t2 =
(*D*) inside 'F'; try let rc =
| (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
- let metasenv, subst = unify hdb true metasenv subst context s1 s2 in
- unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
+ let metasenv, subst = unify rdb true metasenv subst context s1 s2 in
+ unify rdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
| (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
- let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in
- let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in
+ let metasenv,subst=unify rdb test_eq_only metasenv subst context ty1 ty2 in
+ let metasenv,subst=unify rdb test_eq_only metasenv subst context s1 s2 in
let context = (name1, C.Def (s1,ty1))::context in
- unify hdb test_eq_only metasenv subst context t1 t2
+ unify rdb test_eq_only metasenv subst context t1 t2
| (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
(try
(fun t1 t2 (metasenv, subst, to_restrict, i) ->
try
let metasenv, subst =
- unify hdb test_eq_only metasenv subst context
+ unify rdb test_eq_only metasenv subst context
(NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
in
metasenv, subst, to_restrict, i-1
let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
let term1 = NCicSubstitution.subst_meta lc1 term in
let term2 = NCicSubstitution.subst_meta lc2 term in
- unify hdb test_eq_only metasenv subst context term1 term2
+ unify rdb test_eq_only metasenv subst context term1 term2
with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
| _, NCic.Meta (n, _) when is_locked n subst ->
let metasenv, lambda_Mj =
lambda_intros metasenv subst context t1 args
in
- unify hdb test_eq_only metasenv subst context
+ unify rdb test_eq_only metasenv subst context
(C.Meta (i,l)) lambda_Mj,
i
| NCic.Meta (i,_) -> (metasenv, subst), i
match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
in
let metasenv, subst =
- instantiate hdb test_eq_only metasenv subst context j lj t2 true
+ instantiate rdb test_eq_only metasenv subst context j lj t2 true
in
(try
let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
(try
let _,_,term,_ = NCicUtils.lookup_subst n subst in
let term = NCicSubstitution.subst_meta lc term in
- unify hdb test_eq_only metasenv subst context term t
+ unify rdb test_eq_only metasenv subst context term t
with NCicUtils.Subst_not_found _->
- instantiate hdb test_eq_only metasenv subst context n lc
+ instantiate rdb test_eq_only metasenv subst context n lc
(NCicReduction.head_beta_reduce ~subst t) false)
| t, C.Meta (n,lc) ->
(try
let _,_,term,_ = NCicUtils.lookup_subst n subst in
let term = NCicSubstitution.subst_meta lc term in
- unify hdb test_eq_only metasenv subst context t term
+ unify rdb test_eq_only metasenv subst context t term
with NCicUtils.Subst_not_found _->
- instantiate hdb test_eq_only metasenv subst context n lc
+ instantiate rdb test_eq_only metasenv subst context n lc
(NCicReduction.head_beta_reduce ~subst t) true)
| NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
let _,_,term,_ = NCicUtils.lookup_subst i subst in
let term = NCicSubstitution.subst_meta l term in
- unify hdb test_eq_only metasenv subst context
+ unify rdb test_eq_only metasenv subst context
(mk_appl ~upto:(List.length args) term args) t2
| _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
let _,_,term,_ = NCicUtils.lookup_subst i subst in
let term = NCicSubstitution.subst_meta l term in
- unify hdb test_eq_only metasenv subst context t1
+ unify rdb test_eq_only metasenv subst context t1
(mk_appl ~upto:(List.length args) term args)
| NCic.Appl (NCic.Meta (i,_)::_ as l1),
(try
List.fold_left2
(fun (metasenv, subst) t1 t2 ->
- unify hdb test_eq_only metasenv subst context t1 t2)
+ unify rdb test_eq_only metasenv subst context t1 t2)
(metasenv,subst) l1 l2
with Invalid_argument _ ->
raise (fail_exc metasenv subst context t1 t2))
lambda_intros metasenv subst context t1 args
in
let metasenv, subst =
- unify hdb test_eq_only metasenv subst context
+ unify rdb test_eq_only metasenv subst context
(C.Meta (i,l)) lambda_Mj
in
let metasenv, subst =
- unify hdb test_eq_only metasenv subst context t1 t2
+ unify rdb test_eq_only metasenv subst context t1 t2
in
(try
let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
lambda_intros metasenv subst context t2 args
in
let metasenv, subst =
- unify hdb test_eq_only metasenv subst context
+ unify rdb test_eq_only metasenv subst context
lambda_Mj (C.Meta (i,l))
in
let metasenv, subst =
- unify hdb test_eq_only metasenv subst context t1 t2
+ unify rdb test_eq_only metasenv subst context t1 t2
in
(try
let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
let b, relevance =
match relevance with b::tl -> b,tl | _ -> true, [] in
let metasenv, subst =
- try unify hdb test_eq_only metasenv subst context t1 t2
+ try unify rdb test_eq_only metasenv subst context t1 t2
with UnificationFailure _ | Uncertain _ when not b ->
metasenv, subst
in
raise (uncert_exc metasenv subst context t1 t2)
else
let metasenv, subst =
- unify hdb test_eq_only metasenv subst context outtype1 outtype2 in
+ unify rdb test_eq_only metasenv subst context outtype1 outtype2 in
let metasenv, subst =
- try unify hdb test_eq_only metasenv subst context term1 term2
+ try unify rdb test_eq_only metasenv subst context term1 term2
with UnificationFailure _ | Uncertain _ when is_prop ->
metasenv, subst
in
(try
List.fold_left2
(fun (metasenv,subst) ->
- unify hdb test_eq_only metasenv subst context)
+ unify rdb test_eq_only metasenv subst context)
(metasenv, subst) pl1 pl2
with Invalid_argument _ ->
raise (uncert_exc metasenv subst context t1 t2))
NCicPp.ppterm ~metasenv ~subst ~context t2);
*)
let candidates =
- NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
+ NCicUnifHint.look_for_hint
+ rdb.NRstatus.uhint_db metasenv subst context t1 t2
in
let rec cand_iter = function
| [] -> None (* raise exc *)
let metasenv,subst =
List.fold_left
(fun (metasenv, subst) (x,y) ->
- unify hdb test_eq_only metasenv subst context x y)
+ unify rdb test_eq_only metasenv subst context x y)
(metasenv, subst) premises
in
Some (metasenv, subst)
(*D*) in outside(); rc with exn -> outside (); raise exn
;;
-let unify hdb ?(test_eq_only=false) =
+let unify rdb ?(test_eq_only=false) =
indent := "";
- unify hdb test_eq_only;;
+ unify rdb test_eq_only;;
exception AssertFailure of string Lazy.t;;
val unify :
- NCicUnifHint.db ->
+ NRstatus.refiner_status ->
?test_eq_only:bool -> (* default: false *)
NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term ->
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
+
+type refiner_status = {
+ coerc_db : NCicCoercion.db;
+ uhint_db : NCicUnifHint.db;
+}
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
+
+type refiner_status = {
+ coerc_db : NCicCoercion.db;
+ uhint_db : NCicUnifHint.db;
+}
+nCicTacReduction.cmi:
+nTacStatus.cmi:
nTactics.cmi: nTacStatus.cmi
+nCicElim.cmi:
nCicTacReduction.cmo: nCicTacReduction.cmi
nCicTacReduction.cmx: nCicTacReduction.cmi
nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
--- /dev/null
++letin: basta la refine fatta con occurcheck
++cut: letin; clearbody ~-1 (cosa sia ~-1 è da capirsi)
+
+-generalize:
+ a) verificare che tutti i termini selezionati siano convertibili
+ b) spostare i termini selezionati nel contesto corrente/spostare il
+ termine bucato sotto un lambda
+ c) bucare e liftare deve essere fatto contemporaneamente
+ d) poi usare tatticali per fare cut + apply
+
+=fail:
+=id:
+
+apply:
+applyS:
+intros:
+elim:
+cases:
+rewrite:
+??replace: rewrite (?:A=B); [2: apply eq_a_b ]
+=auto/demodulate/solve_rewrite:
+change:
+clear/clearbody:
+destruct:
+inversion:
+lapply:
+??compose:
+whd/simpl/normalize:
+fold:
+unfold:
+
+assumption:
+constructor:
+exists:
+left:
+right:
+reflexivity:
+symmetry:
+transitivity:
+split:
+
+decompose:
+
+#####
+absurd:
+contradiction:
+exact:
+elim_type:
+fourier:
+ring:
+
+####
+applyP:
+fwd_simpl:
type lowtac_status = {
pstatus : NCic.obj;
- lstatus : LexiconEngine.status
+ estatus : NEstatus.extra_status;
}
type lowtactic = lowtac_status -> int -> lowtac_status
(List.rev destination, List.rev source)
in
let lc = (0,NCic.Ctx (List.rev lc)) in
- let db = NCicUnifHint.db () in (* XXX fixme *)
let (metasenv, subst), t =
NCicMetaSubst.delift
~unify:(fun m s c t1 t2 ->
- try Some (NCicUnification.unify db m s c t1 t2)
+ try Some (NCicUnification.unify
+ status.estatus.NEstatus.rstatus m s c t1 t2)
with
| NCicUnification.UnificationFailure _
| NCicUnification.Uncertain _ -> None)
let status, (_,_,x) = relocate status context ty in status, Some x
in
let uri,height,metasenv,subst,obj = status.pstatus in
- let metasenv, subst, lexicon_status, t =
+ let metasenv, subst, estatus, t =
GrafiteDisambiguate.disambiguate_nterm expty
- status.lstatus context metasenv subst t
+ status.estatus context metasenv subst t
in
let new_pstatus = uri,height,metasenv,subst,obj in
- { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t)
+ { estatus = estatus; pstatus = new_pstatus }, (None, context, t)
;;
let typeof status ctx t =
let status, (_,_,b) = relocate status ctx b in
let n,h,metasenv,subst,o = status.pstatus in
let metasenv, subst =
- NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx a b
+ NCicUnification.unify status.estatus.NEstatus.rstatus metasenv subst ctx a b
in
{ status with pstatus = n,h,metasenv,subst,o }
;;
let status, (n,_, e) = relocate status ctx e in status, n, Some e
in
let name,height,metasenv,subst,obj = status.pstatus in
- let db = NCicUnifHint.db () in (* XXX fixme *)
- let coercion_db = NCicCoercion.db () in
- let look_for_coercion = NCicCoercion.look_for_coercion coercion_db in
+ let rdb = status.estatus.NEstatus.rstatus in
let metasenv, subst, t, ty =
- NCicRefiner.typeof db ~look_for_coercion metasenv subst ctx term expty
+ NCicRefiner.typeof rdb metasenv subst ctx term expty
in
{ status with pstatus = name,height,metasenv,subst,obj },
(nt,ctx,t), (ne,ctx,ty)
type lowtac_status = {
pstatus : NCic.obj;
- lstatus : LexiconEngine.status
+ estatus : NEstatus.extra_status;
}
type lowtactic = lowtac_status -> int -> lowtac_status
+helm_registry.cmi:
helm_registry.cmo: helm_registry.cmi
helm_registry.cmx: helm_registry.cmi
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+proofEngineTypes.cmi:
proofEngineHelpers.cmi: proofEngineTypes.cmi
+proofEngineReduction.cmi:
continuationals.cmi: proofEngineTypes.cmi
tacticals.cmi: proofEngineTypes.cmi
reductionTactics.cmi: proofEngineTypes.cmi
proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
+hashtbl_equiv.cmi:
metadataQuery.cmi: proofEngineTypes.cmi
+universe.cmi:
autoTypes.cmi: proofEngineTypes.cmi
+autoCache.cmi:
+paramodulation/utils.cmi:
+closeCoercionGraph.cmi:
+paramodulation/subst.cmi:
paramodulation/equality.cmi: paramodulation/utils.cmi \
paramodulation/subst.cmi
paramodulation/founif.cmi: paramodulation/subst.cmi
auto.cmi: proofEngineTypes.cmi automationCache.cmi
destructTactic.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
+inversion_principle.cmi:
ring.cmi: proofEngineTypes.cmi
setoids.cmi: proofEngineTypes.cmi
+fourier.cmi:
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
+history.cmi:
statefulProofEngine.cmi: proofEngineTypes.cmi
tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi
declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi
*)
let close_coercion_graph src tgt uri saturations baseuri =
(* check if the coercion already exists *)
- let coercions = CoercDb.to_list () in
+ let coercions = CoercDb.to_list (CoercDb.dump ()) in
let todo_list = get_closure_coercions src tgt (uri,saturations,0) coercions in
debug_print (lazy("composed " ^ string_of_int (List.length todo_list)));
let todo_list = filter_duplicates todo_list coercions in
rc
;;
-
(* returns the list of ids that should be factorized *)
let get_duplicate_step_in_wfo bag l p =
let ol = List.rev l in
+threadSafe.cmi:
+extThread.cmi:
threadSafe.cmo: threadSafe.cmi
threadSafe.cmx: threadSafe.cmi
extThread.cmo: extThread.cmi
+uriManager.cmi:
uriManager.cmo: uriManager.cmi
uriManager.cmx: uriManager.cmi
+whelp.cmi:
+fwdQueries.cmi:
whelp.cmo: whelp.cmi
whelp.cmx: whelp.cmi
fwdQueries.cmo: fwdQueries.cmi
+xml.cmi:
+xmlPushParser.cmi:
xml.cmo: xml.cmi
xml.cmx: xml.cmi
xmlPushParser.cmo: xmlPushParser.cmi
+xmlDiff.cmi:
xmlDiff.cmo: xmlDiff.cmi
xmlDiff.cmx: xmlDiff.cmi
ANNOTOPTION =
endif
-OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION)
+OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION)
OCAMLDEP_FLAGS = -pp $(CAMLP5O)
PKGS = -package "$(MATITA_REQUIRES)"
CPKGS = -package "$(MATITA_CREQUIRES)"
`NRef (NReference.reference_of_string uri)
in
(MatitaMathView.cicBrowser ())#load uri));
- let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in
- let sequents_observer _ grafite_status =
+ let browser_observer _ = MatitaMathView.refresh_all_browsers () in
+ let sequents_observer grafite_status =
sequents_viewer#reset;
match grafite_status.proof_status with
| Incomplete_proof ({ stack = stack } as incomplete_proof) ->
ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
in
addDebugItem "dump aliases" (fun _ ->
- let status = script#lexicon_status in
+ let status = GrafiteTypes.get_lexicon script#grafite_status in
LexiconEngine.dump_aliases HLog.debug "" status);
(* FG: DEBUGGING
addDebugItem "dump interpretations" (fun _ ->
"(" ^ string_of_int saturations ^ ")")
ul)) ^ ":"
^ CoercDb.string_of_carr s ^ " -> " ^ CoercDb.string_of_carr t))
- (CoercDb.to_list ()));
+ (CoercDb.to_list (CoercDb.dump ())));
addDebugSeparator ();
let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in
(* addDebugItem "save (sequent) MathML to matita.xml"
in
GrafiteTypes.set_metasenv metasenv grafite_status,tac
-let disambiguate_command lexicon_status_ref grafite_status cmd =
+let disambiguate_command estatus lexicon_status_ref grafite_status cmd =
let baseuri = GrafiteTypes.get_baseuri grafite_status in
- let lexicon_status,metasenv,cmd =
+ let estatus,metasenv,cmd =
GrafiteDisambiguate.disambiguate_command ~baseuri
- !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd
+ { estatus with NEstatus.lstatus = !lexicon_status_ref }
+ (GrafiteTypes.get_proof_metasenv grafite_status) cmd
in
- lexicon_status_ref := lexicon_status;
+ lexicon_status_ref := estatus.NEstatus.lstatus;
GrafiteTypes.set_metasenv metasenv grafite_status,cmd
let disambiguate_macro lexicon_status_ref grafite_status macro context =
in
GrafiteTypes.set_metasenv metasenv grafite_status,macro
-let eval_ast ?do_heavy_checks lexicon_status
- grafite_status (text,prefix_len,ast)
-=
+let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) =
+ let lexicon_status = GrafiteTypes.get_lexicon grafite_status in
let dump = not (Helm_registry.get_bool "matita.moo") in
let lexicon_status_ref = ref lexicon_status in
let baseuri = GrafiteTypes.get_baseuri grafite_status in
let changed_lexicon = ref false in
let wrap f x = changed_lexicon := true; f x in
- let grafite_status =
- match grafite_status.GrafiteTypes.ng_status with
- | GrafiteTypes.CommandMode _ ->
- { grafite_status with GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode lexicon_status }
- | GrafiteTypes.ProofMode s ->
- { grafite_status with GrafiteTypes.ng_status =
- GrafiteTypes.ProofMode
- { s with NTacStatus.istatus = { s.NTacStatus.istatus with NTacStatus.lstatus = lexicon_status }}}
- in
let new_grafite_status,new_objs =
match ast with
| G.Executable (_, G.Command (_, G.Coercion _)) when dump ->
| ast ->
GrafiteEngine.eval_ast
~disambiguate_tactic:(wrap (disambiguate_tactic text prefix_len lexicon_status_ref))
- ~disambiguate_command:(wrap (disambiguate_command lexicon_status_ref))
+ ~disambiguate_command:(wrap
+ (disambiguate_command
+ (GrafiteTypes.get_estatus grafite_status) lexicon_status_ref))
~disambiguate_macro:(wrap (disambiguate_macro lexicon_status_ref))
?do_heavy_checks grafite_status (text,prefix_len,ast)
in
let new_lexicon_status =
if !changed_lexicon then
!lexicon_status_ref
- else
- match new_grafite_status.GrafiteTypes.ng_status with
- | GrafiteTypes.CommandMode l -> l
- | GrafiteTypes.ProofMode s -> s.NTacStatus.istatus.NTacStatus.lstatus
+ else
+ GrafiteTypes.get_lexicon new_grafite_status
in
let new_lexicon_status =
LexiconSync.add_aliases_for_objs new_lexicon_status new_objs in
let new_lexicon_status =
LexiconEngine.set_proof_aliases lexicon_status [k,value]
in
- new_lexicon_status,
- ((grafite_status,new_lexicon_status),Some (k,value))::acc
+ let grafite_status =
+ GrafiteTypes.set_lexicon new_lexicon_status grafite_status
+ in
+ new_lexicon_status, (grafite_status ,Some (k,value))::acc
) (lexicon_status,[]) new_aliases
in
- ((new_grafite_status,new_lexicon_status),None)::intermediate_states
+ let new_grafite_status =
+ GrafiteTypes.set_lexicon new_lexicon_status new_grafite_status
+ in
+ ((new_grafite_status),None)::intermediate_states
+;;
exception TryingToAdd of string
-exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status
+exception EnrichedWithStatus of exn * GrafiteTypes.status
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
+ ?(watch_statuses=fun _ -> ()) grafite_status str cb
=
let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop lexicon_status grafite_status statuses =
+ let rec loop grafite_status statuses =
let loop =
- if first_statement_only then fun _ _ statuses -> statuses
+ if first_statement_only then fun _ statuses -> statuses
else loop
in
- let stop,l,g,s =
+ let stop,g,s =
try
let cont =
try
+ let lexicon_status = GrafiteTypes.get_lexicon grafite_status in
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
+ | None -> true, grafite_status, statuses
| Some (lexicon_status,ast) ->
+ let grafite_status =
+ GrafiteTypes.set_lexicon lexicon_status grafite_status
+ in
(match ast with
GrafiteParser.LNone _ ->
- watch_statuses lexicon_status grafite_status ;
- false, lexicon_status, grafite_status,
- (((grafite_status,lexicon_status),None)::statuses)
+ watch_statuses grafite_status ;
+ false, grafite_status,
+ (((grafite_status),None)::statuses)
| GrafiteParser.LSome ast ->
cb grafite_status ast;
- let new_statuses =
- eval_ast ?do_heavy_checks lexicon_status
- grafite_status ("",0,ast) in
+ let new_statuses =
+ eval_ast ?do_heavy_checks grafite_status ("",0,ast) in
if enforce_no_new_aliases then
List.iter
(fun (_,alias) ->
| Some (k,value) ->
let newtxt = LexiconAstPp.pp_alias value in
raise (TryingToAdd newtxt)) new_statuses;
- let grafite_status,lexicon_status =
+ let grafite_status =
match new_statuses with
[] -> assert false
| (s,_)::_ -> s
in
- watch_statuses lexicon_status grafite_status ;
- false, lexicon_status, grafite_status, (new_statuses @ statuses))
+ watch_statuses grafite_status ;
+ false, grafite_status, (new_statuses @ statuses))
with exn when not matita_debug ->
- raise (EnrichedWithStatus (exn, lexicon_status, grafite_status))
+ raise (EnrichedWithStatus (exn, grafite_status))
in
- if stop then s else loop l g s
+ if stop then s else loop g s
in
- loop lexicon_status grafite_status []
+ loop grafite_status []
;;
val eval_ast :
?do_heavy_checks:bool ->
- LexiconEngine.status ->
GrafiteTypes.status ->
string * int *
((CicNotationPt.term, CicNotationPt.term,
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
GrafiteAst.statement) ->
- ((GrafiteTypes.status * LexiconEngine.status) *
+ (GrafiteTypes.status *
(DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
(* heavy checks slow down the compilation process but give you some interesting
* infos like if the theorem is a duplicate *)
-exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status
+exception EnrichedWithStatus of exn * GrafiteTypes.status
(* should be used only by the compiler since it looses the
* disambiguation_context (text,prefix_len,_) *)
include_paths:string list ->
?do_heavy_checks:bool ->
?enforce_no_new_aliases:bool -> (* default true *)
- ?watch_statuses:(LexiconEngine.status -> GrafiteTypes.status -> unit) ->
- LexiconEngine.status ->
+ ?watch_statuses:(GrafiteTypes.status -> unit) ->
GrafiteTypes.status ->
Ulexing.lexbuf ->
(GrafiteTypes.status ->
(CicNotationPt.term, CicNotationPt.term,
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
GrafiteAst.statement -> unit) ->
- ((GrafiteTypes.status * LexiconEngine.status) *
+ (GrafiteTypes.status *
(DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
None, "NTypeChecker failure: " ^ Lazy.force msg
| NCicTypeChecker.AssertFailure msg ->
None, "NTypeChecker assert failure: " ^ Lazy.force msg
+ | NCicEnvironment.ObjectNotFound msg ->
+ None, "NCicEnvironment object not found: " ^ Lazy.force msg
| NCicRefiner.AssertFailure msg ->
None, "NRefiner assert failure: " ^ Lazy.force msg
| NCicEnvironment.BadDependency (msg,e) ->
None, "Already defined: " ^ UriManager.string_of_uri s
| DisambiguateChoices.Choice_not_found msg ->
None, ("Disambiguation choice not found: " ^ Lazy.force msg)
- | MatitaEngine.EnrichedWithStatus (exn,_,_) ->
+ | MatitaEngine.EnrichedWithStatus (exn,_) ->
None, "EnrichedWithStatus "^snd(to_string exn)
| NTacStatus.Error msg ->
None, "NTactic error: " ^ Lazy.force msg
let clean_current_baseuri grafite_status =
LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status]
-let save_moo lexicon_status grafite_status =
+let save_moo grafite_status =
let script = MatitaScript.current () in
let baseuri = GrafiteTypes.get_baseuri grafite_status in
let no_pstatus =
GrafiteMarshal.save_moo moo_fname
grafite_status.GrafiteTypes.moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname
- lexicon_status.LexiconEngine.lexicon_content_rev
+ (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev
| _ -> clean_current_baseuri grafite_status
;;
else saveAsScript ()
in
let abandon_script () =
- let lexicon_status = (s ())#lexicon_status in
let grafite_status = (s ())#grafite_status in
if source_view#buffer#modified then
(match ask_unsaved main#toplevel with
| `YES -> saveScript ()
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel);
- save_moo lexicon_status grafite_status
+ save_moo grafite_status
in
let loadScript () =
let script = s () in
match ask_unsaved main#toplevel with
| `YES ->
saveScript ();
- save_moo script#lexicon_status script#grafite_status;
+ save_moo script#grafite_status;
GMain.Main.quit ()
| `NO -> GMain.Main.quit ()
| `CANCEL -> ()
else
- (save_moo script#lexicon_status script#grafite_status;
+ (save_moo script#grafite_status;
GMain.Main.quit ()));
connect_button main#scriptAdvanceButton advance;
connect_button main#scriptRetractButton retract;
ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
}
-let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal
+let eval_with_engine include_paths guistuff grafite_status user_goal
skipped_txt nonskipped_txt st
=
let module TAPp = GrafiteAstPp in
let enriched_history_fragment =
MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
"matita.do_heavy_checks")
- lexicon_status grafite_status (text,prefix_len,st)
+ grafite_status (text,prefix_len,st)
in
let enriched_history_fragment = List.rev enriched_history_fragment in
(* really fragile *)
stupid_indenter script
;;
-let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
+let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
let module TAPp = GrafiteAstPp in
let module MQ = MetadataQuery in
let module MDB = LibraryDb in
let loc = HExtlib.floc_of_loc (0,text_len) in
let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
let res,_,_parsed_text_len =
- eval_statement include_paths buffer guistuff lexicon_status
+ eval_statement include_paths buffer guistuff
grafite_status user_goal script statement
in
(* we need to replace all the parsed_text *)
in
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [({grafite_status with proof_status = No_proof},lexicon_status), parsed_text ],"",
+ [({grafite_status with proof_status = No_proof}), parsed_text ],"",
parsed_text_length
| TA.Check (_,term) ->
let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
[], str, String.length parsed_text
and eval_executable include_paths (buffer : GText.buffer) guistuff
-lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
+grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
script ex loc
=
let module TAPp = GrafiteAstPp in
~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
(Glib.Utf8.length skipped_txt))) ;
eval_with_engine include_paths
- guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt
+ guistuff grafite_status user_goal skipped_txt nonskipped_txt
(TA.Executable (loc, ex))
with
MatitaTypes.Cancel -> [], "", 0
None -> []
| Some n -> GrafiteTypes.get_proof_context grafite_status n in
let grafite_status,macro = lazy_macro context in
- eval_macro include_paths buffer guistuff lexicon_status grafite_status
+ eval_macro include_paths buffer guistuff grafite_status
user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
-and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
+and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
let (lexicon_status,st), unparsed_text =
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
wrap_with_make include_paths
- (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status
+ (GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
+ (GrafiteTypes.get_lexicon grafite_status)
in
ast, text
- | `Ast (st, text) -> (lexicon_status, st), text
+ | `Ast (st, text) -> (GrafiteTypes.get_lexicon grafite_status, st), text
in
+ let grafite_status = GrafiteTypes.set_lexicon lexicon_status grafite_status in
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let start, stop = HExtlib.loc_of_floc floc in
match st with
| GrafiteParser.LNone loc ->
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
- [(grafite_status,lexicon_status),parsed_text],"",
+ [grafite_status,parsed_text],"",
parsed_text_length
| GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) ->
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
let s = String.sub unparsed_text parsed_text_length remain_len in
let s,text,len =
try
- eval_statement include_paths buffer guistuff lexicon_status
+ eval_statement include_paths buffer guistuff
grafite_status user_goal script (`Raw s)
with
HExtlib.Localized (floc, exn) ->
let _, nonskipped, skipped, parsed_text_length =
text_of_loc loc
in
- eval_executable include_paths buffer guistuff lexicon_status
+ eval_executable include_paths buffer guistuff
grafite_status user_goal unparsed_text skipped nonskipped script ex loc
let fresh_script_id =
BuildTimeConf.core_notation_script
in
let grafite_status = GrafiteSync.init lexicon_status baseuri in
- grafite_status,lexicon_status
+ grafite_status
in
let read_include_paths file =
try
(* history can't be empty, the invariant above grant that it contains at
* least the init grafite_status *)
- method grafite_status = match history with (s,_)::_ -> s | _ -> assert false
- method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false
+ method grafite_status = match history with s::_ -> s | _ -> assert false
method private _advance ?statement () =
let s = match statement with Some s -> s | None -> self#getFuture in
HLog.debug ("evaluating: " ^ first_line s ^ " ...");
let entries, newtext, parsed_len =
try
- eval_statement self#include_paths buffer guistuff self#lexicon_status
+ eval_statement self#include_paths buffer guistuff
self#grafite_status userGoal self (`Raw s)
with End_of_file -> raise Margin
in
with Failure _ -> None)
| _ -> userGoal <- None
- method private _retract offset lexicon_status grafite_status new_statements
+ method private _retract offset grafite_status new_statements
new_history
=
- let cur_grafite_status,cur_lexicon_status =
+ let cur_grafite_status =
match history with s::_ -> s | [] -> assert false
in
- LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status;
+ LexiconSync.time_travel
+ ~present:(GrafiteTypes.get_lexicon cur_grafite_status)
+ ~past:(GrafiteTypes.get_lexicon grafite_status);
GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
statements <- new_statements;
history <- new_history;
method retract () =
try
- let cmp,new_statements,new_history,(grafite_status,lexicon_status) =
+ let cmp,new_statements,new_history,grafite_status =
match statements,history with
stat::statements, _::(status::_ as history) ->
assert (Glib.Utf8.validate stat);
| [],[_] -> raise Margin
| _,_ -> assert false
in
- self#_retract cmp lexicon_status grafite_status new_statements
+ self#_retract cmp grafite_status new_statements
new_history;
self#notify
with
val mutable observers = []
- method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) =
+ method addObserver (o: GrafiteTypes.status -> unit) =
observers <- o :: observers
method private notify =
- let lexicon_status = self#lexicon_status in
let grafite_status = self#grafite_status in
- List.iter (fun o -> o lexicon_status grafite_status) observers
+ List.iter (fun o -> o grafite_status) observers
method loadFromString s =
buffer#set_text s;
end
method private goto_top =
- let grafite_status,lexicon_status =
+ let grafite_status =
let rec last x = function
| [] -> x
| hd::tl -> last hd tl
in
- last (self#grafite_status,self#lexicon_status) history
+ last (self#grafite_status) history
in
(* FIXME: this is not correct since there is no undo for
* library_objects.set_default... *)
GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
- LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status
+ LexiconSync.time_travel
+ ~present:(GrafiteTypes.get_lexicon self#grafite_status)
+ ~past:(GrafiteTypes.get_lexicon grafite_status)
method private reset_buffer =
statements <- [];
in
let rec back_until_cursor len = (* go backward until locked < cursor *)
function
- statements, ((grafite_status,lexicon_status)::_ as history)
+ statements, ((grafite_status)::_ as history)
when len <= 0 ->
- self#_retract (icmp - len) lexicon_status grafite_status statements
+ self#_retract (icmp - len) grafite_status statements
history
| statement::tl1, _::tl2 ->
back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2)
| GrafiteParser.LSome (GrafiteAst.Executable _) -> false
in
try
- is_there_only_comments self#lexicon_status self#getFuture
+ is_there_only_comments
+ (GrafiteTypes.get_lexicon self#grafite_status) self#getFuture
with
| LexiconEngine.IncludedFileNotCompiled _
| HExtlib.Localized _
method error_tag : GText.tag
(** @return current status *)
- method lexicon_status: LexiconEngine.status
method grafite_status: GrafiteTypes.status
(** {2 Observers} *)
- method addObserver :
- (LexiconEngine.status -> GrafiteTypes.status -> unit) -> unit
+ method addObserver : (GrafiteTypes.status -> unit) -> unit
(** {2 History} *)
(** {2 Initialization} *)
let grafite_status = (ref [] : GrafiteTypes.status list ref)
-let lexicon_status = (ref [] : LexiconEngine.status list ref)
let run_script is eval_function =
- let lexicon_status',grafite_status' =
- match !lexicon_status,!grafite_status with
- | ss::_, s::_ -> ss,s
- | _,_ -> assert false
+ let grafite_status' =
+ match !grafite_status with
+ | s::_ -> s
+ | _ -> assert false
in
let cb = fun _ _ -> () in
let matita_debug = Helm_registry.get_bool "matita.debug" in
try
- match eval_function lexicon_status' grafite_status' is cb with
+ match eval_function grafite_status' is cb with
[] -> raise End_of_file
- | ((grafite_status'',lexicon_status''),None)::_ ->
- lexicon_status := lexicon_status''::!lexicon_status;
+ | (grafite_status'',None)::_ ->
grafite_status := grafite_status''::!grafite_status
| (s,Some _)::_ -> raise AttemptToInsertAnAlias
with
| n,_::l -> drop (n-1,l)
| _,[] -> assert false
in
- let to_be_dropped = List.length !lexicon_status - n in
+ let to_be_dropped = List.length !grafite_status - n in
let safe_hd = function [] -> assert false | he::_ -> he in
- let cur_lexicon_status = safe_hd !lexicon_status in
let cur_grafite_status = safe_hd !grafite_status in
- lexicon_status := drop (to_be_dropped, !lexicon_status) ;
grafite_status := drop (to_be_dropped, !grafite_status) ;
- let lexicon_status = safe_hd !lexicon_status in
let grafite_status = safe_hd !grafite_status in
LexiconSync.time_travel
- ~present:cur_lexicon_status ~past:lexicon_status;
+ ~present:(GrafiteTypes.get_lexicon cur_grafite_status)
+ ~past:(GrafiteTypes.get_lexicon grafite_status);
GrafiteSync.time_travel
~present:cur_grafite_status ~past:grafite_status;
interactive_loop (Some n)
| `Do command ->
let str = Ulexing.from_utf8_string command in
- let watch_statuses lexicon_status grafite_status =
+ let watch_statuses grafite_status =
match grafite_status.GrafiteTypes.proof_status with
GrafiteTypes.Incomplete_proof
{GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
run_script str
(MatitaEngine.eval_from_stream ~first_statement_only:true
~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
- interactive_loop (Some (List.length !lexicon_status))
+ interactive_loop (Some (List.length !grafite_status))
with
| GrafiteEngine.Macro (floc,_) ->
let x, y = HExtlib.loc_of_floc floc in
let system_mode = Helm_registry.get_bool "matita.system" in
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
- lexicon_status :=
- [CicNotation2.load_notation ~include_paths
- BuildTimeConf.core_notation_script] ;
- grafite_status := [GrafiteSync.init (List.hd !lexicon_status) "cic:/matita/tests/"];
+ grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths
+ BuildTimeConf.core_notation_script) "cic:/matita/tests/"];
Sys.catch_break true;
let origcb = HLog.get_log_callback () in
let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
| GrafiteEngine.Drop -> clean_exit 1
);
let proof_status,moo_content_rev,lexicon_content_rev =
- match !lexicon_status,!grafite_status with
- | ss::_, s::_ ->
+ match !grafite_status with
+ | s::_ ->
s.proof_status, s.moo_content_rev,
- ss.LexiconEngine.lexicon_content_rev
- | _,_ -> assert false
+ (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev
+ | _ -> assert false
in
if proof_status <> GrafiteTypes.No_proof then
begin
if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
else pp_ast_statement
in
- let lexicon_status, grafite_status =
- let rec aux_for_dump x lexicon_status grafite_status =
+ let grafite_status =
+ let rec aux_for_dump x grafite_status =
try
match
MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
- lexicon_status grafite_status buf x
+ grafite_status buf x
with
- | [] -> lexicon_status, grafite_status
- | ((grafite,lexicon),None)::_ -> lexicon, grafite
- | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
+ | [] -> grafite_status
+ | (g,None)::_ -> g
+ | (g,Some _)::_ ->
+ raise (AttemptToInsertAnAlias (GrafiteTypes.get_lexicon g))
with MatitaEngine.EnrichedWithStatus
- (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn ->
+ (GrafiteEngine.Macro (floc, f), grafite) as exn ->
match f (get_macro_context (Some grafite)) with
| _, GrafiteAst.Inline (_, _suri, _params) ->
(*
in
!out str;
*)
- aux_for_dump x lexicon grafite
+ aux_for_dump x grafite
|_-> raise exn
in
- aux_for_dump print_cb lexicon_status grafite_status
+ aux_for_dump print_cb grafite_status
in
let elapsed = Unix.time () -. time in
let proof_status,moo_content_rev,lexicon_content_rev =
grafite_status.proof_status, grafite_status.moo_content_rev,
- lexicon_status.LexiconEngine.lexicon_content_rev
+ (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev
in
if proof_status <> GrafiteTypes.No_proof then
(HLog.error
~present:lexicon_status ~past:initial_lexicon_status;
*)
clean_exit baseuri false
- | MatitaEngine.EnrichedWithStatus (exn, _lexicon, _grafite) as exn' ->
+ | MatitaEngine.EnrichedWithStatus (exn, _grafite) as exn' ->
(match exn with
| Sys.Break -> HLog.error "user break!"
| HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+axiom A : Type.
+axiom B : Type.
+axiom C : Type.
+
+axiom f : A → B.
+axiom g : B → C.
+
+(* nlemma xxx : ∀P:C → Prop. ∀x:A. P x. *)
+
+coercion f. coercion g.
+
+axiom T : Type.
+
+axiom h : A → T. coercion h.
+
+nlemma xxx : ∀P:C → Prop. ∀x:A. P x.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+
+axiom A : Type.
+
+axiom a : A.
+axiom b : A.
+
+axiom B : Type.
+
+axiom c : B.
+axiom d : B.
+
+
+notation "#" with precedence 90 for @{ 'foo }.
+interpretation "a" 'foo = a.
+interpretation "b" 'foo = b.
+interpretation "c" 'foo = c.
+interpretation "d" 'foo = d.
+
+alias symbol "foo" = "c".
+alias symbol "foo" = "b".
+alias symbol "foo" = "d".
+alias symbol "foo" = "b".
+
+lemma xx : ∀P: A → B → Prop. P # #. (* NON STAMPA GLI ALIAS *)
+
projects / helm.git / commitdiff