Bug fixed: left parameters of constructors were unified before refining them.

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 027cde4a599d090787e1e2d86661577444df8e8f..8830a600dbaa315497030e0c61c716ab19b1c5b7 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -89,8 +89,13 @@ let ncic_mk_choice = function
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
-      let uri = UriManager.uri_of_string uri in
-       fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+        try
+         let nref = NReference.reference_of_string uri in
+          NCic.Const nref
+        with
+         NReference.IllFormedReference _ ->
+          let uri = UriManager.uri_of_string uri in
+           fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
 ;;
 
 
@@ -152,6 +157,23 @@ let lookup_in_library
   | DisambiguateTypes.Num instance -> mk_num_alias instance
 ;;
 
+let nlookup_in_library 
+  interactive_user_uri_choice input_or_locate_uri item 
+=
+  match item with
+  | DisambiguateTypes.Id id -> 
+     (try
+       let references = NCicLibrary.resolve id in
+        List.map
+         (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
+         ) references @
+        lookup_in_library interactive_user_uri_choice input_or_locate_uri item
+      with
+       NCicLibrary.ObjectNotFound _ ->
+        lookup_in_library interactive_user_uri_choice input_or_locate_uri item)
+  | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item 
+;;
+
   (** @param term not meaningful when context is given *)
 let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
 term =
@@ -181,7 +203,7 @@ let disambiguate_nterm expty lexicon_status context metasenv subst thing
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~expty 
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
-        ~lookup_in_library
+        ~lookup_in_library:nlookup_in_library
         ~mk_choice:ncic_mk_choice
         ~mk_implicit
         ~description_of_alias:LexiconAst.description_of_alias
@@ -234,6 +256,20 @@ let disambiguate_pattern
   (wanted, hyp_paths, goal_path)
 ;;
 
+type pattern = 
+  CicNotationPt.term Disambiguate.disambiguator_input option * 
+  (string * NCic.term) list * NCic.term option
+
+let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
+  let interp path = NCicDisambiguate.disambiguate_path path in
+  let goal_path = HExtlib.map_option interp goal_path in
+  let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
+  let wanted = 
+    match wanted with None -> None | Some x -> Some (text,prefix_len,x)
+  in
+   (wanted, hyp_paths, goal_path)
+;;
+
 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
   | `Unfold (Some t) ->
       let t = 
@@ -650,7 +686,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~lookup_in_library:lookup_in_library
+           ~lookup_in_library:nlookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
            ~mk_implicit
@@ -719,7 +755,36 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
  | exn ->
 (*    try_new None; *)
    raise exn
+;;
 
+let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
+  let uri =
+   let baseuri = 
+     match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
+   in
+   let name = 
+     match obj with
+     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+     | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
+     | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+     | CicNotationPt.Inductive _ -> assert false
+   in
+     UriManager.uri_of_string (baseuri ^ "/" ^ name)
+  in
+  let diff, _, _, cic =
+   singleton "third"
+    (NCicDisambiguate.disambiguate_obj
+      ~lookup_in_library:nlookup_in_library
+      ~description_of_alias:LexiconAst.description_of_alias
+      ~mk_choice:ncic_mk_choice
+      ~mk_implicit
+      ~uri:(OCic2NCic.nuri_of_ouri uri)
+      ~coercion_db:(NCicCoercion.db ())
+      ~aliases:lexicon_status.LexiconEngine.aliases
+      ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
+      (text,prefix_len,obj)) in
+  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+  lexicon_status, cic
 ;;
   
 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
@@ -738,6 +803,10 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
        in
        let metasenv,key = disambiguate_term_option metasenv key in
        !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
+   | GrafiteAst.Select (loc,uri) -> 
+        lexicon_status, metasenv, GrafiteAst.Select(loc,uri)
+   | GrafiteAst.Pump(loc,i) -> 
+        lexicon_status, metasenv, GrafiteAst.Pump(loc,i)
    | GrafiteAst.PreferCoercion (loc,t) -> 
        let lexicon_status_ref = ref lexicon_status in 
        let disambiguate_term =
@@ -750,6 +819,11 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
          disambiguate_term None text prefix_len lexicon_status_ref [] in
       let metasenv,t = disambiguate_term metasenv t in
       !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
+   | GrafiteAst.Inverter (loc,n,indty,params) ->
+       let lexicon_status_ref = ref lexicon_status in
+       let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in
+      let metasenv,indty = disambiguate_term metasenv indty in
+      !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
    | GrafiteAst.UnificationHint (loc, t, n) ->
        let lexicon_status_ref = ref lexicon_status in 
        let disambiguate_term =
@@ -761,6 +835,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Include _
    | GrafiteAst.Print _
    | GrafiteAst.Qed _
+   | GrafiteAst.NQed _
    | GrafiteAst.Set _ as cmd ->
        lexicon_status,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->