From 8ecc9fb74f80c2f5b3e3c70f0a625e63a48292fb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 15 Sep 2005 17:40:32 +0000 Subject: [PATCH] Yet another implementation of the single aliases / multi aliases idea. The new implementation is much simpler: single aliases are used everywhere in the disambiguation phase; however, when a term needs to be looked for in the library, it can be looked in a user-provided multi aliases environment instead. NOTE: the new implementation fixes a bug of the previous implementation: the most recent alias in the multi-alias set was printed last in the .moo files, changing the performances of the system. --- helm/matita/matitaDisambiguator.ml | 34 ++++++++++++++++++----------- helm/matita/matitaDisambiguator.mli | 26 +--------------------- helm/matita/matitaEngine.ml | 20 +++++++++-------- helm/matita/matitaMisc.ml | 2 -- helm/matita/matitaMisc.mli | 1 - helm/matita/matitaScript.ml | 16 +++++++------- helm/matita/matitaSync.ml | 24 ++++++++++---------- helm/matita/matitaTypes.ml | 1 + helm/matita/matitaTypes.mli | 1 + 9 files changed, 55 insertions(+), 70 deletions(-) diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index b7de40ed9..5a7fe0b9f 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -68,14 +68,18 @@ module Disambiguator = Disambiguate.Make (Callbacks) (* implement module's API *) -let disambiguate_thing ~aliases - ~(f:?fresh_instances:bool -> aliases:Disambiguate.aliases -> 'a -> 'b) +let disambiguate_thing ~aliases ~universe + ~(f:?fresh_instances:bool -> + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + 'a -> 'b) ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b) (thing: 'a) = - let library = true, DisambiguateTypes.empty_environment in - let multi_aliases = true, aliases in - let mono_aliases = false, aliases in + assert (universe <> None); + let library = false, DisambiguateTypes.Environment.empty, None in + let multi_aliases=false, DisambiguateTypes.Environment.empty, universe in + let mono_aliases = true, aliases, None in let passes = (* *) [ (false, mono_aliases, false); (false, multi_aliases, false); @@ -86,12 +90,12 @@ let disambiguate_thing ~aliases (true, library, true); ] in - let try_pass (fresh_instances, aliases, use_coercions) = + let try_pass (fresh_instances, (_, aliases, universe), use_coercions) = CoercDb.use_coercions := use_coercions; - f ~fresh_instances ~aliases thing + f ~fresh_instances ~aliases ~universe thing in - let set_aliases (instances,(use_multi_aliases,_),_) (_, user_asked as res) = - if not use_multi_aliases && not instances then + let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = + if use_mono_aliases && not instances then res else if user_asked then res (* one shot aliases *) @@ -120,13 +124,17 @@ 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 disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph + ~aliases ~universe term + = + assert (fresh_instances = None); let f = Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph in - disambiguate_thing ~aliases ~f ~set_aliases term + disambiguate_thing ~aliases ~universe ~f ~set_aliases term -let disambiguate_obj ~dbd ~aliases ~uri obj = +let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj = + assert (fresh_instances = None); let f = Disambiguator.disambiguate_obj ~dbd ~uri in - disambiguate_thing ~aliases ~f ~set_aliases obj + disambiguate_thing ~aliases ~universe ~f ~set_aliases obj diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index a5d0aed44..01fa97ef0 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -47,28 +47,4 @@ val mono_interp_callback: choose_interp_callback (** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) -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? *) - +include Disambiguate.Disambiguator diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 8c891b043..577e243a6 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -165,7 +165,8 @@ let disambiguate_term status_ref term = let (aliases, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status) + ~aliases:status.aliases ~universe:(Some status.multi_aliases) + ~context:(MatitaMisc.get_proof_context status) ~metasenv:(MatitaMisc.get_proof_metasenv status) term) in let status = MatitaTypes.set_metasenv metasenv status in @@ -184,8 +185,8 @@ let disambiguate_lazy_term status_ref term = let (aliases, metasenv, cic, ugraph) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) - ~initial_ugraph:ugraph ~aliases:status.aliases ~context ~metasenv - term) + ~initial_ugraph:ugraph ~aliases:status.aliases + ~universe:(Some status.multi_aliases) ~context ~metasenv term) in let status = MatitaTypes.set_metasenv metasenv status in let status = MatitaSync.set_proof_aliases status aliases in @@ -511,7 +512,7 @@ let disambiguate_obj status obj = let (aliases, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~uri obj) + ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj) in let proof_status = match status.proof_status with @@ -628,17 +629,17 @@ let eval_command opts status cmd = code in DisambiguatePp *) match spec with | GrafiteAst.Ident_alias (id,uri) -> - DisambiguateTypes.Environment.cons + DisambiguateTypes.Environment.add (DisambiguateTypes.Id id) (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) status.aliases | GrafiteAst.Symbol_alias (symb, instance, desc) -> - DisambiguateTypes.Environment.cons + DisambiguateTypes.Environment.add (DisambiguateTypes.Symbol (symb,instance)) (DisambiguateChoices.lookup_symbol_by_dsc symb desc) status.aliases | GrafiteAst.Number_alias (instance,desc) -> - DisambiguateTypes.Environment.cons + DisambiguateTypes.Environment.add (DisambiguateTypes.Num instance) (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases in @@ -648,7 +649,7 @@ let eval_command opts status cmd = | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm -> let status' = add_moo_content [stm] status in let aliases' = - DisambiguateTypes.Environment.cons + DisambiguateTypes.Environment.add (DisambiguateTypes.Symbol (symbol, 0)) (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) status.aliases @@ -800,7 +801,8 @@ let default_options () = let initial_status = lazy { - aliases = DisambiguateTypes.empty_environment; + aliases = DisambiguateTypes.Environment.empty; + multi_aliases = DisambiguateTypes.Environment.empty; moo_content_rev = []; proof_status = No_proof; options = default_options (); diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 78e780a15..97d6cac47 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -275,8 +275,6 @@ let get_proof_conclusion status = conclusion | _ -> statement_error "no ongoing proof" -let get_proof_aliases status = status.aliases - let qualify status name = get_string_option status "baseuri" ^ "/" ^ name let unopt = function None -> failwith "unopt: None" | Some v -> v diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 568bcc5ed..21045c0a3 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -113,7 +113,6 @@ val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv val get_proof_context: MatitaTypes.status -> Cic.context val get_proof_conclusion: MatitaTypes.status -> Cic.term -val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment (** given the base name of an image, returns its full path *) val image_path: string -> string diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 8ef5146ca..f12ac877d 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -118,7 +118,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = let initial_space,status,new_status_and_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in - DTE.fold_flatten ( + DTE.fold ( fun k ((v,_) as value) (initial_space,status,acc) -> let b = try @@ -133,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.cons k value DTE.empty) in + DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in let new_status = - {status with aliases = DTE.cons k value status.aliases} + MatitaSync.set_proof_aliases status (DTE.add k value status.aliases) in "\n",new_status,((new_status, new_text)::acc) ) new_aliases (initial_space,status,[]) in @@ -206,8 +206,9 @@ let disambiguate term status = let dbd = MatitaDb.instance () in let metasenv = MatitaMisc.get_proof_metasenv status in let context = MatitaMisc.get_proof_context status in - let aliases = MatitaMisc.get_proof_aliases status in - let interps = MD.disambiguate_term dbd context metasenv aliases term in + let interps = + MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases + ~universe:(Some status.multi_aliases) term in match interps with | [_,_,x,_], _ -> x | _ -> assert false @@ -294,10 +295,9 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = | TA.Check (_,term) -> let metasenv = MatitaMisc.get_proof_metasenv status in let context = MatitaMisc.get_proof_context status in - let aliases = MatitaMisc.get_proof_aliases status in let interps = - MatitaDisambiguator.disambiguate_term - dbd context metasenv aliases term + MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv + ~aliases:status.aliases ~universe:(Some status.multi_aliases) term in let _, metasenv , term, ugraph = match interps with diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 55cb4a45c..c4f8f5547 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -29,23 +29,19 @@ open MatitaTypes let alias_diff ~from status = let module Map = DisambiguateTypes.Environment in - Map.fold_flatten + Map.fold (fun domain_item codomain_item acc -> if not (Map.mem domain_item from.aliases) then - Map.cons domain_item codomain_item acc + Map.add domain_item codomain_item acc else begin try - 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 + 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 with Not_found -> acc end) status.aliases Map.empty @@ -53,6 +49,10 @@ let alias_diff ~from status = let set_proof_aliases status aliases = let new_status = { status with aliases = aliases } in let diff = alias_diff ~from:status new_status in + let multi_aliases = + DisambiguateTypes.Environment.fold DisambiguateTypes.Environment.cons + diff status.multi_aliases in + let new_status = { new_status with multi_aliases = multi_aliases } in if DisambiguateTypes.Environment.is_empty diff then new_status else diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 4ac480cf1..5df68ea86 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -61,6 +61,7 @@ type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command type status = { aliases: DisambiguateTypes.environment; + multi_aliases: DisambiguateTypes.multiple_environment; moo_content_rev: ast_command list; proof_status: proof_status; options: options; diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index c0946c89f..51744f152 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -51,6 +51,7 @@ type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command type status = { aliases: DisambiguateTypes.environment; (** disambiguation aliases *) + multi_aliases: DisambiguateTypes.multiple_environment; moo_content_rev: ast_command list; proof_status: proof_status; options: options; -- 2.39.2