From: Claudio Sacerdoti Coen Date: Mon, 9 Jun 2008 20:17:20 +0000 (+0000) Subject: It is now possible to use identifiers in place of URI in "interpreation". X-Git-Tag: make_still_working~5048 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=423bf7f85d0959689266cfc7ca57958a04618002;p=helm.git It is now possible to use identifiers in place of URI in "interpreation". The identifier is mapped to an URI according to the last declared alias. --- diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index 1966251ad..aadb3ddf2 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -88,6 +88,35 @@ let set_proof_aliases mode status new_aliases = let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = + let cmd = + match cmd with + | LexiconAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> + let rec disambiguate = + function + CicNotationPt.ApplPattern l -> + CicNotationPt.ApplPattern (List.map disambiguate l) + | CicNotationPt.VarPattern id + when not + (List.exists + (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 + with Not_found -> + prerr_endline ("Domain item not found: " ^ + (DisambiguateTypes.string_of_domain_item item)); + assert false) + | p -> p + in + LexiconAst.Interpretation + (loc, dsc, (symbol, args), disambiguate cic_appl_pattern) + | _-> cmd + in !out cmd; let notation_ids' = CicNotation.process_notation cmd in let status = @@ -124,7 +153,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = DisambiguateChoices.lookup_num_by_dsc desc] in set_proof_aliases mode status diff - | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm -> + | LexiconAst.Interpretation (_, dsc, (symbol, _), _) as stm -> let status = add_lexicon_content [stm] status in let diff = [DisambiguateTypes.Symbol (symbol, 0),