X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=3c8c89468e0f46d9334eb95e4819ca32ff2c2ebe;hb=45a9e84c12f57e5473eccc6f611cdbb343998d5d;hp=b439b6cfc6efa2c383b0389a09532fa808dc3ef0;hpb=36809208fa25a494e50004b321fa9a90108ae262;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index b439b6cfc..3c8c89468 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -30,6 +30,16 @@ let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
+let is_propositional context sort = 
+  match CicReduction.whd context sort with
+  | Cic.Sort Cic.Prop 
+  | Cic.Sort (Cic.CProp _) -> true
+  | _-> false
+;;
+
+
+type auto_params = Cic.term list * (string * string) list 
+
 let elems = ref [] ;;
 
 (* closing a term w.r.t. its metavariables
@@ -66,11 +76,11 @@ let naif_closure ?(prefix_name="xxx_") t metasenv context =
 let lambda_close ?prefix_name t menv ctx =
   let t = naif_closure ?prefix_name t menv ctx in
     List.fold_left
-      (fun t -> function 
-        | None -> CicSubstitution.subst (Cic.Implicit None) t (* delift *)
-        | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t)
-        | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t))
-      t ctx
+      (fun (t,i) -> function 
+        | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
+        | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
+        | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1)
+      (t,List.length menv) ctx
 ;;
   
 (* functions for retrieving theorems *)
@@ -88,7 +98,7 @@ let find_library_theorems dbd proof goal =
   let terms = List.map CicUtil.term_of_uri univ in
   List.map 
     (fun t -> 
-       (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph))) 
+       (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph))) 
     terms
 
 let find_context_theorems context metasenv =
@@ -98,16 +108,9 @@ let find_context_theorems context metasenv =
          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 (_,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
-               in
-                 (t,ty)::res,i+1
-           |  _ -> res,i+1)
+           | None -> res,i+1)
       ([],1) context
   in l
 
@@ -136,18 +139,16 @@ let is_unit_equation context metasenv oldnewmeta term =
           let _,_,mt = CicUtil.lookup_meta i metasenv in
           let sort,u = 
             CicTypeChecker.type_of_aux' metasenv context mt 
-              CicUniv.empty_ugraph
-          in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
+              CicUniv.oblivion_ugraph
           in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
     if propositional_args = [] then 
-      let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+      let newmetas = 
+        List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv 
+      in
         Some (args,metasenv,newmetas,head,newmeta)
     else None
 ;;
@@ -163,19 +164,21 @@ let get_candidates universe cache t =
   candidates
 ;;
 
-let only signature context t =
+let only signature context metasenv t =
   try
-    let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
+    let ty,_ = 
+      CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph 
+    in
     let consts = MetadataConstraints.constants_of ty in
     let b = MetadataConstraints.UriManagerSet.subset consts signature in
     if b then b 
     else
-      try
-        let ty' = unfold context ty in
-        let consts' = MetadataConstraints.constants_of ty' in
-        MetadataConstraints.UriManagerSet.subset consts' signature 
-      with _-> false
-  with _ -> false
+      let ty' = unfold context ty in
+      let consts' = MetadataConstraints.constants_of ty' in
+      MetadataConstraints.UriManagerSet.subset consts' signature 
+  with 
+  | CicTypeChecker.TypeCheckerFailure _ -> assert false
+  | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
 ;;
 
 let not_default_eq_term t =
@@ -184,7 +187,7 @@ let not_default_eq_term t =
       not (LibraryObjects.in_eq_URIs uri)
   with Invalid_argument _ -> true
 
-let retrieve_equations signature universe cache context=
+let retrieve_equations dont_filter signature universe cache context metasenv =
   match LibraryObjects.eq_URI() with
     | None -> [] 
     | Some eq_uri -> 
@@ -192,11 +195,10 @@ let retrieve_equations signature universe cache context=
         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 -> debug_print (lazy (CicPp.ppterm t))) candidates;
-        candidates
+        if dont_filter then candidates
+        else 
+          let candidates = List.filter not_default_eq_term candidates in
+          List.filter (only signature context metasenv) candidates 
 
 let build_equality bag head args proof newmetas maxmeta = 
   match head with
