From 50fffea30b07e377834af799cd262d6f5d5aff0c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Dec 2005 16:18:06 +0000 Subject: [PATCH] alias diffing/insertion is now handled by matitaEngine (invoked both by matita and matitac) --- helm/matita/matitaEngine.ml | 77 +++++++++++++++++++++---------- helm/matita/matitaEngine.mli | 15 ++++-- helm/matita/matitaScript.ml | 88 ++++++++++++++++-------------------- helm/matita/matitacLib.ml | 9 +++- 4 files changed, 112 insertions(+), 77 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 40a80afdd..fa9292c89 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -52,39 +52,68 @@ let disambiguate_tactic lexicon_status_ref status goal tac = GrafiteTypes.set_metasenv metasenv status,tac let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status - status ast + grafite_status ast = let lexicon_status_ref = ref lexicon_status in - let status,new_objs = + let new_grafite_status,new_objs = GrafiteEngine.eval_ast ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref) ~disambiguate_command:(disambiguate_command lexicon_status_ref) - ?do_heavy_checks ?clean_baseuri status ast + ?do_heavy_checks ?clean_baseuri grafite_status ast in + let new_lexicon_status = + LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in + let new_aliases = + LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in + let _,intermediate_states = + let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in + List.fold_left + (fun (lexicon_status,acc) (k,((v,_) as value)) -> + let b = + try + UriManager.buri_of_uri (UriManager.uri_of_string v) = baseuri + with + UriManager.IllFormedUri _ -> false (* v is a description, not a URI *) + in + if b then + lexicon_status,acc + else + let new_lexicon_status = + LexiconEngine.set_proof_aliases lexicon_status [k,value] + in + new_lexicon_status, + ((new_grafite_status,new_lexicon_status),Some (k,value))::acc + ) (lexicon_status,[]) new_aliases in - let lexicon_status = - LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs - in - lexicon_status,status + ((new_grafite_status,new_lexicon_status),None)::intermediate_states let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks - ?clean_baseuri lexicon_status status str cb + ?clean_baseuri lexicon_status grafite_status str cb = - let rec loop lexicon_status status = - if prompt then (print_string "matita> "; flush stdout); - try - let lexicon_status,ast = GrafiteParser.parse_statement ~include_paths str lexicon_status in - (match ast with - GrafiteParser.LNone _ -> loop lexicon_status status - | GrafiteParser.LSome ast -> - cb status ast; - let lexicon_status,status = - eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status status ast - in - loop lexicon_status status) - with - End_of_file -> lexicon_status,status -in - loop lexicon_status status + let rec loop lexicon_status grafite_status statuses = + if prompt then (print_string "matita> "; flush stdout); + try + let lexicon_status,ast = + GrafiteParser.parse_statement ~include_paths str lexicon_status + in + (match ast with + GrafiteParser.LNone _ -> + loop lexicon_status grafite_status + (((grafite_status,lexicon_status),None)::statuses) + | GrafiteParser.LSome ast -> + cb grafite_status ast; + let new_statuses = + eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status + grafite_status ast in + let grafite_status,lexicon_status = + match new_statuses with + [] -> assert false + | (s,_)::_ -> s + in + loop lexicon_status grafite_status (new_statuses @ statuses)) + with + End_of_file -> statuses + in + loop lexicon_status grafite_status [] ;; let eval_string ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 02b33c66b..ddc905db3 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -30,7 +30,11 @@ val eval_ast : GrafiteTypes.status -> (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) - GrafiteAst.statement -> LexiconEngine.status * GrafiteTypes.status + GrafiteAst.statement -> + ((GrafiteTypes.status * LexiconEngine.status) * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option + ) list + (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) @@ -40,7 +44,10 @@ val eval_string : ?clean_baseuri:bool -> LexiconEngine.status -> GrafiteTypes.status -> - string -> LexiconEngine.status * GrafiteTypes.status + string -> + ((GrafiteTypes.status * LexiconEngine.status) * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option + ) list val eval_from_stream : include_paths:string list -> @@ -54,4 +61,6 @@ val eval_from_stream : (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) GrafiteAst.statement -> unit) -> - LexiconEngine.status * GrafiteTypes.status + ((GrafiteTypes.status * LexiconEngine.status) * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option + ) list diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index ffa356b53..e4b1544f9 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -113,49 +113,41 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal [ grafite_status, initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] | _ -> initial_space,grafite_status,[] in *) - let new_lexicon_status,new_grafite_status = + let enriched_history_fragment = MatitaEngine.eval_ast ~do_heavy_checks:true new_lexicon_status new_grafite_status st in - let new_aliases = - LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in - (* we remove the defined object since we consider them "automatic aliases" *) - let dummy_st = - TA.Comment (HExtlib.dummy_floc, TA.Note (HExtlib.dummy_floc, "")) - in - let initial_space,lexicon_status,new_status_and_text_list_rev = + let _,new_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in - let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in - List.fold_left ( - fun (initial_space,lexicon_status,acc) (k,((v,_) as value)) -> - let b = - try - UM.buri_of_uri (UM.uri_of_string v) = baseuri - with - UriManager.IllFormedUri _ -> false (* v is a description, not a URI *) - in - if b then - initial_space,lexicon_status,acc - else - let new_text = - let initial_space = - if initial_space = "" then "\n" else initial_space in - initial_space ^ - DisambiguatePp.pp_environment - (DisambiguateTypes.Environment.add k value - DisambiguateTypes.Environment.empty) in - let new_lexicon_status = - LexiconEngine.set_proof_aliases lexicon_status [k,value] - in - "\n",new_lexicon_status,(((new_grafite_status,new_lexicon_status), (new_text, Some dummy_st))::acc) - ) (initial_space,lexicon_status,[]) new_aliases in - let parsed_text = initial_space ^ parsed_text in - let res = - List.rev new_status_and_text_list_rev @ new_status_and_text_list' @ - [(new_grafite_status,new_lexicon_status),(parsed_text, Some st)] + List.fold_right ( + fun (_,alias) (initial_space,acc) -> + match alias with + None -> initial_space,initial_space::acc + | Some (k,((v,_) as value)) -> + let new_text = + let initial_space = + if initial_space = "" then "\n" else initial_space + in + initial_space ^ + DisambiguatePp.pp_environment + (DisambiguateTypes.Environment.add k value + DisambiguateTypes.Environment.empty) + in + "\n",new_text::acc + ) enriched_history_fragment (initial_space,[]) in + let new_text_list_rev = + match enriched_history_fragment,new_text_list_rev with + (_,None)::_, initial_space::tl -> (initial_space ^ parsed_text)::tl + | _,_ -> assert false in - res,parsed_text_length + let res = + try + List.combine (fst (List.split enriched_history_fragment)) new_text_list_rev + with + Invalid_argument _ -> assert false + in + res,parsed_text_length let eval_with_engine guistuff lexicon_status grafite_status user_goal parsed_text st @@ -305,12 +297,14 @@ let eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text pa TA.Apply (loc, CicNotationPt.Uri (suri, None))), Some (TA.Dot loc)))) in +(* let new_lexicon_status,new_grafite_status = MatitaEngine.eval_ast lexicon_status grafite_status ast in let extra_text = comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in [ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ], parsed_text_length +*) assert false (* implementarla con una ricorsione *) | _ -> HLog.error "The result of the urichooser should be only 1 uri, not:\n"; @@ -416,7 +410,7 @@ let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status match st with | GrafiteParser.LNone loc -> let parsed_text, parsed_text_length = text_of_loc loc in - [(grafite_status,lexicon_status),(parsed_text,None)], + [(grafite_status,lexicon_status),parsed_text], parsed_text_length | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> let parsed_text, parsed_text_length = text_of_loc loc in @@ -435,9 +429,8 @@ let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status (offset+parsed_text_length, errorll)) in (match s with - | (statuses,(text, ast)) :: tl -> - (statuses,(parsed_text ^ text, ast))::tl, - parsed_text_length + len + | (statuses,text)::tl -> + (statuses,parsed_text ^ text)::tl,parsed_text_length + len | [] -> [], 0) | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> let parsed_text, parsed_text_length = text_of_loc loc in @@ -524,15 +517,14 @@ object (self) eval_statement buffer guistuff self#lexicon_status self#grafite_status userGoal self st in - let (new_statuses, new_statements, new_asts) = - let statuses, statements = List.split entries in - let texts, asts = List.split statements in - statuses, texts, asts + let new_statuses, new_statements = + let statuses, texts = List.split entries in + statuses, texts in - history <- List.rev new_statuses @ history; - statements <- List.rev new_statements @ statements; + history <- new_statuses @ history; + statements <- new_statements @ statements; let start = buffer#get_iter_at_mark (`MARK locked_mark) in - let new_text = String.concat "" new_statements in + let new_text = String.concat "" (List.rev new_statements) in if statement <> None then buffer#insert ~iter:start new_text else begin diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 47447e49e..e769fd7d6 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -27,6 +27,8 @@ open Printf open GrafiteTypes +exception AttemptToInsertAnAlias + let pp_ast_statement = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj @@ -60,8 +62,11 @@ let run_script is eval_function = HLog.debug ("Executing: ``" ^ stm ^ "''")) in try - let lexicon_status'', grafite_status'' = - eval_function lexicon_status' grafite_status' is cb + let grafite_status'', lexicon_status'' = + match eval_function lexicon_status' grafite_status' is cb with + [] -> assert false + | (s,None)::_ -> s + | (s,Some _)::_ -> raise AttemptToInsertAnAlias in lexicon_status := Some lexicon_status''; grafite_status := Some grafite_status'' -- 2.39.2