From dc04177512e6db696f669aa561b86701c4ad2511 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 4 Nov 2010 23:10:56 +0000 Subject: [PATCH] - disambiguation code moved from matitaEngine to grafiteDisambiguate - grafiteDisambiguate.db is now opaque --- .../grafite_engine/grafiteEngine.ml | 33 ++------------- .../components/lexicon/grafiteDisambiguate.ml | 42 +++++++++++++++++++ .../lexicon/grafiteDisambiguate.mli | 15 ++++--- matita/matita/matitaEngine.ml | 11 +++-- 4 files changed, 60 insertions(+), 41 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 7fa62ff74..032af19fb 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -609,37 +609,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = eval_add_constraint status [`Type,u1] [`Type,u2] (* ex lexicon commands *) | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> - let rec disambiguate = - function - NotationPt.ApplPattern l -> - NotationPt.ApplPattern (List.map disambiguate l) - | NotationPt.VarPattern id - when not - (List.exists - (function (NotationPt.IdentArg (_,id')) -> id'=id) args) - -> - let item = DisambiguateTypes.Id id in - begin - try - match - DisambiguateTypes.Environment.find item - status#disambiguate_db.GrafiteDisambiguate.aliases - with - GrafiteAst.Ident_alias (_, uri) -> - NotationPt.NRefPattern (NReference.reference_of_string uri) - | _ -> assert false - with Not_found -> - prerr_endline - ("LexiconEngine.eval_command: domain item not found: " ^ - (DisambiguateTypes.string_of_domain_item item)); - GrafiteDisambiguate.dump_aliases prerr_endline "" status; - raise - (Failure - ((DisambiguateTypes.string_of_domain_item item) ^ " not found")) - end - | p -> p + let cic_appl_pattern = + GrafiteDisambiguate.disambiguate_cic_appl_pattern status args + cic_appl_pattern in - let cic_appl_pattern = disambiguate cic_appl_pattern in eval_interpretation status (dsc,(symbol, args),cic_appl_pattern) | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) -> let l1 = diff --git a/matita/components/lexicon/grafiteDisambiguate.ml b/matita/components/lexicon/grafiteDisambiguate.ml index 5b27aba1b..058ddaec3 100644 --- a/matita/components/lexicon/grafiteDisambiguate.ml +++ b/matita/components/lexicon/grafiteDisambiguate.ml @@ -54,6 +54,14 @@ class status = = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db) end +let eval_with_new_aliases status f = + let status = + status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in + let res = f status in + let new_aliases = status#disambiguate_db.new_aliases in + new_aliases,res +;; + let dump_aliases out msg status = out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:"); DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) @@ -272,3 +280,37 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = in estatus, cic ;; + +let disambiguate_cic_appl_pattern status args = + let rec disambiguate = + function + NotationPt.ApplPattern l -> + NotationPt.ApplPattern (List.map disambiguate l) + | NotationPt.VarPattern id + when not + (List.exists + (function (NotationPt.IdentArg (_,id')) -> id'=id) args) + -> + let item = DisambiguateTypes.Id id in + begin + try + match + DisambiguateTypes.Environment.find item + status#disambiguate_db.aliases + with + GrafiteAst.Ident_alias (_, uri) -> + NotationPt.NRefPattern (NReference.reference_of_string uri) + | _ -> assert false + with Not_found -> + prerr_endline + ("LexiconEngine.eval_command: domain item not found: " ^ + (DisambiguateTypes.string_of_domain_item item)); + dump_aliases prerr_endline "" status; + raise + (Failure + ((DisambiguateTypes.string_of_domain_item item) ^ " not found")) + end + | p -> p + in + disambiguate +;; diff --git a/matita/components/lexicon/grafiteDisambiguate.mli b/matita/components/lexicon/grafiteDisambiguate.mli index 6b203cab4..401eba115 100644 --- a/matita/components/lexicon/grafiteDisambiguate.mli +++ b/matita/components/lexicon/grafiteDisambiguate.mli @@ -23,11 +23,7 @@ * http://helm.cs.unibo.it/ *) -type db = { - aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; - multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; - new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -} +type db class type g_status = object @@ -43,6 +39,10 @@ class status : method set_disambiguate_status: #g_status -> 'self end +val eval_with_new_aliases: + #status as 'status -> ('status -> 'a) -> + (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a + val set_proof_aliases: #status as 'status -> implicit_aliases:bool -> (* implicit ones are made explicit *) @@ -71,3 +71,8 @@ type pattern = val disambiguate_npattern: GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern + +val disambiguate_cic_appl_pattern: + #status -> + NotationPt.argument_pattern list -> + NotationPt.cic_appl_pattern -> NotationPt.cic_appl_pattern diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index a95936c97..4c246a253 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -53,12 +53,11 @@ let eval_macro_screenshot (status : GrafiteTypes.status) name = let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = let baseuri = status#baseuri in - let status = - status#set_disambiguate_db { status#disambiguate_db with GrafiteDisambiguate.new_aliases = [] } in - let status = - GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status - (text,prefix_len,ast) in - let new_aliases = status#disambiguate_db.GrafiteDisambiguate.new_aliases in + let new_aliases,status = + GrafiteDisambiguate.eval_with_new_aliases status + (fun status -> + GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status + (text,prefix_len,ast)) in let _,intermediate_states = List.fold_left (fun (status,acc) (k,value) -> -- 2.39.2