From: denes Date: Thu, 18 Jun 2009 15:26:24 +0000 (+0000) Subject: Added ntry and nassumption tactics X-Git-Tag: make_still_working~3847 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d6484aac4ff287a3a3646807801eab4b27cfb054;p=helm.git Added ntry and nassumption tactics --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 6bf050fec..524f99dc2 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -73,6 +73,8 @@ type ntactic = | NSkip of loc | NFocus of loc * int list | NUnfocus of loc + | NTry of loc * ntactic + | NAssumption of loc type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* Higher order tactics (i.e. tacticals) *) @@ -186,7 +188,7 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 23 +let magic = 24 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 5f1213fa4..7ececab72 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -89,7 +89,7 @@ let pp_just ~term_pp = | `Auto params -> pp_auto_params ~term_pp params ;; -let pp_ntactic ~map_unicode_to_tex = function +let rec pp_ntactic ~map_unicode_to_tex = function | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^ assert false ^ " " ^ assert false @@ -119,6 +119,8 @@ let pp_ntactic ~map_unicode_to_tex = function (String.concat " " (List.map string_of_int l)) | NUnfocus _ -> "##unfocus" | NSkip _ -> "##skip" + | NTry (_,tac) -> "ntry (" ^ pp_ntactic ~map_unicode_to_tex tac ^ ")" + | NAssumption _ -> "nassumption" ;; let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 65b6683eb..e02bd159f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -603,7 +603,7 @@ let eval_ng_punct (_text, _prefix_len, punct) = | GrafiteAst.Merge _ -> NTactics.merge_tac ;; -let eval_ng_tac (text, prefix_len, tac) = +let rec eval_ng_tac (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) | GrafiteAst.NAssert (_loc, seqs) -> @@ -654,6 +654,9 @@ let eval_ng_tac (text, prefix_len, tac) = | GrafiteAst.NSkip _ -> NTactics.skip_tac | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac + | GrafiteAst.NTry (_,tac) -> NTactics.try_tac + (eval_ng_tac (text, prefix_len, tac)) + | GrafiteAst.NAssumption _ -> NTactics.assumption_tac ;; let subst_metasenv_and_fix_names s = diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 688e21b8a..481d49f08 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -262,8 +262,10 @@ EXTEND G.NLetIn (loc,where,t,name) | kind = nreduction_kind; p = pattern_spec -> G.NReduce (loc, kind, p) - | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec -> + | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec -> G.NRewrite (loc, dir, what, where) + | IDENT "ntry"; LPAREN ; tac = SELF ; RPAREN -> G.NTry (loc,tac) + | IDENT "nassumption" -> G.NAssumption loc | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n) | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_") | SYMBOL "*" -> G.NCase1 (loc,"_") diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 0d18b6fab..0be24856e 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -224,12 +224,46 @@ let distribute_tac tac status = let atomic_tac htac = distribute_tac (exec htac) ;; +let try_tac tac status = + try + tac status + with NTacStatus.Error _ -> + status +;; + +let first_tac tacl status = + 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"))) + | Some x -> x +;; + let exact_tac t = 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 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) + in + exec htac status goal +;; + +let assumption_tac = + distribute_tac assumption +;; + let find_in_context name context = let rec aux acc = function | [] -> raise Not_found diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 7d8c15068..95cf5c26f 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -20,11 +20,13 @@ val merge_tac: NTacStatus.tactic val focus_tac: int list -> NTacStatus.tactic val unfocus_tac: NTacStatus.tactic val skip_tac: NTacStatus.tactic +val try_tac: NTacStatus.tactic -> NTacStatus.tactic val distribute_tac: NTacStatus.lowtactic -> NTacStatus.tactic val block_tac: NTacStatus.tactic list -> NTacStatus.tactic val apply_tac: NTacStatus.tactic_term -> NTacStatus.tactic +val assumption_tac: NTacStatus.tactic val change_tac: where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term -> NTacStatus.tactic