matitaB/components/ng_disambiguation/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 module Ast = NotationPt
  29
  30 type db = {
  31   (* maps (loc,domain_item) to alias *)
  32   interpr: GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t;
  33   (* the universe of possible interpretations for all symbols/ids/nums *)
  34   multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
  35   (* new_aliases: ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list *)
  36 }
  37
  38 let get_interpr db =
  39   db.interpr
  40 ;;
  41
  42 let initial_status = {
  43   interpr = DisambiguateTypes.InterprEnv.empty;
  44   multi_aliases = DisambiguateTypes.Environment.empty;
  45   (* new_aliases = [] *)
  46 }
  47
  48 class type g_status =
  49   object
  50    inherit Interpretations.g_status
  51    method disambiguate_db: db
  52   end
  53
  54 class virtual status uid =
  55  object (self)
  56   inherit Interpretations.status uid
  57   inherit NCicLibrary.status uid
  58   val disambiguate_db = initial_status
  59   method disambiguate_db = disambiguate_db
  60   method set_disambiguate_db v = {< disambiguate_db = v >}
  61   method reset_disambiguate_db () =
  62     {< disambiguate_db = { self#disambiguate_db with interpr =
  63             DisambiguateTypes.InterprEnv.empty } >}
  64   method set_disambiguate_status
  65    : 'status. #g_status as 'status -> 'self
  66       = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
  67  end
  68
  69 (* let eval_with_new_aliases status f =
  70  let status =
  71   status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
  72  let res = f status in
  73  let new_aliases = status#disambiguate_db.new_aliases in
  74   new_aliases,res
  75 ;;*)
  76
  77 let dump_aliases out msg status =
  78    out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
  79    DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
  80     status#disambiguate_db.interpr
  81
  82 let add_to_interpr status new_aliases =
  83    let interpr =
  84     List.fold_left (fun acc (k,c) ->
  85       DisambiguateTypes.InterprEnv.add k c acc)
  86       status#disambiguate_db.interpr new_aliases
  87    in
  88    let new_status =
  89      {status#disambiguate_db with interpr = interpr }
  90    in
  91     status#set_disambiguate_db new_status
  92
  93 let add_to_disambiguation_univ status new_aliases =
  94    let multi_aliases =
  95     List.fold_left (fun acc (d,c) ->
  96       DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
  97          d c acc)
  98      status#disambiguate_db.multi_aliases new_aliases
  99    in
 100    let new_status =
 101      {status#disambiguate_db with multi_aliases = multi_aliases }
 102    in
 103     status#set_disambiguate_db new_status
 104
 105
 106 exception BaseUriNotSetYet
 107
 108 let singleton msg = function
 109   | [x], _ -> x
 110   | l, _   ->
 111       let debug =
 112          Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
 113          msg (List.length l)
 114       in
 115       prerr_endline debug; assert false
 116
 117 let __Implicit = "__Implicit__"
 118 let __Closed_Implicit = "__Closed_Implicit__"
 119
 120 let ncic_mk_choice status a =
 121   prerr_endline "ncic_mk_choice";
 122   match a with
 123   | GrafiteAst.Symbol_alias (name,_, dsc) ->
 124      prerr_endline ("caso 1: " ^ name ^ "; " ^ dsc);
 125      if name = __Implicit then
 126        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
 127      else if name = __Closed_Implicit then
 128        dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
 129      else
 130        (prerr_endline (Printf.sprintf "mk_choice: symbol %s, interpr %s"
 131          name dsc);
 132        DisambiguateChoices.lookup_symbol_by_dsc status
 133         ~mk_implicit:(function
 134            | true -> NCic.Implicit `Closed
 135            | false -> NCic.Implicit `Term)
 136         ~mk_appl:(function
 137            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
 138         ~term_of_nref:(fun nref -> NCic.Const nref)
 139        name dsc)
 140   | GrafiteAst.Number_alias (_,dsc) ->
 141      prerr_endline ("caso 2: " ^ dsc);
 142      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
 143       desc, `Num_interp
 144        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
 145   | GrafiteAst.Ident_alias (name, uri) ->
 146      prerr_endline ("caso 3: " ^ name);
 147      uri, `Sym_interp
 148       (fun l->assert(l = []);
 149         let nref = NReference.reference_of_string uri in
 150          NCic.Const nref)
 151 ;;
 152
 153
 154 let mk_implicit b =
 155   match b with
 156   | false ->
 157       GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
 158   | true ->
 159       GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
 160 ;;
 161
 162 let nlookup_in_library status
 163   interactive_user_uri_choice input_or_locate_uri item
 164 =
 165   match item with
 166   | DisambiguateTypes.Id id ->
 167      (try
 168        let references = NCicLibrary.resolve status id in
 169         List.map
 170          (fun u ->
 171            GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
 172          ) references
 173       with
 174        NCicEnvironment.ObjectNotFound _ -> [])
 175   | _ -> []
 176 ;;
 177
 178 (* XXX TO BE REMOVED: no need to fix instances any more *)
 179 (*let fix_instance item l =
 180  match item with
 181     DisambiguateTypes.Symbol (_,n) ->
 182      List.map
 183       (function
 184           GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
 185         | _ -> assert false
 186       ) l
 187   | DisambiguateTypes.Num n ->
 188      List.map
 189       (function
 190           GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
 191         | _ -> assert false
 192       ) l
 193   | DisambiguateTypes.Id _ -> l
 194 ;;*)
 195 let fix_instance _ l = l;;
 196
 197 let rec diff_term loc t u = match (t,u) with
 198   | Ast.AttributedTerm (`Loc l,t'), Ast.AttributedTerm (_,u') -> diff_term l t' u'
 199   | Ast.AttributedTerm (_,t'), Ast.AttributedTerm (_,u') -> diff_term loc t' u'
 200   | Ast.Appl tl, Ast.Appl ul ->
 201       List.fold_left2 (fun acc t0 u0 -> diff_term loc t0 u0@acc) [] tl ul
 202   | Ast.Binder (_,v1,b1), Ast.Binder (_,v2,b2) ->
 203      diff_var loc v1 v2@ diff_term loc b1 b2
 204   | Ast.Case (t1,ity1,outty1,pl1),Ast.Case (t2,ity2,outty2,pl2) ->
 205       let ity_interp = match ity1,ity2 with
 206       | Some (i,None), Some (_,Some r) ->
 207          let uri = NReference.string_of_reference r in
 208          [loc,GrafiteAst.Ident_alias (i,uri)]
 209       | _ -> []
 210       in
 211       let oty_interp = match outty1,outty2 with
 212       | Some o1, Some o2 -> diff_term loc o1 o2
 213       | _ -> []
 214       in
 215       (* pl = (case_pattern * term) list *)
 216       let auxpatt (c1,u1) (c2,u2) acc =
 217         let diff_cp = match c1,c2 with
 218         | Ast.Pattern (i,href1,vars1), Ast.Pattern (_,href2,vars2) ->
 219            let diff_i = match href1,href2 with
 220              | None, Some r ->
 221                 let uri = NReference.string_of_reference r in
 222                 [loc,GrafiteAst.Ident_alias (i,uri)]
 223              | _ -> []
 224            in
 225            let diff_vars =
 226              List.fold_right2 (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 []
 227            in
 228            diff_i @ diff_vars
 229         | _ -> []
 230         in
 231         diff_term loc u1 u2 @ diff_cp @ acc
 232       in
 233       let pl_interp = List.fold_right2 auxpatt pl1 pl2 [] in
 234       diff_term loc t1 t2 @ ity_interp @ oty_interp @ pl_interp
 235   | Ast.Cast (u1,v1),Ast.Cast (u2,v2) ->
 236      diff_term loc u1 u2@diff_term loc v1 v2
 237   | Ast.LetIn (var1,u1,v1),Ast.LetIn (var2,u2,v2) ->
 238      diff_var loc var1 var2 @ diff_term loc u1 u2 @ diff_term loc v1 v2
 239   | Ast.LetRec (_,fl1,w1),Ast.LetRec (_,fl2,w2) ->
 240     let diff_funs =
 241       List.fold_right2
 242         (fun (vars1,f1,b1,_) (vars2,f2,b2,_) acc ->
 243            let diff_vars =
 244              List.fold_right2
 245                (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 []
 246            in
 247            diff_vars @ diff_var loc f1 f2 @ diff_term loc b1 b2 @ acc)
 248         fl1 fl2 []
 249     in
 250     diff_funs @ diff_term loc w1 w2
 251   | Ast.Ident (n,`Ambiguous),Ast.Ident (_,`Uri u) ->
 252       [loc,GrafiteAst.Ident_alias (n,u)]
 253   | Ast.Symbol (s, None),Ast.Symbol(_,Some (uri,desc)) ->
 254       [loc,GrafiteAst.Symbol_alias (s,uri,desc)]
 255   | Ast.Num (_, None),Ast.Num (_,Some (uri,desc)) ->
 256       [loc,GrafiteAst.Number_alias (uri,desc)]
 257   | _ -> [] (* leaves *)
 258 and diff_var loc (_,v1) (_,v2) = match v1,v2 with
 259   | Some v1', Some v2' -> diff_term loc v1' v2'
 260   | _ -> []
 261 ;;
 262
 263 let diff_obj loc o1 o2 = match o1,o2 with
 264  | Ast.Inductive (ls1,itys1), Ast.Inductive (ls2,itys2) ->
 265      let diff_ls =
 266        List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
 267      in
 268      let diff_itys =
 269        List.fold_right2
 270          (fun (i1,_,ty1,cl1) (i2,_,ty2,cl2) acc0 ->
 271             let diff_cl =
 272               List.fold_right2
 273                (fun (_,u) (_,v) acc1 -> diff_term loc u v @ acc1)
 274                cl1 cl2 []
 275             in
 276             diff_term loc ty1 ty2 @ diff_cl @ acc0)
 277          itys1 itys2 []
 278      in
 279      diff_ls @ diff_itys
 280  | Ast.Theorem (_,i1,b1,ty1,_), Ast.Theorem (_,i2,b2,ty2,_) ->
 281      let diff_tys = match ty1,ty2 with
 282      | Some ty1', Some ty2' -> diff_term loc ty1' ty2'
 283      | _ -> []
 284      in
 285      diff_term loc b1 b2 @ diff_tys
 286  | Ast.Record (ls1,_,ty1,fl1),Ast.Record (ls2,_,ty2,fl2) ->
 287      let diff_ls =
 288        List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
 289      in
 290      let diff_fl =
 291        List.fold_right2
 292          (fun (_,f1,_,_) (_,f2,_,_) acc -> diff_term loc f1 f2 @ acc) fl1 fl2 []
 293      in
 294      diff_ls @ diff_term loc ty1 ty2 @ diff_fl
 295  | _ -> assert false
 296 ;;
 297
 298 let disambiguate_nterm status expty context metasenv subst thing
 299 =
 300   let newast, metasenv, subst, cic =
 301     singleton "first"
 302       (NCicDisambiguate.disambiguate_term
 303         status
 304         ~aliases:status#disambiguate_db.interpr
 305         ~expty
 306         ~universe:(status#disambiguate_db.multi_aliases)
 307         ~lookup_in_library:(nlookup_in_library status)
 308         ~mk_choice:(ncic_mk_choice status)
 309         ~mk_implicit ~fix_instance
 310         ~description_of_alias:GrafiteAst.description_of_alias
 311         ~context ~metasenv ~subst thing)
 312   in
 313   let _,_,thing' = thing in
 314   let diff = diff_term Stdpp.dummy_loc thing' newast in
 315   let status = add_to_interpr status diff
 316   in
 317    metasenv, subst, status, cic
 318 ;;
 319
 320
 321 type pattern =
 322   NotationPt.term Disambiguate.disambiguator_input option *
 323   (string * NCic.term) list * NCic.term option
 324
 325 let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
 326   let interp path = NCicDisambiguate.disambiguate_path status path in
 327   let goal_path = HExtlib.map_option interp goal_path in
 328   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
 329   let wanted = HExtlib.map_option (fun x -> text,prefix_len,x) wanted in
 330    (wanted, hyp_paths, goal_path)
 331 ;;
 332
 333 let disambiguate_reduction_kind text prefix_len = function
 334   | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
 335   | `Normalize
 336   | `Simpl
 337   | `Unfold None
 338   | `Whd as kind -> kind
 339 ;;
 340
 341 let disambiguate_auto_params
 342   disambiguate_term metasenv context (oterms, params)
 343 =
 344   match oterms with
 345     | None -> metasenv, (None, params)
 346     | Some terms ->
 347         let metasenv, terms =
 348           List.fold_right
 349             (fun t (metasenv, terms) ->
 350                let metasenv,t = disambiguate_term context metasenv t in
 351                  metasenv,t::terms) terms (metasenv, [])
 352         in
 353           metasenv, (Some terms, params)
 354 ;;
 355
 356 let disambiguate_just disambiguate_term context metasenv =
 357  function
 358     `Term t ->
 359       let metasenv,t = disambiguate_term context metasenv t in
 360        metasenv, `Term t
 361   | `Auto params ->
 362       let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
 363        context params
 364       in
 365        metasenv, `Auto params
 366 ;;
 367
 368 let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
 369   let uri =
 370    let baseuri =
 371      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
 372    in
 373    let name =
 374      match obj with
 375      | NotationPt.Inductive (_,(name,_,_,_)::_)
 376      | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
 377      | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
 378      | NotationPt.Inductive _ -> assert false
 379    in
 380      NUri.uri_of_string (baseuri ^ "/" ^ name)
 381   in
 382   let ast, _, _, cic =
 383    singleton "third"
 384     (NCicDisambiguate.disambiguate_obj
 385       status
 386       ~lookup_in_library:(nlookup_in_library status)
 387       ~description_of_alias:GrafiteAst.description_of_alias
 388       ~mk_choice:(ncic_mk_choice status)
 389       ~mk_implicit ~fix_instance ~uri
 390       ~aliases:status#disambiguate_db.interpr
 391       ~universe:(status#disambiguate_db.multi_aliases)
 392       (text,prefix_len,obj)) in
 393   let diff = diff_obj Stdpp.dummy_loc obj ast in
 394   let status = add_to_interpr status diff
 395   in
 396    status, cic
 397 ;;
 398
 399 let disambiguate_cic_appl_pattern status args =
 400  let rec disambiguate =
 401   function
 402     NotationPt.ApplPattern l ->
 403      NotationPt.ApplPattern (List.map disambiguate l)
 404   | NotationPt.VarPattern id
 405      when not
 406       (List.exists
 407        (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
 408      ->
 409       let item = DisambiguateTypes.Id id in
 410        begin
 411         try
 412          match
 413           DisambiguateTypes.Environment.find item
 414            (* status#disambiguate_db.aliases *)
 415            status#disambiguate_db.multi_aliases
 416          with
 417          (* XXX : we only try the first match *)
 418             GrafiteAst.Ident_alias (_,uri)::_ ->
 419              NotationPt.NRefPattern (NReference.reference_of_string uri)
 420           | _ -> assert false
 421         with Not_found ->
 422          prerr_endline
 423           ("LexiconEngine.eval_command: domain item not found: " ^
 424           (DisambiguateTypes.string_of_domain_item item));
 425          dump_aliases prerr_endline "" status;
 426          raise
 427           (Failure
 428            ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
 429              end
 430   | p -> p
 431  in
 432   disambiguate
 433 ;;
 434
 435 let aliases_for_objs status refs =
 436  List.concat
 437   (List.map
 438     (fun nref ->
 439       let references = NCicLibrary.aliases_of status nref in
 440        List.map
 441         (fun u ->
 442           let name = NCicPp.r2s status true u in
 443            (* FIXME : we are forgetting the interpretation of the Id
 444             * but is this useful anymore?!?!? *)
 445            DisambiguateTypes.Id name,
 446             GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
 447         ) references) refs)