Partially restore the assume tactic

[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 5828bdea172b52e70743590f62d2662a83a8bc1c..f76b8b02a802e80a406e1d9b8321c47b5e2b9087 100644 (file)
--- 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,9 +398,9 @@ 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 =
@@ -481,6 +481,7 @@ 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
  in
   aux aux tac (* trick for non uniform recursion call *)
 ;;
@@ -549,6 +550,14 @@ let compute_relevance status uri =
       NCic.Inductive (ind,leftno,tys,attrs)
 ;;
 
+let extract_uris status uris =
+ List.fold_left
+  (fun status uri ->
+    let obj = NCicEnvironment.get_checked_obj status uri in
+     let status = eval_extract_obj status obj in
+      eval_extract_ocaml_obj status obj
+  ) status uris
+;;
 
 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   match cmd with
@@ -590,17 +599,15 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        in
        status, o_t, NotationPt.NCic ty, source, target
      in
-     let status, composites =
-      NCicCoercDeclaration.eval_ncoercion status name compose t ty source
-       target
-     in
-     let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
-     let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
-      eval_alias status (mode,aliases)
+      let cmd = 
+       GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target))
+      in
+      eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
   | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name compose t ty source
        target in
+     let status = extract_uris status composites in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
@@ -657,6 +664,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             | _ -> status)
          else
           status in
+        (* purge tinycals stack *)
+        let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+        let status = status#set_stack ninitial_stack in
 (*
          try 
            index_eq uri status
@@ -688,7 +698,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                 else
                   nstatus
                with
-               | MultiPassDisambiguator.DisambiguationError _ as e ->
+               | MultiPassDisambiguator.DisambiguationError _ ->
                   HLog.warn "error in disambiguating projection/eliminator";
                   status
                | NCicTypeChecker.TypeCheckerFailure _ ->
@@ -808,14 +818,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
                       status (name,true,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
-                 let status =
-                  List.fold_left
-                   (fun status uri ->
-                     let obj = NCicEnvironment.get_checked_obj status uri in
-                      let status = eval_extract_obj status obj in
-                       eval_extract_ocaml_obj status obj
-                   ) status nuris
-                 in
+                 let status = extract_uris status nuris in
                   eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
@@ -882,7 +885,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       else
         let status = status#set_ng_mode `ProofMode in
         let metasenv,subst,status,indty =
-          GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] (text,prefix_len,indty) in
+          GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] (text,prefix_len,indty) in
         let indtyno, (_,_,tys,_,_),leftno = match indty with
             NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
               indtyno, NCicEnvironment.get_checked_indtys status r, leftno
@@ -937,8 +940,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 =