(* Copyright (C) 2000-2002, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(******************************************************************************)
(*                                                                            *)
(*                               PROJECT HELM                                 *)
(*                                                                            *)
(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
(*                                 06/01/2002                                 *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

(** Functions that should be moved in another module **)

exception IllFormedUri of string;;

let string_of_cic_textual_parser_uri uri =
 let module C = Cic in
 let module CTP = CicTextualParser0 in
  let uri' =
   match uri with
      CTP.ConUri uri -> UriManager.string_of_uri uri
    | CTP.VarUri uri -> UriManager.string_of_uri uri
    | CTP.IndTyUri (uri,tyno) ->
       UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
    | CTP.IndConUri (uri,tyno,consno) ->
       UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
        string_of_int consno
  in
   (* 4 = String.length "cic:" *)
   String.sub uri' 4 (String.length uri' - 4)
;;

let cic_textual_parser_uri_of_string uri' =
 prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri');
 try
  (* Constant *)
  if String.sub uri' (String.length uri' - 4) 4 = ".con" then
   CicTextualParser0.ConUri (UriManager.uri_of_string uri')
  else
   if String.sub uri' (String.length uri' - 4) 4 = ".var" then
    CicTextualParser0.VarUri (UriManager.uri_of_string uri')
   else
    (try
      (* Inductive Type *)
      let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
       CicTextualParser0.IndTyUri (uri'',typeno)
     with
      _ ->
       (* Constructor of an Inductive Type *)
       let uri'',typeno,consno =
        CicTextualLexer.indconuri_of_uri uri'
       in
        CicTextualParser0.IndConUri (uri'',typeno,consno)
    )
 with
  _ -> raise (IllFormedUri uri')
;;
let cic_textual_parser_uri_of_string uri' =
  let res = cic_textual_parser_uri_of_string uri' in
  prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res));
  res

(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
let wrong_xpointer_format_from_wrong_xpointer_format' uri =
 try
  let index_sharp =  String.index uri '#' in
  let index_rest = index_sharp + 10 in
   let baseuri = String.sub uri 0 index_sharp in
   let rest =
    String.sub uri index_rest (String.length uri - index_rest - 1)
   in
    baseuri ^ "#" ^ rest
 with Not_found -> uri
;;

(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
let get_last_query = 
 let query = ref "" in
  MQueryGenerator.set_confirm_query
   (function q -> query := MQueryUtil.text_of_query q ; true) ;
  function result ->
   !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
;;

(** This module provides a functor to disambiguate the input **)
(** given a set of user-interface call-backs                 **)

module type Callbacks =
  sig
    val output_html : string -> unit
    val interactive_user_uri_choice :
      selection_mode:[`SINGLE | `EXTENDED] ->
      ?ok:string ->
      ?enable_button_for_non_vars:bool ->
      title:string -> msg:string -> id:string -> string list -> string list
    val interactive_interpretation_choice :
      (string * string) list list -> int
    val input_or_locate_uri : title:string -> UriManager.uri
  end
;;

type domain_and_interpretation =
 string list * (string -> CicTextualParser0.uri option)
;;

module Make(C:Callbacks) =
  struct

   let locate_one_id id =
    let result = MQueryGenerator.locate id in
    let uris =
     List.map
      (function uri,_ ->
        wrong_xpointer_format_from_wrong_xpointer_format' uri
      ) result in
    let html=
     " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
    in
     C.output_html html ;
     let uris' =
      match uris with
         [] ->
          [UriManager.string_of_uri
           (C.input_or_locate_uri
             ~title:("URI matching \"" ^ id ^ "\" unknown."))]
       | [uri] -> [uri]
       | _ ->
         C.interactive_user_uri_choice
          ~selection_mode:`EXTENDED
          ~ok:"Try every selection."
          ~enable_button_for_non_vars:true
          ~title:"Ambiguous input."
          ~msg:
            ("Ambiguous input \"" ^ id ^
             "\". Please, choose one or more interpretations:")
          ~id
          uris
     in
      List.map cic_textual_parser_uri_of_string uris'


   exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput

   type test_result =
      Ok of Cic.term * Cic.metasenv
    | Ko
    | Uncertain

   let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
    let known_ids,resolve_id = id_to_uris in
    let dom' =
     let rec filter =
      function
         [] -> []
       | he::tl ->
          if List.mem he known_ids then filter tl else he::(filter tl)
     in
      filter dom
    in
     (* for each id in dom' we get the list of uris associated to it *)
     let list_of_uris = List.map locate_one_id dom' in
     let tests_no =
      List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
     in
      if tests_no > 1 then
       C.output_html
        ("<h1>Disambiguation phase started: " ^
          string_of_int tests_no ^ " cases will be tried.") ;
     (* and now we compute the list of all possible assignments from *)
     (* id to uris that generate well-typed terms                    *)
     let resolve_ids =
      (* function to test if a partial interpretation is so far correct *)
      let test resolve_id residual_dom =
       (* We put implicits in place of every identifier that is not *)
       (* resolved by resolve_id                                    *)
       let resolve_id'' =
        let resolve_id' =
         function id ->
          match resolve_id id with
             None -> None
           | Some uri -> Some (CicTextualParser0.Uri uri)
        in
         List.fold_left
          (fun f id ->
            function id' ->
             if id = id' then Some (CicTextualParser0.Implicit) else f id'
          ) resolve_id' residual_dom
       in
        (* and we try to refine the term *)
        let saved_status = !CicTextualParser0.metasenv in
        let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
        (* The parser is imperative ==> we must restore the old status ;-(( *)
        CicTextualParser0.metasenv := saved_status ;
         try
          let term,_,_,metasenv'' =
           CicRefine.type_of_aux' metasenv' context expr
          in
           Ok (term,metasenv'')
         with
            CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
             (try
               let term = CicTypeChecker.type_of_aux' metasenv' context expr in
                Ok (term,metasenv')
              with _ -> Ko
             )
          | CicRefine.Uncertain _ ->
prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
             Uncertain
          | _ ->
prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
            Ko
      in
      let rec aux resolve_id ids list_of_uris =
       match ids,list_of_uris with
          [],[] ->
           (match test resolve_id [] with
               Ok (term,metasenv) -> [resolve_id,term,metasenv]
             | Ko | Uncertain -> [])
        | id::idtl,uris::uristl ->
           let rec filter =
            function
               [] -> []
             | uri::uritl ->
                let resolve_id' =
                 function id' -> if id = id' then Some uri else resolve_id id'
                in
                 (match test resolve_id' idtl with
                     Ok (term,metasenv) ->
                      (* the next three ``if''s are used to avoid the base   *)
                      (* case where the term would be refined a second time. *)
                      (if uristl = [] then
                        [resolve_id',term,metasenv]
                       else
                        (aux resolve_id' idtl uristl)
                      ) @ (filter uritl)
                   | Uncertain ->
                      (if uristl = [] then []
                       else
                        (aux resolve_id' idtl uristl)
                      ) @ (filter uritl)
                   | Ko ->
                      filter uritl
                 )
           in
            filter uris
        | _,_ -> assert false
      in
       aux resolve_id dom' list_of_uris
     in
      List.iter
       (function (resolve,term,newmetasenv) ->
         (* If metasen <> newmetasenv is a normal condition, we should *)
         (* be prepared to apply the returned substitution to the      *)
         (* whole current proof.                                       *)
         if metasenv <> newmetasenv then
          begin
           prerr_endline
            ("+++++ ASSERTION FAILED: " ^
             "a refine operation should not modify the metasenv") ;
           (* an assert would raise an exception that could be caught *)
           exit 1
          end
       ) resolve_ids ;
      let resolve_id',term,metasenv' =
       match resolve_ids with
          [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
        | [resolve_id] -> resolve_id
        | _ ->
          let choices =
           List.map
            (function (resolve,_,_) ->
              List.map
               (function id ->
                 id,
                  match resolve id with
                     None -> assert false
                   | Some uri ->
                      match uri with
                         CicTextualParser0.ConUri uri
                       | CicTextualParser0.VarUri uri ->
                          UriManager.string_of_uri uri
                       | CicTextualParser0.IndTyUri (uri,tyno) ->
                          UriManager.string_of_uri uri ^ "#xpointer(1/" ^
                           string_of_int (tyno+1) ^ ")"
                       | CicTextualParser0.IndConUri (uri,tyno,consno) ->
                          UriManager.string_of_uri uri ^ "#xpointer(1/" ^
                           string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
               ) dom
            ) resolve_ids
          in
           let index = C.interactive_interpretation_choice choices in
            List.nth resolve_ids index
      in
       (known_ids @ dom', resolve_id'), metasenv',term
end
;;