X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=6e72042e83c6a34901de94fe5607e6f41ecc9088;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=267b40a20af91da6c3535e12bcfde75f4c24e833;hpb=9a9c5b863f68367119450ae7b806d454ba1265e3;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 267b40a20..6e72042e8 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -27,17 +27,32 @@ let cic_name_of_name = function
   | _ -> assert false
 ;;
 
-let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization_tbl =
+let rec mk_rels howmany from =
+  match howmany with 
+  | 0 -> []
+  | _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
+;;
+
+let refine_term 
+ metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl=
   assert (uri=None);
   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" 
     (NCicPp.ppterm ~metasenv ~subst ~context term)));
   try
     let localise t = 
       try NCicUntrusted.NCicHash.find localization_tbl t
-      with Not_found -> assert false
+      with Not_found -> 
+        prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+        (*assert false*) HExtlib.dummy_floc
     in
     let metasenv, subst, term, _ = 
-      NCicRefiner.typeof metasenv subst context term None ~localise 
+      NCicRefiner.typeof
+        (NCicUnifHint.db ())
+        ~look_for_coercion:(
+          if use_coercions then 
+           NCicCoercion.look_for_coercion coercion_db
+          else (fun _ _ _ _ _ -> []))
+        metasenv subst context term expty ~localise 
     in
      Disambiguate.Ok (term, metasenv, subst, ())
   with
@@ -51,6 +66,41 @@ let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization
       Disambiguate.Ko loc_msg
 ;;
 
+let refine_obj 
+  ~coercion_db metasenv subst context _uri 
+  ~use_coercions obj _ _ugraph ~localization_tbl 
+=
+  assert (metasenv=[]);
+  assert (subst=[]);
+  let localise t = 
+    try NCicUntrusted.NCicHash.find localization_tbl t
+    with Not_found -> 
+      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+      (*assert false*)HExtlib.dummy_floc
+  in
+  try
+    let obj =
+      NCicRefiner.typeof_obj
+        (NCicUnifHint.db ())
+        ~look_for_coercion:(
+          if use_coercions then 
+           NCicCoercion.look_for_coercion coercion_db
+          else (fun _ _ _ _ _ -> []))
+        obj ~localise 
+    in
+      Disambiguate.Ok (obj, [], [], ())
+  with
+  | NCicRefiner.Uncertain loc_msg ->
+      debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^ 
+        NCicPp.ppobj obj)) ;
+      Disambiguate.Uncertain loc_msg
+  | NCicRefiner.RefineFailure loc_msg ->
+      debug_print (lazy (sprintf "PRUNED:\nobj: %s\nmessage: %s"
+        (NCicPp.ppobj obj) (snd(Lazy.force loc_msg))));
+      Disambiguate.Ko loc_msg
+;;
+  
+
   (* TODO move it to Cic *)
 let find_in_context name context =
   let rec aux acc = function
@@ -60,9 +110,9 @@ let find_in_context name context =
   in
   aux 1 context
 
-let interpretate_term 
-  ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast 
-  ~localization_tbl
+let interpretate_term_and_interpretate_term_option 
+  ?(create_dummy_ids=false) 
+    ~obj_context ~mk_choice ~env ~uri ~is_path ~localization_tbl 
 =
   (* create_dummy_ids shouldbe used only for interpretating patterns *)
   assert (uri = None);
@@ -70,8 +120,9 @@ let interpretate_term
   let rec aux ~localize loc context = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         let res = aux ~localize loc context term in
-         if localize then NCicUntrusted.NCicHash.add localization_tbl res loc;
-         res
+        if localize then 
+         NCicUntrusted.NCicHash.add localization_tbl res loc;
+       res
     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
         let cic_args = List.map (aux ~localize loc context) args in
