Universe is used only locally to tactics/

[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index b49af2bbf5999b69f693293c5bb7f7a462345487..b9b4fa42b837d1c64041ad874570add883f40a8d 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -28,7 +28,7 @@ let cic_name_of_name = function
 ;;
 
 let refine_term 
- metasenv subst context uri ~coercion_db ~use_coercions term _ ~localization_tbl=
+ 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)));
@@ -36,8 +36,8 @@ let refine_term
     let localise t = 
       try NCicUntrusted.NCicHash.find localization_tbl t
       with Not_found -> 
-        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-        assert false
+        prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+        (*assert false*) HExtlib.dummy_floc
     in
     let metasenv, subst, term, _ = 
       NCicRefiner.typeof
@@ -46,7 +46,7 @@ let refine_term
           if use_coercions then 
            NCicCoercion.look_for_coercion coercion_db
           else (fun _ _ _ _ _ -> []))
-        metasenv subst context term None ~localise 
+        metasenv subst context term expty ~localise 
     in
      Disambiguate.Ok (term, metasenv, subst, ())
   with
@@ -61,8 +61,8 @@ let refine_term
 ;;
 
 let refine_obj 
-  ~coercion_db metasenv subst context uri 
-  ~use_coercions obj ugraph ~localization_tbl 
+  ~coercion_db metasenv subst context _uri 
+  ~use_coercions obj _ _ugraph ~localization_tbl 
 =
   assert (metasenv=[]);
   assert (subst=[]);
@@ -304,7 +304,7 @@ let interpretate_term_and_interpretate_term_option
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
-    | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false 
+    | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->
@@ -322,8 +322,7 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | 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) ->
@@ -386,6 +385,15 @@ let interpretate_term_option
     ~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 new_flavour_of_flavour = function 
   | `Definition -> `Definition
   | `MutualDefinition -> `Definition 
@@ -562,26 +570,12 @@ let interpretate_obj
 *)
 ;;
 
-let disambiguate_term ~context ~metasenv ~subst ?goal
+let disambiguate_term ~context ~metasenv ~subst ~expty
    ~mk_implicit ~description_of_alias ~mk_choice
    ~aliases ~universe ~coercion_db ~lookup_in_library 
    (text,prefix_len,term) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x 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 res,b =
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_term
@@ -593,7 +587,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
      ~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 ~hint ~subst
+     ~mk_localization_tbl ~expty ~subst
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
 ;;
@@ -604,7 +598,6 @@ let disambiguate_obj
    (text,prefix_len,obj) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
-  let hint = (fun x y -> y), (fun x -> x) in
    let res,b =
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_obj
@@ -619,7 +612,7 @@ let disambiguate_obj
      ~interpretate_thing:(interpretate_obj ~mk_choice)
      ~refine_thing:(refine_obj ~coercion_db) 
      (text,prefix_len,obj)
-     ~mk_localization_tbl ~hint
+     ~mk_localization_tbl ~expty:None
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
 ;;