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