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.MutCaseFixAndCofixRefineNotImplemented ->
  58         (* TODO remove this case as soon as refine is fully implemented *)
  59         (try
  60           debug_print (Printf.sprintf "TYPE CHECKER %s" (CicPp.ppterm term));
  61           let term' = CicTypeChecker.type_of_aux' metasenv context term in
  62           Ok (term',metasenv)
  63 (*         with _ -> Ko) *)
  64         with _ -> Uncertain)
  65     | CicRefine.Uncertain _ ->
  66         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
  67         Uncertain
  68     | _ ->
  69         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
  70         Ko
  71
  72 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
  73   snd (Environment.find item env) env num args
  74
  75   (* TODO move it to Cic *)
  76 let find_in_environment name context =
  77   let rec aux acc = function
  78     | [] -> raise Not_found
  79     | Cic.Name hd :: tl when hd = name -> acc
  80     | _ :: tl ->  aux (acc + 1) tl
  81   in
  82   aux 1 context
  83
  84 let interpretate ~context ~env ast =
  85   let rec aux loc context = function
  86     | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
  87     | CicTextualParser2Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
  88     | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
  89         let cic_args = List.map (aux loc context) args in
  90         resolve env (Symbol (symb, i)) ~args:cic_args ()
  91     | CicTextualParser2Ast.Binder (binder_kind, var, typ, body) ->
  92         let cic_type = aux_option loc context typ in
  93         let cic_body = aux loc (var :: context) body in
  94         (match binder_kind with
  95         | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
  96         | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body)
  97         | `Exists ->
  98             resolve env (Symbol ("exists", 0))
  99               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
 100     | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
 101         let cic_term = aux loc context term in
 102         let cic_outtype = aux_option loc context outtype in
 103         let do_branch (pat, term) =
 104           let rec do_branch' context = function
 105             | [] -> aux loc context term
 106             | hd :: tl ->
 107                 let cic_body = do_branch' (Cic.Name hd :: context) tl in
 108                 Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body)
 109           in
 110           match pat with
 111           | _ :: tl -> (* ignoring constructor *) do_branch' context tl
 112           | [] -> assert false
 113         in
 114         let (indtype_uri, indtype_no) =
 115           match resolve env (Id indty_ident) () with
 116           | Cic.MutInd (uri, tyno, _) -> uri, tyno
 117           | Cic.Implicit -> raise Try_again
 118           | _ -> raise DisambiguateChoices.Invalid_choice
 119         in
 120         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
 121           (List.map do_branch branches))
 122     | CicTextualParser2Ast.LetIn (var, def, body) ->
 123         let cic_def = aux loc context def in
 124         let name = Cic.Name var in
 125         let cic_body = aux loc (name :: context) body in
 126         Cic.LetIn (name, cic_def, cic_body)
 127     | CicTextualParser2Ast.LetRec (kind, defs, body) ->
 128         let context' =
 129           List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
 130             context defs
 131         in
 132         let cic_body = aux loc context' body in
 133         let inductiveFuns =
 134           List.map
 135             (fun (var, body, typ, decr_idx) ->
 136               let cic_body = aux loc context' body in
 137               let cic_type = aux_option loc context typ in
 138               (var, decr_idx, cic_type, cic_body))
 139             defs
 140         in
 141         let counter = ref 0 in
 142         let build_term funs =
 143           (* this is the body of the fold_right function below. Rationale: Fix
 144            * and CoFix cases differs only in an additional index in the
 145            * indcutiveFun list, see Cic.term *)
 146           match kind with
 147           | `Inductive ->
 148               (fun (var, _, _, _) cic ->
 149                 incr counter;
 150                 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
 151           | `CoInductive ->
 152               let funs =
 153                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
 154               in
 155               (fun (var, _, _, _) cic ->
 156                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
 157         in
 158         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
 159     | CicTextualParser2Ast.Ident (name, subst) ->
 160         (* TODO hanlde explicit substitutions *)
 161         (try
 162           let index = find_in_environment name context in
 163           if subst <> [] then
 164             CicTextualParser2.fail loc "Explicit substitutions not allowed here";
 165           Cic.Rel index
 166         with Not_found -> resolve env (Id name) ())
 167     | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num ()
 168     | CicTextualParser2Ast.Meta (index, subst) ->
 169         let cic_subst =
 170           List.map
 171             (function None -> None | Some term -> Some (aux loc context term))
 172             subst
 173         in
 174         Cic.Meta (index, cic_subst)
 175     | CicTextualParser2Ast.Sort `Prop -> Cic.Sort Cic.Prop
 176     | CicTextualParser2Ast.Sort `Set -> Cic.Sort Cic.Set
 177     | CicTextualParser2Ast.Sort `Type -> Cic.Sort Cic.Type
 178     | CicTextualParser2Ast.Sort `CProp -> Cic.Sort Cic.CProp
 179   and aux_option loc context = function
 180     | None -> Cic.Implicit
 181     | Some term -> aux loc context term
 182   in
 183   match ast with
 184   | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
 185   | _ -> assert false
 186
 187 let domain_of_term ~context ast =
 188   let rec aux loc context = function
 189     | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
 190     | CicTextualParser2Ast.Appl terms ->
 191         List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
 192           Domain.empty terms
 193     | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
 194         List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
 195           (Domain.singleton (Symbol (symb, i))) args
 196     | CicTextualParser2Ast.Binder (_, var, typ, body) ->
 197         let type_dom = aux_option loc context typ in
 198         let body_dom = aux loc (var :: context) body in
 199         Domain.union type_dom body_dom
 200     | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
 201         let term_dom = aux loc context term in
 202         let outtype_dom = aux_option loc context outtype in
 203         let do_branch (pat, term) =
 204           match pat with
 205           | _ :: tl ->
 206               aux loc
 207                 (List.fold_left (fun acc var -> (Cic.Name var) :: acc)
 208                   context tl)
 209                 term
 210           | [] -> assert false
 211         in
 212         let branches_dom =
 213           List.fold_left (fun dom branch -> Domain.union dom (do_branch branch))
 214             Domain.empty branches
 215         in
 216         Domain.add (Id indty_ident)
 217           (Domain.union outtype_dom (Domain.union term_dom branches_dom))
 218     | CicTextualParser2Ast.LetIn (var, body, where) ->
 219         let body_dom = aux loc context body in
 220         let where_dom = aux loc (Cic.Name var :: context) where in
 221         Domain.union body_dom where_dom
 222     | CicTextualParser2Ast.LetRec (kind, defs, where) ->
 223         let context' =
 224           List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
 225             context defs
 226         in
 227         let where_dom = aux loc context' where in
 228         let defs_dom =
 229           List.fold_left
 230             (fun dom (_, body, typ, _) ->
 231               Domain.union (aux loc context' body) (aux_option loc context typ))
 232             Domain.empty defs
 233         in
 234         Domain.union where_dom defs_dom
 235     | CicTextualParser2Ast.Ident (name, subst) ->
 236         (* TODO hanlde explicit substitutions *)
 237         (try
 238           let index = find_in_environment name context in
 239           if subst <> [] then
 240             CicTextualParser2.fail loc "Explicit substitutions not allowed here";
 241           Domain.empty
 242         with Not_found -> Domain.singleton (Id name))
 243     | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i)
 244     | CicTextualParser2Ast.Meta (index, local_context) ->
 245         List.fold_left
 246           (fun dom term -> Domain.union dom (aux_option loc context term))
 247             Domain.empty local_context
 248     | CicTextualParser2Ast.Sort _ -> Domain.empty
 249   and aux_option loc context = function
 250     | None -> Domain.empty
 251     | Some t -> aux loc context t
 252   in
 253   match ast with
 254   | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
 255   | _ -> assert false
 256
 257 module Make (C: Callbacks) =
 258   struct
 259     let choices_of_id mqi_handle id =
 260      let query  =  MQueryGenerator.locate id in
 261      let result = MQueryInterpreter.execute mqi_handle query in
 262      let uris =
 263       List.map
 264        (function uri,_ ->
 265          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
 266        ) result in
 267       C.output_html (`Msg (`T "Locate query:"));
 268       MQueryUtil.text_of_query
 269        (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
 270        "" query;
 271       C.output_html (`Msg (`T "Result:"));
 272       MQueryUtil.text_of_result
 273         (fun s -> C.output_html (`Msg (`T s))) "" result;
 274       let uris' =
 275        match uris with
 276         | [] ->
 277            [UriManager.string_of_uri (C.input_or_locate_uri
 278             ~title:("URI matching \"" ^ id ^ "\" unknown."))]
 279         | [uri] -> [uri]
 280         | _ ->
 281             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
 282              ~ok:"Try every selection." ~enable_button_for_non_vars:true
 283              ~title:"Ambiguous input." ~id
 284              ~msg: ("Ambiguous input \"" ^ id ^
 285                 "\". Please, choose one or more interpretations:")
 286              uris
 287       in
 288       List.map
 289         (fun uri ->
 290           (uri,
 291            let term =
 292              try
 293                HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
 294              with _ -> assert false
 295             in
 296            fun _ _ _ -> term))
 297         uris'
 298
 299     let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
 300     =
 301       let current_dom = (* TODO temporary, remove ASAP *)
 302         Environment.fold (fun item _ dom -> Domain.add item dom)
 303           current_env Domain.empty
 304       in
 305       debug_print "NEW DISAMBIGUATE INPUT";
 306       let disambiguate_context =  (* cic context -> disambiguate context *)
 307         List.map
 308           (function None -> Cic.Anonymous | Some (name, _) -> name)
 309           context
 310       in
 311       let term_dom = domain_of_term ~context:disambiguate_context term in
 312       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
 313         (string_of_domain term_dom));
 314       let todo_dom = Domain.diff term_dom current_dom in
 315       (* (2) lookup function for any item (Id/Symbol/Num) *)
 316       let lookup_choices =
 317         let id_choices = Hashtbl.create 1023 in
 318         fun item ->
 319         let choices =
 320           match item with
 321           | Id id ->
 322               (try
 323                 Hashtbl.find id_choices id
 324               with Not_found ->
 325                 let choices = choices_of_id mqi_handle id in
 326                 Hashtbl.add id_choices id choices;
 327                 choices)
 328           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
 329           | Num instance -> DisambiguateChoices.lookup_num_choices ()
 330         in
 331         if choices = [] then raise (No_choices item);
 332         choices
 333       in
 334       (* (3) test an interpretation filling with meta uninterpreted identifiers
 335        *)
 336       let test_env current_env todo_dom =
 337         let filled_env =
 338           Domain.fold
 339             (fun item env ->
 340               Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
 341             todo_dom current_env
 342         in
 343         try
 344           let cic_term =
 345             interpretate ~context:disambiguate_context ~env:filled_env term
 346           in
 347           refine metasenv context cic_term
 348         with
 349         | Try_again -> Uncertain
 350         | DisambiguateChoices.Invalid_choice -> Ko
 351       in
 352       (* (4) build all possible interpretations *)
 353       let rec aux current_env todo_dom =
 354         if Domain.is_empty todo_dom then
 355           match test_env current_env Domain.empty with
 356           | Ok (term, metasenv) -> [ current_env, term, metasenv ]
 357           | Ko | Uncertain -> []
 358         else
 359           let item = Domain.choose todo_dom in
 360           let remaining_dom = Domain.remove item todo_dom in
 361           debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item));
 362           let choices = lookup_choices item in
 363           let rec filter = function
 364             | [] -> []
 365             | codomain_item :: tl ->
 366                 let new_env = Environment.add item codomain_item current_env in
 367                 (match test_env new_env remaining_dom with
 368                 | Ok (term, metasenv) ->
 369                     (if Domain.is_empty remaining_dom then
 370                       [ new_env, term, metasenv ]
 371                     else
 372                       aux new_env remaining_dom)
 373                     @ filter tl
 374                 | Uncertain ->
 375                     (if Domain.is_empty remaining_dom then
 376                       []
 377                     else
 378                       aux new_env remaining_dom)
 379                     @ filter tl
 380                 | Ko -> filter tl)
 381           in
 382           filter choices
 383       in
 384       let (choosed_env, choosed_term, choosed_metasenv) =
 385         match aux current_env todo_dom with
 386         | [] -> raise NoWellTypedInterpretation
 387         | [ x ] ->
 388             debug_print "UNA SOLA SCELTA";
 389             x
 390         | l ->
 391             debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
 392             let choices =
 393               List.map
 394                 (fun (env, _, _) ->
 395                   List.map
 396                     (fun domain_item ->
 397                       let description =
 398                         fst (Environment.find domain_item env)
 399                       in
 400                       (descr_of_domain_item domain_item, description))
 401                     (Domain.elements term_dom))
 402                 l
 403             in
 404             let choosed = C.interactive_interpretation_choice choices in
 405             List.nth l choosed
 406       in
 407       (choosed_env, choosed_metasenv, choosed_term)
 408
 409   end
 410