(* 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                                 *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

open Printf

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

module type Callbacks =
  sig
    val interactive_user_uri_choice :
      selection_mode:[`SINGLE | `MULTIPLE] ->
      ?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 list
    val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri
  end
;;

type domain_and_interpretation =
 CicTextualParser0.interpretation_domain_item list *
  CicTextualParser0.interpretation
;;

module Make(C:Callbacks) =
  struct

   let locate_one_id mqi_handle id =
    let query  =  MQueryGenerator.locate id in
    let result = MQueryInterpreter.execute mqi_handle query in
    let uris =
     List.map
      (function uri,_ ->
        MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
      ) result in
     HelmLogger.log (`Msg (`T "Locate query:"));
     MQueryUtil.text_of_query
      (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s)))
      "" query; 
     HelmLogger.log (`Msg (`T "Result:"));
     MQueryUtil.text_of_result (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
     let uris' =
      match uris with
         [] ->
          [UriManager.string_of_uri
           (C.input_or_locate_uri
             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
       | [uri] -> [uri]
       | _ ->
         C.interactive_user_uri_choice
          ~selection_mode:`MULTIPLE
          ~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 MQueryMisc.cic_textual_parser_uri_of_string uris'


   exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput

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

   type ambiguous_choices =
      Uris of CicTextualParser0.uri list
    | Symbols of (CicTextualParser0.interpretation -> Cic.term) list

   let disambiguate_input mqi_handle 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
       (function
           CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id)
         | CicTextualParser0.Symbol (descr,choices) ->
            (* CSC: Implementare la funzione di filtraggio manuale *)
            (* CSC: corrispondente alla locate_one_id              *)
            Symbols (List.map snd choices)
       ) dom' in
     let tests_no =
      List.fold_left
       (fun i uris ->
         let len =
          match uris with
             Uris l -> List.length l
           | Symbols l -> List.length l
         in
          i * len
       ) 1 list_of_uris
     in
      if tests_no > 1 then
       HelmLogger.log (`Msg (`T (sprintf
        "Disambiguation phase started: up to %d cases will be tried"
        tests_no)));
     (* 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' =
        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 metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
         try
          let term,_,metasenv'' =
           CicRefine.type_of_aux' metasenv' context expr
          in
           Ok (term,metasenv'')
         with
            CicRefine.Uncertain _ ->
prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
             Uncertain
          | CicRefine.RefineFailure _ ->
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 : CicTextualParser0.interpretation_codomain_item)::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
            (match uris with
                Uris uris ->
                 filter
                  (List.map (function uri -> CicTextualParser0.Uri uri) uris)
              | Symbols symbols ->
                 filter
                  (List.map
                    (function sym -> CicTextualParser0.Term sym) symbols))
        | _,_ -> 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
            (Printf.sprintf
              "+++++ ASSERTION FAILED: a refine operation should not modify the metasenv. Old metasenv:\n %s\n New metasenv:\n %s\n"
              (CicMetaSubst.ppmetasenv metasenv [])
              (CicMetaSubst.ppmetasenv newmetasenv [])) ;
           (* an assert would raise an exception that could be caught *)
           exit 1
          end
       ) resolve_ids ;
      let res =
       match resolve_ids with
          [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
        | [_] -> resolve_ids
        | _ ->
          let choices =
           List.map
            (function (resolve,_,_) ->
              List.map
               (function id ->
                 (match id with
                     CicTextualParser0.Id id -> id
                   | CicTextualParser0.Symbol (descr,_) -> descr
                 ),
                  match resolve id with
                     None -> assert false
                   | Some (CicTextualParser0.Uri 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 ^                           ")")
                   | Some (CicTextualParser0.Term term) ->
                      (* CSC: Implementare resa delle scelte *)
                      "To be implemented XXX01"
                   | Some CicTextualParser0.Implicit -> assert false
               ) dom
            ) resolve_ids
          in
           let indexes = C.interactive_interpretation_choice choices in
            List.map (List.nth resolve_ids) indexes
      in
       List.map
        (fun (resolve_id',term,metasenv') ->
          (known_ids @ dom', resolve_id'), metasenv',term
        ) res
end
;;

module EnvironmentP3 =
 struct
  type t = domain_and_interpretation

  let empty = ""

  let to_string (dom,resolve_id) =
   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)
   in
   String.concat "\n"
    (List.map
      (function v ->
        let uri =
         match resolve_id v with
            None -> assert false
          | Some (CicTextualParser0.Uri uri) -> uri
          | Some (CicTextualParser0.Term _)
          | Some CicTextualParser0.Implicit -> assert false
        in
         "alias " ^
          (match v with
              CicTextualParser0.Id id -> id
            | CicTextualParser0.Symbol (descr,_) ->
               (* CSC: To be implemented *)
               assert false
          )^ " " ^ (string_of_cic_textual_parser_uri uri)
      ) dom)

  let of_string inputtext =
    let regexpr =
     let alfa = "[a-zA-Z_-]" in
     let digit = "[0-9]" in
     let ident = alfa ^ "\\(" ^ alfa ^ "\\|" ^ digit ^ "\\)*" in
     let blanks = "\\( \\|\t\\|\n\\)+" in
     let nonblanks = "[^ \t\n]+" in
     let uri = "/\\(" ^ ident ^ "/\\)*" ^ nonblanks in
      (* not very strict check *)
      Str.regexp
       ("alias" ^ blanks ^ "\\(" ^ ident ^ "\\)" ^ blanks ^ "\\(" ^ uri ^ "\\)")
    in
     let rec aux n =
      try
       let n' = Str.search_forward regexpr inputtext n in
        let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
        let uri =
         MQueryMisc.cic_textual_parser_uri_of_string
          ("cic:" ^ (Str.matched_group 5 inputtext))
        in
         let dom,resolve_id = aux (n' + 1) in
          if List.mem id dom then
           dom,resolve_id
          else
           id::dom,
            (function id' ->
              if id = id' then
               Some (CicTextualParser0.Uri uri)
              else resolve_id id')
      with
       Not_found -> ([],function _ -> None)
     in
      aux 0
 end