-let intro_case status gno gty depth cache name =
- (* let status = NTactics.focus_tac [gno] status in *)
- let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
- let open_goals = head_goals status#stack in
- assert (List.length open_goals = 1);
- let open_goal = List.hd open_goals in
- let ngty = get_goalty status open_goal in
- let ctx = ctx_of ngty in
- let t = mk_cic_term ctx (NCic.Rel 1) in
- let status, keys = keys_of_term status t in
- let cache = List.fold_left (add_to_th t) cache keys in
- debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
- incr candidate_no;
- (* XXX compute the sort *)
- [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]],
- cache
+let is_prod status =
+ let _, ctx, gty = current_goal status in
+ let _, raw_gty = term_of_cic_term status gty ctx in
+ match raw_gty with
+ | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
+ | _ -> None
+
+let intro ~depth status facts name =
+ let status = NTactics.intro_tac name status in
+ let _, ctx, ngty = current_goal status in
+ let t = mk_cic_term ctx (NCic.Rel 1) in
+ let status, keys = keys_of_term status t in
+ let facts = List.fold_left (add_to_th t) facts keys in
+ debug_print ~depth (lazy ("intro: "^ name));
+ (* unprovability is not stable w.r.t introduction *)
+ status, facts
+;;
+
+let rec intros_facts ~depth status facts =
+ match is_prod status with
+ | Some(name) ->
+ let status,facts =
+ intro ~depth status facts name
+ in intros_facts ~depth status facts
+ | _ -> status, facts
+;;
+
+let rec intros ~depth status (cache:cache) =
+ match is_prod status with
+ | Some _ ->
+ let status,facts =
+ intros_facts ~depth status cache.facts
+ in
+ (* we reindex the equation from scratch *)
+ let unit_eq =
+ index_local_equations status#eq_cache status in
+ (* under_inspection must be set to empty *)
+ status, init_cache ~facts ~unit_eq ()
+ | _ -> status, cache
+;;
+
+let reduce ~depth status g =
+ let n,h,metasenv,subst,o = status#obj in
+ let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
+ let ty = NCicUntrusted.apply_subst subst ctx ty in
+ let ty' = NCicReduction.whd ~subst ctx ty in
+ if ty = ty' then []
+ else
+ (debug_print ~depth
+ (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
+ let metasenv =
+ (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
+ in
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ incr candidate_no;
+ [(!candidate_no,Ast.Ident("__whd",None)),status])
+;;
+
+let do_something signature flags status g depth gty cache =
+ (* whd *)
+ let l = reduce ~depth status g in
+ (* backward aplications *)
+ let l1 = applicative_case depth signature status flags gty cache in
+ (* fast paramodulation *)
+ let l2 =
+ List.map
+ (fun s ->
+ incr candidate_no;
+ ((!candidate_no,Ast.Ident("__paramod",None)),s))
+ (auto_eq_check cache.unit_eq status)
+ in
+ (* states in l2 have have an set of subgoals: no point to sort them *)
+ l2 @ (sort_new_elems (l@l1)), cache