(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
+let debug s = prerr_endline (Lazy.force s);;
+let debug _ = ();;
+
module COT : Set.OrderedType with type t = NCic.term * int * int =
struct
type t = NCic.term * int * int
let index_coercion status c src tgt arity arg =
let db_src,db_tgt = status#coerc_db in
let data = (c,arity,arg) in
-(*
- prerr_endline ("INDEX:" ^
+
+ debug (lazy ("INDEX:" ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c);
-*)
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
+ string_of_int arg ^ " " ^ string_of_int arity));
+
let db_src = DB.index db_src src data in
let db_tgt = DB.index db_tgt tgt data in
status#set_coerc_db (db_src, db_tgt)
NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
in
(*
- prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s"
+ debug (lazy (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);
+ debug (lazy (
+ NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
assert false
in
index_coercion status c src tgt arity arg
| (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
(NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
| _ ->
-(*
- prerr_endline ("LOOK FOR COERCIONS: " ^
+
+ debug (lazy ("LOOK FOR COERCIONS: " ^
NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
- NCicPp.ppterm ~metasenv ~subst ~context expty);
-*)
+ NCicPp.ppterm ~metasenv ~subst ~context expty));
+
let set_src = DB.retrieve_unifiables db_src infty in
let set_tgt = DB.retrieve_unifiables db_tgt expty in
let candidates = CoercionSet.inter set_src set_tgt in
-(*
- prerr_endline ("CANDIDATES: " ^
+
+ debug (lazy ("CANDIDATES: " ^
String.concat "," (List.map (fun (t,_,_) ->
NCicPp.ppterm ~metasenv ~subst ~context t)
- (CoercionSet.elements candidates)));
-*)
+ (CoercionSet.elements candidates))));
+
List.map
(fun (t,arity,arg) ->
let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
let ty, metasenv, args =
NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
in
- (* prerr_endline (
+
+ debug (lazy (
NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
NCicPp.ppterm ~metasenv ~subst ~context
(NCicUntrusted.mk_appl t args) ^ " --- " ^
- string_of_int (List.length args) ^ " == " ^ string_of_int arg); *)
+ string_of_int (List.length args) ^ " == " ^ string_of_int arg));
+
metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
(CoercionSet.elements candidates)
;;