@@ -218,6 +220,14 @@ let build_equality bag head args proof newmetas maxmeta =
 let partition_unit_equalities context metasenv newmeta bag equations =
   List.fold_left
     (fun (units,other,maxmeta)(t,ty) ->
+       if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
+         let _ = 
+           HLog.warn 
+           ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
+             ^ " since it is not meta closed")
+         in
+         units,(t,ty)::other,maxmeta
+       else
        match is_unit_equation context metasenv maxmeta ty with
          | Some (args,metasenv,newmetas,head,newmeta') ->
              let maxmeta,equality =
@@ -232,50 +242,58 @@ let empty_tables =
    Saturation.make_passive [],
    Equality.mk_equality_bag)
 
-let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
+let init_cache_and_tables 
+  ?dbd use_library paramod use_context dont_filter universe (proof, goal) 
+=
   (* the local cache in initially empty  *)
   let cache = AutoCache.cache_empty in
   let _, metasenv, _subst,_, _, _ = proof in
   let signature = MetadataQuery.signature_of metasenv goal in
   let newmeta = CicMkImplicit.new_meta metasenv [] in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let ct = find_context_theorems context metasenv in
+  let ct = if use_context then find_context_theorems context metasenv else [] in
   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
+    match use_library, dbd with
+    | true, Some dbd -> find_library_theorems dbd metasenv goal 
+    | _ -> []
+  in
   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
+    retrieve_equations dont_filter signature universe cache context metasenv 
+  in
   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
-           (* retrieve_equations could also return flexible terms *)
-           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
-             with _ -> None) (* catturare l'eccezione giusta di unfold *)
-      equations in
+           CicTypeChecker.type_of_aux' 
+             metasenv context t CicUniv.oblivion_ugraph
+         in
+         (* retrieve_equations could also return flexible terms *)
+         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
+           with ProofEngineTypes.Fail _ -> None) 
+      equations
+  in
   let bag = Equality.mk_equality_bag () in
   let units, other_equalities, newmeta = 
-    partition_unit_equalities context metasenv newmeta bag eqs_and_types in
-  (* let env = (metasenv, context, CicUniv.empty_ugraph) in 
-    let equalities = 
-    let eq_uri = 
-    match LibraryObjects.eq_URI() with
-      | None ->assert false
-      | Some eq_uri -> eq_uri in
-    Saturation.simplify_equalities bag eq_uri env units in *)
+    partition_unit_equalities context metasenv newmeta bag eqs_and_types 
+  in
+  (* SIMPLIFICATION STEP 
+  let equalities = 
+    let env = (metasenv, context, CicUniv.oblivion_ugraph) in 
+    let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
+    Saturation.simplify_equalities bag eq_uri env units 
+  in 
+  *)
   let passive = Saturation.make_passive units in
   let no = List.length units in
   let active = Saturation.make_active [] in
@@ -298,13 +316,9 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u
           let _,_,mt = CicUtil.lookup_meta i metasenv in
           let sort,u = 
             CicTypeChecker.type_of_aux' metasenv context mt 
-              CicUniv.empty_ugraph
+              CicUniv.oblivion_ugraph
           in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
-          in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
@@ -380,12 +394,15 @@ let close_more tables maxmeta context status auto universe cache =
   let proof, goalno = status in
   let _, metasenv,_subst,_,_, _ = proof in  
   let signature = MetadataQuery.signature_of metasenv goalno in
-  let equations = retrieve_equations signature universe cache context in
+  let equations = 
+    retrieve_equations false signature universe cache context metasenv 
+  in
   let eqs_and_types =
     HExtlib.filter_map 
       (fun t -> 
          let ty,_ =
-           CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
+           CicTypeChecker.type_of_aux' metasenv context t
+           CicUniv.oblivion_ugraph in
            (* retrieve_equations could also return flexible terms *)
            if is_an_equality ty then Some(t,ty) else None)
       equations in
@@ -466,6 +483,80 @@ let find_context_equalities
   indexes, equalities, maxm, cache
 ;;
 
