Added ntry and nassumption tactics

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index a0d8eba48a6b555718c45625968ccc6ddc451666..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
@@ -553,3 +587,29 @@ let assert_tac seqs status =
           [merge_tac])
      ) 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
+;;