exported disambiguate_thing

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 3d671cd7fd62b5b4fa800559dd80fb79b34a2939..e11927d7d58fe6fb526a80f3347e7d56a5317727 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -103,8 +103,8 @@ let descr_of_domain_item = function
  | Symbol (s, _) -> s
  | Num i -> string_of_int i
 
  | Symbol (s, _) -> s
  | Num i -> string_of_int i
 

-type 'a test_result =
-  | Ok of 'a * Cic.metasenv
+type ('a,'m) test_result =
+  | Ok of 'a * 'm

   | Ko of Stdpp.location option * string Lazy.t
   | Uncertain of Stdpp.location option * string Lazy.t
 
   | Ko of Stdpp.location option * string Lazy.t
   | Uncertain of Stdpp.location option * string Lazy.t
 


@@ -172,12 +172,12 @@ let find_in_context name context =
   in
   aux 1 context
 
   in
   aux 1 context
 

-let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast
+let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast

      ~localization_tbl
 =
   (* create_dummy_ids shouldbe used only for interpretating patterns *)
   assert (uri = None);
      ~localization_tbl
 =
   (* create_dummy_ids shouldbe used only for interpretating patterns *)
   assert (uri = None);

-  let rec aux ~localize loc (context: Cic.name list) = function
+  let rec aux ~localize loc context = function

     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         let res = aux ~localize loc context term in
          if localize then Cic.CicHash.add localization_tbl res loc;
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         let res = aux ~localize loc context term in
          if localize then Cic.CicHash.add localization_tbl res loc;


@@ -203,18 +203,18 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
         let cic_term = aux ~localize loc context term in
         let cic_outtype = aux_option ~localize loc context None outtype in
         let do_branch ((head, _, args), term) =
         let cic_term = aux ~localize loc context term in
         let cic_outtype = aux_option ~localize loc context None outtype in
         let do_branch ((head, _, args), term) =

-          let rec do_branch' context = function
-            | [] -> aux ~localize 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 ~localize loc context typ
-                in
-                Cic.Lambda (cic_name, typ, cic_body)
-          in
+         let rec do_branch' context = function
+           | [] -> aux ~localize 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 ~localize loc context typ
+               in
+               Cic.Lambda (cic_name, typ, cic_body)
+         in

           do_branch' context args
         in
         let indtype_uri, indtype_no =
           do_branch' context args
         in
         let indtype_uri, indtype_no =


@@ -231,12 +231,13 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
               | _ ->
                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
           | None ->
               | _ ->
                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
           | None ->

-              let fst_constructor =
-                match branches with
-                | ((head, _, _), _) :: _ -> head
-                | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined"))
+              let rec fst_constructor =
+                function
+                   (Ast.Pattern (head, _, _), _) :: _ -> head
+                 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
+                 | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))

               in
               in

