X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTypes.ml;h=9bced7618e08ad290726b01089e09a2a1a28b721;hb=abf25195eddebc8859736ff782cade507fdb780e;hp=60643d8702d29822ba15a5243411a584ca534e2c;hpb=041ad23b567b9844ec187ad436595868441802f4;p=helm.git

diff --git a/helm/software/components/tactics/autoTypes.ml b/helm/software/components/tactics/autoTypes.ml
index 60643d870..9bced7618 100644
--- a/helm/software/components/tactics/autoTypes.ml
+++ b/helm/software/components/tactics/autoTypes.ml
@@ -23,144 +23,43 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
-module Codomain = struct 
-  type t = Cic.term 
-  let compare = Pervasives.compare 
-end
-module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
-type universe = TI.t
-
-let empty_universe = TI.empty
-let get_candidates universe ty = 
-  S.elements (TI.retrieve_unifiables universe ty)
-;;
-let rec head = function 
-  | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
-  | t -> t
-;;
-let index acc key term =
-  match key with
-  | Cic.Meta _ -> acc
-  | _ -> 
-      prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
-      TI.index acc key term
-;;
-let universe_of_goals dbd proof gl universe = 
-  let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
-  let terms = List.map CicUtil.term_of_uri univ in
-  let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in
-  List.fold_left 
-    (fun acc term -> 
-      let key = head (tyof term) in
-      index acc key term)
-    universe terms
-;;
-let universe_of_context ctx metasenv universe =  
-  let tail = function [] -> [] | h::tl -> tl in
-  let rc,_,_ = 
-    List.fold_left 
-    (fun (acc,i,ctx) ctxentry ->
-      match ctxentry with
-      | Some (_,Cic.Decl t) -> 
-          let key = CicSubstitution.lift i (head t) in
-          let elem = Cic.Rel i in
-          index acc key elem, i+1, tail ctx
-      | Some (_,Cic.Def (_,Some t)) ->
-          let key = CicSubstitution.lift i (head t) in
-          let elem = Cic.Rel i in
-          index acc key elem, i+1, tail ctx
-      | Some (_,Cic.Def (t,None)) ->
-          let ctx = tail ctx in 
-          let key,_ = 
-            CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph
-          in
-          let elem = Cic.Rel i in
-          let key = CicSubstitution.lift i (head key) in
-          index acc key elem, i+1, ctx
-      |  _ -> universe,i+1,tail ctx)
-    (universe,1,ctx) ctx
-  in
-  rc
-;;
-let add_to_universe key proof universe =
-  index universe key proof
-;;
-
-(* (proof,ty) list *)
-type cache_key = Cic.term
-type cache_elem = 
-  | Failed_in of int
-  | Succeded of Cic.term
-  | UnderInspection
-  | Notfound
-type cache = (cache_key * cache_elem) list
-let cache_examine cache cache_key = 
-  try List.assoc cache_key cache with Not_found -> Notfound
-;;
-let cache_replace cache key v =
-  let cache = List.filter (fun (i,_) -> i <> key) cache in
-  (key,v)::cache
-;;
-let cache_add_failure cache cache_key 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 -> 
-      prerr_endline (CicPp.ppterm t);
-      assert false (* if succed it can't fail *)
-;;
-let cache_add_success cache cache_key proof =
-  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 cache cache_key depth =
-  match cache_examine cache cache_key with
-  | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
-  | Notfound -> (cache_key,UnderInspection)::cache
-  | Failed_in _ 
-  | UnderInspection 
-  | Succeded _ -> assert false (* it must be a new goal *)
-;;
-let cache_empty = []
-let cache_print context cache = 
-  let names = List.map (function None -> None | Some (x,_) -> Some x) context in
-  String.concat "\n" 
-    (HExtlib.filter_map 
-      (function 
-        | (k,Succeded _) -> Some (CicPp.pp k names)
-        | _ -> None)
-      cache)
-;;
-let cache_size cache = 
-  List.length (List.filter (function (_,Succeded _) -> true | _ -> false) cache)
-;;
-let cache_clean cache = 
-  List.filter (function (_,Succeded _) -> true | _ -> false) cache
-;;
-
 type flags = {
   maxwidth: int;
+  maxsize: int;
   maxdepth: int;
+  maxgoalsizefactor : int;
   timeout: float;
+  use_library: bool;
   use_paramod: bool;
   use_only_paramod : bool;
+  close_more : bool; 
+  dont_cache_failures: bool;
+  do_types: bool;
+  skip_trie_filtering: bool;
+  skip_context: bool;
 }
 
 let default_flags _ =
-  {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. 3.0;use_paramod=true;use_only_paramod=false}
+  {maxwidth=3;
+   maxdepth=3;
+   maxsize = 6;
+   maxgoalsizefactor = max_int;
+   timeout=Unix.gettimeofday() +.3.0;
+   use_library=false;
+   use_paramod=true;
+   use_only_paramod=false;
+   close_more=false; 
+   dont_cache_failures=false;
+   do_types=false;
+   skip_trie_filtering=false;
+   skip_context=false;
+}
 ;;
 
 (* (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