Added initial support for inversion principles in Matita NG.

[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 4aadd70779760d9eca5bf1e578a02316ef0f3b50..6b5dfca61b829235b852cdc4e7f0a44cd6d52501 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -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
@@ -200,19 +200,18 @@ let disambiguate_nterm expty estatus context metasenv subst thing
   let diff, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
-        ~rdb:estatus.NEstatus.rstatus
-        ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
+        ~rdb:estatus
+        ~aliases:estatus#lstatus.LexiconEngine.aliases
         ~expty 
-        ~universe:(Some estatus.NEstatus.lstatus.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 estatus.NEstatus.lstatus diff in
-  metasenv, subst, { estatus with NEstatus.lstatus = lexicon_status }, cic
+  let estatus = LexiconEngine.set_proof_aliases estatus diff in
+   metasenv, subst, estatus, cic
 ;;
 
 
@@ -231,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
@@ -634,6 +633,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
    in
      UriManager.uri_of_string (baseuri ^ "/" ^ name)
   in
+(*
  let _try_new cic =
   (NCicLibrary.clear_cache ();
    NCicEnvironment.invalidate ();
@@ -688,14 +688,14 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~rdb:estatus.NEstatus.rstatus
+           ~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)
-           ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
-           ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases)
+           ~aliases:estatus#lstatus.LexiconEngine.aliases
+           ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
            (text,prefix_len,obj)
          with
          | [_,_,_,obj],_ ->
@@ -722,13 +722,13 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
        )
   )
  in 
+*)
 
 
  try
 (*   let time = Unix.gettimeofday () in  *)
 
 
-  let lexicon_status = estatus.NEstatus.lstatus in
   let (diff, metasenv, _, cic, _) =
     singleton "third"
       (CicDisambiguate.disambiguate_obj 
@@ -736,8 +736,8 @@ let disambiguate_obj estatus ?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
@@ -751,8 +751,8 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
 (*    try_new (Some cic);   *)
 
 
-  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
-  { estatus with NEstatus.lstatus = lexicon_status }, metasenv, cic
+  let estatus = LexiconEngine.set_proof_aliases estatus diff in
+   estatus, metasenv, cic
 
  with 
  | Sys.Break as exn -> raise exn
@@ -783,20 +783,18 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~mk_choice:ncic_mk_choice
       ~mk_implicit
       ~uri:(OCic2NCic.nuri_of_ouri uri)
-      ~rdb:estatus.NEstatus.rstatus
-      ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
-      ~universe:(Some estatus.NEstatus.lstatus.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 estatus.NEstatus.lstatus diff in
-  { estatus with NEstatus.lstatus = lexicon_status }, cic
+  let estatus = LexiconEngine.set_proof_aliases estatus diff in
+   estatus, cic
 ;;
   
 let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
   match cmd with
-   | GrafiteAst.NObj(loc,obj) -> estatus, metasenv, GrafiteAst.NObj(loc,obj)
    | GrafiteAst.Index(loc,key,uri) ->
-       let lexicon_status_ref = ref estatus.NEstatus.lstatus 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 =
@@ -807,41 +805,34 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
                  metasenv, Some t
        in
        let metasenv,key = disambiguate_term_option metasenv key in
-       { estatus with NEstatus.lstatus = !lexicon_status_ref }, 
-       metasenv,GrafiteAst.Index(loc,key,uri)
+        !lexicon_status_ref,metasenv,GrafiteAst.Index(loc,key,uri)
    | GrafiteAst.Select (loc,uri) -> 
         estatus, metasenv, GrafiteAst.Select(loc,uri)
    | GrafiteAst.Pump(loc,i) -> 
         estatus, metasenv, GrafiteAst.Pump(loc,i)
    | GrafiteAst.PreferCoercion (loc,t) -> 
-       let lexicon_status_ref = ref estatus.NEstatus.lstatus 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
-      { estatus with NEstatus.lstatus = !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 estatus.NEstatus.lstatus 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
-      { estatus with NEstatus.lstatus = !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 estatus.NEstatus.lstatus in
+       let lexicon_status_ref = ref estatus 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 _
+        !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 ->
        estatus,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->
@@ -849,7 +840,7 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
         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 estatus.NEstatus.lstatus 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 =
@@ -864,7 +855,7 @@ let disambiguate_command estatus ?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
-      { estatus with NEstatus.lstatus = !lexicon_status_ref }, metasenv,
+       !lexicon_status_ref, metasenv,
         GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 
 let disambiguate_macro