moved to pkg-ocaml-maint

[helm.git] / components / tactics / autoTypes.ml

diff --git a/components/tactics/autoTypes.ml b/components/tactics/autoTypes.ml
index f9d6a021621bb3f77aacbc84323f7eba20487c68..874a20dccf4b366bda48cae857dbf6744a2702f6 100644 (file)
--- a/components/tactics/autoTypes.ml
+++ b/components/tactics/autoTypes.ml
@@ -23,126 +23,39 @@
  * 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
-;;
-
-(* (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 = []
-
 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;
 }
 
-let default_flags = {
-  maxwidth = 3;
-  maxdepth = 5;
-  timeout = 0.;
+let default_flags _ =
+  {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;
 }
+;;
 
 (* (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