+(********** PARAMETERS PASSING ***************)
+
+let bool params name default =
+    try 
+      let s = List.assoc name params in 
+      if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
+      else if s = "0" || s = "false" || s = "no" || s= "off" then false
+      else 
+        let msg = "Unrecognized value for parameter "^name^"\n" in
+        let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
+        raise (ProofEngineTypes.Fail (lazy msg))
+    with Not_found -> default
+;; 
+
+let string params name default =
+    try List.assoc name params with
+    | Not_found -> default
+;; 
+
+let int params name default =
+    try int_of_string (List.assoc name params) with
+    | Not_found -> default
+    | Failure _ -> 
+        raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
+;;  
+
+let flags_of_params params ?(for_applyS=false) () =
+ let int = int params in
+ let bool = bool params in
+ let close_more = bool "close_more" false in
+ let use_paramod = bool "use_paramod" true in
+ let use_only_paramod =
+  if for_applyS then true else bool "paramodulation" false in
+ let use_library = bool "library"  
+   ((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 gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
+ let do_type = bool "type" false 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
+       else
+         infinity
+      else
+       Unix.gettimeofday() +. (float_of_int timeout);
+    AutoTypes.use_library = use_library; 
+    AutoTypes.use_paramod = use_paramod;
+    AutoTypes.use_only_paramod = use_only_paramod;
+    AutoTypes.close_more = close_more;
+    AutoTypes.dont_cache_failures = false;
+    AutoTypes.maxgoalsizefactor = gsize;
+    AutoTypes.do_types = do_type;
+  }
+
+let universe_of_params metasenv context universe tl =
+  if tl = [] then universe else 
+   let tys =
+     List.map 
+       (fun term ->
+         fst (CicTypeChecker.type_of_aux' metasenv context term
+                CicUniv.oblivion_ugraph))
+       tl          
+   in
+     Universe.index_list Universe.empty context (List.combine tl tys)
+;;
+
+
 (***************** applyS *******************)
 
 let new_metasenv_and_unify_and_t 
@@ -509,7 +600,7 @@ let new_metasenv_and_unify_and_t
  in
  match 
    let (active, passive,bag), cache, maxmeta =
-     init_cache_and_tables dbd flags.use_library true universe
+     init_cache_and_tables ~dbd flags.use_library true true false universe
      (proof'''',newmeta)
    in
      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive 
@@ -528,12 +619,16 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
+let apply_smart 
+  ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal) 
+=
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
   let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let flags = flags_of_params params ~for_applyS:true () in
+  let universe = universe_of_params metasenv context universe univ in
   let newmeta = CicMkImplicit.new_meta metasenv subst in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
@@ -569,7 +664,7 @@ let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
    in
    let metasenv' = metasenv@newmetasenvfragment in
    let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
    in
    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
    let goal_arity = count_prods context ty in
@@ -583,21 +678,21 @@ let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
 (****************** AUTO ********************)
 
 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
-let ugraph = CicUniv.empty_ugraph;;
+let ugraph = CicUniv.oblivion_ugraph;;
 let typeof = CicTypeChecker.type_of_aux';;
 let ppterm ctx t = 
   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
   CicPp.pp t names
 ;;
 let is_in_prop context subst metasenv ty =
-  let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
-  fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
+  let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
+  is_propositional context sort
 ;;
 
 let assert_proof_is_valid proof metasenv context goalty =
   if debug then
     begin
-      let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
+      let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in
       let b,_ = CicReduction.are_convertible context ty goalty u in
         if not b then
           begin
@@ -628,10 +723,7 @@ let split_goals_in_prop metasenv subst gl =
       let _,context,ty = CicUtil.lookup_meta g metasenv in
       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
+        is_propositional context sort
       with 
       | CicTypeChecker.AssertFailure s 
       | CicTypeChecker.TypeCheckerFailure s -> 
@@ -655,10 +747,11 @@ 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 closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
+  let closed_type, open_type = split_goals_with_metas metasenv subst rest in
   let open_goals =
-    (List.map (fun x -> x,P) (closed_prop @ open_prop)) 
+    (List.map (fun x -> x,P) (open_prop @ closed_prop)) 
     @ 
-    (List.map (fun x -> x,T) rest)
+    (List.map (fun x -> x,T) (open_type @ closed_type))
   in
   let tys = 
     List.map 
@@ -714,7 +807,7 @@ 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 candidate = int * Cic.term Lazy.t
 type cache = AutoCache.cache
 type tables = 
   Saturation.active_table * Saturation.passive_table * Equality.equality_bag
@@ -744,8 +837,8 @@ type auto_result =
 (* the status exported to the external observer *)  
 type auto_status = 
   (* context, (goal,candidate) list, and_list, history *)
-  Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list * 
-  (int * Cic.term * int) list * Cic.term list
+  Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * 
+  (int * Cic.term * int) list * Cic.term Lazy.t list
 
 let d_prefix l =
   let rec aux acc = function
@@ -797,7 +890,7 @@ let pp_status ctx status =
     | 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
+    Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
   in
   let string_of_ol m su l =
     String.concat " | " 
@@ -971,7 +1064,6 @@ let add_to_cache_and_del_from_orlist_if_green_cut
   | 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
@@ -1037,7 +1129,7 @@ let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
   subst, metasenv
 ;;
 let mk_fake_proof metasenv subst (goalno,_,_) goalty context = 
-  None,metasenv,subst ,Cic.Meta(goalno,mk_irl context),goalty, [] 
+  None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] 
 ;;
 let equational_case 
   tables maxm cache depth fake_proof goalno goalty subst context 
@@ -1116,7 +1208,7 @@ let try_candidate
     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;
-    Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
+    Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables , maxmeta
   with 
     | ProofEngineTypes.Fail s -> None,tables, maxm
     | CicUnification.Uncertain s ->  None,tables, maxm
@@ -1228,7 +1320,7 @@ let prunable menv subst ty todo =
     | (D (_,_,T))::tl -> aux tl
     | _ -> false
   and no_progress variant = function
-    | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
+    | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
     | D ((n,_,P) as g)::tl -> 
 	(match calculate_goal_ty g subst menv with
            | None -> no_progress variant tl
@@ -1279,7 +1371,8 @@ let auto_main tables maxm context flags universe cache elems =
     | (m, s, _, _, [],_)::orlist ->
         (* complete success *)
         Proved (m, s, orlist, tables, cache, maxm)
-    | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist ->
+    | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist 
+      when not flags.AutoTypes.do_types ->
         (* skip since not Prop, don't even check if closed by side-effect *)
         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
     | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
@@ -1309,7 +1402,7 @@ let auto_main tables maxm context flags universe cache elems =
         (* timeout *)
         debug_print (lazy ("FAIL: TIMEOUT"));
         Gaveup (tables, cache, maxm)
-    | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
+    | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
         (* attack g *)
         match calculate_goal_ty g s m with
         | None -> 
@@ -1324,7 +1417,7 @@ let auto_main tables maxm context flags universe cache elems =
 	      (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
                aux tables maxm flags cache orlist)
             else if prunable_for_size flags s m todo then
-		(prerr_endline ("POTO at depth: "^(string_of_int depth));
+		(debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
 	         aux tables maxm flags cache orlist)
 	    else
             (* still to be proved *)
@@ -1461,70 +1554,12 @@ let auto flags metasenv tables universe cache context metasenv gl =
       None,cache
 ;;
 
-let bool params name default =
-    try 
-      let s = List.assoc name params in 
-      if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
-      else if s = "0" || s = "false" || s = "no" || s= "off" then false
-      else 
-        let msg = "Unrecognized value for parameter "^name^"\n" in
-        let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
-        raise (ProofEngineTypes.Fail (lazy msg))
-    with Not_found -> default
-;; 
-
-let string params name default =
-    try List.assoc name params with
-    | Not_found -> default
-;; 
-
-let int params name default =
-    try int_of_string (List.assoc name params) with
-    | Not_found -> default
-    | Failure _ -> 
-        raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
-;;  
-
-let flags_of_params params ?(for_applyS=false) () =
- let int = int params in
- let bool = bool params in
- let close_more = bool "close_more" false in
- let use_paramod = bool "use_paramod" true in
- let use_only_paramod =
-  if for_applyS then true else bool "paramodulation" false in
- let use_library = bool "library"  
-   ((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 gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) 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
-       else
-         infinity
-      else
-       Unix.gettimeofday() +. (float_of_int timeout);
-    AutoTypes.use_library = use_library; 
-    AutoTypes.use_paramod = use_paramod;
-    AutoTypes.use_only_paramod = use_only_paramod;
-    AutoTypes.close_more = close_more;
-    AutoTypes.dont_cache_failures = false;
-    AutoTypes.maxgoalsizefactor = gsize;
-  }
-
 let applyS_tac ~dbd ~term ~params ~universe =
  ProofEngineTypes.mk_tactic
   (fun status ->
     try 
       let proof, gl,_,_ =
-       apply_smart ~dbd ~term ~subst:[] ~universe
-        (flags_of_params params ~for_applyS:true ()) status
+       apply_smart ~dbd ~term ~subst:[] ~params ~universe status
       in 
        proof, gl
     with 
@@ -1532,185 +1567,45 @@ let applyS_tac ~dbd ~term ~params ~universe =
     | CicTypeChecker.TypeCheckerFailure msg ->
         raise (ProofEngineTypes.Fail msg))
 
-(* SUPERPOSITION *)
-
-(* Syntax: 
- *   auto superposition target = NAME 
- *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
- *
- *  - if table is omitted no superposition will be performed
- *  - if demod_table is omitted no demodulation will be prformed
- *  - subterms_only is passed to Indexing.superposition_right
- *
- *  lists are coded using _ (example: H_H1_H2)
- *)
-
-let eq_and_ty_of_goal = function
-  | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
-      uri,t
-  | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
-;;
-
-let rec find_in_ctx i name = function
-  | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
-  | Some (Cic.Name name', _)::tl when name = name' -> i
-  | _::tl -> find_in_ctx (i+1) name tl
-;;
-
-let rec position_of i x = function
-  | [] -> assert false
-  | j::tl when j <> x -> position_of (i+1) x tl
-  | _ -> i
-;;
-
-
-let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
-  Saturation.reset_refs();
-  let proof,goalno = status in 
-  let curi,metasenv,_subst,pbo,pty, attrs = proof in
-  let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
-  let eq_uri,tty = eq_and_ty_of_goal ty in
-  let env = (metasenv, context, CicUniv.empty_ugraph) in
-  let names = Utils.names_of_context context in
-  let bag = Equality.mk_equality_bag () in
-  let eq_index, equalities, maxm,cache  = 
-    find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty 
-  in
-  let eq_what = 
-    let what = find_in_ctx 1 target context in
-    List.nth equalities (position_of 0 what eq_index)
-  in
-  let eq_other = 
-    if table <> "" then
-      let other = 
-        let others = Str.split (Str.regexp "_") table in 
-        List.map (fun other -> find_in_ctx 1 other context) others 
-      in
-      List.map 
-        (fun other -> List.nth equalities (position_of 0 other eq_index)) 
-        other 
-    else
-      []
-  in
-  let index = List.fold_left Indexing.index Indexing.empty eq_other in
-  let maxm, eql = 
-    if table = "" then maxm,[eq_what] else 
-    Indexing.superposition_right bag
-      ~subterms_only eq_uri maxm env index eq_what
+let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
+  let _,metasenv,_subst,_,_, _ = proof in
+  let _,context,goalty = CicUtil.lookup_meta goal metasenv in
+  let universe = universe_of_params metasenv context universe univ in
+  let flags = flags_of_params params () in
+  let use_library = flags.use_library in
+  let tables,cache,newmeta =
+    init_cache_and_tables ~dbd use_library flags.use_only_paramod true 
+      false 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
+  let initial_time = Unix.gettimeofday() in
+  let (_,oldmetasenv,_subst,_,_, _) = proof in
+  hint := None;
+  let elem = 
+    metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
   in
-  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
-      debug_print (lazy (CicPp.pp t names))) 
-  eql;
-  debug_print (lazy ("\n result proofs: "));
-  List.iter (fun e -> 
-    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;
-  if demod_table <> "" then
-    begin
-      let eql = 
-        if eql = [] then [eq_what] else eql
-      in
-      let demod = 
-        let demod = Str.split (Str.regexp "_") demod_table in 
-        List.map (fun other -> find_in_ctx 1 other context) demod 
-      in
-      let eq_demod = 
-        List.map 
-          (fun demod -> List.nth equalities (position_of 0 demod eq_index)) 
-          demod 
-      in
-      let table = List.fold_left Indexing.index Indexing.empty eq_demod in
-      let maxm,eql = 
-        List.fold_left 
-          (fun (maxm,acc) e -> 
-            let maxm,eq = 
-              Indexing.demodulation_equality bag eq_uri maxm env table e
-            in
-            maxm,eq::acc) 
-          (maxm,[]) eql
-      in
-      let eql = List.rev eql in
-      debug_print (lazy ("\n result [demod]: "));
-      List.iter 
-        (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
-          debug_print (lazy (CicPp.pp t names)))
-      eql;
-    end;
-  proof,[goalno]
-;;
-
-let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
-  (* argument parsing *)
-  let string = string params in
-  let bool = bool params in
-  (* hacks to debug paramod *)
-  let superposition = bool "superposition" false in
-  let target = string "target" "" in
-  let table = string "table" "" in
-  let subterms_only = bool "subterms_only" false in
-  let demod_table = string "demod_table" "" in
-  match superposition with
-  | true -> 
-      (* this is the ugly hack to debug paramod *)
-      superposition_tac 
-        ~target ~table ~subterms_only ~demod_table (proof,goal)
-  | false -> 
-      (* this is the real auto *)
-      let _,metasenv,_subst,_,_, _ = proof 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
-      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
-      let initial_time = Unix.gettimeofday() in
-      let (_,oldmetasenv,_subst,_,_, _) = proof in
-      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));
-            let proof,metasenv =
-            ProofEngineHelpers.subst_meta_and_metasenv_in_proof
-              proof goal subst metasenv
-            in
-            let opened = 
-              ProofEngineHelpers.compare_metasenvs ~oldmetasenv
-                ~newmetasenv:metasenv
-            in
-              proof,opened
-        | Gaveup (tables,cache,maxm) -> 
-            debug_print
-              (lazy ("TIME:"^
-                string_of_float(Unix.gettimeofday()-.initial_time)));
-            raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+  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));*)
+        let proof,metasenv =
+        ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+          proof goal subst metasenv
+        in
+        let opened = 
+          ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+            ~newmetasenv:metasenv
+        in
+          proof,opened
+    | 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 = 
@@ -1722,15 +1617,60 @@ let eq_of_goal = function
   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
 ;;
 
+(* performs steps of rewrite with the universe, obtaining if possible 
+ * a trivial goal *)
+let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= 
+  let _,metasenv,_subst,_,_,_ = proof in
+  let _,context,ty = CicUtil.lookup_meta goal metasenv in
+  let steps = int_of_string (string params "steps" "1") in 
+  let universe = universe_of_params metasenv context universe univ in
+  let eq_uri = eq_of_goal ty in
+  let (active,passive,bag), cache, maxm =
+     (* we take the whole universe (no signature filtering) *)
+     init_cache_and_tables false true false true universe (proof,goal) 
+  in
+  let initgoal = [], metasenv, ty in
+  let table = 
+    let equalities = (Saturation.list_of_passive passive) in
+    (* we demodulate using both actives passives *)
+    List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
+  in
+  let env = metasenv,context,CicUniv.oblivion_ugraph in
+  match Indexing.solve_demodulating bag env table initgoal steps with 
+  | Some (proof, metasenv, newty) ->
+      let refl = 
+        match newty with
+        | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
+            Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
+        | _ -> assert false
+      in
+      let proofterm,_ = 
+        Equality.build_goal_proof 
+          bag eq_uri proof refl newty [] context metasenv
+      in
+      ProofEngineTypes.apply_tactic
+        (PrimitiveTactics.apply_tac ~term:proofterm) status
+  | None -> 
+      raise 
+        (ProofEngineTypes.Fail (lazy 
+          ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
+;;
+let solve_rewrite_tac ~params ~universe () =
+  ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params)
+;;
+
 (* DEMODULATE *)
-let demodulate_tac ~dbd ~universe (proof,goal)= 
+let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= 
   let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let universe = universe_of_params metasenv context universe univ in
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let initgoal = [], [], ty in
+  let initgoal = [], metasenv, ty in
   let eq_uri = eq_of_goal ty in
   let (active,passive,bag), cache, maxm =
-     init_cache_and_tables dbd false true universe (proof,goal) in
+     init_cache_and_tables 
+       ~dbd false true true false universe (proof,goal) 
+  in
   let equalities = (Saturation.list_of_passive passive) in
   (* we demodulate using both actives passives *)
   let table = 
@@ -1740,7 +1680,7 @@ let demodulate_tac ~dbd ~universe (proof,goal)=
   in
   let changed,(newproof,newmetasenv, newty) = 
     Indexing.demodulation_goal bag
-      (metasenv,context,CicUniv.empty_ugraph) table initgoal 
+      (metasenv,context,CicUniv.oblivion_ugraph) table initgoal 
   in
   if changed then
     begin
@@ -1765,8 +1705,8 @@ let demodulate_tac ~dbd ~universe (proof,goal)=
       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
 ;;
 
-let demodulate_tac ~dbd ~universe = 
-  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
+let demodulate_tac ~dbd ~params ~universe = 
+  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);;
 
 let pp_proofterm = Equality.pp_proofterm;;