+let select ~where status goal =
+ let goalty = get_goalty status goal in
+ let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
+ let path =
+ match where with None -> NCic.Implicit `Term | Some where -> where
+ in
+ let status, newgoalty = select_term status goalty (wanted,path) in
+ let status, instance =
+ mk_meta status (ctx_of newgoalty) (`Decl newgoalty)
+ in
+ instantiate status goal instance
+;;
+
+let select_tac ~where = distribute_tac (select ~where) ;;
+
+let exact t status goal =
+ let goalty = get_goalty status goal in
+ let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
+ instantiate status goal t
+;;
+
+let exact_tac t = distribute_tac (exact t) ;;
+
+let reopen status =
+ let n,h,metasenv,subst,o = status.pstatus in
+ let subst, newm =
+ List.partition
+ (function (_,(Some tag,_,_,_)) ->
+ tag <> in_scope_tag && tag <> out_scope_tag
+ | _ -> true)
+ subst
+ in
+ let in_m, out_m =
+ List.partition
+ (function (_,(Some tag,_,_,_)) -> tag = in_scope_tag | _ -> assert false)
+ newm
+ in
+ let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in
+ let in_m = List.map fst in_m in
+ let out_m = match out_m with [i] -> i | _ -> assert false in
+ { status with pstatus = n,h,metasenv,subst,o }, in_m, out_m
+;;
+
+let change ~where ~with_what status goal =
+ let goalty = get_goalty status goal in
+ let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
+ let path =
+ match where with None -> NCic.Implicit `Term | Some where -> where
+ in
+ let status, newgoalty = select_term status 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
+
+ let j,(n,cctx,bo,_) = out_scope in
+ let _ = typeof status (ctx_of goalty) (Obj.magic (n,cctx,bo)) in
+
+ let n,h,metasenv,subst,o = status.pstatus in
+ let subst = out_scope :: subst in
+ let status = { status with pstatus = n,h,metasenv,subst,o } in
+
+ let status, instance =
+ mk_meta status (ctx_of newgoalty) (`Decl newgoalty)
+ in
+ instantiate status goal instance
+;;
+
+let apply t status goal = exact t status goal;;
+
+let apply_tac t = distribute_tac (apply t) ;;
+let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;;
+
+let elim_tac ~what ~where status =
+ block_tac
+ [ select_tac ~where;
+ distribute_tac (fun status goal ->
+ let goalty = get_goalty status goal in
+ let status, what =
+ disambiguate status what None (ctx_of goalty) in
+ let _ty_what = typeof status (ctx_of what) what in
+ (* check inductive... find eliminator *)
+ let w = (*astify what *) CicNotationPt.Ident ("m",None) in
+ let holes = [
+ CicNotationPt.Implicit;CicNotationPt.Implicit;CicNotationPt.Implicit]
+ in
+ let eliminator =
+ CicNotationPt.Appl(CicNotationPt.Ident("nat_ind",None)::holes @ [ w ])
+ in
+ exec (apply_tac ("",0,eliminator)) status goal) ]
+ status
+;;
+
+let intro_tac name =
+ exact_tac
+ ("",0,(CicNotationPt.Binder (`Lambda,
+ (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
+;;
+
+let case ~what status goal =
+ let gty = get_goalty status goal in
+ let status, what = disambiguate status what None (ctx_of gty) in
+ let ty = typeof status (ctx_of what) what in
+ let ref, consno, left, right = analyse_indty status ty in
+ let t =
+ NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,
+ HExtlib.mk_list (NCic.Implicit `Term) consno)