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