]> matita.cs.unibo.it Git - helm.git/blobdiff - components/tactics/auto.ml
Even if we are at depth 0, we first check in the cache for a solution,
[helm.git] / components / tactics / auto.ml
index c65826a4feab8e9e319df6219c65a8db70d516ca..c7cffc8af6403383a60a18510dafabf1dd65930a 100644 (file)
 open AutoTypes;;
 open AutoCache;;
 
-let debug_print s = () (*prerr_endline s;;*)
+let debug = true;;
+let debug_print s = 
+  if debug then prerr_endline (Lazy.force s);;
 
-(* {{{ *********** local given_clause wrapper ***********)
+(* functions for retrieving theorems *)
 
-let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
-  let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
-    match tables with
-    | None -> 
-        (* first time, do a huge saturation *)
-        let bag, equalities, cache, maxmeta = 
-          Saturation.find_equalities dbd status ?auto smart_flag cache
-        in
-        let passive = Saturation.make_passive equalities in
-        let active = Saturation.make_active [] in
-        let goal_steps, saturation_steps, timeout =
-          if flags.use_only_paramod then max_int,max_int,flags.timeout
-          else 82, 82, infinity
-        in
-        let maxm = max maxm maxmeta in
-        active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
-    | Some (active,passive,bag,oldcache) -> 
-        (* saturate a bit more if cache cahnged *)
-        let bag, equalities, cache, maxm = 
-          if cache_size oldcache <> cache_size cache then 
-            Saturation.saturate_more
-              bag active maxm status smart_flag ?auto cache
-          else
-            bag, [], cache, maxm
-        in
-        let minsteps = List.length equalities in
-        let passive = Saturation.add_to_passive equalities passive in
-        let goal_steps, saturation_steps, timeout =
-          if flags.use_only_paramod then max_int,max_int,flags.timeout
-          else max 50 minsteps, minsteps, infinity
-        in
-        active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
+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')     
+  | t -> ProofEngineReduction.unfold context t
+
+let find_library_theorems dbd proof goal = 
+  let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
+  let terms = List.map CicUtil.term_of_uri univ in
+  List.map 
+    (fun t -> 
+       (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph))) 
+    terms
+
+let find_context_theorems context metasenv =
+  let l,_ =
+    List.fold_left
+      (fun (res,i) ctxentry ->
+        match ctxentry with
+          | Some (_,Cic.Decl t) -> 
+               (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
+          | 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
+               in
+                (t,ty)::res,i+1
+          |  _ -> res,i+1)
+      ([],1) context
+  in l
+
+let rec is_an_equality = function
+  | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] 
+    when (LibraryObjects.is_eq_URI uri) -> true
+  | Cic.Prod (_, _, t) -> is_an_equality t
+  | _ -> false
+;;
+
+let partition_equalities =
+  List.partition (fun (_,ty) -> is_an_equality ty)
+
+
+let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;; 
+
+
+let is_unit_equation context metasenv oldnewmeta term = 
+  let head, metasenv, args, newmeta =
+    TermUtil.saturate_term oldnewmeta metasenv context term 0
   in
-  let res,actives,passives,maxmeta = 
-    Saturation.given_clause bag maxmeta status active passive 
-      goal_steps saturation_steps timeout
+  let propositional_args = 
+    HExtlib.filter_map
+      (function 
+      | Cic.Meta(i,_) -> 
+          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
+          in
+         if b then Some i else None 
+      | _ -> assert false)
+    args
   in
-  res,actives,passives,bag,cache,maxmeta
+    if propositional_args = [] then 
+      let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+       Some (args,metasenv,newmetas,head,newmeta)
+    else None
+;;
+
+let get_candidates universe cache t =
+  let candidates= 
+    (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
+  in 
+  let debug_msg =
+    (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^ 
+            (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
+  debug_print debug_msg;
+  candidates
+;;
+
+let only signature context t =
+  try
+    let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_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 not_default_eq_term t =
+  try
+    let uri = CicUtil.uri_of_term t in
+      not (LibraryObjects.in_eq_URIs uri)
+  with Invalid_argument _ -> true
+
+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
+    (* 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 build_equality bag head args proof newmetas maxmeta = 
+  match head with
+  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
+      let p =
+        if args = [] then proof else Cic.Appl (proof::args)
+      in 
+      let o = !Utils.compare_terms t1 t2 in
+      let stat = (ty,t1,t2,o) in
+      (* let w = compute_equality_weight stat in *)
+      let w = 0 in 
+      let proof = Equality.Exact p in
+      let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
+      (* to clean the local context of metas *)
+      Equality.fix_metas bag maxmeta e
+  | _ -> assert false
 ;;
 
-(* }}} ****************************************************************)
+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)
+    ([],[],newmeta) equations
+
+let empty_tables = 
+  (Saturation.make_active [], 
+   Saturation.make_passive [],
+   Equality.mk_equality_bag)
+
+let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
+  (* the local cache in initially empty  *)
+  let cache = AutoCache.cache_empty in
+  let _, metasenv, _, _, _ = 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
+  prerr_endline 
+    ("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)));
+  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)));
+  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
+  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 *)
+  let passive = Saturation.make_passive units in
+  let no = List.length units in
+  let active = Saturation.make_active [] in
+  let active,passive,newmeta = 
+    if paramod then active,passive,newmeta
+    else
+      Saturation.pump_actives 
+       context bag newmeta active passive (no+1) infinity
+  in 
+    (active,passive,bag),cache,newmeta
+
+let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast = 
+  let head, metasenv, args, newmeta =
+    TermUtil.saturate_term oldnewmeta metasenv context term 0
+  in
+  let propositional_args = 
+    HExtlib.filter_map
+      (function 
+      | Cic.Meta(i,_) -> 
+          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
+          in
+          if b then Some i else None 
+      | _ -> assert false)
+    args
+  in
+  let results,cache,newmeta = 
+    if propositional_args = [] then 
+      let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+      [args,metasenv,newmetas,head,newmeta],cache,newmeta
+    else
+      (*
+      let proof = 
+        None,metasenv,term,term (* term non e' significativo *)
+      in *)
+      let flags = 
+        if fast then
+          {AutoTypes.default_flags() with 
+           AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+           maxwidth = 2;maxdepth = 2;
+           use_paramod=true;use_only_paramod=false}
+        else
+          {AutoTypes.default_flags() with
+           AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+           maxwidth = 2;maxdepth = 4;
+           use_paramod=true;use_only_paramod=false} 
+      in
+      match auto newmeta tables universe cache context metasenv propositional_args flags with
+      | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
+      | substs,cache,newmeta ->
+          List.map 
+            (fun subst ->
+              let metasenv = 
+                CicMetaSubst.apply_subst_metasenv subst metasenv
+              in
+              let head = CicMetaSubst.apply_subst subst head in
+              let newmetas = 
+                List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv 
+              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)
+            substs, cache, newmeta
+  in
+  results,cache,newmeta
+
+let build_equalities auto context metasenv tables universe cache newmeta equations =
+  List.fold_left 
+    (fun (facts,cache,newmeta) (t,ty) ->
+       (* in any case we add the equation to the cache *)
+       let cache = AutoCache.cache_add_list cache context [(t,ty)] in
+       try
+         let saturated,cache,newmeta = 
+           fill_hypothesis context metasenv newmeta ty tables universe cache auto true
+         in
+         let (active,passive,bag) = tables in
+         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'
+                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)
+      )
+    ([],cache,newmeta) equations
+
+let close_more tables maxmeta context status auto universe cache =
+  let (active,passive,bag) = tables in
+  let proof, goalno = status in
+  let _, metasenv,_,_, _ = proof in  
+  let signature = MetadataQuery.signature_of metasenv goalno in
+  let equations = retrieve_equations signature universe cache context in
+  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 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);
+  List.iter
+    (fun e -> prerr_endline (Equality.string_of_equality e)) 
+    units;
+  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+  let passive = Saturation.add_to_passive units passive in
+  let no = List.length units in
+  prerr_endline ("No = " ^ (string_of_int no));
+  let active,passive,newmeta = 
+    Saturation.pump_actives context bag maxm active passive (no+1) infinity
+  in 
+    (active,passive,bag),cache,newmeta
+
+let find_context_equalities 
+  maxmeta bag context proof (universe:Universe.universe) cache 
+=
+  let module C = Cic in
+  let module S = CicSubstitution in
+  let module T = CicTypeChecker in
+  let _,metasenv,_,_, _ = proof in
+  let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
+  (* if use_auto is true, we try to close the hypothesis of equational
+    statements using auto; a naif, and probably wrong approach *)
+  let rec aux cache index newmeta = function
+    | [] -> [], newmeta,cache
+    | (Some (_, C.Decl (term)))::tl ->
+        debug_print
+          (lazy
+             (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
+        let do_find context term =
+          match term with
+          | C.Prod (name, s, t) when is_an_equality t ->
+              (try 
+                
+                let term = S.lift index term in
+                let saturated,cache,newmeta = 
+                  fill_hypothesis context metasenv newmeta term 
+                    empty_tables universe cache default_auto false
+                in
+                let eqs,newmeta = 
+                  List.fold_left 
+                   (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
+                     let newmeta, equality = 
+                       build_equality
+                         bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
+                     in
+                     equality::acc, newmeta + 1)
+                   ([],newmeta) saturated
+                in
+                 eqs, newmeta, cache
+              with FillingFailure (cache,newmeta) ->
+                [],newmeta,cache)
+          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+              when LibraryObjects.is_eq_URI uri ->
+              let term = S.lift index term in
+              let newmeta, e = 
+                build_equality bag term [] (Cic.Rel index) [] newmeta
+              in
+              [e], (newmeta+1),cache
+          | _ -> [], newmeta, cache
+        in 
+        let eqs, newmeta, cache = do_find context term in
+        let rest, newmeta,cache = aux cache (index+1) newmeta tl in
+        List.map (fun x -> index,x) eqs @ rest, newmeta, cache
+    | _::tl ->
+        aux cache (index+1) newmeta tl
+  in
+  let il, maxm, cache = 
+    aux cache 1 newmeta context 
+  in
+  let indexes, equalities = List.split il in
+  indexes, equalities, maxm, cache
+;;
 
-(* {{{ **************** applyS *******************)
+(***************** applyS *******************)
 
 let new_metasenv_and_unify_and_t 
-  dbd proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity 
+ dbd flags universe proof goal ?tables newmeta' metasenv' 
+ context term' ty termty goal_arity 
 =
  let (consthead,newmetasenv,arguments,_) =
-   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
+   TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
  let term'' = 
    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) 
  in
  let proof',oldmetasenv =
-  let (puri,metasenv,pbo,pty) = proof in
-   (puri,newmetasenv,pbo,pty),metasenv
+  let (puri,metasenv,pbo,pty, attrs) = proof in
+   (puri,newmetasenv,pbo,pty, attrs),metasenv
  in
  let goal_for_paramod =
   match LibraryObjects.eq_URI () with
@@ -94,13 +446,13 @@ let new_metasenv_and_unify_and_t
  in
  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
- let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
+ let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
  let proof''',goals =
   ProofEngineTypes.apply_tactic
     (EqualityTactics.rewrite_tac ~direction:`RightToLeft
       ~pattern:(ProofEngineTypes.conclusion_pattern None) 
-        (Cic.Meta(newmeta,irl)))
+        (Cic.Meta(newmeta,irl)) [])
    (proof'',goal)
  in
  let goal = match goals with [g] -> g | _ -> assert false in
@@ -108,18 +460,18 @@ let new_metasenv_and_unify_and_t
    PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) 
  in
  match 
-   let cache, flags = cache_empty, default_flags() in
-   let flags = 
-     {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} 
+   let (active, passive,bag), cache, maxmeta =
+     init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta)
    in
-   given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta) 
+     Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive 
+       max_int max_int flags.timeout
  with
- | None, active, passive, bag,_,_ -> 
+ | None, _,_,_ -> 
      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
- | Some (_,proof''''',_), active, passive,bag,_,_  ->
+ | Some (_,proof''''',_), active,passive,_  ->
      subst,proof''''',
      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
-       ~newmetasenv:(let _,m,_,_ = proof''''' in m),  active, passive
+       ~newmetasenv:(let _,m,_,_, _ = proof''''' in m),  active, passive
 ;;
 
 let rec count_prods context ty =
@@ -127,11 +479,11 @@ 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 ?tables (proof, goal) =
+let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let (_,metasenv,_,_) = proof in
+  let (_,metasenv,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = CicMkImplicit.new_meta metasenv subst in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
@@ -173,15 +525,13 @@ let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
    let goal_arity = count_prods context ty in
    let subst, proof, gl, active, passive =
-    new_metasenv_and_unify_and_t dbd proof goal ?tables
+    new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
      newmeta' metasenv' context term' ty termty goal_arity
    in
     subst, proof, gl, active, passive
 ;;
 
-(* }}} **************** applyS **************)
-
-(* {{{ ***************** AUTO ********************)
+(****************** AUTO ********************)
 
 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 let ugraph = CicUniv.empty_ugraph;;
@@ -192,28 +542,37 @@ let ppterm ctx t =
 ;;
 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 (Cic.Sort Cic.Prop) sort u)
+  fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
 ;;
+
 let assert_proof_is_valid proof metasenv context goalty =
-  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
+  if debug 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 ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
-    end;
-  assert b
+      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 = 
+              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
+    end
+  else ()
 ;;
+
 let assert_subst_are_disjoint subst subst' =
-  assert(List.for_all
-    (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') 
-    subst)
+  if debug then
+    assert(List.for_all
+            (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) 
 ;;
@@ -224,12 +583,16 @@ 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
-        fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
+        let b,_ = 
+         CicReduction.are_convertible 
+           ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
+       b
       with 
       | CicTypeChecker.AssertFailure s 
       | CicTypeChecker.TypeCheckerFailure s -> 
-          debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
-          debug_print (Lazy.force s);
+          debug_print 
+           (lazy (ppterm context (CicMetaSubst.apply_subst subst ty)));
+          debug_print s;
           false)
     (* FIXME... they should type! *)
     gl
@@ -254,12 +617,16 @@ let order_new_goals metasenv subst open_goals ppterm =
   in
   let tys = 
     List.map 
-      (fun (i,_) -> 
-        let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals 
+      (fun (i,sort) -> 
+        let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals 
   in
-  debug_print ("   OPEN: "^
-    String.concat " " 
-      (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
+  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)));
   open_goals
 ;;
 
@@ -269,76 +636,117 @@ let is_an_equational_goal = function
 ;;
 
 let equational_case 
-  dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context 
+  tables maxm cache depth fake_proof goalno goalty subst context 
     flags
 =
+  let active,passive,bag = tables in
   let ppterm = ppterm context in
-  prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
+  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
+      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
+        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 
+      end
+
 (*
-  prerr_endline "<CACHE>";
-  prerr_endline (cache_print context cache);
-  prerr_endline "</CACHE>";
-*)
-  match 
-    given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno) 
-  with
-  | None, active,passive, bag, cache, maxmeta -> 
-      let tables = Some (active,passive,bag,cache) in
-      None, tables, cache, maxmeta
-  | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
-      let tables = Some (active,passive,bag,cache) in
+  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-1,sort) open_goals in
-      Some [metasenv,subst,open_goals], tables, cache, maxmeta
+      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 
-  goalty dbd tables maxm subst fake_proof goalno depth context cand 
+  goalty tables maxm subst fake_proof goalno depth context cand 
 =
   let ppterm = ppterm context in
   try 
-    let subst', ((_,metasenv,_,_), open_goals), maxmeta =
+    let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
       PrimitiveTactics.apply_with_subst 
         ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) 
     in
-    debug_print ("   OK: " ^ ppterm cand);
-    assert (maxmeta >= maxm);
-    (*FIXME:sicuro che posso @?*)
-    assert_subst_are_disjoint subst subst';
-    let subst = subst@subst' 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
-  with ProofEngineTypes.Fail s -> 
+  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
 ;;
 
 let applicative_case 
-  dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
+  tables maxm depth subst fake_proof goalno goalty metasenv context universe
+  cache
 = 
-  let candidates = get_candidates cache goalty in
+  let candidates = get_candidates universe cache goalty in
   let tables, elems, maxm = 
     List.fold_left 
       (fun (tables,elems,maxm) cand ->
         match 
           try_candidate goalty
-            dbd tables maxm subst fake_proof goalno depth context cand
+            tables maxm subst fake_proof goalno depth context cand
         with
         | None, tables,maxm  -> tables,elems, maxm 
         | Some x, tables, maxm -> tables,x::elems, maxm)
       (tables,[],maxm) candidates
   in
   let elems = sort_new_elems elems in
-  elems, tables, cache, maxm
+  elems, tables, cache, maxm 
 ;;
 
 (* Works if there is no dependency over proofs *)
 let is_a_green_cut goalty =
   CicUtil.is_meta_closed goalty
 ;;
-let prop = function (_,_,P) -> true | _ -> false;;
+
+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})
@@ -362,76 +770,65 @@ let cache_add_success sort cache k v =
   cache k
 ;;
 
-let rec auto_main dbd tables maxm context flags elems cache =
-  let callback_for_paramod maxm flags proof commonctx cache l = 
-    let flags = {flags with use_paramod = false;dont_cache_failures=true} in
-    let _,metasenv,_,_ = proof in
-    let oldmetasenv = metasenv in
-    match
-      auto_all_solutions
-        dbd tables maxm cache commonctx metasenv l flags
-    with
-    | [],cache,maxm -> [],cache,maxm
-    | solutions,cache,maxm -> 
-        let solutions = 
-          HExtlib.filter_map
-            (fun (subst,newmetasenv) ->
-              let opened = 
-                ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
-              in
-              if opened = [] then Some subst else None)
-            solutions
-        in
-         solutions,cache,maxm
-  in
+let rec auto_main tables maxm context flags elems universe cache =
   let flags = calculate_timeout flags in
   let ppterm = ppterm context in
   let irl = mk_irl context in
-  let rec aux tables maxm cache = function (* elems in OR *)
+  let rec aux flags tables maxm cache = function (* 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 
       List.length (List.filter prop goals) > flags.maxwidth -> 
-        debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
-        aux tables maxm cache tl (* FAILURE (width) *)
+        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 -> 
         if Unix.gettimeofday() > flags.timeout then 
           Fail "timeout",tables,cache,maxm 
         else
         try
           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
-          debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
-          if sort = T && tl <> [] then (* FIXME!!!! *)
-            (debug_print (" FAILURE(not in prop)");
-            aux tables maxm cache tl (* FAILURE (not in prop) *))
+          debug_print 
+           (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^
+                   "with depth"^string_of_int depth));
+          debug_print (lazy (AutoCache.cache_print context cache));
+          if sort = T (* && tl <> []*)  then 
+          aux flags tables maxm cache ((metasenv,subst,gl)::tl)
+         (* Success (metasenv,subst,tl), tables, cache,maxm *)
+          (*
+            (debug_print 
+              (lazy (" FAILURE(not in prop)"));
+            aux flags tables maxm cache tl (* FAILURE (not in prop) *)) *)
           else
-          match aux_single tables maxm cache metasenv subst elem goalty cc with
+          match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
           | Fail s, tables, cache, maxm' -> 
-              assert(maxm' >= maxm);let maxm = maxm' in
+              let maxm = maxm' in
               debug_print
-                (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
+                (lazy 
+                  (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
               let cache = 
                 if flags.dont_cache_failures then 
                   cache_remove_underinspection cache goalty
                 else cache_add_failure cache goalty depth 
               in
-              aux tables maxm cache tl
+              aux flags tables maxm cache tl
           | Success (metasenv,subst,others), tables, cache, maxm' ->
-              assert(maxm' >= maxm);let maxm = maxm' in
+              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 ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
+                debug_print 
+                 (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
                 if is_a_green_cut goalty then
-                  (assert_proof_is_valid proof metasenv context goalty;
+                  (* assert_proof_is_valid proof metasenv context goalty; *)
                   let cache = cache_add_success sort cache goalty proof in
-                  aux tables maxm cache ((metasenv,subst,gl)::tl))
+                  aux flags tables maxm cache ((metasenv,subst,gl)::tl)
                 else
                   (let goalty = CicMetaSubst.apply_subst subst goalty in
-                  assert_proof_is_valid proof metasenv context goalty;
+                 (* assert_proof_is_valid proof metasenv context goalty; *)
                   let cache = 
                     if is_a_green_cut goalty then
                       cache_add_success sort cache goalty proof
@@ -443,14 +840,17 @@ let rec auto_main dbd tables maxm context flags elems cache =
                       (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl)) 
                     others
                   in 
-                  aux tables maxm cache ((metasenv,subst,gl)::others@tl))
+                  aux flags tables maxm cache ((metasenv,subst,gl)::others@tl))
               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 ("Goal "^string_of_int goalno^" closed by sideeffect");
-          aux tables maxm cache ((metasenv,subst,gl)::tl)
-  and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
+          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 =
+    (* 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 *)
       (* FAILURE (euristic cut) *)
@@ -459,47 +859,53 @@ let rec auto_main dbd tables maxm context flags elems cache =
         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
         tables,cache,maxm(*FAILURE(depth)*)
     | Succeded t -> 
-        assert(List.for_all (fun (i,_) -> i <> goalno) subst);
         let entry = goalno, (cc, t,goalty) in
         assert_subst_are_disjoint subst [entry];
         let subst = entry :: subst in
         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-        debug_print ("  CACHE HIT!");
+        debug_print (lazy ("  CACHE HIT!"));
         Success (metasenv, subst, []), tables, cache, maxm
-    | UnderInspection -> Fail "looping",tables,cache, maxm
+    | UnderInspection -> 
+       (* 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
-        let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
-        let elems, tables, cache, maxm =
+        let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
+        let elems, tables, cache, maxm, flags =
           if is_equational_case goalty flags then
-            match 
-              equational_case dbd tables maxm
-                ~auto:callback_for_paramod cache
-                depth fake_proof goalno goalty subst context flags 
-            with
-            | Some elems, tables, cache, maxm -> 
-                elems, tables, cache, maxm 
-            | None, tables,cache,maxm -> 
-                applicative_case dbd tables maxm depth subst fake_proof goalno 
-                  goalty metasenv context 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            
           else
-            applicative_case dbd tables maxm depth subst fake_proof goalno 
-              goalty metasenv context cache
+           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  
         in
-        aux tables maxm cache elems
-    | _ -> Fail "??",tables,cache,maxm 
+        aux flags tables maxm cache elems
+    | _ -> Fail "depth = 0",tables,cache,maxm 
   in
-    aux tables maxm cache elems
+    aux flags tables maxm cache elems
 
 and
-  auto_all_solutions dbd tables maxm cache context metasenv gl flags 
+  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 rec aux tables maxm solutions cache elems flags =
-    match auto_main dbd tables maxm context flags elems cache with
+    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 -> 
         if Unix.gettimeofday () > flags.timeout then
@@ -508,39 +914,334 @@ and
           aux tables maxm ((subst,metasenv)::solutions) cache others flags
   in
   let rc = aux tables maxm [] cache elems flags in
-  prerr_endline "fine auto all solutions";
-  rc
+    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
 ;;
 
 (* }}} ****************** AUTO ***************)
 
-let auto_all_solutions dbd cache context metasenv gl flags =
+let auto_all tables universe cache context metasenv gl flags =
   let solutions, cache, _ = 
-    auto_all_solutions dbd None 0 cache context metasenv gl flags
+    auto_all_solutions 0 tables universe cache context metasenv gl flags
   in
   solutions, cache
 ;;
 
-let auto dbd cache context metasenv gl flags =
+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 dbd None 0 context flags elems cache with
+  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));
       Some (subst,metasenv), cache
   | Fail s,tables,cache,maxm -> None,cache
 ;;
 
-let applyS_tac ~dbd ~term =
+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 timeout = int "timeout" 0 in
+  { AutoTypes.maxdepth = 
+      if use_only_paramod then 2 else depth;
+    AutoTypes.maxwidth = width;
+    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;
+  }
+
+let applyS_tac ~dbd ~term ~params ~universe =
  ProofEngineTypes.mk_tactic
   (fun status ->
     try 
-      let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in 
-      proof, gl
+      let _, proof, gl,_,_ =
+       apply_smart ~dbd ~term ~subst:[] ~universe
+        (flags_of_params params ~for_applyS:true ()) status
+      in 
+       proof, gl
     with 
     | CicUnification.UnificationFailure msg
     | 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,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
+  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): ");
+  List.iter 
+    (fun e -> 
+      let t = Equality.term_of_equality eq_uri e in
+      prerr_endline (CicPp.pp t names)) 
+  eql;
+  prerr_endline ("\n result proofs: ");
+  List.iter (fun e -> 
+    prerr_endline (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
+      prerr_endline ("\n result [demod]: ");
+      List.iter 
+        (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
+      prerr_endline ("\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)) 
+      eql;
+    end;
+  proof,[goalno]
+;;
+
+let auto_tac ~(dbd:HMysql.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,_,_, _ = proof in
+      let _,context,_ = 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,_,_, _) = 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 = 
+            ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+              proof goal (CicMetaSubst.apply_subst subst) metasenv
+            in
+            let opened = 
+              ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+               ~newmetasenv:metasenv
+            in
+              proof,opened
+       | Fail s,tables,cache,maxm -> 
+           raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+;;
+
+let auto_tac ~dbd ~params ~universe = 
+  ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
+
+let eq_of_goal = function
+  | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
+      uri
+  | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
+(* DEMODULATE *)
+let demodulate_tac ~dbd ~universe (proof,goal)= 
+  let curi,metasenv,pbo,pty, attrs = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+  let initgoal = [], [], 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
+  let equalities = (Saturation.list_of_passive passive) in
+  (* we demodulate using both actives passives *)
+  let table = 
+    List.fold_left 
+      (fun tbl eq -> Indexing.index tbl eq) 
+      (snd active) equalities
+  in
+  let changed,(newproof,newmetasenv, newty) = 
+    Indexing.demodulation_goal bag
+      (metasenv,context,CicUniv.empty_ugraph) table initgoal 
+  in
+  if changed then
+    begin
+      let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
+      let proofterm,_ = 
+        Equality.build_goal_proof bag
+          eq_uri newproof opengoal ty [] context metasenv
+      in
+        let extended_metasenv = (maxm,context,newty)::metasenv in
+        let extended_status = 
+          (curi,extended_metasenv,pbo,pty, attrs),goal in
+        let (status,newgoals) = 
+          ProofEngineTypes.apply_tactic 
+            (PrimitiveTactics.apply_tac ~term:proofterm)
+            extended_status in
+        (status,maxm::newgoals)
+    end
+  else (* if newty = ty then *)
+    raise (ProofEngineTypes.Fail (lazy "no progress"))
+  (*else ProofEngineTypes.apply_tactic 
+    (ReductionTactics.simpl_tac
+      ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
+;;
+
+let demodulate_tac ~dbd ~universe = 
+  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
+
+
+