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

open Printf

open DisambiguateTypes
open UriManager

exception No_choices of domain_item
exception NoWellTypedInterpretation
exception PathNotWellFormed

  (** raised when an environment is not enough informative to decide *)
exception Try_again

let debug = false
let debug_print = if debug then prerr_endline else ignore

(*
  (** print benchmark information *)
let benchmark = true
let max_refinements = ref 0       (* benchmarking is not thread safe *)
let actual_refinements = ref 0
let domain_size = ref 0
let choices_avg = ref 0.
*)

let floc_of_loc (loc_begin, loc_end) =
  let floc_begin =
    { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
      Lexing.pos_cnum = loc_begin }
  in
  let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
  (floc_begin, floc_end)

let dummy_floc = floc_of_loc (-1, -1)

let descr_of_domain_item = function
 | Id s -> s
 | Symbol (s, _) -> s
 | Num i -> string_of_int i

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

let refine_term metasenv context uri term ugraph =
(*   if benchmark then incr actual_refinements; *)
  assert (uri=None);
  let metasenv, term = 
    CicMkImplicit.expand_implicits metasenv [] context term in
    debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
    try
      let term', _, metasenv',ugraph1 = 
	CicRefine.type_of_aux' metasenv context term ugraph in
	(Ok (term', metasenv')),ugraph1
    with
      | CicRefine.Uncertain s ->
          debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
          Uncertain,ugraph
      | CicRefine.RefineFailure msg ->
          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
            (CicPp.ppterm term) msg);
          Ko,ugraph

let refine_obj metasenv context uri obj ugraph =
 assert (context = []);
 let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in
   debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj));
   try
     let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
       (Ok (obj', metasenv)),ugraph
   with
     | CicRefine.Uncertain s ->
         debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj) ;
         Uncertain,ugraph
     | CicRefine.RefineFailure msg ->
         debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
           (CicPp.ppobj obj) msg);
         Ko,ugraph

let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
  try
    snd (Environment.find item env) env num args
  with Not_found -> 
    failwith ("Domain item not found: " ^ 
      (DisambiguateTypes.string_of_domain_item item))

  (* TODO move it to Cic *)
let find_in_environment name (context: Cic.name list) =
  let rec aux acc = function
    | [] -> raise Not_found
    | Cic.Name hd :: tl when hd = name -> acc
    | _ :: tl ->  aux (acc + 1) tl
  in
  aux 1 context

