added better debug_pps and add_user_provided_unification_hint

[helm.git] / helm / software / components / ng_refiner / nCicUnifHint.ml

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index 7961be96a80a234afed831403bdfb11cb7586de1..918ada5991202d0c82cb700a6e6f9a54c143b50d 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -51,11 +51,33 @@ let index_hint hdb context t1 t2 =
             NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t
         | _ -> assert false) 
      pair' context in
+  prerr_endline ("INDEXING: " ^ 
+    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
+    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data);
   DB.index hdb src data
 ;;
 
 let empty_db = DB.empty ;;
 
+let user_db = ref empty_db ;;
+
+let add_user_provided_hint t =
+  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
+      | _ -> assert false
+    in
+      aux [] (fst (OCic2NCic.convert_term u t))
+  in
+  user_db := index_hint !user_db c a b 
+;;
+
 let db () = 
   let combine f cmp l1 l2 =
    List.flatten
@@ -104,9 +126,9 @@ let db () =
   in
   List.fold_left 
     (fun db -> function 
-     |None -> db 
+     | None -> db 
      | Some (ctx,b1,b2) -> index_hint db ctx b1 b2)
-    empty_db hints
+    !user_db hints
 ;;