Add drafts for some tactics

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index be7154179812b0df00929c80a47541928f7c7819..9dd266ed95b50748fc2d64499daab1b2de167bf7 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -404,6 +404,16 @@ let eval_add_constraint status acyclic u1 u2 =
 ;;
 
 let eval_ng_tac tac =
+ let just_to_tacstatus_just just text prefix_len =
+    match just with
+    | `Term t -> `Term (text,prefix_len,t)
+    | `Auto (l,params) -> 
+    (
+        match l with
+        | None -> `Auto (None,params)
+        | Some l -> `Auto (Some (List.map (fun t -> (text,prefix_len,t)) l),params)
+    )
+ in
  let rec aux f (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
@@ -481,8 +491,22 @@ let eval_ng_tac tac =
       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
   |GrafiteAst.NRepeat (_,tac) ->
       NTactics.repeat_tac (f f (text, prefix_len, tac))
-  |GrafiteAst.Assume (_,id,t) -> Declarative.assume id t
-  |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose t id t1
+  |GrafiteAst.Assume (_,id,t,t1) -> Declarative.assume id (text,prefix_len,t) (match t1 with None ->
+  None | Some t1 -> (Some (text,prefix_len,t1)))
+  |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose (text,prefix_len,t) id (match t1 with None
+  -> None | Some t1 -> (Some (text,prefix_len,t1)))
+  |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
+  (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
+  Some t2 -> (Some (text,prefix_len,t2)))
+  |GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id
+  (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))
+  | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
+  (*
+  | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
+     Declarative.existselim just id1 t1 t2 id2
+  | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) ->
+     Declarative.andelim just t1 id1 t2 id2
+     *)
  in
   aux aux tac (* trick for non uniform recursion call *)
 ;;