Added ntry and nassumption tactics

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 6bf050fec3f1ffb8013b369a4a768fe34eaf25ff..524f99dc2ff389356bb1de7b2f586f3cd3cf9a1e 100644 (file)
--- 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 5f1213fa48578d59c3970a8e8b9b40f8089037be..7ececab722b2b5ff61037ed76ea76df4c0276d81 100644 (file)
--- 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 65b6683ebc384e107331a0c42c51a5f0a9ca323b..e02bd159fe0d13544c5cc33252810b2d5bdcff0e 100644 (file)
--- 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 688e21b8ac1a89b703c2380c4f9b039792219df3..481d49f08db75716160add58d1d42958c41effef 100644 (file)
--- 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 0d18b6fabbfd80d1d2e1f34b5858701eddad2364..0be24856e7c4222ec0667b1c2ed8c1bd0493ac55 100644 (file)
--- 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 7d8c15068bf67c7985ed37846356edbeceaa77ed..95cf5c26f8c4c0e54bec5b8970bd55f89bc67359 100644 (file)
--- 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