X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=93d8c965c41e1b6181cf29d7f2808e20265992bc;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=01a57f0c45fa2851722bfac93e9f4e8bc8afceb6;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 01a57f0c4..93d8c965c 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -22,7 +22,7 @@ module Ast = CicNotationPt let id_tac status = status ;; let print_tac print_status message status = - if print_status then pp_status status; + if print_status then pp_tac_status status; prerr_endline message; status ;; @@ -46,13 +46,14 @@ let dot_tac status = status#set_stack gstatus ;; -let branch_tac status = +let branch_tac ?(force=false) status = let gstatus = match status#stack with | [] -> assert false | (g, t, k, tag) :: s -> match init_pos g with (* TODO *) - | [] | [ _ ] -> fail (lazy "too few goals to branch"); + | [] -> fail (lazy "empty goals") + | [_] when (not force) -> fail (lazy "too few goals to branch") | loc :: loc_tl -> ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s in @@ -87,6 +88,26 @@ let pos_tac i_s status = status#set_stack gstatus ;; +let case_tac lab status = + let gstatus = + match status#stack with + | [] -> assert false + | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + when is_fresh loc -> + let l_js = + List.filter + (fun curloc -> + let _,_,metasenv,_,_ = status#obj in + match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with + attrs,_,_ when List.mem (`Name lab) attrs -> true + | _ -> false) ([loc] @+ g') in + ((l_js, t , [],`BranchTag) + :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + | _ -> fail (lazy "can't use relative positioning here") + in + status#set_stack gstatus +;; + let wildcard_tac status = let gstatus = match status#stack with @@ -133,8 +154,9 @@ let unfocus_tac status = let gstatus = match status#stack with | [] -> assert false - | ([], [], [], `FocusTag) :: s -> s - | _ -> fail (lazy "can't unfocus, some goals are still open") + | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s + | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^ + Continuationals.Stack.pp s)) in status#set_stack gstatus ;; @@ -214,9 +236,7 @@ let distribute_tac tac (status : #tac_status) = in aux s go gc loc_tl in - let s0 = - (new NTacStatus.status status#obj ())#set_estatus - (status :> NEstatus.status) in + let s0 = (new NTacStatus.status status#obj ())#set_estatus status in let s0, go0, gc0 = s0, [], [] in let sn, gon, gcn = aux s0 go0 gc0 g in debug_print (lazy ("opened: " @@ -241,10 +261,13 @@ let repeat_tac t s = let try_tac tac status = + let try_tac status = try tac status with NTacStatus.Error _ -> status + in + atomic_tac try_tac status ;; let first_tac tacl status = @@ -258,9 +281,7 @@ let first_tac tacl status = ;; let exact_tac t : 's tactic = distribute_tac (fun 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) + instantiate_with_ast status goal t) ;; let assumption_tac status = distribute_tac (fun status goal -> @@ -297,7 +318,7 @@ let clear_tac names = names in let n,h,metasenv,subst,o = status#obj in - let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in + let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in status#set_obj (n,h,metasenv,subst,o)) ;; @@ -351,9 +372,9 @@ let select0_tac ~where:(wanted,hyps,where) ~job = let newgoalty = mk_cic_term newgoalctx newgoalty in let status, instance = - mk_meta status newgoalctx (`Decl newgoalty) + mk_meta status newgoalctx (`Decl newgoalty) `IsTerm in - instantiate status goal instance) + instantiate ~refine:false status goal instance) ;; let select_tac ~where ~job move_down_hyps = @@ -378,7 +399,6 @@ 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 = @@ -388,7 +408,7 @@ let generalize_tac ~where = _,_,(None,_,_) -> fail (lazy "No term to generalize") | txt,txtlen,(Some what,_,_) -> let status, what = - disambiguate status (txt,txtlen,what) None (ctx_of goalty) + disambiguate status (ctx_of goalty) (txt,txtlen,what) None in status,what,[] ) @@ -403,12 +423,12 @@ let generalize_tac ~where = ;; let cut_tac t = - block_tac [ + atomic_tac (block_tac [ exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]); branch_tac; - pos_tac [2]; exact_tac t; - shift_tac; pos_tac [1]; skip_tac; - merge_tac ] + pos_tac [3]; exact_tac t; + shift_tac; pos_tac [2]; skip_tac; + merge_tac ]) ;; let lapply_tac (s,n,t) = @@ -431,7 +451,7 @@ let reduce_tac ~reduction ~where = let change_tac ~where ~with_what = let change status t = - let status, ww = disambiguate status with_what None (ctx_of t) in + let status, ww = disambiguate status (ctx_of t) with_what None in let status = unify status (ctx_of t) t ww in status, ww in @@ -456,31 +476,30 @@ type indtyinfo = { rightno: int; leftno: int; consno: int; - lefts: NCic.term list; - rights: NCic.term list; reference: NReference.reference; } ;; +let ref_of_indtyinfo iti = iti.reference;; + let analyze_indty_tac ~what indtyref = - distribute_tac (fun status goal -> + distribute_tac (fun (status as orig_status) goal -> let goalty = get_goalty status goal in - let status, what = disambiguate status what None (ctx_of goalty) in + let status, what = disambiguate status (ctx_of goalty) what None 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 lefts in let rightno = List.length rights in indtyref := Some { - rightno = rightno; leftno = leftno; consno = consno; - lefts = lefts; rights = rights; reference = r; + rightno = rightno; leftno = leftno; consno = consno; reference = r; }; - exec id_tac status goal) + exec id_tac orig_status goal) ;; let sort_of_goal_tac sortref = distribute_tac (fun status goal -> let goalty = get_goalty status goal in let status,sort = typeof status (ctx_of goalty) goalty in - let sort = fix_sorts sort in + let status, sort = fix_sorts status sort in let status, sort = term_of_cic_term status sort (ctx_of goalty) in sortref := sort; status) @@ -521,8 +540,9 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status = `LeftToRight -> "eq" ^ suffix ^ "_r" | `RightToLeft -> "eq" ^ suffix in + let what = Ast.Appl [what; Ast.Implicit `Vector] in block_tac - [ select_tac ~where ~job:(`Substexpand 1) true; + [ select_tac ~where ~job:(`Substexpand 2) true; exact_tac ("",0, Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@ @@ -537,9 +557,28 @@ let intro_tac name = if name = "_" then clear_tac [name] else id_tac ] ;; +let name_counter = ref 0;; +let intros_tac ?names_ref names s = + let names_ref, prefix = + match names_ref with | None -> ref [], "__" | Some r -> r, "H" + in + if names = [] then + repeat_tac + (fun s -> + incr name_counter; + (* TODO: generate better names *) + let name = prefix ^ string_of_int !name_counter in + let s = intro_tac name s in + names_ref := !names_ref @ [name]; + s) + s + else + block_tac (List.map intro_tac names) s +;; + let cases ~what status goal = let gty = get_goalty status goal in - let status, what = disambiguate status what None (ctx_of gty) in + let status, what = disambiguate status (ctx_of gty) what None in let status, ty = typeof status (ctx_of what) what in let status, (ref, consno, _, _) = analyse_indty status ty in let status, what = term_of_cic_term status what (ctx_of gty) in @@ -547,9 +586,7 @@ let cases ~what status goal = NCic.Match (ref,NCic.Implicit `Term, what, HExtlib.mk_list (NCic.Implicit `Term) consno) in - let ctx = ctx_of gty in - let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in - instantiate status goal t + instantiate status goal (mk_cic_term (ctx_of gty) t) ;; let cases_tac ~what:(txt,len,what) ~where = @@ -572,7 +609,7 @@ let case1_tac name = if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] ;; -let constructor ?(num=1) ~args status goal = +let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal -> if num < 1 then fail (lazy "constructor numbers begin with 1"); let gty = get_goalty status goal in let status, (r,_,_,_) = analyse_indty status gty in @@ -582,15 +619,13 @@ let constructor ?(num=1) ~args status goal = Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector] ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args)) in - exec (apply_tac ("",0,t)) status goal + exec (apply_tac ("",0,t)) status goal) ;; -let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);; - let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let gty = get_goalty status goal in let eq status ctx t1 t2 = - let status,t1 = disambiguate status t1 None ctx in + let status,t1 = disambiguate status ctx t1 None in let status,t1 = apply_subst status ctx t1 in let status,t1 = term_of_cic_term status t1 ctx in let t2 = mk_cic_term ctx t2 in @@ -630,37 +665,33 @@ let assert_tac seqs status = | [seq] -> assert0_tac seq | _ -> block_tac - (branch_tac:: + ((branch_tac ~force:false):: HExtlib.list_concat ~sep:[shift_tac] (List.map (fun seq -> [assert0_tac seq]) seqs)@ [merge_tac]) ) status ;; -let auto ~params:(l,_) status goal = - let gty = get_goalty status goal in - let n,h,metasenv,subst,o = status#obj in - let status,t = term_of_cic_term status gty (ctx_of gty) in - let status, l = - List.fold_left - (fun (status, l) t -> - let status, t = disambiguate status t None (ctx_of gty) in - let status, ty = typeof status (ctx_of t) t in - let status, t = term_of_cic_term status t (ctx_of gty) in - let status, ty = term_of_cic_term status ty (ctx_of ty) in - (status, (t,ty) :: l)) - (status,[]) l - in - match - NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l - with - | [] -> raise (NTacStatus.Error (lazy "no proof found",None)) - | (pt, metasenv, subst)::_ -> - let status = status#set_obj (n,h,metasenv,subst,o) in - instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt) -;; - -let auto_tac ~params status = - distribute_tac (auto ~params) status +let inversion_tac ~what:(txt,len,what) ~where = + let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in + let indtyinfo = ref None in + let sort = ref (NCic.Rel 1) in + atomic_tac (block_tac [ + analyze_indty_tac ~what indtyinfo; + (fun s -> select_tac + ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s); + sort_of_goal_tac sort; + (fun status -> + let ity = HExtlib.unopt !indtyinfo in + let NReference.Ref (uri, _) = ity.reference in + let name = + NUri.name_of_uri uri ^ "_inv_" ^ + snd (NCicElim.ast_of_sort + (match !sort with NCic.Sort x -> x | _ -> assert false)) + in + let eliminator = + let _,_,w = what in + Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ] + in + exact_tac ("",0,eliminator) status) ]) ;; -