Very experimental commit: the type of the source is now required in LetIns

[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 bfeb65d37ea2d39888abb3303026ead0ad5d62e7..d58dc9854bceef447083e2ff628bfe99ef6eee91 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -30,9 +30,14 @@ open Printf
 open DisambiguateTypes
 open UriManager
 
 open DisambiguateTypes
 open UriManager
 

+module Ast = CicNotationPt
+

 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of

- int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Token.flocation option * string Lazy.t) list
+ int *
+ ((Stdpp.location list * string * string) list *
+  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) 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 *)


@@ -41,6 +46,46 @@ exception Try_again of string Lazy.t
 type aliases = bool * DisambiguateTypes.environment
 type 'a disambiguator_input = string * int * 'a
 
 type aliases = bool * DisambiguateTypes.environment
 type 'a disambiguator_input = string * int * 'a
 

+type domain = domain_tree list
+and domain_tree = Node of Stdpp.location list * domain_item * domain
+
+let rec string_of_domain =
+ function
+    [] -> ""
+  | Node (_,domain_item,l)::tl ->
+     DisambiguateTypes.string_of_domain_item domain_item ^
+      " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl
+
+let rec filter_map_domain f =
+ function
+    [] -> []
+  | Node (locs,domain_item,l)::tl ->
+     match f locs domain_item with
+        None -> filter_map_domain f l @ filter_map_domain f tl
+      | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl
+
+let rec map_domain f =
+ function
+    [] -> []
+  | Node (locs,domain_item,l)::tl ->
+     f locs domain_item :: map_domain f l @ map_domain f tl
+
+let uniq_domain dom =
+ let rec aux seen =
+  function
+     [] -> seen,[]
+   | Node (locs,domain_item,l)::tl ->
+      if List.mem domain_item seen then
+       let seen,l = aux seen l in
+       let seen,tl = aux seen tl in
+        seen, l @ tl
+      else
+       let seen,l = aux (domain_item::seen) l in
+       let seen,tl = aux seen tl in
+        seen, Node (locs,domain_item,l)::tl
+ in
+  snd (aux [] dom)
+

 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 


@@ -60,8 +105,8 @@ let descr_of_domain_item = function
 
 type 'a test_result =
   | Ok of 'a * Cic.metasenv
 
 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
+  | 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; *)


@@ -127,9 +172,10 @@ let find_in_context name context =
   in
   aux 1 context
 
   in
   aux 1 context
 

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

      ~localization_tbl
 =
      ~localization_tbl
 =

+  (* create_dummy_ids shouldbe used only for interpretating patterns *)

   assert (uri = None);
   let rec aux ~localize loc (context: Cic.name list) = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
   assert (uri = None);
   let rec aux ~localize loc (context: Cic.name list) = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->


@@ -157,21 +203,24 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
         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

           match indty_ident with
           | Some (indty_ident, _) ->
              (match resolve env (Id indty_ident) () with
           match indty_ident with
           | Some (indty_ident, _) ->
              (match resolve env (Id indty_ident) () with


@@ -180,21 +229,112 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                  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.empty_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))


@@ -205,13 +345,13 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | 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


@@ -222,14 +362,14 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
         let cic_body =
          let unlocalized_body = aux ~localize:false loc context' body in
          match unlocalized_body with
         let cic_body =
          let unlocalized_body = aux ~localize:false loc context' body in
          match unlocalized_body with

