First commit with new (incomplete) disambiguation engine.

[helm.git] / matitaB / components / ng_disambiguation / grafiteDisambiguate.ml

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index dbdd2131304c1ec34b4da5a0e717fa24e7743ab9..cbe14f9d5b8aaf0bcb370a70dc22d8fd86a0e494 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -68,9 +68,11 @@ let dump_aliases out msg status =
     status#disambiguate_db.aliases
    
 let set_proof_aliases status ~implicit_aliases mode new_aliases =
+ prerr_endline "set_proof_aliases";
  if mode = GrafiteAst.WithoutPreferences then
    status
  else
+   (prerr_endline "set_proof_aliases 2";
    let aliases =
     List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
      status#disambiguate_db.aliases new_aliases in
@@ -87,7 +89,7 @@ let set_proof_aliases status ~implicit_aliases mode new_aliases =
       (if implicit_aliases then new_aliases else []) @
         status#disambiguate_db.new_aliases}
    in
-    status#set_disambiguate_db new_status
+    status#set_disambiguate_db new_status)
 
 exception BaseUriNotSetYet
 
@@ -104,7 +106,7 @@ let __Implicit = "__Implicit__"
 let __Closed_Implicit = "__Closed_Implicit__"
 
 let ncic_mk_choice status = function
-  | GrafiteAst.Symbol_alias (name, _, dsc) ->
+  | GrafiteAst.Symbol_alias (name,_, dsc) ->
      if name = __Implicit then
        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
      else if name = __Closed_Implicit then 
@@ -118,7 +120,7 @@ let ncic_mk_choice status = function
            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
         ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
-  | GrafiteAst.Number_alias (_, dsc) -> 
+  | GrafiteAst.Number_alias (_,dsc) -> 
      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
       desc, `Num_interp
        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
@@ -133,32 +135,34 @@ let ncic_mk_choice status = function
 let mk_implicit b =
   match b with
   | false -> 
-      GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
+      GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
   | true -> 
-      GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
+      GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
 ;;
 
 let nlookup_in_library 
   interactive_user_uri_choice input_or_locate_uri item 
 =
   match item with
-  | DisambiguateTypes.Id id -> 
+  | DisambiguateTypes.Id (id,_) -> 
      (try
        let references = NCicLibrary.resolve id in
         List.map
-         (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
+         (fun u -> 
+           GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
          ) references
       with
        NCicEnvironment.ObjectNotFound _ -> [])
   | _ -> []
 ;;
 
-let fix_instance item l =
+(* XXX TO BE REMOVED: no need to fix instances any more *)
+(*let fix_instance item l =
  match item with
     DisambiguateTypes.Symbol (_,n) ->
      List.map
       (function
-          GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
+          GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
         | _ -> assert false
       ) l
   | DisambiguateTypes.Num n ->
@@ -168,18 +172,19 @@ let fix_instance item l =
         | _ -> assert false
       ) l
   | DisambiguateTypes.Id _ -> l
-;;
+;;*)
+let fix_instance _ l = l;;
 
 
 let disambiguate_nterm status expty context metasenv subst thing
 =
-  let diff, metasenv, subst, cic =
+  let newast, diff, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
         status
         ~aliases:status#disambiguate_db.aliases
         ~expty 
-        ~universe:(Some status#disambiguate_db.multi_aliases)
+        ~universe:(status#disambiguate_db.multi_aliases)
         ~lookup_in_library:nlookup_in_library
         ~mk_choice:(ncic_mk_choice status)
         ~mk_implicit ~fix_instance
@@ -190,7 +195,7 @@ let disambiguate_nterm status expty context metasenv subst thing
    set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
     diff
   in
-   metasenv, subst, status, cic
+   newast, metasenv, subst, status, cic
 ;;
 
 
@@ -264,7 +269,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
       ~mk_choice:(ncic_mk_choice status)
       ~mk_implicit ~fix_instance ~uri
       ~aliases:status#disambiguate_db.aliases
-      ~universe:(Some status#disambiguate_db.multi_aliases) 
+      ~universe:(status#disambiguate_db.multi_aliases) 
       (text,prefix_len,obj)) in
   let status =
    set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
@@ -283,14 +288,14 @@ let disambiguate_cic_appl_pattern status args =
       (List.exists
        (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
      ->
-      let item = DisambiguateTypes.Id id in
+      let item = DisambiguateTypes.Id (id,None) in
        begin
         try
          match
           DisambiguateTypes.Environment.find item
            status#disambiguate_db.aliases
          with
-            GrafiteAst.Ident_alias (_, uri) ->
+            GrafiteAst.Ident_alias (_,uri) ->
              NotationPt.NRefPattern (NReference.reference_of_string uri)
           | _ -> assert false
         with Not_found -> 
@@ -315,6 +320,6 @@ let aliases_for_objs status refs =
        List.map
         (fun u ->
           let name = NCicPp.r2s status true u in
-           DisambiguateTypes.Id name,
+           DisambiguateTypes.Id (name, Some (NReference.string_of_reference u)),
             GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
         ) references) refs)