From aa6153d8e480abfe52b00e1bc6bd48ef84c48988 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 12 Sep 2005 16:06:33 +0000 Subject: [PATCH] Added support for multiple disambiguation passes. Actually, passes can differ in: - whether they use library as fallback for unbound domain items or not - whether they use multi-aliases or not - whether they use coercions or not. The current policy is to postpone the use of coercions as much as possible and to fallback to library only as a last resort. Passes can be configured from matitaDisambiguator.ml. --- helm/matita/matita.txt | 46 +++++++++++----------- helm/matita/matitaDisambiguator.ml | 61 +++++++++++++++++++++++++++-- helm/matita/matitaDisambiguator.mli | 28 +++++++++++-- helm/matita/matitaEngine.ml | 37 ++++++++++------- helm/matita/matitaScript.ml | 14 ++++--- helm/matita/matitaSync.ml | 22 ++++++----- 6 files changed, 148 insertions(+), 60 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 543aa8b1b..253b18d02 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -96,27 +96,6 @@ TODO mentre si compila Z/times.ma. Il bug sembra essere transiente. - in MatitaEngine unificare/rimuovere eval_string, eval_from_stream e eval_from_stream_greedy - - disambiguazione: attualmente io (CSC) ho committato la versione di - disambiguate.ml che NON ricorda gli alias in caso di disambiguazione - univoca (senza scelte per l'utente). [ cercare commento "Experimental" ] - Il problema di questa soluzione e' che rallenta in maniera significativa - l'esecuzione degli script. DOMANDA: quanto costano le fasi di - fetch/decode/execute delle linee dello script? - Una possibile alternativa e' avere alias "soft": se la disambiguazione - fallisce gli alias soft vengono ripuliti e si riprova. - Altra soluzione (Gares): avere alias multipli e provare tutti gli alias - multipli. Da combinare con il "ritenta con istanze multiple in caso di - fallimento". - SOLUZIONE PENSATA CON ANDREA: 1. la interpretate aggiunge un alias - implicito; 2. gli alias vengono ricordati come nella soluzione originale - (e veloce); 3. se la disambiguazione fallisce, allora gli alias vengono - dimenticati (quali? tutti? tutti tranne quelli chiesti all'utente?) - e si ritenta; se fallisce ancora si generano - istanze differenti e si ritenta; 4. ritentare anche senza e poi con - coercions? oppure ordinare preferendo la soluzione che non ha introdotto - coercions?; 5. che fare se alla fine restano piu' scelte? se si mettono - gli alias nello script viene un paciugo, credo! in particolare quando - vengono usate n istanze - matitamake foo/a.ma non funziona; bisogna chiamarlo con matitamake /x/y/z/foo/a.ma - notazione -> Luca e Zack @@ -125,11 +104,32 @@ TODO DEMONI E ALTRO DONE +- disambiguazione: attualmente io (CSC) ho committato la versione di + disambiguate.ml che NON ricorda gli alias in caso di disambiguazione + univoca (senza scelte per l'utente). [ cercare commento "Experimental" ] + Il problema di questa soluzione e' che rallenta in maniera significativa + l'esecuzione degli script. DOMANDA: quanto costano le fasi di + fetch/decode/execute delle linee dello script? + Una possibile alternativa e' avere alias "soft": se la disambiguazione + fallisce gli alias soft vengono ripuliti e si riprova. + Altra soluzione (Gares): avere alias multipli e provare tutti gli alias + multipli. Da combinare con il "ritenta con istanze multiple in caso di + fallimento". + SOLUZIONE PENSATA CON ANDREA: 1. la interpretate aggiunge un alias + implicito; 2. gli alias vengono ricordati come nella soluzione originale + (e veloce); 3. se la disambiguazione fallisce, allora gli alias vengono + dimenticati (quali? tutti? tutti tranne quelli chiesti all'utente?) + e si ritenta; se fallisce ancora si generano + istanze differenti e si ritenta; 4. ritentare anche senza e poi con + coercions? oppure ordinare preferendo la soluzione che non ha introdotto + coercions?; 5. che fare se alla fine restano piu' scelte? se si mettono + gli alias nello script viene un paciugo, credo! in particolare quando + vengono usate n istanze -> Zack, CSC - theorem t: True. elim O. ==> BOOM! unificazione di una testa flessibile con True -> Gares - parsing contestuale (tattiche replace, change e forse altre) capire dove fare la select per avere i contesti in cui disambiguare gli - altri argomenti. -> Zack, Enrico, CSC + altri argomenti. -> Zack - tattica unfold su rel a let-in bound variables: c'e' ancora un bug aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto del goal e non in quello del pattern. Pertanto invece di cercare di @@ -143,7 +143,7 @@ DONE con pattern, visto che in tal caso e' l'intero parsing a dover essere fatto in un contesto differente. Risolvendo quel bug si risolve automaticamente anche questo. - -> Zack, Enrico, CSC + -> Zack - Usare il cicbrowser per fare "Whelp instance": lui riscrive la barra con la notazione alla Coq V7.0 che non riesce piu' a riparsare! -> Zack - implementare inclusione file di configurazione (perche' ora tutti diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index d2c11890f..db69cb71d 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -29,7 +29,9 @@ open MatitaTypes exception Ambiguous_input -type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list +type choose_uris_callback = + id:string -> UriManager.uri list -> UriManager.uri list + type choose_interp_callback = (string * string) list list -> int list let mono_uris_callback ~id = @@ -37,6 +39,7 @@ let mono_uris_callback ~id = function l -> l else raise Ambiguous_input + let mono_interp_callback _ = raise Ambiguous_input let _choose_uris_callback = ref mono_uris_callback @@ -65,6 +68,58 @@ module Disambiguator = Disambiguate.Make (Callbacks) (* implement module's API *) -let disambiguate_term = Disambiguator.disambiguate_term +let disambiguate_thing ~aliases + ~(f:?fresh_instances:bool -> aliases:Disambiguate.aliases -> 'a -> 'b) + ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b) + (thing: 'a) += + let library = false, DisambiguateTypes.empty_environment in + let multi_aliases = true, aliases in + let mono_aliases = false, aliases in + let passes = (* *) + [ (false, mono_aliases, false); + (false, multi_aliases, false); + (true, library, false); + (true, mono_aliases, true); + (true, multi_aliases, true); + (true, library, true); + ] + in + let try_pass (fresh_instances, aliases, use_coercions) = + CoercDb.use_coercions := use_coercions; + f ~fresh_instances ~aliases thing + in + let rec aux = + function + | [ pass ] -> try_pass pass + | hd :: tl -> + (try + try_pass hd + with Disambiguate.NoWellTypedInterpretation -> + let (_, user_asked) as res = aux tl in + if user_asked then res else set_aliases aliases res) + | [] -> assert false + in + let saved_use_coercions = !CoercDb.use_coercions in + try + let res = aux passes in + CoercDb.use_coercions := saved_use_coercions; + res + with exn -> + CoercDb.use_coercions := saved_use_coercions; + raise exn + +let set_aliases aliases (choices, user_asked) = + (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices), + user_asked + +let disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph ~aliases term = + let f = + Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph + in + disambiguate_thing ~aliases ~f ~set_aliases term + +let disambiguate_obj ~dbd ~aliases ~uri obj = + let f = Disambiguator.disambiguate_obj ~dbd ~uri in + disambiguate_thing ~aliases ~f ~set_aliases obj -let disambiguate_obj = Disambiguator.disambiguate_obj diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index 740de989e..a5d0aed44 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -47,8 +47,28 @@ val mono_interp_callback: choose_interp_callback (** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) -include Disambiguate.Disambiguator - (* - * val disambiguate_term: ... - *) +val disambiguate_term : + dbd:Mysql.dbd -> + context:Cic.context -> + metasenv:Cic.metasenv -> + ?initial_ugraph:CicUniv.universe_graph -> + aliases:DisambiguateTypes.environment -> (* previous interpretation status *) + DisambiguateTypes.term -> + (DisambiguateTypes.environment * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.term * + CicUniv.universe_graph) list * (* disambiguated term *) + bool (* has interactive_interpretation_choice been invoked? *) + +(** @param fresh_instances as per disambiguate_term *) +val disambiguate_obj : + dbd:Mysql.dbd -> + aliases:DisambiguateTypes.environment -> (* previous interpretation status *) + uri:UriManager.uri option -> (* required only for inductive types *) + GrafiteAst.obj -> + (DisambiguateTypes.environment * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.obj * + CicUniv.universe_graph) list * (* disambiguated obj *) + bool (* has interactive_interpretation_choice been invoked? *) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index a9b46267f..19944417f 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -156,7 +156,7 @@ let tactic_of_ast ast = | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term let singleton = function - | [x] -> x + | [x], _ -> x | _ -> assert false let disambiguate_term status_ref term = @@ -192,9 +192,7 @@ let disambiguate_lazy_term status_ref term = cic, metasenv, ugraph) let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) = - let interp path = - Disambiguate.interpretate_path [] !status_ref.aliases path - in + let interp path = Disambiguate.interpretate_path [] path in let goal_path = interp goal_path in let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in let wanted = @@ -513,12 +511,9 @@ let disambiguate_obj status obj = | GrafiteAst.Inductive _ -> assert false | GrafiteAst.Theorem _ -> None in let (aliases, metasenv, cic, _) = - match - MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~uri obj - with - | [x] -> x - | _ -> assert false + singleton + (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) + ~aliases:(status.aliases) ~uri obj) in let proof_status = match status.proof_status with @@ -612,7 +607,7 @@ let eval_command opts status cmd = set_option status name value | GrafiteAst.Drop loc -> raise Drop | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty = + let uri, metasenv, bo, ty = match status.proof_status with | Proof (Some uri, metasenv, body, ty) -> uri, metasenv, body, ty @@ -636,24 +631,36 @@ let eval_command opts status cmd = code in DisambiguatePp *) match spec with | GrafiteAst.Ident_alias (id,uri) -> - DisambiguateTypes.Environment.add + DisambiguateTypes.Environment.cons (DisambiguateTypes.Id id) (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) status.aliases | GrafiteAst.Symbol_alias (symb, instance, desc) -> - DisambiguateTypes.Environment.add + DisambiguateTypes.Environment.cons (DisambiguateTypes.Symbol (symb,instance)) (DisambiguateChoices.lookup_symbol_by_dsc symb desc) status.aliases | GrafiteAst.Number_alias (instance,desc) -> - DisambiguateTypes.Environment.add + DisambiguateTypes.Environment.cons (DisambiguateTypes.Num instance) (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases in MatitaSync.set_proof_aliases status aliases | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *) | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *) - | GrafiteAst.Interpretation _ + | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm -> + let status' = + { status with + moo_content_rev = + (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev } + in + let aliases' = + DisambiguateTypes.Environment.cons + (DisambiguateTypes.Symbol (symbol, 0)) + (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) + status.aliases + in + MatitaSync.set_proof_aliases status' aliases' | GrafiteAst.Notation _ as stm -> { status with moo_content_rev = (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev } diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 987e60560..1bd4b9fd1 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -109,14 +109,16 @@ let eval_with_engine guistuff status user_goal parsed_text st = let new_aliases = match ex with | TA.Command (_, TA.Alias _) - | TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty + | TA.Command (_, TA.Include _) + | TA.Command (_, TA.Interpretation _) -> + DisambiguateTypes.Environment.empty | _ -> MatitaSync.alias_diff ~from:status new_status in (* we remove the defined object since we consider them "automatic aliases" *) let initial_space,status,new_status_and_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in - DTE.fold ( + DTE.fold_flatten ( fun k ((v,_) as value) (initial_space,status,acc) -> let b = try @@ -131,9 +133,9 @@ let eval_with_engine guistuff status user_goal parsed_text st = let initial_space = if initial_space = "" then "\n" else initial_space in initial_space ^ - DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in + DisambiguatePp.pp_environment(DTE.cons k value DTE.empty) in let new_status = - {status with aliases = DTE.add k value status.aliases} + {status with aliases = DTE.cons k value status.aliases} in "\n",new_status,((new_status, new_text)::acc) ) new_aliases (initial_space,status,[]) in @@ -207,7 +209,7 @@ let disambiguate term status = let aliases = MatitaMisc.get_proof_aliases status in let interps = MD.disambiguate_term dbd context metasenv aliases term in match interps with - | [_,_,x,_] -> x + | [_,_,x,_], _ -> x | _ -> assert false let eval_macro guistuff status unparsed_text parsed_text script mac = @@ -299,7 +301,7 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = in let _, metasenv , term, ugraph = match interps with - | [x] -> x + | [x], _ -> x | _ -> assert false in let ty,_ = CTC.type_of_aux' metasenv context term ugraph in diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index e12c1cd14..a77c24761 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -29,25 +29,29 @@ open MatitaTypes let alias_diff ~from status = let module Map = DisambiguateTypes.Environment in - Map.fold + Map.fold_flatten (fun domain_item codomain_item acc -> if not (Map.mem domain_item from.aliases) then - Map.add domain_item codomain_item acc + Map.cons domain_item codomain_item acc else begin try - let description1 = fst(Map.find domain_item from.aliases) in - let description2 = fst(Map.find domain_item status.aliases) in - if description1 <> description2 then - Map.add domain_item codomain_item acc - else - acc + let codomain1 = Map.find domain_item from.aliases in + let codomain2 = Map.find domain_item status.aliases in + List.fold_right + (fun item env -> + let dsc = fst item in + if not (List.exists (fun (dsc', _) -> dsc'=dsc) codomain1) then + Map.cons domain_item codomain_item env + else + env) + codomain2 acc with Not_found -> acc end) status.aliases Map.empty let set_proof_aliases status aliases = - let new_status = {status with aliases = aliases } in + let new_status = { status with aliases = aliases } in let diff = alias_diff ~from:status new_status in let textual_diff = if DisambiguateTypes.Environment.is_empty diff then -- 2.39.2