-            Cic.Rel 1 -> `AvoidLetInNoAppl
-          | Cic.Appl (Cic.Rel 1::l) ->
+            Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
+          | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->

              (try
                let l' =
                 List.map
                  (function t ->
                    let t',subst,metasenv =
              (try
                let l' =
                 List.map
                  (function t ->
                    let t',subst,metasenv =

-                    CicMetaSubst.delift_rels [] [] 1 t
+                    CicMetaSubst.delift_rels [] [] (List.length defs) t

                    in
                     assert (subst=[]);
                     assert (metasenv=[]);
                    in
                     assert (subst=[]);
                     assert (metasenv=[]);


@@ -241,10 +381,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
                      let l' = List.map (aux ~localize loc context) l in
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
                      let l' = List.map (aux ~localize loc context) l in

-                      `AvoidLetIn l'
+                      `AvoidLetIn (n,l')

                   | _ -> assert false
                 else
                   | _ -> assert false
                 else

-                 `AvoidLetIn l'
+                 `AvoidLetIn (n,l')

               with
                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                 if localize then
               with
                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                 if localize then


@@ -279,42 +419,32 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
               (name, decr_idx, cic_type, cic_body))
             defs
         in
               (name, decr_idx, cic_type, cic_body))
             defs
         in

-        let counter = ref ~-1 in
-        let build_term funs =
-          (* this is the body of the fold_right function below. Rationale: Fix
-           * and CoFix cases differs only in an additional index in the
-           * inductiveFun list, see Cic.term *)
-          match kind with
-          | `Inductive ->
-              (fun (var, _, _, _) cic ->
-                incr counter;
-                let fix = Cic.Fix (!counter,funs) in
-                 match cic with
-                    `Recipe (`AddLetIn cic) ->
-                      `Term (Cic.LetIn (Cic.Name var, fix, cic))
-                  | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l))
-                  | `Recipe `AvoidLetInNoAppl -> `Term fix
-                  | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t)))
+        let fix_or_cofix n =
+         match kind with
+            `Inductive -> Cic.Fix (n,inductiveFuns)

           | `CoInductive ->
           | `CoInductive ->

-              let funs =
-                List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
+              let coinductiveFuns =
+                List.map
+                 (fun (name, _, typ, body) -> name, typ, body)
+                 inductiveFuns

               in
               in

-              (fun (var, _, _, _) cic ->
-                incr counter;
-                let cofix = Cic.CoFix (!counter,funs) in
-                 match cic with
-                    `Recipe (`AddLetIn cic) ->
-                      `Term (Cic.LetIn (Cic.Name var, cofix, cic))
-                  | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l))
-                  | `Recipe `AvoidLetInNoAppl -> `Term cofix
-                  | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t)))
+               Cic.CoFix (n,coinductiveFuns)

         in
         in

-         (match
-           List.fold_right (build_term inductiveFuns) inductiveFuns
-            (`Recipe cic_body)
-          with
-             `Recipe _ -> assert false
-           | `Term t -> t)
+         let counter = ref ~-1 in
+         let build_term funs (var,_,ty,_) t =
+          incr counter;
+          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
+         in
+          (match cic_body with
+              `AvoidLetInNoAppl n ->
+                let n' = List.length inductiveFuns - n in
+                 fix_or_cofix n'
+            | `AvoidLetIn (n,l) ->
+                let n' = List.length inductiveFuns - n in
+                 Cic.Appl (fix_or_cofix n'::l)
+            | `AddLetIn cic_body ->         
+                List.fold_right (build_term inductiveFuns) inductiveFuns
+                 cic_body)

     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
     | CicNotationPt.Ident (name, subst)
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
     | CicNotationPt.Ident (name, subst)


@@ -347,7 +477,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                     (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
                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
           in


@@ -391,10 +521,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
 *)
                 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 ()


@@ -424,7 +554,8 @@ let interpretate_path ~context path =
  let localization_tbl = Cic.CicHash.create 23 in
   (* here we are throwing away useful localization informations!!! *)
   fst (
  let localization_tbl = Cic.CicHash.create 23 in
   (* here we are throwing away useful localization informations!!! *)
   fst (

-   interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true
+   interpretate_term ~create_dummy_ids:true 
+    ~context ~env:Environment.empty ~uri:None ~is_path:true

     path ~localization_tbl, localization_tbl)
 
 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
     path ~localization_tbl, localization_tbl)
 
 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =


@@ -529,103 +660,115 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))
           
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))
           

-
-  (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
-let rev_uniq =
-  let module SortedItem =
-    struct
-      type t = DisambiguateTypes.domain_item
-      let compare = Pervasives.compare
-    end
-  in
-  let module Map = Map.Make (SortedItem) in
-  fun l ->
-    let rev_l = List.rev l in
-    let (members, uniq_rev_l) =
-      List.fold_left
-        (fun (members, rev_l) (loc,elt) ->
-          try 
-            let locs = Map.find elt members in
-            if List.mem loc locs then
-              members, rev_l
-            else
-              Map.add elt (loc::locs) members, rev_l
-          with
-          | Not_found -> Map.add elt [loc] members, elt :: rev_l)
-        (Map.empty, []) rev_l
-    in
-    List.rev_map 
-      (fun e -> try Map.find e members,e with Not_found -> assert false)
-      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 = HExtlib.dummy_floc) context = function
-  | CicNotationPt.AttributedTerm (`Loc loc, term) ->
-     domain_rev_of_term ~loc context term
-  | CicNotationPt.AttributedTerm (_, term) ->
-      domain_rev_of_term ~loc context term
-  | CicNotationPt.Appl terms ->
-      List.fold_left
-       (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
-  | CicNotationPt.Binder (kind, (var, typ), body) ->
-      let kind_dom =
-        match kind with
-        | `Exists -> [ loc, Symbol ("exists", 0) ]
-        | _ -> []
+let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
+  | Ast.AttributedTerm (`Loc loc, term) ->
+     domain_of_term ~loc ~context term
+  | Ast.AttributedTerm (_, term) ->
+      domain_of_term ~loc ~context term
+  | Ast.Symbol (symbol, instance) ->
+      [ Node ([loc], Symbol (symbol, instance), []) ]
+      (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
+  | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
+  | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
+     ->
+      let args_dom =
+        List.fold_right
+          (fun term acc -> domain_of_term ~loc ~context term @ acc)
+          args [] in
+      let loc =
+       match hd with
+          Ast.AttributedTerm (`Loc loc,_)  -> loc
+        | _ -> loc

       in
       in

-      let type_dom = domain_rev_of_term_option ~loc context typ in
-      let body_dom =
-        domain_rev_of_term ~loc
-          (CicNotationUtil.cic_name_of_name var :: context) body
+       [ Node ([loc], Symbol (symbol, instance), args_dom) ]
+  | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
+  | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
+      let args_dom =
+        List.fold_right
+          (fun term acc -> domain_of_term ~loc ~context term @ acc)
+          args [] in
+      let loc =
+       match hd with
+          Ast.AttributedTerm (`Loc loc,_)  -> loc
+        | _ -> loc

       in
       in

-      body_dom @ type_dom @ kind_dom
-  | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
-      let term_dom = domain_rev_of_term ~loc context term in
-      let outtype_dom = domain_rev_of_term_option loc context outtype in
-      let get_first_constructor = function
+      (try
+        (* the next line can raise Not_found *)
+        ignore(find_in_context name context);
+        if subst <> None then
+          Ast.fail loc "Explicit substitutions not allowed here"
+        else
+          args_dom
+      with Not_found ->
+        (match subst with
+        | None -> [ Node ([loc], Id name, args_dom) ]
+        | Some subst ->
+            let terms =
+              List.fold_left
+                (fun dom (_, term) ->
+                  let dom' = domain_of_term ~loc ~context term in
+                  dom @ dom')
+                [] subst in
+            [ Node ([loc], Id name, terms @ args_dom) ]))
+  | Ast.Appl terms ->
+      List.fold_right
+        (fun term acc -> domain_of_term ~loc ~context term @ acc)
+        terms []
+  | Ast.Binder (kind, (var, typ), body) ->
+      let type_dom = domain_of_term_option ~loc ~context typ in
+      let body_dom =
+        domain_of_term ~loc
+          ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
+      (match kind with
+      | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
+      | _ -> type_dom @ body_dom)
+  | 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 rec get_first_constructor = function

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

-        | ((head, _, _), _) :: _ -> [ 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 -> domain_rev_of_term ~loc cont typ @ dom)))
-            (context, []) args
-        in
-        args_domain @ domain_rev_of_term ~loc term_context term
+        | (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 =
       in
       let branches_dom =

-        List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
-      in
-      branches_dom @ outtype_dom @ term_dom @
+        List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in

       (match indty_ident with
        | None -> get_first_constructor branches
       (match indty_ident with
        | None -> get_first_constructor branches

-       | Some (ident, _) -> [ loc, Id ident ])
-  | CicNotationPt.Cast (term, ty) ->
-      let term_dom = domain_rev_of_term ~loc context term in
-      let ty_dom = domain_rev_of_term ~loc context ty in
-      ty_dom @ term_dom
-  | CicNotationPt.LetIn ((var, typ), body, where) ->
-      let body_dom = domain_rev_of_term ~loc context body in
-      let type_dom = domain_rev_of_term_option loc context typ in
+       | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
+      @ term_dom @ outtype_dom @ branches_dom
+  | Ast.Cast (term, ty) ->
+      let term_dom = domain_of_term ~loc ~context term in
+      let ty_dom = domain_of_term ~loc ~context ty in
+      term_dom @ ty_dom
+  | Ast.LetIn ((var, typ), body, where) ->
+      let body_dom = domain_of_term ~loc ~context body in
+      let type_dom = domain_of_term_option ~loc ~context typ in

       let where_dom =
       let where_dom =

-        domain_rev_of_term ~loc
-          (CicNotationUtil.cic_name_of_name var :: context) where
-      in
-      where_dom @ type_dom @ body_dom
-  | CicNotationPt.LetRec (kind, defs, where) ->
+        domain_of_term ~loc
+          ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
+      body_dom @ type_dom @ where_dom
+  | Ast.LetRec (kind, defs, where) ->

       let add_defs context =
         List.fold_left
           (fun acc (_, (var, _), _, _) ->
             CicNotationUtil.cic_name_of_name var :: acc
           ) context defs in
       let add_defs context =
         List.fold_left
           (fun acc (_, (var, _), _, _) ->
             CicNotationUtil.cic_name_of_name var :: acc
           ) context defs in

-      let where_dom = domain_rev_of_term ~loc (add_defs context) where in
+      let where_dom = domain_of_term ~loc ~context:(add_defs context) where in

       let defs_dom =
         List.fold_left
           (fun dom (params, (_, typ), body, _) ->
       let defs_dom =
         List.fold_left
           (fun dom (params, (_, typ), body, _) ->


@@ -635,112 +778,108 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
                 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
                 context params)
             in
                 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
                 context params)
             in

-            domain_rev_of_term ~loc context' body @
-            domain_rev_of_term_option ~loc context typ @

             List.rev
              (snd
                (List.fold_left
                 (fun (context,res) (var,ty) ->
                   CicNotationUtil.cic_name_of_name var :: context,
             List.rev
              (snd
                (List.fold_left
                 (fun (context,res) (var,ty) ->
                   CicNotationUtil.cic_name_of_name var :: context,

-                  res @ domain_rev_of_term_option ~loc context ty)
+                  domain_of_term_option ~loc ~context ty @ res)

                 (add_defs context,[]) params))
                 (add_defs context,[]) params))

+            @ domain_of_term_option ~loc ~context:context' typ
+            @ domain_of_term ~loc ~context:context' body

           ) [] defs
       in
           ) [] defs
       in

-      where_dom @ defs_dom
-  | CicNotationPt.Ident (name, subst) ->
+      defs_dom @ where_dom
+  | Ast.Ident (name, subst) ->

       (try
         (* the next line can raise Not_found *)
         ignore(find_in_context name context);
         if subst <> None then
       (try
         (* the next line can raise Not_found *)
         ignore(find_in_context name context);
         if subst <> None then

-          CicNotationPt.fail loc "Explicit substitutions not allowed here"
+          Ast.fail loc "Explicit substitutions not allowed here"

         else
           []
       with Not_found ->
         (match subst with
         else
           []
       with Not_found ->
         (match subst with

-        | None -> [loc, Id name]
+        | None -> [ Node ([loc], Id name, []) ]

         | Some subst ->
         | Some subst ->

-            List.fold_left
-              (fun dom (_, term) ->
-                let dom' = domain_rev_of_term ~loc context term in
-                dom' @ dom)
-              [loc, Id name] subst))
-  | CicNotationPt.Uri _ -> []
-  | CicNotationPt.Implicit -> []
-  | CicNotationPt.Num (num, i) -> [loc, Num i ]
-  | CicNotationPt.Meta (index, local_context) ->
+            let terms =
+              List.fold_left
+                (fun dom (_, term) ->
+                  let dom' = domain_of_term ~loc ~context term in
+                  dom @ dom')
+                [] subst in
+            [ Node ([loc], Id name, terms) ]))
+  | Ast.Uri _ -> []
+  | Ast.Implicit -> []
+  | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
+  | Ast.Meta (index, local_context) ->

       List.fold_left
       List.fold_left

-       (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
-        local_context
-  | CicNotationPt.Sort _ -> []
-  | CicNotationPt.Symbol (symbol, instance) -> [loc, Symbol (symbol, instance) ]
-  | CicNotationPt.UserInput
-  | CicNotationPt.Literal _
-  | CicNotationPt.Layout _
-  | CicNotationPt.Magic _
-  | CicNotationPt.Variable _ -> assert false
+       (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
+       [] local_context
+  | Ast.Sort _ -> []
+  | Ast.UserInput
+  | Ast.Literal _
+  | Ast.Layout _
+  | Ast.Magic _
+  | Ast.Variable _ -> assert false

 
 

-and domain_rev_of_term_option ~loc context = function
+and domain_of_term_option ~loc ~context = function

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

-  | Some t -> domain_rev_of_term ~loc context t
+  | Some t -> domain_of_term ~loc ~context t

 
 

-let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast)
+let domain_of_term ~context term = 
+ uniq_domain (domain_of_term ~context term)

 
 let domain_of_obj ~context ast =
  assert (context = []);
 
 let domain_of_obj ~context ast =
  assert (context = []);

- let domain_rev =

   match ast with
   match ast with

-   | CicNotationPt.Theorem (_,_,ty,bo) ->
-      (match bo with
+   | Ast.Theorem (_,_,ty,bo) ->
+      domain_of_term [] ty
+      @ (match bo with

           None -> []
           None -> []

-        | Some bo -> domain_rev_of_term [] bo) @
-      domain_rev_of_term [] ty
-   | CicNotationPt.Inductive (params,tyl) ->
-      let dom =
-       List.flatten (
-        List.rev_map
-         (fun (_,_,ty,cl) ->
-           List.flatten (
-            List.rev_map
-             (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
-            domain_rev_of_term [] ty) tyl) in
-      let dom = 
+        | Some bo -> domain_of_term [] bo)
+   | Ast.Inductive (params,tyl) ->
+      let context, dom = 

        List.fold_left
        List.fold_left

-        (fun dom (_,ty) ->
+        (fun (context, dom) (var, ty) ->
+          let context' = CicNotationUtil.cic_name_of_name var :: context in

           match ty with
           match ty with

-             None -> dom
-           | Some ty -> domain_rev_of_term [] ty @ dom
-        ) dom params
-      in
-       List.filter
-        (fun (_,name) ->
-          not (  List.exists (fun (name',_) ->
-                  match CicNotationUtil.cic_name_of_name name' with
-                     Cic.Anonymous -> false
-                   | Cic.Name name' -> name = Id name') params
-              || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
-        ) dom
-   | CicNotationPt.Record (params,_,ty,fields) ->
-      let dom =
-       List.flatten
-        (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in
-      let dom =
+             None -> context', dom
+           | Some ty -> context', dom @ domain_of_term context ty
+        ) ([], []) params in
+      let context_w_types =
+        List.rev_map
+          (fun (var, _, _, _) -> Cic.Name var) tyl
+        @ context in
+      dom
+      @ List.flatten (
+         List.map
+          (fun (_,_,ty,cl) ->
+            domain_of_term context ty
+            @ List.flatten (
+               List.map
+                (fun (_,ty) -> domain_of_term context_w_types ty) cl))
+                tyl)
+   | CicNotationPt.Record (params,var,ty,fields) ->
+      let context, dom = 

        List.fold_left
        List.fold_left

-        (fun dom (_,ty) ->
+        (fun (context, dom) (var, ty) ->
+          let context' = CicNotationUtil.cic_name_of_name var :: context in

           match ty with
           match ty with

-             None -> dom
-           | Some ty -> domain_rev_of_term [] ty @ dom
-        ) (dom @ domain_rev_of_term [] ty) params
-      in
-       List.filter
-        (fun (_,name) ->
-          not (  List.exists (fun (name',_) ->
-                  match CicNotationUtil.cic_name_of_name name' with
-                     Cic.Anonymous -> false
-                   | Cic.Name name' -> name = Id name') params
-              || List.exists (fun (name',_,_,_) -> name = Id name') fields)
-        ) dom
- in
-  rev_uniq domain_rev
+             None -> context', dom
+           | Some ty -> context', dom @ domain_of_term context ty
+        ) ([], []) params in
+      let context_w_types = Cic.Name var :: context in
+      dom
+      @ domain_of_term context ty
+      @ snd
+         (List.fold_left
+          (fun (context,res) (name,ty,_,_) ->
+            Cic.Name name::context, res @ domain_of_term context ty
+          ) (context_w_types,[]) fields)
+
+let domain_of_obj ~context obj = 
+ uniq_domain (domain_of_obj ~context obj)

 
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =


@@ -759,13 +898,19 @@ let domain_diff dom1 dom2 =
        | item -> elt = item
      ) dom2
   in
        | item -> elt = item
      ) dom2
   in

-  List.filter (fun (_,elt) -> not (is_in_dom2 elt)) dom1
+   let rec aux =
+    function
+       [] -> []
+     | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
+     | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
+   in
+    aux dom1

 
 module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->
 
 module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->

-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->

     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 


@@ -780,11 +925,11 @@ sig
 
   val disambiguate_obj :
     ?fresh_instances:bool ->
 
   val disambiguate_obj :
     ?fresh_instances:bool ->

-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->

     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)

-    CicNotationPt.obj disambiguator_input ->
+    CicNotationPt.term CicNotationPt.obj disambiguator_input ->

     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *


@@ -843,8 +988,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
       in
       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
       in
       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
       let thing_dom = domain_of_thing ~context:disambiguate_context thing in

-      debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"
-        (string_of_domain (List.map snd thing_dom))));
+      debug_print
+       (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));

 (*
       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
         (DisambiguatePp.pp_environment aliases)));
 (*
       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
         (DisambiguatePp.pp_environment aliases)));


@@ -852,9 +997,10 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
         (match universe with None -> "None" | Some _ -> "Some _")));
 *)
       let current_dom =
         (match universe with None -> "None" | Some _ -> "Some _")));
 *)
       let current_dom =

-        Environment.fold (fun item _ dom -> item :: dom) aliases []
-      in
+        Environment.fold (fun item _ dom -> item :: dom) aliases [] in

       let todo_dom = domain_diff thing_dom current_dom in
       let todo_dom = domain_diff thing_dom current_dom in

+      debug_print
+       (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));

       (* (2) lookup function for any item (Id/Symbol/Num) *)
       let lookup_choices =
         fun item ->
       (* (2) lookup function for any item (Id/Symbol/Num) *)
       let lookup_choices =
         fun item ->


@@ -863,8 +1009,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
               match item with
               | Id id -> choices_of_id dbd id
               | Symbol (symb, _) ->
               match item with
               | Id id -> choices_of_id dbd id
               | Symbol (symb, _) ->

-                  List.map DisambiguateChoices.mk_choice
+                 (try
+                   List.map DisambiguateChoices.mk_choice

                     (TermAcicContent.lookup_interpretations symb)
                     (TermAcicContent.lookup_interpretations symb)

+                  with
+                   TermAcicContent.Interpretation_not_found -> [])

               | Num instance ->
                   DisambiguateChoices.lookup_num_choices ()
             in
               | Num instance ->
                   DisambiguateChoices.lookup_num_choices ()
             in


@@ -910,16 +1059,19 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
       (* (3) test an interpretation filling with meta uninterpreted identifiers
        *)
       let test_env aliases todo_dom ugraph = 
       (* (3) test an interpretation filling with meta uninterpreted identifiers
        *)
       let test_env aliases todo_dom ugraph = 

-        let filled_env =
-          List.fold_left
-            (fun env (_,item) ->
-               Environment.add item
-               ("Implicit",
-                 (match item with
-                    | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
-                    | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
-            aliases todo_dom 
-        in
+        let rec aux env = function
+          | [] -> env
+          | Node (_, item, l) :: tl ->
+              let env =
+                Environment.add item
+                 ("Implicit",
+                   (match item with
+                      | Id _ | Num _ ->
+                          (fun _ _ _ -> Cic.Implicit (Some `Closed))
+                      | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
+                 env in
+              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 =
         try
           let localization_tbl = Cic.CicHash.create 503 in
           let cic_thing =


@@ -934,19 +1086,24 @@ 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 *)
       in
       (* (4) build all possible interpretations *)

-      let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in
-      let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ =
+      let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
+      (* aux returns triples Ok/Uncertain/Ko *)
+      (* rem_dom is the concatenation of all the remainin domains *)
+      let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
+        debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));

         match todo_dom with
         | [] ->
             assert (lookup_in_todo_dom = None);
         match todo_dom with
         | [] ->
             assert (lookup_in_todo_dom = None);

-            (match test_env aliases [] base_univ with
+            (match test_env aliases rem_dom base_univ with

             | Ok (thing, metasenv),new_univ -> 
             | Ok (thing, metasenv),new_univ -> 

-               [ aliases, diff, metasenv, thing, new_univ ], []
-            | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[diff,loc,msg])
-        | (locs,item) :: remaining_dom ->
+               [ aliases, diff, metasenv, thing, new_univ ], [], []
+            | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
+            | Uncertain (loc,msg),new_univ ->
+               [],[aliases,diff,loc,msg,new_univ],[])
+        | Node (locs,item,inner_dom) :: remaining_dom ->

             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
             let choices =
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
             let choices =


@@ -955,9 +1112,11 @@ in refine_profiler.HExtlib.profile foo ()
               | Some choices -> choices in
             match choices with
                [] ->
               | Some choices -> choices in
             match choices with
                [] ->

-                [], [diff,
-                     Some (List.hd locs),
-                     lazy ("No choices for " ^ string_of_domain_item item)]
+                [], [],
+                 [aliases, diff, Some (List.hd locs),
+                  lazy ("No choices for " ^ string_of_domain_item item),
+                  true]
+(*

              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
                     if the next set of choices is also a singleton we
              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
                     if the next set of choices is also a singleton we


@@ -986,51 +1145,117 @@ in refine_profiler.HExtlib.profile foo ()
                             remaining_dom new_univ)
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
                             remaining_dom new_univ)
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with

-                        | [] -> [], [diff,loc,msg]
+                        | [] -> [], [new_env,new_diff,loc,msg,true]

                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)
                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)

-                    | Ko (loc,msg),_ -> [], [diff,loc,msg])
+                    | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
+*)

              | _::_ ->
              | _::_ ->

+                 let mark_not_significant failures =
+                   List.map
+                    (fun (env, diff, loc, msg, _b) ->
+                      env, diff, loc, msg, false)
+                    failures in
+                 let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
+                  if ok_l <> [] || uncertain_l <> [] then
+                   ok_l,uncertain_l,mark_not_significant error_l
+                  else
+                   outcome in

                let rec filter univ = function 
                let rec filter univ = function 

-                | [] -> [],[]
+                | [] -> [],[],[]

                 | codomain_item :: tl ->
                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
                     let new_env = Environment.add item codomain_item aliases in
                     let new_diff = (item,codomain_item)::diff in
                 | codomain_item :: tl ->
                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
                     let new_env = Environment.add item codomain_item aliases in
                     let new_diff = (item,codomain_item)::diff in

-                    (match test_env new_env remaining_dom univ with
+                    (match
+                      test_env new_env (inner_dom@remaining_dom@rem_dom) univ
+                     with

                     | Ok (thing, metasenv),new_univ ->
                     | Ok (thing, metasenv),new_univ ->

-                        (match remaining_dom with
-                        | [] -> [new_env,new_diff,metasenv,thing,new_univ], []
-                        | _ -> aux new_env new_diff None remaining_dom new_univ
-                        ) @@ 
-                          filter univ tl
+                        let res = 
+                          (match inner_dom with
+                          | [] ->
+                             [new_env,new_diff,metasenv,thing,new_univ], [], []
+                          | _ ->
+                             aux new_env new_diff None inner_dom
+                              (remaining_dom@rem_dom) new_univ
+                          ) 
+                        in
+                         res @@ filter univ tl

                     | Uncertain (loc,msg),new_univ ->
                     | Uncertain (loc,msg),new_univ ->

-                        (match remaining_dom with
-                        | [] -> [],[diff,loc,msg]
-                        | _ -> aux new_env new_diff None remaining_dom new_univ
-                        ) @@ 
-                          filter univ tl
-                    | Ko (loc,msg),_ -> ([],[diff,loc,msg]) @@ filter univ tl)
+                        let res =
+                          (match inner_dom with
+                          | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
+                          | _ ->
+                             aux new_env new_diff None inner_dom
+                              (remaining_dom@rem_dom) new_univ
+                          )
+                        in
+                         res @@ filter univ tl
+                    | Ko (loc,msg),_ ->
+                        let res = [],[],[new_env,new_diff,loc,msg,true] in
+                         res @@ filter univ tl)

                in
                in

-                filter base_univ choices
+                let ok_l,uncertain_l,error_l =
+                 classify_errors (filter base_univ choices)
+                in
+                 let res_after_ok_l =
+                  List.fold_right
+                   (fun (env,diff,_,_,univ) res ->
+                     aux env diff None remaining_dom rem_dom univ @@ res
+                   ) ok_l ([],[],error_l)
+                in
+                 List.fold_right
+                  (fun (env,diff,_,_,univ) res ->
+                    aux env diff None remaining_dom rem_dom univ @@ res
+                  ) uncertain_l res_after_ok_l

       in
       in

+      let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
+       match test_env aliases todo_dom base_univ with
+        | Ok _,_
+        | Uncertain _,_ ->
+           aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
+        | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in

       let base_univ = initial_ugraph in
       try
         let res =
       let base_univ = initial_ugraph in
       try
         let res =

-         match aux aliases [] None todo_dom base_univ with
-         | [],errors -> raise (NoWellTypedInterpretation (0,errors))
-         | [_,diff,metasenv,t,ugraph],_ ->
+         match aux' aliases [] None todo_dom base_univ with
+         | [],uncertain,errors ->
+            let errors =
+             List.map
+              (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
+              ) uncertain @ errors
+            in
+            let errors =
+             List.map
+              (fun (env,diff,loc,msg,significant) ->
+                let env' =
+                 filter_map_domain
+                   (fun locs domain_item ->
+                     try
+                      let description =
+                       fst (Environment.find domain_item env)
+                      in
+                       Some (locs,descr_of_domain_item domain_item,description)
+                     with
+                      Not_found -> None)
+                   thing_dom
+                in
+                 env',diff,loc,msg,significant
+              ) errors
+            in
+             raise (NoWellTypedInterpretation (0,errors))
+         | [_,diff,metasenv,t,ugraph],_,_ ->

              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false
              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false

-         | l,_ ->
+         | l,_,_ ->

              debug_print 
                (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
              let choices =
                List.map
                  (fun (env, _, _, _, _) ->
              debug_print 
                (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
              let choices =
                List.map
                  (fun (env, _, _, _, _) ->

-                   List.map
-                     (fun (locs,domain_item) ->
+                   map_domain
+                     (fun locs domain_item ->

                        let description =
                          fst (Environment.find domain_item env)
                        in
                        let description =
                          fst (Environment.find domain_item env)
                        in


@@ -1059,7 +1284,8 @@ in refine_profiler.HExtlib.profile foo ()
       in
       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
       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
+        ~domain_of_thing:domain_of_term
+        ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))

         ~refine_thing:refine_term (text,prefix_len,term)
 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
         ~refine_thing:refine_term (text,prefix_len,term)
 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri


@@ -1069,7 +1295,7 @@ in refine_profiler.HExtlib.profile foo ()
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri

-        ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
+        ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj

         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         (text,prefix_len,obj)
   end
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         (text,prefix_len,obj)
   end