huge commit regarding the grafite_status:

[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..5002e58abca402e7f4691954ca93b7128c6766e5 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -195,23 +195,24 @@ 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.NEstatus.rstatus
+        ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
         ~expty 
-        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+        ~universe:(Some estatus.NEstatus.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 lexicon_status = 
+    LexiconEngine.set_proof_aliases estatus.NEstatus.lstatus diff in
+  metasenv, subst, { estatus with NEstatus.lstatus = lexicon_status }, cic
 ;;
 
 
@@ -619,7 +620,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 +669,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 +688,14 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
+           ~rdb:estatus.NEstatus.rstatus
            ~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.NEstatus.lstatus.LexiconEngine.aliases
+           ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases)
            (text,prefix_len,obj)
          with
          | [_,_,_,obj],_ ->
@@ -727,6 +728,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
 (*   let time = Unix.gettimeofday () in  *)
 
 
+  let lexicon_status = estatus.NEstatus.lstatus in
   let (diff, metasenv, _, cic, _) =
     singleton "third"
       (CicDisambiguate.disambiguate_obj 
@@ -737,7 +739,8 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
         ~uri:(Some uri)
-        (text,prefix_len,obj)) in
+        (text,prefix_len,obj)) 
+  in
 
 
 (*
@@ -749,7 +752,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
 
 
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
-  lexicon_status, metasenv, cic
+  { estatus with NEstatus.lstatus = lexicon_status }, metasenv, cic
 
  with 
  | Sys.Break as exn -> raise exn
@@ -758,7 +761,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 +783,20 @@ 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.NEstatus.rstatus
+      ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
+      ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) 
       (text,prefix_len,obj)) in
-  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
-  lexicon_status, cic
+  let lexicon_status =
+    LexiconEngine.set_proof_aliases estatus.NEstatus.lstatus diff in
+  { estatus with NEstatus.lstatus = lexicon_status }, 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.NObj(loc,obj) -> estatus, metasenv, GrafiteAst.NObj(loc,obj)
    | GrafiteAst.Index(loc,key,uri) ->
-       let lexicon_status_ref = ref lexicon_status in 
+       let lexicon_status_ref = ref estatus.NEstatus.lstatus in 
        let disambiguate_term =
          disambiguate_term None text prefix_len lexicon_status_ref [] in
        let disambiguate_term_option metasenv =
@@ -803,34 +807,40 @@ 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)
+       { estatus with NEstatus.lstatus = !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.NEstatus.lstatus 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)
+      { estatus with NEstatus.lstatus = !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.NEstatus.lstatus 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)
+      { estatus with NEstatus.lstatus = !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)
+       let lexicon_status_ref = ref estatus.NEstatus.lstatus in
+       let disambiguate_term = 
+         disambiguate_term None text prefix_len lexicon_status_ref [] in
+       let metasenv,indty = disambiguate_term metasenv indty in
+       { estatus with NEstatus.lstatus = !lexicon_status_ref }, 
+       metasenv, GrafiteAst.Inverter (loc,n,indty,params)
    | GrafiteAst.UnificationHint (loc, t, n) ->
-       let lexicon_status_ref = ref lexicon_status in 
+       let lexicon_status_ref = ref estatus.NEstatus.lstatus 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)
+      { estatus with NEstatus.lstatus = !lexicon_status_ref }, 
+      metasenv, GrafiteAst.UnificationHint (loc,t,n)
    | GrafiteAst.Default _
    | GrafiteAst.Drop _
    | GrafiteAst.Include _
@@ -839,13 +849,13 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | 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.NEstatus.lstatus in 
       let disambiguate_term =
        disambiguate_term None text prefix_len lexicon_status_ref [] in
       let disambiguate_term_option metasenv =
@@ -860,7 +870,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
       let metasenv,refl = disambiguate_term_option metasenv refl in
       let metasenv,sym = disambiguate_term_option metasenv sym in
       let metasenv,trans = disambiguate_term_option metasenv trans in
-       !lexicon_status_ref, metasenv,
+      { estatus with NEstatus.lstatus = !lexicon_status_ref }, metasenv,
         GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 
 let disambiguate_macro