+
+let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status =
+ let goal = extract_first_goal_from_status status in
+ let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
+ let indtyinfo = ref None in
+ let cl = ref [] in
+ try
+ assert_tac t2 None status goal (block_tac [
+ analyze_indty_tac ~what:npt1 indtyinfo;
+ cases_tac ~what:t1 ~where:("",0,(None,[],Some
+ Ast.UserInput));
+ print_goals_names_tac "Pre Adding";
+ (
+ fun status ->
+ let ity = HExtlib.unopt !indtyinfo in
+ cl := ity.cl; add_names_to_goals_tac cl status
+ );
+ print_goals_names_tac "Post Adding";
+ dot_tac] status)
+ with
+ | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+;;
+
+let byinduction t1 id = suppose t1 id None ;;
+
+let name_of_conj conj =
+ let mattrs,_,_ = conj in
+ let rec search_name mattrs =
+ match mattrs with
+ [] -> "Anonymous"
+ | hd::tl ->
+ match hd with
+ `Name n -> n
+ | _ -> search_name tl
+ in
+ search_name mattrs
+
+let rec loc_of_goal goal l =
+ match l with
+ [] -> fail (lazy "Reached the end")
+ | hd :: tl ->
+ let _,sw = hd in
+ let g = goal_of_switch sw in
+ if g = goal then hd
+ else loc_of_goal goal tl
+;;
+
+let focus_on_case_tac case status =
+ let goal = extract_first_goal_from_status status in
+ let (_,_,metasenv,_,_) = status#obj in
+ let rec goal_of_case case metasenv =
+ match metasenv with
+ [] -> fail (lazy "The given case does not exist")
+ | (goal,conj) :: tl ->
+ if name_of_conj conj = case then goal
+ else goal_of_case case tl
+ in
+ let goal_to_focus = goal_of_case case metasenv in
+ let gstatus =
+ match status#stack with
+ [] -> fail (lazy "There is nothing to prove")
+ | (g,t,k,tag) :: s ->
+ let loc = loc_of_goal goal_to_focus k in
+ let curloc = loc_of_goal goal g in
+ (((g @- [curloc]) @+ [loc]),t,([curloc] @+ (k @- [loc])),tag) :: s
+ in status#set_stack gstatus
+
+let case id l status =
+ let goal = extract_first_goal_from_status status in
+ let (_,_,metasenv,_,_) = status#obj in
+ let conj = NCicUtils.lookup_meta goal metasenv in
+ let name = name_of_conj conj in
+ let continuation =
+ let rec aux l =
+ match l with
+ [] -> [id_tac]
+ | (id,ty)::tl ->
+ (try_tac (assume id ("",0,ty) None)) :: (aux tl)
+ in
+ aux l
+ in
+ if name = id then block_tac continuation status
+ else block_tac ([focus_on_case_tac id] @ continuation) status
+;;
+
+let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
+
+(* vim: ts=2: sw=0: et:
+ * *)