@@ -128,14 +179,15 @@ let interpretate_term
           | Some (indty_ident, _) ->
              (match Disambiguate.resolve ~env ~mk_choice 
                 (Id indty_ident) (`Args []) with
-              | NCic.Const r -> r
+              | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
               | NCic.Implicit _ ->
                  raise (Disambiguate.Try_again 
                   (lazy "The type of the term to be matched is still unknown"))
-              | _ ->
+              | t ->
                 raise (DisambiguateTypes.Invalid_choice 
                   (lazy (loc,"The type of the term to be matched "^
-                          "is not (co)inductive!"))))
+                          "is not (co)inductive: " ^ NCicPp.ppterm 
+                          ~metasenv:[] ~subst:[] ~context:[] t))))
           | None ->
               let rec fst_constructor =
                 function
@@ -146,16 +198,26 @@ let interpretate_term
                      "because it is an inductive type without constructors "^
                      "or because all patterns use wildcards")))
               in
-              (match Disambiguate.resolve ~env ~mk_choice 
+(*
+              DisambiguateTypes.Environment.iter
+                  (fun k v ->
+                      prerr_endline
+                        (DisambiguateTypes.string_of_domain_item k ^ " => " ^
+                        description_of_alias v)) env; 
+*)
+              (match Disambiguate.resolve ~env ~mk_choice
                 (Id (fst_constructor branches)) (`Args []) with
-              | NCic.Const r -> r
+              | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> 
+                   let b,_,_,_,_ = NCicEnvironment.get_checked_indtys r in
+                   NReference.mk_indty b r
               | NCic.Implicit _ ->
                  raise (Disambiguate.Try_again 
                   (lazy "The type of the term to be matched is still unknown"))
-              | _ ->
+              | t ->
                 raise (DisambiguateTypes.Invalid_choice 
                   (lazy (loc, 
-                  "The type of the term to be matched is not (co)inductive!"))))
+                  "The type of the term to be matched is not (co)inductive: " 
+                  ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
          in
          let _,leftsno,itl,_,indtyp_no =
           NCicEnvironment.get_checked_indtys indtype_ref in
@@ -164,7 +226,7 @@ let interpretate_term
            List.nth itl indtyp_no
           with _ -> assert false in
          let rec count_prod t =
-           match NCicReduction.whd [] t with
+                 match NCicReduction.whd ~subst:[] [] t with
                NCic.Prod (_, _, t) -> 1 + (count_prod t)
              | _ -> 0 
          in 
@@ -247,121 +309,28 @@ let interpretate_term
           | Some t -> aux ~localize loc context t
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
-        NCic.LetIn (cic_name, cic_def, cic_typ, cic_body)
-    | CicNotationPt.LetRec (_kind, _defs, _body) ->
-       assert false (*
-        let context' =
-          List.fold_left
-            (fun acc (_, (name, _), _, _) ->
-              cic_name_of_name name :: acc)
-            context defs
-        in
-        let cic_body =
-         let unlocalized_body = aux ~localize:false loc context' body in
-         match unlocalized_body with
-            NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
-          | NCic.Appl (NCic.Rel n::l) when n <= List.length defs ->
-             (try
-               let l' =
-                List.map
-                 (function t ->
-                   let t',subst,metasenv =
-                    CicMetaSubst.delift_rels [] [] (List.length defs) t
-                   in
-                    assert (subst=[]);
-                    assert (metasenv=[]);
-                    t') l
-               in
-                (* We can avoid the LetIn. But maybe we need to recompute l'
-                   so that it is localized *)
-                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
-                else
-                 `AvoidLetIn (n,l')
-              with
-               CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-                if localize then
-                 `AddLetIn (aux ~localize loc context' body)
-                else
-                 `AddLetIn unlocalized_body)
-          | _ ->
-             if localize then
-              `AddLetIn (aux ~localize loc context' body)
-             else
-              `AddLetIn unlocalized_body
-        in
-        let inductiveFuns =
-          List.map
-            (fun (params, (name, typ), body, decr_idx) ->
-              let add_binders kind t =
-               List.fold_right
-                (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
-              in
-              let cic_body =
-               aux ~localize loc context' (add_binders `Lambda body) in
-              let cic_type =
-               aux_option ~localize loc context (Some `Type)
-                (HExtlib.map_option (add_binders `Pi) typ) in
-              let name =
-                match cic_name_of_name name with
-                | NCic.Anonymous ->
-                    CicNotationPt.fail loc
-                      "Recursive functions cannot be anonymous"
-                | NCic.Name name -> name
-              in
-              (name, decr_idx, cic_type, cic_body))
-            defs
-        in
-        let fix_or_cofix n =
-         match kind with
-            `Inductive -> NCic.Fix (n,inductiveFuns)
-          | `CoInductive ->
-              let coinductiveFuns =
-                List.map
-                 (fun (name, _, typ, body) -> name, typ, body)
-                 inductiveFuns
-              in
-               NCic.CoFix (n,coinductiveFuns)
-        in
-         let counter = ref ~-1 in
-         let build_term _ (var,_,ty,_) t =
-          incr counter;
-          NCic.LetIn (NCic.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
-                 NCic.Appl (fix_or_cofix n'::l)
-            | `AddLetIn cic_body ->         
-                List.fold_right (build_term inductiveFuns) inductiveFuns
-                 cic_body)
-*)
+        NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
+    | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | CicNotationPt.Ident _
-    | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.Uri _
+    | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->
        assert (subst = None);
        (try
-         NCic.Rel (find_in_context name context)
+             NCic.Rel (find_in_context name context)
        with Not_found -> 
-         Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
-    | CicNotationPt.Uri (name, subst) ->
+         try NCic.Const (List.assoc name obj_context)
+         with Not_found ->
+           Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+    | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (NRef.reference_of_string name)
+         NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
+    | CicNotationPt.NRef nref -> NCic.Const nref
     | CicNotationPt.Implicit -> NCic.Implicit `Term
-    | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole)
-patterns not implemented *)
+    | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
     | CicNotationPt.Meta (index, subst) ->
@@ -372,60 +341,276 @@ patterns not implemented *)
         in
          NCic.Meta (index, (0, NCic.Ctx cic_subst))
     | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
-    | CicNotationPt.Sort `Set -> assert false
-    | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
+    | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
        [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+    | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
+       [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
+    | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
+       [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
+    | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
+       [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
+       [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
-    | _ -> assert false (* god bless Bologna *)
+    | CicNotationPt.Variable _
+    | CicNotationPt.Magic _
+    | CicNotationPt.Layout _
+    | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
   and aux_option ~localize loc context annotation = function
     | None -> NCic.Implicit annotation
     | Some (CicNotationPt.AttributedTerm (`Loc loc, term)) ->
         let res = aux_option ~localize loc context annotation (Some term) in
