X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=b71e908856ba017df051a5d244f7ab39a1fd9035;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=786971fc11cddcecab7d6e11a6785923753135f2;hpb=6459acbd4bb69475cfaa0b37a9771ced94193667;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 786971fc1..b71e90885 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -34,9 +34,18 @@ exception NoWellTypedInterpretation
   (** raised when an environment is not enough informative to decide *)
 exception Try_again
 
-let debug = true
+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 descr_of_domain_item = function
  | Id s -> s
  | Symbol (s, _) -> s
@@ -47,30 +56,30 @@ type test_result =
   | Ko
   | Uncertain
 
-let refine metasenv context term =
-  let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
-  debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
-  try
-    let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in
-    Ok (term', metasenv')
-  with
-    | CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
-        (* TODO remove this case as soon as refine is fully implemented *)
-        (try
-          debug_print (Printf.sprintf "TYPE CHECKER %s" (CicPp.ppterm term));
-          let term' = CicTypeChecker.type_of_aux' metasenv context term in
-          Ok (term',metasenv)
-(*         with _ -> Ko) *)
-        with _ -> Uncertain)
-    | CicRefine.Uncertain _ ->
-        debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
-        Uncertain
-    | _ ->
-        debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
-        Ko
+let refine metasenv context term ugraph =
+(*   if benchmark then incr actual_refinements; *)
+  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 _ ->
+          debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+          Uncertain,ugraph
+      | CicRefine.RefineFailure msg ->
+          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+            (CicPp.ppterm term) msg);
+          Ko,ugraph
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
-  snd (Environment.find item env) env 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 =
@@ -83,12 +92,14 @@ let find_in_environment name context =
 
 let interpretate ~context ~env ast =
   let rec aux loc context = function
