removed debug code

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index 01f9b594b472b973b75f0d8839da570660d3f492..c797b2eee6d752ca6a5e868384d0c26ba3465663 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -28,6 +28,13 @@ let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
 let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
 
 let index_hint hdb context t1 t2 =
+  assert (
+    (match t1 with
+    | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
+    &&
+    (match t2 with
+    | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
+  );
   let pair' = pair t1 t2 in
   let data = 
     List.fold_left 
@@ -40,27 +47,19 @@ let index_hint hdb context t1 t2 =
     List.fold_left 
      (fun t (_,e) -> 
         match e with
-        | NCic.Decl _ -> NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t
+        | NCic.Decl _ -> 
+            NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t
         | _ -> assert false) 
      pair' context in
-  let _ = prerr_endline ("SONO PASSATO DI QUI") in
-
-(*
-  prerr_endline ("INDEX:" ^ 
-    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
-    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
-    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c);
-*)
   DB.index hdb src data
 ;;
 
 let empty_db = DB.empty ;;
 
 let db () = 
-  try let _,_,_,x,_,_ = NCicEnvironment.get_checked_def
+  let _,_,_,x,_,_ = NCicEnvironment.get_checked_def
     (NReference.reference_of_string "cic:/matita/tests/pullback/xxx.def(0)")
   in
-    prerr_endline "iiiiiiiiiiiiiiiiii";
   let rec decontextualize ctx = function
     | NCic.Prod (n,s,t) -> decontextualize ((n,NCic.Decl s)::ctx) t
     | t -> ctx, t
@@ -68,60 +67,36 @@ let db () =
     match (decontextualize [] x) with
     | ctx, NCic.Appl [_;_;a;b] -> index_hint empty_db ctx a b
     | _ -> assert false
-  with exn -> prerr_endline ("PIPPO" ^ Printexc.to_string exn); empty_db
-  
-(*  List.fold_left 
-    (fun db (_,tgt,clist) -> 
-       List.fold_left 
-         (fun db (uri,_,arg) ->
-            let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
-            let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
-            let src, tgt = 
-              let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
-              let scty, metasenv,_ = 
-                NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) 
-              in
-              match scty with
-              | NCic.Prod (_, src, tgt) -> 
-                 let tgt =
-                   NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
-                 in
-(*
-            prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s" 
-              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
-              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
-              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
-*)
-                src, tgt
-              | t -> 
-                  prerr_endline (
-                    NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
-                  assert false
-            in
-            index_coercion db c src tgt arity arg)
-         db clist)
-    (DB.empty,DB.empty) (CoercDb.to_list ())
- *)
 ;;
 
 
 let look_for_hint hdb metasenv subst context t1 t2 =
-
-  let candidates = DB.retrieve_unifiables hdb (pair t1 t2) in
-  let res = List.map
-      (fun ty ->
-          let ty, metasenv, _ = 
-           NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0 
-          in
-          match ty with
-          | NCic.Appl [_; t1; t2] -> 
-          prerr_endline ("candidate1: " ^ NCicPp.ppterm ~metasenv ~subst ~context t1);
-          prerr_endline ("candidate2: " ^ NCicPp.ppterm ~metasenv ~subst ~context t2);
-              
-              metasenv, t1, t2
-          | _ -> assert false)
-      (HintSet.elements candidates)
+(*
+  prerr_endline ("KEY1: "^NCicPp.ppterm ~metasenv ~subst ~context (pair t1 t2));
+  prerr_endline ("KEY2: "^NCicPp.ppterm ~metasenv ~subst ~context (pair t2 t1));
+  DB.iter hdb
+   (fun p ds ->
+      prerr_endline ("ENTRY: " ^
+      NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
+      String.concat "|" (List.map (NCicPp.ppterm ~metasenv:[] ~subst:[]
+      ~context:[]) (HintSet.elements ds))));
+*)
+  let candidates1 = DB.retrieve_unifiables hdb (pair t1 t2) in
+  let candidates2 = DB.retrieve_unifiables hdb (pair t2 t1) in
+  let candidates1 = 
+    List.map (fun ty -> 
+       true,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0) 
+    (HintSet.elements candidates1) 
+  in
+  let candidates2 = 
+    List.map (fun ty -> 
+       false,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0) 
+    (HintSet.elements candidates2) 
   in
-  let _ = prerr_endline ("DENTRO RICERCA: " ^ (string_of_int (List.length res))) in
-  res
+  List.map
+   (function 
+    | (true,(NCic.Appl [_; t1; t2],metasenv,_)) -> metasenv, t1, t2
+    | (false,(NCic.Appl [_; t1; t2],metasenv,_)) -> metasenv, t2, t1
+    | _ -> assert false)
+   (candidates1 @ candidates2)
 ;;