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