added unification hints

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
new file mode 100644 (file)
index 0000000..01f9b59
--- /dev/null
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -0,0 +1,127 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
+
+module COT : Set.OrderedType with type t = NCic.term = 
+  struct
+        type t = NCic.term
+        let compare = Pervasives.compare
+  end
+
+module HintSet = Set.Make(COT)
+
+module DB = 
+  Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)
+
+type db = DB.t
+
+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 =
+  let pair' = pair t1 t2 in
+  let data = 
+    List.fold_left 
+     (fun t (n,e) -> 
+        match e with
+        | NCic.Decl ty -> NCic.Prod (n,ty,t)
+        | _ -> assert false) 
+      pair' context in
+  let src = 
+    List.fold_left 
+     (fun t (_,e) -> 
+        match e with
+        | 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
+    (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
+  in
+    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)
+  in
+  let _ = prerr_endline ("DENTRO RICERCA: " ^ (string_of_int (List.length res))) in
+  res
+;;

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
new file mode 100644 (file)
index 0000000..115ddfb
--- /dev/null
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -0,0 +1,28 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
+
+type db
+
+val index_hint: 
+  db -> NCic.context -> NCic.term -> NCic.term -> db
+
+  (* gets the old imperative coercion DB *)
+val db : unit -> db
+
+val empty_db : db
+
+val look_for_hint:
+    db ->
+    NCic.metasenv -> NCic.substitution -> NCic.context -> 
+    NCic.term -> NCic.term -> 
+      (NCic.metasenv * NCic.term * NCic.term) list