let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
  assert (uri = None);
  let rec aux loc (context: Cic.name list) = function
    | CicNotationPt.AttributedTerm (`Loc loc, term) ->
        aux loc context term
    | CicNotationPt.AttributedTerm (_, term) -> aux loc context term
    | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
        let cic_args = List.map (aux loc context) args in
        resolve env (Symbol (symb, i)) ~args:cic_args ()
    | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
    | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
        let cic_type = aux_option loc context (Some `Type) typ in
        let cic_name = CicNotationUtil.cic_name_of_name var in
        let cic_body = aux loc (cic_name :: context) body in
        (match binder_kind with
        | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
        | `Pi
        | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
        | `Exists ->
            resolve env (Symbol ("exists", 0))
              ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
    | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
        let cic_term = aux loc context term in
        let cic_outtype = aux_option loc context None outtype in
        let do_branch ((head, args), term) =
          let rec do_branch' context = function
            | [] -> aux loc context term
            | (name, typ) :: tl ->
                let cic_name = CicNotationUtil.cic_name_of_name name in
                let cic_body = do_branch' (cic_name :: context) tl in
                let typ =
                  match typ with
                  | None -> Cic.Implicit (Some `Type)
                  | Some typ -> aux loc context typ
                in
                Cic.Lambda (cic_name, typ, cic_body)
          in
          do_branch' context args
        in
        let (indtype_uri, indtype_no) =
          match indty_ident with
          | Some indty_ident ->
              (match resolve env (Id indty_ident) () with
              | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
              | Cic.Implicit _ -> raise Try_again
              | _ -> raise Invalid_choice)
          | None ->
              let fst_constructor =
                match branches with
                | ((head, _), _) :: _ -> head
                | [] -> raise Invalid_choice
              in
              (match resolve env (Id fst_constructor) () with
              | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
                  (indtype_uri, indtype_no)
              | Cic.Implicit _ -> raise Try_again
              | _ -> raise Invalid_choice)
        in
        Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
          (List.map do_branch branches))
    | CicNotationPt.Cast (t1, t2) ->
        let cic_t1 = aux loc context t1 in
        let cic_t2 = aux loc context t2 in
        Cic.Cast (cic_t1, cic_t2)
    | CicNotationPt.LetIn ((name, typ), def, body) ->
        let cic_def = aux loc context def in
        let cic_name = CicNotationUtil.cic_name_of_name name in
        let cic_def =
          match typ with
          | None -> cic_def
          | Some t -> Cic.Cast (cic_def, aux loc context t)
        in
        let cic_body = aux loc (cic_name :: context) body in
        Cic.LetIn (cic_name, cic_def, cic_body)
    | CicNotationPt.LetRec (kind, defs, body) ->
        let context' =
          List.fold_left
            (fun acc ((name, _), _, _) ->
              CicNotationUtil.cic_name_of_name name :: acc)
            context defs
        in
        let cic_body = aux loc context' body in
        let inductiveFuns =
          List.map
            (fun ((name, typ), body, decr_idx) ->
              let cic_body = aux loc context' body in
              let cic_type = aux_option loc context (Some `Type) typ in
              let name =
                match CicNotationUtil.cic_name_of_name name with
                | Cic.Anonymous ->
                    CicNotationPt.fail loc
                      "Recursive functions cannot be anonymous"
                | Cic.Name name -> name
              in
              (name, decr_idx, cic_type, cic_body))
            defs
        in
        let counter = ref ~-1 in
        let build_term funs =
          (* this is the body of the fold_right function below. Rationale: Fix
           * and CoFix cases differs only in an additional index in the
           * inductiveFun list, see Cic.term *)
          match kind with
          | `Inductive ->
              (fun (var, _, _, _) cic ->
                incr counter;
                Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
          | `CoInductive ->
              let funs =
                List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
              in
              (fun (var, _, _, _) cic ->
                incr counter;
                Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
        in
        List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
    | CicNotationPt.Ident _
    | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
    | CicNotationPt.Ident (name, subst)
    | CicNotationPt.Uri (name, subst) as ast ->
        let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
        (try
          if is_uri ast then raise Not_found;(* don't search the env for URIs *)
          let index = find_in_environment name context in
          if subst <> None then
            CicNotationPt.fail loc "Explicit substitutions not allowed here";
          Cic.Rel index
        with Not_found ->
          let cic =
            if is_uri ast then  (* we have the URI, build the term out of it *)
              try
                CicUtil.term_of_uri (UriManager.uri_of_string name)
              with UriManager.IllFormedUri _ ->
                CicNotationPt.fail loc "Ill formed URI"
            else
              resolve env (Id name) ()
          in
          let mk_subst uris =
            let ids_to_uris =
              List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
            in
            (match subst with
            | Some subst ->
                List.map
                  (fun (s, term) ->
                    (try
                      List.assoc s ids_to_uris, aux loc context term
                     with Not_found ->
                       raise Invalid_choice))
                  subst
            | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
          in
          (try 
            match cic with
            | Cic.Const (uri, []) ->
                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                let uris = CicUtil.params_of_obj o in
                Cic.Const (uri, mk_subst uris)
            | Cic.Var (uri, []) ->
                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                let uris = CicUtil.params_of_obj o in
                Cic.Var (uri, mk_subst uris)
            | Cic.MutInd (uri, i, []) ->
               (try
                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                 let uris = CicUtil.params_of_obj o in
                 Cic.MutInd (uri, i, mk_subst uris)
                with
                 CicEnvironment.Object_not_found _ ->
                  (* if we are here it is probably the case that during the
                     definition of a mutual inductive type we have met an
                     occurrence of the type in one of its constructors.
                     However, the inductive type is not yet in the environment
                  *)
                  (*here the explicit_named_substituion is assumed to be of length 0 *)
                  Cic.MutInd (uri,i,[]))
            | Cic.MutConstruct (uri, i, j, []) ->
                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                let uris = CicUtil.params_of_obj o in
                Cic.MutConstruct (uri, i, j, mk_subst uris)
            | Cic.Meta _ | Cic.Implicit _ as t ->
(*
                debug_print (sprintf
                  "Warning: %s must be instantiated with _[%s] but we do not enforce it"
                  (CicPp.ppterm t)
                  (String.concat "; "
                    (List.map
                      (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
                      subst)));
*)
                t
            | _ ->
              raise Invalid_choice
           with 
             CicEnvironment.CircularDependency _ -> 
               raise Invalid_choice))
    | CicNotationPt.Implicit -> Cic.Implicit None
    | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
    | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
    | CicNotationPt.Meta (index, subst) ->
        let cic_subst =
          List.map
            (function None -> None | Some term -> Some (aux loc context term))
            subst
        in
        Cic.Meta (index, cic_subst)
    | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
    | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
    | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
    | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
    | CicNotationPt.Symbol (symbol, instance) ->
        resolve env (Symbol (symbol, instance)) ()
    | _ -> assert false (* god bless Bologna *)
  and aux_option loc (context: Cic.name list) annotation = function
    | None -> Cic.Implicit annotation
    | Some term -> aux loc context term
  in
  match ast with
  | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term
  | term -> aux dummy_floc context term

let interpretate_path ~context ~env path =
 interpretate_term ~context ~env ~uri:None ~is_path:true path

let interpretate_obj ~context ~env ~uri ~is_path obj =
 assert (context = []);
 assert (is_path = false);
 match obj with
  | GrafiteAst.Inductive (params,tyl) ->
     let uri = match uri with Some uri -> uri | None -> assert false in
     let context,params =
      let context,res =
       List.fold_left
        (fun (context,res) (name,t) ->
          Cic.Name name :: context,
          (name, interpretate_term context env None false t)::res
        ) ([],[]) params
      in
       context,List.rev res in
     let add_params =
      List.fold_right
       (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
     let name_to_uris =
      snd (
       List.fold_left
        (*here the explicit_named_substituion is assumed to be of length 0 *)
        (fun (i,res) (name,_,_,_) ->
          i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
        ) (0,[]) tyl) in
     let con_env = DisambiguateTypes.env_of_list name_to_uris env in
     let undebrujin t =
      snd
       (List.fold_right
         (fun (name,_,_,_) (i,t) ->
           (*here the explicit_named_substituion is assumed to be of length 0 *)
           let t' = Cic.MutInd (uri,i,[])  in
           let t = CicSubstitution.subst t' t in
            i - 1,t
         ) tyl (List.length tyl - 1,t)) in
     let tyl =
      List.map
       (fun (name,b,ty,cl) ->
         let ty' = add_params (interpretate_term context env None false ty) in
         let cl' =
          List.map
           (fun (name,ty) ->
             let ty' =
              add_params (interpretate_term context con_env None false ty)
             in
              name,undebrujin ty'
           ) cl
         in
          name,b,ty',cl'
       ) tyl
     in
      Cic.InductiveDefinition (tyl,[],List.length params,[])
  | GrafiteAst.Record (params,name,ty,fields) ->
     let uri = match uri with Some uri -> uri | None -> assert false in
     let context,params =
      let context,res =
       List.fold_left
        (fun (context,res) (name,t) ->
          (Cic.Name name :: context),
          (name, interpretate_term context env None false t)::res
        ) ([],[]) params
      in
       context,List.rev res in
     let add_params =
      List.fold_right
       (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
     let ty' = add_params (interpretate_term context env None false ty) in
     let fields' =
      snd (
       List.fold_left
        (fun (context,res) (name,ty) ->
          let context' = Cic.Name name :: context in
           context',(name,interpretate_term context env None false ty)::res
        ) (context,[]) fields) in
     let concl =
      (*here the explicit_named_substituion is assumed to be of length 0 *)
      let mutind = Cic.MutInd (uri,0,[]) in
      if params = [] then mutind
      else
       Cic.Appl
        (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
     let con =
      List.fold_left
       (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
       concl fields' in
     let con' = add_params con in
     let tyl = [name,true,ty',["mk_" ^ name,con']] in
     let field_names = List.map fst fields in
      Cic.InductiveDefinition
       (tyl,[],List.length params,[`Class (`Record field_names)])
  | GrafiteAst.Theorem (flavour, name, ty, bo) ->
     let attrs = [`Flavour flavour] in
     let ty' = interpretate_term [] env None false ty in
     (match bo with
        None ->
         Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
      | Some bo ->
         let bo' = Some (interpretate_term [] env None false bo) in
          Cic.Constant (name,bo',ty',[],attrs))
          

  (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
let rev_uniq =
  let module SortedItem =
    struct
      type t = DisambiguateTypes.domain_item
      let compare = Pervasives.compare
    end
  in
  let module Set = Set.Make (SortedItem) in
  fun l ->
    let rev_l = List.rev l in
    let (_, uniq_rev_l) =
      List.fold_left
        (fun (members, rev_l) elt ->
          if Set.mem elt members then
            (members, rev_l)
          else
            Set.add elt members, elt :: rev_l)
        (Set.empty, []) rev_l
    in
    List.rev uniq_rev_l

(* "aux" keeps domain in reverse order and doesn't care about duplicates.
 * Domain item more in deep in the list will be processed first.
 *)
let rec domain_rev_of_term ?(loc = dummy_floc) context = function
  | CicNotationPt.AttributedTerm (`Loc loc, term) ->
     domain_rev_of_term ~loc context term
  | CicNotationPt.AttributedTerm (_, term) ->
      domain_rev_of_term ~loc context term
  | CicNotationPt.Appl terms ->
      List.fold_left
       (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
  | CicNotationPt.Binder (kind, (var, typ), body) ->
      let kind_dom =
        match kind with
        | `Exists -> [ Symbol ("exists", 0) ]
        | _ -> []
      in
      let type_dom = domain_rev_of_term_option loc context typ in
      let body_dom =
        domain_rev_of_term ~loc
          (CicNotationUtil.cic_name_of_name var :: context) body
      in
      body_dom @ type_dom @ kind_dom
  | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
      let term_dom = domain_rev_of_term ~loc context term in
      let outtype_dom = domain_rev_of_term_option loc context outtype in
      let get_first_constructor = function
        | [] -> []
        | ((head, _), _) :: _ -> [ Id head ]
      in
      let do_branch ((head, args), term) =
        let (term_context, args_domain) =
          List.fold_left
            (fun (cont, dom) (name, typ) ->
              (CicNotationUtil.cic_name_of_name name :: cont,
               (match typ with
               | None -> dom
               | Some typ -> domain_rev_of_term ~loc cont typ @ dom)))
            (context, []) args
        in
        args_domain @ domain_rev_of_term ~loc term_context term
      in
      let branches_dom =
        List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
      in
      branches_dom @ outtype_dom @ term_dom @
      (match indty_ident with
       | None -> get_first_constructor branches
       | Some ident -> [ Id ident ])
  | CicNotationPt.Cast (term, ty) ->
      let term_dom = domain_rev_of_term ~loc context term in
      let ty_dom = domain_rev_of_term ~loc context ty in
      ty_dom @ term_dom
  | CicNotationPt.LetIn ((var, typ), body, where) ->
      let body_dom = domain_rev_of_term ~loc context body in
      let type_dom = domain_rev_of_term_option loc context typ in
      let where_dom =
        domain_rev_of_term ~loc
          (CicNotationUtil.cic_name_of_name var :: context) where
      in
      where_dom @ type_dom @ body_dom
  | CicNotationPt.LetRec (kind, defs, where) ->
      let context' =
        List.fold_left
          (fun acc ((var, typ), _, _) ->
            CicNotationUtil.cic_name_of_name var :: acc)
          context defs
      in
      let where_dom = domain_rev_of_term ~loc context' where in
      let defs_dom =
        List.fold_left
          (fun dom ((_, typ), body, _) ->
            domain_rev_of_term ~loc context' body @
            domain_rev_of_term_option loc context typ)
          [] defs
      in
      where_dom @ defs_dom
  | CicNotationPt.Ident (name, subst) ->
      (try
        let index = find_in_environment name context in
        if subst <> None then
          CicNotationPt.fail loc "Explicit substitutions not allowed here"
        else
          []
      with Not_found ->
        (match subst with
        | None -> [Id name]
        | Some subst ->
            List.fold_left
              (fun dom (_, term) ->
                let dom' = domain_rev_of_term ~loc context term in
                dom' @ dom)
              [Id name] subst))
  | CicNotationPt.Uri _ -> []
  | CicNotationPt.Implicit -> []
  | CicNotationPt.Num (num, i) -> [ Num i ]
  | CicNotationPt.Meta (index, local_context) ->
      List.fold_left
       (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
        local_context
  | CicNotationPt.Sort _ -> []
  | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
  | CicNotationPt.UserInput
  | CicNotationPt.Literal _
  | CicNotationPt.Layout _
  | CicNotationPt.Magic _
  | CicNotationPt.Variable _ -> assert false

and domain_rev_of_term_option loc context = function
  | None -> []
  | Some t -> domain_rev_of_term ~loc context t

let domain_of_term ~context ast =
 rev_uniq (domain_rev_of_term context ast)

let domain_of_obj ~context ast =
 assert (context = []);
 let domain_rev =
  match ast with
   | GrafiteAst.Theorem (_,_,ty,bo) ->
      (match bo with
          None -> []
        | Some bo -> domain_rev_of_term [] bo) @
      domain_of_term [] ty
   | GrafiteAst.Inductive (params,tyl) ->
      let dom =
       List.flatten (
        List.rev_map
         (fun (_,_,ty,cl) ->
           List.flatten (
            List.rev_map
             (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
            domain_rev_of_term [] ty) tyl) in
      let dom = 
       List.fold_left
        (fun dom (_,ty) ->
          domain_rev_of_term [] ty @ dom
        ) dom params
      in
       List.filter
        (fun name ->
          not (  List.exists (fun (name',_) -> name = Id name') params
              || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
        ) dom
   | GrafiteAst.Record (params,_,ty,fields) ->
      let dom =
       List.flatten
        (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
      let dom =
       List.filter
        (fun name->
          not (  List.exists (fun (name',_) -> name = Id name') params
              || List.exists (fun (name',_) -> name = Id name') fields)
        ) dom
      in
       List.fold_left
        (fun dom (_,ty) ->
          domain_rev_of_term [] ty @ dom
        ) (dom @ domain_rev_of_term [] ty) params
 in
  rev_uniq domain_rev

  (* dom1 \ dom2 *)
let domain_diff dom1 dom2 =
(* let domain_diff = Domain.diff *)
  let is_in_dom2 =
    List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
      (fun _ -> false) dom2
  in
  List.filter (fun elt -> not (is_in_dom2 elt)) dom1

module type Disambiguator =
sig
  val disambiguate_term :
    dbd:Mysql.dbd ->
    context:Cic.context ->
    metasenv:Cic.metasenv ->
    ?initial_ugraph:CicUniv.universe_graph -> 
    aliases:environment ->  (* previous interpretation status *)
    CicNotationPt.term ->
    (environment *                   (* new interpretation status *)
     Cic.metasenv *                  (* new metasenv *)
     Cic.term*
     CicUniv.universe_graph) list    (* disambiguated term *)

  val disambiguate_obj :
    dbd:Mysql.dbd ->
    aliases:environment ->           (* previous interpretation status *)
    uri:UriManager.uri option ->     (* required only for inductive types *)
    GrafiteAst.obj ->
    (environment *                   (* new interpretation status *)
     Cic.metasenv *                  (* new metasenv *)
     Cic.obj *
     CicUniv.universe_graph) list    (* disambiguated obj *)
end

module Make (C: Callbacks) =
  struct
    let choices_of_id dbd id =
      let uris = MetadataQuery.locate ~dbd id in
      let uris =
       match uris with
        | [] ->
           [(C.input_or_locate_uri
            ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
        | [uri] -> [uri]
        | _ ->
            C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
             ~ok:"Try selected." ~enable_button_for_non_vars:true
             ~title:"Ambiguous input." ~id
             ~msg: ("Ambiguous input \"" ^ id ^
                "\". Please, choose one or more interpretations:")
             uris
      in
      List.map
        (fun uri ->
          (UriManager.string_of_uri uri,
           let term =
             try
               CicUtil.term_of_uri uri
             with exn ->
               debug_print (UriManager.string_of_uri uri);
               debug_print (Printexc.to_string exn);
               assert false
            in
           fun _ _ _ -> term))
        uris

    let disambiguate_thing ~dbd ~context ~metasenv
      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
    =
      debug_print "NEW DISAMBIGUATE INPUT";
      let disambiguate_context =  (* cic context -> disambiguate context *)
        List.map
          (function None -> Cic.Anonymous | Some (name, _) -> name)
          context
      in
      debug_print ("TERM IS: " ^ (pp_thing thing));
      let thing_dom = domain_of_thing ~context:disambiguate_context thing in
      debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
        (string_of_domain thing_dom));
      let current_dom =
        Environment.fold (fun item _ dom -> item :: dom) current_env []
      in
      let todo_dom = domain_diff thing_dom current_dom in
      (* (2) lookup function for any item (Id/Symbol/Num) *)
      let lookup_choices =
        let id_choices = Hashtbl.create 1023 in
        fun item ->
        let choices =
          match item with
          | Id id ->
              (try
                Hashtbl.find id_choices id
              with Not_found ->
                let choices = choices_of_id dbd id in
                Hashtbl.add id_choices id choices;
                choices)
          | Symbol (symb, _) ->
              List.map DisambiguateChoices.mk_choice
                (CicNotationRew.lookup_interpretations symb)
(*               DisambiguateChoices.lookup_symbol_choices symb *)
          | Num instance -> DisambiguateChoices.lookup_num_choices ()
        in
        if choices = [] then raise (No_choices item);
        choices
      in

(*
      (* <benchmark> *)
      let _ =
        if benchmark then begin
          let per_item_choices =
            List.map
              (fun dom_item ->
                try
                  let len = List.length (lookup_choices dom_item) in
                  debug_print (sprintf "BENCHMARK %s: %d"
                    (string_of_domain_item dom_item) len);
                  len
                with No_choices _ -> 0)
              thing_dom
          in
          max_refinements := List.fold_left ( * ) 1 per_item_choices;
          actual_refinements := 0;
          domain_size := List.length thing_dom;
          choices_avg :=
            (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
        end
      in
      (* </benchmark> *)
*)

      (* (3) test an interpretation filling with meta uninterpreted identifiers
       *)
      let test_env current_env todo_dom ugraph = 
        let filled_env =
          List.fold_left
            (fun env item ->
               Environment.add item
               ("Implicit",
                 (match item with
                    | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
                    | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
            current_env todo_dom 
        in
        try
          let cic_thing =
            interpretate_thing ~context:disambiguate_context ~env:filled_env
             ~uri ~is_path:false thing
          in
          let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
            (k , ugraph1 )
        with
        | Try_again -> Uncertain, ugraph
        | Invalid_choice -> Ko, ugraph
      in
      (* (4) build all possible interpretations *)
      let rec aux current_env todo_dom base_univ =
        match todo_dom with
        | [] ->
            (match test_env current_env [] base_univ with
            | Ok (thing, metasenv),new_univ -> 
               [ current_env, metasenv, thing, new_univ ]
            | Ko,_ | Uncertain,_ -> [])
        | item :: remaining_dom ->
            debug_print (sprintf "CHOOSED ITEM: %s"
             (string_of_domain_item item));
            let choices = lookup_choices item in
            let rec filter univ = function 
              | [] -> []
              | codomain_item :: tl ->
                  debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
                  let new_env =
                    Environment.add item codomain_item current_env
                  in
                  (match test_env new_env remaining_dom univ with
                  | Ok (thing, metasenv),new_univ ->
                      (match remaining_dom with
                      | [] -> [ new_env, metasenv, thing, new_univ ]
                      | _ -> aux new_env remaining_dom new_univ )@ 
                        filter univ tl
                  | Uncertain,new_univ ->
                      (match remaining_dom with
                      | [] -> []
                      | _ -> aux new_env remaining_dom new_univ )@ 
                        filter univ tl
                  | Ko,_ -> filter univ tl)
            in
            filter base_univ choices 
      in
      let base_univ = initial_ugraph in
      try
        let res =
         match aux current_env todo_dom base_univ with
         | [] -> raise NoWellTypedInterpretation
         | [ e,me,t,u ] ->
             debug_print "UNA SOLA SCELTA";
             (* Experimental: we forget the environment [e] since we are able
                to recompute it. In this way we are forced to do more work
                later (since we have less aliases), but we have more freedom
                (since we have less aliases) in the future disambiguations. *)
             [ current_env,me,t,u]
         | l ->
             debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
             let choices =
               List.map
                 (fun (env, _, _, _) ->
                   List.map
                     (fun domain_item ->
                       let description =
                         fst (Environment.find domain_item env)
                       in
                       (descr_of_domain_item domain_item, description))
                     thing_dom)
                 l
             in
             let choosed = C.interactive_interpretation_choice choices in
             List.map (List.nth l) choosed
        in
(*
        (if benchmark then
          let res_size = List.length res in
          debug_print (sprintf
            ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
            "BENCHMARK:   estimated %.2f")
            !actual_refinements !max_refinements !domain_size res_size
            !choices_avg
            (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
*)
        res
     with
      CicEnvironment.CircularDependency s -> 
        failwith "Disambiguate: circular dependency"

    let disambiguate_term ~dbd ~context ~metasenv
      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
    =
     disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
      ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term
      ~interpretate_thing:interpretate_term ~refine_thing:refine_term term

    let disambiguate_obj ~dbd ~aliases ~uri obj =
     disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
      ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
      ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
      obj
  end

module Trivial =
struct
  exception Ambiguous_term of string
  exception Exit
  module Callbacks =
  struct
    let interactive_user_uri_choice ~selection_mode ?ok
          ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
              raise Exit
    let interactive_interpretation_choice interp = raise Exit
    let input_or_locate_uri ~(title:string) ?id = raise Exit
  end
  module Disambiguator = Make (Callbacks)
  let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
    ?(aliases = DisambiguateTypes.Environment.empty) term
  =
    let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
    try
      Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
        ?initial_ugraph ~aliases
    with Exit -> raise (Ambiguous_term term)
end