-              (match resolve env (Id fst_constructor) () with
+              (match resolve env (Id (fst_constructor branches)) () with

               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
                   (indtype_uri, indtype_no)
               | Cic.Implicit _ ->
               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
                   (indtype_uri, indtype_no)
               | Cic.Implicit _ ->


@@ -246,7 +247,15 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
         in
         let branches =
                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
         in
         let branches =

-         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
+         if create_dummy_ids then
+          List.map
+           (function
+               Ast.Wildcard,term -> ("wildcard",None,[]), term
+             | Ast.Pattern _,_ ->
+                raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
+           ) branches
+         else
+         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with

             Cic.InductiveDefinition (il,_,leftsno,_) ->
              let _,_,_,cl =
               try
             Cic.InductiveDefinition (il,_,leftsno,_) ->
              let _,_,_,cl =
               try


@@ -261,14 +270,31 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
               let rec sort branches cl =
                match cl with
                   [] ->
               let rec sort branches cl =
                match cl with
                   [] ->

-                   if branches = [] then []
-                   else
-                    raise (Invalid_choice
-                     (Some loc,
-                      lazy
-                       ("Unrecognized constructors: " ^
-                        String.concat " "
-                         (List.map (fun ((head,_,_),_) -> head) branches))))
+                   let rec analyze unused unrecognized useless =
+                    function
+                       [] ->
+                        if unrecognized != [] then
+                         raise (Invalid_choice
+                          (Some loc,
+                           lazy
+                            ("Unrecognized constructors: " ^
+                             String.concat " " unrecognized)))
+                        else if useless > 0 then
+                         raise (Invalid_choice
+                          (Some loc,
+                           lazy
+                            ("The last " ^ string_of_int useless ^
+                             "case" ^ if useless > 1 then "s are" else " is" ^
+                             " unused")))
+                        else
+                         []
+                     | (Ast.Wildcard,_)::tl when not unused ->
+                         analyze true unrecognized useless tl
+                     | (Ast.Pattern (head,_,_),_)::tl when not unused ->
+                         analyze unused (head::unrecognized) useless tl
+                     | _::tl -> analyze unused unrecognized (useless + 1) tl
+                   in
+                    analyze false [] 0 branches

                 | (name,ty)::cltl ->
                    let rec find_and_remove =
                     function
                 | (name,ty)::cltl ->
                    let rec find_and_remove =
                     function


@@ -276,21 +302,36 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                         raise
                          (Invalid_choice
                           (Some loc, lazy ("Missing case: " ^ name)))
                         raise
                          (Invalid_choice
                           (Some loc, lazy ("Missing case: " ^ name)))

-                     | ((name',_,_),_) as branch :: tl when name = name' ->
-                        branch,tl
+                     | ((Ast.Wildcard, _) as branch :: _) as branches ->
+                         branch, branches
+                     | (Ast.Pattern (name',_,_),_) as branch :: tl
+                        when name = name' ->
+                         branch,tl

                      | branch::tl ->
                         let found,rest = find_and_remove tl in
                          found, branch::rest
                    in
                     let branch,tl = find_and_remove branches in
                      | branch::tl ->
                         let found,rest = find_and_remove tl in
                          found, branch::rest
                    in
                     let branch,tl = find_and_remove branches in

-                    let (_,_,args),_ = branch in
-                     if List.length args = count_prod ty - leftsno then
-                      branch::sort tl cltl
-                     else
-                      raise
-                       (Invalid_choice
-                        (Some loc,
-                          lazy ("Wrong number of arguments for " ^ name)))
+                    match branch with
+                       Ast.Pattern (name,y,args),term ->
+                        if List.length args = count_prod ty - leftsno then
+                         ((name,y,args),term)::sort tl cltl
+                        else
+                         raise
+                          (Invalid_choice
+                           (Some loc,
+                             lazy ("Wrong number of arguments for " ^ name)))
+                     | Ast.Wildcard,term ->
+                        let rec mk_lambdas =
+                         function
+                            0 -> term
+                          | n ->
+                             CicNotationPt.Binder
+                              (`Lambda, (CicNotationPt.Ident ("_", None), None),
+                                mk_lambdas (n - 1))
+                        in
+                         (("wildcard",None,[]),
+                          mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl

               in
                sort branches cl
           | _ -> assert false
               in
                sort branches cl
           | _ -> assert false


@@ -304,13 +345,13 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.LetIn ((name, typ), def, body) ->
         let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in
     | CicNotationPt.LetIn ((name, typ), def, body) ->
         let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in

-        let cic_def =
+        let cic_typ =

           match typ with
           match typ with

-          | None -> cic_def
-          | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
+          | None -> Cic.Implicit (Some `Type)
+          | Some t -> aux ~localize loc context t

         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in

-        Cic.LetIn (cic_name, cic_def, cic_body)
+        Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)

     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left
     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left


@@ -339,6 +380,8 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                 if localize then
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
                 if localize then
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->

+                     (* since we avoid the letin, the context has no
+                      * recfuns in it *)

                      let l' = List.map (aux ~localize loc context) l in
                       `AvoidLetIn (n,l')
                   | _ -> assert false
                      let l' = List.map (aux ~localize loc context) l in
                       `AvoidLetIn (n,l')
                   | _ -> assert false


@@ -390,9 +433,9 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                Cic.CoFix (n,coinductiveFuns)
         in
          let counter = ref ~-1 in
                Cic.CoFix (n,coinductiveFuns)
         in
          let counter = ref ~-1 in

-         let build_term funs (var,_,_,_) t =
+         let build_term funs (var,_,ty,_) t =

           incr counter;
           incr counter;

-          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)

          in
           (match cic_body with
               `AvoidLetInNoAppl n ->
          in
           (match cic_body with
               `AvoidLetInNoAppl n ->


@@ -443,16 +486,16 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
           (try 
             match cic with
             | Cic.Const (uri, []) ->
           (try 
             match cic with
             | Cic.Const (uri, []) ->

-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                 let uris = CicUtil.params_of_obj o in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
                 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 o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                 let uris = CicUtil.params_of_obj o in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                (try
                 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 o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                  let uris = CicUtil.params_of_obj o in
                  Cic.MutInd (uri, i, mk_subst uris)
                 with
                  let uris = CicUtil.params_of_obj o in
                  Cic.MutInd (uri, i, mk_subst uris)
                 with


@@ -465,7 +508,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                   (*here the explicit_named_substituion is assumed to be of length 0 *)
                   Cic.MutInd (uri,i,[]))
             | Cic.MutConstruct (uri, i, j, []) ->
                   (*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 o,_ = CicEnvironment.get_obj CicUniv.oblivion_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 ->
                 let uris = CicUtil.params_of_obj o in
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->


@@ -499,11 +542,11 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)

-    | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)

     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)

-  and aux_option ~localize loc (context: Cic.name list) annotation = function
+  and aux_option ~localize loc context annotation = function

     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in


@@ -618,6 +661,16 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
       | Some bo,_ ->
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))
       | Some bo,_ ->
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))

+;;
+
+let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
+     ~localization_tbl
+=
+  let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
+interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
+~localization_tbl
+;;
+

           
 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.AttributedTerm (`Loc loc, term) ->
           
 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.AttributedTerm (`Loc loc, term) ->


@@ -684,20 +737,25 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.Case (term, indty_ident, outtype, branches) ->
       let term_dom = domain_of_term ~loc ~context term in
       let outtype_dom = domain_of_term_option ~loc ~context outtype in
   | Ast.Case (term, indty_ident, outtype, branches) ->
       let term_dom = domain_of_term ~loc ~context term in
       let outtype_dom = domain_of_term_option ~loc ~context outtype in

-      let get_first_constructor = function
+      let rec get_first_constructor = function

         | [] -> []
         | [] -> []

-        | ((head, _, _), _) :: _ -> [ Node ([loc], 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 -> dom @ domain_of_term ~loc ~context:cont typ)))
-            (context, []) args
-        in
-        domain_of_term ~loc ~context:term_context term @ args_domain
+        | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
+        | _ :: tl -> get_first_constructor tl in
+      let do_branch =
+       function
+          Ast.Pattern (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 -> dom @ domain_of_term ~loc ~context:cont typ)))
+               (context, []) args
+           in
+            domain_of_term ~loc ~context:term_context term @ args_domain
+        | Ast.Wildcard, term ->
+            domain_of_term ~loc ~context term

       in
       let branches_dom =
         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
       in
       let branches_dom =
         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in


