]> matita.cs.unibo.it Git - helm.git/commitdiff
auto rewritten with only one tail recursive function.
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 May 2007 15:45:59 +0000 (15:45 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 May 2007 15:45:59 +0000 (15:45 +0000)
this allows to have a GUI to drive the procedure.
a new measure size has been added, and width changed its meaning.
a bunch of unfold lt added to library_auto.

25 files changed:
helm/software/components/acic_procedural/.depend
helm/software/components/acic_procedural/.depend.opt
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/autoCache.ml
helm/software/components/tactics/autoTypes.ml
helm/software/components/tactics/autoTypes.mli
helm/software/components/tactics/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineHelpers.mli
helm/software/matita/.depend
helm/software/matita/library/decidable_kit/decidable.ma
helm/software/matita/library/demo/power_derivative.ma
helm/software/matita/library/nat/factorization.ma
helm/software/matita/library_auto/auto/Z/times.ma
helm/software/matita/library_auto/auto/nat/congruence.ma
helm/software/matita/library_auto/auto/nat/euler_theorem.ma
helm/software/matita/library_auto/auto/nat/factorization.ma
helm/software/matita/library_auto/auto/nat/fermat_little_theorem.ma
helm/software/matita/library_auto/auto/nat/gcd.ma
helm/software/matita/library_auto/auto/nat/nth_prime.ma
helm/software/matita/library_auto/auto/nat/ord.ma
helm/software/matita/library_auto/auto/nat/primes.ma
helm/software/matita/matita.glade
helm/software/matita/matita.ml
helm/software/matita/matitaAutoGui.ml [new file with mode: 0644]

index 1de52479db5345b234e473b1d34a3a75d5e1d4cc..f0b67ebc3660729e6fc732470de5fcbee648ed6d 100644 (file)
@@ -6,13 +6,13 @@ proceduralOptimizer.cmo: proceduralHelpers.cmi proceduralClassify.cmi \
     proceduralOptimizer.cmi 
 proceduralOptimizer.cmx: proceduralHelpers.cmx proceduralClassify.cmx \
     proceduralOptimizer.cmi 
-proceduralTypes.cmo: proceduralTypes.cmi 
-proceduralTypes.cmx: proceduralTypes.cmi 
+proceduralTypes.cmo: proceduralHelpers.cmi proceduralTypes.cmi 
+proceduralTypes.cmx: proceduralHelpers.cmx proceduralTypes.cmi 
 proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralConversion.cmi 
-acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
-    proceduralClassify.cmi acic2Procedural.cmi 
-acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
-    proceduralClassify.cmx acic2Procedural.cmi 
+acic2Procedural.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
+    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
+    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
index 1de52479db5345b234e473b1d34a3a75d5e1d4cc..f0b67ebc3660729e6fc732470de5fcbee648ed6d 100644 (file)
@@ -6,13 +6,13 @@ proceduralOptimizer.cmo: proceduralHelpers.cmi proceduralClassify.cmi \
     proceduralOptimizer.cmi 
 proceduralOptimizer.cmx: proceduralHelpers.cmx proceduralClassify.cmx \
     proceduralOptimizer.cmi 
-proceduralTypes.cmo: proceduralTypes.cmi 
-proceduralTypes.cmx: proceduralTypes.cmi 
+proceduralTypes.cmo: proceduralHelpers.cmi proceduralTypes.cmi 
+proceduralTypes.cmx: proceduralHelpers.cmx proceduralTypes.cmi 
 proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralConversion.cmi 
-acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
-    proceduralClassify.cmi acic2Procedural.cmi 
-acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
-    proceduralClassify.cmx acic2Procedural.cmi 
+acic2Procedural.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
+    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
+    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
index c2d933b0a091750b5205587faddbf872984f7216..3bec5b0444d47e53f6bab870eb6d6b5ad36dffd6 100644 (file)
 open AutoTypes;;
 open AutoCache;;
 
-let debug = false;;
+let debug = true;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
+let elems = ref [] ;;
+
+(* closing a term w.r.t. its metavariables
+   very naif version: it does not take dependencies into account *)
+
+let naif_closure t metasenv context =
+  let metasenv = ProofEngineHelpers.sort_metasenv metasenv in
+  let n = List.length metasenv in
+  let what = List.map (fun (i,cc,ty) -> Cic.Meta(i,[])) metasenv in
+  let _,with_what =
+    List.fold_left
+      (fun (i,acc) (_,cc,ty) -> (i-1,Cic.Rel i::acc)) 
+      (n,[]) metasenv 
+  in
+  let t = CicSubstitution.lift n t in
+  let body =
+    ProofEngineReduction.replace_lifting 
+      ~equality:(fun c t1 t2 ->
+         match t1,t2 with
+         | Cic.Meta(i,_),Cic.Meta(j,_) -> i = j
+         | _ -> false) 
+      ~context ~what ~with_what ~where:t 
+  in
+  let _, t =
+    List.fold_left
+      (fun (n,t) (_,cc,ty) -> 
+        n-1, Cic.Lambda(Cic.Name ("x_"^string_of_int n),
+               CicSubstitution.lift n ty,t))
+      (n-1,body) metasenv 
+  in
+  t
+;;
+  
 (* functions for retrieving theorems *)
 
 exception FillingFailure of AutoCache.cache * int
@@ -37,7 +70,7 @@ exception FillingFailure of AutoCache.cache * int
 let rec unfold context = function
   | Cic.Prod(name,s,t) -> 
       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
-       Cic.Prod(name,s,t')     
+        Cic.Prod(name,s,t')        
   | t -> ProofEngineReduction.unfold context t
 
 let find_library_theorems dbd proof goal = 
@@ -52,19 +85,19 @@ let find_context_theorems context metasenv =
   let l,_ =
     List.fold_left
       (fun (res,i) ctxentry ->
-        match ctxentry with
-          | Some (_,Cic.Decl t) -> 
+         match ctxentry with
+           | Some (_,Cic.Decl t) -> 
                (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
-          | Some (_,Cic.Def (_,Some t)) ->
+           | Some (_,Cic.Def (_,Some t)) ->
                (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
-          | Some (_,Cic.Def (_,None)) ->
-              let t = Cic.Rel i in
-              let ty,_ = 
-                CicTypeChecker.type_of_aux' 
-                  metasenv context t CicUniv.empty_ugraph
+           | Some (_,Cic.Def (_,None)) ->
+               let t = Cic.Rel i in
+               let ty,_ = 
+                 CicTypeChecker.type_of_aux' 
+                   metasenv context t CicUniv.empty_ugraph
                in
-                (t,ty)::res,i+1
-          |  _ -> res,i+1)
+                 (t,ty)::res,i+1
+           |  _ -> res,i+1)
       ([],1) context
   in l
 
@@ -99,13 +132,13 @@ let is_unit_equation context metasenv oldnewmeta term =
             CicReduction.are_convertible ~metasenv context 
               sort (Cic.Sort Cic.Prop) u
           in
-         if b then Some i else None 
+          if b then Some i else None 
       | _ -> assert false)
     args
   in
     if propositional_args = [] then 
       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
-       Some (args,metasenv,newmetas,head,newmeta)
+        Some (args,metasenv,newmetas,head,newmeta)
     else None
 ;;
 
@@ -115,7 +148,7 @@ let get_candidates universe cache t =
   in 
   let debug_msg =
     (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^ 
-            (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
+             (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
   debug_print debug_msg;
   candidates
 ;;
@@ -128,9 +161,9 @@ let only signature context t =
     if b then b 
     else
       try
-       let ty' = unfold context ty in
-       let consts' = MetadataConstraints.constants_of ty' in
-       MetadataConstraints.UriManagerSet.subset consts' signature 
+        let ty' = unfold context ty in
+        let consts' = MetadataConstraints.constants_of ty' in
+        MetadataConstraints.UriManagerSet.subset consts' signature 
       with _-> false
   with _ -> false
 ;;
@@ -145,15 +178,15 @@ let retrieve_equations signature universe cache context=
   match LibraryObjects.eq_URI() with
     | None -> [] 
     | Some eq_uri -> 
-       let eq_uri = UriManager.strip_xpointer eq_uri in
-       let fake= Cic.Meta(-1,[]) in
-       let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
-       let candidates = get_candidates universe cache fake_eq in
+        let eq_uri = UriManager.strip_xpointer eq_uri in
+        let fake= Cic.Meta(-1,[]) in
+        let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
+        let candidates = get_candidates universe cache fake_eq in
     (* defaults eq uris are built-in in auto *)
         let candidates = List.filter not_default_eq_term candidates in
-       let candidates = List.filter (only signature context) candidates in
-       List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates;
-       candidates
+        let candidates = List.filter (only signature context) candidates in
+        List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates;
+        candidates
 
 let build_equality bag head args proof newmetas maxmeta = 
   match head with
@@ -176,12 +209,12 @@ let partition_unit_equalities context metasenv newmeta bag equations =
   List.fold_left
     (fun (units,other,maxmeta)(t,ty) ->
        match is_unit_equation context metasenv maxmeta ty with
-        | Some (args,metasenv,newmetas,head,newmeta') ->
-            let maxmeta,equality =
-              build_equality bag head args t newmetas newmeta' in
-            equality::units,other,maxmeta
-        | None -> 
-            units,(t,ty)::other,maxmeta)
+         | Some (args,metasenv,newmetas,head,newmeta') ->
+             let maxmeta,equality =
+               build_equality bag head args t newmetas newmeta' in
+             equality::units,other,maxmeta
+         | None -> 
+             units,(t,ty)::other,maxmeta)
     ([],[],newmeta) equations
 
 let empty_tables = 
@@ -197,30 +230,30 @@ let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
   let newmeta = CicMkImplicit.new_meta metasenv [] in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let ct = find_context_theorems context metasenv in
-  prerr_endline 
-    ("ho trovato nel contesto " ^ (string_of_int (List.length ct)));
+  debug_print 
+    (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
   let lt = 
     if use_library then 
        find_library_theorems dbd metasenv goal 
     else [] in
-  prerr_endline 
-    ("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
+  debug_print 
+    (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
   let cache = cache_add_list cache context (ct@lt) in  
   let equations = 
     retrieve_equations signature universe cache context in
-  prerr_endline 
-    ("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
+  debug_print 
+    (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
   let eqs_and_types =
     HExtlib.filter_map 
       (fun t -> 
-        let ty,_ =
-          CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
+         let ty,_ =
+           CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
            (* retrieve_equations could also return flexible terms *)
-          if is_an_equality ty then Some(t,ty) 
-          else
-            try
+           if is_an_equality ty then Some(t,ty) 
+           else
+             try
                let ty' = unfold context ty in
-                if is_an_equality ty' then Some(t,ty') else None
+                 if is_an_equality ty' then Some(t,ty') else None
              with _ -> None) (* catturare l'eccezione giusta di unfold *)
       equations in
   let bag = Equality.mk_equality_bag () in
@@ -240,7 +273,7 @@ let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
     if paramod then active,passive,newmeta
     else
       Saturation.pump_actives 
-       context bag newmeta active passive (no+1) infinity
+        context bag newmeta active passive (no+1) infinity
   in 
     (active,passive,bag),cache,newmeta
 
@@ -300,7 +333,7 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u
               in
               let args = List.map (CicMetaSubst.apply_subst subst) args in
               let newm = CicMkImplicit.new_meta metasenv subst in
-               args,metasenv,newmetas,head,max newm newmeta)
+                args,metasenv,newmetas,head,max newm newmeta)
             substs, cache, newmeta
   in
   results,cache,newmeta
@@ -318,17 +351,17 @@ let build_equalities auto context metasenv tables universe cache newmeta equatio
          let eqs,bag,newmeta = 
            List.fold_left 
              (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
-               let maxmeta,equality =
-                 build_equality bag head args t newmetas newmeta'
+                let maxmeta,equality =
+                  build_equality bag head args t newmetas newmeta'
                 in
                   equality::acc,bag,maxmeta)
              ([],bag,newmeta) saturated
          in
            (eqs@facts, cache, newmeta)
        with FillingFailure (cache,newmeta) ->
-        (* if filling hypothesis fails we add the equation to
-           the cache *)
-        (facts,cache,newmeta)
+         (* if filling hypothesis fails we add the equation to
+            the cache *)
+         (facts,cache,newmeta)
       )
     ([],cache,newmeta) equations
 
@@ -341,22 +374,22 @@ let close_more tables maxmeta context status auto universe cache =
   let eqs_and_types =
     HExtlib.filter_map 
       (fun t -> 
-        let ty,_ =
-          CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
+         let ty,_ =
+           CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
            (* retrieve_equations could also return flexible terms *)
-          if is_an_equality ty then Some(t,ty) else None)
+           if is_an_equality ty then Some(t,ty) else None)
       equations in
   let units, cache, maxm = 
       build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
-  prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
-    string_of_int maxm);
+  debug_print (lazy (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
+    string_of_int maxm));
   List.iter
-    (fun e -> prerr_endline (Equality.string_of_equality e)) 
+    (fun e -> debug_print (lazy (Equality.string_of_equality e))) 
     units;
-  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+  debug_print (lazy ">>>>>>>>>>>>>>>>>>>>>>");
   let passive = Saturation.add_to_passive units passive in
   let no = List.length units in
-  prerr_endline ("No = " ^ (string_of_int no));
+  debug_print (lazy ("No = " ^ (string_of_int no)));
   let active,passive,newmeta = 
     Saturation.pump_actives context bag maxm active passive (no+1) infinity
   in 
@@ -550,17 +583,17 @@ let assert_proof_is_valid proof metasenv context goalty =
     begin
       let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
       let b,_ = CicReduction.are_convertible context ty goalty u in
-       if not b then
-         begin
-           let names = 
+        if not b then
+          begin
+            let names = 
               List.map (function None -> None | Some (x,_) -> Some x) context 
-           in
-             prerr_endline ("PROOF:" ^ CicPp.pp proof names);
-             prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
-             prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
-             prerr_endline ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
-         end;
-       assert b
+            in
+              debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
+              debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names));
+              debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
+              debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
+          end;
+        assert b
     end
   else ()
 ;;
@@ -568,15 +601,11 @@ let assert_proof_is_valid proof metasenv context goalty =
 let assert_subst_are_disjoint subst subst' =
   if debug then
     assert(List.for_all
-            (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') 
-            subst)
+             (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') 
+             subst)
   else ()
 ;;
 
-let sort_new_elems = 
-  List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) 
-;;
-
 let split_goals_in_prop metasenv subst gl =
   List.partition 
     (fun g ->
@@ -584,14 +613,14 @@ let split_goals_in_prop metasenv subst gl =
       try
         let sort,u = typeof ~subst metasenv context ty ugraph in
         let b,_ = 
-         CicReduction.are_convertible 
-           ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
-       b
+          CicReduction.are_convertible 
+            ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
+        b
       with 
       | CicTypeChecker.AssertFailure s 
       | CicTypeChecker.TypeCheckerFailure s -> 
           debug_print 
-           (lazy (ppterm context (CicMetaSubst.apply_subst subst ty)));
+            (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
           debug_print s;
           false)
     (* FIXME... they should type! *)
@@ -609,7 +638,7 @@ let split_goals_with_metas metasenv subst gl =
 
 let order_new_goals metasenv subst open_goals ppterm =
   let prop,rest = split_goals_in_prop metasenv subst open_goals in
-  let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
+  let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
   let open_goals =
     (List.map (fun x -> x,P) (closed_prop @ open_prop)) 
     @ 
@@ -623,10 +652,10 @@ let order_new_goals metasenv subst open_goals ppterm =
   debug_print (lazy ("   OPEN: "^
     String.concat "\n" 
       (List.map 
-        (function
-           | (i,t,P) -> string_of_int i   (* ":"^ppterm t^ "Prop" *)
-           | (i,t,T) -> string_of_int i ) (* ":"^ppterm t^ "Type")*)
-        tys)));
+         (function
+            | (i,t,P) -> string_of_int i   ^ ":"^ppterm t^ "Prop" 
+            | (i,t,T) -> string_of_int i  ^ ":"^ppterm t^ "Type")
+         tys)));
   open_goals
 ;;
 
@@ -635,6 +664,355 @@ let is_an_equational_goal = function
   | _ -> false
 ;;
 
+(*
+let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
+*)
+
+let calculate_timeout flags = 
+    if flags.timeout = 0. then 
+      (debug_print (lazy "AUTO WITH NO TIMEOUT");
+       {flags with timeout = infinity})
+    else 
+      flags 
+;;
+let is_equational_case goalty flags =
+  let ensure_equational t = 
+    if is_an_equational_goal t then true 
+    else false
+    (*
+      let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
+      raise (ProofEngineTypes.Fail (lazy msg))
+    *)
+  in
+  (flags.use_paramod && is_an_equational_goal goalty) || 
+  (flags.use_only_paramod && ensure_equational goalty)
+;;
+(*
+let cache_add_success sort cache k v =
+  if sort = P then cache_add_success cache k v else cache_remove_underinspection
+  cache k
+;;
+*)
+
+type menv = Cic.metasenv
+type subst = Cic.substitution
+type goal = ProofEngineTypes.goal * int * AutoTypes.sort
+let candidate_no = ref 0;;
+type candidate = int * Cic.term
+type cache = AutoCache.cache
+type tables = 
+  Saturation.active_table * Saturation.passive_table * Equality.equality_bag
+
+type fail = 
+  (* the goal (mainly for depth) and key of the goal *)
+  goal * AutoCache.cache_key
+type op = 
+  (* goal has to be proved *)
+  | D of goal 
+  (* goal has to be cached as a success obtained using candidate as the first
+   * step *)
+  | S of goal * AutoCache.cache_key * candidate * int 
+type elem = 
+  (* menv, subst, size, operations to do, failures to cache if any op fails *)
+  menv * subst * int * op list * fail list 
+type status = 
+  (* list of computations that may lead to the solution: all op list will
+   * end with the same (S(g,_)) *)
+  elem list
+type auto_result = 
+  (* menv, subst, alternatives, tables, cache, maxmeta *)
+  | Proved of menv * subst * elem list * tables * cache * int
+  | Gaveup of tables * cache * int 
+
+
+(* the status exported to the external observer *)  
+type auto_status = 
+  (* context, (goal,candidate) list, and_list, history *)
+  Cic.context * (Cic.term * (int * Cic.term) list) list * 
+  Cic.term list * Cic.term list
+
+let d_prefix l =
+  let rec aux acc = function
+    | (D g)::tl -> aux (acc@[g]) tl
+    | _ -> acc
+  in
+    aux [] l
+;;
+let prop_only l =
+  List.filter (function (_,_,P) -> true | _ -> false) l
+;;
+
+let d_goals l =
+  let rec aux acc = function
+    | (D g)::tl -> aux (acc@[g]) tl
+    | (S _)::tl -> aux acc tl
+    | [] -> acc
+  in
+    aux [] l
+;;
+let calculate_goal_ty (goalno,_,_) s m = 
+  try
+    let _,cc,goalty = CicUtil.lookup_meta goalno m in
+    (* XXX applicare la subst al contesto? *)
+    Some (cc, CicMetaSubst.apply_subst s goalty)
+  with CicUtil.Meta_not_found i when i = goalno -> None
+;;
+let calculate_closed_goal_ty (goalno,_,_) s = 
+  try
+    let cc,_,goalty = List.assoc goalno s in
+    (* XXX applicare la subst al contesto? *)
+    Some (cc, CicMetaSubst.apply_subst s goalty)
+  with Not_found -> None
+;;
+let pp_status ctx status = 
+  if debug then 
+  let names = Utils.names_of_context ctx in
+  let pp x = 
+    let x = 
+      ProofEngineReduction.replace 
+        ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false) 
+          ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
+    in
+    CicPp.pp x names
+  in
+  let string_of_do m s (gi,_,_ as g) d =
+    match calculate_goal_ty g s m with
+    | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
+    | None -> Printf.sprintf "D(%d, _, %d)" gi d
+  in
+  let string_of_s m su k (ci,ct) gi =
+    Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp ct) ci
+  in
+  let string_of_ol m su l =
+    String.concat " | " 
+      (List.map 
+        (function 
+          | D (g,d,s) -> string_of_do m su (g,d,s) d 
+          | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi) 
+        l)
+  in
+  let string_of_fl m s fl = 
+    String.concat " | " 
+      (List.map (fun ((i,_,_),ty) -> 
+         Printf.sprintf "(%d, %s)" i (pp ty)) fl)
+  in
+  let rec aux = function
+    | [] -> ()
+    | (m,s,ol,fl)::tl ->
+        Printf.eprintf "< [%s] ;;; [%s]>\n" 
+          (string_of_ol m s ol) (string_of_fl m s fl);
+        aux tl
+  in
+    Printf.eprintf "-------------------------- status -------------------\n";
+    aux status;
+    Printf.eprintf "-----------------------------------------------------\n";
+;;
+  
+let auto_status = ref [] ;;
+let auto_context = ref [];;
+let in_pause = ref false;;
+let pause b = in_pause := b;;
+let cond = Condition.create ();;
+let mutex = Mutex.create ();;
+let hint = ref None;;
+
+let step _ = Condition.signal cond;;
+let give_hint n = hint := Some n;;
+
+let check_pause _ =
+  if !in_pause then
+    begin
+      Mutex.lock mutex;
+      Condition.wait cond mutex;
+      Mutex.unlock mutex
+    end
+;;
+
+let get_auto_status _ = 
+  let status = !auto_status in
+(*
+  debug_print "status:";
+  List.iter (fun ((cand,ty),_,_,gl) ->
+    Printf.eprintf "cand: %s; ty: %s; gl: %d\n" 
+      (CicPp.ppterm cand) (CicPp.ppterm ty) (List.length gl)) status;
+*)
+  let and_list,elems,last = 
+    match status with
+    | [] -> [],[],[]
+    | (m,s,_,gl,fail)::tl ->
+        let and_list = 
+          List.map snd 
+            (HExtlib.filter_map 
+              (fun g -> calculate_goal_ty g s m) (d_goals gl))
+        in
+        let rows = 
+          (* these are the S goalsin the or list *)
+          let orlist = 
+            List.map
+              (fun (m,s,_,gl,fail) -> 
+                HExtlib.filter_map
+                  (function S (g,k,c,_) -> Some (g,k,c) | _ -> None) gl)
+              status
+          in
+          (* this function eats id from a list l::[id,x] returning x, l *)
+          let eat_tail_if_eq id l = 
+            match (List.rev l) with 
+            | ((id1,_,_),k1,c)::tl when id = id1 -> Some c, List.rev tl
+            | _ -> None, l
+          in
+          let eat_in_parallel id l =
+            let rec aux (eaten, new_l as acc) l =
+              match l with
+              | [] -> acc
+              | l::tl ->
+                  match eat_tail_if_eq id l with
+                  | None, l -> aux (eaten, new_l@[l]) tl
+                  | Some t,l -> aux (eaten@[t], new_l@[l]) tl
+            in
+            aux ([],[]) l
+          in
+          let rec eat_all rows l =
+            match l with
+            | [] -> rows
+            | elem::or_list ->
+                match List.rev elem with
+                | ((to_eat,_,_),k,_)::next_lunch ->
+                    let eaten, l = eat_in_parallel to_eat l in
+                    let eaten = HExtlib.list_uniq eaten in
+                    let rows = rows @ [k,eaten] in
+                    eat_all rows l
+                | [] -> eat_all rows or_list
+          in
+          eat_all [] orlist
+        in
+        let history = 
+          HExtlib.filter_map
+            (function (S (_,_,(_,c),_)) -> Some c | _ -> None) 
+            gl 
+        in
+(*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
+        and_list, rows, history
+  in
+  !auto_context, elems, and_list, last
+;;
+
+(* Works if there is no dependency over proofs *)
+let is_a_green_cut goalty =
+  CicUtil.is_meta_closed goalty
+;;
+let rec first_s = function
+  | (D _)::tl -> first_s tl
+  | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
+  | [] -> None
+;;
+let list_union l1 l2 =
+  (* TODO ottimizzare compare *)
+  HExtlib.list_uniq (List.sort compare (l1 @ l1))
+;;
+let eat_head todo id fl orlist = 
+  let rec aux acc = function
+  | [] -> [], acc
+  | (m, s, _, todo1, fl1)::tl as orlist -> 
+      let rec aux1 todo1 =
+        match first_s todo1 with
+        | None -> orlist, acc
+        | Some (((gno,_,_),_,_,_), todo11) ->
+            (* TODO confronto tra todo da ottimizzare *)
+            if gno = id && todo11 = todo then 
+              aux (list_union fl1 acc) tl
+            else 
+              aux1 todo11
+      in
+       aux1 todo1
+  in 
+    aux fl orlist
+;;
+let close_proof p ty menv context = 
+  let metas =
+    List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
+  in
+  let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
+  naif_closure p menv context
+;;
+(* XXX capire bene quando aggiungere alla cache *)
+let add_to_cache_and_del_from_orlist_if_green_cut
+  g s m cache key todo orlist fl ctx size minsize
+= 
+  let cache = cache_remove_underinspection cache key in
+  (* prima per fare la irl usavamo il contesto vero e proprio e non quello 
+   * canonico! XXX *)
+  match calculate_closed_goal_ty g s with
+  | None -> assert false
+  | Some (canonical_ctx , gty) ->
+      let goalno,depth,sort = g in
+      assert (sort = P);
+      let irl = mk_irl canonical_ctx in
+      let goal = Cic.Meta(goalno, irl) in
+      let proof = CicMetaSubst.apply_subst s goal in
+      let green_proof, closed_proof = 
+        let b = is_a_green_cut proof in
+        if not b then
+          b, (* close_proof proof gty m ctx *) proof 
+        else
+          b, proof
+      in
+      debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
+      if is_a_green_cut key then
+        (* if the initia goal was closed, we cut alternatives *)
+        let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
+        let orlist, fl = eat_head todo goalno fl orlist in
+        let cache = 
+          if size < minsize then 
+            (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
+          else 
+          (* if the proof is closed we cache it *)
+          if green_proof then cache_add_success cache key proof
+          else (* cache_add_success cache key closed_proof *) 
+            (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
+        in
+        cache, orlist, fl
+      else
+        let cache = 
+          debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
+          if size < minsize then 
+            (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
+          (* if the substituted goal and the proof are closed we cache it *)
+          if is_a_green_cut gty then
+            if green_proof then cache_add_success cache gty proof
+            else (* cache_add_success cache gty closed_proof *) 
+              (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
+          else (*
+            try
+              let ty, _ =
+                CicTypeChecker.type_of_aux' ~subst:s 
+                  m ctx closed_proof CicUniv.oblivion_ugraph
+              in
+              if is_a_green_cut ty then 
+                cache_add_success cache ty closed_proof
+              else cache
+            with
+            | CicTypeChecker.TypeCheckerFailure _ ->*) 
+          (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
+        in
+        cache, orlist, fl
+;;
+let close_failures (fl : fail list) (cache : cache) = 
+  List.fold_left 
+    (fun cache ((gno,depth,_),gty) -> 
+      debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
+      cache_add_failure cache gty depth) 
+    cache fl
+;;
+let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
+  let entry = goalno, (canonical_ctx, t,ty) in
+  assert_subst_are_disjoint subst [entry];
+  let subst = entry :: subst in
+  let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+  subst, metasenv
+;;
+let mk_fake_proof metasenv (goalno,_,_) goalty context = 
+  None,metasenv,Cic.Meta(goalno,mk_irl context),goalty, [] 
+;;
 let equational_case 
   tables maxm cache depth fake_proof goalno goalty subst context 
     flags
@@ -644,57 +1022,58 @@ let equational_case
   let status = (fake_proof,goalno) in
     if flags.use_only_paramod then
       begin
-       prerr_endline ("PARAMODULATION SU: " ^ 
-                        string_of_int goalno ^ " " ^ ppterm goalty );
-       let goal_steps, saturation_steps, timeout = max_int,max_int,flags.timeout in
-       match
-         Saturation.given_clause bag maxm status active passive 
-           goal_steps saturation_steps timeout
-       with 
-         | None, active, passive, maxmeta -> 
-             [], (active,passive,bag), cache, maxmeta, flags
-         | Some(subst',(_,metasenv,proof,_, _),open_goals),active,passive,maxmeta ->
-             assert_subst_are_disjoint subst subst';
-             let subst = subst@subst' in
-             let open_goals = order_new_goals metasenv subst open_goals ppterm in
-             let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
-               [metasenv,subst,open_goals], (active,passive,bag), 
-             cache, maxmeta, flags
+        debug_print (lazy ("PARAMODULATION SU: " ^ 
+                         string_of_int goalno ^ " " ^ ppterm goalty ));
+        let goal_steps, saturation_steps, timeout =
+          max_int,max_int,flags.timeout 
+        in
+        match
+          Saturation.given_clause bag maxm status active passive 
+            goal_steps saturation_steps timeout
+        with 
+          | None, active, passive, maxmeta -> 
+              [], (active,passive,bag), cache, maxmeta, flags
+          | Some(subst',(_,metasenv,proof,_, _),open_goals),active,
+            passive,maxmeta ->
+              assert_subst_are_disjoint subst subst';
+              let subst = subst@subst' in
+              let open_goals = 
+                order_new_goals metasenv subst open_goals ppterm 
+              in
+              let open_goals = 
+                List.map (fun (x,sort) -> x,depth-1,sort) open_goals 
+              in
+              incr candidate_no;
+                      [(!candidate_no,proof),metasenv,subst,open_goals], 
+                (active,passive,bag), 
+                cache, maxmeta, flags
       end
     else
       begin
-       prerr_endline ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
-       let res, maxmeta = Saturation.all_subsumed bag maxm status active passive in
+        debug_print 
+          (lazy 
+           ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
+        let res, maxmeta = 
+          Saturation.all_subsumed bag maxm status active passive 
+        in
         assert (maxmeta >= maxm);
-       let res' =
-         List.map 
-           (fun subst',(_,metasenv,proof,_, _),open_goals ->
-              assert_subst_are_disjoint subst subst';
-              let subst = subst@subst' in
-              let open_goals = order_new_goals metasenv subst open_goals ppterm in
-              let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
-                metasenv,subst,open_goals)
-           res in
-         res', (active,passive,bag), cache, maxmeta, flags 
+        let res' =
+          List.map 
+            (fun subst',(_,metasenv,proof,_, _),open_goals ->
+               assert_subst_are_disjoint subst subst';
+               let subst = subst@subst' in
+               let open_goals = 
+                 order_new_goals metasenv subst open_goals ppterm 
+               in
+               let open_goals = 
+                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals 
+               in
+               incr candidate_no;
+                 (!candidate_no,proof),metasenv,subst,open_goals)
+            res 
+          in
+          res', (active,passive,bag), cache, maxmeta, flags 
       end
-
-(*
-  let active,passive,bag,cache,maxmeta,flags,goal_steps,saturation_steps,timeout =
-    given_clause_params 
-      tables maxm auto cache subst flags context status in
-  match
-    Saturation.given_clause bag maxmeta status active passive 
-      goal_steps saturation_steps timeout
-  with 
-  | None, active, passive, maxmeta -> 
-      None, (active,passive,bag), cache, maxmeta, flags
-  | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
-      assert_subst_are_disjoint subst subst';
-      let subst = subst@subst' in
-      let open_goals = order_new_goals metasenv subst open_goals ppterm in
-      let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
-      Some [metasenv,subst,open_goals], (active,passive,bag), cache, maxmeta, flags
-*)
 ;;
 
 let try_candidate 
@@ -708,16 +1087,18 @@ let try_candidate
     in
     debug_print (lazy ("   OK: " ^ ppterm cand));
     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
-    (* assert_subst_are_disjoint subst subst'; *)
     let subst = subst' in
     let open_goals = order_new_goals metasenv subst open_goals ppterm in
     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
-    Some (metasenv,subst,open_goals), tables , maxmeta
+    incr candidate_no;
+    Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
   with 
-    | ProofEngineTypes.Fail s -> 
-    (*debug_print("   KO: "^Lazy.force s);*)None,tables, maxm
-    | CicUnification.Uncertain s ->  
-    (*debug_print("   BECCATO: "^Lazy.force s);*)None,tables, maxm
+    | ProofEngineTypes.Fail s -> None,tables, maxm
+    | CicUnification.Uncertain s ->  None,tables, maxm
+;;
+
+let sort_new_elems = 
+  List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) 
 ;;
 
 let applicative_case 
@@ -740,89 +1121,232 @@ let applicative_case
   elems, tables, cache, maxm 
 ;;
 
-(* Works if there is no dependency over proofs *)
-let is_a_green_cut goalty =
-  CicUtil.is_meta_closed goalty
+let equational_and_applicative_case 
+  universe flags m s g gty tables cache maxm context 
+=
+  let goalno, depth, sort = g in
+  let fake_proof = mk_fake_proof m g gty context in
+  if is_equational_case gty flags then
+    let elems,tables,cache,maxm1, flags =
+      equational_case tables maxm cache
+        depth fake_proof goalno gty s context flags 
+    in
+    let maxm = maxm1 in
+    let more_elems, tables, cache, maxm1 =
+      if flags.use_only_paramod then
+        [],tables, cache, maxm
+      else
+        applicative_case 
+          tables maxm depth s fake_proof goalno 
+            gty m context universe cache 
+    in
+    let maxm = maxm1 in
+      elems@more_elems, tables, cache, maxm, flags            
+  else
+    let elems, tables, cache, maxm =
+      applicative_case tables maxm depth s fake_proof goalno 
+        gty m context universe cache 
+    in
+      elems, tables, cache, maxm, flags  
 ;;
-
-let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
-
-let calculate_timeout flags = 
-    if flags.timeout = 0. then 
-      (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
-    else 
-      flags 
+let rec first_s_cand = function
+  | [] -> 0
+  | S (_,_,(i,_),_):: _ -> i
+  | _::tl -> first_s_cand tl
 ;;
-let is_equational_case goalty flags =
-  let ensure_equational t = 
-    if is_an_equational_goal t then true 
-    else false
-    (*
-      let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
-      raise (ProofEngineTypes.Fail (lazy msg))
-    *)
-  in
-  (flags.use_paramod && is_an_equational_goal goalty) || 
-  (flags.use_only_paramod && ensure_equational goalty)
+let remove_s_from_fl (id,_,_) (fl : fail list) =
+  let rec aux = function
+    | [] -> []
+    | ((id1,_,_),_)::tl when id = id1 -> tl
+    | hd::tl ->  hd :: aux tl
+  in 
+    aux fl
 ;;
-let cache_add_success sort cache k v =
-  if sort = P then cache_add_success cache k v else cache_remove_underinspection
-  cache k
+let auto_main tables maxm context flags universe cache elems =
+  auto_context := context;
+  let rec aux tables maxm flags cache (elems : status) =
+(*     pp_status context elems;  *)
+    match elems with
+    | [] ->
+        (* complete failure *)
+        Gaveup (tables, cache, maxm)
+    | (m, s, _, [],_)::orlist ->
+        (* complete success *)
+        Proved (m, s, orlist, tables, cache, maxm)
+    | (m, s, size, (D (_,_,T))::todo, fl)::orlist ->
+        (* skip since not Prop, don't even check if closed by side-effect *)
+        aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
+    | (m, s, size, (S(g, key, c,minsize))::todo, fl)::orlist ->
+        (* partial success, cache g and go on *)
+        let cache, orlist, fl = 
+          add_to_cache_and_del_from_orlist_if_green_cut 
+            g s m cache key todo orlist fl context size minsize
+        in
+        debug_print (lazy (AutoCache.cache_print context cache));
+        let fl = remove_s_from_fl g fl in
+        aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
+    | (m, s, size, todo, fl)::orlist 
+      when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
+        debug_print (lazy ("FAIL: WIDTH"));
+        (* too many goals in and generated by last th *)
+        let cache = close_failures fl cache in
+        aux tables maxm flags cache orlist
+    | (m, s, size, todo, fl)::orlist 
+      when size > flags.maxsize ->
+        debug_print (lazy ("FAIL: SIZE"));
+        (* we already have a too large proof term *)
+        let cache = close_failures fl cache in
+        aux tables maxm flags cache orlist
+    | _ when Unix.gettimeofday () > flags.timeout ->
+        (* timeout *)
+        debug_print (lazy ("FAIL: SIZE"));
+        Gaveup (tables, cache, maxm)
+    | (m, s, size, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
+        (* attack g *)
+        match calculate_goal_ty g s m with
+        | None -> 
+            (* closed by side effect *)
+            debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
+            aux tables maxm flags cache ((m,s,size,todo, fl)::orlist)
+        | Some (canonical_ctx, gty) -> 
+            (* still to be proved *)
+            debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
+            debug_print (lazy (AutoCache.cache_print context cache));
+            match cache_examine cache gty with
+            | Failed_in d when d >= depth -> 
+                (* fail depth *)
+                debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
+                let cache = close_failures fl cache in
+                aux tables maxm flags cache orlist
+            | UnderInspection -> 
+                (* fail loop *)
+                debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
+                let cache = close_failures fl cache in
+                aux tables maxm flags cache orlist
+            | Succeded t -> 
+                debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
+                let s, m = put_in_subst s m g canonical_ctx t gty in
+                aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
+            | Notfound 
+            | Failed_in _ when depth > 0 -> 
+                (match !hint with
+                | Some i when first_s_cand todo <> i ->
+                    aux tables maxm flags cache orlist
+                | _ -> hint := None;
+                    (* more depth or is the first time we see the goal *)
+                    let cache = cache_add_underinspection cache gty depth in
+                    auto_status := status;
+                    check_pause ();
+                    debug_print 
+                      (lazy ("INSPECTING: " ^ 
+                        string_of_int gno ^ "("^ string_of_int size ^ "): "^CicPp.ppterm gty));
+                    (* elems are possible computations for proving gty *)
+                    let elems, tables, cache, maxm, flags =
+                      equational_and_applicative_case 
+                        universe flags m s g gty tables cache maxm context
+                    in
+                    if elems = [] then
+                      (* this goal has failed *)
+                      let cache = close_failures ((g,gty)::fl) cache in
+                      aux tables maxm flags cache orlist
+                    else
+                      (* elems = (cand,m,s,gl) *)
+                      let size_gl l = List.length 
+                        (List.filter (function (_,_,P) -> true | _ -> false) l) 
+                      in
+                      let elems = 
+                        let inj_gl gl = List.map (fun g -> D g) gl in
+                        let rec map = function
+                          | [] -> assert false
+                          | (cand,m,s,gl)::[] ->
+                              (* in the last one we add the failure *)
+                              let todo = inj_gl gl @ (S(g,gty,cand,size+1))::todo in
+                              (* we are the last in OR, we fail on g and 
+                               * also on all failures implied by g *)
+                              (m,s, size + size_gl gl, todo, (g,gty)::fl) :: orlist
+                          | (cand,m,s,gl)::tl -> 
+                              (* we add the S step after gl and before todo *)
+                              let todo = inj_gl gl @ (S(g,gty,cand,size+1))::todo in
+                              (* since we are not the last in OR, we do not
+                               * imply failures *)
+                              (m,s, size + size_gl gl, todo, []) :: map tl
+                        in
+                          map elems
+                      in
+                        aux tables maxm flags cache elems)
+            | _ -> 
+                (* no more depth *)
+                debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
+                let cache = close_failures fl cache in
+                aux tables maxm flags cache orlist
+  in
+    (aux tables maxm flags cache elems : auto_result)
 ;;
-
+    
+(*
 let rec auto_main tables maxm context flags elems universe cache =
+  auto_context := context;
   let flags = calculate_timeout flags in
   let ppterm = ppterm context in
   let irl = mk_irl context in
-  let rec aux flags tables maxm cache = function (* elems in OR *)
+  let rec aux flags tables maxm cache elems status = 
+    match elems with (* elems in OR *)
     | [] -> Fail "no more steps can be done", tables, cache, maxm
          (*COMPLETE FAILURE*)
-    | (metasenv,subst,[])::tl -> 
-        Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
-    | (metasenv,subst,goals)::tl when 
+    | (p ,metasenv,subst,[])::tl -> 
+        Success (p,metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
+    | (_,metasenv,subst,goals)::tl when 
       List.length (List.filter prop goals) > flags.maxwidth -> 
         debug_print 
-         (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
-        aux flags tables maxm cache tl (* FAILURE (width) *)
-    | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl -> 
+          (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
+        aux flags tables maxm cache tl (List.tl status) (* FAILURE (width) *)
+    | (p,metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl -> 
+        let (_,_,_,_::gl_status)::tl_status = status in
         if Unix.gettimeofday() > flags.timeout then 
           Fail "timeout",tables,cache,maxm 
         else
         try
           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
+          let id,_,_ = p in
           debug_print 
-           (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^
+            (lazy ("INSPECTING " ^ string_of_int goalno^
+            ":"^"(id="^string_of_int id^")"^ppterm goalty ^
                    "with depth"^string_of_int depth));
           debug_print (lazy (AutoCache.cache_print context cache));
           if sort = T (* && tl <> []*)  then 
             (debug_print 
-              (lazy (" FAILURE(not in prop)"));
-            aux flags tables maxm cache ((metasenv,subst,gl)::tl))
+               (lazy (" FAILURE(not in prop)"));
+            aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
+            ((p,metasenv,subst,gl)::tl_status))
           else
-          match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
+          match aux_single flags tables maxm universe cache metasenv subst elem
+          goalty cc gl_status tl_status p with
           | Fail s, tables, cache, maxm' -> 
               let maxm = maxm' in
               debug_print
                 (lazy 
-                  (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
+                   (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
               let cache = 
-                if flags.dont_cache_failures then 
+                if flags.dont_cache_failures or s = "hint" then 
                   cache_remove_underinspection cache goalty
-                else cache_add_failure cache goalty depth 
+                else 
+                  cache_add_failure cache goalty depth 
               in
-              aux flags tables maxm cache tl
-          | Success (metasenv,subst,others), tables, cache, maxm' ->
+              aux flags tables maxm cache tl tl_status
+          | Success (p1,metasenv,subst,others), tables, cache, maxm' ->
               let maxm = maxm' in
               (* others are alternatives in OR *)
               try
                 let goal = Cic.Meta(goalno,irl) in
                 let proof = CicMetaSubst.apply_subst subst goal in
                 debug_print 
-                 (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
+                  (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
                 if is_a_green_cut goalty then
                   (* assert_proof_is_valid proof metasenv context goalty; *)
                   let cache = cache_add_success sort cache goalty proof in
-                  aux flags tables maxm cache ((metasenv,subst,gl)::tl)
+                  aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
+                    ((p,metasenv,subst,gl)::tl_status)
+                  
                 else
                   (let goalty = CicMetaSubst.apply_subst subst goalty in
                  (* assert_proof_is_valid proof metasenv context goalty; *)
@@ -834,19 +1358,31 @@ let rec auto_main tables maxm context flags elems universe cache =
                   in
                   let others = 
                     List.map 
-                      (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl)) 
+                      (fun (p,metasenv,subst,goals) -> 
+                        (p,metasenv,subst,goals@gl)) 
                     others
                   in 
-                  aux flags tables maxm cache ((metasenv,subst,gl)::others@tl))
+                  aux flags tables maxm cache 
+                    ((p,metasenv,subst,gl)::others@tl)
+                    ((p,metasenv,subst,gl)::others@tl_status)
+                    
+                    )
+                    
               with CicUtil.Meta_not_found i when i = goalno ->
                 assert false
         with CicUtil.Meta_not_found i when i = goalno -> 
           (* goalno was closed by sideeffect *)
           debug_print 
-           (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
-          aux flags tables maxm cache ((metasenv,subst,gl)::tl)
-
-  and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc =
+            (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
+          aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
+            ((p,metasenv,subst,gl)::tl_status)
+
+  and aux_single flags tables maxm universe cache metasenv subst (goalno, depth,
+  _) goalty cc e l (id,_,_) =
+    match !hint with
+    | Some id' when id <> id' -> Fail "hint", tables,cache,maxm
+    | _ -> 
+        hint := None;
     (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
     let goalty = CicMetaSubst.apply_subst subst goalty in
 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
@@ -861,10 +1397,11 @@ let rec auto_main tables maxm context flags elems universe cache =
         let subst = entry :: subst in
         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
         debug_print (lazy ("  CACHE HIT!"));
-        Success (metasenv, subst, []), tables, cache, maxm
+        incr candidate_no;
+        Success ((!candidate_no,t,goalty),metasenv, subst, []), tables, cache, maxm
     | UnderInspection -> 
-       (* assert (not (is_a_green_cut goalty)); *)
-       Fail "looping",tables,cache, maxm
+        (* assert (not (is_a_green_cut goalty)); *)
+        Fail "looping",tables,cache, maxm
     | Notfound 
     | Failed_in _ when depth > 0 -> (* we have more depth now *)
         let cache = cache_add_underinspection cache goalty depth in
@@ -874,37 +1411,83 @@ let rec auto_main tables maxm context flags elems universe cache =
             let elems,tables,cache,maxm1, flags =
               equational_case tables maxm cache
                 depth fake_proof goalno goalty subst context flags in
-             let maxm = maxm1 in
-           let more_elems, tables, cache, maxm1 =
-             if flags.use_only_paramod then
-               [],tables, cache, maxm
-             else
-               applicative_case 
-                 tables maxm depth subst fake_proof goalno 
-                 goalty metasenv context universe cache in
-             let maxm = maxm1 in
-             elems@more_elems, tables, cache, maxm, flags            
+              let maxm = maxm1 in
+            let more_elems, tables, cache, maxm1 =
+              if flags.use_only_paramod then
+                [],tables, cache, maxm
+              else
+                applicative_case 
+                  tables maxm depth subst fake_proof goalno 
+                  goalty metasenv context universe cache in
+              let maxm = maxm1 in
+              elems@more_elems, tables, cache, maxm, flags            
           else
-           let elems, tables, cache, maxm =
+            let elems, tables, cache, maxm =
             applicative_case tables maxm depth subst fake_proof goalno 
               goalty metasenv context universe cache in
-           elems, tables, cache, maxm, flags  
+            elems, tables, cache, maxm, flags  
+        in
+        let status =
+          List.map (fun (p,m,s,l) -> p,m,s,l@e) elems @ l
         in
-        aux flags tables maxm cache elems
+    auto_status := status;
+    check_pause ();
+        let rc = aux flags tables maxm cache elems status in
+        debug_print "BACK!";
+        rc
     | _ -> Fail "depth = 0",tables,cache,maxm 
   in
-    aux flags tables maxm cache elems
+  aux flags tables maxm cache elems elems
 
 and
+*)
+
+(*
+let
   auto_all_solutions maxm tables universe cache context metasenv gl flags 
 =
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
-  let elems = [metasenv,[],goals] in
+  let elems = [(0,Cic.Implicit None,Cic.Implicit None), metasenv,[],goals] in
   let rec aux tables maxm solutions cache elems flags =
     match auto_main tables maxm context flags elems universe cache with
-    | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
-    | Success (metasenv,subst,others),tables,cache,maxm -> 
+    | Fail s,tables,cache,maxm ->debug_print s; solutions,cache,maxm
+    | Success (_,metasenv,subst,others),tables,cache,maxm -> 
+        if Unix.gettimeofday () > flags.timeout then
+          ((subst,metasenv)::solutions), cache, maxm
+        else
+          aux tables maxm ((subst,metasenv)::solutions) cache others flags
+  in
+  let rc = aux tables maxm [] cache elems flags in
+    match rc with
+    | [],cache,maxm -> [],cache,maxm
+    | solutions,cache,maxm -> 
+        let solutions = 
+          HExtlib.filter_map
+            (fun (subst,newmetasenv) ->
+              let opened = 
+                ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
+              in
+              if opened = [] then Some subst else None)
+            solutions
+        in
+         solutions,cache,maxm
+;;
+*)
+let
+  auto_all_solutions maxm tables universe cache context metasenv gl flags 
+=
+  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
+  let rec aux tables maxm solutions cache elems flags =
+    match auto_main tables maxm context flags universe cache elems with
+    | Gaveup (tables,cache,maxm) ->
+        solutions,cache,maxm
+    | Proved (metasenv,subst,others,tables,cache,maxm) -> 
         if Unix.gettimeofday () > flags.timeout then
           ((subst,metasenv)::solutions), cache, maxm
         else
@@ -928,24 +1511,140 @@ and
 
 (* }}} ****************** AUTO ***************)
 
+(* script generation for applicative proofs 
+let cic2grafite context menv t =
+  let module PT = CicNotationPt in
+  let module GA = GrafiteAst in
+  let pp_t context t =
+    let names = Utils.names_of_context context in
+    CicPp.pp t names
+  in
+  let sort_of context t = 
+    let ty,_ = 
+      CicTypeChecker.type_of_aux' menv context t
+        CicUniv.oblivion_ugraph 
+    in
+    let sort,_ = CicTypeChecker.type_of_aux' menv context ty
+        CicUniv.oblivion_ugraph
+    in
+    match sort with
+    | Cic.Sort Cic.Prop -> P
+    | _ -> T
+  in
+  let floc = HExtlib.dummy_floc in
+  let rec print_term c = function
+    | Cic.Rel _
+    | Cic.MutConstruct _ 
+    | Cic.MutInd _ 
+    | Cic.Const _ as t -> 
+        PT.Ident (pp_t c t, None)
+    | Cic.Appl l -> PT.Appl (List.map (print_term c) l)
+    | Cic.Implicit _ -> PT.Implicit
+    | Cic.Lambda (Cic.Name n, s, t) ->
+        PT.Binder (`Lambda, (PT.Ident (n,None), Some (print_term c s)),
+          print_term (Some (Cic.Name n, Cic.Decl s)::c) t)
+    | Cic.Prod (Cic.Name n, s, t) ->
+        PT.Binder (`Forall, (PT.Ident (n,None), Some (print_term c s)),
+          print_term (Some (Cic.Name n, Cic.Decl s)::c) t)
+    | Cic.LetIn (Cic.Name n, s, t) ->
+        PT.Binder (`Lambda, (PT.Ident (n,None), Some (print_term c s)),
+          print_term (Some (Cic.Name n, Cic.Def (s,None))::c) t)
+    | Cic.Meta _ -> PT.Implicit
+    | _ as t -> 
+        PT.Ident ("ERROR"^CicPp.ppterm t, None)
+    (*
+        debug_print (lazy (CicPp.ppterm t));
+        assert false
+        *)
+  in
+  let rec print_proof context = function
+    | Cic.Rel _
+    | Cic.Const _ as t -> 
+        [GA.Executable (floc, 
+          GA.Tactic (floc,
+          Some (GA.Apply (floc, print_term context t)), GA.Dot floc))]
+    | Cic.Appl (he::tl) ->
+        let tl = List.map (fun t -> t, sort_of context t) tl in
+        let subgoals = 
+          HExtlib.filter_map (function (t,P) -> Some t | _ -> None) tl
+        in
+        let args = 
+            List.map 
+              (function 
+                | (t,P) -> Cic.Implicit None
+                | (t,_) -> t)
+              tl
+        in
+        if List.length subgoals > 1 then
+          (* branch *)
+          [GA.Executable (floc, 
+            GA.Tactic (floc,
+              Some (GA.Apply (floc, print_term context (Cic.Appl (he::args)))),
+              GA.Semicolon floc))] @
+          [GA.Executable (floc, GA.Tactic (floc, None, GA.Branch floc))] @
+          (HExtlib.list_concat 
+          ~sep:[GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))]
+            (List.map (print_proof context) subgoals)) @
+          [GA.Executable (floc, GA.Tactic (floc, None,GA.Merge floc))]
+        else
+          (* simple apply *)
+          [GA.Executable (floc, 
+            GA.Tactic (floc,
+            Some (GA.Apply 
+              (floc, print_term context (Cic.Appl (he::args)) )), GA.Dot floc))]
+          @
+          (match subgoals with
+          | [] -> []
+          | [x] -> print_proof context x
+          | _ -> assert false)
+    | _ -> []
+    (*
+        debug_print (lazy (CicPp.ppterm t));
+        assert false
+        *)
+  in
+  let ast = print_proof context t in
+  let pp t = 
+    (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
+     * which will show up using the following command line:
+     * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
+    let width = max_int in
+    let term_pp content_term =
+      let pres_term = TermContentPres.pp_ast content_term in
+      let dummy_tbl = Hashtbl.create 1 in
+      let markup = CicNotationPres.render dummy_tbl pres_term in
+      let s = "(" ^ BoxPp.render_to_string List.hd width markup ^ ")" in
+      Pcre.substitute 
+        ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
+    in
+    CicNotationPp.set_pp_term term_pp;
+    let lazy_term_pp = fun x -> assert false in
+    let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
+    GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
+  in
+  String.concat "\n" (List.map pp ast)
+;;
 let auto_all tables universe cache context metasenv gl flags =
   let solutions, cache, _ = 
     auto_all_solutions 0 tables universe cache context metasenv gl flags
   in
   solutions, cache
 ;;
+*)
 
 let auto flags metasenv tables universe cache context metasenv gl =
   let initial_time = Unix.gettimeofday() in
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
-  let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
-  let elems = [metasenv,[],goals] in
-  match auto_main tables 0 context flags elems universe cache with
-  | Success (metasenv,subst,_), tables,cache,_ -> 
-      prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+  let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
+  let elems = [metasenv,[],1,goals,[]] in
+  match auto_main tables 0 context flags universe cache elems with
+  | Proved (metasenv,subst,_, tables,cache,_) -> 
+      debug_print(lazy
+        ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
       Some (subst,metasenv), cache
-  | Fail s,tables,cache,maxm -> 
-      prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+  | Gaveup (tables,cache,maxm) -> 
+      debug_print(lazy
+        ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
       None,cache
 ;;
 
@@ -984,10 +1683,12 @@ let flags_of_params params ?(for_applyS=false) () =
    ((AutoTypes.default_flags()).AutoTypes.use_library) in
  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
+ let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
  let timeout = int "timeout" 0 in
   { AutoTypes.maxdepth = 
       if use_only_paramod then 2 else depth;
     AutoTypes.maxwidth = width;
+    AutoTypes.maxsize = size;
     AutoTypes.timeout = 
       if timeout = 0 then
        if for_applyS then Unix.gettimeofday () +. 30.0
@@ -1082,24 +1783,26 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
     Indexing.superposition_right bag
       ~subterms_only eq_uri maxm env index eq_what
   in
-  prerr_endline ("Superposition right:");
-  prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
-  prerr_endline ("\n table: ");
-  List.iter (fun e -> prerr_endline ("  " ^ Equality.string_of_equality e ~env)) eq_other;
-  prerr_endline ("\n result: ");
-  List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
-  prerr_endline ("\n result (cut&paste): ");
+  debug_print (lazy ("Superposition right:"));
+  debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
+  debug_print (lazy ("\n table: "));
+  List.iter 
+    (fun e -> 
+       debug_print (lazy ("  " ^ Equality.string_of_equality e ~env))) eq_other;
+  debug_print (lazy ("\n result: "));
+  List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
+  debug_print (lazy ("\n result (cut&paste): "));
   List.iter 
     (fun e -> 
       let t = Equality.term_of_equality eq_uri e in
-      prerr_endline (CicPp.pp t names)) 
+      debug_print (lazy (CicPp.pp t names))) 
   eql;
-  prerr_endline ("\n result proofs: ");
+  debug_print (lazy ("\n result proofs: "));
   List.iter (fun e -> 
-    prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
+    debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
     let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
     Subst.ppsubst s ^ "\n" ^ 
-    CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
+    CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
   if demod_table <> "" then
     begin
       let eql = 
@@ -1125,14 +1828,14 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
           (maxm,[]) eql
       in
       let eql = List.rev eql in
-      prerr_endline ("\n result [demod]: ");
+      debug_print (lazy ("\n result [demod]: "));
       List.iter 
-        (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
-      prerr_endline ("\n result [demod] (cut&paste): ");
+        (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
+      debug_print (lazy ("\n result [demod] (cut&paste): "));
       List.iter 
         (fun e -> 
           let t = Equality.term_of_equality eq_uri e in
-          prerr_endline (CicPp.pp t names)) 
+          debug_print (lazy (CicPp.pp t names)))
       eql;
     end;
   proof,[goalno]
@@ -1156,36 +1859,49 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
   | false -> 
       (* this is the real auto *)
       let _,metasenv,_,_, _ = proof in
-      let _,context,_ = CicUtil.lookup_meta goal metasenv in
+      let _,context,goalty = CicUtil.lookup_meta goal metasenv in
       let flags = flags_of_params params () in
       (* just for testing *)
       let use_library = flags.use_library in
       let tables,cache,newmeta =
-       init_cache_and_tables dbd use_library flags.use_only_paramod 
-         universe (proof, goal) in
+        init_cache_and_tables dbd use_library flags.use_only_paramod 
+          universe (proof, goal) in
       let tables,cache,newmeta =
         if flags.close_more then
-         close_more 
-           tables newmeta context (proof, goal) auto_all_solutions universe cache 
-       else tables,cache,newmeta in
+          close_more 
+            tables newmeta context (proof, goal) 
+              auto_all_solutions universe cache 
+        else tables,cache,newmeta in
       let initial_time = Unix.gettimeofday() in
       let (_,oldmetasenv,_,_, _) = proof in
-      let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
-      match auto_main tables newmeta context flags [elem] universe cache with
-       | Success (metasenv,subst,_), tables,cache,_ -> 
-           prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
-           let proof,metasenv = 
+      hint := None;
+      let elem = 
+        metasenv,[],1,[D (goal,flags.maxdepth,P)],[]
+      in
+      match auto_main tables newmeta context flags universe cache [elem] with
+        | Proved (metasenv,subst,_, tables,cache,_) -> 
+            prerr_endline 
+              ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+            (* script generation 
+            let irl = mk_irl context in
+            let goal_term = Cic.Meta(goal, irl) in
+            let proof_term = CicMetaSubst.apply_subst subst goal_term in
+            HLog.debug (cic2grafite context metasenv proof_term);
+            *)
+            let proof,metasenv = 
             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
               proof goal (CicMetaSubst.apply_subst subst) metasenv
             in
             let opened = 
               ProofEngineHelpers.compare_metasenvs ~oldmetasenv
-               ~newmetasenv:metasenv
+                ~newmetasenv:metasenv
             in
               proof,opened
-       | Fail s,tables,cache,maxm -> 
-           prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
-           raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+        | Gaveup (tables,cache,maxm) -> 
+            debug_print
+              (lazy ("TIME:"^
+                string_of_float(Unix.gettimeofday()-.initial_time)));
+            raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
 ;;
 
 let auto_tac ~dbd ~params ~universe = 
@@ -1243,5 +1959,3 @@ let demodulate_tac ~dbd ~universe (proof,goal)=
 let demodulate_tac ~dbd ~universe = 
   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
 
-
-
index d8efa613e1ae599242177294fd5b4b9b209d4065..f0bc752f670fe624e7be58be3fae4a7d6e190c69 100644 (file)
@@ -41,3 +41,14 @@ val demodulate_tac :
   dbd:HMysql.dbd -> 
   universe:Universe.universe ->
   ProofEngineTypes.tactic
+
+type auto_status = 
+  Cic.context * (Cic.term * (int * Cic.term) list) list * Cic.term list *
+  Cic.term list
+val get_auto_status : unit -> auto_status
+val pause: bool -> unit
+val step : unit -> unit
+val give_hint : int -> unit
+(*
+val cic2grafite : Cic.context -> Cic.metasenv -> Cic.term -> string
+*)
index 5fb4640d71e2c8308280a64e090c0bb5a32d6494..b12b26c054853d8288ddbc68d7e5e9dd93927c34 100644 (file)
@@ -31,6 +31,10 @@ type cache_elem =
   | Notfound
 type cache = (Universe.universe * ((cache_key * cache_elem) list));;
 
+let debug = false;;
+let prerr_endline s = 
+  if debug then prerr_endline s else ()
+;;
 
 let cache_empty = (Universe.empty,[]);;
 
@@ -59,7 +63,10 @@ let cache_add_list (univ,cache) context terms_and_types =
   univ, cache
 
 let cache_examine (_,oldcache) cache_key = 
-  try List.assoc cache_key oldcache with Not_found -> Notfound
+  prerr_endline ("examine : " ^ CicPp.ppterm cache_key);
+  try List.assoc cache_key oldcache with Not_found -> 
+    prerr_endline "notfound";
+    Notfound
 ;;
 let cache_replace (univ,oldcache) key v =
   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
@@ -70,27 +77,46 @@ let cache_remove (univ,oldcache) key =
   univ,oldcache
 ;;
 let cache_add_failure cache cache_key depth =
+  prerr_endline 
+    ("CACHE: ADD FAIL " ^ CicPp.ppterm cache_key ^ 
+      " depth: " ^ string_of_int depth);
   match cache_examine cache cache_key with
   | Failed_in i when i > depth -> cache
   | Notfound  
   | Failed_in _ 
   | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
-  | Succeded t -> 
+  | Succeded t -> cache 
+                  (*
       prerr_endline (CicPp.ppterm t);
-      assert false (* if succed it can't fail *)
+      assert false (* if succed it can't fail *) *)
 ;;
 let cache_add_success ((univ,_) as cache) cache_key proof =
+  let u_key = Universe.key cache_key in
+  if u_key <> cache_key then
+    Universe.index univ u_key proof, snd cache
+  else
+    univ, 
+    snd 
+    (match cache_examine cache cache_key with
+    | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
+    | UnderInspection -> cache_replace cache cache_key (Succeded proof)
+    | Succeded t -> (* we may decide to keep the smallest proof *) cache
+    | Notfound -> cache_replace cache cache_key (Succeded proof))
+(*
   (if Universe.key cache_key = cache_key then
     Universe.index univ cache_key proof
   else
     univ),snd
-  (match cache_examine cache cache_key with
+  (prerr_endline ("CACHE: ADD SUCCESS" ^ CicPp.ppterm cache_key);
+  match cache_examine cache cache_key with
   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
   | Succeded t -> (* we may decide to keep the smallest proof *) cache
   | Notfound -> cache_replace cache cache_key (Succeded proof))
 ;;
+*)
 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
+  prerr_endline ("CACHE: ADD INSPECTING" ^ CicPp.ppterm cache_key);
   match cache_examine cache cache_key with
   | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
   | Notfound -> univ,(cache_key,UnderInspection)::oldcache
@@ -103,16 +129,19 @@ let cache_print context (_,oldcache) =
   String.concat "\n" 
     (HExtlib.filter_map 
       (function 
-        | (k,Succeded _) -> Some (CicPp.pp k names)
+        | (k,Succeded _) -> Some ("CACHE SUCCESS: " ^ CicPp.pp k names)
         | _ -> None)
       oldcache)
 ;;
 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
+  prerr_endline ("CACHE: REMOVE INSPECTING" ^ CicPp.ppterm cache_key);
   match cache_examine cache cache_key with
   | Notfound 
+  | Failed_in _ (* -> assert false  *)
   | UnderInspection ->  cache_remove cache cache_key
-  | Failed_in _ -> assert false
-  | Succeded _ -> assert false (* it must be a new goal *)
+  | Succeded _ -> cache (* 
+      prerr_endline (CicPp.ppterm cache_key);            
+      assert false (* it must be a new goal *) *)
 ;;
 let cache_size (_,oldcache) = 
   List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
index 5a84c2c2ba73bab691fdd39cc606ebfa718346a9..b0833c947e03f61fc75a20a12c96081c173a0ac7 100644 (file)
@@ -25,6 +25,7 @@
 
 type flags = {
   maxwidth: int;
+  maxsize: int;
   maxdepth: int;
   timeout: float;
   use_library: bool;
@@ -37,6 +38,7 @@ type flags = {
 let default_flags _ =
   {maxwidth=3;
    maxdepth=3;
+   maxsize = 6;
    timeout=Unix.gettimeofday() +.3.0;
    use_library=false;
    use_paramod=true;
@@ -47,8 +49,8 @@ let default_flags _ =
 
 (* (metasenv, subst, (metano,depth)list *)
 type sort = P | T;;
-type and_elem =  Cic.metasenv * Cic.substitution * (int * int * sort) list
+type and_elem =  (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * (int * int * sort) list
 type auto_result = 
   | Fail of string 
-  | Success of Cic.metasenv * Cic.substitution * and_elem list
+  | Success of (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * and_elem list
 
index 5014f41ce10d6eb75c60a6b2ec1a768cf5120ae0..a026a908fa659fd869d5720673fc9a534e934314 100644 (file)
@@ -25,6 +25,7 @@
 
 type flags = {
   maxwidth: int;
+  maxsize: int;
   maxdepth: int;
   timeout: float;
   use_library: bool;
@@ -39,8 +40,8 @@ val default_flags : unit -> flags
 (* (metasenv, subst, (metano,depth)list *)
 type sort = P | T;;
 type and_elem =  
-  Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list
+  (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list
 type auto_result = 
   | Fail of string
-  | Success of Cic.metasenv * Cic.substitution * and_elem list
+  | Success of (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * and_elem list
 
index 177471c7403a4d9eb2da538289f76e5e718f0681..2a637135351516703b6e83e8c500ef467e11687a 100644 (file)
@@ -648,3 +648,36 @@ let split_with_whd (c, t) =
       | v                   -> aux true a n c (CicReduction.whd c v)
     in
     aux false [] 0 c t
+
+
+  (* menv sorting *)
+module OT = 
+  struct 
+    type t = Cic.conjecture
+    let compare (i,_,_) (j,_,_) = Pervasives.compare i j
+  end
+module MS = HTopoSort.Make(OT)
+let relations_of_menv m c =
+  let i, ctx, ty = c in
+  let m = List.filter (fun (j,_,_) -> j <> i) m in
+  let m_ty = List.map fst (CicUtil.metas_of_term ty) in
+  let m_ctx = 
+    List.flatten
+      (List.map 
+        (function 
+         | None -> []
+         | Some (_,Cic.Decl t)
+         | Some (_,Cic.Def (t,None)) -> 
+             List.map fst (CicUtil.metas_of_term ty)
+         | Some (_,Cic.Def (t,Some ty)) -> 
+             List.map fst (CicUtil.metas_of_term ty) @
+             List.map fst (CicUtil.metas_of_term t))
+        ctx)
+  in
+  let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
+  List.filter (fun (i,_,_) -> List.exists ((=) i) metas) m
+;;
+let sort_metasenv (m : Cic.metasenv) =
+  (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
+;;
+  
index 1ac3ee707f17c7ef3eca3f7ec284885c9d5107a8..0a053ece7dcd212f1e37aef499ee6e6977529705 100644 (file)
@@ -106,6 +106,10 @@ val locate_in_conjecture:
 (* returns the index and the type of a premise in a context *)
 val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
 
+(* orders a metasenv w.r.t. dependency among metas *)
+val sort_metasenv: Cic.metasenv -> Cic.metasenv
+
+
 (* FG: some helper functions ************************************************)
 
 val get_name: Cic.context -> int -> string option
index add1a46c368998004c9f02aec983dae07f75c414..f1e2078ebb18e30005ca8f166e70d2cc4cd57c03 100644 (file)
@@ -8,6 +8,8 @@ gragrep.cmo: matitaInit.cmi buildTimeConf.cmi gragrep.cmi
 gragrep.cmx: matitaInit.cmx buildTimeConf.cmx gragrep.cmi 
 lablGraphviz.cmo: lablGraphviz.cmi 
 lablGraphviz.cmx: lablGraphviz.cmi 
+matitaAutoGui.cmo: matitaGeneratedGui.cmo 
+matitaAutoGui.cmx: matitaGeneratedGui.cmx 
 matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi 
 matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi 
 matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \
@@ -53,11 +55,11 @@ matitaMathView.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \
 matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi 
 matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi 
 matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \
-    matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi \
-    applyTransformation.cmi 
+    matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaAutoGui.cmo \
+    buildTimeConf.cmi applyTransformation.cmi 
 matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \
-    matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \
-    applyTransformation.cmx 
+    matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaAutoGui.cmx \
+    buildTimeConf.cmx applyTransformation.cmx 
 matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
     buildTimeConf.cmi matitaprover.cmi 
 matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
index 158d4d48a42b948ea86200c506ea977bd0fc1646..d58996de307488cc24f3dc96e8e12fcbd57e42fc 100644 (file)
@@ -109,7 +109,7 @@ intros (n); apply (p2bT ? ? (lebP ? ?)); apply le_n; qed.
 
 lemma lebW : ∀n,m. leb (S n) m = true → leb n m = true.
 intros (n m H); lapply (b2pT ? ? (lebP ? ?) H); clear H;
-apply (p2bT ? ? (lebP ? ?)); auto.
+apply (p2bT ? ? (lebP ? ?)); apply lt_to_le; assumption.
 qed. 
 
 definition ltb ≝ λx,y.leb (S x) y.
@@ -149,7 +149,8 @@ qed.
 
 
 (* OUT OF PLACE *)
-lemma ltW : ∀n,m. n < m → n < (S m). intros; auto. qed.
+lemma ltW : ∀n,m. n < m → n < (S m).
+intros; unfold lt; unfold lt in H; auto. qed.
 
 lemma ltbW : ∀n,m. ltb n m = true → ltb n (S m) = true.
 intros (n m H); letin H1 ≝ (b2pT ? ? (ltbP ? ?) H); clearbody H1;
index dc3f4c828f25c26e716678abdbd13e69c2a132f0..07e658e0b0c0c373c3ab6fbbbbb8d54d895cdf61 100644 (file)
@@ -251,8 +251,9 @@ alias symbol "times" = "Fmult".
 
 theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
  assume n:nat.
- we proceed by induction on n to prove
- (D[x \sup n] = n · x \sup (pred n)).
+ (*we proceed by induction on n to prove
+ (D[x \sup n] = n · x \sup (pred n)).*)
+ elim n 0.
  case O.
    the thesis becomes (D[x \sup 0] = 0·x \sup (pred 0)).
    by _
@@ -306,8 +307,8 @@ interpretation "Rderivative" 'derivative f =
 
 theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n.
  assume n:nat.
- we proceed by induction on n to prove
- (D[x \sup (1+n)] = (1+n) · x \sup n).
(*we proceed by induction on n to prove
+ (D[x \sup (1+n)] = (1+n) · x \sup n).*) elim n 0.
  case O.
    the thesis becomes (D[x \sup 1] = 1 · x \sup 0).
    by _
index 826a2670a70a6c80822c2baeb4764962822af120..f5b147005f84ff8b9490bff1f66ec44a04524192 100644 (file)
@@ -125,7 +125,7 @@ cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
     *)
   |letin z \def le.
    cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n)));
-   [2: rewrite < H1.assumption.|letin x \def le.auto width = 4 new]
+   [2: rewrite < H1.assumption.|letin x \def le.auto width = 4 depth = 2]
    (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
   ].
 (*
index a95dc4e27df3c2467bb76990f2c487ffa02744f3..49e8a199e7bb077eb1e1129f5c79a5313d326f5f 100644 (file)
@@ -233,7 +233,7 @@ rewrite < S_pred
   | apply lt_O_times_S_S                    
   | apply lt_O_times_S_S
   ]
-| auto
+| unfold lt.auto
   (*simplify.
   unfold lt.
   apply le_SO_minus.
index 606fdfcf8a061b3ada38bef52a455a0dbd69ea1a..9683869c1aa171e48e7a90ba8c61716c4f2f1173 100644 (file)
@@ -231,9 +231,10 @@ congruent m m1 p \to congruent (n*m) (n1*m1) p.
 unfold congruent. 
 intros. 
 rewrite > (mod_times n m p H).
-auto.
-(*rewrite > H1.
+rewrite > H1.
 rewrite > H2.
+auto.
+(*
 apply sym_eq.
 apply mod_times.
 assumption.*)
index 8d16ac7234c975a85f0113f661a3c7872217ad60..232ace21fa299d506898a67dc862e08f95f40b36 100644 (file)
@@ -181,7 +181,7 @@ split
       apply (trans_le ? (j -i))
       [ apply divides_to_le
         [(*fattorizzare*)
-          auto (*qui auto e' efficace, ma impiega un tempo piuttosto alto a chiudere il goal corrente*)
+          unfold lt.auto.
           (*apply (lt_plus_to_lt_l i).
           simplify.
           rewrite < (plus_minus_m_m)
@@ -214,7 +214,7 @@ split
       apply (trans_le ? (i -j))
       [ apply divides_to_le
         [(*fattorizzare*)
-          auto (*qui auto e' efficace, ma impiega un tempo piuttosto alto per concludere il goal attuale*)
+          unfold lt.auto.
           (*apply (lt_plus_to_lt_l j).
           simplify.
           rewrite < (plus_minus_m_m)
index 073318f9e8a0f9bf3fa6730b664ccc25e2a09461..69acf1837fcc3ab912eea14bdf0ad28248c23593 100644 (file)
@@ -598,7 +598,6 @@ apply (nat_case n)
           ]
         ]
       | (* prova del cut *)
-        goal 20.
         apply (p_ord_aux_to_exp (S(S m1)));auto
         (*[ apply lt_O_nth_prime_n
         | assumption
index df8aff7275aba39992d550388fbc02340af046b1..6fc31a7d1760ca79ba67d72930f8fd08d5a1537f 100644 (file)
@@ -53,20 +53,18 @@ split
                   apply le_S_S.
                   apply le_O_n*)
                 | rewrite > lt_to_eq_mod;
-                    auto(*unfold lt;apply le_S_S;assumption*)                  
+                    unfold lt;auto.(*apply le_S_S;assumption*)                  
                 ]
               | auto
                 (*unfold lt.
                 apply le_S_S.
                 apply le_O_n*)              
               | rewrite > lt_to_eq_mod
-                [ auto
-                  (*unfold lt.
-                  apply le_S_S.
+                [ unfold lt.auto
+                  (*apply le_S_S.
                   assumption*)
-                | auto
-                  (*unfold lt.
-                  apply le_S_S.
+                | unfold lt.auto
+                  (*apply le_S_S.
                   assumption*)
                 ]
               ]
@@ -80,16 +78,14 @@ split
               [ rewrite < H4 in \vdash (? ? ? (? %?)).
                 rewrite < mod_S
                 [ assumption
-                | auto
-                  (*unfold lt.
-                  apply le_S_S.
+                | unfold lt.auto
+                  (*apply le_S_S.
                   apply le_O_n*)
                 | rewrite > lt_to_eq_mod;
-                    auto;(*unfold lt;apply le_S_S;assumption*)                
+                    unfold lt;auto;(*apply le_S_S;assumption*)                
                 ]
-              | auto
-                (*unfold lt.
-                apply le_S_S.
+              | unfold lt.auto
+                (*apply le_S_S.
                 apply le_O_n*)
               ]
             ]
@@ -101,16 +97,14 @@ split
               [ rewrite < H3 in \vdash (? ? (? %?) ?).
                 rewrite < mod_S
                 [ assumption
-                | auto
-                  (*unfold lt.
-                  apply le_S_S.
+                | unfold lt.auto
+                  (*apply le_S_S.
                   apply le_O_n*)
                 | rewrite > lt_to_eq_mod;
-                    auto(*unfold lt;apply le_S_S;assumption*)                  
+                    unfold lt;auto(*apply le_S_S;assumption*)                  
                 ]
-              | auto
-                (*unfold lt.
-                apply le_S_S.
+              | unfold lt.auto
+                (*apply le_S_S.
                 apply le_O_n*)
               ]
             |(* i = n, j= n*)
@@ -128,14 +122,12 @@ split
         (*apply le_to_or_lt_eq.
         assumption*)
       ]                  
-    | auto
-      (*unfold lt.
-      apply le_S_S.
+    | unfold lt.auto
+      (*apply le_S_S.
       assumption*)
     ]
-  | auto
-    (*unfold lt.
-    apply le_S_S.
+  | unfold lt.auto
+    (*apply le_S_S.
     assumption*)
   ]
 ]
@@ -246,9 +238,8 @@ split
         | rewrite > sym_plus.
           apply le_plus_n
         ]*)
-      | auto
-        (*unfold prime in H.
-        elim H.
+      | unfold prime in H. elim H. auto.
+        (*
         apply (trans_lt ? (S O))
         [ unfold lt.
           apply le_n
@@ -257,9 +248,8 @@ split
       ]
     | apply (le_to_not_lt p (j-i)).
       apply divides_to_le
-      [ auto
-        (*unfold lt.
-        apply le_SO_minus.
+      [ unfold lt.auto
+        (*apply le_SO_minus.
         assumption*)
       | cut (divides p a \lor divides p (j-i))
         [ elim Hcut
@@ -273,10 +263,8 @@ split
           [ assumption
           | rewrite > distr_times_minus.
             apply eq_mod_to_divides
-            [ auto
-              (*unfold prime in H.                        
-              elim H.
-              apply (trans_lt ? (S O))
+            [ unfold prime in H.elim H.auto
+              (*apply (trans_lt ? (S O))
               [ unfold lt.
                 apply le_n
               | assumption
@@ -306,9 +294,8 @@ split
         | rewrite > sym_plus.
           apply le_plus_n
         ]*)
-      | auto
-        (*unfold prime in H.
-        elim H.
+      | unfold prime in H.elim H.auto.
+        (*
         apply (trans_lt ? (S O))
         [ unfold lt.
           apply le_n
@@ -317,9 +304,8 @@ split
       ]
     | apply (le_to_not_lt p (i-j)).
       apply divides_to_le
-      [ auto
-        (*unfold lt.
-        apply le_SO_minus.
+      [ unfold lt.auto
+        (*apply le_SO_minus.
         assumption*)
       | cut (divides p a \lor divides p (i-j))
         [ elim Hcut
@@ -333,9 +319,8 @@ split
           [ assumption
           | rewrite > distr_times_minus.
             apply eq_mod_to_divides
-            [ auto
-              (*unfold prime in H.
-              elim H.
+            [ unfold prime in H.elim H.auto.
+              (*
               apply (trans_lt ? (S O))
               [ unfold lt.
                 apply le_n
index ae59700c435c5541c23365c122557fe18043874a..93589d66e1d9542a40fe22865446b94866bdf038 100644 (file)
@@ -100,7 +100,7 @@ elim p
         cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
         gcd_aux n n1 (m \mod n1) \divides mod m n1)
         [ elim Hcut1.
-          auto
+          auto width = 4.
           (*split
           [ apply (divides_mod_to_divides ? ? n1);assumption           
           | assumption
@@ -263,7 +263,8 @@ elim p
 | simplify.
   cut (n1 \divides m \lor n1 \ndivides m)
   [ elim Hcut.
-    rewrite > divides_to_divides_b_true;auto.
+    rewrite > divides_to_divides_b_true;
+    simplify; auto.
     (*[ simplify.
       assumption.
     | assumption. 
@@ -337,9 +338,8 @@ apply (leb_elim n m)
   | intros.
     change with (d \divides gcd_aux (S m1) m (S m1)).
     apply divides_gcd_aux      
-    [ auto
-      (*unfold lt.
-      apply le_S_S.
+    [ unfold lt.auto
+      (*apply le_S_S.
       apply le_O_n.*)
     | assumption.
     | apply le_n. (*chiude il goal anche con auto*)
@@ -355,9 +355,8 @@ apply (leb_elim n m)
   | intros.
     change with (d \divides gcd_aux (S m1) n (S m1)).
     apply divides_gcd_aux
-    [ auto
-      (*unfold lt.
-      apply le_S_S.
+    [ unfold lt.auto
+      (*apply le_S_S.
       apply le_O_n*)
     | auto
       (*apply lt_to_le.
@@ -590,13 +589,18 @@ m = O \land n = O.
 intros.
 cut (O \divides n \land O \divides m)
 [ elim Hcut.
-  auto
-  (*elim H2.
-  split
-  [ assumption
-  | elim H1.
-    assumption
-  ]*)
+  auto size = 7;
+  (*
+  split; 
+    [ apply antisymmetric_divides
+      [ apply divides_n_O
+      | assumption
+      ]
+    | apply antisymmetric_divides
+      [ apply divides_n_O
+      | assumption
+      ]
+    ]*)
 | rewrite < H.
   apply divides_gcd_nm
 ]
@@ -605,39 +609,26 @@ qed.
 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
 intros.
 auto.
-(*apply (nat_case1 (gcd m n))
-[ intros.
-  generalize in match (gcd_O_to_eq_O m n H1).
-  intros.
-  elim H2.
-  rewrite < H4 in \vdash (? ? %).
-  assumption
-| intros.
-  unfold lt.
-  apply le_S_S.
-  apply le_O_n
-]*)
+(*
+apply (divides_to_lt_O (gcd m n) n ? ?);
+  [apply (H).
+  |apply (divides_gcd_m m n).
+  ]
+*)
 qed.
 
 theorem gcd_n_n: \forall n.gcd n n = n.
 intro.
 auto.
-(*elim n
-[ reflexivity
-| apply le_to_le_to_eq
-  [ apply divides_to_le
-    [ apply lt_O_S
-    | apply divides_gcd_n      
-    ]
-  | apply divides_to_le
-    [ apply lt_O_gcd.apply lt_O_S
-    | apply divides_d_gcd
-      [ apply divides_n_n
-      | apply divides_n_n
-      ]
+(*
+apply (antisymmetric_divides (gcd n n) n ? ?);
+  [apply (divides_gcd_n n n).
+  |apply (divides_d_gcd n n n ? ?);
+    [apply (reflexive_divides n).
+    |apply (reflexive_divides n).
     ]
   ]
-]*)
+*)
 qed.
 
 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
@@ -699,54 +690,19 @@ theorem symmetric_gcd: symmetric nat gcd.
 change with 
 (\forall n,m:nat. gcd n m = gcd m n).
 intros.
-auto.
-(*cut (O < (gcd n m) \lor O = (gcd n m))
-[ elim Hcut
-  [ cut (O < (gcd m n) \lor O = (gcd m n))
-    [ elim Hcut1
-      [ apply antisym_le
-        [ apply divides_to_le
-          [ assumption
-          | apply divides_d_gcd
-            [ apply divides_gcd_n
-            | apply divides_gcd_m
-            ]
-          ]
-        | apply divides_to_le
-          [ assumption
-          | apply divides_d_gcd
-            [ apply divides_gcd_n
-            | apply divides_gcd_m
-            ] 
-          ]
-        ]
-      | rewrite < H1.
-        cut (m=O \land n=O)
-        [ elim Hcut2.
-          rewrite > H2.
-          rewrite > H3.
-          reflexivity
-        | apply gcd_O_to_eq_O.
-          apply sym_eq.
-          assumption
-        ]
-      ]
-    | apply le_to_or_lt_eq.
-      apply le_O_n
+auto size = 7.
+(*
+apply (antisymmetric_divides (gcd n m) (gcd m n) ? ?);
+  [apply (divides_d_gcd n m (gcd n m) ? ?);
+    [apply (divides_gcd_n n m).
+    |apply (divides_gcd_m n m).
     ]
-  | rewrite < H.
-    cut (n=O \land m=O)
-    [ elim Hcut1.
-      rewrite > H1.
-      rewrite > H2.
-      reflexivity
-    | apply gcd_O_to_eq_O.apply sym_eq.
-      assumption
+  |apply (divides_d_gcd m n (gcd m n) ? ?);
+    [apply (divides_gcd_n m n).
+    |apply (divides_gcd_m m n).
     ]
   ]
-| apply le_to_or_lt_eq.
-  apply le_O_n
-]*)
+*)
 qed.
 
 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
@@ -844,36 +800,19 @@ qed.
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.
 auto.
-(*apply antisym_le
-[ apply divides_to_le
-  [ unfold lt.
-    apply le_n
-  | apply divides_gcd_n
+(*
+apply (symmetric_eq nat (S O) (gcd (S O) n) ?).
+apply (antisymmetric_divides (S O) (gcd (S O) n) ? ?);
+  [apply (divides_SO_n (gcd (S O) n)).
+  |apply (divides_gcd_n (S O) n).
   ]
-| cut (O < gcd (S O) n \lor O = gcd (S O) n)
-  [ elim Hcut
-    [ assumption
-    | apply False_ind.
-      apply (not_eq_O_S O).
-      cut ((S O)=O \land n=O)
-      [ elim Hcut1.
-        apply sym_eq.
-        assumption
-      | apply gcd_O_to_eq_O.
-        apply sym_eq.
-        assumption
-      ]
-    ]
-  | apply le_to_or_lt_eq.
-    apply le_O_n
-  ]
-]*)
+*)
 qed.
 
 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
 divides (gcd m n) (gcd n (m \mod n)).
 intros.
-auto.
+auto width = 4.
 (*apply divides_d_gcd
 [ apply divides_mod
   [ assumption
@@ -920,7 +859,8 @@ apply antisym_le
 [ apply not_lt_to_le.unfold Not.unfold lt.
   intro.
   apply H1.
-  rewrite < (H3 (gcd n m));auto
+  rewrite < (H3 (gcd n m));
+  [auto|auto| unfold lt; auto]
   (*[ apply divides_gcd_m
   | apply divides_gcd_n
   | assumption
@@ -1025,7 +965,16 @@ apply antisymmetric_le
       [ auto
         (*apply lt_SO_smallest_factor.
         assumption*)
-      | apply divides_to_le;auto
+      | apply divides_to_le; 
+        [ auto |   
+        apply divides_d_gcd
+         [ assumption
+         | apply (transitive_divides ? (gcd m (n*p)))
+           [ auto.
+           | auto.
+           ]
+         ]
+        ]
         (*[ rewrite > H2.
           unfold lt.
           apply le_n
@@ -1049,7 +998,16 @@ apply antisymmetric_le
       apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
       [ apply lt_SO_smallest_factor.
         assumption
-      | apply divides_to_le;auto
+      | apply divides_to_le; 
+        [ auto |
+        apply divides_d_gcd
+         [ assumption
+         | apply (transitive_divides ? (gcd m (n*p)))
+           [ auto.
+           | auto.
+           ]
+         ]
+        ]
         (*[ rewrite > H3.
           unfold lt.
           apply le_n
@@ -1068,7 +1026,14 @@ apply antisymmetric_le
         ]*)
       ]
     ]
-  | apply divides_times_to_divides;auto
+  | apply divides_times_to_divides;
+    [ auto | 
+      apply (transitive_divides ? (gcd m (n*p)))
+           [ auto.
+           | auto.
+           ]
+         ]
+        ]
     (*[ apply prime_smallest_factor_n.
       assumption
     | auto.apply (transitive_divides ? (gcd m (n*p)))
@@ -1081,7 +1046,6 @@ apply antisymmetric_le
       | apply divides_gcd_m
       ]
     ]*)
-  ]
 | auto
   (*change with (O < gcd m (n*p)).
   apply lt_O_gcd.
index edc677b2fdfcf192b63fbe9b170889c0e8444bfb..8d948a510a354d04ad7454ebc96a154d090995bb 100644 (file)
@@ -46,9 +46,8 @@ unfold Not.
 intro.
 apply (not_divides_S_fact n (smallest_factor(S n!)))
 [ apply lt_SO_smallest_factor.
-  auto
-  (*unfold lt.
-  apply le_S_S.
+  unfold lt.auto
+  (*apply le_S_S.
   apply le_SO_fact*)
 | assumption
 | auto
@@ -80,9 +79,8 @@ elim H
     ]*)
   | (* Andrea: ancora hint non lo trova *)
     apply prime_smallest_factor_n.
-    auto
-    (*unfold lt.
-    apply le_S.
+    unfold lt.auto
+    (*apply le_S.
     apply le_SSO_fact.
     unfold lt.
     apply le_S_S.
@@ -101,7 +99,7 @@ match n with
     
 (* it works, but nth_prime 4 takes already a few minutes -
 it must compute factorial of 7 ...*)
-
+(*
 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
 auto.
 (*normalize.reflexivity.*)
@@ -116,7 +114,7 @@ theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O)))))))))
 auto.
 (*normalize.reflexivity.*)
 qed.
-
+*)
 (*
 theorem example14 : nth_prime (S(S(S(S(S O))))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
 normalize.reflexivity.
@@ -152,9 +150,8 @@ apply (nat_case n)
     ]
   | apply prime_to_primeb_true.
     apply prime_smallest_factor_n.
-    auto
-    (*unfold lt.
-    apply le_S_S.
+    unfold lt.auto
+    (*apply le_S_S.
     apply le_SO_fact*)
   ]
 ]
@@ -195,9 +192,8 @@ intros.
  * ancora terminata
  *)
 elim n
-[ auto
-  (*unfold lt.
-  apply le_n*)
+[ unfold lt.auto
+  (*apply le_n*)
 | auto
   (*apply (trans_lt ? (nth_prime n1))
   [ assumption
index 3df876c6918c46d4563fba870fd3ccd637e45d48..c51f828eff56a43d425f483e68c61a56be6cbde8 100644 (file)
@@ -214,6 +214,8 @@ apply p_ord_aux_to_Prop1;
   assumption.
 qed.
 
+axiom not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
+
 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
 n = p \sup q * r \to p_ord n p = pair nat nat q r.
 intros.
@@ -257,8 +259,7 @@ apply p_ord_exp
           ]
         ]
       ]*)
-    | alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
-      apply not_eq_to_le_to_lt
+    | apply not_eq_to_le_to_lt
       [ unfold.
         intro.
         auto
index dc19fb65bc9cde562f6e75bce759d2d3f2a90566..ee925ed38b90af2c02001a5a215ef7feba89d429 100644 (file)
@@ -510,17 +510,11 @@ cut (n! \mod i = O)
   | rewrite > Hcut.
     assumption
   ]
-| auto
-  (*apply divides_to_mod_O
-  [ apply (trans_lt O (S O))
-    [ apply (le_n (S O))
-    | assumption 
-    ]
+| auto(*
+  apply divides_to_mod_O
+  [ apply ltn_to_ltO [| apply H]
   | apply divides_fact
-    [ apply (trans_lt O (S O))
-      [ apply (le_n (S O))
-      | assumption
-      ]
+    [ apply ltn_to_ltO [| apply H]
     | assumption
     ]
   ]*)
@@ -643,9 +637,8 @@ apply (nat_case n)
       (*unfold lt.
       apply le_n*)
     | apply lt_SO_smallest_factor.
-      auto
-      (*unfold lt.
-      apply le_S_S.
+      unfold lt.auto
+      (*apply le_S_S.
       apply le_S_S.
       apply le_O_n*)     
     ]
@@ -902,9 +895,8 @@ apply (nat_case n)
       simplify.
       rewrite < H.
       apply prime_smallest_factor_n.
-      auto
-      (*unfold lt.
-      apply le_S_S.
+      unfold lt.auto
+      (*apply le_S_S.
       apply le_S_S.
       apply le_O_n*)
     | intro.
index 6d11b4fa1b7c06f57b11879db7a8787dc1a8e703..9a2f3fd3942c83e9ee864dc0faf1736529eefd0c 100644 (file)
   </child>
 </widget>
 
+<widget class="GtkWindow" id="AutoWin">
+  <property name="width_request">600</property>
+  <property name="height_request">400</property>
+  <property name="visible">True</property>
+  <property name="title" translatable="yes">Auto</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_CENTER</property>
+  <property name="modal">False</property>
+  <property name="resizable">True</property>
+  <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+  <property name="focus_on_map">True</property>
+  <property name="urgency_hint">False</property>
+
+  <child>
+    <widget class="GtkVBox" id="vbox17">
+      <property name="visible">True</property>
+      <property name="homogeneous">False</property>
+      <property name="spacing">0</property>
+
+      <child>
+       <widget class="GtkHBox" id="hbox30">
+         <property name="visible">True</property>
+         <property name="homogeneous">False</property>
+         <property name="spacing">2</property>
+
+         <child>
+           <widget class="GtkScrolledWindow" id="scrolledwindow14">
+             <property name="visible">True</property>
+             <property name="can_focus">True</property>
+             <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+             <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+             <property name="shadow_type">GTK_SHADOW_IN</property>
+             <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+             <child>
+               <widget class="GtkViewport" id="viewport3">
+                 <property name="visible">True</property>
+                 <property name="shadow_type">GTK_SHADOW_IN</property>
+
+                 <child>
+                   <widget class="GtkTable" id="table">
+                     <property name="visible">True</property>
+                     <property name="n_rows">3</property>
+                     <property name="n_columns">3</property>
+                     <property name="homogeneous">False</property>
+                     <property name="row_spacing">0</property>
+                     <property name="column_spacing">0</property>
+                   </widget>
+                 </child>
+               </widget>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">True</property>
+             <property name="fill">True</property>
+           </packing>
+         </child>
+
+         <child>
+           <widget class="GtkVBox" id="vbox18">
+             <property name="visible">True</property>
+             <property name="homogeneous">False</property>
+             <property name="spacing">0</property>
+
+             <child>
+               <widget class="GtkButton" id="buttonUP">
+                 <property name="visible">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
+
+                 <child>
+                   <widget class="GtkAlignment" id="alignment19">
+                     <property name="visible">True</property>
+                     <property name="xalign">0.5</property>
+                     <property name="yalign">0.5</property>
+                     <property name="xscale">0</property>
+                     <property name="yscale">0</property>
+                     <property name="top_padding">0</property>
+                     <property name="bottom_padding">0</property>
+                     <property name="left_padding">0</property>
+                     <property name="right_padding">0</property>
+
+                     <child>
+                       <widget class="GtkHBox" id="hbox31">
+                         <property name="visible">True</property>
+                         <property name="homogeneous">False</property>
+                         <property name="spacing">2</property>
+
+                         <child>
+                           <widget class="GtkImage" id="image1066">
+                             <property name="visible">True</property>
+                             <property name="stock">gtk-go-up</property>
+                             <property name="icon_size">4</property>
+                             <property name="xalign">0.5</property>
+                             <property name="yalign">0.5</property>
+                             <property name="xpad">0</property>
+                             <property name="ypad">0</property>
+                           </widget>
+                           <packing>
+                             <property name="padding">0</property>
+                             <property name="expand">False</property>
+                             <property name="fill">False</property>
+                           </packing>
+                         </child>
+
+                         <child>
+                           <widget class="GtkLabel" id="label30">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes"></property>
+                             <property name="use_underline">True</property>
+                             <property name="use_markup">False</property>
+                             <property name="justify">GTK_JUSTIFY_LEFT</property>
+                             <property name="wrap">False</property>
+                             <property name="selectable">False</property>
+                             <property name="xalign">0.5</property>
+                             <property name="yalign">0.5</property>
+                             <property name="xpad">0</property>
+                             <property name="ypad">0</property>
+                             <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                             <property name="width_chars">-1</property>
+                             <property name="single_line_mode">False</property>
+                             <property name="angle">0</property>
+                           </widget>
+                           <packing>
+                             <property name="padding">0</property>
+                             <property name="expand">False</property>
+                             <property name="fill">False</property>
+                           </packing>
+                         </child>
+                       </widget>
+                     </child>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="padding">0</property>
+                 <property name="expand">True</property>
+                 <property name="fill">True</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkButton" id="buttonDOWN">
+                 <property name="visible">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
+
+                 <child>
+                   <widget class="GtkImage" id="image1065">
+                     <property name="visible">True</property>
+                     <property name="stock">gtk-go-down</property>
+                     <property name="icon_size">4</property>
+                     <property name="xalign">0.5</property>
+                     <property name="yalign">0.5</property>
+                     <property name="xpad">0</property>
+                     <property name="ypad">0</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="padding">0</property>
+                 <property name="expand">True</property>
+                 <property name="fill">True</property>
+               </packing>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">False</property>
+             <property name="fill">False</property>
+           </packing>
+         </child>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">True</property>
+         <property name="fill">True</property>
+       </packing>
+      </child>
+
+      <child>
+       <widget class="GtkHSeparator" id="hseparator3">
+         <property name="visible">True</property>
+       </widget>
+       <packing>
+         <property name="padding">3</property>
+         <property name="expand">False</property>
+         <property name="fill">True</property>
+       </packing>
+      </child>
+
+      <child>
+       <widget class="GtkHBox" id="hbox32">
+         <property name="visible">True</property>
+         <property name="homogeneous">False</property>
+         <property name="spacing">0</property>
+
+         <child>
+           <widget class="GtkLabel" id="labelLAST">
+             <property name="visible">True</property>
+             <property name="label" translatable="yes">Last:</property>
+             <property name="use_underline">False</property>
+             <property name="use_markup">False</property>
+             <property name="justify">GTK_JUSTIFY_LEFT</property>
+             <property name="wrap">False</property>
+             <property name="selectable">False</property>
+             <property name="xalign">0</property>
+             <property name="yalign">0.5</property>
+             <property name="xpad">0</property>
+             <property name="ypad">0</property>
+             <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+             <property name="width_chars">-1</property>
+             <property name="single_line_mode">False</property>
+             <property name="angle">0</property>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">True</property>
+             <property name="fill">True</property>
+           </packing>
+         </child>
+
+         <child>
+           <widget class="GtkHButtonBox" id="hbuttonbox3">
+             <property name="border_width">4</property>
+             <property name="visible">True</property>
+             <property name="layout_style">GTK_BUTTONBOX_END</property>
+             <property name="spacing">4</property>
+
+             <child>
+               <widget class="GtkButton" id="buttonPAUSE">
+                 <property name="visible">True</property>
+                 <property name="can_default">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="label">gtk-media-pause</property>
+                 <property name="use_stock">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
+               </widget>
+             </child>
+
+             <child>
+               <widget class="GtkButton" id="buttonPLAY">
+                 <property name="visible">True</property>
+                 <property name="can_default">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="label">gtk-media-play</property>
+                 <property name="use_stock">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
+               </widget>
+             </child>
+
+             <child>
+               <widget class="GtkButton" id="buttonNEXT">
+                 <property name="visible">True</property>
+                 <property name="can_default">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="label">gtk-media-next</property>
+                 <property name="use_stock">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
+               </widget>
+             </child>
+
+             <child>
+               <widget class="GtkButton" id="buttonCLOSE">
+                 <property name="visible">True</property>
+                 <property name="can_default">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="label">gtk-close</property>
+                 <property name="use_stock">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
+               </widget>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">True</property>
+             <property name="fill">True</property>
+           </packing>
+         </child>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">False</property>
+         <property name="fill">True</property>
+       </packing>
+      </child>
+    </widget>
+  </child>
+</widget>
+
 </glade-interface>
index a23558aa85e0ff83ca12707b4c732a4ba6db829c..5df8656cdbb4cdbdffb930971c2ea4a0b19210ff 100644 (file)
@@ -258,6 +258,8 @@ let _ =
         ~doc:(HExtlib.unopt (mview ())#get_document) ~name:"matita.xml" ())); *)
     addDebugItem "load (sequent) MathML from matita.xml"
       (fun _ -> (mview ())#load_uri ~filename:"matita.xml");
+    addDebugItem "autoWin"
+    (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
   end
   (** Debugging }}} *)
 
diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
new file mode 100644 (file)
index 0000000..e3a5bff
--- /dev/null
@@ -0,0 +1,165 @@
+(* Copyright (C) 2003, HELM Team.
+ * 
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+type status = 
+  Cic.context * (Cic.term * (int * Cic.term) list) list * Cic.term list *
+  Cic.term list
+let fake_goal = Cic.Implicit None;;
+let fake_candidates = [];;
+
+let start = ref 0;;
+let len = ref 10;;
+
+let pp c t =
+  let names = List.map (function None -> None | Some (n,_) -> Some n) c in
+  let t = 
+    ProofEngineReduction.replace 
+      ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false) 
+      ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t
+  in
+  CicPp.pp t names
+;;
+let pp_goal context x = 
+  if x == fake_goal then "" else pp context x
+;;
+let pp_candidate context x = pp context x
+
+let sublist start len l = 
+  let rec aux pos len = function
+    | [] when pos < start -> aux (pos+1) len []
+    | [] when len > 0 -> (fake_goal, fake_candidates) :: aux (pos+1) (len-1) [] 
+    | [] (* when len <= 0 *) -> []
+    | he::tl when pos < start -> aux (pos+1) len tl
+    | he::tl when pos >= start && len > 0 -> he::aux (pos+1) (len-1) tl
+    | he::tl (* when pos >= start && len <= 0 *) -> []
+  in
+  aux 0 len l
+;;
+
+let cell_of_candidate context ?(active=false) g id c = 
+  let tooltip = GData.tooltips () in (* should be only one isn't it? *)
+  let button = 
+    GButton.button 
+      ~label:(pp_candidate context c(* ^ " - " ^ string_of_int id*)) () 
+  in
+  if active then
+    button#misc#set_sensitive false;
+  let text = 
+    "Follow computation of "^pp_candidate context c^" on "^pp_goal context g
+  in
+  tooltip#set_tip ~text (button :> GObj.widget);
+  ignore(button#connect#clicked 
+    (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
+  button
+;;
+let cell_of_goal win_width context goal = 
+  GMisc.label ~text:(pp_goal context goal) ~xalign:0.0 ()
+;;
+let cell_of_int n = 
+  GMisc.label ~text:(string_of_int n) 
+    ~line_wrap:true ~justify:`RIGHT ()
+;;
+let cell_of_candidates context goal cads = 
+  let hbox = GPack.hbox () in
+  match cads with
+  | [] -> hbox
+  | (id,c)::tl ->
+      hbox#pack 
+        (cell_of_candidate ~active:true context goal id c :> GObj.widget);
+      List.iter
+        (fun (id,c) -> 
+        hbox#pack (cell_of_candidate context goal id c :> GObj.widget)) tl;
+        hbox
+;;
+
+let elems_to_rows context win_width (table : GPack.table) (or_list) =
+  let _ = 
+   List.fold_left 
+    (fun position (goal, candidates) ->
+      table#attach ~left:0 ~top:position 
+        (cell_of_int (position + !start) :> GObj.widget);
+      table#attach ~left:1 ~top:position ~expand:`BOTH ~fill:`BOTH
+        (cell_of_goal win_width context goal :> GObj.widget);
+      table#attach ~left:2 ~top:position 
+        (cell_of_candidates context goal candidates :> GObj.widget);
+      position+1)
+    0 or_list
+  in 
+  ()
+;;
+
+let old_displayed_status = ref ([]);;
+let old_size = ref 0;;
+
+let fill_win (win : MatitaGeneratedGui.autoWin) cb =
+  let init = Unix.gettimeofday () in
+    try 
+      let (status : status) = cb () in
+      let win_size = win#toplevel#misc#allocation.Gtk.width in
+      let ctx, or_list, and_list, last_moves = status in
+      let displayed_status = 
+        sublist !start !len (or_list @ (List.map (fun x -> x,[]) and_list)) 
+      in
+      if displayed_status <> !old_displayed_status || !old_size <> win_size then
+        begin
+          old_displayed_status := displayed_status;
+          old_size := win_size;
+          win#labelLAST#set_text 
+            (String.concat ";" (List.map (pp_candidate ctx) last_moves));
+          List.iter win#table#remove win#table#children;
+          elems_to_rows ctx win_size win#table displayed_status;
+          Printf.eprintf 
+            "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -.  init);
+        end
+    with exn -> prerr_endline (Printexc.to_string exn); ()
+;;
+
+let auto_dialog elems =
+  let win = new MatitaGeneratedGui.autoWin () in
+  win#check_widgets ();
+  win#table#set_columns 3;
+  win#table#set_col_spacings 6;
+  win#table#set_row_spacings 4;
+  ignore(win#buttonUP#connect#clicked 
+    (fun _ -> start := max 0 (!start -1); fill_win win elems));
+  ignore(win#buttonDOWN#connect#clicked 
+    (fun _ -> incr start; fill_win win elems));
+  ignore(win#buttonCLOSE#connect#clicked 
+    (fun _ -> win#toplevel#destroy ();GMain.Main.quit ()));
+  let redraw_callback _ = fill_win win elems;true in
+  let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
+  ignore(win#buttonPAUSE#connect#clicked 
+    (fun _ -> Auto.pause true));
+  ignore(win#buttonPLAY#connect#clicked 
+    (fun _ -> Auto.pause false;Auto.step ()));
+  ignore(win#buttonNEXT#connect#clicked 
+    (fun _ -> Auto.step ()));
+  fill_win win elems;
+  win#toplevel#show ();
+  GtkThread.main ();
+  GMain.Timeout.remove redraw;
+;;
+