X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaEngine.ml;h=a8dcf98092e29a8d68009d012a6469ed3542f18f;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=5f8a1b7a7e6cc74d9d074a5f3d1d8aacf0d95762;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 5f8a1b7a7..a8dcf9809 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -25,7 +25,7 @@ (* $Id$ *) -open Printf +module G = GrafiteAst let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; @@ -35,7 +35,7 @@ let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal t GrafiteDisambiguate.disambiguate_tactic lexicon_status_ref (GrafiteTypes.get_proof_context grafite_status goal) - (GrafiteTypes.get_proof_metasenv grafite_status) + (GrafiteTypes.get_proof_metasenv grafite_status) (Some goal) tac in GrafiteTypes.set_metasenv metasenv grafite_status,tac @@ -61,28 +61,65 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context = let eval_ast ?do_heavy_checks lexicon_status grafite_status (text,prefix_len,ast) = + 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 -> +(* FG: some commands can not be executed when mmas are parsed *************) +(* To be removed when mmas will be executed *) + grafite_status, `Old [] + | ast -> GrafiteEngine.eval_ast - ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref) - ~disambiguate_command:(disambiguate_command lexicon_status_ref) - ~disambiguate_macro:(disambiguate_macro lexicon_status_ref) - ?do_heavy_checks grafite_status (text,prefix_len,ast) in + ~disambiguate_tactic:(wrap (disambiguate_tactic text prefix_len lexicon_status_ref)) + ~disambiguate_command:(wrap (disambiguate_command 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 = - LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in + 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 + in + let new_lexicon_status = + LexiconSync.add_aliases_for_objs new_lexicon_status new_objs in let new_aliases = LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in let _,intermediate_states = List.fold_left - (fun (lexicon_status,acc) (k,((v,_) as value)) -> + (fun (lexicon_status,acc) (k,value) -> + let v = LexiconAst.description_of_alias value in let b = try (* this hack really sucks! *) UriManager.buri_of_uri (UriManager.uri_of_string v) = baseuri with - UriManager.IllFormedUri _ -> false (* v is a description, not a URI *) + UriManager.IllFormedUri _ -> + try + (* this too! *) + let NReference.Ref (uri,_) = NReference.reference_of_string v in + let ouri = NCic2OCic.ouri_of_nuri uri in + UriManager.buri_of_uri ouri = baseuri + with + NReference.IllFormedReference _ -> + false (* v is a description, not a URI *) in if b then lexicon_status,acc @@ -98,16 +135,13 @@ let eval_ast ?do_heavy_checks lexicon_status ((new_grafite_status,new_lexicon_status),None)::intermediate_states exception TryingToAdd of string -exception EnrichedWithLexiconStatus of exn * LexiconEngine.status - -let out = ref ignore - -let set_callback f = out := f +exception EnrichedWithStatus of exn * LexiconEngine.status * 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 = + let matita_debug = Helm_registry.get_bool "matita.debug" in let rec loop lexicon_status grafite_status statuses = let loop = if first_statement_only then fun _ _ statuses -> statuses @@ -130,7 +164,6 @@ let eval_from_stream ~first_statement_only ~include_paths false, lexicon_status, grafite_status, (((grafite_status,lexicon_status),None)::statuses) | GrafiteParser.LSome ast -> - !out ast; cb grafite_status ast; let new_statuses = eval_ast ?do_heavy_checks lexicon_status @@ -140,12 +173,8 @@ let eval_from_stream ~first_statement_only ~include_paths (fun (_,alias) -> match alias with None -> () - | Some (k,((v,_) as value)) -> - let newtxt = - DisambiguatePp.pp_environment - (DisambiguateTypes.Environment.add k value - DisambiguateTypes.Environment.empty) - in + | Some (k,value) -> + let newtxt = LexiconAstPp.pp_alias value in raise (TryingToAdd newtxt)) new_statuses; let grafite_status,lexicon_status = match new_statuses with @@ -154,8 +183,8 @@ let eval_from_stream ~first_statement_only ~include_paths in watch_statuses lexicon_status grafite_status ; false, lexicon_status, grafite_status, (new_statuses @ statuses)) - with exn -> - raise (EnrichedWithLexiconStatus (exn, lexicon_status)) + with exn when not matita_debug -> + raise (EnrichedWithStatus (exn, lexicon_status, grafite_status)) in if stop then s else loop l g s in