]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
- init_cache_and_tables rewritten using the automation_cache
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index 1f32e8c9e2db06944bf86b6e4ca8938940093fca..c06750039c7dfafc4e83274dad4731d1746b36c3 100644 (file)
@@ -649,6 +649,22 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 *)
       let status = GrafiteTypes.add_moo_content [cmd] status in
       status,[] 
+  | GrafiteAst.Select (_,uri) as cmd ->
+      if List.mem cmd status.GrafiteTypes.moo_content_rev then status, []
+      else 
+       let cache = 
+         AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache
+           [] [] [] (CicUtil.term_of_uri uri) None
+       in
+       let status = { status with GrafiteTypes.automation_cache = cache } in
+       let status = GrafiteTypes.add_moo_content [cmd] status in
+       status, []
+  | GrafiteAst.Pump (_,steps) ->
+      let cache = 
+        AutomationCache.pump status.GrafiteTypes.automation_cache steps
+      in
+      let status = { status with GrafiteTypes.automation_cache = cache } in
+      status, []
   | GrafiteAst.PreferCoercion (loc, coercion) ->
      eval_prefer_coercion status coercion
   | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->