- let match_term status ctx (wanted : cic_term) t =
- let rec aux ctx status t =
- let b, status = found status ctx t wanted in
- if b then
- let status, (_,_,t) =
- mk_meta status ~name:in_scope_tag (`Ctx ctx) (`Def (None,ctx,t))
- in
- status, t
- else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
- in
- aux ctx status t
- in
- let rec select status ctx pat cic =
- match pat, cic with
- | NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) ->
- let status, t = select status ctx t1 t2 in
- let status, s = select status ctx s1 s2 in
- let ctx = (n, NCic.Def (s2,t2)) :: ctx in
- let status, b = select status ctx b1 b2 in
- status, NCic.LetIn (n,t,s,b)
- | NCic.Lambda (_,s1,t1), NCic.Lambda (n,s2,t2) ->
- let status, s = select status ctx s1 s2 in
- let ctx = (n, NCic.Decl s2) :: ctx in
- let status, t = select status ctx t1 t2 in
- status, NCic.Lambda (n,s,t)
- | NCic.Prod (_,s1,t1), NCic.Prod (n,s2,t2) ->
- let status, s = select status ctx s1 s2 in
- let ctx = (n, NCic.Decl s2) :: ctx in
- let status, t = select status ctx t1 t2 in
- status, NCic.Prod (n,s,t)
- | NCic.Appl l1, NCic.Appl l2 ->
- let status, l =
- List.fold_left2
- (fun (status,l) x y ->
- let status, x = select status ctx x y in
- status, x::l)
- (status,[]) l1 l2
- in
- status, NCic.Appl (List.rev l)
- | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) ->
- let status, t = select status ctx t1 t2 in
- let status, ot = select status ctx ot1 ot2 in
- let status, pl =
- List.fold_left2
- (fun (status,l) x y ->
- let status, x = select status ctx x y in
- status, x::l)
- (status,[]) pl1 pl2
- in
- status, NCic.Match (u,ot,t,List.rev pl)
- | NCic.Implicit `Hole, t ->
- (match wanted with
- | Some wanted ->
- let status, wanted = disambiguate status wanted None (`Ctx ctx) in
- match_term status ctx wanted t
- | None -> match_term status ctx (None,ctx,t) t)
- | NCic.Implicit _, t -> status, t
- | _,t ->
- fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[]
- ~context:[] ~subst:[] pat))
+ block_tac [
+ generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
+ select0_tac ~where:(wanted,[],Some path) ~job;
+ clear_tac (List.map fst hyps) ]
+;;
+
+let generalize_tac ~where =
+ let l = ref [] in
+ block_tac [
+ select_tac ~where ~job:(`Collect l) true;
+ (fun s -> distribute_tac (fun status goal ->
+ let goalty = get_goalty status goal in
+ let status,canon,rest =
+ match !l with
+ [] ->
+ (match where with
+ _,_,(None,_,_) -> fail (lazy "No term to generalize")
+ | txt,txtlen,(Some what,_,_) ->
+ let status, what =
+ disambiguate status (ctx_of goalty) (txt,txtlen,what) None
+ in
+ status,what,[]
+ )
+ | he::tl -> status,he,tl in
+ let status =
+ List.fold_left
+ (fun s t -> unify s (ctx_of goalty) canon t) status rest in
+ let status, canon = term_of_cic_term status canon (ctx_of goalty) in
+ instantiate status goal
+ (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
+ ) s) ]
+;;
+
+let cut_tac t =
+ 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 ])
+;;
+
+let lapply_tac (s,n,t) =
+ exact_tac (s,n, Ast.Appl [Ast.Implicit `JustOne; t])
+;;
+
+let reduce_tac ~reduction ~where =
+ let change status t =
+ match reduction with
+ | `Normalize perform_delta ->
+ normalize status
+ ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
+ | `Whd perform_delta ->
+ whd status
+ ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t