- let status,t = term_of_cic_term status gty ctx in
- let build_status (pt, metasenv, subst) =
- let status = status#set_obj (n,h,metasenv,subst,o) in
- let gty = get_goalty status goal in
- instantiate status goal (mk_cic_term ctx pt)
- in
- List.map build_status
- (NCicParamod.fast_eq_check status metasenv subst ctx
- eq_cache (NCic.Rel ~-1,t))
+ let gname, ctx, gty = List.assoc goal metasenv in
+ let gty = NCicUntrusted.apply_subst subst ctx gty in
+ let build_status (pt, _, metasenv, subst) =
+ try
+ print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+ let stamp = Unix.gettimeofday () in
+ let metasenv, subst, pt, pty =
+ NCicRefiner.typeof status
+ (* (status#set_coerc_db NCicCoercion.empty_db) *)
+ metasenv subst ctx pt None in
+ print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
+ let metasenv, subst =
+ NCicUnification.unify status metasenv subst ctx gty pty
+ (* the previous code is much less expensive than directly refining
+ pt with expected type pty
+ in
+ prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty));
+ NCicRefiner.typeof
+ (status#set_coerc_db NCicCoercion.empty_db)
+ metasenv subst ctx pt (Some gty) *)
+ in
+ print (lazy (Printf.sprintf "Refined in %fs"
+ (Unix.gettimeofday() -. stamp)));
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
+ let subst = (goal,(gname,ctx,pt,pty)) :: subst in
+ Some (status#set_obj (n,h,metasenv,subst,o))
+ with
+ NCicRefiner.RefineFailure msg
+ | NCicRefiner.Uncertain msg ->
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ snd (Lazy.force msg))); None
+ | NCicRefiner.AssertFailure msg ->
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ Lazy.force msg)); None
+ | _ -> None
+ in
+ HExtlib.filter_map build_status
+ (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))