matita/components/grafite_parser/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 class type g_status =
  29   object
  30    inherit LexiconTypes.g_status
  31    inherit NCicCoercion.g_status
  32   end
  33
  34 class status =
  35  object (self)
  36   inherit LexiconTypes.status
  37   inherit NCicCoercion.status
  38   method set_grafite_disambiguate_status
  39    : 'status. #g_status as 'status -> 'self
  40       = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o
  41  end
  42
  43 exception BaseUriNotSetYet
  44
  45 let singleton msg = function
  46   | [x], _ -> x
  47   | l, _   ->
  48       let debug =
  49          Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
  50          msg (List.length l)
  51       in
  52       prerr_endline debug; assert false
  53
  54 let __Implicit = "__Implicit__"
  55 let __Closed_Implicit = "__Closed_Implicit__"
  56
  57 let ncic_mk_choice status = function
  58   | GrafiteAst.Symbol_alias (name, _, dsc) ->
  59      if name = __Implicit then
  60        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
  61      else if name = __Closed_Implicit then
  62        dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
  63      else
  64        DisambiguateChoices.lookup_symbol_by_dsc status
  65         ~mk_implicit:(function
  66            | true -> NCic.Implicit `Closed
  67            | false -> NCic.Implicit `Term)
  68         ~mk_appl:(function
  69            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
  70         ~term_of_nref:(fun nref -> NCic.Const nref)
  71        name dsc
  72   | GrafiteAst.Number_alias (_, dsc) ->
  73      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
  74       desc, `Num_interp
  75        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
  76   | GrafiteAst.Ident_alias (name, uri) ->
  77      uri, `Sym_interp
  78       (fun l->assert(l = []);
  79         let nref = NReference.reference_of_string uri in
  80          NCic.Const nref)
  81 ;;
  82
  83
  84 let mk_implicit b =
  85   match b with
  86   | false ->
  87       GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
  88   | true ->
  89       GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
  90 ;;
  91
  92 let nlookup_in_library
  93   interactive_user_uri_choice input_or_locate_uri item
  94 =
  95   match item with
  96   | DisambiguateTypes.Id id ->
  97      (try
  98        let references = NCicLibrary.resolve id in
  99         List.map
 100          (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
 101          ) references
 102       with
 103        NCicEnvironment.ObjectNotFound _ -> [])
 104   | _ -> []
 105 ;;
 106
 107 let fix_instance item l =
 108  match item with
 109     DisambiguateTypes.Symbol (_,n) ->
 110      List.map
 111       (function
 112           GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
 113         | _ -> assert false
 114       ) l
 115   | DisambiguateTypes.Num n ->
 116      List.map
 117       (function
 118           GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
 119         | _ -> assert false
 120       ) l
 121   | DisambiguateTypes.Id _ -> l
 122 ;;
 123
 124
 125 let disambiguate_nterm expty estatus context metasenv subst thing
 126 =
 127   let diff, metasenv, subst, cic =
 128     singleton "first"
 129       (NCicDisambiguate.disambiguate_term
 130         ~rdb:estatus
 131         ~aliases:estatus#lstatus.LexiconTypes.aliases
 132         ~expty
 133         ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
 134         ~lookup_in_library:nlookup_in_library
 135         ~mk_choice:(ncic_mk_choice estatus)
 136         ~mk_implicit ~fix_instance
 137         ~description_of_alias:GrafiteAst.description_of_alias
 138         ~context ~metasenv ~subst thing)
 139   in
 140   let estatus =
 141     LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
 142      GrafiteAst.WithPreferences diff
 143   in
 144    metasenv, subst, estatus, cic
 145 ;;
 146
 147
 148 type pattern =
 149   NotationPt.term Disambiguate.disambiguator_input option *
 150   (string * NCic.term) list * NCic.term option
 151
 152 let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
 153   let interp path = NCicDisambiguate.disambiguate_path path in
 154   let goal_path = HExtlib.map_option interp goal_path in
 155   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
 156   let wanted =
 157     match wanted with None -> None | Some x -> Some (text,prefix_len,x)
 158   in
 159    (wanted, hyp_paths, goal_path)
 160 ;;
 161
 162 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
 163   | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
 164   | `Normalize
 165   | `Simpl
 166   | `Unfold None
 167   | `Whd as kind -> kind
 168 ;;
 169
 170 let disambiguate_auto_params
 171   disambiguate_term metasenv context (oterms, params)
 172 =
 173   match oterms with
 174     | None -> metasenv, (None, params)
 175     | Some terms ->
 176         let metasenv, terms =
 177           List.fold_right
 178             (fun t (metasenv, terms) ->
 179                let metasenv,t = disambiguate_term context metasenv t in
 180                  metasenv,t::terms) terms (metasenv, [])
 181         in
 182           metasenv, (Some terms, params)
 183 ;;
 184
 185 let disambiguate_just disambiguate_term context metasenv =
 186  function
 187     `Term t ->
 188       let metasenv,t = disambiguate_term context metasenv t in
 189        metasenv, `Term t
 190   | `Auto params ->
 191       let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
 192        context params
 193       in
 194        metasenv, `Auto params
 195 ;;
 196
 197 let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
 198   let uri =
 199    let baseuri =
 200      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
 201    in
 202    let name =
 203      match obj with
 204      | NotationPt.Inductive (_,(name,_,_,_)::_)
 205      | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
 206      | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
 207      | NotationPt.Inductive _ -> assert false
 208    in
 209      NUri.uri_of_string (baseuri ^ "/" ^ name)
 210   in
 211   let diff, _, _, cic =
 212    singleton "third"
 213     (NCicDisambiguate.disambiguate_obj
 214       ~lookup_in_library:nlookup_in_library
 215       ~description_of_alias:GrafiteAst.description_of_alias
 216       ~mk_choice:(ncic_mk_choice estatus)
 217       ~mk_implicit ~fix_instance
 218       ~uri
 219       ~rdb:estatus
 220       ~aliases:estatus#lstatus.LexiconTypes.aliases
 221       ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
 222       (text,prefix_len,obj)) in
 223   let estatus =
 224    LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
 225     GrafiteAst.WithPreferences diff
 226   in
 227    estatus, cic
 228 ;;