1) grafiteWalker removed

[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 9c12d1173c6c9b212e021f52b71e24b1d7ea863b..a0558d9f65a06af2f3703d3826f5f4a678339092 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -170,7 +170,7 @@ let nlookup_in_library
          ) references @
         lookup_in_library interactive_user_uri_choice input_or_locate_uri item
       with
-       NCicLibrary.ObjectNotFound _ ->
+       NCicEnvironment.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 
 ;;
@@ -182,8 +182,8 @@ term =
   let (diff, metasenv, subst, cic, _) =
     singleton "first"
       (CicDisambiguate.disambiguate_term
-        ~aliases:lexicon_status.LexiconEngine.aliases
-        ~expty ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+        ~aliases:lexicon_status#lstatus.LexiconEngine.aliases
+        ~expty ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases)
         ~lookup_in_library
         ~mk_choice:cic_mk_choice
         ~mk_implicit
@@ -195,23 +195,23 @@ term =
   metasenv,(*subst,*) cic
 ;;
 
-let disambiguate_nterm expty lexicon_status context metasenv subst thing
+let disambiguate_nterm expty estatus context metasenv subst thing
 =
   let diff, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
-        ~coercion_db:(NCicCoercion.db ())
-        ~aliases:lexicon_status.LexiconEngine.aliases
+        ~rdb:estatus
+        ~aliases:estatus#lstatus.LexiconEngine.aliases
         ~expty 
-        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+        ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
         ~lookup_in_library:nlookup_in_library
         ~mk_choice:ncic_mk_choice
         ~mk_implicit
         ~description_of_alias:LexiconAst.description_of_alias
         ~context ~metasenv ~subst thing)
   in
-  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
-  metasenv, subst, lexicon_status, cic
+  let estatus = LexiconEngine.set_proof_aliases estatus diff in
+   metasenv, subst, estatus, cic
 ;;
 
 
@@ -230,8 +230,8 @@ let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
           ~mk_choice:cic_mk_choice
           ~mk_implicit
           ~description_of_alias:LexiconAst.description_of_alias
-          ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
-          ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+          ~initial_ugraph:ugraph ~aliases:lexicon_status#lstatus.LexiconEngine.aliases
+          ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases)
           ~context ~metasenv ~subst:[] 
           (text,prefix_len,term) ~expty) in
     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
@@ -619,7 +619,7 @@ let rec disambiguate_tactic
           | `Proof as t -> metasenv,t in
         metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)   
 
-let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
+let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
   let uri =
    let baseuri = 
      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
@@ -668,7 +668,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
                 let _,g = CicTypeChecker.typecheck uri in
                 CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri))
              graph l)
-       graph (CoercDb.to_list ())
+       graph (CoercDb.to_list (CoercDb.dump ()))
    in
    ignore(CicUniv.do_rank graph);
 
@@ -687,14 +687,14 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
+           ~rdb:estatus
            ~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) 
+           ~aliases:estatus#lstatus.LexiconEngine.aliases
+           ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
            (text,prefix_len,obj)
          with
          | [_,_,_,obj],_ ->
@@ -734,10 +734,11 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         ~mk_choice:cic_mk_choice
         ~mk_implicit
         ~description_of_alias:LexiconAst.description_of_alias
-        ~aliases:lexicon_status.LexiconEngine.aliases
-        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
+        ~aliases:estatus#lstatus.LexiconEngine.aliases
+        ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) 
         ~uri:(Some uri)
-        (text,prefix_len,obj)) in
+        (text,prefix_len,obj)) 
+  in
 
 
 (*
@@ -748,8 +749,8 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
 (*    try_new (Some cic);   *)
 
 
-  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
-  lexicon_status, metasenv, cic
+  let estatus = LexiconEngine.set_proof_aliases estatus diff in
+   estatus, metasenv, cic
 
  with 
  | Sys.Break as exn -> raise exn
@@ -758,7 +759,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
    raise exn
 ;;
 
-let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
+let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
   let uri =
    let baseuri = 
      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
@@ -780,19 +781,18 @@ let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
       ~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) 
+      ~rdb:estatus
+      ~aliases:estatus#lstatus.LexiconEngine.aliases
+      ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) 
       (text,prefix_len,obj)) in
-  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
-  lexicon_status, cic
+  let estatus = LexiconEngine.set_proof_aliases estatus diff in
+   estatus, cic
 ;;
   
-let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
+let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
   match cmd with
-   | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj)
    | GrafiteAst.Index(loc,key,uri) ->
-       let lexicon_status_ref = ref lexicon_status in 
+       let lexicon_status_ref = ref estatus in 
        let disambiguate_term =
          disambiguate_term None text prefix_len lexicon_status_ref [] in
        let disambiguate_term_option metasenv =
@@ -803,49 +803,42 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
                  metasenv, Some t
        in
        let metasenv,key = disambiguate_term_option metasenv key in
-       !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
+        !lexicon_status_ref,metasenv,GrafiteAst.Index(loc,key,uri)
    | GrafiteAst.Select (loc,uri) -> 
-        lexicon_status, metasenv, GrafiteAst.Select(loc,uri)
+        estatus, metasenv, GrafiteAst.Select(loc,uri)
    | GrafiteAst.Pump(loc,i) -> 
-        lexicon_status, metasenv, GrafiteAst.Pump(loc,i)
+        estatus, metasenv, GrafiteAst.Pump(loc,i)
    | GrafiteAst.PreferCoercion (loc,t) -> 
-       let lexicon_status_ref = ref lexicon_status in 
+       let lexicon_status_ref = ref estatus in 
        let disambiguate_term =
          disambiguate_term None text prefix_len lexicon_status_ref [] in
       let metasenv,t = disambiguate_term metasenv t in
-      !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t)
+       !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t)
    | GrafiteAst.Coercion (loc,t,b,a,s) -> 
-       let lexicon_status_ref = ref lexicon_status in 
+       let lexicon_status_ref = ref estatus in 
        let disambiguate_term =
          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)
+       !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 =
+       let lexicon_status_ref = ref estatus in
+       let disambiguate_term = 
          disambiguate_term None text prefix_len lexicon_status_ref [] in
-      let metasenv,t = disambiguate_term metasenv t in
-      !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t,n)
+       let metasenv,indty = disambiguate_term metasenv indty in
+        !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
    | GrafiteAst.Default _
    | GrafiteAst.Drop _
    | GrafiteAst.Include _
    | GrafiteAst.Print _
    | GrafiteAst.Qed _
-   | GrafiteAst.NQed _
-   | GrafiteAst.NUnivConstraint _
    | GrafiteAst.Set _ as cmd ->
-       lexicon_status,metasenv,cmd
+       estatus,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->
-       let lexicon_status,metasenv,obj =
-        disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
-       lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
+       let estatus,metasenv,obj =
+        disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj)in
+       estatus, metasenv, GrafiteAst.Obj (loc,obj)
    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
-      let lexicon_status_ref = ref lexicon_status in 
+      let lexicon_status_ref = ref estatus in 
       let disambiguate_term =
        disambiguate_term None text prefix_len lexicon_status_ref [] in
       let disambiguate_term_option metasenv =