matita/components/lexicon/grafiteDisambiguate.ml

   1 (*
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 type db = {
  29   aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
  30   multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
  31   new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
  32 }
  33
  34 let initial_status = {
  35   aliases = DisambiguateTypes.Environment.empty;
  36   multi_aliases = DisambiguateTypes.Environment.empty;
  37   new_aliases = []
  38 }
  39
  40 class type g_status =
  41   object
  42    inherit Interpretations.g_status
  43    method disambiguate_db: db
  44   end
  45
  46 class status =
  47  object (self)
  48   inherit Interpretations.status
  49   val disambiguate_db = initial_status
  50   method disambiguate_db = disambiguate_db
  51   method set_disambiguate_db v = {< disambiguate_db = v >}
  52   method set_disambiguate_status
  53    : 'status. #g_status as 'status -> 'self
  54       = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
  55  end
  56
  57 let dump_aliases out msg status =
  58    out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
  59    DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
  60     status#disambiguate_db.aliases
  61
  62 let set_proof_aliases status ~implicit_aliases mode new_aliases =
  63  if mode = GrafiteAst.WithoutPreferences then
  64    status
  65  else
  66    (* MATITA 1.0
  67    let new_commands =
  68      List.map
  69       (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases
  70    in *)
  71    let aliases =
  72     List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
  73      status#disambiguate_db.aliases new_aliases in
  74    let multi_aliases =
  75     List.fold_left (fun acc (d,c) ->
  76       DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
  77          d c acc)
  78      status#disambiguate_db.multi_aliases new_aliases
  79    in
  80    let new_status =
  81     {multi_aliases = multi_aliases ;
  82      aliases = aliases;
  83      new_aliases =
  84       (if implicit_aliases then new_aliases else []) @
  85         status#disambiguate_db.new_aliases}
  86    in
  87     status#set_disambiguate_db new_status
  88
  89 exception BaseUriNotSetYet
  90
  91 let singleton msg = function
  92   | [x], _ -> x
  93   | l, _   ->
  94       let debug =
  95          Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
  96          msg (List.length l)
  97       in
  98       prerr_endline debug; assert false
  99
 100 let __Implicit = "__Implicit__"
 101 let __Closed_Implicit = "__Closed_Implicit__"
 102
 103 let ncic_mk_choice status = function
 104   | GrafiteAst.Symbol_alias (name, _, dsc) ->
 105      if name = __Implicit then
 106        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
 107      else if name = __Closed_Implicit then
 108        dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
 109      else
 110        DisambiguateChoices.lookup_symbol_by_dsc status
 111         ~mk_implicit:(function
 112            | true -> NCic.Implicit `Closed
 113            | false -> NCic.Implicit `Term)
 114         ~mk_appl:(function
 115            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
 116         ~term_of_nref:(fun nref -> NCic.Const nref)
 117        name dsc
 118   | GrafiteAst.Number_alias (_, dsc) ->
 119      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
 120       desc, `Num_interp
 121        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
 122   | GrafiteAst.Ident_alias (name, uri) ->
 123      uri, `Sym_interp
 124       (fun l->assert(l = []);
 125         let nref = NReference.reference_of_string uri in
 126          NCic.Const nref)
 127 ;;
 128
 129
 130 let mk_implicit b =
 131   match b with
 132   | false ->
 133       GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
 134   | true ->
 135       GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
 136 ;;
 137
 138 let nlookup_in_library
 139   interactive_user_uri_choice input_or_locate_uri item
 140 =
 141   match item with
 142   | DisambiguateTypes.Id id ->
 143      (try
 144        let references = NCicLibrary.resolve id in
 145         List.map
 146          (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
 147          ) references
 148       with
 149        NCicEnvironment.ObjectNotFound _ -> [])
 150   | _ -> []
 151 ;;
 152
 153 let fix_instance item l =
 154  match item with
 155     DisambiguateTypes.Symbol (_,n) ->
 156      List.map
 157       (function
 158           GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
 159         | _ -> assert false
 160       ) l
 161   | DisambiguateTypes.Num n ->
 162      List.map
 163       (function
 164           GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
 165         | _ -> assert false
 166       ) l
 167   | DisambiguateTypes.Id _ -> l
 168 ;;
 169
 170
 171 let disambiguate_nterm estatus expty context metasenv subst thing
 172 =
 173   let diff, metasenv, subst, cic =
 174     singleton "first"
 175       (NCicDisambiguate.disambiguate_term
 176         ~rdb:estatus
 177         ~aliases:estatus#disambiguate_db.aliases
 178         ~expty
 179         ~universe:(Some estatus#disambiguate_db.multi_aliases)
 180         ~lookup_in_library:nlookup_in_library
 181         ~mk_choice:(ncic_mk_choice estatus)
 182         ~mk_implicit ~fix_instance
 183         ~description_of_alias:GrafiteAst.description_of_alias
 184         ~context ~metasenv ~subst thing)
 185   in
 186   let estatus =
 187    set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
 188     diff
 189   in
 190    metasenv, subst, estatus, cic
 191 ;;
 192
 193
 194 type pattern =
 195   NotationPt.term Disambiguate.disambiguator_input option *
 196   (string * NCic.term) list * NCic.term option
 197
 198 let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
 199   let interp path = NCicDisambiguate.disambiguate_path path in
 200   let goal_path = HExtlib.map_option interp goal_path in
 201   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
 202   let wanted =
 203     match wanted with None -> None | Some x -> Some (text,prefix_len,x)
 204   in
 205    (wanted, hyp_paths, goal_path)
 206 ;;
 207
 208 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
 209   | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
 210   | `Normalize
 211   | `Simpl
 212   | `Unfold None
 213   | `Whd as kind -> kind
 214 ;;
 215
 216 let disambiguate_auto_params
 217   disambiguate_term metasenv context (oterms, params)
 218 =
 219   match oterms with
 220     | None -> metasenv, (None, params)
 221     | Some terms ->
 222         let metasenv, terms =
 223           List.fold_right
 224             (fun t (metasenv, terms) ->
 225                let metasenv,t = disambiguate_term context metasenv t in
 226                  metasenv,t::terms) terms (metasenv, [])
 227         in
 228           metasenv, (Some terms, params)
 229 ;;
 230
 231 let disambiguate_just disambiguate_term context metasenv =
 232  function
 233     `Term t ->
 234       let metasenv,t = disambiguate_term context metasenv t in
 235        metasenv, `Term t
 236   | `Auto params ->
 237       let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
 238        context params
 239       in
 240        metasenv, `Auto params
 241 ;;
 242
 243 let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
 244   let uri =
 245    let baseuri =
 246      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
 247    in
 248    let name =
 249      match obj with
 250      | NotationPt.Inductive (_,(name,_,_,_)::_)
 251      | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
 252      | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
 253      | NotationPt.Inductive _ -> assert false
 254    in
 255      NUri.uri_of_string (baseuri ^ "/" ^ name)
 256   in
 257   let diff, _, _, cic =
 258    singleton "third"
 259     (NCicDisambiguate.disambiguate_obj
 260       ~lookup_in_library:nlookup_in_library
 261       ~description_of_alias:GrafiteAst.description_of_alias
 262       ~mk_choice:(ncic_mk_choice estatus)
 263       ~mk_implicit ~fix_instance
 264       ~uri
 265       ~rdb:estatus
 266       ~aliases:estatus#disambiguate_db.aliases
 267       ~universe:(Some estatus#disambiguate_db.multi_aliases)
 268       (text,prefix_len,obj)) in
 269   let estatus =
 270    set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
 271     diff
 272   in
 273    estatus, cic
 274 ;;