+let type_of_tactic_term status ctx t =
+ let status,cicterm = disambiguate status ctx t `XTNone in
+ let (_,cicty) = typeof status ctx cicterm in
+ cicty
+
+let swap_first_two_goals_tac status =
+ let gstatus =
+ match status#stack with
+ | [] -> assert false
+ | (g,t,k,tag,p) :: s ->
+ match g with
+ | (loc1) :: (loc2) :: tl ->
+ ([loc2;loc1] @+ tl,t,k,tag,p) :: s
+ | _ -> assert false
+ in
+ status#set_stack gstatus
+
+let thesisbecomes t1 = we_need_to_prove t1 None
+;;
+
+let obtain id t1 status =
+ let goal = extract_first_goal_from_status status in
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let cicty = type_of_tactic_term status ctx t1 in
+ let _,ty = term_of_cic_term status cicty ctx in
+ let (_,_,t1) = t1 in
+ block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
+ `JustOne]));
+ swap_first_two_goals_tac;
+ branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
+ add_parameter_tac "volatile_context" "rewrite"
+ ]
+ status
+;;
+
+let conclude t1 status =
+ let goal = extract_first_goal_from_status status in
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let _,gty = term_of_cic_term status cicgty ctx in
+ match gty with
+ (* The first term of this Appl should probably be "eq" *)
+ NCic.Appl [_;_;plhs;_] ->
+ if alpha_eq_tacterm_kerterm t1 plhs status goal then
+ add_parameter_tac "volatile_context" "rewrite" status
+ else
+ fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
+ | _ -> fail (lazy "Your conclusion needs to be an equality")
+;;
+
+let rewritingstep rhs just last_step status =
+ let ctx = status_parameter "volatile_context" status in
+ if ctx = "rewrite" then
+ (
+ let goal = extract_first_goal_from_status status in
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let _,gty = term_of_cic_term status cicgty ctx in
+ let cicty = type_of_tactic_term status ctx rhs in
+ let _,ty = term_of_cic_term status cicty ctx in
+ let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
+ match just with
+ `Auto (univ, params) ->
+ let params =
+ if not (List.mem_assoc "timeout" params) then
+ ("timeout","3")::params
+ else params
+ in
+ let params' =
+ if not (List.mem_assoc "paramodulation" params) then
+ ("paramodulation","1")::params
+ else params
+ in
+ if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
+ else
+ first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
+ ~params:(univ, params') status goal]
+ | `Term just -> apply_tac just
+ | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
+ | `Proof -> id_tac
+ in
+ let plhs,prhs,prepare =
+ match gty with (* Extracting the lhs and rhs of the previous equality *)
+ NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
+ | _ -> fail (lazy "You are not building an equaility chain")
+ in
+ let continuation =
+ if last_step then
+ let todo = [just'] @ (done_continuation status) in
+ block_tac todo
+ else
+ let (_,_,rhs) = rhs in
+ block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
+ rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
+ in
+ prepare continuation
+ )
+ else
+ fail (lazy "You are not building an equality chain")
+;;
+
+let rec pp_metasenv_names (metasenv:NCic.metasenv) =
+ match metasenv with
+ [] -> ""
+ | hd :: tl ->
+ let n,conj = hd in
+ let meta_attrs,_,_ = conj in
+ let rec find_name_aux meta_attrs = match meta_attrs with
+ [] -> "Anonymous"
+ | hd :: tl -> match hd with
+ `Name n -> n
+ | _ -> find_name_aux tl
+ in
+ let name = find_name_aux meta_attrs
+ in
+ "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl)
+;;
+
+let print_goals_names_tac s (status:#NTacStatus.tac_status) =
+ let (_,_,metasenv,_,_) = status#obj in
+ prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
+
+(* Useful as it does not change the order in the list *)
+let rec list_change_assoc k v = function
+ [] -> []
+ | (k',_v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
+;;
+
+let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
+ let add_name_to_goal name goal metasenv =
+ let (mattrs,ctx,t) = try List.assoc goal metasenv with _ -> assert false in
+ let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
+ let newconj = (mattrs,ctx,t) in
+ list_change_assoc goal newconj metasenv
+ in
+ let new_goals =
+ (* It's important that this tactic is called before branching and right after the creation of
+ * the new goals, when they are still under focus *)
+ match status#stack with
+ [] -> fail (lazy "Can not add names to an empty stack")
+ | (g,_,_,_,_) :: _tl ->
+ let rec sublist n = function
+ [] -> []
+ | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
+ in
+ List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
+ in
+ let rec add_names_to_goals g cl metasenv =
+ match g,cl with
+ [],[] -> metasenv
+ | hd::tl, (_,consname,_)::tl' ->
+ add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
+ | _,_ -> fail (lazy "There are less goals than constructors")
+ in
+ let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+ let newmetasenv = add_names_to_goals new_goals !cl metasenv
+ in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
+;;