nasty change in the lexer/parser:

[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 53120a44d80940decbd54ad7d6b5932f6f7bd8cc..34b305ba54d06e7d3f514e9dc2b018bf783805db 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -38,12 +38,14 @@ let ppterm ctx t =
   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
   CicPp.pp t names
 ;;
+
 let is_propositional context sort = 
   match CicReduction.whd context sort with
   | Cic.Sort Cic.Prop 
   | Cic.Sort (Cic.CProp _) -> true
   | _-> false
 ;;
+
 let is_in_prop context subst metasenv ty =
   let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
   is_propositional context sort
@@ -516,10 +518,9 @@ let build_equalities auto context metasenv subst tables universe cache equations
       )
     (tables,[],cache) equations
 
-let close_more tables context status auto universe cache =
+let close_more tables context status auto signature universe cache =
   let proof, goalno = status in
   let _, metasenv,subst,_,_, _ = proof in  
-  let signature = MetadataQuery.signature_of metasenv goalno in
   let equations = 
     retrieve_equations false signature universe cache context metasenv 
   in
@@ -1631,18 +1632,27 @@ let try_candidate dbd
 ;;
 
 let applicative_case dbd
-  tables depth subst fake_proof goalno goalty metasenv context universe
-  cache flags
+  tables depth subst fake_proof goalno goalty metasenv context 
+  signature universe cache flags
 = 
-  let goalty_aux = 
+  (* let goalty_aux = 
     match goalty with
     | Cic.Appl (hd::tl) -> 
         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
     | _ -> goalty
-  in
+  in *)
+  let goalty_aux = goalty in
   let candidates = 
     get_candidates flags.skip_trie_filtering universe cache goalty_aux
   in
+  (* 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
+  let candidates = List.filter (only signature context metasenv) candidates 
+  in
   let tables, elems = 
     List.fold_left 
       (fun (tables,elems) cand ->
@@ -1690,10 +1700,9 @@ let try_smart_candidate dbd
 ;;
 
 let smart_applicative_case dbd
-  tables depth subst fake_proof goalno goalty metasenv context universe
-  cache flags
+  tables depth subst fake_proof goalno goalty metasenv context signature
+  universe cache flags
 = 
-  let signature = MetadataQuery.signature_of metasenv goalno in
   let goalty_aux = 
     match goalty with
     | Cic.Appl (hd::tl) -> 
@@ -1757,7 +1766,7 @@ let smart_applicative_case dbd
 ;;
 
 let equational_and_applicative_case dbd
-  universe flags m s g gty tables cache context 
+  signature universe flags m s g gty tables cache context 
 =
   let goalno, depth, sort = g in
   let fake_proof = mk_fake_proof m s g gty context in
@@ -1772,7 +1781,7 @@ let equational_and_applicative_case dbd
       else
         applicative_case dbd
           tables depth s fake_proof goalno 
-            gty m context universe cache flags
+            gty m context signature universe cache flags
     in
       elems@more_elems, tables, cache, flags            
   else
@@ -1780,10 +1789,10 @@ let equational_and_applicative_case dbd
       match LibraryObjects.eq_URI () with
       | Some _ ->
          smart_applicative_case dbd tables depth s fake_proof goalno 
-           gty m context universe cache flags
+           gty m context signature universe cache flags
       | None -> 
          applicative_case dbd tables depth s fake_proof goalno 
-           gty m context universe cache flags
+           gty m context signature universe cache flags
     in
       elems, tables, cache, flags  
 ;;
@@ -1880,7 +1889,8 @@ let filter_prune_hint c l =
     cache_reset_underinspection c,      
     List.filter (condition_for_prune_hint prune) l
 ;;
-let auto_main dbd tables context flags universe cache elems =
+
+let auto_main dbd tables context flags signature universe cache elems =
   auto_context := context;
   let rec aux tables flags cache (elems : status) =
     pp_status context elems;
@@ -1992,7 +2002,7 @@ let auto_main dbd tables context flags universe cache elems =
                     (* elems are possible computations for proving gty *)
                     let elems, tables, cache, flags =
                       equational_and_applicative_case dbd
-                        universe flags m s g gty tables cache context
+                        signature universe flags m s g gty tables cache context
                     in
                     if elems = [] then
                       (* this goal has failed *)
@@ -2041,6 +2051,14 @@ let auto_main dbd tables context flags universe cache elems =
 let
   auto_all_solutions dbd tables universe cache context metasenv gl flags 
 =
+  let signature =
+    List.fold_left 
+      (fun set g ->
+        MetadataConstraints.UriManagerSet.union set 
+            (MetadataQuery.signature_of metasenv g)
+       )
+      MetadataConstraints.UriManagerSet.empty gl 
+  in
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = 
     List.map 
@@ -2048,7 +2066,7 @@ let
   in
   let elems = [metasenv,[],1,[],goals,[]] in
   let rec aux tables solutions cache elems flags =
-    match auto_main dbd tables context flags universe cache elems with
+    match auto_main dbd tables context flags signature universe cache elems with
     | Gaveup (tables,cache) ->
         solutions,cache, tables
     | Proved (metasenv,subst,others,tables,cache) -> 
@@ -2075,12 +2093,21 @@ let
 
 (******************* AUTO ***************)
 
+
 let auto dbd flags metasenv tables universe cache context metasenv gl =
-  let initial_time = Unix.gettimeofday() in
+  let initial_time = Unix.gettimeofday() in  
+  let signature =
+    List.fold_left 
+      (fun set g ->
+        MetadataConstraints.UriManagerSet.union set 
+            (MetadataQuery.signature_of metasenv g)
+       )
+      MetadataConstraints.UriManagerSet.empty gl 
+  in
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
   let elems = [metasenv,[],1,[],goals,[]] in
-  match auto_main dbd tables context flags universe cache elems with
+  match auto_main dbd tables context flags signature universe cache elems with
   | Proved (metasenv,subst,_, tables,cache) -> 
       debug_print(lazy
         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
@@ -2101,19 +2128,32 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
   in
   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
+  in
   let tables,cache =
     if flags.close_more then
       close_more 
         tables context (proof, goal) 
-          (auto_all_solutions dbd) universe cache 
+          (auto_all_solutions dbd) signature universe cache 
     else tables,cache in
   let initial_time = Unix.gettimeofday() in
   let (_,oldmetasenv,_,_,_, _) = proof in
-  hint := None;
+    hint := None;
   let elem = 
     metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
   in
-  match auto_main dbd tables context flags universe cache [elem] with
+  match auto_main dbd tables context flags signature universe cache [elem] with
     | Proved (metasenv,subst,_, tables,cache) -> 
         debug_print (lazy 
           ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));