matita/components/ng_disambiguation/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 virtual 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 eval_with_new_aliases status f =
  58  let status =
  59   status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
  60  let new_status = f status in
  61  let new_aliases = new_status#disambiguate_db.new_aliases in
  62   new_aliases,new_status
  63 ;;
  64
  65 let dump_aliases out msg status =
  66    out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
  67    DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
  68     status#disambiguate_db.aliases
  69
  70 let set_proof_aliases status ~implicit_aliases mode new_aliases =
  71  if mode = GrafiteAst.WithoutPreferences then
  72    status
  73  else
  74    let aliases =
  75     List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
  76      status#disambiguate_db.aliases new_aliases in
  77    let multi_aliases =
  78     List.fold_left (fun acc (d,c) ->
  79       DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
  80          d c acc)
  81      status#disambiguate_db.multi_aliases new_aliases
  82    in
  83    let new_status =
  84     {multi_aliases = multi_aliases ;
  85      aliases = aliases;
  86      new_aliases =
  87       (if implicit_aliases then new_aliases else []) @
  88         status#disambiguate_db.new_aliases}
  89    in
  90     status#set_disambiguate_db new_status
  91
  92 exception BaseUriNotSetYet
  93
  94 let singleton msg = function
  95   | [x], _ -> x
  96   | l, _   ->
  97       let debug =
  98          Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
  99          msg (List.length l)
 100       in
 101       prerr_endline debug; assert false
 102
 103 let __Implicit = "__Implicit__"
 104 let __Closed_Implicit = "__Closed_Implicit__"
 105
 106 let ncic_mk_choice status = function
 107   | GrafiteAst.Symbol_alias (name, _, dsc) ->
 108      if name = __Implicit then
 109        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
 110      else if name = __Closed_Implicit then
 111        dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
 112      else
 113        DisambiguateChoices.lookup_symbol_by_dsc status
 114         ~mk_implicit:(function
 115            | true -> NCic.Implicit `Closed
 116            | false -> NCic.Implicit `Term)
 117         ~mk_appl:(function
 118            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
 119         ~term_of_nref:(fun nref -> NCic.Const nref)
 120        name dsc
 121   | GrafiteAst.Number_alias (_, dsc) ->
 122      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
 123       desc, `Num_interp
 124        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
 125   | GrafiteAst.Ident_alias (_name, uri) ->
 126      uri, `Sym_interp
 127       (fun l->assert(l = []);
 128         let nref = NReference.reference_of_string uri in
 129          NCic.Const nref)
 130 ;;
 131
 132
 133 let mk_implicit b =
 134   match b with
 135   | false ->
 136       GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
 137   | true ->
 138       GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
 139 ;;
 140
 141 let nlookup_in_library
 142   _interactive_user_uri_choice _input_or_locate_uri item
 143 =
 144   match item with
 145   | DisambiguateTypes.Id id ->
 146      (try
 147        let references = NCicLibrary.resolve id in
 148         List.map
 149          (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
 150          ) references
 151       with
 152        NCicEnvironment.ObjectNotFound _ -> [])
 153   | _ -> []
 154 ;;
 155
 156 let fix_instance item l =
 157  match item with
 158     DisambiguateTypes.Symbol (_,n) ->
 159      List.map
 160       (function
 161           GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
 162         | _ -> assert false
 163       ) l
 164   | DisambiguateTypes.Num n ->
 165      List.map
 166       (function
 167           GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
 168         | _ -> assert false
 169       ) l
 170   | DisambiguateTypes.Id _ -> l
 171 ;;
 172
 173
 174 let disambiguate_nterm status expty context metasenv subst thing
 175 =
 176   let diff, metasenv, subst, cic =
 177     singleton "first"
 178       (NCicDisambiguate.disambiguate_term
 179         status
 180         ~aliases:status#disambiguate_db.aliases
 181         ~expty
 182         ~universe:(Some status#disambiguate_db.multi_aliases)
 183         ~lookup_in_library:nlookup_in_library
 184         ~mk_choice:(ncic_mk_choice status)
 185         ~mk_implicit ~fix_instance
 186         ~description_of_alias:GrafiteAst.description_of_alias
 187         ~context ~metasenv ~subst thing)
 188   in
 189   let status =
 190    set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
 191     diff
 192   in
 193    metasenv, subst, status, cic
 194 ;;
 195
 196
 197 type pattern =
 198   NotationPt.term Disambiguate.disambiguator_input option *
 199   (string * NCic.term) list * NCic.term option
 200
 201 let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
 202   let interp path = NCicDisambiguate.disambiguate_path status path in
 203   let goal_path = HExtlib.map_option interp goal_path in
 204   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
 205   let wanted = HExtlib.map_option (fun x -> text,prefix_len,x) wanted in
 206    (wanted, hyp_paths, goal_path)
 207 ;;
 208
 209 let disambiguate_reduction_kind _text _prefix_len = function
 210   | `Unfold (Some _t) -> assert false (* MATITA 1.0 *)
 211   | `Normalize
 212   | `Simpl
 213   | `Unfold None
 214   | `Whd as kind -> kind
 215 ;;
 216
 217 let disambiguate_auto_params
 218   disambiguate_term metasenv context (oterms, params)
 219 =
 220   match oterms with
 221     | None -> metasenv, (None, params)
 222     | Some terms ->
 223         let metasenv, terms =
 224           List.fold_right
 225             (fun t (metasenv, terms) ->
 226                let metasenv,t = disambiguate_term context metasenv t in
 227                  metasenv,t::terms) terms (metasenv, [])
 228         in
 229           metasenv, (Some terms, params)
 230 ;;
 231
 232 let disambiguate_just disambiguate_term context metasenv =
 233  function
 234     `Term t ->
 235       let metasenv,t = disambiguate_term context metasenv t in
 236        metasenv, `Term t
 237   | `Auto params ->
 238       let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
 239        context params
 240       in
 241        metasenv, `Auto params
 242 ;;
 243
 244 let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
 245   let uri =
 246    let baseuri =
 247      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
 248    in
 249    let name =
 250      match obj with
 251      | NotationPt.Inductive (_,(name,_,_,_)::_,_)
 252      | NotationPt.Record (_,name,_,_,_) -> name ^ ".ind"
 253      | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
 254      | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con"
 255      | NotationPt.LetRec _
 256      | NotationPt.Inductive _ -> assert false
 257    in
 258      NUri.uri_of_string (baseuri ^ "/" ^ name)
 259   in
 260   let diff, _, _, cic =
 261    singleton "third"
 262     (NCicDisambiguate.disambiguate_obj
 263       status
 264       ~lookup_in_library:nlookup_in_library
 265       ~description_of_alias:GrafiteAst.description_of_alias
 266       ~mk_choice:(ncic_mk_choice status)
 267       ~mk_implicit ~fix_instance ~uri
 268       ~aliases:status#disambiguate_db.aliases
 269       ~universe:(Some status#disambiguate_db.multi_aliases)
 270       (text,prefix_len,obj)) in
 271   let status =
 272    set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
 273     diff
 274   in
 275    status, cic
 276 ;;
 277
 278 let disambiguate_cic_appl_pattern status args =
 279  let rec disambiguate =
 280   function
 281     NotationPt.ApplPattern l ->
 282      NotationPt.ApplPattern (List.map disambiguate l)
 283   | NotationPt.VarPattern id
 284      when not
 285       (List.exists
 286        (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
 287      ->
 288       let item = DisambiguateTypes.Id id in
 289        begin
 290         try
 291          match
 292           DisambiguateTypes.Environment.find item
 293            status#disambiguate_db.aliases
 294          with
 295             GrafiteAst.Ident_alias (_, uri) ->
 296              NotationPt.NRefPattern (NReference.reference_of_string uri)
 297           | _ -> assert false
 298         with Not_found ->
 299          prerr_endline
 300           ("LexiconEngine.eval_command: domain item not found: " ^
 301           (DisambiguateTypes.string_of_domain_item item));
 302          dump_aliases prerr_endline "" status;
 303          raise
 304           (Failure
 305            ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
 306              end
 307   | p -> p
 308  in
 309   disambiguate
 310 ;;
 311
 312 let aliases_for_objs status refs =
 313  List.concat
 314   (List.map
 315     (fun nref ->
 316       let references = NCicLibrary.aliases_of nref in
 317        List.map
 318         (fun u ->
 319           let name = NCicPp.r2s status true u in
 320            DisambiguateTypes.Id name,
 321             GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
 322         ) references) refs)