First commit with new (incomplete) disambiguation engine.

[helm.git] / matitaB / components / grafite_engine / grafiteEngine.ml

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index 7febf874e3a25ac5defb81232663ace8756a3fe2..ff9d00b819e74ae57830a8bc4f234d004636ad93 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -54,7 +54,7 @@ let inject_unification_hint =
 ;;
 
 let eval_unification_hint status t n = 
- let metasenv,subst,status,t =
+ let newast,metasenv,subst,status,t =
   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst status subst [] t in
@@ -81,7 +81,9 @@ let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern
  in
  let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
  let diff =
-  [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
+  (* FIXME! the uri should be filled with something meaningful! *)
+  [DisambiguateTypes.Symbol (symbol, Some (None,dsc)),
+   GrafiteAst.Symbol_alias (symbol,None,dsc)]
  in
   GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
 ;;
@@ -113,6 +115,7 @@ let eval_interpretation status data=
 ;;
 
 let basic_eval_alias (mode,diff) status =
+  prerr_endline "basic_eval_alias";
   GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
 ;;
 
@@ -615,9 +618,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             List.fold_left
              (fun status (name,cpos,arity) ->
                try
-                 let metasenv,subst,status,t =
+                 let newast,metasenv,subst,status,t =
                   GrafiteDisambiguate.disambiguate_nterm status None [] [] []
-                   ("",0,NotationPt.Ident (name,None)) in
+                   ("",0,NotationPt.Ident (name,`Ambiguous)) in
                  assert (metasenv = [] && subst = []);
                  let status, nuris = 
                    NCicCoercDeclaration.
@@ -708,8 +711,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let metasenv,subst,status,sort = match sort with
         | None -> [],[],status,NCic.Sort NCic.Prop
         | Some s ->
-           GrafiteDisambiguate.disambiguate_nterm status None [] [] []
-            (text,prefix_len,s) 
+            let newast,metasenv,subst,status,sort = 
+              GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+              (text,prefix_len,s) 
+            in metasenv,subst,status,sort
       in
       assert (metasenv = []);
       let sort = NCicReduction.whd status ~subst [] sort in
@@ -721,7 +726,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             "ninverter: found target %s, which is not a sort"
              (status#ppterm ~metasenv ~subst ~context:[] sort))) in
       let status = status#set_ng_mode `ProofMode in
-      let metasenv,subst,status,indty =
+      let newast,metasenv,subst,status,indty =
        GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
         (text,prefix_len,indty) in
       let indtyno,(_,leftno,tys,_,_) =
@@ -768,11 +773,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
-         [DisambiguateTypes.Id id,spec]
-      | GrafiteAst.Symbol_alias (symb, instance, desc) ->
-         [DisambiguateTypes.Symbol (symb,instance),spec]
-      | GrafiteAst.Number_alias (instance,desc) ->
-         [DisambiguateTypes.Num instance,spec]
+         [DisambiguateTypes.Id (id,Some uri),spec]
+      | GrafiteAst.Symbol_alias (symb, uri, desc) ->
+         [DisambiguateTypes.Symbol (symb, Some (uri,desc)),spec]
+      | GrafiteAst.Number_alias (uri,desc) ->
+         [DisambiguateTypes.Num (Some (uri,desc)),spec]
      in
       let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
        eval_alias status (mode,diff)