let id_tac status = status ;;
let print_tac print_status message status =
- if print_status then pp_status status;
+ if print_status then pp_tac_status status;
prerr_endline message;
status
;;
let try_tac tac status =
+ let try_tac status =
try
tac status
with NTacStatus.Error _ ->
status
+ in
+ atomic_tac try_tac status
;;
let first_tac tacl status =
let status, instance =
mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
in
- instantiate status goal instance)
+ instantiate ~refine:false status goal instance)
;;
let select_tac ~where ~job move_down_hyps =
;;
let cut_tac t =
- block_tac [
+ atomic_tac (block_tac [
exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
branch_tac;
pos_tac [3]; exact_tac t;
shift_tac; pos_tac [2]; skip_tac;
- merge_tac ]
+ merge_tac ])
;;
let lapply_tac (s,n,t) =
lefts: NCic.term list;
rights: NCic.term list;
reference: NReference.reference;
+ term: NCic.term
}
;;
let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
let leftno = List.length lefts in
let rightno = List.length rights in
+ let status,what = term_of_cic_term status what (ctx_of goalty) in
indtyref := Some {
rightno = rightno; leftno = leftno; consno = consno;
- lefts = lefts; rights = rights; reference = r;
+ lefts = lefts; rights = rights; reference = r; term = what
};
exec id_tac status goal)
;;
(match !sort with NCic.Sort x -> x | _ -> assert false))
in
let eliminator =
- let _,_,w = what in
- Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ let what = (HExtlib.unopt !indtyinfo).term in
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
in
exact_tac ("",0,eliminator) status) ])
;;
`LeftToRight -> "eq" ^ suffix ^ "_r"
| `RightToLeft -> "eq" ^ suffix
in
+ let what = Ast.Appl [what; Ast.Implicit `Vector] in
block_tac
- [ select_tac ~where ~job:(`Substexpand 1) true;
+ [ select_tac ~where ~job:(`Substexpand 2) true;
exact_tac
("",0,
Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
if name = "_" then clear_tac [name] else id_tac ]
;;
+let name_counter = ref 0;;
+let intros_tac ?names_ref names s =
+ let names_ref, prefix =
+ match names_ref with | None -> ref [], "__" | Some r -> r, "H"
+ in
+ if names = [] then
+ repeat_tac
+ (fun s ->
+ incr name_counter;
+ (* TODO: generate better names *)
+ let name = prefix ^ string_of_int !name_counter in
+ let s = intro_tac name s in
+ names_ref := !names_ref @ [name];
+ s)
+ s
+ else
+ block_tac (List.map intro_tac names) s
+;;
+
let cases ~what status goal =
let gty = get_goalty status goal in
let status, what = disambiguate status (ctx_of gty) what None in
atomic_tac
(block_tac [
analyze_indty_tac ~what indtyinfo;
- (fun s -> select_tac
- ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
- distribute_tac (cases ~what) ])
+ (fun s ->
+ select_tac
+ ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true
+ s);
+ (fun s ->
+ distribute_tac
+ (cases ~what:("",0,Ast.NCic (HExtlib.unopt !indtyinfo).term)) s); ])
;;
let case1_tac name =
(match !sort with NCic.Sort x -> x | _ -> assert false))
in
let eliminator =
- let _,_,w = what in
- Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ let what = (HExtlib.unopt !indtyinfo).term in
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
in
exact_tac ("",0,eliminator) status) ])
;;