(*
 * 
 * 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://helm.cs.unibo.it/
 *)

(* $Id$ *)

module Ast = NotationPt

type db = {
  (* maps (loc,domain_item) to alias *)
  interpr: GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t;
  (* the universe of possible interpretations for all symbols/ids/nums *)
  multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
  (* new_aliases: ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list *)
}

let get_interpr db =
  db.interpr
;;

let initial_status = {
  interpr = DisambiguateTypes.InterprEnv.empty;
  multi_aliases = DisambiguateTypes.Environment.empty;
  (* new_aliases = [] *)
}

class type g_status =
  object
   inherit Interpretations.g_status
   method disambiguate_db: db
  end

class virtual status uid =
 object (self)
  inherit Interpretations.status uid
  val disambiguate_db = initial_status
  method disambiguate_db = disambiguate_db
  method set_disambiguate_db v = {< disambiguate_db = v >}
  method set_disambiguate_status
   : 'status. #g_status as 'status -> 'self
      = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
 end

(* let eval_with_new_aliases status f =
 let status =
  status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
 let res = f status in
 let new_aliases = status#disambiguate_db.new_aliases in
  new_aliases,res
;;*)

let dump_aliases out msg status =
   out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
   DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
    status#disambiguate_db.interpr

let add_to_interpr status new_aliases =
   let interpr =
    List.fold_left (fun acc (k,c) -> 
      DisambiguateTypes.InterprEnv.add k c acc)
      status#disambiguate_db.interpr new_aliases 
   in
   let new_status =
     {status#disambiguate_db with interpr = interpr }
   in
    status#set_disambiguate_db new_status
   
let add_to_disambiguation_univ status new_aliases =
   let multi_aliases =
    List.fold_left (fun acc (d,c) -> 
      DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias 
         d c acc)
     status#disambiguate_db.multi_aliases new_aliases
   in
   let new_status =
     {status#disambiguate_db with multi_aliases = multi_aliases }
   in
    status#set_disambiguate_db new_status


exception BaseUriNotSetYet

let singleton msg = function
  | [x], _ -> x
  | l, _   ->
      let debug = 
         Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
         msg (List.length l)
      in
      prerr_endline debug; assert false

let __Implicit = "__Implicit__"
let __Closed_Implicit = "__Closed_Implicit__"

let ncic_mk_choice status a =
  prerr_endline "ncic_mk_choice";
  match a with
  | GrafiteAst.Symbol_alias (name,_, dsc) ->
     prerr_endline ("caso 1: " ^ name ^ "; " ^ dsc);
     if name = __Implicit then
       dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
     else if name = __Closed_Implicit then 
       dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
     else
       (prerr_endline (Printf.sprintf "mk_choice: symbol %s, interpr %s"
         name dsc);
       DisambiguateChoices.lookup_symbol_by_dsc status
        ~mk_implicit:(function 
           | true -> NCic.Implicit `Closed
           | false -> NCic.Implicit `Term)
        ~mk_appl:(function 
           (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
        ~term_of_nref:(fun nref -> NCic.Const nref)
       name dsc)
  | GrafiteAst.Number_alias (_,dsc) -> 
     prerr_endline ("caso 2: " ^ dsc);
     let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
      desc, `Num_interp
       (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
  | GrafiteAst.Ident_alias (name, uri) -> 
     prerr_endline ("caso 3: " ^ name);
     uri, `Sym_interp 
      (fun l->assert(l = []);
        let nref = NReference.reference_of_string uri in
         NCic.Const nref)
;;


let mk_implicit b =
  match b with
  | false -> 
      GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
  | true -> 
      GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
;;

let nlookup_in_library 
  interactive_user_uri_choice input_or_locate_uri item 
=
  match item with
  | DisambiguateTypes.Id id -> 
     (try
       let references = NCicLibrary.resolve id in
        List.map
         (fun u -> 
           GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
         ) references
      with
       NCicEnvironment.ObjectNotFound _ -> [])
  | _ -> []
;;

(* XXX TO BE REMOVED: no need to fix instances any more *)
(*let fix_instance item l =
 match item with
    DisambiguateTypes.Symbol (_,n) ->
     List.map
      (function
          GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
        | _ -> assert false
      ) l
  | DisambiguateTypes.Num n ->
     List.map
      (function
          GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
        | _ -> assert false
      ) l
  | DisambiguateTypes.Id _ -> l
;;*)
let fix_instance _ l = l;;

let rec diff_term loc t u = match (t,u) with
  | Ast.AttributedTerm (`Loc l,t'), Ast.AttributedTerm (_,u') -> diff_term l t' u'
  | Ast.AttributedTerm (_,t'), Ast.AttributedTerm (_,u') -> diff_term loc t' u' 
  | Ast.Appl tl, Ast.Appl ul ->
      List.fold_left2 (fun acc t0 u0 -> diff_term loc t0 u0@acc) [] tl ul
  | Ast.Binder (_,v1,b1), Ast.Binder (_,v2,b2) -> 
     diff_var loc v1 v2@ diff_term loc b1 b2
  | Ast.Case (t1,ity1,outty1,pl1),Ast.Case (t2,ity2,outty2,pl2) -> 
      let ity_interp = match ity1,ity2 with
      | Some (i,None), Some (_,Some r) -> 
         let uri = NReference.string_of_reference r in
         [loc,GrafiteAst.Ident_alias (i,uri)]
      | _ -> []
      in
      let oty_interp = match outty1,outty2 with
      | Some o1, Some o2 -> diff_term loc o1 o2
      | _ -> []
      in
      (* pl = (case_pattern * term) list *)
      let auxpatt (c1,u1) (c2,u2) acc =
        let diff_cp = match c1,c2 with
        | Ast.Pattern (i,href1,vars1), Ast.Pattern (_,href2,vars2) ->
           let diff_i = match href1,href2 with
             | None, Some r ->
                let uri = NReference.string_of_reference r in
                [loc,GrafiteAst.Ident_alias (i,uri)]
             | _ -> []
           in
           let diff_vars = 
             List.fold_right2 (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 []
           in
           diff_i @ diff_vars
        | _ -> []
        in
        diff_term loc u1 u2 @ diff_cp @ acc
      in
      let pl_interp = List.fold_right2 auxpatt pl1 pl2 [] in
      diff_term loc t1 t2 @ ity_interp @ oty_interp @ pl_interp
  | Ast.Cast (u1,v1),Ast.Cast (u2,v2) -> 
     diff_term loc u1 u2@diff_term loc v1 v2
  | Ast.LetIn (var1,u1,v1),Ast.LetIn (var2,u2,v2) ->
     diff_var loc var1 var2 @ diff_term loc u1 u2 @ diff_term loc v1 v2
  | Ast.LetRec (_,fl1,w1),Ast.LetRec (_,fl2,w2) ->
    let diff_funs =
      List.fold_right2 
        (fun (vars1,f1,b1,_) (vars2,f2,b2,_) acc ->
           let diff_vars = 
             List.fold_right2 
               (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 [] 
           in
           diff_vars @ diff_var loc f1 f2 @ diff_term loc b1 b2 @ acc)
        fl1 fl2 []
    in  
    diff_funs @ diff_term loc w1 w2
  | Ast.Ident (n,`Ambiguous),Ast.Ident (_,`Uri u) ->
      [loc,GrafiteAst.Ident_alias (n,u)]
  | Ast.Symbol (s, None),Ast.Symbol(_,Some (uri,desc)) ->
      [loc,GrafiteAst.Symbol_alias (s,uri,desc)]
  | Ast.Num (_, None),Ast.Num (_,Some (uri,desc)) ->
      [loc,GrafiteAst.Number_alias (uri,desc)]
  | _ -> [] (* leaves *)
and diff_var loc (_,v1) (_,v2) = match v1,v2 with
  | Some v1', Some v2' -> diff_term loc v1' v2'
  | _ -> []
;;

let diff_obj loc o1 o2 = match o1,o2 with
 | Ast.Inductive (ls1,itys1), Ast.Inductive (ls2,itys2) ->
     let diff_ls = 
       List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
     in
     let diff_itys =
       List.fold_right2
         (fun (i1,_,ty1,cl1) (i2,_,ty2,cl2) acc0 -> 
            let diff_cl =
              List.fold_right2 
               (fun (_,u) (_,v) acc1 -> diff_term loc u v @ acc1)
               cl1 cl2 []
            in
            diff_term loc ty1 ty2 @ diff_cl @ acc0)
         itys1 itys2 []
     in
     diff_ls @ diff_itys
 | Ast.Theorem (_,i1,b1,ty1,_), Ast.Theorem (_,i2,b2,ty2,_) ->
     let diff_tys = match ty1,ty2 with
     | Some ty1', Some ty2' -> diff_term loc ty1' ty2'
     | _ -> []
     in
     diff_term loc b1 b2 @ diff_tys
 | Ast.Record (ls1,_,ty1,fl1),Ast.Record (ls2,_,ty2,fl2) ->
     let diff_ls = 
       List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
     in
     let diff_fl =
       List.fold_right2
         (fun (_,f1,_,_) (_,f2,_,_) acc -> diff_term loc f1 f2 @ acc) fl1 fl2 []
     in
     diff_ls @ diff_term loc ty1 ty2 @ diff_fl
 | _ -> assert false
;;

let disambiguate_nterm status expty context metasenv subst thing
=
  let newast, metasenv, subst, cic =
    singleton "first"
      (NCicDisambiguate.disambiguate_term
        status
        ~aliases:status#disambiguate_db.interpr
        ~expty 
        ~universe:(status#disambiguate_db.multi_aliases)
        ~lookup_in_library:nlookup_in_library
        ~mk_choice:(ncic_mk_choice status)
        ~mk_implicit ~fix_instance
        ~description_of_alias:GrafiteAst.description_of_alias
        ~context ~metasenv ~subst thing)
  in
  let _,_,thing' = thing in
  let diff = diff_term Stdpp.dummy_loc thing' newast in
  let status = add_to_interpr status diff
  in
   metasenv, subst, status, cic
;;


type pattern = 
  NotationPt.term Disambiguate.disambiguator_input option * 
  (string * NCic.term) list * NCic.term option

let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
  let interp path = NCicDisambiguate.disambiguate_path status path in
  let goal_path = HExtlib.map_option interp goal_path in
  let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
  let wanted = HExtlib.map_option (fun x -> text,prefix_len,x) wanted in
   (wanted, hyp_paths, goal_path)
;;

let disambiguate_reduction_kind text prefix_len = function
  | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
  | `Normalize
  | `Simpl
  | `Unfold None
  | `Whd as kind -> kind
;;

let disambiguate_auto_params 
  disambiguate_term metasenv context (oterms, params) 
=
  match oterms with 
    | None -> metasenv, (None, params)
    | Some terms ->
	let metasenv, terms = 
	  List.fold_right 
	    (fun t (metasenv, terms) ->
               let metasenv,t = disambiguate_term context metasenv t in
		 metasenv,t::terms) terms (metasenv, [])
	in
	  metasenv, (Some terms, params)
;;

let disambiguate_just disambiguate_term context metasenv =
 function
    `Term t ->
      let metasenv,t = disambiguate_term context metasenv t in
       metasenv, `Term t
  | `Auto params ->
      let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
       context params
      in
       metasenv, `Auto params
;;
      
let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
  let uri =
   let baseuri = 
     match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
   in
   let name = 
     match obj with
     | NotationPt.Inductive (_,(name,_,_,_)::_)
     | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
     | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
     | NotationPt.Inductive _ -> assert false
   in
     NUri.uri_of_string (baseuri ^ "/" ^ name)
  in
  let ast, _, _, cic =
   singleton "third"
    (NCicDisambiguate.disambiguate_obj
      status
      ~lookup_in_library:nlookup_in_library
      ~description_of_alias:GrafiteAst.description_of_alias
      ~mk_choice:(ncic_mk_choice status)
      ~mk_implicit ~fix_instance ~uri
      ~aliases:status#disambiguate_db.interpr
      ~universe:(status#disambiguate_db.multi_aliases) 
      (text,prefix_len,obj)) in
  let diff = diff_obj Stdpp.dummy_loc obj ast in
  let status = add_to_interpr status diff
  in
   status, cic
;;

let disambiguate_cic_appl_pattern status args =
 let rec disambiguate =
  function
    NotationPt.ApplPattern l ->
     NotationPt.ApplPattern (List.map disambiguate l)
  | NotationPt.VarPattern id
     when not
      (List.exists
       (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
     ->
      let item = DisambiguateTypes.Id id in
       begin
        try
         match
          DisambiguateTypes.Environment.find item
           (* status#disambiguate_db.aliases *)
           status#disambiguate_db.multi_aliases
         with
         (* XXX : we only try the first match *)
            GrafiteAst.Ident_alias (_,uri)::_ ->
             NotationPt.NRefPattern (NReference.reference_of_string uri)
          | _ -> assert false
        with Not_found -> 
         prerr_endline
          ("LexiconEngine.eval_command: domain item not found: " ^ 
          (DisambiguateTypes.string_of_domain_item item));
         dump_aliases prerr_endline "" status;
         raise 
          (Failure
           ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
             end
  | p -> p
 in
  disambiguate
;;

let aliases_for_objs status refs =
 List.concat
  (List.map
    (fun nref ->
      let references = NCicLibrary.aliases_of nref in
       List.map
        (fun u ->
          let name = NCicPp.r2s status true u in
           (* FIXME : we are forgetting the interpretation of the Id
            * but is this useful anymore?!?!? *)
           DisambiguateTypes.Id name,
            GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
        ) references) refs)