-    | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-    | CicTextualParser2Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
-    | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
+    | CicAst.AttributedTerm (`Loc loc, term) ->
+        aux loc context term
+    | CicAst.AttributedTerm (_, term) -> aux loc context term
+    | CicAst.Appl (CicAst.Symbol (symb, i) :: args) ->
         let cic_args = List.map (aux loc context) args in
         resolve env (Symbol (symb, i)) ~args:cic_args ()
-    | CicTextualParser2Ast.Binder (binder_kind, var, typ, body) ->
+    | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
+    | CicAst.Binder (binder_kind, (var, typ), body) ->
         let cic_type = aux_option loc context typ in
         let cic_body = aux loc (var :: context) body in
         (match binder_kind with
@@ -97,52 +108,79 @@ let interpretate ~context ~env ast =
         | `Exists ->
             resolve env (Symbol ("exists", 0))
               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
-    | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
+    | CicAst.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux loc context term in
         let cic_outtype = aux_option loc context outtype in
-        let do_branch (pat, term) =
+        let do_branch ((head, args), term) =
           let rec do_branch' context = function
             | [] -> aux loc context term
-            | hd :: tl ->
-                let cic_body = do_branch' (Cic.Name hd :: context) tl in
-                Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body)
+            | (name, typ) :: tl ->
+                let cic_body = do_branch' (name :: context) tl in
+                let typ =
+                  match typ with
+                  | None -> Cic.Implicit (Some `Type)
+                  | Some typ -> aux loc context typ
+                in
+                Cic.Lambda (name, typ, cic_body)
           in
-          match pat with
-          | _ :: tl -> (* ignoring constructor *) do_branch' context tl
-          | [] -> assert false
+          do_branch' context args
         in
         let (indtype_uri, indtype_no) =
-          match resolve env (Id indty_ident) () with
-          | Cic.MutInd (uri, tyno, _) -> uri, tyno
-          | Cic.Implicit -> raise Try_again
-          | _ -> raise DisambiguateChoices.Invalid_choice
+          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 DisambiguateChoices.Invalid_choice)
+          | None ->
+              let fst_constructor =
+                match branches with
+                | ((head, _), _) :: _ -> head
+                | [] -> raise DisambiguateChoices.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 DisambiguateChoices.Invalid_choice)
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
-    | CicTextualParser2Ast.LetIn (var, def, body) ->
+    | CicAst.LetIn ((name, typ), def, body) ->
         let cic_def = aux loc context def in
-        let name = Cic.Name var 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 (name :: context) body in
         Cic.LetIn (name, cic_def, cic_body)
-    | CicTextualParser2Ast.LetRec (kind, defs, body) ->
+    | CicAst.LetRec (kind, defs, body) ->
         let context' =
-          List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
+          List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
             context defs
         in
         let cic_body = aux loc context' body in
         let inductiveFuns =
           List.map
-            (fun (var, body, typ, decr_idx) ->
+            (fun ((name, typ), body, decr_idx) ->
               let cic_body = aux loc context' body in
               let cic_type = aux_option loc context typ in
-              (var, decr_idx, cic_type, cic_body))
+              let name =
+                match name with
+                | Cic.Anonymous ->
+                    CicTextualParser2.fail loc
+                      "Recursive functions cannot be anonymous"
+                | Cic.Name name -> name
+              in
+              (name, decr_idx, cic_type, cic_body))
             defs
         in
-        let counter = ref 0 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
-           * indcutiveFun list, see Cic.term *)
+           * inductiveFun list, see Cic.term *)
           match kind with
           | `Inductive ->
               (fun (var, _, _, _) cic ->
@@ -153,133 +191,264 @@ let interpretate ~context ~env ast =
                 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
-    | CicTextualParser2Ast.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
+    | CicAst.Ident (name, subst)
+    | CicAst.Uri (name, subst) as ast ->
+        let is_uri = function CicAst.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 <> [] then
-            CicTextualParser2.fail loc "Explicit substitutions not allowed here";
+          if subst <> None then
+            CicTextualParser2.fail loc
+              "Explicit substitutions not allowed here";
           Cic.Rel index
-        with Not_found -> resolve env (Id name) ())
-    | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num ()
-    | CicTextualParser2Ast.Meta (index, subst) ->
+        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 name
+              with UriManager.IllFormedUri _ ->
+                CicTextualParser2.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 DisambiguateChoices.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, []) ->
+                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)
+            | 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 ^ " := " ^ CicAstPp.pp_term term)
+                      subst)));
+*)
+                t
+            | _ ->
+              raise DisambiguateChoices.Invalid_choice
+           with 
+             CicEnvironment.CircularDependency _ -> 
+               raise DisambiguateChoices.Invalid_choice))
+    | CicAst.Implicit -> Cic.Implicit None
+    | CicAst.UserInput -> Cic.Implicit (Some `Hole)
+(*    | CicAst.UserInput -> assert false*)
+    | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
+    | CicAst.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)
-    | CicTextualParser2Ast.Sort `Prop -> Cic.Sort Cic.Prop
-    | CicTextualParser2Ast.Sort `Set -> Cic.Sort Cic.Set
-    | CicTextualParser2Ast.Sort `Type -> Cic.Sort Cic.Type
-    | CicTextualParser2Ast.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
+    | CicAst.Sort `Set -> Cic.Sort Cic.Set
+    | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+    | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicAst.Symbol (symbol, instance) ->
+        resolve env (Symbol (symbol, instance)) ()
   and aux_option loc context = function
-    | None -> Cic.Implicit
+    | None -> Cic.Implicit (Some `Type)
     | Some term -> aux loc context term
   in
   match ast with
-  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-  | _ -> assert false
+  | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+  | term -> aux CicAst.dummy_floc context term
 
 let domain_of_term ~context ast =
