added better debug_pps and add_user_provided_unification_hint

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 7fbb781df0eff98e37a683788db4da372b5965c7..4e85f9bae069d64214ccb599d4d9579e6e83f62c 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -193,7 +193,7 @@ let _ =
     | NCicTypeChecker.TypeCheckerFailure s
     | NCicEnvironment.ObjectNotFound s
     | NCicEnvironment.BadConstraint s
-    | NCicEnvironment.BadDependency s as e -> 
+    | NCicEnvironment.BadDependency (s,_) as e -> 
        prerr_endline ("######### " ^ Lazy.force s);
        if not ignore_exc then raise e
     )

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
 ;;
 
 

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index 115ddfb15b27fa5ad3868e9bef6d54ff5149bbb7..2e94d9c8d0d65b0642d8f0a6b127ae6fb20e8a03 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -18,6 +18,7 @@ val index_hint:
 
   (* gets the old imperative coercion DB *)
 val db : unit -> db
+val add_user_provided_hint : Cic.term -> unit 
 
 val empty_db : db
 

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c6f4f6d9139cf1146f465791457cc800090c5712..838fad9dedfb4288d2d4dac99326da6f693bd1d5 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -249,12 +249,17 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
  (*D*) inside 'U'; try let rc =
    let fo_unif test_eq_only metasenv subst t1 t2 =
     (*D*) inside 'F'; try let rc =  
-     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context t2));
+     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
+         NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv
+         ~subst metasenv));
      if t1 === t2 then
        metasenv, subst
      else
        match (t1,t2) with
+       | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl [] 
+       | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> 
+           prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
+           assert false 
        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
            if NCicEnvironment.universe_leq a b then metasenv, subst
            else raise (fail_exc metasenv subst context t1 t2)