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