X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=366a9fe16f61ce3666767bec64cc3985ee69e648;hb=8e905c34eb47a3f5fa67afa7997576d57588a50f;hp=0be24856e7c4222ec0667b1c2ed8c1bd0493ac55;hpb=d6484aac4ff287a3a3646807801eab4b27cfb054;p=helm.git diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 0be24856e..366a9fe16 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -13,7 +13,7 @@ open Printf -let debug = true +let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () open Continuationals.Stack @@ -22,14 +22,14 @@ module Ast = CicNotationPt let id_tac status = status ;; let print_tac print_status message status = - if print_status then pp_tac_status status; + if print_status then pp_status status; prerr_endline message; status ;; let dot_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | ([], _, [], _) :: _ as stack -> (* backward compatibility: do-nothing-dot *) @@ -43,12 +43,12 @@ let dot_tac status = (([ loc ], t, k, tag) :: s) | _ -> fail (lazy "can't use \".\" here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let branch_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | (g, t, k, tag) :: s -> match init_pos g with (* TODO *) @@ -56,12 +56,12 @@ let branch_tac status = | loc :: loc_tl -> ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let shift_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> (match g' with | [] -> fail (lazy "no more goals to shift") @@ -70,12 +70,12 @@ let shift_tac status = :: (loc_tl, t', k', tag) :: s)) | _ -> fail (lazy "can't shift goals here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let pos_tac i_s status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s when is_fresh loc -> @@ -84,35 +84,55 @@ let pos_tac i_s status = :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) | _ -> fail (lazy "can't use relative positioning here") in - { status with gstatus = new_gstatus } + 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 new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s when is_fresh loc -> (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s) | _ -> fail (lazy "can't use wildcard here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let merge_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) | _ -> fail (lazy "can't merge goals here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let focus_tac gs status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | s -> assert(gs <> []); let stack_locs = @@ -126,22 +146,23 @@ let focus_tac gs status = gs; (zero_pos gs, [], [], `FocusTag) :: deep_close gs s in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let unfocus_tac status = - let new_gstatus = - match status.gstatus with + 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 with gstatus = new_gstatus } + status#set_stack gstatus ;; let skip_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | (gl, t, k, tag) :: s -> let gl = List.map switch_of_loc gl in @@ -150,16 +171,17 @@ let skip_tac status = else ([],t,k,tag) :: s in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let block_tac l status = List.fold_left (fun status tac -> tac status) status l ;; + let compare_statuses ~past ~present = - let _,_,past,_,_ = past.pstatus in - let _,_,present,_,_ = present.pstatus in + let _,_,past,_,_ = past#obj in + let _,_,present,_,_ = present#obj in List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present), List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) ;; @@ -179,14 +201,17 @@ let compare_statuses ~past ~present = (e.g. the tactic could perform a global analysis of the set of goals) *) -let exec tac low_status g = +let exec tac (low_status : #lowtac_status) g = let stack = [ [0,Open g], [], [], `NoTag ] in - let status = tac { gstatus = stack ; istatus = low_status } in - status.istatus + let status = + (new NTacStatus.status low_status#obj stack)#set_estatus low_status + in + let status = tac status in + (low_status#set_estatus status)#set_obj status#obj ;; -let distribute_tac tac status = - match status.gstatus with +let distribute_tac tac (status : #tac_status) = + match status#stack with | [] -> assert false | (g, t, k, tag) :: s -> debug_print (lazy ("context length " ^string_of_int (List.length g))); @@ -210,7 +235,8 @@ let distribute_tac tac status = in aux s go gc loc_tl in - let s0, go0, gc0 = status.istatus, [], [] 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: " ^ String.concat " " (List.map string_of_int gon))); @@ -219,10 +245,19 @@ let distribute_tac tac status = let stack = (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s in - { gstatus = stack; istatus = sn } + ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn +;; + +let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;; + +let repeat_tac t s = + let rec repeat t (status : #tac_status as 'a) : 'a = + try repeat t (t status) + with NTacStatus.Error _ -> status + in + atomic_tac (repeat t) s ;; -let atomic_tac htac = distribute_tac (exec htac) ;; let try_tac tac status = try @@ -232,36 +267,30 @@ let try_tac tac status = ;; let first_tac tacl status = - let res = HExtlib.list_findopt - (fun tac _ -> - try Some (tac status) with - NTacStatus.Error _ -> None) tacl + let res = + HExtlib.list_findopt + (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl in match res with - | None -> raise (NTacStatus.Error (lazy("No tactic left"))) + | None -> fail (lazy "No tactics left") | Some x -> x ;; -let exact_tac t = distribute_tac (fun status goal -> +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) ;; -let assumption status goal = +let assumption_tac status = distribute_tac (fun status goal -> let gty = get_goalty status goal in let context = ctx_of gty in - let (htac:NTacStatus.tactic) = - first_tac (List.map - (fun (name,_) -> - exact_tac ("",0,(Ast.Ident (name,None)))) - context) + let htac = + first_tac + (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None)))) + context) in - exec htac status goal -;; - -let assumption_tac = - distribute_tac assumption + exec htac status goal) status ;; let find_in_context name context = @@ -286,14 +315,14 @@ let clear_tac names = fail (lazy ("hypothesis '" ^ name ^ "' not found"))) names in - let n,h,metasenv,subst,o = status.pstatus in + let n,h,metasenv,subst,o = status#obj in let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in - { status with pstatus = n,h,metasenv,subst,o }) + status#set_obj (n,h,metasenv,subst,o)) ;; let generalize0_tac args = if args = [] then id_tac - else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args)) + else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args)) ;; let select0_tac ~where:(wanted,hyps,where) ~job = @@ -392,6 +421,19 @@ let generalize_tac ~where = ) s) ] ;; +let cut_tac t = + 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 ] +;; + +let lapply_tac (s,n,t) = + exact_tac (s,n, Ast.Appl [Ast.Implicit `JustOne; t]) +;; + let reduce_tac ~reduction ~where = let change status t = match reduction with @@ -419,11 +461,15 @@ let change_tac ~where ~with_what = let letin_tac ~where ~what:(_,_,w) name = block_tac [ select_tac ~where ~job:(`Substexpand 1) true; - exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit)); + exact_tac + ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne)); ] ;; -let apply_tac = exact_tac;; +let apply_tac (s,n,t) = + let t = Ast.Appl [t; Ast.Implicit `Vector] in + exact_tac (s,n,t) +;; type indtyinfo = { rightno: int; @@ -435,12 +481,13 @@ type indtyinfo = { } ;; -let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal -> +let analyze_indty_tac ~what indtyref = + distribute_tac (fun status goal -> let goalty = get_goalty status goal in let status, what = disambiguate status what None (ctx_of goalty) 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 rights in + let leftno = List.length lefts in let rightno = List.length rights in indtyref := Some { rightno = rightno; leftno = leftno; consno = consno; @@ -449,58 +496,63 @@ let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal -> exec id_tac status goal) ;; -let elim_tac ~what ~where = +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 = term_of_cic_term status sort (ctx_of goalty) in + sortref := sort; + status) +;; + +let elim_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 None in - let compute_goal_sort_tac = distribute_tac (fun status goal -> - let goalty = get_goalty status goal in - let status, goalsort = typeof status (ctx_of goalty) goalty in - sort := Some goalsort; - exec id_tac status goal) - 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); - compute_goal_sort_tac; + sort_of_goal_tac sort; (fun status -> - let sort = HExtlib.unopt !sort in let ity = HExtlib.unopt !indtyinfo in let NReference.Ref (uri, _) = ity.reference in - let istatus, sort = term_of_cic_term status.istatus sort (ctx_of sort) in - let status = { status with istatus = istatus } in - let name = NUri.name_of_uri uri ^ - match sort with - | NCic.Sort NCic.Prop -> "_ind" - | NCic.Sort _ -> "_rect" - | _ -> assert false + let name = + NUri.name_of_uri uri ^ "_" ^ + snd (NCicElim.ast_of_sort + (match !sort with NCic.Sort x -> x | _ -> assert false)) in - let holes = - HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in let eliminator = let _,_,w = what in - Ast.Appl(Ast.Ident(name,None)::holes @ [ w ]) + Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ] in exact_tac ("",0,eliminator) status) ]) ;; -let rewrite_tac ~dir ~what:(_,_,what) ~where = +let rewrite_tac ~dir ~what:(_,_,what) ~where status = + let sortref = ref (NCic.Rel 1) in + let status = sort_of_goal_tac sortref status in + let suffix = "_" ^ snd (NCicElim.ast_of_sort + (match !sortref with NCic.Sort x -> x | _ -> assert false)) + in let name = - match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind" + match dir with + `LeftToRight -> "eq" ^ suffix ^ "_r" + | `RightToLeft -> "eq" ^ suffix in block_tac [ select_tac ~where ~job:(`Substexpand 1) true; exact_tac ("",0, - Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @ - [what]))] + Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@ + [what]))] status ;; let intro_tac name = block_tac [ exact_tac ("",0,(Ast.Binder (`Lambda, - (Ast.Ident (name,None),None),Ast.Implicit))); + (Ast.Ident (name,None),None),Ast.Implicit `JustOne))); if name = "_" then clear_tac [name] else id_tac ] ;; @@ -519,7 +571,8 @@ let cases ~what status goal = instantiate status goal t ;; -let cases_tac ~what ~where = +let cases_tac ~what:(txt,len,what) ~where = + let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in let indtyinfo = ref None in atomic_tac (block_tac [ @@ -538,6 +591,21 @@ let case1_tac name = if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] ;; +let constructor ?(num=1) ~args 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 + let ref = NReference.mk_constructor num r in + let t = + if args = [] then Ast.NRef ref else + 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 +;; + +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 = @@ -572,7 +640,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> ;; let assert_tac seqs status = - match status.gstatus with + match status#stack with | [] -> assert false | (g,_,_,_) :: s -> assert (List.length g = List.length seqs); @@ -588,28 +656,3 @@ let assert_tac seqs status = ) status ;; -let auto ~params:(l,_) status goal = - let gty = get_goalty status goal in - let n,h,metasenv,subst,o = status.pstatus 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 - let rdb = status.estatus in - let pt, metasenv, subst = - Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l - in - let status = { status with pstatus = 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 -;;