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