+(* ======================= utility functions ========================= *)
+module IntSet = Set.Make(struct type t = int let compare = compare end)
+
+let get_sgoalty status g =
+ let _,_,metasenv,subst,_ = status#obj in
+ try
+ let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
+ let ty = NCicUntrusted.apply_subst subst ctx ty in
+ let ctx = NCicUntrusted.apply_subst_context
+ ~fix_projections:true subst ctx
+ in
+ NTacStatus.mk_cic_term ctx ty
+ with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
+;;
+
+let deps status g =
+ let gty = get_sgoalty status g in
+ metas_of_term status gty
+;;
+
+let menv_closure status gl =
+ let rec closure acc = function
+ | [] -> acc
+ | x::l when IntSet.mem x acc -> closure acc l
+ | x::l -> closure (IntSet.add x acc) (deps status x @ l)
+ in closure IntSet.empty gl
+;;
+
+(* we call a "fact" an object whose hypothesis occur in the goal
+ or in types of goal-variables *)
+let is_a_fact status ty =
+ let status, ty, _ = saturate ~delta:max_int status ty in
+ 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 (i,_) -> IntSet.add i acc)
+ IntSet.empty metasenv
+ in IntSet.equal clos menv;;
+
+let is_a_fact_obj s uri =
+ let obj = NCicEnvironment.get_checked_obj uri in
+ match obj with
+ | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
+ is_a_fact s (mk_cic_term [] ty)
+(* aggiungere i costruttori *)
+ | _ -> false
+
+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
+
+
+(* =============================== paramod =========================== *)