-(* 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 ****************)
-