X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=9dd266ed95b50748fc2d64499daab1b2de167bf7;hb=433e66b381d1b89e48c05d517494fc300fd0abb5;hp=5086eb845c6424574c565f8471ecc96b216bac14;hpb=f811e07f481b135bd7c621c2d10a268dc35d599b;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 5086eb845..9dd266ed9 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -380,7 +380,7 @@ let index_eq_for_auto status uri =
 ;; 
 
 let inject_constraint =
- let basic_eval_add_constraint (u1,u2) 
+ let basic_eval_add_constraint (acyclic,u1,u2) 
      ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
      ~alias_only status
  =
@@ -390,7 +390,7 @@ let inject_constraint =
     (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment
      * and also to the storage (for undo/redo). During inclusion of compiled
      * files the storage must not be touched. *)
-    NCicEnvironment.add_lt_constraint u1 u2;
+    NCicEnvironment.add_lt_constraint acyclic u1 u2;
     status
   else
    status
@@ -398,12 +398,22 @@ let inject_constraint =
   GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint 
 ;;
 
-let eval_add_constraint status u1 u2 = 
- let status = NCicLibrary.add_constraint status u1 u2 in
-  NCicLibrary.dump_obj status (inject_constraint (u1,u2))
+let eval_add_constraint status acyclic u1 u2 = 
+ let status = NCicLibrary.add_constraint status acyclic u1 u2 in
+  NCicLibrary.dump_obj status (inject_constraint (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,6 +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,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 *)
 ;;
@@ -939,8 +965,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             eval_ncommand ~include_paths opts status
              ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
         | _ -> assert false)
-  | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
-      eval_add_constraint status [`Type,u1] [`Type,u2]
+  | GrafiteAst.NUnivConstraint (loc,acyclic,u1,u2) ->
+      eval_add_constraint status acyclic [`Type,u1] [`Type,u2]
   (* ex lexicon commands *)
   | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
      let cic_appl_pattern =