]> matita.cs.unibo.it Git - helm.git/commitdiff
auto snapshot
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 27 Sep 2006 16:20:40 +0000 (16:20 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 27 Sep 2006 16:20:40 +0000 (16:20 +0000)
22 files changed:
helm/software/components/cic/discrimination_tree.ml
helm/software/components/tactics/.depend
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/autoTactic.ml
helm/software/components/tactics/autoTactic.mli
helm/software/components/tactics/autoTypes.ml
helm/software/components/tactics/autoTypes.mli
helm/software/components/tactics/metadataQuery.ml
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/paramodulation/equality.mli
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/indexing.mli
helm/software/components/tactics/paramodulation/inference.ml
helm/software/components/tactics/paramodulation/inference.mli
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/saturation.mli
helm/software/components/tactics/paramodulation/utils.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/primitiveTactics.mli
helm/software/components/tactics/tactics.ml
helm/software/components/tactics/tactics.mli

index 33ecea7cecabc2c6bbf93bb0732bd93f8cf91c79..9d691484701477b94554a3d72b4853741ec739f5 100644 (file)
@@ -242,6 +242,10 @@ let remove_index tree equality =
         | term -> term
       ;;
 
+      let rec skip_prods = function
+        | Cic.Prod (_,_,t) -> skip_prods t
+        | term -> term
+      ;;
 
       let rec subterm_at_pos pos term =
         match pos with
@@ -287,6 +291,7 @@ let remove_index tree equality =
       ;;     
 
       let retrieve_generalizations (tree,arity) term =
+        let term = skip_prods term in
         let rec retrieve tree term pos =
           match tree with
             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
@@ -347,6 +352,7 @@ let remove_index tree equality =
 
 
       let retrieve_unifiables (tree,arities) term =
+        let term = skip_prods term in
         let rec retrieve tree term pos =
           match tree with
             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
index 380c50f5184f2680c138e2abf7f38512254ad74e..04154280be6e3ef3316ae7b0620c50c62c1cdc2b 100644 (file)
@@ -8,15 +8,15 @@ metadataQuery.cmi: proofEngineTypes.cmi
 autoTypes.cmi: proofEngineTypes.cmi 
 paramodulation/equality.cmi: paramodulation/utils.cmi \
     paramodulation/subst.cmi 
-paramodulation/inference.cmi: paramodulation/utils.cmi \
-    paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/equality.cmi \
-    autoTypes.cmi 
+paramodulation/inference.cmi: paramodulation/subst.cmi proofEngineTypes.cmi \
+    paramodulation/equality.cmi autoTypes.cmi 
 paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \
     paramodulation/equality.cmi 
 paramodulation/indexing.cmi: paramodulation/utils.cmi \
     paramodulation/subst.cmi paramodulation/equality_indexing.cmi \
     paramodulation/equality.cmi 
-paramodulation/saturation.cmi: proofEngineTypes.cmi autoTypes.cmi 
+paramodulation/saturation.cmi: proofEngineTypes.cmi \
+    paramodulation/inference.cmi paramodulation/equality.cmi autoTypes.cmi 
 variousTactics.cmi: proofEngineTypes.cmi 
 introductionTactics.cmi: proofEngineTypes.cmi 
 eliminationTactics.cmi: proofEngineTypes.cmi 
@@ -63,8 +63,8 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     hashtbl_equiv.cmi metadataQuery.cmi 
 metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     hashtbl_equiv.cmx metadataQuery.cmi 
-autoTypes.cmo: metadataQuery.cmi paramodulation/equality.cmi autoTypes.cmi 
-autoTypes.cmx: metadataQuery.cmx paramodulation/equality.cmx autoTypes.cmi 
+autoTypes.cmo: metadataQuery.cmi autoTypes.cmi 
+autoTypes.cmx: metadataQuery.cmx autoTypes.cmi 
 paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi 
 paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi 
 paramodulation/subst.cmo: paramodulation/subst.cmi 
@@ -98,12 +98,12 @@ paramodulation/indexing.cmx: paramodulation/utils.cmx \
 paramodulation/saturation.cmo: paramodulation/utils.cmi \
     paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
     proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \
-    paramodulation/indexing.cmi paramodulation/equality.cmi \
+    paramodulation/indexing.cmi paramodulation/equality.cmi autoTypes.cmi \
     paramodulation/saturation.cmi 
 paramodulation/saturation.cmx: paramodulation/utils.cmx \
     paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/inference.cmx \
-    paramodulation/indexing.cmx paramodulation/equality.cmx \
+    paramodulation/indexing.cmx paramodulation/equality.cmx autoTypes.cmx \
     paramodulation/saturation.cmi 
 variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
@@ -133,22 +133,26 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
     proofEngineStructuralRules.cmx proofEngineReduction.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
     equalityTactics.cmi 
-auto.cmo: proofEngineTypes.cmi primitiveTactics.cmi autoTypes.cmi auto.cmi 
-auto.cmx: proofEngineTypes.cmx primitiveTactics.cmx autoTypes.cmx auto.cmi 
-autoTactic.cmo: tacticals.cmi paramodulation/saturation.cmi \
-    proofEngineTypes.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
-    metadataQuery.cmi equalityTactics.cmi paramodulation/equality.cmi \
-    autoTypes.cmi auto.cmi autoTactic.cmi 
-autoTactic.cmx: tacticals.cmx paramodulation/saturation.cmx \
-    proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
-    metadataQuery.cmx equalityTactics.cmx paramodulation/equality.cmx \
-    autoTypes.cmx auto.cmx autoTactic.cmi 
+auto.cmo: tacticals.cmi paramodulation/saturation.cmi proofEngineTypes.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \
+    autoTypes.cmi auto.cmi 
+auto.cmx: tacticals.cmx paramodulation/saturation.cmx proofEngineTypes.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \
+    autoTypes.cmx auto.cmi 
+autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \
+    paramodulation/equality.cmi autoTypes.cmi auto.cmi autoTactic.cmi 
+autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \
+    paramodulation/equality.cmx autoTypes.cmx auto.cmx autoTactic.cmi 
 discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
-    proofEngineTypes.cmi primitiveTactics.cmi introductionTactics.cmi \
-    equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi 
+    proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
+    introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \
+    discriminationTactics.cmi 
 discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
-    proofEngineTypes.cmx primitiveTactics.cmx introductionTactics.cmx \
-    equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi 
+    proofEngineTypes.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
+    introductionTactics.cmx equalityTactics.cmx eliminationTactics.cmx \
+    discriminationTactics.cmi 
 inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     equalityTactics.cmi inversion.cmi 
@@ -192,13 +196,13 @@ tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi \
     proofEngineStructuralRules.cmi primitiveTactics.cmi negationTactics.cmi \
     inversion.cmi introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \
     equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \
-    autoTactic.cmi tactics.cmi 
+    autoTactic.cmi auto.cmi tactics.cmi 
 tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx \
     paramodulation/saturation.cmx ring.cmx reductionTactics.cmx \
     proofEngineStructuralRules.cmx primitiveTactics.cmx negationTactics.cmx \
     inversion.cmx introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
-    autoTactic.cmx tactics.cmi 
+    autoTactic.cmx auto.cmx tactics.cmi 
 declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
 declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
index e377b63683049ae55d0fd30ea6a355d90fe0a01c..6b1bf82abd7598cbef245ee740fac09e26243d6b 100644 (file)
 
 open AutoTypes;;
 
-let debug_print s = ();;(*prerr_endline s;;*)
+let debug_print s = () (* prerr_endline s;; *)
+
+let given_clause dbd ?tables maxm ?auto cache subst flags status =
+  prerr_endline ("given_clause " ^ string_of_int maxm);
+  let active, passive, bag, cache, maxmeta, goal_steps, saturation_steps, timeout = 
+    match tables with
+    | None -> 
+        let bag, equalities, cache, maxmeta = 
+          Saturation.find_equalities dbd status ?auto true 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) -> 
+        let bag, equalities, cache, maxm = 
+          if cache_size oldcache <> cache_size cache then 
+            Saturation.saturate_more bag active maxm status true ?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 30 minsteps, minsteps, infinity
+        in
+        active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
+  in
+  let res,a,p, maxmeta = 
+    Saturation.given_clause bag maxmeta status active passive 
+      goal_steps saturation_steps timeout
+  in
+  res,a,p,bag,cache,maxmeta
+;;
+
+(* {{{ **************** applyS *******************)
+
+let new_metasenv_and_unify_and_t 
+  dbd 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
+ 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
+ in
+ let goal_for_paramod =
+  match LibraryObjects.eq_URI () with
+  | Some uri -> 
+      Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
+  | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
+ 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 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)))
+   (proof'',goal)
+ in
+ let goal = match goals with [g] -> g | _ -> assert false in
+ let subst, (proof'''', _), _ =
+   PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) 
+ in
+ match 
+   let cache, flags = AutoTypes.cache_empty, AutoTypes.default_flags() in
+   let flags = 
+     {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} 
+   in
+   given_clause dbd ?tables 0 cache [] flags (proof'''',newmeta) 
+ with
+ | None, active, passive, bag,_,_ -> 
+     raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
+ | Some (_,proof''''',_), active, passive,bag,_,_  ->
+     subst,proof''''',
+     ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+       ~newmetasenv:(let _,m,_,_ = proof''''' in m),  active, passive
+;;
+
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+    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 module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic 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' =
+    match term with
+       C.Var (uri,exp_named_subst) ->
+        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+          exp_named_subst
+        in
+         exp_named_subst_diff,newmeta',newmetasenvfragment,
+          C.Var (uri,exp_named_subst')
+     | C.Const (uri,exp_named_subst) ->
+        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+          exp_named_subst
+        in
+         exp_named_subst_diff,newmeta',newmetasenvfragment,
+          C.Const (uri,exp_named_subst')
+     | C.MutInd (uri,tyno,exp_named_subst) ->
+        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+          exp_named_subst
+        in
+         exp_named_subst_diff,newmeta',newmetasenvfragment,
+          C.MutInd (uri,tyno,exp_named_subst')
+     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+          exp_named_subst
+        in
+         exp_named_subst_diff,newmeta',newmetasenvfragment,
+          C.MutConstruct (uri,tyno,consno,exp_named_subst')
+     | _ -> [],newmeta,[],term
+   in
+   let metasenv' = metasenv@newmetasenvfragment in
+   let termty,_ = 
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+   in
+   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
+     newmeta' metasenv' context term' ty termty goal_arity
+   in
+    subst, proof, gl, active, passive
+;;
+
+(* }}} **************** applyS **************)
+
+(* {{{ ***************** AUTO ********************)
 
 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 let ugraph = CicUniv.empty_ugraph;;
@@ -43,9 +192,13 @@ let assert_proof_is_valid proof metasenv context goalty =
   let b,_ = CicReduction.are_convertible context ty goalty u in
   if not b then
     begin
-      prerr_endline (CicPp.ppterm proof);
-      prerr_endline (CicPp.ppterm ty);
-      prerr_endline (CicPp.ppterm goalty);
+      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
 ;;
@@ -103,21 +256,73 @@ let order_new_goals metasenv subst open_goals ppterm =
   open_goals
 ;;
 
-let try_candidate subst fake_proof goalno depth context cand =
+let is_an_equational_goal = function
+  | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
+  | _ -> false
+;;
+
+let equational_case 
+  dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context 
+    flags
+=
+  let ppterm = ppterm context in
+  prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
+  prerr_endline "<CACHE>";
+  prerr_endline (cache_print context cache);
+  prerr_endline "</CACHE>";
+  match 
+    given_clause dbd ?tables maxm ?auto cache subst flags (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
+      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 try_candidate 
+  goalty dbd tables maxm subst fake_proof goalno depth context cand 
+=
   let ppterm = ppterm context in
   try 
-    debug_print ("   PROVO: " ^ ppterm cand);
-    let subst', ((_,metasenv,_,_), open_goals) =
-      PrimitiveTactics.apply_with_subst ~term:cand ~subst (fake_proof,goalno) 
+    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
     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) 
-  with ProofEngineTypes.Fail s -> (*debug_print("   KO: "^Lazy.force s);*)None
+    Some (metasenv,subst,open_goals), tables , maxmeta
+  with ProofEngineTypes.Fail s -> 
+    (*debug_print("   KO: "^Lazy.force s);*)None,tables, maxm
+;;
+
+let applicative_case 
+  dbd tables maxm depth subst fake_proof goalno goalty metasenv context universe
+= 
+  let candidates = get_candidates universe 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
+        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, maxm
 ;;
 
 (* Works if there is no dependency over proofs *)
@@ -125,40 +330,79 @@ let is_a_green_cut goalty =
   CicUtil.is_meta_closed goalty
 ;;
 let prop = function (_,_,P) -> true | _ -> false;;
-
-let auto_main context flags elems cache universe =
-  let timeout = 
+let calculate_timeout flags = 
     if flags.timeout = 0. then 
-      infinity 
+      (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
     else 
-      Unix.gettimeofday () +. flags.timeout 
+      flags 
+;;
+let is_equational_case goalty flags =
+  let ensure_equational t = 
+    if is_an_equational_goal t then true 
+    else 
+      let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
+      raise (ProofEngineTypes.Fail (lazy msg))
   in
+  (flags.use_paramod && is_an_equational_goal goalty) || 
+  (flags.use_only_paramod && ensure_equational goalty)
+;;
+let cache_add_success sort cache k v =
+  if sort = P then cache_add_success cache k v else cache
+;;
+
+let rec auto_main dbd tables maxm context flags elems cache universe =
+  let callback_for_paramod maxm flags proof commonctx cache l = 
+    let flags = {flags with use_paramod = false} in
+    let _,metasenv,_,_ = proof in
+    let oldmetasenv = metasenv in
+    match
+      auto_all_solutions
+        dbd tables maxm universe 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 flags = calculate_timeout flags in
   let ppterm = ppterm context in
   let irl = mk_irl context in
-  let rec aux cache = function (* elems in OR *)
-    | [] -> Fail "no more steps can be done", cache (* COMPLETE FAILURE *)
+  let rec aux 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), cache (* solution::cont *)
+        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 cache tl (* FAILURE (width) *)
+        aux tables maxm cache tl (* FAILURE (width) *)
     | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl -> 
-        if Unix.gettimeofday() > timeout then Fail "timeout",cache 
+        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 then
+          if sort = T && tl <> [] then (* FIXME!!!! *)
             (debug_print (" FAILURE(not in prop)");
-            aux cache tl (* FAILURE (not in prop) *))
+            aux tables maxm cache tl (* FAILURE (not in prop) *))
           else
-          match aux_single cache metasenv subst elem goalty cc with
-          | Fail _, cache -> 
+          match aux_single tables maxm cache metasenv subst elem goalty cc with
+          | Fail _, tables, cache, maxm' -> 
+              assert(maxm' >= maxm);let maxm = maxm' in
               debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
               let cache = cache_add_failure cache goalty depth in
-              aux cache tl
-          | Success (metasenv,subst,others), cache ->
+              aux tables maxm cache tl
+          | Success (metasenv,subst,others), tables, cache, maxm' ->
+              assert(maxm' >= maxm);let maxm = maxm' in
               (* others are alternatives in OR *)
               try
                 let goal = Cic.Meta(goalno,irl) in
@@ -166,14 +410,14 @@ let auto_main context flags elems cache universe =
                 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
                 if is_a_green_cut goalty then
                   (assert_proof_is_valid proof metasenv context goalty;
-                  let cache = cache_add_success cache goalty proof in
-                  aux cache ((metasenv,subst,gl)::tl))
+                  let cache = cache_add_success sort cache goalty proof in
+                  aux tables maxm cache ((metasenv,subst,gl)::tl))
                 else
                   (let goalty = CicMetaSubst.apply_subst subst goalty in
                   assert_proof_is_valid proof metasenv context goalty;
                   let cache = 
                     if is_a_green_cut goalty then
-                      cache_add_success cache goalty proof
+                      cache_add_success sort cache goalty proof
                     else
                       cache
                   in
@@ -182,18 +426,20 @@ let auto_main context flags elems cache universe =
                       (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl)) 
                     others
                   in 
-                  aux cache ((metasenv,subst,gl)::others@tl))
+                  aux 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 *)
-          aux cache ((metasenv,subst,gl)::tl)
-  and aux_single cache metasenv subst (goalno, depth, _) goalty cc =
+          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 =
     let goalty = CicMetaSubst.apply_subst subst goalty in
 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
       (* FAILURE (euristic cut) *)
     match cache_examine cache goalty with
-    | Failed_in d when d >= depth -> Fail "depth",cache(*FAILURE(depth)*)
+    | Failed_in d when d >= depth -> 
+        Fail "depth",tables,cache,maxm(*FAILURE(depth)*)
     | Succeded t -> 
         assert(List.for_all (fun (i,_) -> i <> goalno) subst);
         let entry = goalno, (cc, t,goalty) in
@@ -201,49 +447,88 @@ let auto_main context flags elems cache universe =
         let subst = entry :: subst in
         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
         debug_print ("  CACHE HIT!");
-        Success (metasenv, subst, []),cache
-    | UnderInspection -> Fail "looping",cache
+        Success (metasenv, subst, []), tables, cache, maxm
+    | UnderInspection -> 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 candidates = get_candidates universe goalty in
         let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
-        let elems = 
-          HExtlib.filter_map
-            (try_candidate subst fake_proof goalno depth context)
-            candidates
+        let elems, tables, cache, maxm =
+          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 (* manca cache *)
+            | None, tables,cache,maxm -> 
+                let elems, tables, maxm =
+                applicative_case dbd tables maxm depth subst fake_proof goalno 
+                  goalty metasenv context universe 
+                in elems, tables, cache, maxm
+          else
+            let elems, tables, maxm =
+            applicative_case dbd tables maxm depth subst fake_proof goalno 
+              goalty metasenv context universe
+            in elems, tables, cache, maxm
         in
-        let elems = sort_new_elems elems in
-        aux cache elems
-    | _ -> Fail "??",cache 
+        aux tables maxm cache elems
+    | _ -> Fail "??",tables,cache,maxm 
   in
-    aux cache elems
-;;
-    
-let auto universe cache context metasenv gl flags =
+    aux tables maxm cache elems
+
+and
+  auto_all_solutions dbd tables maxm 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
-  match auto_main context flags elems cache universe with
-  | Fail s,cache -> prerr_endline s;None,cache
-  | Success (metasenv,subst,_), cache -> Some (subst,metasenv), cache
+  let rec aux tables maxm solutions cache elems flags =
+    match auto_main dbd tables maxm context flags elems cache universe 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
+          ((subst,metasenv)::solutions), cache, maxm
+        else
+          aux tables maxm ((subst,metasenv)::solutions) cache others flags
+  in
+  let rc = aux tables maxm [] cache elems flags in
+  prerr_endline "fine auto all solutions";
+  rc
 ;;
 
-let auto_all_solutions universe cache context metasenv gl flags =
+(* }}} ****************** AUTO ***************)
+
+let auto_all_solutions dbd universe cache context metasenv gl flags =
+  let solutions, cache, _ = 
+    auto_all_solutions dbd None 0 universe cache context metasenv gl flags
+  in
+  solutions, cache
+;;
+
+let auto dbd 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 bigbang = Unix.gettimeofday () in
-  let rec aux solutions cache elems flags =
-    match auto_main context flags elems cache universe with
-    | Fail s,cache ->prerr_endline s; solutions,cache
-    | Success (metasenv,subst,others), cache -> 
-        let elapsed = Unix.gettimeofday () -. bigbang in
-        if elapsed > flags.timeout then
-          ((subst,metasenv)::solutions), cache
-        else
-          aux ((subst,metasenv)::solutions) cache others 
-            {flags with timeout = flags.timeout -. elapsed}
-  in
-  aux [] cache elems flags
+  match auto_main dbd None 0 context flags elems cache universe with
+  | Success (metasenv,subst,_), tables,cache,_ -> Some (subst,metasenv), cache
+  | Fail s,tables,cache,maxm ->
+      let cache = cache_clean cache in
+      match auto_main dbd tables maxm context flags elems cache universe with
+      | Success (metasenv,subst,_), tables,cache,_ -> 
+          Some (subst,metasenv), cache
+      | Fail s,tables,cache,maxm -> prerr_endline s;None,cache
 ;;
+
+let applyS_tac ~dbd ~term =
+ ProofEngineTypes.mk_tactic
+  (fun status ->
+    try 
+      let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in 
+      proof, gl
+    with 
+    | CicUnification.UnificationFailure msg
+    | CicTypeChecker.TypeCheckerFailure msg ->
+        raise (ProofEngineTypes.Fail msg))
+
index 7150a124687af4e7e72da23a5c4a3cdd0eb7a61f..68057fa9c348021580cc0a5654c94117fd205996 100644 (file)
@@ -25,6 +25,7 @@
 
 (* stops at the first solution *)
 val auto: 
+  HMysql.dbd ->
   AutoTypes.universe ->
   AutoTypes.cache ->
   Cic.context ->
@@ -34,6 +35,7 @@ val auto:
     (Cic.substitution * Cic.metasenv) option * AutoTypes.cache
 
 val auto_all_solutions: 
+  HMysql.dbd ->
   AutoTypes.universe ->
   AutoTypes.cache ->
   Cic.context ->
@@ -41,3 +43,6 @@ val auto_all_solutions:
   ProofEngineTypes.goal list ->
   AutoTypes.flags ->
     (Cic.substitution * Cic.metasenv) list * AutoTypes.cache
+
+val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
+
index 61d078c22140dce589be39211b1bc0289e48ed4c..03fdf9555ea00048d4bb4ef9c4784163d40094b8 100644 (file)
@@ -266,123 +266,46 @@ and auto_new_aux dbd width already_seen_goals universe = function
         | _ -> assert false
  ;; 
 
-let default_depth = 5
-let default_width = 3
-
-(*
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
-  ()
-=
-  let auto_tac dbd (proof,goal) =
-  let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in
-  Hashtbl.clear inspected_goals;
-  debug_print (lazy "Entro in Auto");
-  let id t = t in
-  let t1 = Unix.gettimeofday () in
-  match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with
-      [] ->  debug_print (lazy "Auto failed");
-        raise (ProofEngineTypes.Fail "No Applicable theorem")
-    | (_,(proof,[],_))::_ ->
-        let t2 = Unix.gettimeofday () in
-        debug_print (lazy "AUTO_TAC HA FINITO");
-        let _,_,p,_ = proof in
-        debug_print (lazy (CicPp.ppterm p));
-        Printf.printf "tempo: %.9f\n" (t2 -. t1);
-        (proof,[])
-    | _ -> assert false
-  in
-  ProofEngineTypes.mk_tactic (auto_tac dbd)
-;;
-*)
-
-(*
-let paramodulation_tactic = ref
-  (fun dbd ?full ?depth ?width status ->
-     raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
-
-let term_is_equality = ref
-  (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
-*)
-
-let bool name params =
-    try let _ = List.assoc name params in true with
-    | Not_found -> false
+let bool params name default =
+    try 
+      let s = List.assoc name params in 
+      if s = "" || s = "1" || s = "true" || s = "yes" then true
+      else if s = "0" || s = "false" || s = "no" then false
+      else 
+        let msg = "Unrecognized value for parameter "^name^"\n" in
+        let msg = msg ^ "Accepted values are 1,true,yes and 0,false,no" in
+        raise (ProofEngineTypes.Fail (lazy msg))
+    with Not_found -> default
 ;; 
 
-let string name params =
+let string params name default =
     try List.assoc name params with
-    | Not_found -> ""
+    | Not_found -> default
 ;; 
 
-let int name default params =
+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 callback_for_paramodulation dbd width depth t l =
-  let _,y,x,xx = t in 
-  let universe = MetadataQuery.universe_of_goals ~dbd t l in
-  let todo = List.map (fun g -> (g, depth)) l in
-  prerr_endline ("AUTO: " ^ CicPp.ppterm x ^ " : " ^ CicPp.ppterm xx);
-  prerr_endline ("MENV: " ^ CicMetaSubst.ppmetasenv [] y);
-  match auto_new dbd width [] universe [(fun x -> x), (t, todo, None)] with
-  | (_,(proof,[],_))::_ -> proof
-  | _ -> raise (Failure "xxx")
-;;
-*)
-
-let callback_for_paramodulation dbd flags proof commonctx ?universe cache l =
-  let _,metasenv,_,_ = proof in
-  let oldmetasenv = metasenv in
-  let universe = 
-    match universe with
-    | Some u -> u 
-    | None -> 
-      let universe = 
-        AutoTypes.universe_of_goals dbd proof l AutoTypes.empty_universe 
-      in
-      AutoTypes.universe_of_context commonctx metasenv universe 
-  in
-  match
-    Auto.auto_all_solutions universe cache commonctx metasenv l flags
-  with
-  | [],cache -> [],cache,universe
-  | solutions,cache -> 
-      let solutions = 
-        HExtlib.filter_map
-          (fun (subst,metasenv) ->
-            let opened = 
-              ProofEngineHelpers.compare_metasenvs 
-                ~oldmetasenv ~newmetasenv:metasenv
-            in
-            if opened = [] then
-              Some subst
-                else
-              None)
-          solutions
-      in
-       solutions,cache,universe
-;;
-
 let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
   (* argument parsing *)
-  let depth = int "depth" AutoTypes.default_flags.AutoTypes.maxdepth params in
-  let width = int "width" AutoTypes.default_flags.AutoTypes.maxwidth params in
-  let timeout = string "timeout" params in
-  let paramodulation = bool "paramodulation" params in
-  let full = bool "full" params in
-  let superposition = bool "superposition" params in
-  let target = string "target" params in
-  let table = string "table" params in
-  let subterms_only = bool "subterms_only" params in
-  let caso_strano = bool "caso_strano" params in
-  let demod_table = string "demod_table" params in
-  let timeout = 
-    try Some (float_of_string timeout) with Failure _ -> None
-  in
+  let int = int params 
+  and string = string params 
+  and bool = bool params 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
+  let use_paramod = bool "use_paramod" true in
+  let use_only_paramod = bool "paramodulation" false 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 *)
@@ -392,166 +315,38 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
       (* this is the real auto *)
       let _, metasenv, _, _ = proof in
       let _, context, goalty = CicUtil.lookup_meta goal metasenv in
-      let use_paramodulation = 
-        paramodulation && Equality.term_is_equality goalty
+      let universe = 
+        AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe 
+      in 
+      let universe = AutoTypes.universe_of_context context metasenv universe in
+      let oldmetasenv = metasenv in
+      let flags = {
+        AutoTypes.maxdepth = depth;
+        AutoTypes.maxwidth = width;
+        AutoTypes.timeout = 
+          if timeout = 0 then float_of_int timeout 
+          else Unix.gettimeofday() +. (float_of_int timeout); 
+        AutoTypes.use_paramod = use_paramod;
+        AutoTypes.use_only_paramod = use_only_paramod}
       in
-      if use_paramodulation then
-        try
-          let rc = 
-           Saturation.saturate 
-            ~auto:(callback_for_paramodulation dbd) 
-            caso_strano dbd ~depth ~width ~full
-            ?timeout (proof, goal) 
+      let cache = AutoTypes.cache_empty in
+      match Auto.auto dbd universe cache context metasenv [goal] flags with
+      | None,cache -> 
+          raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+      | Some (subst,metasenv),cache -> 
+          let proof,metasenv = 
+            ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+              proof goal (CicMetaSubst.apply_subst subst) metasenv
           in
-          prerr_endline (Saturation.get_stats ());rc
-        with exn ->
-          prerr_endline (Saturation.get_stats ());raise exn
-      else
-        let universe = 
-          AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe 
-        in 
-        let universe = (* we should get back a menv too XXX *)
-          AutoTypes.universe_of_context context metasenv universe 
-        in
-        let oldmetasenv = metasenv in
-        match
-          Auto.auto universe AutoTypes.cache_empty context metasenv [goal]
-            {AutoTypes.default_flags with 
-              AutoTypes.maxdepth = depth;
-              AutoTypes.maxwidth = width;
-(*               AutoTypes.timeout = 0; *)
-            }
-        with
-        | None,cache -> 
-            raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
-        | Some (subst,metasenv),cache -> 
-            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
+          let opened = 
+            ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+              ~newmetasenv:metasenv
+          in
+          proof,opened
 ;;
 
 let auto_tac ~params ~dbd =
       ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
 ;;
 
-(* {{{ **************** applyS *******************)
-
-let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity =
- let (consthead,newmetasenv,arguments,_) =
-   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
- let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in
-  let proof',metasenv =
-   let (puri,metasenv,pbo,pty) = proof in
-    (puri,newmetasenv,pbo,pty),metasenv
-  in
-   let proof'',goals =
-    match LibraryObjects.eq_URI () with
-    | Some uri -> 
-            ProofEngineTypes.apply_tactic
-             (Tacticals.then_
-               ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*))
-               ~continuation:
-                 (PrimitiveTactics.cut_tac
-                   (CicSubstitution.lift 1
-                    (Cic.Appl
-                     [Cic.MutInd (uri,0,[]);
-                      Cic.Sort Cic.Prop;
-                      consthead;
-                      ty])))) (proof',goal)
-   | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
-    in
-     match goals with
-        [g1;g2] ->
-          let proof'',goals =
-           ProofEngineTypes.apply_tactic
-           (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2)
-          in
-           let proof'',goals =
-            ProofEngineTypes.apply_tactic
-             (Tacticals.then_
-              ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft
-                ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1))
-              ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
-             ) (proof'',g1)
-           in
-            proof'',
-             (*CSC: Brrrr.... *)
-             ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
-              ~newmetasenv:(let _,m,_,_ = proof'' in m)
-      | _ -> assert false
-
-let rec count_prods context ty =
- match CicReduction.whd context ty with
-    Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
-  | _ -> 0
-
-let applyS_tac ~dbd ~term (proof, goal) =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let module C = Cic in
-  let (_,metasenv,_,_) = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
-   let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
-    match term with
-       C.Var (uri,exp_named_subst) ->
-        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
-         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
-          exp_named_subst
-        in
-         exp_named_subst_diff,newmeta',newmetasenvfragment,
-          C.Var (uri,exp_named_subst')
-     | C.Const (uri,exp_named_subst) ->
-        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
-         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
-          exp_named_subst
-        in
-         exp_named_subst_diff,newmeta',newmetasenvfragment,
-          C.Const (uri,exp_named_subst')
-     | C.MutInd (uri,tyno,exp_named_subst) ->
-        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
-         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
-          exp_named_subst
-        in
-         exp_named_subst_diff,newmeta',newmetasenvfragment,
-          C.MutInd (uri,tyno,exp_named_subst')
-     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
-         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
-          exp_named_subst
-        in
-         exp_named_subst_diff,newmeta',newmetasenvfragment,
-          C.MutConstruct (uri,tyno,consno,exp_named_subst')
-     | _ -> [],newmeta,[],term
-   in
-   let metasenv' = metasenv@newmetasenvfragment in
-   let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
-   in
-   let termty =
-     CicSubstitution.subst_vars exp_named_subst_diff termty in
-   let goal_arity = count_prods context ty in
-   let res =
-    new_metasenv_and_unify_and_t dbd proof goal
-     newmeta' metasenv' context term' ty termty goal_arity
-   in
-    res
-
-let applyS_tac ~dbd ~term =
- ProofEngineTypes.mk_tactic
-  (fun status ->
-    try applyS_tac ~dbd ~term status
-    with 
-    | CicUnification.UnificationFailure msg
-    | CicTypeChecker.TypeCheckerFailure msg ->
-        raise (ProofEngineTypes.Fail msg))
-
-(* }}} ********************************)
-
 let pp_proofterm = Equality.pp_proofterm;;
index 354b1b7387d0b1496ded7981740d32e585af3f6b..fadb603ebf484a5c90c4d60e9a360f10e3b3106d 100644 (file)
@@ -29,6 +29,4 @@ val auto_tac:
   dbd:HMysql.dbd -> 
   ProofEngineTypes.tactic
 
-val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
-
 val pp_proofterm: Cic.term -> string
index f9d6a021621bb3f77aacbc84323f7eba20487c68..60643d8702d29822ba15a5243411a584ca534e2c 100644 (file)
@@ -84,6 +84,9 @@ let universe_of_context ctx metasenv universe =
   in
   rc
 ;;
+let add_to_universe key proof universe =
+  index universe key proof
+;;
 
 (* (proof,ty) list *)
 type cache_key = Cic.term
@@ -126,18 +129,33 @@ let cache_add_underinspection cache cache_key depth =
   | Succeded _ -> assert false (* it must be a new goal *)
 ;;
 let cache_empty = []
+let cache_print context cache = 
+  let names = List.map (function None -> None | Some (x,_) -> Some x) context in
+  String.concat "\n" 
+    (HExtlib.filter_map 
+      (function 
+        | (k,Succeded _) -> Some (CicPp.pp k names)
+        | _ -> None)
+      cache)
+;;
+let cache_size cache = 
+  List.length (List.filter (function (_,Succeded _) -> true | _ -> false) cache)
+;;
+let cache_clean cache = 
+  List.filter (function (_,Succeded _) -> true | _ -> false) cache
+;;
 
 type flags = {
   maxwidth: int;
   maxdepth: int;
   timeout: float;
+  use_paramod: bool;
+  use_only_paramod : bool;
 }
 
-let default_flags = {
-  maxwidth = 3;
-  maxdepth = 5;
-  timeout = 0.;
-}
+let default_flags _ =
+  {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. 3.0;use_paramod=true;use_only_paramod=false}
+;;
 
 (* (metasenv, subst, (metano,depth)list *)
 type sort = P | T;;
index c580bff3955849162e35785a6d0a77c16e339efb..1cf966ca0d96e7a7e56fc233e427b7037d0bf5dd 100644 (file)
@@ -30,6 +30,7 @@ val universe_of_goals:
   HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
     universe -> universe
 val universe_of_context: Cic.context -> Cic.metasenv -> universe -> universe
+val add_to_universe: Cic.term -> Cic.term -> universe -> universe
 
 type cache
 type cache_key = Cic.term
@@ -43,14 +44,19 @@ val cache_add_failure: cache -> cache_key -> int -> cache
 val cache_add_success: cache -> cache_key -> Cic.term -> cache
 val cache_add_underinspection: cache -> cache_key -> int -> cache
 val cache_empty: cache
+val cache_print: Cic.context -> cache -> string
+val cache_size: cache -> int
+val cache_clean: cache -> cache
 
 type flags = {
   maxwidth: int;
   maxdepth: int;
   timeout: float;
+  use_paramod: bool;
+  use_only_paramod : bool;
 }
 
-val default_flags : flags
+val default_flags : unit -> flags
 
 (* (metasenv, subst, (metano,depth)list *)
 type sort = P | T;;
index 0dc19582a329261b1d8e43e0b20a0c017b0d6646..cd14f3f5eb8d6be766c272b73e5af3fd9aa730fa 100644 (file)
@@ -207,6 +207,14 @@ let is_predicate u =
     check_last_pi ty
 ;;
 
+let only constants uri =
+  prerr_endline (UriManager.string_of_uri uri);
+  let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
+  let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+  let consts = Constr.constants_of ty in
+  Constr.UriManagerSet.subset consts constants 
+;;
+
 let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
   let (_, metasenv, _, _) = proof in
   let add_uris_for acc goal =
@@ -245,6 +253,7 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
 *)
   let uris = List.filter nonvar (List.map snd uris) in
   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+  let uris = List.filter (only all_constants_closed) uris in
    uris
 ;;
 
index 2c287d5637668775c3fb0628ded2a1e10e39273f..cfef9452f0a3094c4283c1392f6dfc98495849c1 100644 (file)
@@ -29,6 +29,7 @@
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 type uncomparable = int -> int 
+
 type equality =
     uncomparable *       (* trick to break structural equality *)
     int  *               (* weight *)
@@ -45,29 +46,29 @@ and proof =
             (* subst, (rule,eq1, eq2,predicate) *)  
 and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
+type equality_bag = (int,equality) Hashtbl.t * int ref
 
 type goal = goal_proof * Cic.metasenv * Cic.term
 
 (* globals *)
-let maxid = ref 0;;
-let id_to_eq = Hashtbl.create 1024;;
+let mk_equality_bag () =
+  Hashtbl.create 1024, ref 0
+;;
 
-let freshid () =
-  incr maxid; !maxid
+let freshid (_,i) =
+  incr i; !i
 ;;
 
-let reset () = 
-  maxid := 0;
-  Hashtbl.clear  id_to_eq
+let add_to_bag (id_to_eq,_) id eq =
+  Hashtbl.add id_to_eq id eq
 ;;
 
 let uncomparable = fun _ -> 0
 
-let mk_equality (weight,p,(ty,l,r,o),m) =
-  let id = freshid () in
+let mk_equality bag (weight,p,(ty,l,r,o),m) =
+  let id = freshid bag in
   let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
-  Hashtbl.add id_to_eq id eq;
-
+  add_to_bag bag id eq;
   eq
 ;;
 
@@ -111,7 +112,7 @@ let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
   Pervasives.compare s1 s2
 ;;
 
-let rec max_weight_in_proof current =
+let rec max_weight_in_proof ((id_to_eq,_) as bag) current =
   function
    | Exact _ -> current
    | Step (_, (_,id1,(_,id2),_)) ->
@@ -120,23 +121,23 @@ let rec max_weight_in_proof current =
        let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
        let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
        let current = max current w1 in
-       let current = max_weight_in_proof current p1 in
+       let current = max_weight_in_proof bag current p1 in
        let current = max current w2 in
-       max_weight_in_proof current p2
+       max_weight_in_proof bag current p2
 
-let max_weight_in_goal_proof =
+let max_weight_in_goal_proof ((id_to_eq,_) as bag) =
   List.fold_left 
     (fun current (_,_,id,_,_) ->
        let eq = Hashtbl.find id_to_eq id in
        let (w,p,(_,_,_,_),_,_) = open_equality eq in
        let current = max current w in
-       max_weight_in_proof current p)
+       max_weight_in_proof bag current p)
 
-let max_weight goal_proof proof =
-  let current = max_weight_in_proof 0 proof in
-  max_weight_in_goal_proof current goal_proof
+let max_weight bag goal_proof proof =
+  let current = max_weight_in_proof bag 0 proof in
+  max_weight_in_goal_proof bag current goal_proof
 
-let proof_of_id id =
+let proof_of_id (id_to_eq,_) id =
   try
     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
       p,l,r
@@ -144,7 +145,7 @@ let proof_of_id id =
       Not_found -> assert false
 
 
-let string_of_proof ?(names=[]) p gp = 
+let string_of_proof ?(names=[]) bag p gp = 
   let str_of_pos = function
     | Utils.Left -> "left"
     | Utils.Right -> "right"
@@ -159,8 +160,8 @@ let string_of_proof ?(names=[]) p gp =
         Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
           prefix (string_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
           (CicPp.pp pred names)^ 
-        aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ 
-        aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) 
+        aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id bag eq1)) ^ 
+        aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id bag eq2)) 
   in
   aux 0 "" p ^ 
   String.concat "\n" 
@@ -169,11 +170,11 @@ let string_of_proof ?(names=[]) p gp =
         (Printf.sprintf 
           "GOAL: %s %s %d %s %s\n" (string_of_rule r)
             (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ 
-        aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
+        aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id bag i)))
       gp)
 ;;
 
-let rec depend eq id seen =
+let rec depend ((id_to_eq,_) as bag) eq id seen =
   let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
   if List.mem ideq seen then 
     false,seen
@@ -187,11 +188,11 @@ let rec depend eq id seen =
           let seen = ideq::seen in
           let eq1 = Hashtbl.find id_to_eq id1 in
           let eq2 = Hashtbl.find id_to_eq id2 in  
-          let b1,seen = depend eq1 id seen in
-          if b1 then b1,seen else depend eq2 id seen
+          let b1,seen = depend bag eq1 id seen in
+          if b1 then b1,seen else depend bag eq2 id seen
 ;;
 
-let depend eq id = fst (depend eq id []);;
+let depend bag eq id = fst (depend bag eq id []);;
 
 let ppsubst = Subst.ppsubst ~names:[];;
 
@@ -612,9 +613,9 @@ let parametrize_proof p l r ty =
   proof, instance
 ;;
 
-let wfo goalproof proof id =
+let wfo bag goalproof proof id =
   let rec aux acc id =
-    let p,_,_ = proof_of_id id in
+    let p,_,_ = proof_of_id bag id in
     match p with
     | Exact _ -> if (List.mem id acc) then acc else id :: acc
     | Step (_,(_,id1, (_,id2), _)) -> 
@@ -630,7 +631,7 @@ let wfo goalproof proof id =
   List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof
 ;;
 
-let string_of_id names id = 
+let string_of_id (id_to_eq,_) names id = 
   if id = 0 then "" else 
   try
     let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
@@ -649,8 +650,8 @@ let string_of_id names id =
   with
       Not_found -> assert false
 
-let pp_proof names goalproof proof subst id initial_goal =
-  String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^ 
+let pp_proof bag names goalproof proof subst id initial_goal =
+  String.concat "\n" (List.map (string_of_id bag names) (wfo bag goalproof proof id)) ^ 
   "\ngoal:\n   " ^ 
     (String.concat "\n   " 
       (fst (List.fold_right
@@ -675,24 +676,24 @@ module OT =
 
 module M = Map.Make(OT)
 
-let rec find_deps m i = 
+let rec find_deps bag m i = 
   if M.mem i m then m
   else 
-    let p,_,_ = proof_of_id i in
+    let p,_,_ = proof_of_id bag i in
     match p with
     | Exact _ -> M.add i [] m
     | Step (_,(_,id1,(_,id2),_)) -> 
-        let m = find_deps m id1 in
-        let m = find_deps m id2 in
+        let m = find_deps bag m id1 in
+        let m = find_deps bag m id2 in
         (* without the uniq there is a stack overflow doing concatenation *)
         let xxx = [id1;id2] @ M.find id1 m @ M.find id2 m in 
         let xxx = HExtlib.list_uniq (List.sort Pervasives.compare xxx) in
         M.add i xxx m
 ;;
 
-let topological_sort l = 
+let topological_sort bag l = 
   (* build the partial order relation *)
-  let m = List.fold_left (fun m i -> find_deps m i) M.empty l in
+  let m = List.fold_left (fun m i -> find_deps bag m i) M.empty l in
   let m = (* keep only deps inside l *) 
     List.fold_left 
       (fun m' i ->
@@ -724,14 +725,14 @@ let topological_sort l =
   
 
 (* returns the list of ids that should be factorized *)
-let get_duplicate_step_in_wfo l p =
+let get_duplicate_step_in_wfo bag l p =
   let ol = List.rev l in
   let h = Hashtbl.create 13 in
   (* NOTE: here the n parameter is an approximation of the dependency 
      between equations. To do things seriously we should maintain a 
      dependency graph. This approximation is not perfect. *)
   let add i = 
-    let p,_,_ = proof_of_id i in 
+    let p,_,_ = proof_of_id bag i in 
     match p with 
     | Exact _ -> true
     | _ -> 
@@ -746,23 +747,23 @@ let get_duplicate_step_in_wfo l p =
     | Step (_,(_,i1,(_,i2),_)) -> 
         let go_on_1 = add i1 in
         let go_on_2 = add i2 in
-        if go_on_1 then aux (let p,_,_ = proof_of_id i1 in p);
-        if go_on_2 then aux (let p,_,_ = proof_of_id i2 in p)
+        if go_on_1 then aux (let p,_,_ = proof_of_id bag i1 in p);
+        if go_on_2 then aux (let p,_,_ = proof_of_id bag i2 in p)
   in
   aux p;
   List.iter
-    (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id id in p))
+    (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id bag id in p))
     ol;
   (* now h is complete *)
   let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
   let proofs = List.filter (fun (_,c) -> c > 1) proofs in
-  let res = topological_sort (List.map (fun (i,_) -> i) proofs) in
+  let res = topological_sort bag (List.map (fun (i,_) -> i) proofs) in
   res
 ;;
 
-let build_proof_term eq h lift proof =
+let build_proof_term bag eq h lift proof =
   let proof_of_id aux id =
-    let p,l,r = proof_of_id id in
+    let p,l,r = proof_of_id bag id in
     try List.assoc id h,l,r with Not_found -> aux p, l, r
   in
   let rec aux = function
@@ -792,17 +793,17 @@ let build_proof_term eq h lift proof =
    aux proof
 ;;
 
-let build_goal_proof eq l initial ty se context menv =
+let build_goal_proof bag eq l initial ty se context menv =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
-  let lets = get_duplicate_step_in_wfo l initial in
+  let lets = get_duplicate_step_in_wfo bag l initial in
   let letsno = List.length lets in
   let _,mty,_,_ = open_eq ty in
   let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in
   let lets,_,h = 
     List.fold_left
       (fun (acc,n,h) id -> 
-        let p,l,r = proof_of_id id in
-        let cic = build_proof_term eq h n p in
+        let p,l,r = proof_of_id bag id in
+        let cic = build_proof_term bag eq h n p in
         let real_cic,instance = 
           parametrize_proof cic l r (CicSubstitution.lift n mty)
         in
@@ -814,8 +815,8 @@ let build_goal_proof eq l initial ty se context menv =
     let rec aux se current_proof = function
       | [] -> current_proof,se
       | (rule,pos,id,subst,pred)::tl ->
-          let p,l,r = proof_of_id id in
-           let p = build_proof_term eq h letsno p in
+          let p,l,r = proof_of_id bag id in
+           let p = build_proof_term bag eq h letsno p in
            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
          let varname = 
            match rule with
@@ -833,9 +834,9 @@ let build_goal_proof eq l initial ty se context menv =
            in
            let proof,se = aux se proof tl in
            Subst.apply_subst_lift letsno subst proof,
-           List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
+           List.map (fun x -> Subst.apply_subst(*_lift letsno*) subst x) se
     in
-    aux se (build_proof_term eq h letsno initial) l
+    aux se (build_proof_term bag eq h letsno initial) l
   in
   let n,proof = 
     let initial = proof in
@@ -857,7 +858,7 @@ let refl_proof eq_uri ty term =
   Cic.Appl [Cic.MutConstruct (eq_uri, 0, 1, []); ty; term]
 ;;
 
-let metas_of_proof p =
+let metas_of_proof bag p =
   let eq = 
     match LibraryObjects.eq_URI () with
     | Some u -> u 
@@ -866,7 +867,7 @@ let metas_of_proof p =
           (ProofEngineTypes.Fail 
             (lazy "No default equality defined when calling metas_of_proof"))
   in
-  let p = build_proof_term eq [] 0 p in
+  let p = build_proof_term bag eq [] 0 p in
   Utils.metas_of_term p
 ;;
 
@@ -908,7 +909,7 @@ let fix_metas_goal newmeta goal =
   newmeta+1,(proof, menv, ty)
 ;;
 
-let fix_metas newmeta eq = 
+let fix_metas bag newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated = 
 (* List.map (fun i ,_,_ -> i) menv *)
@@ -926,7 +927,7 @@ let fix_metas newmeta eq =
         Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
   in
   let p = fix_proof p in
-  let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in
+  let eq' = mk_equality bag (w, p, (ty, left, right, o), metasenv) in
   newmeta+1, eq'  
 
 exception NotMetaConvertible;;
@@ -1066,14 +1067,14 @@ let term_is_equality term =
   | _ -> false
 ;;
 
-let equality_of_term proof term =
+let equality_of_term bag proof term =
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] 
     when LibraryObjects.is_eq_URI uri ->
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = Utils.compute_equality_weight stat in
-      let e = mk_equality (w, Exact proof, stat,[]) in
+      let e = mk_equality bag (w, Exact proof, stat,[]) in
       e
   | _ ->
       raise TermIsNotAnEquality
@@ -1114,7 +1115,7 @@ let term_of_equality eq_uri equality =
       menv (argsno, t))
 ;;
 
-let symmetric eq_ty l id uri m =
+let symmetric bag eq_ty l id uri m =
   let eq = Cic.MutInd(uri,0,[]) in
   let pred = 
     Cic.Lambda (Cic.Name "Sym",eq_ty,
@@ -1127,7 +1128,7 @@ let symmetric eq_ty l id uri m =
       [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) 
   in
   let id1 = 
-    let eq = mk_equality (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
+    let eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
     let (_,_,_,_,id) = open_equality eq in
     id
   in
@@ -1144,10 +1145,10 @@ module IntSet = Set.Make(IntOT);;
 
 let n_purged = ref 0;;
 
-let collect alive1 alive2 alive3 =
+let collect ((id_to_eq,_) as bag) alive1 alive2 alive3 =
 (*   let _ = <:start<collect>> in *)
   let deps_of id = 
-    let p,_,_ = proof_of_id id in  
+    let p,_,_ = proof_of_id bag id in  
     match p with
     | Exact _ -> IntSet.empty
     | Step (_,(_,id1,(_,id2),_)) ->
index 1a909dfc4b387c40465d5743bfc940964ba5e79c..bd3d4c2acda6de7212d31697b3ebc18da189a5e3 100644 (file)
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 
+type equality_bag
+
+val mk_equality_bag: unit -> equality_bag
+
 type equality 
 
 and proof =
@@ -36,21 +40,20 @@ and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 type goal = goal_proof * Cic.metasenv * Cic.term
 
 val pp_proof: 
+  equality_bag ->
   (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int ->
     Cic.term -> string
 
 val pp_proofterm: Cic.term -> string
     
-val reset : unit -> unit
-
 val mk_equality :
-  int * proof * 
+  equality_bag -> int * proof * 
   (Cic.term * Cic.term * Cic.term * Utils.comparison) *
   Cic.metasenv -> 
     equality
 
 val mk_tmp_equality :
 int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> 
+ int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> 
     equality
     
 val open_equality :
@@ -58,28 +61,31 @@ val open_equality :
     int * proof * 
     (Cic.term * Cic.term * Cic.term * Utils.comparison) *
     Cic.metasenv * int
-val depend : equality -> int -> bool
+val depend : equality_bag -> equality -> int -> bool
 val compare : equality -> equality -> int
-val max_weight_in_proof : int-> proof -> int
-val max_weight : goal_proof -> proof -> int
-val string_of_equality : ?env:Utils.environment -> equality -> string
+val max_weight_in_proof : equality_bag -> int -> proof -> int
+val max_weight : equality_bag -> goal_proof -> proof -> int
+val string_of_equality : 
+  ?env:Utils.environment -> equality -> string
 val string_of_proof : 
-  ?names:(Cic.name option)list -> proof -> goal_proof -> string
+  ?names:(Cic.name option)list -> equality_bag -> proof -> goal_proof -> string
 (* given a proof and a list of meta indexes we are interested in the
  * instantiation gives back the cic proof and the list of instantiations *)  
 (* build_goal_proof [eq_URI] [goal_proof] [initial_proof] [ty] 
  *  [ty] is the type of the goal *)
 val build_goal_proof: 
+  equality_bag ->
   UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> 
     Cic.context -> Cic.metasenv -> 
     Cic.term * Cic.term list
-val build_proof_term : 
+val build_proof_term :
+  equality_bag ->
   UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term
 val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
 val fix_metas_goal: int -> goal -> int * goal
-val fix_metas: int -> equality -> int * equality
-val metas_of_proof: proof -> int list
+val fix_metas: equality_bag -> int -> equality -> int * equality
+val metas_of_proof: equality_bag -> proof -> int list
 
 (* this should be used _only_ to apply (efficiently) this subst on the 
  * initial proof passed to build_goal_proof *)
@@ -90,7 +96,7 @@ exception TermIsNotAnEquality;;
    raises TermIsNotAnEquality if term is not an equation.
    The first Cic.term is a proof of the equation
 *)
-val equality_of_term: Cic.term -> Cic.term -> equality
+val equality_of_term: equality_bag -> Cic.term -> Cic.term -> equality
 
 (**
    Re-builds the term corresponding to this equality
@@ -117,13 +123,13 @@ val is_identity: Utils.environment -> equality -> bool
  * [eq_ty] the ty of the equality sides
  *)
 val symmetric:
-  Cic.term -> Cic.term -> int -> UriManager.uri ->
+  equality_bag -> Cic.term -> Cic.term -> int -> UriManager.uri ->
     Cic.metasenv -> proof
 
 (* takes 3 lists of alive ids (they are threated the same way, the type is
  * funny just to not oblige you to concatenate them) and drops all the dead
  * equalities *)
-val collect: int list -> int list -> int list -> unit
+val collect: equality_bag -> int list -> int list -> int list -> unit
 
 (* given an equality, returns the numerical id *)
 val id_of: equality -> int
index f3af1b482e8afb2eece8d1ce79d3e10af7812ec7..0b3ec04a8176d53b9af64b0e384bab55f090b3fb 100644 (file)
@@ -127,14 +127,14 @@ let check_res res msg =
     | None -> ()
 ;;
 
-let check_target context target msg =
+let check_target bag context target msg =
   let w, proof, (eq_ty, left, right, order), metas,_ = 
     Equality.open_equality target in
   (* check that metas does not contains duplicates *)
   let eqs = Equality.string_of_equality target in
   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
   let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
-    @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof)  in
+    @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof)  in
   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
   let _ = if menv <> metas then 
     begin 
@@ -210,7 +210,7 @@ let get_candidates ?env mode tree term =
          the build_newtarget functions]
    ))
 *)
-let rec find_matches metasenv context ugraph lift_amount term termty =
+let rec find_matches bag metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
   let module S = CicSubstitution in
@@ -226,7 +226,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
           Equality.open_equality equality 
         in
         if Utils.debug_metas then 
-          ignore(check_target context (snd candidate) "find_matches");
+          ignore(check_target bag context (snd candidate) "find_matches");
         if Utils.debug_res then 
           begin
             let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
@@ -242,7 +242,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
           end;
         if check && not (fst (CicReduction.are_convertible
                                 ~metasenv context termty ty ugraph)) then (
-          find_matches metasenv context ugraph lift_amount term termty tl
+          find_matches bag metasenv context ugraph lift_amount term termty tl
         ) else
           let do_match c =
             let subst', metasenv', ugraph' =
@@ -260,7 +260,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
               try
                 do_match c 
               with Inference.MatchingFailure ->
-                find_matches metasenv context ugraph lift_amount term termty tl
+                find_matches bag metasenv context ugraph lift_amount term termty tl
             in
               if Utils.debug_res then ignore (check_res res "find1");
               res
@@ -280,10 +280,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
                 if order = U.Gt then
                   res
                 else
-                  find_matches
+                  find_matches bag
                     metasenv context ugraph lift_amount term termty tl
             | None ->
-                find_matches metasenv context ugraph lift_amount term termty tl
+                find_matches bag metasenv context ugraph lift_amount term termty tl
 ;;
 
 let find_matches metasenv context ugraph lift_amount term termty =
@@ -370,7 +370,7 @@ let print_res l =
 
 let subsumption_aux use_unification env table target = 
   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
-  let metasenv, context, ugraph = env in
+  let _, context, ugraph = env in
   let metasenv = tmetas in
   let predicate, unif_fun = 
     if use_unification then
@@ -426,7 +426,7 @@ let unification x y z =
   subsumption_aux true x y z
 ;;
 
-let rec demodulation_aux ?from ?(typecheck=false) 
+let rec demodulation_aux bag ?from ?(typecheck=false) 
   metasenv context ugraph table lift_amount term =
 (*  Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
   let module C = Cic in
@@ -448,7 +448,7 @@ let rec demodulation_aux ?from ?(typecheck=false)
               C.Implicit None, ugraph
           in
           let res =
-            find_matches metasenv context ugraph lift_amount term termty candidates
+            find_matches bag metasenv context ugraph lift_amount term termty candidates
           in
           if Utils.debug_res then ignore(check_res res "demod1"); 
             if res <> None then
@@ -463,7 +463,7 @@ let rec demodulation_aux ?from ?(typecheck=false)
                              (res, tl @ [S.lift 1 t])
                            else 
                              let r =
-                               demodulation_aux ~from:"1" metasenv context ugraph table
+                               demodulation_aux bag ~from:"1" metasenv context ugraph table
                                  lift_amount t
                              in
                                match r with
@@ -478,12 +478,12 @@ let rec demodulation_aux ?from ?(typecheck=false)
                       )
                 | C.Prod (nn, s, t) ->
                     let r1 =
-                      demodulation_aux ~from:"2"
+                      demodulation_aux bag ~from:"2"
                         metasenv context ugraph table lift_amount s in (
                         match r1 with
                           | None ->
                               let r2 =
-                                demodulation_aux metasenv
+                                demodulation_aux bag metasenv
                                   ((Some (nn, C.Decl s))::context) ugraph
                                   table (lift_amount+1) t
                               in (
@@ -499,12 +499,12 @@ let rec demodulation_aux ?from ?(typecheck=false)
                       )
                 | C.Lambda (nn, s, t) ->
                     let r1 =
-                      demodulation_aux 
+                      demodulation_aux bag
                         metasenv context ugraph table lift_amount s in (
                         match r1 with
                           | None ->
                               let r2 =
-                                demodulation_aux metasenv
+                                demodulation_aux bag metasenv
                                   ((Some (nn, C.Decl s))::context) ugraph
                                   table (lift_amount+1) t
                               in (
@@ -528,7 +528,7 @@ let rec demodulation_aux ?from ?(typecheck=false)
 exception Foo
 
 (** demodulation, when target is an equality *)
-let rec demodulation_equality ?from eq_uri newmeta env table target =
+let rec demodulation_equality bag ?from eq_uri newmeta env table target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -546,7 +546,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target =
 (*  let w = Utils.compute_equality_weight stat in*)
   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
   if Utils.debug_metas then 
-    ignore(check_target context target "demod equalities input");
+    ignore(check_target bag context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
   let maxmeta = ref newmeta in
   
@@ -557,7 +557,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target =
         ignore(check_for_duplicates menv "input1");
         ignore(check_disjoint_invariant subst menv "input2");
         let substs = Subst.ppsubst subst in 
-        ignore(check_target context (snd eq_found) ("input3" ^ substs))
+        ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
       end;
     let pos, equality = eq_found in
     let (_, proof', 
@@ -585,14 +585,14 @@ let rec demodulation_equality ?from eq_uri newmeta env table target =
     let stat = (eq_ty, left, right, ordering) in
     let res =
       let w = Utils.compute_equality_weight stat in
-          (Equality.mk_equality (w, newproof, stat,newmenv))
+          (Equality.mk_equality bag (w, newproof, stat,newmenv))
     in
     if Utils.debug_metas then 
-      ignore(check_target context res "buildnew_target output");
+      ignore(check_target bag context res "buildnew_target output");
     !maxmeta, res 
   in
 
-  let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
+  let res = demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left in
   if Utils.debug_res then check_res res "demod result";
   let newmeta, newtarget = 
     match res with
@@ -603,9 +603,9 @@ let rec demodulation_equality ?from eq_uri newmeta env table target =
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
-            demodulation_equality ?from eq_uri newmeta env table newtarget
+            demodulation_equality bag ?from eq_uri newmeta env table newtarget
     | None ->
-        let res = demodulation_aux metasenv' context ugraph table 0 right in
+        let res = demodulation_aux bag metasenv' context ugraph table 0 right in
         if Utils.debug_res then check_res res "demod result 1"; 
           match res with
           | Some t ->
@@ -614,7 +614,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target =
                   (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
-                   demodulation_equality ?from eq_uri newmeta env table newtarget
+                   demodulation_equality bag ?from eq_uri newmeta env table newtarget
           | None ->
               newmeta, target
   in
@@ -760,7 +760,7 @@ let rec betaexpand_term
    the first free meta index, i.e. the first number above the highest meta
    index: its updated value is also returned
 *)
-let superposition_right 
+let superposition_right bag
   ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
   let module C = Cic in
   let module S = CicSubstitution in
@@ -772,7 +772,7 @@ let superposition_right
     Equality.open_equality target 
   in 
   if Utils.debug_metas then 
-    ignore (check_target context target "superpositionright");
+    ignore (check_target bag context target "superpositionright");
   let metasenv' = newmetas in
   let maxmeta = ref newmeta in
   let res1, res2 =
@@ -794,7 +794,7 @@ let superposition_right
   in
   let build_new ordering (bo, s, m, ug, eq_found) =
     if Utils.debug_metas then 
-      ignore (check_target context (snd eq_found) "buildnew1" );
+      ignore (check_target bag context (snd eq_found) "buildnew1" );
     
     let pos, equality =  eq_found in
     let (_, proof', (ty, what, other, _), menv',id') = 
@@ -826,17 +826,17 @@ let superposition_right
       let stat = (eq_ty, left, right, neworder) in
       let eq' =
         let w = Utils.compute_equality_weight stat in
-        Equality.mk_equality (w, newproof, stat, newmenv) in
+        Equality.mk_equality bag (w, newproof, stat, newmenv) in
       if Utils.debug_metas then 
-        ignore (check_target context eq' "buildnew3");
-      let newm, eq' = Equality.fix_metas !maxmeta eq' in
+        ignore (check_target bag context eq' "buildnew3");
+      let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
       if Utils.debug_metas then 
-        ignore (check_target context eq' "buildnew4");
+        ignore (check_target bag context eq' "buildnew4");
       newm, eq'
     in
     maxmeta := newmeta;
     if Utils.debug_metas then 
-      ignore(check_target context newequality "buildnew2"); 
+      ignore(check_target bag context newequality "buildnew2"); 
     newequality
   in
   let new1 = List.map (build_new U.Gt) res1
@@ -847,7 +847,7 @@ let superposition_right
 ;;
 
 (** demodulation, when the target is a theorem *)
-let rec demodulation_theorem newmeta env table theorem =
+let rec demodulation_theorem bag newmeta env table theorem =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -879,7 +879,7 @@ let rec demodulation_theorem newmeta env table theorem =
     !maxmeta, (newterm, newty, menv)
   in  
   let res =
-    demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
+    demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
   in
   match res with
   | Some t ->
@@ -888,7 +888,7 @@ let rec demodulation_theorem newmeta env table theorem =
       if Equality.meta_convertibility termty newty then
         newmeta, newthm
       else
-        demodulation_theorem newmeta env table newthm
+        demodulation_theorem bag newmeta env table newthm
   | None ->
       newmeta, theorem
 ;;
@@ -934,7 +934,7 @@ let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
 
 (* ginve the old [goal], the side that has not changed [posu] and the 
  * expansion builds a new goal *)
-let build_newgoal context goal posu rule expansion =
+let build_newgoal bag context goal posu rule expansion =
   let goalproof,_,_,_,_,_ = open_goal goal in
   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
   let pos, equality = eq_found in
@@ -960,7 +960,7 @@ let build_newgoal context goal posu rule expansion =
    returns a list of new clauses inferred with a left superposition step
    the negative equation "target" and one of the positive equations in "table"
 *)
-let superposition_left (metasenv, context, ugraph) table goal maxmeta = 
+let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = 
   let names = Utils.names_of_context context in
   let proof,menv,eq,ty,l,r = open_goal goal in
   let c = !Utils.compare_terms l r in
@@ -973,9 +973,9 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta =
       prerr_endline (string_of_int (List.length expansionsl));
       prerr_endline (string_of_int (List.length expansionsr));
       *)
-      List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+      List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
       @
-      List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+      List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
       end
     else
         match c with 
@@ -983,13 +983,13 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta =
             let big,small,possmall = l,r,Utils.Right in
             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
             List.map 
-              (build_newgoal context goal possmall Equality.SuperpositionLeft) 
+              (build_newgoal bag context goal possmall Equality.SuperpositionLeft) 
               expansions
         | Utils.Lt -> (* prerr_endline "LT"; *) 
             let big,small,possmall = r,l,Utils.Left in
             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
             List.map 
-              (build_newgoal context goal possmall Equality.SuperpositionLeft) 
+              (build_newgoal bag context goal possmall Equality.SuperpositionLeft) 
               expansions
         | Utils.Eq -> []
         | _ ->
@@ -1005,31 +1005,31 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta =
 ;;
 
 (** demodulation, when the target is a goal *)
-let rec demodulation_goal env table goal =
+let rec demodulation_goal bag env table goal =
   let goalproof,menv,_,_,left,right = open_goal goal in
   let _, context, ugraph = env in
 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
   let do_right () = 
-      let resright = demodulation_aux menv context ugraph table 0 right in
+      let resright = demodulation_aux bag menv context ugraph table 0 right in
       match resright with
       | Some t ->
           let newg = 
-            build_newgoal context goal Utils.Left Equality.Demodulation t 
+            build_newgoal bag context goal Utils.Left Equality.Demodulation t 
           in
           if goal_metaconvertibility_eq goal newg then
             false, goal
           else
-            true, snd (demodulation_goal env table newg)
+            true, snd (demodulation_goal bag env table newg)
       | None -> false, goal
   in
-  let resleft = demodulation_aux menv context ugraph table 0 left in
+  let resleft = demodulation_aux bag menv context ugraph table 0 left in
   match resleft with
   | Some t ->
-      let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
+      let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
       if goal_metaconvertibility_eq goal newg then
         do_right ()
       else
-        true, snd (demodulation_goal env table newg)
+        true, snd (demodulation_goal bag env table newg)
   | None -> do_right ()
 ;;
 
index ef068151ea3210aa5463b0f66b7b79f86e68aa27..e180511a64cbbd9f6d84d779249e83833b6ef615 100644 (file)
@@ -50,11 +50,13 @@ val subsumption :
   (Subst.substitution * Equality.equality * bool) option
 
 val superposition_left :
+  Equality.equality_bag ->
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
   Index.t -> Equality.goal -> int ->
     int * Equality.goal list
 
 val superposition_right :
+  Equality.equality_bag ->
   ?subterms_only:bool ->
     UriManager.uri ->
   int ->
@@ -64,6 +66,7 @@ val superposition_right :
   int * Equality.equality list
 
 val demodulation_equality :
+  Equality.equality_bag ->
   ?from:string -> 
   UriManager.uri ->
   int ->
@@ -71,17 +74,20 @@ val demodulation_equality :
   Index.t ->
   Equality.equality -> int * Equality.equality
 val demodulation_goal :
+  Equality.equality_bag ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.goal ->
   bool * Equality.goal
 val demodulation_theorem :
+  Equality.equality_bag ->
   'a ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Cic.term * Cic.term * Cic.metasenv ->
   'a * (Cic.term * Cic.term * Cic.metasenv)
 val check_target:
+  Equality.equality_bag ->
   Cic.context ->
     Equality.equality -> string -> unit
 
index e7f3d8d21eff29bcd40c9499e1fbd9fae49a3f27..9ada6994319818edfec0cbdc0c960327bf03a18a 100644 (file)
@@ -31,12 +31,13 @@ open Utils;;
 open Printf;;
 
 type auto_type = 
+  int ->
   AutoTypes.flags ->
   ProofEngineTypes.proof -> 
   Cic.context -> 
-  ?universe:AutoTypes.universe -> AutoTypes.cache -> 
+  AutoTypes.cache -> 
   ProofEngineTypes.goal list ->
-    Cic.substitution list * AutoTypes.cache * AutoTypes.universe
+    Cic.substitution list * AutoTypes.cache * int
 
 let debug_print s = prerr_endline (Lazy.force s);;
 
@@ -220,8 +221,8 @@ let check_eq context msg eq =
   else ()
 ;;
 
-let default_auto _ _ _ ?(universe:AutoTypes.universe option) _ _ = 
-  [],AutoTypes.cache_empty,AutoTypes.empty_universe
+let default_auto maxm _ _ _ _ _ = 
+  [],AutoTypes.cache_empty,maxm
 ;;
 
 (* far sta roba e' un casino perche' bisogna pulire il contesto lasciando solo
@@ -256,9 +257,9 @@ let ty_of_eq = function
   | _ -> assert false
 ;;
 
-exception UnableToSaturate of AutoTypes.universe option * AutoTypes.cache
+exception UnableToSaturate of AutoTypes.cache * int
 
-let saturate_term context metasenv oldnewmeta term ?universe cache auto fast = 
+let saturate_term context metasenv oldnewmeta term cache auto fast = 
   let head, metasenv, args, newmeta =
     ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
   in
@@ -280,23 +281,27 @@ let saturate_term context metasenv oldnewmeta term ?universe cache auto fast =
       | _ -> assert false)
     args
   in
-  let results,universe,cache = 
+  let results,cache,newmeta = 
     if args_for_auto = [] then 
       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
-      [args,metasenv,newmetas,head,newmeta],universe,cache
+      [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.timeout = 1.0;maxwidth = 2;maxdepth = 2}
+          {AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+           maxwidth = 2;maxdepth = 2;
+           use_paramod=true;use_only_paramod=false}
         else
-          {AutoTypes.timeout = 1.0;maxwidth = 3;maxdepth = 3} 
+          {AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+           maxwidth = 3;maxdepth = 3;
+           use_paramod=true;use_only_paramod=false} 
       in
-      match auto flags proof context ?universe cache args_for_auto with
-      | [],cache,universe -> raise (UnableToSaturate (Some universe,cache))
-      | substs,cache,universe ->
+      match auto newmeta flags proof context cache args_for_auto with
+      | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta))
+      | substs,cache,newmeta ->
           List.map 
             (fun subst ->
               let metasenv = 
@@ -307,11 +312,11 @@ let saturate_term context metasenv oldnewmeta term ?universe cache auto fast =
                 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv 
               in
               let args = List.map (CicMetaSubst.apply_subst subst) args in
-              args,metasenv,newmetas,head,newmeta)
-            substs,
-          Some universe,cache
+              let newm = CicMkImplicit.new_meta metasenv subst in
+              args,metasenv,newmetas,head,max newm newmeta)
+            substs, cache, newmeta
   in
-  results,universe,cache
+  results,cache,newmeta
 ;;
 
 let rec is_an_equality = function
@@ -321,7 +326,7 @@ let rec is_an_equality = function
   | _ -> false
 ;;
 
-let build_equality_of_hypothesis index head args newmetas = 
+let build_equality_of_hypothesis bag index head args newmetas maxmeta = 
   match head with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
       let p =
@@ -335,27 +340,31 @@ let build_equality_of_hypothesis index head args newmetas =
       (* let w = compute_equality_weight stat in *)
       let w = 0 in 
       let proof = Equality.Exact p in
-      Equality.mk_equality (w, proof, stat, newmetas)
+      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 build_equality ty t1 t2 proof menv =
+let build_equality bag ty t1 t2 proof menv maxmeta =
   let o = !Utils.compare_terms t1 t2 in
   let stat = (ty,t1,t2,o) in
   let w = compute_equality_weight stat in
   let proof = Equality.Exact proof in
-  Equality.mk_equality (w, proof, stat, menv)
+  let e = Equality.mk_equality bag (w, proof, stat, menv) in
+  (* to clean the local context of metas *)
+  Equality.fix_metas bag maxmeta e
 ;;
 
-let find_equalities ?(auto = default_auto) context proof ?universe cache =
+let find_equalities maxmeta bag ?(auto = default_auto) context proof cache =
   prerr_endline "find_equalities";
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
   let _,metasenv,_,_ = proof in
-  let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
-  let rec aux universe cache index newmeta = function
-    | [] -> [], newmeta,universe,cache
+  let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
+  let rec aux cache index newmeta = function
+    | [] -> [], newmeta,cache
     | (Some (_, C.Decl (term)))::tl ->
         debug_print
           (lazy
@@ -365,47 +374,50 @@ let find_equalities ?(auto = default_auto) context proof ?universe cache =
           | C.Prod (name, s, t) when is_an_equality t ->
               (try 
                 let term = S.lift index term in
-                let saturated ,universe,cache = 
+                let saturated,cache,newmeta = 
                   saturate_term context metasenv newmeta term 
-                    ?universe cache auto false
+                    cache auto false
                 in
                 let eqs,newmeta = 
                   List.fold_left 
                    (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
-                     let equality = 
-                       build_equality_of_hypothesis index head args newmetas 
+                     let newmeta, equality = 
+                       build_equality_of_hypothesis 
+                         bag index head args newmetas (max newmeta newmeta')
                      in
-                     equality::acc,(max newmeta newmeta' + 1))
-                   ([],0) saturated
+                     equality::acc, newmeta + 1)
+                   ([],newmeta) saturated
                 in
-                 eqs, newmeta, universe, cache
-              with UnableToSaturate (universe,cache) ->
-                [],newmeta,universe,cache)
+                 eqs, newmeta, cache
+              with UnableToSaturate (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 e = build_equality_of_hypothesis index term [] [] in
-              [e], (newmeta+1),universe,cache
-          | _ -> [], newmeta, universe, cache
+              let newmeta, e = 
+                build_equality_of_hypothesis bag index term [] [] newmeta
+              in
+              [e], (newmeta+1),cache
+          | _ -> [], newmeta, cache
         in 
-        let eqs, newmeta, universe, cache = do_find context term in
+        let eqs, newmeta, cache = do_find context term in
         if eqs = [] then 
           debug_print (lazy "skipped")
         else 
           debug_print (lazy "ok");
-        let rest, newmeta,universe,cache = 
-          aux universe cache (index+1) newmeta tl
+        let rest, newmeta,cache = 
+          aux cache (index+1) newmeta tl
         in
-        List.map (fun x -> index,x) eqs @ rest, newmeta, universe, cache
+        List.map (fun x -> index,x) eqs @ rest, newmeta, cache
     | _::tl ->
-        aux universe cache (index+1) newmeta tl
+        aux cache (index+1) newmeta tl
   in
-  let il, maxm, universe, cache = 
-    aux universe cache 1 newmeta context 
+  let il, maxm, cache = 
+    aux cache 1 newmeta context 
   in
   let indexes, equalities = List.split il in
   (* ignore (List.iter (check_eq context "find") equalities); *)
-  indexes, equalities, maxm, universe, cache
+  indexes, equalities, maxm, cache
 ;;
 
 
@@ -458,8 +470,8 @@ let utty_of_u u =
   u, t, ty
 ;;
 
-let find_library_equalities 
-  ?(auto = default_auto) caso_strano dbd context status maxmeta ?universe cache 
+let find_library_equalities bag
+  ?(auto = default_auto) caso_strano dbd context status maxmeta cache 
 = 
   prerr_endline "find_library_equalities";
   let module C = Cic in
@@ -519,20 +531,20 @@ let find_library_equalities
  let candidates = List.map utty_of_u eqs in
  let candidates = List.filter is_monomorphic_eq candidates in
  let candidates = List.filter is_var_free candidates in
- let rec aux universe cache newmeta = function
-    | [] -> [], newmeta, universe, cache
+ let rec aux cache newmeta = function
+    | [] -> [], newmeta, cache
     | (uri, term, termty)::tl ->
         debug_print
           (lazy
              (Printf.sprintf "Examining: %s (%s)"
                 (CicPp.ppterm term) (CicPp.ppterm termty)));
-        let res, newmeta, universe, cache = 
+        let res, newmeta, cache = 
           match termty with
           | C.Prod (name, s, t) ->
               (try
-                let saturated, universe,cache = 
+                let saturated,cache,newmeta = 
                   saturate_term context metasenv newmeta termty 
-                    ?universe cache auto true
+                    cache auto true
                 in
                 let eqs,newmeta = 
                   List.fold_left 
@@ -542,27 +554,28 @@ let find_library_equalities
                        when LibraryObjects.is_eq_URI uri ->
                          let proof = C.Appl (term::args) in
                          prerr_endline ("PROVA: " ^ CicPp.ppterm proof);
-                         let equality = 
-                           build_equality ty t1 t2 proof newmetas 
+                         let maxmeta, equality = 
+                           build_equality bag ty t1 t2 proof newmetas 
+                             (max newmeta newmeta')
                          in
-                         equality::acc,(max newmeta newmeta' + 1)
+                         equality::acc,maxmeta + 1
                      | _ -> assert false)
-                   ([],0) saturated
+                   ([],newmeta) saturated
                 in
-                 eqs, newmeta , universe, cache
-              with UnableToSaturate (universe,cache) ->
-                [], newmeta , universe, cache)
+                 eqs, newmeta , cache
+              with UnableToSaturate (cache,newmeta) ->
+                [], newmeta , cache)
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> 
-              let e = build_equality ty t1 t2 term [] in
-              [e], (newmeta+1), universe, cache
+              let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
+              [e], newmeta+1, cache
           | _ -> assert false
         in
         let res = List.map (fun e -> uri, e) res in
-        let tl, newmeta, universe, cache = aux universe cache newmeta tl in
-        res @ tl, newmeta, universe, cache
+        let tl, newmeta, cache = aux cache newmeta tl in
+        res @ tl, newmeta, cache
   in
-  let found, maxm, universe, cache = 
-    aux universe cache maxmeta candidates 
+  let found, maxm, cache = 
+    aux cache maxmeta candidates 
   in
   let uriset, eqlist = 
     let mceq = Equality.meta_convertibility_eq in
@@ -577,7 +590,7 @@ let find_library_equalities
           ) else (UriManager.UriSet.add u s, (u, e)::l))
        (UriManager.UriSet.empty, []) found)
   in
-  uriset, eqlist, maxm, universe, cache
+  uriset, eqlist, maxm, cache
 ;;
 
 let get_stats () = "" (*<:show<Inference.>>*) ;;
index 47626fcf00f21e9e91ffe5b96bcb87298c8fb89a..97c86898561c8f2a30f28248ae254f26e9021e4f 100644 (file)
@@ -42,13 +42,14 @@ val unification:
   CicUniv.universe_graph ->
     Subst.substitution * Cic.metasenv * CicUniv.universe_graph
 
-type auto_type = 
+type auto_type = (* the universe must be hardocded *)
+  int -> (* maxmeta *)
   AutoTypes.flags ->
   ProofEngineTypes.proof -> 
   Cic.context -> 
-  ?universe:AutoTypes.universe -> AutoTypes.cache -> 
+  AutoTypes.cache -> 
   ProofEngineTypes.goal list ->
-    Cic.substitution list * AutoTypes.cache * AutoTypes.universe
+    Cic.substitution list * AutoTypes.cache * int
     
 (**
    scans the context to find all Declarations "left = right"; returns a
@@ -57,20 +58,22 @@ type auto_type =
    fresh metas...
 *)
 val find_equalities:
+  int ->
+  Equality.equality_bag ->
   ?auto:auto_type ->
   Cic.context -> ProofEngineTypes.proof -> 
-  ?universe:AutoTypes.universe -> AutoTypes.cache -> 
-    int list * Equality.equality list * int *
-    AutoTypes.universe option * AutoTypes.cache
+  AutoTypes.cache -> 
+    int list * Equality.equality list * int * AutoTypes.cache
 
 (**
    searches the library for equalities that can be applied to the current goal
 *)
 val find_library_equalities:
+  Equality.equality_bag ->
   ?auto:auto_type ->
   bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
-  ?universe:AutoTypes.universe -> AutoTypes.cache ->  
+  AutoTypes.cache ->  
     UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int *
-    AutoTypes.universe option * AutoTypes.cache
+    AutoTypes.cache
 
 val get_stats: unit -> string
index cf093473c7e77088bbffdb219382cbabfc5d9426..11966ef8d016ef7eb8dba7a7e4a2cda72d3882eb 100644 (file)
@@ -70,15 +70,6 @@ let maxmeta = ref 0;;
 let maxdepth = ref 3;;
 let maxwidth = ref 3;;
 
-type new_proof = 
-  Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv
-type result =
-  | ParamodulationFailure of string
-  | ParamodulationSuccess of new_proof
-;;
-
-(* type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; *)
-
 type theorem = Cic.term * Cic.term * Cic.metasenv;;
 
 let symbols_of_equality equality = 
@@ -117,22 +108,25 @@ end
 
 module EqualitySet = Set.Make(OrderedEquality);;
 
-exception Empty_list;;
-
-type passives = Equality.equality list * EqualitySet.t;;
-type actives = Equality.equality list * Indexing.Index.t;;
-
-(* initializes the passive set of equalities 
- * XXX I think EqualitySet.elements should be ok (to eliminate duplicates)
- *)
-let make_passive pos =
+type passive_table = Equality.equality list * EqualitySet.t
+type active_table = Equality.equality list * Indexing.Index.t
+type new_proof = 
+  Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv
+type result =
+  | ParamodulationFailure of string * active_table * passive_table
+  | ParamodulationSuccess of new_proof * active_table * passive_table
+;;
+let make_passive eq_list =
   let set =
-    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty pos
+    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
   in
-  (*EqualitySet.elements*) pos, set
+  (*EqualitySet.elements set*) eq_list, set
+;;
+let make_empty_active () = [], Indexing.empty ;;
+let make_active eq_list = 
+  eq_list, List.fold_left Indexing.index Indexing.empty eq_list
 ;;
 
-let make_active () = [], Indexing.empty ;;
 let size_of_passive (passive_list, _) = List.length passive_list;;
 let size_of_active (active_list, _) = List.length active_list;;
 let passive_is_empty = function
@@ -256,12 +250,12 @@ let rec select env g passive =
 ;;
 
 
-let filter_dependent passive id =
+let filter_dependent bag passive id =
   let pos_list, pos_set = passive in
   let passive,no_pruned =
     List.fold_right
       (fun eq ((list,set),no) ->
-         if Equality.depend eq id then
+         if Equality.depend bag eq id then
            (list, EqualitySet.remove eq set), no + 1
          else 
            (eq::list, set), no)
@@ -288,7 +282,6 @@ let add_to_passive passive new_pos preferred =
       (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred)  
       pos 
   in
-  assert(pos_head = []);
   pos_head @ pos_list @ pos_tail, add pos_set pos
 ;;
 
@@ -350,30 +343,30 @@ let prune_passive howmany (active, _) passive =
 
 
 (** inference of new equalities between current and some in active *)
-let infer eq_uri env current (active_list, active_table) =
+let infer bag eq_uri env current (active_list, active_table) =
   let (_,c,_) = env in 
   if Utils.debug_metas then
-    (ignore(Indexing.check_target c current "infer1");
-     ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list)); 
+    (ignore(Indexing.check_target bag c current "infer1");
+     ignore(List.map (function current -> Indexing.check_target bag c current "infer2") active_list)); 
   let new_pos = 
-      let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
+      let maxm, copy_of_current = Equality.fix_metas bag !maxmeta current in
         maxmeta := maxm;
       let active_table =  Indexing.index active_table copy_of_current in
 (*       let _ = <:start<current contro active>> in *)
       let maxm, res =
-        Indexing.superposition_right eq_uri !maxmeta env active_table current 
+        Indexing.superposition_right bag eq_uri !maxmeta env active_table current 
       in
 (*       let _ = <:stop<current contro active>> in *)
       if Utils.debug_metas then
         ignore(List.map 
                  (function current -> 
-                    Indexing.check_target c current "sup0") res);
+                    Indexing.check_target bag c current "sup0") res);
       maxmeta := maxm;
       let rec infer_positive table = function
         | [] -> []
         | equality::tl ->
             let maxm, res =
-              Indexing.superposition_right 
+              Indexing.superposition_right bag 
                 ~subterms_only:true eq_uri !maxmeta env table equality 
             in
               maxmeta := maxm;
@@ -381,7 +374,7 @@ let infer eq_uri env current (active_list, active_table) =
                 ignore
                   (List.map 
                      (function current -> 
-                        Indexing.check_target c current "sup2") res);
+                        Indexing.check_target bag c current "sup2") res);
               let pos = infer_positive table tl in
               res @ pos
       in
@@ -396,7 +389,7 @@ let infer eq_uri env current (active_list, active_table) =
       if Utils.debug_metas then 
         ignore(List.map 
                  (function current -> 
-                    Indexing.check_target c current "sup3") pos);
+                    Indexing.check_target bag c current "sup3") pos);
       res @ pos
   in
   derived_clauses := !derived_clauses + (List.length new_pos);
@@ -444,22 +437,22 @@ let check_for_deep_subsumption env active_table eq =
 ;;
 
 (** simplifies current using active and passive *)
-let forward_simplify eq_uri env current (active_list, active_table) =
+let forward_simplify bag eq_uri env current (active_list, active_table) =
   let _, context, _ = env in
   let demodulate table current = 
     let newmeta, newcurrent =
-      Indexing.demodulation_equality eq_uri !maxmeta env table current
+      Indexing.demodulation_equality bag eq_uri !maxmeta env table current
     in
     maxmeta := newmeta;
     if Equality.is_identity env newcurrent then None else Some newcurrent
   in
   let rec demod current =
     if Utils.debug_metas then
-      ignore (Indexing.check_target context current "demod0");
+      ignore (Indexing.check_target bag context current "demod0");
     let res = demodulate active_table current in
       if Utils.debug_metas then
         ignore ((function None -> () | Some x -> 
-                   ignore (Indexing.check_target context x "demod1");()) res);
+                   ignore (Indexing.check_target bag context x "demod1");()) res);
     res
   in 
   let res = demod current in
@@ -475,18 +468,18 @@ let forward_simplify eq_uri env current (active_list, active_table) =
 ;;
 
 (** simplifies new using active and passive *)
-let forward_simplify_new eq_uri env new_pos active =
+let forward_simplify_new bag eq_uri env new_pos active =
   if Utils.debug_metas then
     begin
       let m,c,u = env in
         ignore(List.map 
-        (fun current -> Indexing.check_target c current "forward new pos") 
+        (fun current -> Indexing.check_target bag c current "forward new pos") 
       new_pos;)
     end;
   let active_list, active_table = active in
   let demodulate table target =
     let newmeta, newtarget =
-      Indexing.demodulation_equality eq_uri !maxmeta env table target 
+      Indexing.demodulation_equality bag eq_uri !maxmeta env table target 
     in
     maxmeta := newmeta;
     newtarget
@@ -510,27 +503,29 @@ let forward_simplify_new eq_uri env new_pos active =
 
 
 (** simplifies a goal with equalities in active and passive *)  
-let rec simplify_goal env goal (active_list, active_table) =
-  let demodulate table goal = Indexing.demodulation_goal env table goal in
+let rec simplify_goal bag env goal (active_list, active_table) =
+  let demodulate table goal = Indexing.demodulation_goal bag env table goal in
   let changed, goal = demodulate active_table goal in
   changed,
   if not changed then 
     goal 
   else 
-    snd (simplify_goal env goal (active_list, active_table)) 
+    snd (simplify_goal bag env goal (active_list, active_table)) 
 ;;
 
 
-let simplify_goals env goals active =
+let simplify_goals bag env goals active =
   let a_goals, p_goals = goals in
-  let p_goals = List.map (fun g -> snd (simplify_goal env g active)) p_goals in
-  let a_goals = List.map (fun g -> snd (simplify_goal env g active)) a_goals in
+  let p_goals = List.map (fun g -> snd (simplify_goal bag env g active)) p_goals in
+  let a_goals = List.map (fun g -> snd (simplify_goal bag env g active)) a_goals in
   a_goals, p_goals
 ;;
 
 
 (** simplifies active usign new *)
-let backward_simplify_active eq_uri env new_pos new_table min_weight active =
+let backward_simplify_active 
+  bag eq_uri env new_pos new_table min_weight active 
+=
   let active_list, active_table = active in
   let active_list, newa, pruned = 
     List.fold_right
@@ -540,7 +535,7 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active =
            equality::res, newn,pruned
          else
            match 
-             forward_simplify eq_uri env equality (new_pos, new_table) 
+             forward_simplify bag eq_uri env equality (new_pos, new_table) 
            with
            | None -> res, newn, id::pruned
            | Some e ->
@@ -580,7 +575,9 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active =
 
 
 (** simplifies passive using new *)
-let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
+let backward_simplify_passive 
+  bag eq_uri env new_pos new_table min_weight passive 
+=
   let (pl, ps), passive_table = passive in
   let f equality (resl, ress, newn) =
     let ew, _, _, _ , _ = Equality.open_equality equality in
@@ -588,7 +585,7 @@ let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
       equality::resl, ress, newn
     else
       match 
-        forward_simplify eq_uri env equality (new_pos, new_table) 
+        forward_simplify bag eq_uri env equality (new_pos, new_table) 
       with
       | None -> resl, EqualitySet.remove equality ress, newn
       | Some e ->
@@ -617,15 +614,15 @@ let build_table equations =
 ;;
   
 
-let backward_simplify eq_uri env new' active =
+let backward_simplify bag eq_uri env new' active =
   let new_pos, new_table, min_weight = build_table new' in
   let active, newa, pruned =
-    backward_simplify_active eq_uri env new_pos new_table min_weight active 
+    backward_simplify_active bag eq_uri env new_pos new_table min_weight active 
   in
-  active, newa, None, pruned
+  active, newa, pruned
 ;;
 
-let close eq_uri env new' given =
+let close bag eq_uri env new' given =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
@@ -635,7 +632,7 @@ let close eq_uri env new' given =
   in
   List.fold_left
     (fun p c ->
-       let pos = infer eq_uri env c (new_pos,new_table) in
+       let pos = infer bag eq_uri env c (new_pos,new_table) in
          pos@p)
     [] given 
 ;;
@@ -651,7 +648,7 @@ let is_commutative_law eq =
       | _ -> false
 ;;
 
-let prova eq_uri env new' active = 
+let prova bag eq_uri env new' active = 
   let given = List.filter is_commutative_law (fst active) in
   let _ =
     Utils.debug_print
@@ -661,7 +658,7 @@ let prova eq_uri env new' active =
                (List.map
                   (fun e -> Equality.string_of_equality ~env e)
                    given)))) in
-    close eq_uri env new' given
+    close bag eq_uri env new' given
 ;;
 
 (* returns an estimation of how many equalities in passive can be activated
@@ -710,7 +707,7 @@ let activate_theorem (active, passive) =
 
 
 
-let simplify_theorems env theorems ?passive (active_list, active_table) =
+let simplify_theorems bag env theorems ?passive (active_list, active_table) =
   let pl, passive_table =
     match passive with
     | None -> [], None
@@ -719,7 +716,7 @@ let simplify_theorems env theorems ?passive (active_list, active_table) =
   let a_theorems, p_theorems = theorems in
   let demodulate table theorem =
     let newmeta, newthm =
-      Indexing.demodulation_theorem !maxmeta env table theorem in
+      Indexing.demodulation_theorem bag !maxmeta env table theorem in
     maxmeta := newmeta;
     theorem != newthm, newthm
   in
@@ -741,20 +738,20 @@ let simplify_theorems env theorems ?passive (active_list, active_table) =
 ;;
 
 
-let rec simpl eq_uri env e others others_simpl =
+let rec simpl bag eq_uri env e others others_simpl =
   let active = others @ others_simpl in
   let tbl =
     List.fold_left
       (fun t e -> 
-        if Equality.is_weak_identity e then t else Indexing.index t e)
+         if Equality.is_weak_identity e then t else Indexing.index t e) 
       Indexing.empty active
   in
-  let res = forward_simplify eq_uri env e (active, tbl) in
+  let res = forward_simplify bag eq_uri env e (active, tbl) in
     match others with
       | hd::tl -> (
           match res with
-            | None -> simpl eq_uri env hd tl others_simpl
-            | Some e -> simpl eq_uri env hd tl (e::others_simpl)
+            | None -> simpl bag eq_uri env hd tl others_simpl
+            | Some e -> simpl bag eq_uri env hd tl (e::others_simpl)
         )
       | [] -> (
           match res with
@@ -763,7 +760,7 @@ let rec simpl eq_uri env e others others_simpl =
         )
 ;;
 
-let simplify_equalities eq_uri env equalities =
+let simplify_equalities bag eq_uri env equalities =
   Utils.debug_print
     (lazy 
        (Printf.sprintf "equalities:\n%s\n"
@@ -774,7 +771,7 @@ let simplify_equalities eq_uri env equalities =
     | [] -> []
     | hd::tl ->
         let res =
-          List.rev (simpl eq_uri env hd tl [])
+          List.rev (simpl bag eq_uri env hd tl [])
         in
           Utils.debug_print
             (lazy
@@ -807,13 +804,13 @@ let pp_goal_set msg goals names =
     passive_goals)))
 ;;
 
-let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
+let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
 (*   let names = Utils.names_of_context ctx in *)
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when LibraryObjects.is_eq_URI uri ->
       (let goal_equation = 
-         Equality.mk_equality
+         Equality.mk_equality bag
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 
       in
 (*      match Indexing.subsumption env table goal_equation with*)
@@ -830,7 +827,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
               if swapped then
-                Equality.symmetric eq_ty l id uri m
+                Equality.symmetric bag eq_ty l id uri m
               else
                 p
             in
@@ -866,7 +863,7 @@ let rec check goal = function
       | (Some p) as ok  -> ok
 ;;
   
-let simplify_goal_set env goals active = 
+let simplify_goal_set bag env goals active = 
   let active_goals, passive_goals = goals in 
   let find (_,_,g) where =
     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
@@ -877,7 +874,7 @@ let simplify_goal_set env goals active =
   in *)
     List.fold_left
       (fun (acc_a,acc_p) goal -> 
-        match simplify_goal env goal active with 
+        match simplify_goal bag env goal active with 
         | changed, g -> 
             if changed then 
               if find g acc_p then acc_a,acc_p else acc_a,g::acc_p
@@ -886,7 +883,7 @@ let simplify_goal_set env goals active =
       ([],passive_goals) active_goals
 ;;
 
-let check_if_goals_set_is_solved env active goals =
+let check_if_goals_set_is_solved bag env active goals =
   let active_goals, passive_goals = goals in
   List.fold_left 
     (fun proof goal ->
@@ -895,17 +892,17 @@ let check_if_goals_set_is_solved env active goals =
       | None -> 
           check goal [
             check_if_goal_is_identity env;
-            check_if_goal_is_subsumed env (snd active)])
+            check_if_goal_is_subsumed bag env (snd active)])
 (* provare active and passive?*)
     None active_goals
 ;;
 
-let infer_goal_set env active goals = 
+let infer_goal_set bag env active goals = 
   let active_goals, passive_goals = goals in
   let rec aux = function
     | [] -> active_goals, []
     | hd::tl ->
-        let changed,selected = simplify_goal env hd active in
+        let changed,selected = simplify_goal bag env hd active in
 (*
         if changed then
           prerr_endline ("--------------- goal semplificato");
@@ -923,7 +920,7 @@ let infer_goal_set env active goals =
               if Utils.metas_of_term t1 = [] then passive_goals
               else 
                 let newmaxmeta,new' = 
-                   Indexing.superposition_left env (snd active) selected
+                   Indexing.superposition_left bag env (snd active) selected
                    !maxmeta 
                 in
                 maxmeta := newmaxmeta;
@@ -934,15 +931,13 @@ let infer_goal_set env active goals =
   aux passive_goals
 ;;
 
-let infer_goal_set_with_current env current goals active = 
-  let active_goals, passive_goals = 
-    simplify_goal_set env goals active
-  in
+let infer_goal_set_with_current bag env current goals active = 
+  let active_goals, passive_goals = simplify_goal_set bag env goals active in
   let l,table,_  = build_table [current] in
   active_goals, 
   List.fold_left 
     (fun acc g ->
-      let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+      let newmaxmeta, new' = Indexing.superposition_left bag env table g !maxmeta in
       maxmeta := newmaxmeta;
       acc @ new')
     passive_goals active_goals
@@ -986,7 +981,8 @@ let print_status iterno goals active passive =
 (** given-clause algorithm with full reduction strategy: NEW implementation *)
 (* here goals is a set of goals in OR *)
 let given_clause 
-  eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
+  bag eq_uri ((_,context,_) as env) goals passive active 
+  goal_steps saturation_steps max_time
 = 
   let initial_time = Unix.gettimeofday () in
   let iterations_left iterno = 
@@ -999,19 +995,19 @@ let given_clause
     let iterations_left = time_left /. iteration_medium_cost in
     int_of_float iterations_left 
   in
-  let rec step goals theorems passive active iterno =
-    if iterno > max_iterations then
-      (ParamodulationFailure "No more iterations to spend")
+  let rec step goals passive active g_iterno s_iterno =
+    if g_iterno > goal_steps && s_iterno > saturation_steps then
+      (ParamodulationFailure ("No more iterations to spend",active,passive))
     else if Unix.gettimeofday () > max_time then
-      (ParamodulationFailure "No more time to spend")
+      (ParamodulationFailure ("No more time to spend",active,passive))
     else
       let _ = 
-(*         print_status iterno goals active passive  *)
-        Printf.eprintf ".%!";
+         print_status (max g_iterno s_iterno) goals active passive  
+(*         Printf.eprintf ".%!"; *)
       in
       (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) 
       let passive =
-        let selection_estimate = iterations_left iterno in
+        let selection_estimate = iterations_left (max g_iterno s_iterno) in
         let kept = size_of_passive passive in
         if kept > selection_estimate then 
           begin
@@ -1022,49 +1018,55 @@ let given_clause
           passive
       in
       kept_clauses := (size_of_passive passive) + (size_of_active active);
-      let goals = infer_goal_set env active goals 
+      let goals = 
+        if g_iterno < goal_steps then
+          infer_goal_set bag env active goals 
+        else
+          goals
       in
-      match check_if_goals_set_is_solved env active goals with
+      match check_if_goals_set_is_solved bag env active goals with
       | Some p -> 
           prerr_endline 
             (Printf.sprintf "\nFound a proof in: %f\n" 
               (Unix.gettimeofday() -. initial_time));
-          ParamodulationSuccess p
+          ParamodulationSuccess (p,active,passive)
       | None -> 
           (* SELECTION *)
           if passive_is_empty passive then
             if no_more_passive_goals goals then 
-              ParamodulationFailure "No more passive equations/goals"
+              ParamodulationFailure 
+                ("No more passive equations/goals",active,passive)
               (*maybe this is a success! *)
             else
-              step goals theorems passive active (iterno+1)
+              step goals passive active (g_iterno+1) (s_iterno+1)
           else
             begin
               (* COLLECTION OF GARBAGED EQUALITIES *)
-              if iterno mod 40 = 0 then
+              if max g_iterno s_iterno mod 40 = 0 then
                 begin
-                  print_status iterno goals active passive;
+                  print_status (max g_iterno s_iterno) goals active passive;
                   let active = List.map Equality.id_of (fst active) in
                   let passive = List.map Equality.id_of (fst passive) in
                   let goal = ids_of_goal_set goals in
-                  Equality.collect active passive goal
+                  Equality.collect bag active passive goal
                 end;
-              let current, passive = select env goals passive in
-              (* SIMPLIFICATION OF CURRENT *)
-(*
-              prerr_endline
-                    ("Selected : " ^ 
-                      Equality.string_of_equality ~env  current);
-*)
-              let res = 
-                forward_simplify eq_uri env current active 
+              let res, passive = 
+                if s_iterno < saturation_steps then
+                  let current, passive = select env goals passive in
+                  (* SIMPLIFICATION OF CURRENT *)
+                  prerr_endline
+                        ("Selected : " ^ 
+                          Equality.string_of_equality ~env  current);
+                  forward_simplify bag eq_uri env current active, passive
+                else
+                  None, passive
               in
               match res with
-              | None -> step goals theorems passive active (iterno+1)
+              | None -> step goals passive active (g_iterno+1) (s_iterno+1)
               | Some current ->
                   (* GENERATION OF NEW EQUATIONS *)
 (*                   prerr_endline "infer"; *)
-                  let new' = infer eq_uri env current active in
+                  let new' = infer bag eq_uri env current active in
 (*                   prerr_endline "infer goal"; *)
 (*
       match check_if_goals_set_is_solved env active goals with
@@ -1080,59 +1082,56 @@ let given_clause
                       al @ [current], Indexing.index tbl current
                   in
                   let goals = 
-                    infer_goal_set_with_current env current goals active 
+                    infer_goal_set_with_current bag env current goals active 
                   in
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
 (*                   prerr_endline "fwd/back simpl"; *)
-                  let rec simplify new' active passive head =
+                  let rec simplify new' active passive =
                     let new' = 
-                      forward_simplify_new eq_uri env new' active 
+                      forward_simplify_new bag eq_uri env new' active 
                     in
-                    let active, newa, retained, pruned =
-                      backward_simplify eq_uri env new' active 
+                    let active, newa, pruned =
+                      backward_simplify bag eq_uri env new' active 
                     in
                     let passive = 
-                      List.fold_left filter_dependent passive pruned 
+                      List.fold_left (filter_dependent bag) passive pruned 
                     in
-                    match newa, retained with
-                    | None, None -> active, passive, new', head
-                    | Some p, None 
-                    | None, Some p -> simplify (new' @ p) active passive head
-                    | Some p, Some rp -> 
-                        simplify (new' @ p @ rp) active passive (head @ p)
+                    match newa with
+                    | None -> active, passive, new'
+                    | Some p -> simplify (new' @ p) active passive 
                   in
-                  let active, passive, new', head = 
-                    simplify new' active passive []
+                  let active, passive, new' = 
+                    simplify new' active passive
                   in
 (*                   prerr_endline "simpl goal with new"; *)
                   let goals = 
                     let a,b,_ = build_table new' in
 (*                     let _ = <:start<simplify_goal_set new>> in *)
-                    let rc = simplify_goal_set env goals (a,b) in
+                    let rc = simplify_goal_set bag env goals (a,b) in
 (*                     let _ = <:stop<simplify_goal_set new>> in *)
                     rc
                   in
-                  let passive = add_to_passive passive new' head in
-                  step goals theorems passive active (iterno+1)
+                  let passive = add_to_passive passive new' [] in
+                  step goals passive active (g_iterno+1) (s_iterno+1)
             end
   in
-    step goals theorems passive active 1
+    step goals passive active 1 1
 ;;
 
-let rec saturate_equations eq_uri env goal accept_fun passive active =
+let rec saturate_equations bag eq_uri env goal accept_fun passive active =
   elapsed_time := Unix.gettimeofday () -. !start_time;
   if !elapsed_time > !time_limit then
     (active, passive)
   else
     let current, passive = select env ([goal],[]) passive in
-    let res = forward_simplify eq_uri env current active in
+    let res = forward_simplify bag eq_uri env current active in
     match res with
     | None ->
-        saturate_equations eq_uri env goal accept_fun passive active
+        saturate_equations bag eq_uri env goal accept_fun passive active
     | Some current ->
         Utils.debug_print (lazy (Printf.sprintf "selected: %s"
                              (Equality.string_of_equality ~env current)));
-        let new' = infer eq_uri env current active in
+        let new' = infer bag eq_uri env current active in
         let active =
           if Equality.is_identity env current then active
           else
@@ -1142,16 +1141,14 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
         (* alla fine new' contiene anche le attive semplificate!
          * quindi le aggiungo alle passive insieme alle new *)
         let rec simplify new' active passive =
-          let new' = forward_simplify_new eq_uri env new' active in
-          let active, newa, retained, pruned =
-            backward_simplify eq_uri env new' active in
+          let new' = forward_simplify_new bag eq_uri env new' active in
+          let active, newa, pruned =
+            backward_simplify bag eq_uri env new' active in
           let passive = 
-            List.fold_left filter_dependent passive pruned in
-          match newa, retained with
-          | None, None -> active, passive, new'
-          | Some p, None
-          | None, Some p -> simplify (new' @ p) active passive
-          | Some p, Some rp -> simplify (new' @ p @ rp) active passive
+            List.fold_left (filter_dependent bag) passive pruned in
+          match newa with
+          | None -> active, passive, new'
+          | Some p -> simplify (new' @ p) active passive
         in
         let active, passive, new' = simplify new' active passive in
         let _ =
@@ -1174,7 +1171,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
         in
         let new' = List.filter accept_fun new' in
         let passive = add_to_passive passive new' [] in
-        saturate_equations eq_uri env goal accept_fun passive active
+        saturate_equations bag eq_uri env goal accept_fun passive active
 ;;
   
 let default_depth = !maxdepth
@@ -1195,7 +1192,6 @@ let reset_refs () =
   passive_maintainance_time := 0.;
   derived_clauses := 0;
   kept_clauses := 0;
-  Equality.reset ();
 ;;
 
 let eq_of_goal = function
@@ -1210,102 +1206,26 @@ let eq_and_ty_of_goal = function
   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
 ;;
 
-let saturate 
-    caso_strano 
-    dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) 
-    ?(timeout=600.) ?auto status = 
-  let module C = Cic in
-  reset_refs ();
-  Indexing.init_index ();
-  maxdepth := depth;
-  maxwidth := width;
-(*  CicUnification.unif_ty := false;*)
+(* status: input proof status
+ * goalproof: forward steps on goal
+ * newproof: backward steps
+ * subsumption_id: the equation used if goal is closed by subsumption
+ *   (0 if not closed by subsumption) (DEBUGGING: can be safely removed)
+ * subsumption_subst: subst to make newproof and goalproof match
+ * proof_menv: final metasenv
+ *)
+let build_proof 
+  bag status  
+  goalproof newproof subsumption_id subsumption_subst proof_menv
+=
   let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
-  let cleaned_goal = Utils.remove_local_context type_of_goal in
-  Utils.set_goal_symbols cleaned_goal;
-  let names = Utils.names_of_context context in
-  let eq_indexes, equalities, maxm, universe, cache = 
-    Inference.find_equalities ?auto context proof AutoTypes.cache_empty
-  in
-  prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
-  List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
-  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
-  let ugraph = CicUniv.empty_ugraph in
-  let env = (metasenv, context, ugraph) in 
-  let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
-  let res, time =
-    let t1 = Unix.gettimeofday () in
-    let lib_eq_uris, library_equalities, maxm, universe, cache =
-      Inference.find_library_equalities 
-        ?auto caso_strano dbd context (proof, goalno) (maxm+2)
-        ?universe cache
-    in
-    prerr_endline ">>>>>>>>>>  gained from the library >>>>>>>>>>>>";
-    List.iter
-      (fun (_,e) -> prerr_endline (Equality.string_of_equality e)) 
-      library_equalities;
-    prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
-    let library_equalities = List.map snd library_equalities in
-    let t2 = Unix.gettimeofday () in
-    maxmeta := maxm+2;
-    let equalities = 
-      simplify_equalities eq_uri env (equalities@library_equalities) 
-    in 
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
-    let t1 = Unix.gettimeofday () in
-    let theorems =
-      let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
-      let t = CicUtil.term_of_uri refl_equal in
-      let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-      [(t, ty, [])], []
-    in
-    let t2 = Unix.gettimeofday () in
-    let _ =
-      Utils.debug_print
-        (lazy
-           (Printf.sprintf
-              "Theorems:\n-------------------------------------\n%s\n"
-              (String.concat "\n"
-                 (List.map
-                    (fun (t, ty, _) ->
-                       Printf.sprintf
-                         "Term: %s, type: %s"
-                         (CicPp.ppterm t) (CicPp.ppterm ty))
-                    (fst theorems)))));
-      Utils.debug_print
-        (lazy
-           (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
-    in
-    let active = make_active () in
-    let passive = make_passive equalities in
-    let start = Unix.gettimeofday () in
-    let res =
-(*
-      let goals = make_goals goal in
-      given_clause_fullred dbd env goals theorems passive active
-*)
-      let goals = make_goal_set goal in
-      let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  timeout (* minutes *) in
-      given_clause 
-        eq_uri env goals theorems passive active max_iterations max_time 
-    in
-    let finish = Unix.gettimeofday () in
-    (res, finish -. start)
-  in
-  match res with
-  | ParamodulationFailure s ->
-      raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
-  | ParamodulationSuccess 
-    (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
+      let names = Utils.names_of_context context in
       prerr_endline "Proof:";
       prerr_endline 
-        (Equality.pp_proof names goalproof newproof subsumption_subst
+        (Equality.pp_proof bag names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
 (*       prerr_endline "ENDOFPROOFS"; *)
 (*
@@ -1320,7 +1240,7 @@ let saturate
       in
       let goal_proof, side_effects_t = 
         let initial = Equality.add_subst subsumption_subst newproof in
-        Equality.build_goal_proof 
+        Equality.build_goal_proof bag
           eq_uri goalproof initial type_of_goal side_effects
           context proof_menv
       in
@@ -1341,7 +1261,8 @@ let saturate
           (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> 
              match uniq with
                | Some m -> 
-                   acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq
+(*                    acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *)
+                   (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl))::acc3, uniq
                | None ->
                    [i,context,ty], (Cic.Meta(i,[]))::acc2, 
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
@@ -1381,6 +1302,12 @@ let saturate
         let free_metas_menv = 
           List.map (fun i -> CicUtil.lookup_meta i goal_proof_menv) free_metas
         in
+(*
+        prerr_endline ("XX type_of_goal  " ^ CicPp.ppterm type_of_goal);
+        prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal);
+        prerr_endline ("XX metasenv      " ^ 
+        CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv));
+*)
         try
           CicUnification.fo_unif_subst [] context (metasenv @ free_metas_menv)
            replaced_goal type_of_goal CicUniv.empty_ugraph
@@ -1422,192 +1349,192 @@ let saturate
           (CicMetaSubst.ppmetasenv [] metasenv)
           (CicMetaSubst.ppmetasenv [] real_metasenv);
 *)
-      prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
-      proof, open_goals
+      final_subst, proof, open_goals
 ;;
 
-let main _ _ _ _ _ = () ;;
-
-let retrieve_and_print dbd term metasenv ugraph = 
-  let module C = Cic in
-  let module T = CicTypeChecker in
-  let module PET = ProofEngineTypes in
-  let module PP = CicPp in
-  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
-  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
-  let proof, goals = status in
-  let goal' = List.nth goals 0 in
-  let uri, metasenv, meta_proof, term_to_prove = proof in
-  let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
+let find_equalities dbd status smart_flag ?auto cache =
+  let proof, goalno = status in
+  let _, metasenv,_,_ = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
-  let eq_indexes, equalities, maxm,universe,cache = 
-    Inference.find_equalities context proof AutoTypes.cache_empty in
-  let ugraph = CicUniv.empty_ugraph in
-  let env = (metasenv, context, ugraph) in
-  let t1 = Unix.gettimeofday () in
-  let lib_eq_uris, library_equalities, maxm, unvierse, cache =
-    Inference.find_library_equalities 
-      false dbd context (proof, goal') (maxm+2) ?universe cache
-  in 
-  let t2 = Unix.gettimeofday () in
-  maxmeta := maxm+2;
-  let equalities = (* equalities @ *) library_equalities in
-  Utils.debug_print
-     (lazy
-        (Printf.sprintf "\n\nequalities:\n%s\n"
-           (String.concat "\n"
-              (List.map 
-          (fun (u, e) ->
-(*                  Printf.sprintf "%s: %s" *)
-                   (UriManager.string_of_uri u)
-(*                    (string_of_equality e) *)
-                     )
-          equalities))));
-  Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
-  let rec simpl e others others_simpl =
-    let (u, e) = e in
-    let active = (others @ others_simpl) in
-    let tbl =
-      List.fold_left
-        (fun t (_, e) -> Indexing.index t e)
-        Indexing.empty active
-    in
-    let res = forward_simplify eq_uri env e (active, tbl) in
-    match others with
-        | hd::tl -> (
-            match res with
-              | None -> simpl hd tl others_simpl
-              | Some e -> simpl hd tl ((u, e)::others_simpl)
-          )
-        | [] -> (
-            match res with
-              | None -> others_simpl
-              | Some e -> (u, e)::others_simpl
-          ) 
+  let env = (metasenv, context, CicUniv.empty_ugraph) in 
+  let bag = Equality.mk_equality_bag () in
+  let eq_indexes, equalities, maxm, cache = 
+    Inference.find_equalities 0 bag ?auto context proof cache
   in
-  let _equalities =
-    match equalities with
-      | [] -> []
-      | hd::tl ->
-          let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
-          let res =
-            List.rev (simpl (*(Positive,*) hd others [])
-          in
-            Utils.debug_print
-              (lazy
-                 (Printf.sprintf "\nequalities AFTER:\n%s\n"
-                    (String.concat "\n"
-                       (List.map
-                          (fun (u, e) ->
-                             Printf.sprintf "%s: %s"
-                               (UriManager.string_of_uri u)
-                               (Equality.string_of_equality e)
-                          )
-                          res))));
-            res in
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+  prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
+  List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
+  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+  let lib_eq_uris, library_equalities, maxm, cache =
+    Inference.find_library_equalities bag
+      ?auto smart_flag dbd context (proof, goalno) (maxm+2)
+      cache
+  in
+  prerr_endline (">>>>>>>>>>  gained from the library >>>>>>>>>>>>" ^
+    string_of_int maxm);
+  List.iter
+    (fun (_,e) -> prerr_endline (Equality.string_of_equality e)) 
+    library_equalities;
+  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+  let equalities = List.map snd library_equalities @ equalities in
+  let equalities = 
+    simplify_equalities bag eq_uri env equalities
+  in 
+  prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
+  List.iter
+    (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
+  prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
+  bag, equalities, cache, maxm
 ;;
 
+let saturate_more bag active maxmeta status smart_flag ?auto cache =
+  let proof, goalno = status in
+  let _, metasenv,_,_ = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri = eq_of_goal type_of_goal in 
+  let env = (metasenv, context, CicUniv.empty_ugraph) in 
+  let eq_indexes, equalities, maxm, cache = 
+    Inference.find_equalities maxmeta bag ?auto context proof cache
+  in
+  let equalities = 
+(*
+    HExtlib.filter_map 
+      (fun e -> forward_simplify bag eq_uri env e active)
+*)
+    equalities
+  in
+  bag, equalities, cache, maxm
 
-let main_demod_equalities dbd term metasenv ugraph =
+let saturate 
+    smart_flag 
+    dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) 
+    ?(timeout=600.) ?auto status = 
   let module C = Cic in
-  let module T = CicTypeChecker in
-  let module PET = ProofEngineTypes in
-  let module PP = CicPp in
-  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
-  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
-  let proof, goals = status in
-  let goal' = List.nth goals 0 in
-  let _, metasenv, meta_proof, _ = proof in
-  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
-  let eq_uri = eq_of_goal goal in 
-  let eq_indexes, equalities, maxm, universe, cache = 
-    Inference.find_equalities context proof AutoTypes.cache_empty in
-  let lib_eq_uris, library_equalities, maxm,universe,cache =
-    Inference.find_library_equalities 
-      false dbd context (proof, goal') (maxm+2) ?universe cache
-  in
-  let library_equalities = List.map snd library_equalities in
-  maxmeta := maxm+2; (* TODO ugly!! *)
-  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let new_meta_goal, metasenv, type_of_goal =
-    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
-            (CicPp.ppterm ty)));
-    Cic.Meta (maxm+1, irl),
-    (maxm+1, context, ty)::metasenv,
-    ty
+  reset_refs ();
+  maxdepth := depth;
+  maxwidth := width;
+(*  CicUnification.unif_ty := false;*)
+  let proof, goalno = status in
+  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri = eq_of_goal type_of_goal in 
+  let cleaned_goal = Utils.remove_local_context type_of_goal in
+  Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
+  let ugraph = CicUniv.empty_ugraph in
+  let env = (metasenv, context, ugraph) in 
+  let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
+  let bag, equalities, cache, maxm = 
+    find_equalities dbd status smart_flag ?auto AutoTypes.cache_empty 
   in
-  let env = (metasenv, context, ugraph) in
-  (*try*)
-    let goal = [], [], goal 
+  let res, time =
+    maxmeta := maxm+2;
+    let t1 = Unix.gettimeofday () in
+    let theorems =
+      let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
+      let t = CicUtil.term_of_uri refl_equal in
+      let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+      [(t, ty, [])], []
     in
-    let equalities = 
-      simplify_equalities eq_uri env (equalities@library_equalities) 
+    let t2 = Unix.gettimeofday () in
+    let _ =
+      Utils.debug_print
+        (lazy
+           (Printf.sprintf
+              "Theorems:\n-------------------------------------\n%s\n"
+              (String.concat "\n"
+                 (List.map
+                    (fun (t, ty, _) ->
+                       Printf.sprintf
+                         "Term: %s, type: %s"
+                         (CicPp.ppterm t) (CicPp.ppterm ty))
+                    (fst theorems)))));
+      Utils.debug_print
+        (lazy
+           (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
     in
-    let active = make_active () in
+    let active = make_empty_active () in
     let passive = make_passive equalities in
-    Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
-    Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
-    Printf.eprintf "\nequalities:\n%s\n"
-      (String.concat "\n"
-         (List.map
-            (Equality.string_of_equality ~env) equalities));
-    prerr_endline "--------------------------------------------------";
-    prerr_endline "GO!";
-    start_time := Unix.gettimeofday ();
-    if !time_limit < 1. then time_limit := 60.;    
-    let ra, rp =
-      saturate_equations eq_uri env goal (fun e -> true) passive active
-    in
-
-    let initial =
-      List.fold_left (fun s e -> EqualitySet.add e s)
-        EqualitySet.empty equalities
+    let start = Unix.gettimeofday () in
+    let res =
+(*
+      let goals = make_goals goal in
+      given_clause_fullred dbd env goals theorems passive active
+*)
+      let goals = make_goal_set goal in
+      let max_iterations = 10000 in
+      let max_time = Unix.gettimeofday () +.  timeout (* minutes *) in
+      given_clause bag
+        eq_uri env goals passive active max_iterations max_iterations max_time 
     in
-    let addfun s e = 
-      if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+    let finish = Unix.gettimeofday () in
+    (res, finish -. start)
+  in
+  match res with
+  | ParamodulationFailure (s,_,_) ->
+      raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
+  | ParamodulationSuccess 
+    ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),_,_) ->
+      prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
+    let _,p,gl = 
+      build_proof bag
+        status goalproof newproof subsumption_id subsumption_subst proof_menv
     in
+    p,gl
+;;
+(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
 
-    let passive =
-      match rp with
-      | p, _ ->
-          EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
-    in
-    let active =
-      let l = fst ra in
-      EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+(* exported version of given_clause *)
+let given_clause 
+  bag maxm status active passive goal_steps saturation_steps max_time 
+=
+  reset_refs();
+  maxmeta := maxm;
+  let max_l l = 
+    List.fold_left 
+     (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
+      List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
+     0 l
+  in
+  let active_l = fst active in
+  let passive_l = fst passive in
+  let ma = max_l active_l in
+  let mp = max_l passive_l in
+  assert (maxm > max ma mp);
+  let proof, goalno = status in
+  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri = eq_of_goal type_of_goal in 
+  let cleaned_goal = Utils.remove_local_context type_of_goal in
+  Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
+  let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
+  let env = metasenv,context,CicUniv.empty_ugraph in
+  let goals = make_goal_set goal in
+  match 
+    given_clause bag eq_uri env goals passive active 
+      goal_steps saturation_steps max_time
+  with
+  | ParamodulationFailure (_,a,p) ->
+      None, a, p, !maxmeta
+  | ParamodulationSuccess 
+    ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p) ->
+    let subst, proof, gl =
+      build_proof bag
+        status goalproof newproof subsumption_id subsumption_subst proof_menv
     in
-    Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
-       (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) 
-     (*  (String.concat "\n"
-         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
-(*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
-      (String.concat "\n"
-         (List.map 
-           (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e)) 
-          passive));
-    print_newline ();
-(*
-  with e ->
-    Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
-*)
+    Some (subst, proof,gl),a,p, !maxmeta
 ;;
 
 let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let eq_uri = eq_of_goal ty in 
-  let eq_indexes, equalities, maxm, universe, cache = 
-    Inference.find_equalities context proof AutoTypes.cache_empty
+  let eq_uri = eq_of_goal ty in
+  let bag = Equality.mk_equality_bag () in
+  let eq_indexes, equalities, maxm, cache = 
+    Inference.find_equalities 0 bag context proof AutoTypes.cache_empty
   in
-  let lib_eq_uris, library_equalities, maxm, universe, cache =
-    Inference.find_library_equalities 
-      false dbd context (proof, goal) (maxm+2) ?universe cache 
+  let lib_eq_uris, library_equalities, maxm, cache =
+    Inference.find_library_equalities bag 
+      false dbd context (proof, goal) (maxm+2)  cache 
   in
   if library_equalities = [] then prerr_endline "VUOTA!!!";
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
@@ -1615,7 +1542,7 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
   let initgoal = [], [], ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let equalities = 
-    simplify_equalities eq_uri env (equalities@library_equalities) 
+    simplify_equalities bag eq_uri env (equalities@library_equalities) 
   in   
   let table = 
     List.fold_left 
@@ -1623,14 +1550,14 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
       Indexing.empty equalities 
   in
   let changed,(newproof,newmetasenv, newty) = 
-    Indexing.demodulation_goal 
+    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 
+        Equality.build_goal_proof bag
           eq_uri newproof opengoal ty [] context metasenv
       in
         let extended_metasenv = (maxm,context,newty)::metasenv in
@@ -1676,15 +1603,15 @@ let rec position_of i x = function
 
 let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   reset_refs();
-  Indexing.init_index ();
   let proof,goalno = status in 
   let curi,metasenv,pbo,pty = 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 eq_index, equalities, maxm,universe,cache  = 
-    Inference.find_equalities context proof AutoTypes.cache_empty 
+  let bag = Equality.mk_equality_bag () in
+  let eq_index, equalities, maxm,cache  = 
+    Inference.find_equalities 0 bag context proof AutoTypes.cache_empty 
   in
   let eq_what = 
     let what = find_in_ctx 1 target context in
@@ -1705,7 +1632,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   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 
+    Indexing.superposition_right bag
       ~subterms_only eq_uri maxm env index eq_what
   in
   prerr_endline ("Superposition right:");
@@ -1725,7 +1652,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
     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 eq_uri [] 0 p) names)) eql;
+    CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
   if demod_table <> "" then
     begin
       let eql = 
@@ -1745,7 +1672,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
         List.fold_left 
           (fun (maxm,acc) e -> 
             let maxm,eq = 
-              Indexing.demodulation_equality eq_uri maxm env table e
+              Indexing.demodulation_equality bag eq_uri maxm env table e
             in
             maxm,eq::acc) 
           (maxm,[]) eql
@@ -1771,3 +1698,186 @@ let get_stats () = ""
 ;;
 *)
 
+(* THINGS USED ONLY BY saturate_main.ml *)
+
+let main _ _ _ _ _ = () ;;
+
+let retrieve_and_print dbd term metasenv ugraph = 
+  let module C = Cic in
+  let module T = CicTypeChecker in
+  let module PET = ProofEngineTypes in
+  let module PP = CicPp in
+  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+  let proof, goals = status in
+  let goal' = List.nth goals 0 in
+  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
+  let eq_uri = eq_of_goal type_of_goal in
+  let bag = Equality.mk_equality_bag () in
+  let eq_indexes, equalities, maxm,cache = 
+    Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in
+  let ugraph = CicUniv.empty_ugraph in
+  let env = (metasenv, context, ugraph) in
+  let t1 = Unix.gettimeofday () in
+  let lib_eq_uris, library_equalities, maxm, cache =
+    Inference.find_library_equalities bag
+      false dbd context (proof, goal') (maxm+2)  cache
+  in 
+  let t2 = Unix.gettimeofday () in
+  maxmeta := maxm+2;
+  let equalities = (* equalities @ *) library_equalities in
+  Utils.debug_print
+     (lazy
+        (Printf.sprintf "\n\nequalities:\n%s\n"
+           (String.concat "\n"
+              (List.map 
+          (fun (u, e) ->
+(*                  Printf.sprintf "%s: %s" *)
+                   (UriManager.string_of_uri u)
+(*                    (string_of_equality e) *)
+                     )
+          equalities))));
+  Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
+  let rec simpl e others others_simpl =
+    let (u, e) = e in
+    let active = (others @ others_simpl) in
+    let tbl =
+      List.fold_left
+        (fun t (_, e) -> Indexing.index t e)
+        Indexing.empty active
+    in
+    let res = forward_simplify bag eq_uri env e (active, tbl) in
+    match others with
+        | hd::tl -> (
+            match res with
+              | None -> simpl hd tl others_simpl
+              | Some e -> simpl hd tl ((u, e)::others_simpl)
+          )
+        | [] -> (
+            match res with
+              | None -> others_simpl
+              | Some e -> (u, e)::others_simpl
+          ) 
+  in
+  let _equalities =
+    match equalities with
+      | [] -> []
+      | hd::tl ->
+          let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
+          let res =
+            List.rev (simpl (*(Positive,*) hd others [])
+          in
+            Utils.debug_print
+              (lazy
+                 (Printf.sprintf "\nequalities AFTER:\n%s\n"
+                    (String.concat "\n"
+                       (List.map
+                          (fun (u, e) ->
+                             Printf.sprintf "%s: %s"
+                               (UriManager.string_of_uri u)
+                               (Equality.string_of_equality e)
+                          )
+                          res))));
+            res in
+    Utils.debug_print
+      (lazy
+         (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+;;
+
+
+let main_demod_equalities dbd term metasenv ugraph =
+  let module C = Cic in
+  let module T = CicTypeChecker in
+  let module PET = ProofEngineTypes in
+  let module PP = CicPp in
+  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+  let proof, goals = status in
+  let goal' = List.nth goals 0 in
+  let _, metasenv, meta_proof, _ = proof in
+  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+  let eq_uri = eq_of_goal goal in 
+  let bag = Equality.mk_equality_bag () in
+  let eq_indexes, equalities, maxm,  cache = 
+    Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in
+  let lib_eq_uris, library_equalities, maxm,cache =
+    Inference.find_library_equalities bag
+      false dbd context (proof, goal') (maxm+2)  cache
+  in
+  let library_equalities = List.map snd library_equalities in
+  maxmeta := maxm+2; (* TODO ugly!! *)
+  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+  let new_meta_goal, metasenv, type_of_goal =
+    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+    Utils.debug_print
+      (lazy
+         (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
+            (CicPp.ppterm ty)));
+    Cic.Meta (maxm+1, irl),
+    (maxm+1, context, ty)::metasenv,
+    ty
+  in
+  let env = (metasenv, context, ugraph) in
+  (*try*)
+    let goal = [], [], goal 
+    in
+    let equalities = 
+      simplify_equalities bag eq_uri env (equalities@library_equalities) 
+    in
+    let active = make_empty_active () in
+    let passive = make_passive equalities in
+    Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
+    Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
+    Printf.eprintf "\nequalities:\n%s\n"
+      (String.concat "\n"
+         (List.map
+            (Equality.string_of_equality ~env) equalities));
+    prerr_endline "--------------------------------------------------";
+    prerr_endline "GO!";
+    start_time := Unix.gettimeofday ();
+    if !time_limit < 1. then time_limit := 60.;    
+    let ra, rp =
+      saturate_equations bag eq_uri env goal (fun e -> true) passive active
+    in
+
+    let initial =
+      List.fold_left (fun s e -> EqualitySet.add e s)
+        EqualitySet.empty equalities
+    in
+    let addfun s e = 
+      if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+    in
+
+    let passive =
+      match rp with
+      | p, _ ->
+          EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
+    in
+    let active =
+      let l = fst ra in
+      EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+    in
+    Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+       (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) 
+     (*  (String.concat "\n"
+         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
+(*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
+      (String.concat "\n"
+         (List.map 
+           (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e)) 
+          passive));
+    print_newline ();
+(*
+  with e ->
+    Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
+*)
+;;
+let saturate_equations eq_uri env goal accept_fun passive active =
+  let bag = Equality.mk_equality_bag () in
+  saturate_equations bag eq_uri env goal accept_fun passive active
+;;
+
+let add_to_passive eql passives = 
+  add_to_passive passives eql eql
+;;
index abf8808ca5d4aa42e8d427ca9531856ad5188ca7..3bd04454c2e5ad2d25817b4775bd9d05c4645578 100644 (file)
 
 (* $Id$ *)
 
-
-val saturate :
+val saturate : (* FIXME: should be exported a a tactic *)
   bool ->
   HMysql.dbd ->
   ?full:bool ->
   ?depth:int ->
   ?width:int ->
   ?timeout:float ->
-  ?auto:(AutoTypes.flags -> ProofEngineTypes.proof -> Cic.context -> 
-    ?universe:AutoTypes.universe ->
-    AutoTypes.cache -> ProofEngineTypes.goal list ->
-    Cic.substitution list * AutoTypes.cache * AutoTypes.universe) ->
-  ProofEngineTypes.proof * ProofEngineTypes.goal ->
+  ?auto:Inference.auto_type ->
+  ProofEngineTypes.status ->
   ProofEngineTypes.proof * ProofEngineTypes.goal list
 
+type active_table 
+type passive_table 
+val make_active: Equality.equality list -> active_table
+val make_passive: Equality.equality list -> passive_table
+val add_to_passive: Equality.equality list -> passive_table -> passive_table
+
+val find_equalities:
+  HMysql.dbd ->
+  ProofEngineTypes.status ->
+  bool -> (* smart_flag *)
+  ?auto:Inference.auto_type -> 
+  AutoTypes.cache ->
+  Equality.equality_bag *
+    Equality.equality list * AutoTypes.cache * int
+val saturate_more: 
+  Equality.equality_bag ->
+  active_table ->
+  int -> (* maxmeta *)
+  ProofEngineTypes.status ->
+  bool -> (* smart flag *)
+  ?auto:Inference.auto_type ->
+  AutoTypes.cache ->
+    Equality.equality_bag * Equality.equality list * AutoTypes.cache * int
+
+val given_clause: 
+  Equality.equality_bag ->
+  int -> (* maxmeta *)
+  ProofEngineTypes.status ->
+  active_table ->
+  passive_table -> 
+  int -> int -> float -> 
+    (Cic.substitution * 
+     ProofEngineTypes.proof * 
+     ProofEngineTypes.goal list) option * 
+    active_table * passive_table * int
+
+val demodulate_tac: dbd:HMysql.dbd ->  ProofEngineTypes.tactic
+
+val superposition_tac: 
+  target:string -> table:string -> subterms_only:bool ->
+  demod_table:string ->  ProofEngineTypes.proof * ProofEngineTypes.goal ->
+   ProofEngineTypes.proof * ProofEngineTypes.goal list
+
+val get_stats: unit -> string
+  
+(* this is used only in saturate_main: MUST BE REMOVED!  *)
 val weight_age_ratio : int ref
 val weight_age_counter: int ref
 val symbols_ratio: int ref
@@ -48,16 +90,10 @@ val use_fullred: bool ref
 val time_limit: float ref
 val maxwidth: int ref
 val maxdepth: int ref
-val retrieve_and_print: HMysql.dbd -> Cic.term -> Cic.conjecture list -> 'a -> unit
+val retrieve_and_print: 
+  HMysql.dbd -> Cic.term -> Cic.conjecture list -> 'a -> unit
 val main_demod_equalities: HMysql.dbd ->
     Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
 val main: HMysql.dbd ->
     bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
-val demodulate_tac: dbd:HMysql.dbd ->  ProofEngineTypes.tactic
-
-val superposition_tac: 
-  target:string -> table:string -> subterms_only:bool ->
-  demod_table:string ->  ProofEngineTypes.proof * ProofEngineTypes.goal ->
-   ProofEngineTypes.proof * ProofEngineTypes.goal list
-
-val get_stats: unit -> string
+(* eof *)
index eabf24353395f443beea557563d0daa4a4a7273c..6ac2132aaa8f203a945982c3f4ecb913868199f9 100644 (file)
@@ -356,7 +356,7 @@ let compute_equality_weight e =
    d
   );
 *)
-  w + d
+  w + d 
 ;;
 
 (* old
index 1398424353462320e130403a5bbc0a325d4d8e6b..16cff94d7796493f52a05658332a8261f564be4f 100644 (file)
@@ -246,14 +246,14 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_with_subst ~term ~subst (proof, goal) =
+let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let newmeta = CicMkImplicit.new_meta metasenv subst in
+  let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
        C.Var (uri,exp_named_subst) ->
@@ -321,16 +321,17 @@ let apply_with_subst ~term ~subst (proof, goal) =
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
      newmetasenv''
    in
-   (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
-    (newproof, 
-     List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+   let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+   subst,
+   (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
+   max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
 
 
 (* ALB *)
-let apply_with_subst ~term ?(subst=[]) status =
+let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
   try
 (*     apply_tac_verbose ~term status *)
-    apply_with_subst ~term ~subst status
+    apply_with_subst ~term ~subst ~maxmeta status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure msg
@@ -339,7 +340,7 @@ let apply_with_subst ~term ?(subst=[]) status =
 
 (* ALB *)
 let apply_tac_verbose ~term status =
-  let subst, status = apply_with_subst ~term status in
+  let subst, status, _ = apply_with_subst ~term status in
   (CicMetaSubst.apply_subst subst), status
 
 let apply_tac ~term status = snd (apply_tac_verbose ~term status)
index c30952cae8b4ba6dc99aeca7549aa0ed98ad840a..6e0c821cca0333bfaf6b03ea5291f83ac02a6f3c 100644 (file)
@@ -44,8 +44,8 @@ val classify_metas :
 
 (* ALB, needed by the new paramodulation... *)
 val apply_with_subst:
-  term:Cic.term -> ?subst:Cic.substitution -> ProofEngineTypes.proof * int ->
-  Cic.substitution * (ProofEngineTypes.proof * int list)
+  term:Cic.term -> ?subst:Cic.substitution -> ?maxmeta:int -> ProofEngineTypes.proof * int ->
+  Cic.substitution * (ProofEngineTypes.proof * int list) * int
 
 (* not a real tactic *)
 val apply_tac_verbose :
index dfca1c90852ea5f25514cdacff6039eefc3626da..f146d45e6bc1f99eedd9a0cdfe431c2236a04fa3 100644 (file)
@@ -27,7 +27,7 @@
 
 let absurd = NegationTactics.absurd_tac
 let apply = PrimitiveTactics.apply_tac
-let applyS = AutoTactic.applyS_tac
+let applyS = Auto.applyS_tac
 let assumption = VariousTactics.assumption_tac
 let auto = AutoTactic.auto_tac
 let change = ReductionTactics.change_tac
index a5d6f00862a468df0a9c6642b3064779ab5d8940..9060afdd61d9eef885b63ce62372e3224dcc772f 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Sep 25 18:28:48 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Sep 27 17:37:14 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic