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 9dc19c7c6a3b281056d4c0c9c640b41d58217a43..d58dc9854bceef447083e2ff628bfe99ef6eee91 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


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


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


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


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


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


@@ -267,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=[]);


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


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


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


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


@@ -469,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 =


@@ -639,20 +725,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


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

-            @ domain_of_term_option ~loc ~context typ
+            @ domain_of_term_option ~loc ~context:context' typ

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


@@ -819,7 +910,7 @@ module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->
 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 -> 


@@ -834,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 *


@@ -995,7 +1086,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


@@ -1194,7 +1285,7 @@ in refine_profiler.HExtlib.profile foo ()
       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_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
+        ~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


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