X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=f5ae3a721e4880a955d4be5463252cf4423e2a36;hb=12f96bd48b460d06f9858a334ee7c52d6831712f;hp=366a9fe16f61ce3666767bec64cc3985ee69e648;hpb=941dcd389bce3e0df96281e32238010cd758999a;p=helm.git diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 366a9fe16..f5ae3a721 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -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 @@ -277,9 +278,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 -> @@ -316,7 +315,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)) ;; @@ -370,7 +369,7 @@ 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) ;; @@ -397,7 +396,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 = @@ -407,7 +405,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,[] ) @@ -425,8 +423,8 @@ 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; + pos_tac [3]; exact_tac t; + shift_tac; pos_tac [2]; skip_tac; merge_tac ] ;; @@ -450,7 +448,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 @@ -481,10 +479,12 @@ type indtyinfo = { } ;; +let ref_of_indtyinfo iti = iti.reference;; + 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, 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 @@ -499,7 +499,7 @@ let analyze_indty_tac ~what indtyref = 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) @@ -558,7 +558,7 @@ let intro_tac name = 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 @@ -566,9 +566,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 = @@ -591,7 +589,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 @@ -601,15 +599,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 @@ -649,7 +645,7 @@ 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])