X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconEngine.ml;h=805da25c8e53c18340649fcbd6ead78db3b6fdde;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=8a51e9523055fe51326a5be45372ba53fdbb6495;hpb=8e6a30412bbac3acc0a020e0fe90d492b0fc6776;p=helm.git diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index 8a51e9523..805da25c8 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -25,21 +25,27 @@ (* $Id$ *) -let out = ref ignore +module L = LexiconAst -let set_callback f = out := f +let debug = ref false (* lexicon file name * ma file name *) exception IncludedFileNotCompiled of string * string exception MetadataNotFound of string (* file name *) type status = { - aliases: DisambiguateTypes.environment; (** disambiguation aliases *) - multi_aliases: DisambiguateTypes.multiple_environment; + aliases: L.alias_spec DisambiguateTypes.Environment.t; + multi_aliases: L.alias_spec list DisambiguateTypes.Environment.t; lexicon_content_rev: LexiconMarshal.lexicon; notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) } +let dump_aliases out msg status = + out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:"); + DisambiguateTypes.Environment.iter + (fun _ x -> out (LexiconAstPp.pp_alias x)) + status.aliases + let initial_status = { aliases = DisambiguateTypes.Environment.empty; multi_aliases = DisambiguateTypes.Environment.empty; @@ -53,49 +59,56 @@ let add_lexicon_content cmds status = List.fold_right (fun cmd acc -> match cmd with - | LexiconAst.Alias _ - | LexiconAst.Include _ - | LexiconAst.Notation _ -> cmd :: (List.filter ((<>) cmd) acc) - | LexiconAst.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc) + | L.Alias _ + | L.Include _ + | L.Notation _ -> cmd :: (List.filter ((<>) cmd) acc) + | L.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc) cmds content in -(* prerr_endline ("new lexicon content: " ^ String.concat " " (List.map - LexiconAstPp.pp_command content')); *) +(* + prerr_endline ("new lexicon content: " ^ + String.concat "; " (List.map LexiconAstPp.pp_command content') + ); +*) { status with lexicon_content_rev = content' } let set_proof_aliases mode status new_aliases = - if mode = LexiconAst.WithoutPreferences then + if mode = L.WithoutPreferences then status else let commands_of_aliases = List.map - (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias)) + (fun _,alias -> L.Alias (HExtlib.dummy_floc, alias)) in let aliases = List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) status.aliases new_aliases in let multi_aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) - status.multi_aliases new_aliases in + List.fold_left (fun acc (d,c) -> + DisambiguateTypes.Environment.cons L.description_of_alias + d c acc) + status.multi_aliases new_aliases + in let new_status = { status with multi_aliases = multi_aliases ; aliases = aliases} in if new_aliases = [] then new_status else - let aliases = - DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases - in let status = - add_lexicon_content (commands_of_aliases aliases) new_status + add_lexicon_content (commands_of_aliases new_aliases) new_status in status -let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = +let rec eval_command ?(mode=L.WithPreferences) status cmd = +(* + let bmode = match mode with L.WithPreferences -> true | _ -> false in + Printf.eprintf "Include preferences: %b\n" bmode; +*) let cmd = match cmd with - | LexiconAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> + | L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> let rec disambiguate = function CicNotationPt.ApplPattern l -> @@ -106,28 +119,33 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args) -> let item = DisambiguateTypes.Id id in - (try - let t = - snd (DisambiguateTypes.Environment.find item status.aliases) - status.aliases "" [] in - let uri = CicUtil.uri_of_term t in - CicNotationPt.UriPattern uri + begin try + match DisambiguateTypes.Environment.find item status.aliases with + L.Ident_alias (_, uri) -> + (try + CicNotationPt.NRefPattern + (NReference.reference_of_string uri) + with + NReference.IllFormedReference _ -> + CicNotationPt.UriPattern (UriManager.uri_of_string uri)) + | _ -> assert false with Not_found -> - prerr_endline ("Domain item not found: " ^ + prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ (DisambiguateTypes.string_of_domain_item item)); - assert false) + dump_aliases prerr_endline "" status; + assert false + end | p -> p in - LexiconAst.Interpretation + L.Interpretation (loc, dsc, (symbol, args), disambiguate cic_appl_pattern) | _-> cmd in - !out cmd; let notation_ids' = CicNotation.process_notation cmd in let status = { status with notation_ids = notation_ids' @ status.notation_ids } in match cmd with - | LexiconAst.Include (loc, baseuri, mode, fullpath) -> + | L.Include (loc, baseuri, mode, fullpath) -> let lexiconpath_rw, lexiconpath_r = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~writable:true ~baseuri, @@ -142,28 +160,25 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = let lexicon = LexiconMarshal.load_lexicon lexiconpath in let status = List.fold_left (eval_command ~mode) status lexicon in status - | LexiconAst.Alias (loc, spec) -> + | L.Alias (loc, spec) -> let diff = (*CSC: Warning: this code should be factorized with the corresponding code in DisambiguatePp *) match spec with - | LexiconAst.Ident_alias (id,uri) -> - [DisambiguateTypes.Id id, - (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))] - | LexiconAst.Symbol_alias (symb, instance, desc) -> - [DisambiguateTypes.Symbol (symb,instance), - DisambiguateChoices.lookup_symbol_by_dsc symb desc] - | LexiconAst.Number_alias (instance,desc) -> - [DisambiguateTypes.Num instance, - DisambiguateChoices.lookup_num_by_dsc desc] + | L.Ident_alias (id,uri) -> + [DisambiguateTypes.Id id,spec] + | L.Symbol_alias (symb, instance, desc) -> + [DisambiguateTypes.Symbol (symb,instance),spec] + | L.Number_alias (instance,desc) -> + [DisambiguateTypes.Num instance,spec] in set_proof_aliases mode status diff - | LexiconAst.Interpretation (_, dsc, (symbol, _), _) as stm -> + | L.Interpretation (_, dsc, (symbol, _), _) as stm -> let status = add_lexicon_content [stm] status in let diff = try [DisambiguateTypes.Symbol (symbol, 0), - DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] + L.Symbol_alias (symbol,0,dsc)] with DisambiguateChoices.Choice_not_found msg -> prerr_endline (Lazy.force msg); @@ -171,10 +186,17 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = in let status = set_proof_aliases mode status diff in status - | LexiconAst.Notation _ as stm -> + | L.Notation _ as stm -> add_lexicon_content [stm] status -let eval_command = eval_command ?mode:None +let eval_command status cmd = + if !debug then dump_aliases prerr_endline "before eval_command" status; + let status = eval_command ?mode:None status cmd in + if !debug then dump_aliases prerr_endline "after eval_command" status; + status -let set_proof_aliases = set_proof_aliases LexiconAst.WithPreferences - +let set_proof_aliases status aliases = + if !debug then dump_aliases prerr_endline "before set_proof_aliases" status; + let status = set_proof_aliases L.WithPreferences status aliases in + if !debug then dump_aliases prerr_endline "after set_proof_aliases" status; + status