helm/gTopLevel/disambiguate.ml

   1 (* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 06/01/2002                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
  37 (* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE                   *)
  38 let get_last_query =
  39  let query = ref "" in
  40   let out s = query := ! query ^ s in
  41   MQueryGenerator.set_confirm_query
  42    (function q ->
  43     query := ""; MQueryUtil.text_of_query out q ""; true);
  44   function result ->
  45    out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
  46    !query
  47 ;;
  48
  49 (** This module provides a functor to disambiguate the input **)
  50 (** given a set of user-interface call-backs                 **)
  51
  52 module type Callbacks =
  53   sig
  54     val output_html : string -> unit
  55     val interactive_user_uri_choice :
  56       selection_mode:[`SINGLE | `EXTENDED] ->
  57       ?ok:string ->
  58       ?enable_button_for_non_vars:bool ->
  59       title:string -> msg:string -> id:string -> string list -> string list
  60     val interactive_interpretation_choice :
  61       (string * string) list list -> int
  62     val input_or_locate_uri : title:string -> UriManager.uri
  63   end
  64 ;;
  65
  66 type domain_and_interpretation =
  67  string list * (string -> CicTextualParser0.uri option)
  68 ;;
  69
  70 module Make(C:Callbacks) =
  71   struct
  72
  73    let locate_one_id id =
  74     let result = MQueryGenerator.locate id in
  75     let uris =
  76      List.map
  77       (function uri,_ ->
  78         MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
  79       ) result in
  80     let html=
  81      " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
  82     in
  83      C.output_html html ;
  84      let uris' =
  85       match uris with
  86          [] ->
  87           [UriManager.string_of_uri
  88            (C.input_or_locate_uri
  89              ~title:("URI matching \"" ^ id ^ "\" unknown."))]
  90        | [uri] -> [uri]
  91        | _ ->
  92          C.interactive_user_uri_choice
  93           ~selection_mode:`EXTENDED
  94           ~ok:"Try every selection."
  95           ~enable_button_for_non_vars:true
  96           ~title:"Ambiguous input."
  97           ~msg:
  98             ("Ambiguous input \"" ^ id ^
  99              "\". Please, choose one or more interpretations:")
 100           ~id
 101           uris
 102      in
 103       List.map MQueryMisc.cic_textual_parser_uri_of_string uris'
 104
 105
 106    exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
 107
 108    type test_result =
 109       Ok of Cic.term * Cic.metasenv
 110     | Ko
 111     | Uncertain
 112
 113    let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
 114     let known_ids,resolve_id = id_to_uris in
 115     let dom' =
 116      let rec filter =
 117       function
 118          [] -> []
 119        | he::tl ->
 120           if List.mem he known_ids then filter tl else he::(filter tl)
 121      in
 122       filter dom
 123     in
 124      (* for each id in dom' we get the list of uris associated to it *)
 125      let list_of_uris = List.map locate_one_id dom' in
 126      let tests_no =
 127       List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
 128      in
 129       if tests_no > 1 then
 130        C.output_html
 131         ("<h1>Disambiguation phase started: " ^
 132           string_of_int tests_no ^ " cases will be tried.") ;
 133      (* and now we compute the list of all possible assignments from *)
 134      (* id to uris that generate well-typed terms                    *)
 135      let resolve_ids =
 136       (* function to test if a partial interpretation is so far correct *)
 137       let test resolve_id residual_dom =
 138        (* We put implicits in place of every identifier that is not *)
 139        (* resolved by resolve_id                                    *)
 140        let resolve_id'' =
 141         let resolve_id' =
 142          function id ->
 143           match resolve_id id with
 144              None -> None
 145            | Some uri -> Some (CicTextualParser0.Uri uri)
 146         in
 147          List.fold_left
 148           (fun f id ->
 149             function id' ->
 150              if id = id' then Some (CicTextualParser0.Implicit) else f id'
 151           ) resolve_id' residual_dom
 152        in
 153         (* and we try to refine the term *)
 154         let saved_status = !CicTextualParser0.metasenv in
 155         let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
 156 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
 157         (* The parser is imperative ==> we must restore the old status ;-(( *)
 158         CicTextualParser0.metasenv := saved_status ;
 159          try
 160           let term,_,_,metasenv'' =
 161            CicRefine.type_of_aux' metasenv' context expr
 162           in
 163            Ok (term,metasenv'')
 164          with
 165             CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
 166              (try
 167                let term = CicTypeChecker.type_of_aux' metasenv' context expr in
 168                 Ok (term,metasenv')
 169               with _ -> Ko
 170              )
 171           | CicRefine.Uncertain _ ->
 172 prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
 173              Uncertain
 174           | _ ->
 175 prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
 176             Ko
 177       in
 178       let rec aux resolve_id ids list_of_uris =
 179        match ids,list_of_uris with
 180           [],[] ->
 181            (match test resolve_id [] with
 182                Ok (term,metasenv) -> [resolve_id,term,metasenv]
 183              | Ko | Uncertain -> [])
 184         | id::idtl,uris::uristl ->
 185            let rec filter =
 186             function
 187                [] -> []
 188              | uri::uritl ->
 189                 let resolve_id' =
 190                  function id' -> if id = id' then Some uri else resolve_id id'
 191                 in
 192                  (match test resolve_id' idtl with
 193                      Ok (term,metasenv) ->
 194                       (* the next three ``if''s are used to avoid the base   *)
 195                       (* case where the term would be refined a second time. *)
 196                       (if uristl = [] then
 197                         [resolve_id',term,metasenv]
 198                        else
 199                         (aux resolve_id' idtl uristl)
 200                       ) @ (filter uritl)
 201                    | Uncertain ->
 202                       (if uristl = [] then []
 203                        else
 204                         (aux resolve_id' idtl uristl)
 205                       ) @ (filter uritl)
 206                    | Ko ->
 207                       filter uritl
 208                  )
 209            in
 210             filter uris
 211         | _,_ -> assert false
 212       in
 213        aux resolve_id dom' list_of_uris
 214      in
 215       List.iter
 216        (function (resolve,term,newmetasenv) ->
 217          (* If metasen <> newmetasenv is a normal condition, we should *)
 218          (* be prepared to apply the returned substitution to the      *)
 219          (* whole current proof.                                       *)
 220          if metasenv <> newmetasenv then
 221           begin
 222            prerr_endline
 223             ("+++++ ASSERTION FAILED: " ^
 224              "a refine operation should not modify the metasenv") ;
 225            (* an assert would raise an exception that could be caught *)
 226            exit 1
 227           end
 228        ) resolve_ids ;
 229       let resolve_id',term,metasenv' =
 230        match resolve_ids with
 231           [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
 232         | [resolve_id] -> resolve_id
 233         | _ ->
 234           let choices =
 235            List.map
 236             (function (resolve,_,_) ->
 237               List.map
 238                (function id ->
 239                  id,
 240                   match resolve id with
 241                      None -> assert false
 242                    | Some uri ->
 243                       match uri with
 244                          CicTextualParser0.ConUri uri
 245                        | CicTextualParser0.VarUri uri ->
 246                           UriManager.string_of_uri uri
 247                        | CicTextualParser0.IndTyUri (uri,tyno) ->
 248                           UriManager.string_of_uri uri ^ "#xpointer(1/" ^
 249                            string_of_int (tyno+1) ^ ")"
 250                        | CicTextualParser0.IndConUri (uri,tyno,consno) ->
 251                           UriManager.string_of_uri uri ^ "#xpointer(1/" ^
 252                            string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
 253                ) dom
 254             ) resolve_ids
 255           in
 256            let index = C.interactive_interpretation_choice choices in
 257             List.nth resolve_ids index
 258       in
 259        (known_ids @ dom', resolve_id'), metasenv',term
 260 end
 261 ;;