- let status,t = term_of_cic_term status gty (ctx_of gty) in
- let status, l =
- List.fold_left
- (fun (status, l) t ->
- let status, t = disambiguate status (ctx_of gty) t None in
- let status, ty = typeof status (ctx_of t) t in
- let status, t = term_of_cic_term status t (ctx_of gty) in
- let status, ty = term_of_cic_term status ty (ctx_of ty) in
- (status, (t,ty) :: l))
- (status,[]) l
- in
- match
- NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
- with
- | [] -> raise (Error (lazy "no proof found",None))
- | (pt, metasenv, subst)::_ ->
- let status = status#set_obj (n,h,metasenv,subst,o) in
- instantiate status goal (mk_cic_term (ctx_of gty) pt)
-;;
-
-let auto_paramod_tac ~params status =
- NTactics.distribute_tac (auto_paramod ~params) status
-;;
-
-let fast_eq_check_all status eq_cache goal =
- let gty = get_goalty status goal in
- let ctx = ctx_of gty in
- let n,h,metasenv,subst,o = status#obj in
- 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
+ debug_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
+ debug_print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt)));
+ debug_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
+ debug_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))