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