milestone in basic_2, λδ-2A reconstructed

[helm.git] / helm / software / components / library / coercDb.ml

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 312c2f1e49adb612332d6e0a1ddbcfa5923a8065..b7e3902296fc986edbffe93a7f5a161542c33e62 100644 (file)
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -50,6 +50,7 @@ type coerc_db = (* coercion_entry grouped by carrier with molteplicity *)
 let db =  ref ([] : coerc_db)
 let dump () = !db 
 let restore coerc_db = db := coerc_db
+let empty_coerc_db = []
 
 let rec coerc_carr_of_term t a =
  try
@@ -78,15 +79,14 @@ let eq_carr ?(exact=false) src tgt =
       | Cic.Prod _, true -> false
       | Cic.Prod _, false -> coarse_eq
       | _ -> coarse_eq) 
-  | Sort (Cic.Type _), Sort (Cic.Type _) -> true
-  | Sort src, Sort tgt when src = tgt -> true
+  | Sort _, Sort _ -> true
   | Fun _,Fun _ when not exact -> true (* only one Funclass *)
   | Fun i,Fun j when i = j -> true (* only one Funclass *)
   | _, _ -> false
 ;;
 
-let to_list () =
-  List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) !db
+let to_list db =
+  List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db
 ;;
 
 let rec myfilter p = function
@@ -166,3 +166,10 @@ let add_coercion (src,tgt,u,saturations,cpos) =
         db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest
 ;;
 
+let prefer u = 
+  let prefer (s,t,l) =
+    let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in
+    s,t,lb@la
+  in
+  db := List.map prefer !db;
+;;