+(* we call a "fact" an object whose hypothesis occur in the goal
+ or in types of goal-variables *)
+let branch status ty =
+ let status, ty, metas = saturate ~delta:0 status ty in
+ noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
+ let g_metas = metas_of_term status ty in
+ let clos = menv_closure status g_metas in
+ (* let _,_,metasenv,_,_ = status#obj in *)
+ let menv =
+ List.fold_left
+ (fun acc m ->
+ let _, m = term_of_cic_term status m (ctx_of m) in
+ match m with
+ | NCic.Meta(i,_) -> IntSet.add i acc
+ | _ -> assert false)
+ IntSet.empty metas
+ in
+ (* IntSet.subset menv clos *)
+ IntSet.cardinal(IntSet.diff menv clos)
+
+let is_a_fact status ty = branch status ty = 0
+
+let is_a_fact_obj s uri =
+ let obj = NCicEnvironment.get_checked_obj uri in
+ match obj with
+ | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
+ is_a_fact s (mk_cic_term [] ty)
+(* aggiungere i costruttori *)
+ | _ -> false
+
+let is_a_fact_ast status subst metasenv ctx cand =
+ debug_print ~depth:0
+ (lazy ("------- checking " ^ CicNotationPp.pp_term cand));
+ let status, t = disambiguate status ctx ("",0,cand) None in
+ let status,t = term_of_cic_term status t ctx in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ is_a_fact status (mk_cic_term ctx ty)
+
+let current_goal status =
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals = 1);
+ let open_goal = List.hd open_goals in
+ let gty = get_goalty status open_goal in
+ let ctx = ctx_of gty in
+ open_goal, ctx, gty
+
+let height_of_ref (NReference.Ref (uri, x)) =
+ match x with
+ | NReference.Decl
+ | NReference.Ind _
+ | NReference.Con _
+ | NReference.CoFix _ ->
+ let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
+ height
+ | NReference.Def h -> h
+ | NReference.Fix (_,_,h) -> h
+;;
+
+(*************************** height functions ********************************)
+let fast_height_of_term t =
+ let h = ref 0 in
+ let rec aux =
+ function
+ NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
+ | NCic.Meta _ -> ()
+ | NCic.Rel _
+ | NCic.Sort _ -> ()
+ | NCic.Implicit _ -> assert false
+ | NCic.Const nref ->
+(*
+ prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
+ ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));
+*)
+ h := max !h (height_of_ref nref)
+ | NCic.Prod (_,t1,t2)
+ | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
+ | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+ | NCic.Appl l -> List.iter aux l
+ | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ in
+ aux t; !h
+;;
+
+let height_of_goal g status =
+ let ty = get_goalty status g in
+ let context = ctx_of ty in
+ let _, ty = term_of_cic_term status ty (ctx_of ty) in
+ let h = ref (fast_height_of_term ty) in
+ List.iter
+ (function
+ | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty)
+ | _, NCic.Def (bo,ty) ->
+ h := max !h (fast_height_of_term ty);
+ h := max !h (fast_height_of_term bo);
+ )
+ context;
+ !h
+;;
+
+let height_of_goals status =
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals > 0);
+ let h = ref 1 in
+ List.iter
+ (fun open_goal ->
+ h := max !h (height_of_goal open_goal status))
+ open_goals;
+ debug_print (lazy ("altezza sequente: " ^ string_of_int !h));
+ !h
+;;
+
+(* =============================== paramod =========================== *)
+let solve f status eq_cache goal =
+(*
+ let f =
+ if fast then NCicParamod.fast_eq_check
+ else NCicParamod.paramod in
+*)
+ let n,h,metasenv,subst,o = status#obj in
+ 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
+ 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 *)
+ 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\n" ^
+ snd (Lazy.force msg) ^
+ "\n in the environment\n" ^
+ NCicPp.ppmetasenv subst metasenv)); None
+ | NCicRefiner.AssertFailure msg ->
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ Lazy.force msg ^
+ "\n in the environment\n" ^
+ NCicPp.ppmetasenv subst metasenv)); None
+ | _ -> None
+ in
+ HExtlib.filter_map build_status
+ (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
+;;
+
+let fast_eq_check eq_cache status (goal:int) =
+ match solve NCicParamod.fast_eq_check status eq_cache goal with
+ | [] -> raise (Error (lazy "no proof found",None))
+ | s::_ -> s
+;;
+
+let dist_fast_eq_check eq_cache s =
+ NTactics.distribute_tac (fast_eq_check eq_cache) s
+;;
+
+let auto_eq_check eq_cache status =
+ try
+ let s = dist_fast_eq_check eq_cache status in
+ [s]
+ with
+ | Error _ -> debug_print (lazy ("no paramod proof found"));[]
+;;
+
+let index_local_equations eq_cache status =
+ debug_print (lazy "indexing equations");
+ let open_goals = head_goals status#stack in
+ let open_goal = List.hd open_goals in
+ let ngty = get_goalty status open_goal in
+ let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
+ let c = ref 0 in
+ List.fold_left
+ (fun eq_cache _ ->
+ c:= !c+1;
+ let t = NCic.Rel !c in
+ try
+ let ty = NCicTypeChecker.typeof [] [] ctx t in
+ if is_a_fact status (mk_cic_term ctx ty) then
+ (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+ NCicParamod.forward_infer_step eq_cache t ty)
+ else
+ (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
+ eq_cache)
+ with
+ | NCicTypeChecker.TypeCheckerFailure _
+ | NCicTypeChecker.AssertFailure _ -> eq_cache)
+ eq_cache ctx
+;;
+
+let fast_eq_check_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ dist_fast_eq_check unit_eq s
+;;
+
+let paramod eq_cache status goal =
+ match solve NCicParamod.paramod status eq_cache goal with
+ | [] -> raise (Error (lazy "no proof found",None))
+ | s::_ -> s
+;;
+
+let paramod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (paramod unit_eq) s
+;;
+
+let demod eq_cache status goal =
+ match solve NCicParamod.demod status eq_cache goal with
+ | [] -> raise (Error (lazy "no progress",None))
+ | s::_ -> s
+;;
+
+let demod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (demod unit_eq) s
+;;
+
+(*
+let fast_eq_check_tac_all ~params eq_cache status =
+ let g,_,_ = current_goal status in
+ let allstates = fast_eq_check_all status eq_cache g in
+ let pseudo_low_tac s _ _ = s in
+ let pseudo_low_tactics =
+ List.map pseudo_low_tac allstates
+ in
+ List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
+;;
+*)
+
+(*
+let demod status eq_cache goal =
+ let n,h,metasenv,subst,o = status#obj in
+ let gname, ctx, gty = List.assoc goal metasenv in
+ let gty = NCicUntrusted.apply_subst subst ctx gty in
+
+let demod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ dist_fast_eq_check unit_eq s
+*)
+
+(*************** subsumption ****************)
+