-let apply t (status,goal) =
- let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
- let name,context,gty = List.assoc goal metasenv in
- let metasenv, subst, lexicon_status, t =
- GrafiteDisambiguate.disambiguate_nterm (Some gty)
- status.lstatus context metasenv subst t
- in
- let subst, metasenv =
- (goal, (name, context, t, gty)):: subst,
- List.filter(fun (x,_) -> x <> goal) metasenv
+let letin_tac ~where:(_,_,(m,hyp,gp)) ~what:(_,_,w) name =
+ assert(m = None);
+ let where = Some w, [],
+ match gp with
+ | None -> Some Ast.Implicit
+ | Some where ->
+ Some
+ (List.fold_left
+ (fun t _ ->
+ Ast.Binder(`Pi,(Ast.Ident("_",None),Some Ast.UserInput),t))
+ where hyp)
+ in
+ block_tac [
+ generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyp);
+ exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
+ change_tac ~where:("",0,where) ~with_what:("",0,Ast.Ident (name,None))
+ ]
+;;
+
+let apply_tac = exact_tac;;
+
+type indtyinfo = {
+ rightno: int;
+ leftno: int;
+ consno: int;
+ lefts: NCic.term list;
+ rights: NCic.term list;
+ reference: NReference.reference;
+ }
+;;
+
+let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
+ let goalty = get_goalty status goal in
+ let status, what = disambiguate status what None (ctx_of goalty) in
+ let status, ty_what = typeof status (ctx_of what) what in
+ let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
+ let leftno = List.length rights in
+ let rightno = List.length rights in
+ indtyref := Some {
+ rightno = rightno; leftno = leftno; consno = consno;
+ lefts = lefts; rights = rights; reference = r;
+ };
+ exec id_tac status goal)
+;;
+
+let elim_tac ~what ~where =
+ let indtyinfo = ref None in
+ let sort = ref None in
+ let compute_goal_sort_tac = distribute_tac (fun status goal ->
+ let goalty = get_goalty status goal in
+ let status, goalsort = typeof status (ctx_of goalty) goalty in
+ sort := Some goalsort;
+ exec id_tac status goal)
+ in
+ atomic_tac (block_tac [
+ analyze_indty_tac ~what indtyinfo;
+ (fun s -> select_tac
+ ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
+ compute_goal_sort_tac;
+ (fun status ->
+ let sort = HExtlib.unopt !sort in
+ let ity = HExtlib.unopt !indtyinfo in
+ let NReference.Ref (uri, _) = ity.reference in
+ let istatus, sort = term_of_cic_term status.istatus sort (ctx_of sort) in
+ let status = { status with istatus = istatus } in
+ let name = NUri.name_of_uri uri ^
+ match sort with
+ | NCic.Sort NCic.Prop -> "_ind"
+ | NCic.Sort _ -> "_rect"
+ | _ -> assert false
+ in
+ let holes =
+ HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
+ let eliminator =
+ let _,_,w = what in
+ Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
+ in
+ exact_tac ("",0,eliminator) status) ])
+;;
+
+let rewrite_tac ~dir ~what:(_,_,what) ~where =
+ let name =
+ match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"