X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=4a12727c7df207a6b381db4e4b8ae6b680a1c27b;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;hp=2775aed3b97428354897113d441a2c48c69e0f50;hpb=53ee2f5095adadffcafb40e436d23dc330d3bd87;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 2775aed3b..4a12727c7 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -30,6 +30,7 @@ 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
@@ -51,13 +52,14 @@ let descr_of_domain_item = function
  | Symbol (s, _) -> s
  | Num i -> string_of_int i
 
-type test_result =
-  | Ok of Cic.term * Cic.metasenv
+type 'a test_result =
+  | Ok of 'a * Cic.metasenv
   | Ko
   | Uncertain
 
-let refine metasenv context term ugraph =
+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));
@@ -74,6 +76,22 @@ let refine metasenv context term ugraph =
             (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
@@ -90,7 +108,8 @@ let find_in_environment name context =
   in
   aux 1 context
 
-let interpretate ~context ~env ast =
+let interpretate_term ~context ~env ~uri ~is_path ast =
+  assert (uri = None);
   let rec aux loc context = function
     | CicAst.AttributedTerm (`Loc loc, term) ->
         aux loc context term
@@ -195,6 +214,8 @@ let interpretate ~context ~env ast =
                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
+    | CicAst.Ident _
+    | CicAst.Uri _ when is_path -> raise PathNotWellFormed
     | CicAst.Ident (name, subst)
     | CicAst.Uri (name, subst) as ast ->
         let is_uri = function CicAst.Uri _ -> true | _ -> false in
@@ -241,9 +262,19 @@ let interpretate ~context ~env ast =
                 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)
+               (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
@@ -266,7 +297,6 @@ let interpretate ~context ~env ast =
                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 =
@@ -289,128 +319,263 @@ let interpretate ~context ~env ast =
   | 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
-    | 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
-        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 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 -> 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 ])
-    | CicAst.LetIn ((var, typ), body, where) ->
-        let body_dom = aux loc context body in
-        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, typ), _, _) -> var :: acc)
-            context defs
-        in
-        let where_dom = aux loc context' where in
-        let defs_dom =
-          List.fold_left
-            (fun dom ((_, typ), body, _) ->
-              aux loc context' body @ aux_option loc context typ)
-            [] defs
-        in
-        where_dom @ defs_dom
-    | CicAst.Ident (name, subst) ->
-        (try
-          let index = find_in_environment name context in
-          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
+let interpretate_path ~context ~env path =
+ interpretate_term ~context ~env ~uri:None ~is_path:true path
 
-  and aux_option loc context = function
-    | None -> []
-    | Some t -> aux loc context t
-  in
+let interpretate_obj ~context ~env ~uri ~is_path obj =
+ assert (context = []);
+ assert (is_path = false);
+ match obj with
+  | TacticAst.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,[])
+  | TacticAst.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
+      Cic.InductiveDefinition (tyl,[],List.length params,[`Class `Record])
+  | TacticAst.Theorem (_,name,ty,bo) ->
+     let ty' = interpretate_term [] env None false ty in
+     match bo with
+        None ->
+         Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],[])
+      | Some bo ->
+         let bo' = Some (interpretate_term [] env None false bo) in
+          Cic.Constant (name,bo',ty',[],[])
 
-    (* 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
+  (* 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
-    let module Set = Set.Make (SortedItem) in
-    fun l ->
-      let rev_l = List.rev l in
-      let (_, uniq_rev_l) =
+    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 = CicAst.dummy_floc) context = function
+  | CicAst.AttributedTerm (`Loc loc, term) ->
+     domain_rev_of_term ~loc context term
+  | CicAst.AttributedTerm (_, term) -> domain_rev_of_term ~loc context term
+  | CicAst.Appl terms ->
+      List.fold_left
+       (fun dom term -> domain_rev_of_term ~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 = domain_rev_of_term_option loc context typ in
+      let body_dom = domain_rev_of_term ~loc (var :: context) body in
+      body_dom @ type_dom @ kind_dom
+  | CicAst.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) ->
+              (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 ])
+  | CicAst.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 (var :: context) where in
+      where_dom @ type_dom @ body_dom
+  | CicAst.LetRec (kind, defs, where) ->
+      let context' =
+        List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
+          context defs
+      in
+      let where_dom = domain_rev_of_term ~loc context' where in
+      let defs_dom =
         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
+          (fun dom ((_, typ), body, _) ->
+            domain_rev_of_term ~loc context' body @
+            domain_rev_of_term_option loc context typ)
+          [] defs
       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)