-        if localize then NCicUntrusted.NCicHash.add localization_tbl res loc;
+        if localize then 
+          NCicUntrusted.NCicHash.add localization_tbl res loc;
         res
     | Some (CicNotationPt.AttributedTerm (_, term)) ->
         aux_option ~localize loc context annotation (Some term)
     | Some CicNotationPt.Implicit -> NCic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in
-   aux ~localize:true HExtlib.dummy_floc context ast
+   (fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
+   (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
+;;
 
 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
-     ~localization_tbl
+     ~obj_context ~localization_tbl ~mk_choice
 =
   let context = List.map fst context in
-  interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
-~localization_tbl
+  fst 
+    (interpretate_term_and_interpretate_term_option 
+      ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+    ~context ast
 ;;
 
-let domain_of_term ~context = 
-  Disambiguate.domain_of_ast_term ~context
-;; 
+let interpretate_term_option 
+  ?(create_dummy_ids=false) ~context ~env ~uri ~is_path 
+  ~localization_tbl ~mk_choice ~obj_context
+=
+  let context = List.map fst context in
+  snd 
+    (interpretate_term_and_interpretate_term_option 
+      ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+    ~context 
+;;
+
+let disambiguate_path path =
+  let localization_tbl = NCicUntrusted.NCicHash.create 23 in
+  fst
+    (interpretate_term_and_interpretate_term_option 
+    ~obj_context:[] ~mk_choice:(fun _ -> assert false)
+    ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
+    ~uri:None ~is_path:true ~localization_tbl) ~context:[] path
+;;
 
-let disambiguate_term ~context ~metasenv ~subst ?goal
+let new_flavour_of_flavour = function 
+  | `Definition -> `Definition
+  | `MutualDefinition -> `Definition 
+  | `Fact -> `Fact
+  | `Lemma -> `Lemma
+  | `Remark -> `Corollary
+  | `Theorem -> `Theorem
+  | `Variant -> `Corollary 
+  | `Axiom -> `Fact
+;;
+
+let ncic_name_of_ident = function
+  | Ast.Ident (name, None) -> name
+  | _ -> assert false
+;;
+
+let interpretate_obj 
+(*      ?(create_dummy_ids=false)  *)
+     ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice 
+=
+ assert (context = []);
+ assert (is_path = false);
+ let interpretate_term ~obj_context =
+  interpretate_term ~mk_choice ~localization_tbl ~obj_context in
+ let interpretate_term_option ~obj_context =
+   interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
+ let uri = match uri with | None -> assert false | Some u -> u in
+ match obj with
+ | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+     let ty' = 
+       interpretate_term 
+         ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty 
+     in
+     let height = (* XXX calculate *) 0 in
+     uri, height, [], [], 
+     (match bo,flavour with
+      | None,`Axiom -> 
+          let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+          NCic.Constant ([],name,None,ty',attrs)
+      | Some _,`Axiom -> assert false
+      | None,_ ->
+          let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+          NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
+      | Some bo,_ ->
+        (match bo with
+         | CicNotationPt.LetRec (kind, defs, _) ->
+             let inductive = kind = `Inductive in
+             let _,obj_context =
+               List.fold_left
+                 (fun (i,acc) (_,(name,_),_,k) -> 
+                  (i+1, 
+                    (ncic_name_of_ident name, NReference.reference_of_spec uri 
+                     (if inductive then NReference.Fix (i,k,0)
+                      else NReference.CoFix i)) :: acc))
+                 (0,[]) defs
+             in
+             let inductiveFuns =
+               List.map
+                 (fun (params, (name, typ), body, decr_idx) ->
+                   let add_binders kind t =
+                    List.fold_right
+                     (fun var t -> 
+                        CicNotationPt.Binder (kind, var, t)) params t
+                   in
+                   let cic_body =
+                     interpretate_term 
+                       ~obj_context ~context ~env ~uri:None ~is_path:false
+                       (add_binders `Lambda body) 
+                   in
+                   let cic_type =
+                     interpretate_term_option 
+                       ~obj_context:[]
+                       ~context ~env ~uri:None ~is_path:false `Type
+                       (HExtlib.map_option (add_binders `Pi) typ)
+                   in
+                   ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
+                 defs
+             in
+             let attrs = `Provided, new_flavour_of_flavour flavour in
+             NCic.Fixpoint (inductive,inductiveFuns,attrs)
+         | bo -> 
+             let bo = 
+               interpretate_term 
+                ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
+             in
+             let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+             NCic.Constant ([],name,Some bo,ty',attrs)))
+ | CicNotationPt.Inductive (params,tyl) ->
+    let context,params =
+     let context,res =
+      List.fold_left
+       (fun (context,res) (name,t) ->
+         let t =
+          match t with
+             None -> CicNotationPt.Implicit
+           | Some t -> t in
+         let name = cic_name_of_name name in
+         let t =
+          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false t
+         in
+          (name,NCic.Decl t)::context,(name,t)::res
+       ) ([],[]) params
+     in
+      context,List.rev res in
+    let add_params =
+     List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
+    let leftno = List.length params in
+    let obj_context =
+     snd (
+      List.fold_left
+       (fun (i,res) (name,_,_,_) ->
+         let _,inductive,_,_ =
+          (* ??? *)
+          try List.hd tyl with Failure _ -> assert false in
+         let nref =
+          NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
+         in
+          i+1,(name,nref)::res)
+       (0,[]) tyl) in
+    let tyl =
+     List.map
+      (fun (name,_,ty,cl) ->
+        let ty' =
+         add_params
+         (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false ty) in
+        let cl' =
+         List.map
+          (fun (name,ty) ->
+            let ty' =
+             add_params
+              (interpretate_term ~obj_context ~context ~env ~uri:None
+                ~is_path:false ty) in
+            let relevance = [] in
+             relevance,name,ty'
+          ) cl in
+        let relevance = [] in
+         relevance,name,ty',cl'
+      ) tyl
+    in
+     let height = (* XXX calculate *) 0 in
+     let attrs = `Provided, `Regular in
+     uri, height, [], [], 
+     NCic.Inductive (true,leftno,tyl,attrs)
+ | CicNotationPt.Record (params,name,ty,fields) ->
+    let context,params =
+     let context,res =
+      List.fold_left
+       (fun (context,res) (name,t) ->
+         let t =
+          match t with
+             None -> CicNotationPt.Implicit
+           | Some t -> t in
+         let name = cic_name_of_name name in
+         let t =
+          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false t
+         in
+          (name,NCic.Decl t)::context,(name,t)::res
+       ) ([],[]) params
+     in
+      context,List.rev res in
+    let add_params =
+     List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
+    let leftno = List.length params in
+    let ty' =
+     add_params
+      (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+        ~is_path:false ty) in
+    let nref =
+     NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+    let obj_context = [name,nref] in
+    let fields' =
+     snd (
+      List.fold_left
+       (fun (context,res) (name,ty,_coercion,_arity) ->
+         let ty =
+          interpretate_term ~obj_context ~context ~env ~uri:None
+           ~is_path:false ty in
+         let context' = (name,NCic.Decl ty)::context in
+          context',(name,ty)::res
+       ) (context,[]) fields) in
+    let concl =
+     let mutind = NCic.Const nref in
+     if params = [] then mutind
+     else
+      NCic.Appl
+       (mutind::mk_rels (List.length params) (List.length fields)) in
+    let con =
+     List.fold_left (fun t (name,ty) -> NCic.Prod (name,ty,t)) concl fields' in
+    let con' = add_params con in
+    let relevance = [] in
+    let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
+    let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
+     let height = (* XXX calculate *) 0 in
+     let attrs = `Provided, `Record field_names in
+     uri, height, [], [], 
+     NCic.Inductive (true,leftno,tyl,attrs)
+;;
+
+let disambiguate_term ~context ~metasenv ~subst ~expty
    ~mk_implicit ~description_of_alias ~mk_choice
-   ~aliases ~universe ~lookup_in_library 
+   ~aliases ~universe ~coercion_db ~lookup_in_library 
    (text,prefix_len,term) 
  =
-  let localization_tbl = NCicUntrusted.NCicHash.create 503 in
-  let hint =
-   match goal with
-      None -> (fun _ y -> y),(fun x -> x)
-    | Some n ->
-       (fun metasenv y ->
-         let _,_,ty = NCicUtils.lookup_meta n metasenv in
-          NCic.LetIn ("_",ty,y,NCic.Rel 1)),
-       (function  
-        | Disambiguate.Ok (t,m,s,ug) ->
-            (match t with
-            | NCic.LetIn ("_",_,y,NCic.Rel 1) -> Disambiguate.Ok (y,m,s,ug)
-            | _ -> assert false)
-        | k -> k)
-  in
+  let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
    let res,b =
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_term
@@ -434,11 +619,76 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
      ~passes:(MultiPassDisambiguator.passes ())
-     ~lookup_in_library ~domain_of_thing:domain_of_term
-     ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None))
-     ~refine_thing:refine_term (text,prefix_len,term)
-     ~localization_tbl ~hint ~subst
+     ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
+     ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
+     ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term)
+     ~mk_localization_tbl ~expty ~subst
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
 ;;
 
+let disambiguate_obj 
+   ~mk_implicit ~description_of_alias ~mk_choice
+   ~aliases ~universe ~coercion_db ~lookup_in_library ~uri
+   (text,prefix_len,obj) 
+ =
+  let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
+   let res,b =
+    MultiPassDisambiguator.disambiguate_thing
+     ~freshen_thing:CicNotationUtil.freshen_obj
+     ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
+     ~mk_implicit ~description_of_alias
+     ~string_context_of_context:(List.map (fun (x,_) -> Some x))
+     ~universe 
+     ~uri:(Some uri)
+     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+     ~passes:(MultiPassDisambiguator.passes ())
+     ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
+     ~interpretate_thing:(interpretate_obj ~mk_choice)
+     ~refine_thing:(refine_obj ~coercion_db) 
+     (text,prefix_len,obj)
+     ~mk_localization_tbl ~expty:None
+   in
+    List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+;;
+(*
+let _ = 
+let mk_type n = 
+  if n = 0 then
+     [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+  else
+     [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+in
+let mk_cprop n = 
+  if n = 0 then 
+    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+  else
+    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+in
+         NCicEnvironment.add_constraint true (mk_type 0) (mk_type 1);
+         NCicEnvironment.add_constraint true (mk_cprop 0) (mk_cprop 1);
+         NCicEnvironment.add_constraint true (mk_cprop 0) (mk_type 1);
+         NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1);
+         NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0);
+         NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0);
+
+         NCicEnvironment.add_constraint true (mk_type 1) (mk_type 2);
+         NCicEnvironment.add_constraint true (mk_cprop 1) (mk_cprop 2);
+         NCicEnvironment.add_constraint true (mk_cprop 1) (mk_type 2);
+         NCicEnvironment.add_constraint true (mk_type 1) (mk_cprop 2);
+         NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1);
+         NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1);
+
+         NCicEnvironment.add_constraint true (mk_type 2) (mk_type 3);
+         NCicEnvironment.add_constraint true (mk_cprop 2) (mk_cprop 3);
+         NCicEnvironment.add_constraint true (mk_cprop 2) (mk_type 3);
+         NCicEnvironment.add_constraint true (mk_type 2) (mk_cprop 3);
+         NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2);
+         NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2);
+
+         NCicEnvironment.add_constraint false (mk_cprop 3) (mk_type 3);
+         NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
+
+;;
+*)
+