WARNING: partial commit.

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

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index c23e5acffd9d7270cd344fb18064e87409d1c550..143ac5e11f83949682d513dfd51bb0f39328f4c1 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -25,16 +25,22 @@
 
 (* $Id$ *)
 
-exception BaseUriNotSetYet
+class type g_status =
+  object
+   inherit LexiconEngine.g_status
+   inherit NCicCoercion.g_status
+  end
+
+class status =
+ object (self)
+  inherit LexiconEngine.status
+  inherit NCicCoercion.status
+  method set_grafite_disambiguate_status
+   : 'status. #g_status as 'status -> 'self
+      = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o
+ end
 
-type tactic = 
- (NotationPt.term, NotationPt.term, 
-  NotationPt.term GrafiteAst.reduction, string) 
-   GrafiteAst.tactic
-   
-type lazy_tactic = 
-  (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
-    GrafiteAst.tactic
+exception BaseUriNotSetYet
 
 let singleton msg = function
   | [x], _ -> x
@@ -48,20 +54,19 @@ let singleton msg = function
 let __Implicit = "__Implicit__"
 let __Closed_Implicit = "__Closed_Implicit__"
 
-let ncic_mk_choice = function
+let ncic_mk_choice status = function
   | LexiconAst.Symbol_alias (name, _, dsc) ->
      if name = __Implicit then
        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
      else if name = __Closed_Implicit then 
        dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
      else
-       DisambiguateChoices.lookup_symbol_by_dsc 
+       DisambiguateChoices.lookup_symbol_by_dsc status
         ~mk_implicit:(function 
            | true -> NCic.Implicit `Closed
            | false -> NCic.Implicit `Term)
         ~mk_appl:(function 
            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
-        ~term_of_uri:(fun _ -> assert false)
         ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
   | LexiconAst.Number_alias (_, dsc) -> 
@@ -127,7 +132,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing
         ~expty 
         ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
         ~lookup_in_library:nlookup_in_library
-        ~mk_choice:ncic_mk_choice
+        ~mk_choice:(ncic_mk_choice estatus)
         ~mk_implicit ~fix_instance
         ~description_of_alias:LexiconAst.description_of_alias
         ~context ~metasenv ~subst thing)
@@ -205,7 +210,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
     (NCicDisambiguate.disambiguate_obj
       ~lookup_in_library:nlookup_in_library
       ~description_of_alias:LexiconAst.description_of_alias
-      ~mk_choice:ncic_mk_choice
+      ~mk_choice:(ncic_mk_choice estatus)
       ~mk_implicit ~fix_instance
       ~uri
       ~rdb:estatus
@@ -215,20 +220,3 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
   let estatus = LexiconEngine.set_proof_aliases estatus diff in
    estatus, cic
 ;;
-let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)=
-  match cmd with
-   | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false
-   | GrafiteAst.Select (loc,uri) -> 
-        estatus, GrafiteAst.Select(loc,uri)
-   | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false
-   | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false
-   | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false
-   | GrafiteAst.Default _
-   | GrafiteAst.Drop _
-   | GrafiteAst.Include _
-   | GrafiteAst.Print _
-   | GrafiteAst.Qed _
-   | GrafiteAst.Set _ as cmd ->
-       estatus,cmd
-   | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
-   | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false