X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=c45e825a40359ff75fbe464416d19d9bc692760c;hb=65e8f1ba961ef81c5604168e7f1c891063c1ec76;hp=10fa168d492517123eff7b4b18861cb9827cfa47;hpb=2dd6e8f11fa3ac2995f326ecb742d9b4e8948fce;p=helm.git diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 10fa168d4..c45e825a4 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 @@ -419,12 +420,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 [3]; exact_tac t; shift_tac; pos_tac [2]; skip_tac; - merge_tac ] + merge_tac ]) ;; let lapply_tac (s,n,t) = @@ -540,7 +541,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status = | `RightToLeft -> "eq" ^ suffix 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@ @@ -555,6 +556,25 @@ 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 (ctx_of gty) what None in @@ -644,10 +664,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 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) ]) +;;