@@ -739,6 +797,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))

+            @ dom

             @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs
             @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs


@@ -785,6 +844,7 @@ let domain_of_term ~context term =
  uniq_domain (domain_of_term ~context term)
 
 let domain_of_obj ~context ast =
  uniq_domain (domain_of_term ~context term)
 
 let domain_of_obj ~context ast =

+ let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in

  assert (context = []);
   match ast with
    | Ast.Theorem (_,_,ty,bo) ->
  assert (context = []);
   match ast with
    | Ast.Theorem (_,_,ty,bo) ->


@@ -835,6 +895,12 @@ let domain_of_obj ~context ast =
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 

+let domain_of_term ~context term = 
+ let context = 
+   List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context 
+ in
+ domain_of_term ~context term
+

   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)


@@ -862,6 +928,33 @@ let domain_diff dom1 dom2 =
 
 module type Disambiguator =
 sig
 
 module type Disambiguator =
 sig

+  val disambiguate_thing:
+    dbd:HSql.dbd ->
+    context:'context ->
+    metasenv:'metasenv ->
+    initial_ugraph:'ugraph ->
+    aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+    universe:DisambiguateTypes.codomain_item list
+             DisambiguateTypes.Environment.t option ->
+    uri:'uri ->
+    pp_thing:('ast_thing -> string) ->
+    domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+    interpretate_thing:(context:'context ->
+                        env:DisambiguateTypes.codomain_item
+                            DisambiguateTypes.Environment.t ->
+                        uri:'uri ->
+                        is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
+    refine_thing:('metasenv ->
+                  'context ->
+                  'uri ->
+                  'raw_thing ->
+                  'ugraph -> localization_tbl:'cichash -> ('refined_thing,
+                  'metasenv) test_result * 'ugraph) ->
+    localization_tbl:'cichash ->
+    string * int * 'ast_thing ->
+    ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
+     list * 'metasenv * 'refined_thing * 'ugraph)
+    list * bool

   val disambiguate_term :
     ?fresh_instances:bool ->
     dbd:HSql.dbd ->
   val disambiguate_term :
     ?fresh_instances:bool ->
     dbd:HSql.dbd ->


@@ -930,18 +1023,14 @@ module Make (C: Callbacks) =
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv

-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+      ~initial_ugraph ~aliases ~universe

       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 

+      ~localization_tbl

       (thing_txt,thing_txt_prefix_len,thing)
     =
       debug_print (lazy "DISAMBIGUATE INPUT");
       (thing_txt,thing_txt_prefix_len,thing)
     =
       debug_print (lazy "DISAMBIGUATE INPUT");

-      let disambiguate_context =  (* cic context -> disambiguate context *)
-        List.map
-          (function None -> Cic.Anonymous | Some (name, _) -> name)
-          context
-      in

       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));

-      let thing_dom = domain_of_thing ~context:disambiguate_context thing in
+      let thing_dom = domain_of_thing ~context thing in

       debug_print
        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
 (*
       debug_print
        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
 (*


@@ -1027,9 +1116,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
               aux (aux env l) tl in
         let filled_env = aux aliases todo_dom in
         try
               aux (aux env l) tl in
         let filled_env = aux aliases todo_dom in
         try

-          let localization_tbl = Cic.CicHash.create 503 in

           let cic_thing =
           let cic_thing =

-            interpretate_thing ~context:disambiguate_context ~env:filled_env
+            interpretate_thing ~context ~env:filled_env

              ~uri ~is_path:false thing ~localization_tbl
           in
 let foo () =
              ~uri ~is_path:false thing ~localization_tbl
           in
 let foo () =


@@ -1230,17 +1318,19 @@ in refine_profiler.HExtlib.profile foo ()
         failwith "Disambiguate: circular dependency"
 
     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
         failwith "Disambiguate: circular dependency"
 
     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv

-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe 
+      ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe 

       (text,prefix_len,term)
     =
       let term =
         if fresh_instances then CicNotationUtil.freshen_term term else term
       in
       (text,prefix_len,term)
     =
       let term =
         if fresh_instances then CicNotationUtil.freshen_term term else term
       in

+      let localization_tbl = Cic.CicHash.create 503 in

       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_term
         ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
         ~refine_thing:refine_term (text,prefix_len,term)
       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_term
         ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
         ~refine_thing:refine_term (text,prefix_len,term)

+        ~localization_tbl

 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
      (text,prefix_len,obj)
 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
      (text,prefix_len,obj)


@@ -1248,9 +1338,14 @@ in refine_profiler.HExtlib.profile foo ()
       let obj =
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
       let obj =
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in

+      let localization_tbl = Cic.CicHash.create 503 in

       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj

+        ~initial_ugraph:CicUniv.empty_ugraph

         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj

+        ~localization_tbl

         (text,prefix_len,obj)
         (text,prefix_len,obj)

+

   end
 
   end
 

+