parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / auto.ml

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 34b305ba54d06e7d3f514e9dc2b018bf783805db..a89bbd4a164b9e1c673b9ea9a7a0e2620788904d 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -141,7 +141,7 @@ let is_an_equational_goal = function
   | _ -> false
 ;;
 
-type auto_params = Cic.term list * (string * string) list 
+type auto_params = Cic.term list option * (string * string) list 
 
 let elems = ref [] ;;
 
@@ -377,52 +377,53 @@ let init_cache_and_tables
            metasenv subst context t None)
       automation_cache ct
   in
-  if restricted_univ = [] then
-    let ct = 
-      if use_context then find_context_theorems context metasenv else [] 
-    in
-    let lt = 
-      match use_library, dbd with
-      | true, Some dbd -> find_library_theorems dbd metasenv goal 
-      | _ -> []
-    in
-    let cache = AutoCache.cache_empty in
-    let cache = cache_add_list cache context (ct@lt) in  
-    let automation_cache = 
-      add_list_to_tables metasenv subst automation_cache ct 
-    in
+  match restricted_univ with
+    | None ->
+       let ct = 
+         if use_context then find_context_theorems context metasenv else [] 
+       in
+       let lt = 
+         match use_library, dbd with
+           | true, Some dbd -> find_library_theorems dbd metasenv goal 
+           | _ -> []
+       in
+       let cache = AutoCache.cache_empty in
+       let cache = cache_add_list cache context (ct@lt) in  
+       let automation_cache = 
+         add_list_to_tables metasenv subst automation_cache ct 
+       in
 (*     AutomationCache.pp_cache automation_cache; *)
-    automation_cache.AutomationCache.univ, 
-    automation_cache.AutomationCache.tables, 
-    cache
-  else
-    let t_ty = 
-      List.map
-        (fun  t ->
-          let ty, _ = CicTypeChecker.type_of_aux' 
-            metasenv ~subst:[] context t CicUniv.oblivion_ugraph
-          in
-            t, ty)
-        restricted_univ
-    in
-    (* let automation_cache = AutomationCache.empty () in *) 
-    let automation_cache = 
-      let universe = Universe.empty in
-      let universe = 
-        Universe.index_list universe context t_ty
-      in
-      { automation_cache with AutomationCache.univ = universe }
-    in
-    let ct = 
-     if use_context then find_context_theorems context metasenv else t_ty
-    in
-    let automation_cache = 
-      add_list_to_tables metasenv subst automation_cache ct
-    in
+         automation_cache.AutomationCache.univ, 
+       automation_cache.AutomationCache.tables, 
+       cache
+    | Some restricted_univ ->
+       let t_ty = 
+         List.map
+            (fun  t ->
+               let ty, _ = CicTypeChecker.type_of_aux' 
+                metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+               in
+                t, ty)
+            restricted_univ
+       in
+         (* let automation_cache = AutomationCache.empty () in *) 
+       let automation_cache = 
+         let universe = Universe.empty in
+         let universe = 
+            Universe.index_list universe context t_ty
+         in
+           { automation_cache with AutomationCache.univ = universe }
+       in
+       let ct = 
+         if use_context then find_context_theorems context metasenv else t_ty
+       in
+       let automation_cache = 
+         add_list_to_tables metasenv subst automation_cache ct
+       in
     (* AutomationCache.pp_cache automation_cache; *)
-    automation_cache.AutomationCache.univ, 
-    automation_cache.AutomationCache.tables, 
-    cache_empty
+         automation_cache.AutomationCache.univ, 
+       automation_cache.AutomationCache.tables, 
+       cache_empty
 ;;
 
 let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast = 
@@ -956,7 +957,7 @@ let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache =
 (***************** applyS *******************)
 
 let apply_smart_aux 
- dbd automation_cache params proof goal newmeta' metasenv' subst
+ dbd automation_cache (params:auto_params) proof goal newmeta' metasenv' subst
   context term' ty termty goal_arity 
 = 
  let consthead,newmetasenv,arguments,_ =
@@ -1037,7 +1038,7 @@ let apply_smart_aux
         in
         match
           Saturation.solve_narrowing bag (proof'''',newmeta) active passive 
-            1 (*0 infinity*)
+            2 (*0 infinity*)
         with 
           | None, active, passive, bag -> 
               raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
@@ -1645,12 +1646,12 @@ let applicative_case dbd
   let candidates = 
     get_candidates flags.skip_trie_filtering universe cache goalty_aux
   in
-  (* if the goal is an equality we skip the congruence theorems *)
+  (* if the goal is an equality we skip the congruence theorems 
   let candidates =
     if is_equational_case goalty flags 
-    then List.filter not_default_eq_term candidates
-    else candidates
-  in
+    then List.filter not_default_eq_term candidates 
+    else candidates 
+  in *)
   let candidates = List.filter (only signature context metasenv) candidates 
   in
   let tables, elems = 
@@ -1673,7 +1674,7 @@ let try_smart_candidate dbd
 =
   let ppterm = ppterm context in
   try
-    let params = ([],[]) in
+    let params = (None,[]) in
     let automation_cache = { 
           AutomationCache.tables = tables ;
           AutomationCache.univ = Universe.empty; }
@@ -2129,17 +2130,20 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
   let _,metasenv,subst,_,_, _ = proof in
   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
   let signature = MetadataQuery.signature_of metasenv goal in
-  let signature = 
-    List.fold_left 
-      (fun set t ->
-         let ty, _ = 
-          CicTypeChecker.type_of_aux' metasenv context t 
-            CicUniv.oblivion_ugraph
-        in
-        MetadataConstraints.UriManagerSet.union set 
-          (MetadataConstraints.constants_of ty)
-       )
-      signature univ
+  let signature =
+    match univ with
+      | None -> signature
+      | Some l -> 
+         List.fold_left 
+           (fun set t ->
+               let ty, _ = 
+                CicTypeChecker.type_of_aux' metasenv context t 
+                  CicUniv.oblivion_ugraph
+              in
+                MetadataConstraints.UriManagerSet.union set 
+                  (MetadataConstraints.constants_of ty)
+           )
+           signature l
   in
   let tables,cache =
     if flags.close_more then