| NId of loc
| NIntro of loc * string
| NRewrite of loc * direction * CicNotationPt.term * npattern
+ | NGeneralize of loc * npattern
type ('term, 'lazy_term, 'reduction, 'ident) tactic =
(* Higher order tactics (i.e. tacticals) *)
NTactics.elim_tac
~what:(text,prefix_len,what)
~where:(text,prefix_len,where)
+ | GrafiteAst.NGeneralize (_loc, where) ->
+ NTactics.generalize_tac ~where:(text,prefix_len,where)
| GrafiteAst.NId _ -> (fun x -> x)
| GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
| GrafiteAst.NRewrite (_loc,dir,what,where) ->
GrafiteAst.NChange (loc, what, with_what)
| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
GrafiteAst.NElim (loc, what, where)
+ | IDENT "ngeneralize"; p=pattern_spec ->
+ GrafiteAst.NGeneralize (loc, p)
| IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
GrafiteAst.NRewrite (loc, dir, what, where)
| SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
status, (None,ctx,instance)
;;
+let mk_in_scope status t =
+ mk_meta status ~name:NCicMetaSubst.in_scope_tag (ctx_of t) (`Def t)
+;;
+
+let mk_out_scope n status t =
+ mk_meta status ~name:(NCicMetaSubst.out_scope_tag n) (ctx_of t) (`Def t)
+;;
+
(* the following unification problem will be driven by
- * select s argsno t pattern
+ * select s ~found:mk_in_scope ~postprocess:(mk_out_scope argsno) t pattern
*
* ? args = t
*
* where argsn = length args and the pattern matches t
+ *
+ * found is called on every selected term to map them
+ * postprocess is called on the entire term after selection
*)
-let select_term low_status argsno (name,context,term) (wanted,path) =
- let found status ctx t wanted =
+let select_term
+ low_status ~found ~postprocess (name,context,term) (wanted,path)
+=
+ let is_found status ctx t wanted =
(* we could lift wanted step-by-step *)
try true, unify status ctx (None, ctx, t) wanted
with
in
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:NCicMetaSubst.in_scope_tag
- ctx (`Def (None, ctx, t))
- in
- status, t
- else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
+ let b, status = is_found status ctx t wanted in
+ if b then
+ let status , (_,_,t) = found status (None, ctx, t) in
+ status, t
+ else
+ let _,_,_,subst,_ = status.pstatus in
+ match t with
+ | NCic.Meta (i,lc) when List.mem_assoc i subst ->
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ aux ctx status t
+ | NCic.Meta _ -> status, t
+ | _ ->
+ NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
in
aux ctx status t
in
in
let status, term = select low_status context path term in
let term = (name, context, term) in
- mk_meta status ~name:(NCicMetaSubst.out_scope_tag argsno) context (`Def term)
+ postprocess status term
;;
let analyse_indty status ty =
val instantiate: lowtac_status -> int -> cic_term -> lowtac_status
val select_term:
- lowtac_status -> int -> cic_term -> ast_term option * NCic.term ->
+ lowtac_status ->
+ found: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
+ postprocess: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
+ cic_term -> ast_term option * NCic.term ->
lowtac_status * cic_term
+val mk_in_scope: lowtac_status -> cic_term -> lowtac_status * cic_term
+val mk_out_scope: int -> lowtac_status -> cic_term -> lowtac_status * cic_term
+
val pp_tac_status: tac_status -> unit
(* end *)
{ status with pstatus = n,h,metasenv,subst,o }
;;
+let force f s = Lazy.force f s;;
+
let clear_tac names =
if names = [] then id_tac else distribute_tac (clear names)
;;
else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
;;
-let select0_tac ~where:(wanted,_,where) ~argsno =
+let select0_tac ~where:(wanted,_,where) ~job =
+ let found, postprocess =
+ match job with
+ | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
+ | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
+ in
distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let path =
match where with None -> NCic.Implicit `Term | Some where -> where
in
- let status, newgoalty = select_term status argsno goalty (wanted,path) in
+ let status, newgoalty =
+ select_term status ~found ~postprocess goalty (wanted,path)
+ in
let status, instance =
mk_meta status (ctx_of newgoalty) (`Decl newgoalty)
in
instantiate status goal instance)
;;
-let select_tac ~where ~argsno move_down_hyps =
+let select_tac ~where ~job move_down_hyps =
let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
let path =
match where with None -> NCic.Implicit `Term | Some where -> where in
if not move_down_hyps then
- select0_tac ~where:(wanted,hyps,Some path) ~argsno
+ select0_tac ~where:(wanted,hyps,Some path) ~job
else
let path =
List.fold_left
in
block_tac [
generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
- select0_tac ~where:(wanted,[],Some path) ~argsno;
+ select0_tac ~where:(wanted,[],Some path) ~job;
clear_tac (List.map fst hyps) ]
;;
-(*
let generalize_tac ~where =
- block_tac [ select_tac ~where true ; generalize0_tac ???? ]
+ let l = ref [] in
+ block_tac [
+ select_tac ~where ~job:(`Collect l) true;
+ force (lazy (distribute_tac (fun status goal ->
+ let goalty = get_goalty status goal in
+ (* unift (ctx_of goal) t s *)
+ instantiate status goal
+ (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ;
+ term_of_cic_term (List.hd !l) (ctx_of goalty) ]))
+ ))) ]
;;
-*)
let reopen status =
let path =
match where with None -> NCic.Implicit `Term | Some where -> where
in
- let status, newgoalty = select_term status 1 goalty (wanted,path) in
+ let status, newgoalty = assert false (*
+ select_term status 1 goalty (wanted,path)*) in
let status, in_scope, out_scope = reopen status in
let status = List.fold_left (exact with_what) status in_scope in
exec id_tac status goal)
;;
-let force f s = Lazy.force f s;;
-
let elim_tac ~what ~where =
let indtyinfo = ref None in
let sort = ref None in
atomic_tac (block_tac [
analyze_indty_tac ~what indtyinfo;
force (lazy (select_tac
- ~where ~argsno:((HExtlib.unopt !indtyinfo).rightno+1) true));
+ ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true));
print_tac "CIAO";
compute_goal_sort_tac;
print_tac "CIAO2";
match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
in
block_tac
- [ select_tac ~where ~argsno:2 true;
+ [ select_tac ~where ~job:(`Substexpand 2) true;
exact_tac
("",0,
Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
atomic_tac
(block_tac [
analyze_indty_tac ~what indtyinfo;
- select_tac ~where ~argsno:((HExtlib.unopt !indtyinfo).rightno+1) true;
+ force (lazy (select_tac
+ ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true));
distribute_tac (cases ~what) ])
;;
dir:[ `LeftToRight | `RightToLeft ] ->
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
NTacStatus.tactic
+val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic
projects / helm.git / commitdiff