- let match_term m =
- let rec aux ctx status t =
- let b, status = eq ctx status t m in
- if b then
- let n,h,metasenv,subst,o = status.pstatus in
- let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
- let metasenv, instance, ty =
- NCicMetaSubst.mk_meta ~name:"expanded" metasenv ctx (`WithType ty)
- in
- let metasenv, subst =
- NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx
- t instance
- in
- let status = { status with pstatus = n,h,metasenv,subst,o } in
- status, instance
- else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
- in
- aux
- in
- let rec select status ctx pat cic =
- match pat, cic with
- | 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, l @ [x])
- (status,[]) l1 l2
- in
- status, NCic.Appl l
- | NCic.Implicit `Hole, t -> status, t
- | NCic.Implicit `Term, t ->
- let status, matched = disambiguate status matched None (Ctx ctx) in
- match_term matched ctx status t
- | _,t -> status, t
- in
- let status, term = select low_status context path term in
- let _,_,_,subst,_ = status.pstatus in
- let selections =
- HExtlib.filter_map
- (function (i,(Some "expanded",c,_,_)) -> Some i | _ -> None)
- subst
+ 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;
+ print_tac true "ha selezionato?";
+ (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 (txt,txtlen,what) None (ctx_of goalty)
+ 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 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