+    (* "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 aux loc context = function
-    | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
-    | CicTextualParser2Ast.Appl terms ->
-        List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
-          Domain.empty terms
-    | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
-        List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
-          (Domain.singleton (Symbol (symb, i))) args
-    | CicTextualParser2Ast.Binder (_, var, typ, body) ->
+    | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+    | CicAst.AttributedTerm (_, term) -> aux loc context term
+    | CicAst.Appl terms ->
+        List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
+    | CicAst.Binder (kind, (var, typ), body) ->
+        let kind_dom =
+          match kind with
+          | `Exists -> [ Symbol ("exists", 0) ]
+          | _ -> []
+        in
         let type_dom = aux_option loc context typ in
         let body_dom = aux loc (var :: context) body in
-        Domain.union type_dom body_dom
-    | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
+        body_dom @ type_dom @ kind_dom
+    | CicAst.Case (term, indty_ident, outtype, branches) ->
         let term_dom = aux loc context term in
         let outtype_dom = aux_option loc context outtype in
-        let do_branch (pat, term) =
-          match pat with
-          | _ :: tl ->
-              aux loc
-                (List.fold_left (fun acc var -> (Cic.Name var) :: acc)
-                  context tl)
-                term
-          | [] -> assert false
+        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) ->
+                (name :: cont,
+                 (match typ with
+                 | None -> dom
+                 | Some typ -> aux loc cont typ @ dom)))
+              (context, []) args
+          in
+          args_domain @ aux loc term_context term
         in
         let branches_dom =
-          List.fold_left (fun dom branch -> Domain.union dom (do_branch branch))
-            Domain.empty branches
+          List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
         in
-        Domain.add (Id indty_ident)
-          (Domain.union outtype_dom (Domain.union term_dom branches_dom))
-    | CicTextualParser2Ast.LetIn (var, body, where) ->
+        branches_dom @ outtype_dom @ term_dom @
+        (match indty_ident with
+         | None -> get_first_constructor branches
+         | Some ident -> [ Id ident ])
+    | CicAst.LetIn ((var, typ), body, where) ->
         let body_dom = aux loc context body in
-        let where_dom = aux loc (Cic.Name var :: context) where in
-        Domain.union body_dom where_dom
-    | CicTextualParser2Ast.LetRec (kind, defs, where) ->
+        let type_dom = aux_option loc context typ in
+        let where_dom = aux loc (var :: context) where in
+        where_dom @ type_dom @ body_dom
+    | CicAst.LetRec (kind, defs, where) ->
         let context' =
-          List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
+          List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
             context defs
         in
         let where_dom = aux loc context' where in
         let defs_dom =
           List.fold_left
-            (fun dom (_, body, typ, _) ->
-              Domain.union (aux loc context' body) (aux_option loc context typ))
-            Domain.empty defs
+            (fun dom ((_, typ), body, _) ->
+              aux loc context' body @ aux_option loc context typ)
+            [] defs
         in
-        Domain.union where_dom defs_dom
-    | CicTextualParser2Ast.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
+        where_dom @ defs_dom
+    | CicAst.Ident (name, subst) ->
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
-            CicTextualParser2.fail loc "Explicit substitutions not allowed here";
-          Domain.empty
-        with Not_found -> Domain.singleton (Id name))
-    | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i)
-    | CicTextualParser2Ast.Meta (index, local_context) ->
-        List.fold_left
-          (fun dom term -> Domain.union dom (aux_option loc context term))
-            Domain.empty local_context
-    | CicTextualParser2Ast.Sort _ -> Domain.empty
+          if subst <> None then
+            CicTextualParser2.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' = aux loc context term in
+                  dom' @ dom)
+                [Id name] subst))
+    | CicAst.Uri _ -> []
+    | CicAst.Implicit -> []
+    | CicAst.Num (num, i) -> [ Num i ]
+    | CicAst.Meta (index, local_context) ->
+        List.fold_left (fun dom term -> aux_option loc context term @ dom) []
+          local_context
+    | CicAst.Sort _ -> []
+    | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+    | CicAst.UserInput -> assert false
+
   and aux_option loc context = function
-    | None -> Domain.empty
+    | None -> []
     | Some t -> aux loc context t
   in
-  match ast with
-  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-  | _ -> assert false
+
+    (* 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
+  in
+            
+  rev_uniq
+    (match ast with
+    | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+    | term -> aux CicAst.dummy_floc context term)
+
+
+  (* 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 *)
+    CicAst.term ->
+    (environment *                   (* new interpretation status *)
+     Cic.metasenv *                  (* new metasenv *)
+     Cic.term*
+     CicUniv.universe_graph) list    (* disambiguated term *)
+end
 
 module Make (C: Callbacks) =
   struct
-    let choices_of_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
-      C.output_html (`Msg (`T "Locate query:"));
-      MQueryUtil.text_of_query
-       (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
-       "" query; 
-      C.output_html (`Msg (`T "Result:"));
-      MQueryUtil.text_of_result
-        (fun s -> C.output_html (`Msg (`T s))) "" result;
-      let uris' =
+    let choices_of_id dbd id =
+      let uris = MetadataQuery.locate ~dbd id in
+      let uris =
        match uris with
         | [] ->
            [UriManager.string_of_uri (C.input_or_locate_uri
-            ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+            ~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
+             ~ok:"Try selected." ~enable_button_for_non_vars:true
              ~title:"Ambiguous input." ~id
              ~msg: ("Ambiguous input \"" ^ id ^
                 "\". Please, choose one or more interpretations:")
@@ -290,28 +459,33 @@ module Make (C: Callbacks) =
           (uri,
            let term =
              try
-               HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
-             with _ -> assert false
+               CicUtil.term_of_uri uri
+             with exn ->
+               debug_print uri;
+               debug_print (Printexc.to_string exn);
+               assert false
             in
            fun _ _ _ -> term))
-        uris'
+        uris
 
-    let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
+    let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv
+      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+      term
     =
-      let current_dom = (* TODO temporary, remove ASAP *)
-        Environment.fold (fun item _ dom -> Domain.add item dom)
-          current_env Domain.empty
-      in
       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: " ^ (CicAstPp.pp_term term));
       let term_dom = domain_of_term ~context:disambiguate_context term in
       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
         (string_of_domain term_dom));
-      let todo_dom = Domain.diff term_dom current_dom in
+      let current_dom =
+        Environment.fold (fun item _ dom -> item :: dom) current_env []
+      in
+      let todo_dom = domain_diff term_dom current_dom in
       (* (2) lookup function for any item (Id/Symbol/Num) *)
       let lookup_choices =
         let id_choices = Hashtbl.create 1023 in
@@ -322,7 +496,7 @@ module Make (C: Callbacks) =
               (try
                 Hashtbl.find id_choices id
               with Not_found ->
-                let choices = choices_of_id mqi_handle id in
+                let choices = choices_of_id dbd id in
                 Hashtbl.add id_choices id choices;
                 choices)
           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
@@ -331,80 +505,149 @@ module Make (C: Callbacks) =
         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)
+              term_dom
+          in
+          max_refinements := List.fold_left ( * ) 1 per_item_choices;
+          actual_refinements := 0;
+          domain_size := List.length term_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 =
+      let test_env current_env todo_dom ugraph = 
         let filled_env =
-          Domain.fold
-            (fun item env ->
-              Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
-            todo_dom current_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_term =
             interpretate ~context:disambiguate_context ~env:filled_env term
           in
-          refine metasenv context cic_term
+          let k,ugraph1 = refine metasenv context cic_term ugraph in
+            (k , ugraph1 )
         with
-        | Try_again -> Uncertain
-        | DisambiguateChoices.Invalid_choice -> Ko
+        | Try_again -> Uncertain,ugraph
+        | DisambiguateChoices.Invalid_choice -> Ko,ugraph
       in
       (* (4) build all possible interpretations *)
-      let rec aux current_env todo_dom =
-        if Domain.is_empty todo_dom then
-          match test_env current_env Domain.empty with
-          | Ok (term, metasenv) -> [ current_env, term, metasenv ]
-          | Ko | Uncertain -> []
-        else
-          let item = Domain.choose todo_dom in
-          let remaining_dom = Domain.remove item todo_dom in
-          debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item));
-          let choices = lookup_choices item in
-          let rec filter = function
-            | [] -> []
-            | codomain_item :: tl ->
-                let new_env = Environment.add item codomain_item current_env in
-                (match test_env new_env remaining_dom with
-                | Ok (term, metasenv) ->
-                    (if Domain.is_empty remaining_dom then
-                      [ new_env, term, metasenv ]
-                    else
-                      aux new_env remaining_dom)
-                    @ filter tl
-                | Uncertain ->
-                    (if Domain.is_empty remaining_dom then
-                      []
-                    else
-                      aux new_env remaining_dom)
-                    @ filter tl
-                | Ko -> filter tl)
-          in
-          filter choices
-      in
-      let (choosed_env, choosed_term, choosed_metasenv) =
-        match aux current_env todo_dom with
-        | [] -> raise NoWellTypedInterpretation
-        | [ x ] ->
-            debug_print "UNA SOLA SCELTA";
-            x
-        | 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))
-                    (Domain.elements term_dom))
-                l
+      let rec aux current_env todo_dom base_univ =
+        match todo_dom with
+        | [] ->
+            (match test_env current_env [] base_univ with
+            | Ok (term, metasenv),new_univ -> 
+                               [ current_env, metasenv, term, 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 (term, metasenv),new_univ ->
+                      (match remaining_dom with
+                      | [] -> [ new_env, metasenv, term, 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
-            let choosed = C.interactive_interpretation_choice choices in
-            List.nth l choosed
+            filter base_univ choices 
       in
-      (choosed_env, choosed_metasenv, choosed_term)
+      let base_univ = initial_ugraph in
+      try
+        let res =
+         match aux current_env todo_dom base_univ with
+         | [] -> raise NoWellTypedInterpretation
+         | [ e,me,t,u ] as l ->
+             debug_print "UNA SOLA SCELTA";
+             [ e,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))
+                     term_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"
+  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 = CicTextualParser2.parse_term (Stream.of_string term) in
+    try
+      Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+        ?initial_ugraph ~aliases
+    with Exit -> raise (Ambiguous_term term)
+end