+      where_dom @ defs_dom
+  | CicAst.Ident (name, subst) ->
+      (try
+        let index = find_in_environment name context in
+        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' = domain_rev_of_term ~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 -> domain_rev_of_term_option loc context term @ dom) []
+        local_context
+  | CicAst.Sort _ -> []
+  | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+  | CicAst.UserInput -> 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
+   | TacticAst.Theorem (_,_,ty,bo) ->
+      (match bo with
+          None -> []
+        | Some bo -> domain_rev_of_term [] bo) @
+      domain_of_term [] ty
+   | TacticAst.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
+       List.filter
+        (fun name ->
+          not (  List.exists (fun (name',_) -> name = Id name') params
+              || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
+        ) dom
+   | TacticAst.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
+       dom' @ domain_rev_of_term [] ty
+ in
+  rev_uniq domain_rev
 
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
@@ -434,6 +599,16 @@ sig
      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 *)
+    TacticAst.obj ->
+    (environment *                   (* new interpretation status *)
+     Cic.metasenv *                  (* new metasenv *)
+     Cic.obj *
+     CicUniv.universe_graph) list    (* disambiguated obj *)
 end
 
 module Make (C: Callbacks) =
@@ -468,9 +643,9 @@ module Make (C: Callbacks) =
            fun _ _ _ -> term))
         uris
 
-    let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv
+    let disambiguate_thing ~dbd ~context ~metasenv
       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
-      term
+      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
     =
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -478,14 +653,14 @@ module Make (C: Callbacks) =
           (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 ("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 term_dom));
+        (string_of_domain thing_dom));
       let current_dom =
         Environment.fold (fun item _ dom -> item :: dom) current_env []
       in
-      let todo_dom = domain_diff term_dom current_dom 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
@@ -519,11 +694,11 @@ module Make (C: Callbacks) =
                     (string_of_domain_item dom_item) len);
                   len
                 with No_choices _ -> 0)
-              term_dom
+              thing_dom
           in
           max_refinements := List.fold_left ( * ) 1 per_item_choices;
           actual_refinements := 0;
-          domain_size := List.length term_dom;
+          domain_size := List.length thing_dom;
           choices_avg :=
             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
         end
@@ -545,10 +720,11 @@ module Make (C: Callbacks) =
             current_env todo_dom 
         in
         try
-          let cic_term =
-            interpretate ~context:disambiguate_context ~env:filled_env term
+          let cic_thing =
+            interpretate_thing ~context:disambiguate_context ~env:filled_env
+             ~uri ~is_path:false thing
           in
-          let k,ugraph1 = refine metasenv context cic_term ugraph in
+          let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
             (k , ugraph1 )
         with
         | Try_again -> Uncertain,ugraph
@@ -559,8 +735,8 @@ module Make (C: Callbacks) =
         match todo_dom with
         | [] ->
             (match test_env current_env [] base_univ with
-            | Ok (term, metasenv),new_univ -> 
-                               [ current_env, metasenv, term, new_univ ]
+            | Ok (thing, metasenv),new_univ -> 
+               [ current_env, metasenv, thing, new_univ ]
             | Ko,_ | Uncertain,_ -> [])
         | item :: remaining_dom ->
             debug_print (sprintf "CHOOSED ITEM: %s"
@@ -574,9 +750,9 @@ module Make (C: Callbacks) =
                     Environment.add item codomain_item current_env
                   in
                   (match test_env new_env remaining_dom univ with
-                  | Ok (term, metasenv),new_univ ->
+                  | Ok (thing, metasenv),new_univ ->
                       (match remaining_dom with
-                      | [] -> [ new_env, metasenv, term, new_univ ]
+                      | [] -> [ new_env, metasenv, thing, new_univ ]
                       | _ -> aux new_env remaining_dom new_univ )@ 
                         filter univ tl
                   | Uncertain,new_univ ->
@@ -607,7 +783,7 @@ module Make (C: Callbacks) =
                          fst (Environment.find domain_item env)
                        in
                        (descr_of_domain_item domain_item, description))
-                     term_dom)
+                     thing_dom)
                  l
              in
              let choosed = C.interactive_interpretation_choice choices in
@@ -627,6 +803,19 @@ module Make (C: Callbacks) =
      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:CicAstPp.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:TacticAstPp.pp_obj ~domain_of_thing:domain_of_obj
+      ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
+      obj
   end
 
 module Trivial =