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 e93c54808298f14879396fbf637c3444c5bd775f..e11927d7d58fe6fb526a80f3347e7d56a5317727 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -35,9 +35,9 @@ module Ast = CicNotationPt
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
  int *
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
  int *

- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *

   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *

-  Token.flocation option * string Lazy.t * bool) list
+  Stdpp.location option * string Lazy.t * bool) list

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


@@ -47,7 +47,7 @@ type aliases = bool * DisambiguateTypes.environment
 type 'a disambiguator_input = string * int * 'a
 
 type domain = domain_tree list
 type 'a disambiguator_input = string * int * 'a
 
 type domain = domain_tree list

-and domain_tree = Node of Token.flocation list * domain_item * domain
+and domain_tree = Node of Stdpp.location list * domain_item * domain

 
 let rec string_of_domain =
  function
 
 let rec string_of_domain =
  function


@@ -103,10 +103,10 @@ 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
-  | Ko of Token.flocation option * string Lazy.t
-  | Uncertain of Token.flocation option * string Lazy.t
+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

 
 let refine_term metasenv context uri term ugraph ~localization_tbl =
 (*   if benchmark then incr actual_refinements; *)
 
 let refine_term metasenv context uri term ugraph ~localization_tbl =
 (*   if benchmark then incr actual_refinements; *)


@@ -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,21 +203,21 @@ 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
           do_branch' context args
         in

-        let (indtype_uri, indtype_no) =
+        let indtype_uri, indtype_no =

           if create_dummy_ids then
             (UriManager.uri_of_string "cic:/fake_indty.con", 0)
           else
           if create_dummy_ids then
             (UriManager.uri_of_string "cic:/fake_indty.con", 0)
           else


@@ -229,21 +229,112 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->

-                raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))

           | None ->
           | None ->

-              let fst_constructor =
-                match branches with
-                | ((head, _, _), _) :: _ -> head
-                | [] -> raise (Invalid_choice (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 _ ->
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
                   (indtype_uri, indtype_no)
               | Cic.Implicit _ ->
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->

-                raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+        in
+        let branches =
+         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
+               List.nth il indtype_no
+              with _ -> assert false
+             in
+              let rec count_prod t =
+                match CicReduction.whd [] t with
+                    Cic.Prod (_, _, t) -> 1 + (count_prod t)
+                  | _ -> 0 
+              in 
+              let rec sort branches cl =
+               match cl with
+                  [] ->
+                   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
+                       [] ->
+                        raise
+                         (Invalid_choice
+                          (Some loc, lazy ("Missing case: " ^ name)))
+                     | ((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
+                    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
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))


@@ -254,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


@@ -289,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


@@ -340,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 ->


@@ -386,23 +479,23 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                     (try
                       List.assoc s ids_to_uris, aux ~localize loc context term
                      with Not_found ->
                     (try
                       List.assoc s ids_to_uris, aux ~localize loc context term
                      with Not_found ->

-                       raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
+                       raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))

                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
           in
           (try 
             match cic with
             | Cic.Const (uri, []) ->
                   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 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


@@ -415,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 ->


@@ -430,10 +523,10 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
 *)
                 t
             | _ ->
 *)
                 t
             | _ ->

-              raise (Invalid_choice (lazy "??? Can this happen?"))
+              raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))

            with 
              CicEnvironment.CircularDependency _ -> 
            with 
              CicEnvironment.CircularDependency _ -> 

-               raise (Invalid_choice (lazy "Circular dependency in the environment"))))
+               raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))

     | CicNotationPt.Implicit -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
     | CicNotationPt.Implicit -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()


@@ -449,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


@@ -568,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) ->


@@ -634,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


@@ -689,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


@@ -735,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) ->


@@ -785,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 *)


@@ -812,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 ->


@@ -880,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)));
 (*


@@ -977,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 () =


@@ -990,7 +1128,7 @@ let foo () =
 in refine_profiler.HExtlib.profile foo ()
         with
         | Try_again msg -> Uncertain (None,msg), ugraph
 in refine_profiler.HExtlib.profile foo ()
         with
         | Try_again msg -> Uncertain (None,msg), ugraph

-        | Invalid_choice msg -> Ko (None,msg), ugraph
+        | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph

       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in


@@ -1180,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)


@@ -1198,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
 

+