helm/ocaml/cic_disambiguation/disambiguate.ml

   1 (* Copyright (C) 2004, HELM Team.
   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 open Printf
  27
  28 open DisambiguateTypes
  29 open UriManager
  30
  31 exception No_choices of domain_item
  32 exception NoWellTypedInterpretation
  33
  34   (** raised when an environment is not enough informative to decide *)
  35 exception Try_again
  36
  37 let debug = true
  38 let debug_print = if debug then prerr_endline else ignore
  39
  40 let descr_of_domain_item = function
  41  | Id s -> s
  42  | Symbol (s, _) -> s
  43  | Num i -> string_of_int i
  44
  45 type test_result =
  46   | Ok of Cic.term * Cic.metasenv
  47   | Ko
  48   | Uncertain
  49
  50 let refine metasenv context term =
  51   let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
  52   debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
  53   try
  54     let term', _, metasenv' = CicRefine.type_of_aux' metasenv context term in
  55     Ok (term', metasenv')
  56   with
  57     | CicRefine.Uncertain _ ->
  58         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
  59         Uncertain
  60     | _ ->
  61         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
  62         Ko
  63
  64 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
  65   snd (Environment.find item env) env num args
  66
  67   (* TODO move it to Cic *)
  68 let find_in_environment name context =
  69   let rec aux acc = function
  70     | [] -> raise Not_found
  71     | Cic.Name hd :: tl when hd = name -> acc
  72     | _ :: tl ->  aux (acc + 1) tl
  73   in
  74   aux 1 context
  75
  76 let interpretate ~context ~env ast =
  77   let rec aux loc context = function
  78     | CicAst.AttributedTerm (`Loc loc, term) ->
  79         aux loc context term
  80     | CicAst.AttributedTerm (_, term) -> aux loc context term
  81     | CicAst.Appl (CicAst.Symbol (symb, i) :: args) ->
  82         let cic_args = List.map (aux loc context) args in
  83         resolve env (Symbol (symb, i)) ~args:cic_args ()
  84     | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
  85     | CicAst.Binder (binder_kind, (var, typ), body) ->
  86         let cic_type = aux_option loc context typ in
  87         let cic_body = aux loc (var :: context) body in
  88         (match binder_kind with
  89         | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
  90         | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body)
  91         | `Exists ->
  92             resolve env (Symbol ("exists", 0))
  93               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
  94     | CicAst.Case (term, indty_ident, outtype, branches) ->
  95         let cic_term = aux loc context term in
  96         let cic_outtype = aux_option loc context outtype in
  97         let do_branch ((head, args), term) =
  98           let rec do_branch' context = function
  99             | [] -> aux loc context term
 100             | (name, typ) :: tl ->
 101                 let cic_body = do_branch' (name :: context) tl in
 102                 let typ =
 103                   match typ with
 104                   | None -> Cic.Implicit
 105                   | Some typ -> aux loc context typ
 106                 in
 107                 Cic.Lambda (name, typ, cic_body)
 108           in
 109           do_branch' context args
 110         in
 111         let (indtype_uri, indtype_no) =
 112           match resolve env (Id indty_ident) () with
 113           | Cic.MutInd (uri, tyno, _) -> uri, tyno
 114           | Cic.Implicit -> raise Try_again
 115           | _ -> raise DisambiguateChoices.Invalid_choice
 116         in
 117         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
 118           (List.map do_branch branches))
 119     | CicAst.LetIn ((name, typ), def, body) ->
 120         let cic_def = aux loc context def in
 121         let cic_def =
 122           match typ with
 123           | None -> cic_def
 124           | Some t -> Cic.Cast (cic_def, aux loc context t)
 125         in
 126         let cic_body = aux loc (name :: context) body in
 127         Cic.LetIn (name, cic_def, cic_body)
 128     | CicAst.LetRec (kind, defs, body) ->
 129         let context' =
 130           List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
 131             context defs
 132         in
 133         let cic_body = aux loc context' body in
 134         let inductiveFuns =
 135           List.map
 136             (fun ((name, typ), body, decr_idx) ->
 137               let cic_body = aux loc context' body in
 138               let cic_type = aux_option loc context typ in
 139               let name =
 140                 match name with
 141                 | Cic.Anonymous ->
 142                     CicTextualParser2.fail loc
 143                       "Recursive functions cannot be anonymous"
 144                 | Cic.Name name -> name
 145               in
 146               (name, decr_idx, cic_type, cic_body))
 147             defs
 148         in
 149         let counter = ref ~-1 in
 150         let build_term funs =
 151           (* this is the body of the fold_right function below. Rationale: Fix
 152            * and CoFix cases differs only in an additional index in the
 153            * inductiveFun list, see Cic.term *)
 154           match kind with
 155           | `Inductive ->
 156               (fun (var, _, _, _) cic ->
 157                 incr counter;
 158                 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
 159           | `CoInductive ->
 160               let funs =
 161                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
 162               in
 163               (fun (var, _, _, _) cic ->
 164                 incr counter;
 165                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
 166         in
 167         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
 168     | CicAst.Ident (name, subst) ->
 169         (* TODO hanlde explicit substitutions *)
 170         (try
 171           let index = find_in_environment name context in
 172           if subst <> [] then
 173             CicTextualParser2.fail loc
 174               "Explicit substitutions not allowed here";
 175           Cic.Rel index
 176         with Not_found -> resolve env (Id name) ())
 177     | CicAst.Implicit -> Cic.Implicit
 178     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
 179     | CicAst.Meta (index, subst) ->
 180         let cic_subst =
 181           List.map
 182             (function None -> None | Some term -> Some (aux loc context term))
 183             subst
 184         in
 185         Cic.Meta (index, cic_subst)
 186     | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
 187     | CicAst.Sort `Set -> Cic.Sort Cic.Set
 188     | CicAst.Sort `Type -> Cic.Sort Cic.Type
 189     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
 190     | CicAst.Symbol (symbol, instance) ->
 191         resolve env (Symbol (symbol, instance)) ()
 192   and aux_option loc context = function
 193     | None -> Cic.Implicit
 194     | Some term -> aux loc context term
 195   in
 196   match ast with
 197   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
 198   | _ -> assert false
 199
 200 let domain_of_term ~context ast =
 201     (* "aux" keeps domain in reverse order and doesn't care about duplicates.
 202      * Domain item more in deep in the list will be processed first.
 203      *)
 204   let rec aux loc context = function
 205     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
 206     | CicAst.AttributedTerm (_, term) -> aux loc context term
 207     | CicAst.Appl terms ->
 208         List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
 209     | CicAst.Binder (_, (var, typ), body) ->
 210         let type_dom = aux_option loc context typ in
 211         let body_dom = aux loc (var :: context) body in
 212         body_dom @ type_dom
 213     | CicAst.Case (term, indty_ident, outtype, branches) ->
 214         let term_dom = aux loc context term in
 215         let outtype_dom = aux_option loc context outtype in
 216         let do_branch ((head, args), term) =
 217           let (term_context, args_domain) =
 218             List.fold_left
 219               (fun (cont, dom) (name, typ) ->
 220                 (name :: cont,
 221                  (match typ with
 222                  | None -> dom
 223                  | Some typ -> aux loc cont typ @ dom)))
 224               (context, []) args
 225           in
 226           args_domain @ aux loc term_context term
 227         in
 228         let branches_dom =
 229           List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
 230         in
 231         branches_dom @ outtype_dom @ term_dom @ [ Id indty_ident ]
 232     | CicAst.LetIn ((var, typ), body, where) ->
 233         let body_dom = aux loc context body in
 234         let type_dom = aux_option loc context typ in
 235         let where_dom = aux loc (var :: context) where in
 236         where_dom @ type_dom @ body_dom
 237     | CicAst.LetRec (kind, defs, where) ->
 238         let context' =
 239           List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
 240             context defs
 241         in
 242         let where_dom = aux loc context' where in
 243         let defs_dom =
 244           List.fold_left
 245             (fun dom ((_, typ), body, _) ->
 246               aux loc context' body @ aux_option loc context typ)
 247             [] defs
 248         in
 249         where_dom @ defs_dom
 250     | CicAst.Ident (name, subst) ->
 251         (* TODO hanlde explicit substitutions *)
 252         (try
 253           let index = find_in_environment name context in
 254           if subst <> [] then
 255             CicTextualParser2.fail loc
 256               "Explicit substitutions not allowed here";
 257           []
 258         with Not_found -> [ Id name ])
 259     | CicAst.Implicit -> []
 260     | CicAst.Num (num, i) -> [ Num i ]
 261     | CicAst.Meta (index, local_context) ->
 262         List.fold_left (fun dom term -> aux_option loc context term @ dom) []
 263           local_context
 264     | CicAst.Sort _ -> []
 265     | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
 266
 267   and aux_option loc context = function
 268     | None -> []
 269     | Some t -> aux loc context t
 270   in
 271
 272     (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
 273   let rev_uniq =
 274     let module SortedItem =
 275       struct
 276         type t = DisambiguateTypes.domain_item
 277         let compare = Pervasives.compare
 278       end
 279     in
 280     let module Set = Set.Make (SortedItem) in
 281     fun l ->
 282       let rev_l = List.rev l in
 283       let (_, uniq_rev_l) =
 284         List.fold_left
 285           (fun (members, rev_l) elt ->
 286             if Set.mem elt members then
 287               (members, rev_l)
 288             else
 289               Set.add elt members, elt :: rev_l)
 290           (Set.empty, []) rev_l
 291       in
 292       List.rev uniq_rev_l
 293   in
 294
 295   match ast with
 296   | CicAst.AttributedTerm (`Loc loc, term) -> rev_uniq (aux loc context term)
 297   | _ -> assert false
 298
 299
 300   (* dom1 \ dom2 *)
 301 let domain_diff dom1 dom2 =
 302 (* let domain_diff = Domain.diff *)
 303   let is_in_dom2 =
 304     List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
 305       (fun _ -> false) dom2
 306   in
 307   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
 308
 309 module Make (C: Callbacks) =
 310   struct
 311     let choices_of_id mqi_handle id =
 312      let query  =  MQueryGenerator.locate id in
 313      let result = MQueryInterpreter.execute mqi_handle query in
 314      let uris =
 315       List.map
 316        (function uri,_ ->
 317          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
 318        ) result in
 319       C.output_html (`Msg (`T "Locate query:"));
 320       MQueryUtil.text_of_query
 321        (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
 322        "" query;
 323       C.output_html (`Msg (`T "Result:"));
 324       MQueryUtil.text_of_result
 325         (fun s -> C.output_html (`Msg (`T s))) "" result;
 326       let uris' =
 327        match uris with
 328         | [] ->
 329            [UriManager.string_of_uri (C.input_or_locate_uri
 330             ~title:("URI matching \"" ^ id ^ "\" unknown."))]
 331         | [uri] -> [uri]
 332         | _ ->
 333             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
 334              ~ok:"Try selected." ~enable_button_for_non_vars:true
 335              ~title:"Ambiguous input." ~id
 336              ~msg: ("Ambiguous input \"" ^ id ^
 337                 "\". Please, choose one or more interpretations:")
 338              uris
 339       in
 340       List.map
 341         (fun uri ->
 342           (uri,
 343            let term =
 344              try
 345                HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
 346              with _ -> assert false
 347             in
 348            fun _ _ _ -> term))
 349         uris'
 350
 351     let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
 352     =
 353       debug_print "NEW DISAMBIGUATE INPUT";
 354       let disambiguate_context =  (* cic context -> disambiguate context *)
 355         List.map
 356           (function None -> Cic.Anonymous | Some (name, _) -> name)
 357           context
 358       in
 359       let term_dom = domain_of_term ~context:disambiguate_context term in
 360       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
 361         (string_of_domain term_dom));
 362       let current_dom =
 363         Environment.fold (fun item _ dom -> item :: dom) current_env []
 364       in
 365       let todo_dom = domain_diff term_dom current_dom in
 366       (* (2) lookup function for any item (Id/Symbol/Num) *)
 367       let lookup_choices =
 368         let id_choices = Hashtbl.create 1023 in
 369         fun item ->
 370         let choices =
 371           match item with
 372           | Id id ->
 373               (try
 374                 Hashtbl.find id_choices id
 375               with Not_found ->
 376                 let choices = choices_of_id mqi_handle id in
 377                 Hashtbl.add id_choices id choices;
 378                 choices)
 379           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
 380           | Num instance -> DisambiguateChoices.lookup_num_choices ()
 381         in
 382         if choices = [] then raise (No_choices item);
 383         choices
 384       in
 385       (* (3) test an interpretation filling with meta uninterpreted identifiers
 386        *)
 387       let test_env current_env todo_dom =
 388         let filled_env =
 389           List.fold_left
 390             (fun env item ->
 391               Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
 392             current_env todo_dom
 393         in
 394         try
 395           let cic_term =
 396             interpretate ~context:disambiguate_context ~env:filled_env term
 397           in
 398           refine metasenv context cic_term
 399         with
 400         | Try_again -> Uncertain
 401         | DisambiguateChoices.Invalid_choice -> Ko
 402       in
 403       (* (4) build all possible interpretations *)
 404       let rec aux current_env todo_dom =
 405         match todo_dom with
 406         | [] ->
 407             (match test_env current_env [] with
 408             | Ok (term, metasenv) -> [ current_env, term, metasenv ]
 409             | Ko | Uncertain -> [])
 410         | item :: remaining_dom ->
 411             debug_print (sprintf "CHOOSED ITEM: %s"
 412               (string_of_domain_item item));
 413             let choices = lookup_choices item in
 414             let rec filter = function
 415               | [] -> []
 416               | codomain_item :: tl ->
 417                   debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
 418                   let new_env =
 419                     Environment.add item codomain_item current_env
 420                   in
 421                   (match test_env new_env remaining_dom with
 422                   | Ok (term, metasenv) ->
 423                       (match remaining_dom with
 424                       | [] -> [ new_env, term, metasenv ]
 425                       | _ -> aux new_env remaining_dom) @ filter tl
 426                   | Uncertain ->
 427                       (match remaining_dom with
 428                       | [] -> []
 429                       | _ -> aux new_env remaining_dom) @ filter tl
 430                   | Ko -> filter tl)
 431             in
 432             filter choices
 433       in
 434       let (choosed_env, choosed_term, choosed_metasenv) =
 435         match aux current_env todo_dom with
 436         | [] -> raise NoWellTypedInterpretation
 437         | [ x ] ->
 438             debug_print "UNA SOLA SCELTA";
 439             x
 440         | l ->
 441             debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
 442             let choices =
 443               List.map
 444                 (fun (env, _, _) ->
 445                   List.map
 446                     (fun domain_item ->
 447                       let description =
 448                         fst (Environment.find domain_item env)
 449                       in
 450                       (descr_of_domain_item domain_item, description))
 451                     term_dom)
 452                 l
 453             in
 454             let choosed = C.interactive_interpretation_choice choices in
 455             List.nth l choosed
 456       in
 457       (choosed_env, choosed_metasenv, choosed_term)
 458
 459   end
 460