1) unification hint now takes NG terms (as it should have been from the very

   beginning)
2) refresh_uris_in_term is now passed to the constructor of the
   existential/universal data type in NCicLibrary
3) URIs are now refreshed in unification hint data

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 27afd3904c405c666484d4da50f792e83f5ae0df..fe060d41591b4ca1331c4c3e1e1b789c19c4c6bb 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -196,7 +196,7 @@ type ('term,'obj) command =
      int (* arity *) * int (* saturations *)
   | PreferCoercion of loc * 'term
   | Inverter of loc * string * 'term * bool list
-  | UnificationHint of loc * 'term * int (* term, precedence *)
+  | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
   | Default of loc * string * UriManager.uri list
   | Drop of loc
   | Include of loc * bool (* normal? *) * string 

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 98d33464b63405083c89664905c91248cfae315e..c1c83ee0921974b69eca8585dadb575feaf4c8ec 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -360,7 +360,7 @@ let pp_command ~term_pp ~obj_pp = function
   | Inverter (_,n,ty,params) ->
      "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
   | UnificationHint (_,t, n) -> 
-      "unification hint " ^ string_of_int n ^ " " ^ term_pp t
+      "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,true,path) -> "include \"" ^ path ^ "\""

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 98bfef9d6f5c60a6b445e2c2feb400032e1955f6..6e6a5bc733d364b9ac16179660129d6c0b8bd7ac 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -478,10 +478,19 @@ let basic_eval_unification_hint (t,n) status =
 ;;
 
 let inject_unification_hint =
- NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
+ let basic_eval_unification_hint (t,n) ~refresh_uri_in_term =
+  let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
+ in
+  NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
 ;;
 
 let eval_unification_hint status t n = 
+ let estatus = GrafiteTypes.get_estatus status in
+ let metasenv,subst,estatus,t =
+  GrafiteDisambiguate.disambiguate_nterm None estatus [] [] [] ("",0,t) in
+ assert (metasenv=[]);
+ let t = NCicUntrusted.apply_subst subst [] t in
+ let status = GrafiteTypes.set_estatus estatus status in
  let rstatus =
   basic_eval_unification_hint (t,n) (GrafiteTypes.get_rstatus status) in
  let status = GrafiteTypes.set_rstatus rstatus status in
@@ -721,8 +730,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       Inversion_principle.build_inverter ~add_obj status uri indty_uri params
      in
       res,`Old uris
-  | GrafiteAst.UnificationHint (loc, t, n) ->
-     eval_unification_hint status t n
+  | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,`Old []

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 64c4c8ebe9e2d84043224b891aee6ca861575804..0dfab7a371c376fadb1dda67e61bc94861db1c05 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -834,13 +834,7 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
        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 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
-      { estatus with NEstatus.lstatus = !lexicon_status_ref }, 
-      metasenv, GrafiteAst.UnificationHint (loc,t,n)
+   | GrafiteAst.UnificationHint _
    | GrafiteAst.Default _
    | GrafiteAst.Drop _
    | GrafiteAst.Include _

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 80b0911b2d41453ef2ff3b8789af110933e99806..cc13dde6e306959c18ba48d0a64f4a992c1e7012 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -79,7 +79,10 @@ module type Serializer =
  sig
   type status
   type obj
-  val register: string -> ('a -> status -> status) -> ('a -> obj)
+  val register:
+   string ->
+    ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
+    ('a -> obj)
   val serialize: baseuri:NUri.uri -> obj list -> unit
   val require: baseuri:NUri.uri -> status -> status
  end
@@ -97,7 +100,10 @@ module Serializer(S: sig type status end) =
    already_registered := tag :: !already_registered;
    require1 :=
     (fun (tag',data) as x ->
-     if tag=tag' then require (Obj.magic data) else !require1 x);
+     if tag=tag' then
+      require (Obj.magic data) ~refresh_uri_in_term
+     else
+      !require1 x);
    (fun x -> tag,Obj.repr x)
 
   let serialize = serialize

diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index 2d04b7d11f97caf667e4361387ccd29e8a7faa58..5266325656a7cdd14f21323a9d0201cf58d71be1 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -31,7 +31,10 @@ module type Serializer =
  sig
   type status
   type obj
-  val register: string -> ('a -> status -> status) -> ('a -> obj)
+  val register:
+   string ->
+    ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
+    ('a -> obj)
   val serialize: baseuri:NUri.uri -> obj list -> unit
   val require: baseuri:NUri.uri -> status -> status
  end

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index 9532ba985e67553e771ec495c032757226ea22fd..c09e08d3c6b506c4f144d929ce8c273975bb79a5 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -63,20 +63,17 @@ let index_hint hdb context t1 t2 precedence =
 let empty_db = DB.empty ;;
 
 let add_user_provided_hint db t precedence =
-  let u = UriManager.uri_of_string "cic:/foo/bar.con" in
   let c, a, b = 
     let rec aux ctx = function
       | NCic.Appl l ->
           (match List.rev l with
           | b::a::_ -> ctx, a, b
           | _ -> assert false)
-      | NCic.Prod (n,s,t) ->
-          aux ((n, NCic.Decl s) :: ctx) t
-      | NCic.LetIn (n,ty,t,b) -> 
-          aux  ((n, NCic.Def (t,ty)) :: ctx) b
+      | NCic.Prod (n,s,t) -> aux ((n, NCic.Decl s) :: ctx) t
+      | NCic.LetIn (n,ty,t,b) -> aux  ((n, NCic.Def (t,ty)) :: ctx) b
       | _ -> assert false
     in
-      aux [] (fst (OCic2NCic.convert_term u t))
+      aux [] t
   in
    index_hint db c a b precedence
 ;;

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index bb8bc6af16bd436edb7f0a52cb840c474fff1793..21820ace4f98ca6a70f81bdf9227de790aa25633 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -16,7 +16,7 @@ type db
 val index_hint: 
   db -> NCic.context -> NCic.term -> NCic.term -> int -> db
 
-val add_user_provided_hint : db -> Cic.term -> int -> db 
+val add_user_provided_hint : db -> NCic.term -> int -> db 
 
 val empty_db : db