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
| 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
| (src,tgt,l)::tl ->
assert (tl = []); (* not sure, this may be a feature *)
if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then
- let l = List.map
+ let l =
+ let l =
+ (* this code reorders the list so that adding an already declared
+ * coercion moves it to the begging of the list *)
+ let item = List.find (fun (x,_,_,_) -> UriManager.eq u x) l in
+ let rest=List.filter (fun (x,_,_,_) -> not (UriManager.eq u x)) l in
+ item :: rest
+ in
+ List.map
(fun (x,n,x_saturations,x_cpos) as e ->
if UriManager.eq u x then
(* not sure, this may be a feature *)
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;
+;;