]> matita.cs.unibo.it Git - helm.git/commitdiff
Modifications to auto due to the introduction of the universe in
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 23 Nov 2006 14:31:56 +0000 (14:31 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 23 Nov 2006 14:31:56 +0000 (14:31 +0000)
the status.

16 files changed:
helm/software/components/tactics/.depend
helm/software/components/tactics/Makefile
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/autoCache.ml
helm/software/components/tactics/autoTactic.ml
helm/software/components/tactics/autoTactic.mli
helm/software/components/tactics/autoTypes.ml
helm/software/components/tactics/declarative.ml
helm/software/components/tactics/metadataQuery.ml
helm/software/components/tactics/metadataQuery.mli
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/utils.ml
helm/software/components/tactics/tactics.mli

index 398c2af396c6c63c2d84b5b57bc1d20ece9830ee..c8317fca41aa1c00c0a0900425c5b840f3b85c9b 100644 (file)
@@ -21,8 +21,8 @@ introductionTactics.cmi: proofEngineTypes.cmi
 eliminationTactics.cmi: proofEngineTypes.cmi 
 negationTactics.cmi: proofEngineTypes.cmi 
 equalityTactics.cmi: proofEngineTypes.cmi 
-auto.cmi: proofEngineTypes.cmi 
-autoTactic.cmi: proofEngineTypes.cmi 
+auto.cmi: universe.cmi proofEngineTypes.cmi 
+autoTactic.cmi: universe.cmi proofEngineTypes.cmi 
 discriminationTactics.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
 ring.cmi: proofEngineTypes.cmi 
@@ -30,6 +30,7 @@ setoids.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
+tactics.cmi: universe.cmi proofEngineTypes.cmi 
 declarative.cmi: proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
@@ -61,10 +62,12 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     hashtbl_equiv.cmi metadataQuery.cmi 
 metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     hashtbl_equiv.cmx metadataQuery.cmi 
+universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi 
+universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi 
 autoTypes.cmo: autoTypes.cmi 
 autoTypes.cmx: autoTypes.cmi 
-autoCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi autoCache.cmi 
-autoCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx autoCache.cmi 
+autoCache.cmo: universe.cmi autoCache.cmi 
+autoCache.cmx: universe.cmx autoCache.cmi 
 paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi 
 paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi 
 paramodulation/subst.cmo: paramodulation/subst.cmi 
@@ -92,15 +95,13 @@ paramodulation/indexing.cmx: paramodulation/utils.cmx \
     paramodulation/equality_indexing.cmx paramodulation/equality.cmx \
     paramodulation/indexing.cmi 
 paramodulation/saturation.cmo: paramodulation/utils.cmi \
-    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
-    proofEngineHelpers.cmi paramodulation/indexing.cmi \
-    paramodulation/founif.cmi paramodulation/equality.cmi \
-    paramodulation/saturation.cmi 
+    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
+    paramodulation/indexing.cmi paramodulation/founif.cmi \
+    paramodulation/equality.cmi paramodulation/saturation.cmi 
 paramodulation/saturation.cmx: paramodulation/utils.cmx \
-    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
-    proofEngineHelpers.cmx paramodulation/indexing.cmx \
-    paramodulation/founif.cmx paramodulation/equality.cmx \
-    paramodulation/saturation.cmi 
+    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
+    paramodulation/indexing.cmx paramodulation/founif.cmx \
+    paramodulation/equality.cmx paramodulation/saturation.cmi 
 variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     variousTactics.cmi 
@@ -129,16 +130,16 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
     proofEngineStructuralRules.cmx proofEngineReduction.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
     equalityTactics.cmi 
-auto.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \
-    paramodulation/saturation.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
-    primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \
-    equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \
-    autoCache.cmi auto.cmi 
-auto.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \
-    paramodulation/saturation.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
-    primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \
-    equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \
-    autoCache.cmx auto.cmi 
+auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/subst.cmi \
+    paramodulation/saturation.cmi proofEngineTypes.cmi \
+    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+    metadataQuery.cmi paramodulation/indexing.cmi equalityTactics.cmi \
+    paramodulation/equality.cmi autoTypes.cmi autoCache.cmi auto.cmi 
+auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
+    paramodulation/saturation.cmx proofEngineTypes.cmx \
+    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+    metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
+    paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi 
 autoTactic.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \
     primitiveTactics.cmi metadataQuery.cmi paramodulation/equality.cmi \
     autoTypes.cmi auto.cmi autoTactic.cmi 
@@ -203,7 +204,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
     fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
     eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \
     tactics.cmi 
-declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
-declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
     declarative.cmi 
index 74117ed87c2ceec77f4dab8011c58ed6acb749f9..cdb16efe466ab2eca4a476efc82e92b959a1439f 100644 (file)
@@ -6,10 +6,11 @@ INTERFACE_FILES = \
        continuationals.mli \
        tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
        primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
+       universe.mli \
        autoTypes.mli \
        autoCache.mli \
        paramodulation/utils.mli \
-       paramodulation/subst.mli\
+       paramodulation/subst.mli \
        paramodulation/equality.mli\
        paramodulation/founif.mli\
        paramodulation/equality_indexing.mli\
index 698053b40d48fff8c92823522f6aec05056abdf5..1e326df1086c25f7ce6f92640aff9d87b413dcc8 100644 (file)
 open AutoTypes;;
 open AutoCache;;
 
-let debug_print s = prerr_endline (Lazy.force s);;
+let debug_print s = prerr_endline (Lazy.force s);; 
 
 (* functions for retrieving theorems *)
 
 exception FillingFailure of AutoCache.cache * int
 
+let rec unfold context = function
+  | Cic.Prod(name,s,t) -> 
+      let t' = unfold ((Some (name,Cic.Decl s))::context) t in
+       Cic.Prod(name,s,t')     
+  | t -> ProofEngineReduction.unfold context t
 
-
-let find_library_theorems dbd proof gl = 
-  let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
+let find_library_theorems dbd proof goal = 
+  let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
   let terms = List.map CicUtil.term_of_uri univ in
   List.map 
     (fun t -> 
@@ -73,7 +77,7 @@ let partition_equalities =
   List.partition (fun (_,ty) -> is_an_equality ty)
 
 
-let default_auto maxm _ cache _ _ _ _ = [],cache,maxm ;; 
+let default_auto maxm _ cache _ _ _ _ = [],cache,maxm ;; 
 
 
 let is_unit_equation context metasenv oldnewmeta term = 
@@ -93,7 +97,7 @@ let is_unit_equation context metasenv oldnewmeta term =
             CicReduction.are_convertible ~metasenv context 
               sort (Cic.Sort Cic.Prop) u
           in
-          if b then Some i else None 
+         if b then Some i else None 
       | _ -> assert false)
     args
   in
@@ -101,48 +105,36 @@ let is_unit_equation context metasenv oldnewmeta term =
       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
        Some (args,metasenv,newmetas,head,newmeta)
     else None
+;;
 
-let retrieve_equations cache =
-  let eq_uri = 
-    match LibraryObjects.eq_URI() with
-      | None ->assert false
-      | Some eq_uri -> eq_uri in
-  let fake= Cic.Meta(-1,[]) in
-  let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);Cic.Meta(-1,[]); 
-    Cic.Meta(-2,[]); Cic.Meta(-3,[])] in
-  let candidates = get_candidates cache fake_eq in
+let get_candidates universe cache t =
+  let candidates = 
+    (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
+  in 
   let debug_msg =
-    (lazy ("candidates for " ^ (CicPp.ppterm fake_eq) ^ " = " ^ 
+    (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^ 
             (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
   debug_print debug_msg;
   candidates
-  
-(*
-  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 = 
-    Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache
-  in
-  prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
-    string_of_int maxm);
-  List.iter
-    (fun e -> prerr_endline (Equality.string_of_equality ~env e)) 
-    equalities;
-  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
-  let equalities = 
-    HExtlib.filter_map 
-      (fun e -> forward_simplify bag eq_uri env e active)
-    equalities
-  in
-  prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
-  List.iter
-    (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
-  prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
-  bag, equalities, cache, maxm
-*)
+;;
+
+let only singature context t =
+  try
+    let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
+    let consts = MetadataConstraints.constants_of ty in
+      MetadataConstraints.UriManagerSet.subset consts singature 
+  with _ -> false
+;;
+
+let retrieve_equations signature universe cache context=
+  match LibraryObjects.eq_URI() with
+    | None -> [] 
+    | Some eq_uri -> 
+       let eq_uri = UriManager.strip_xpointer eq_uri in
+       let fake= Cic.Meta(-1,[]) in
+       let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
+       let candidates = get_candidates universe cache fake_eq in
+       List.filter (only signature context) candidates
 
 let build_equality bag head args proof newmetas maxmeta = 
   match head with
@@ -178,41 +170,58 @@ let empty_tables =
    Saturation.make_passive [],
    Equality.mk_equality_bag)
 
-let init_cache_and_tables dbd use_library (proof, goal) =
+let init_cache_and_tables dbd use_library universe (proof, goal) =
+  (* the local cache in initially empty  *)
+  let cache = AutoCache.cache_empty in
   let _, metasenv, _, _ = proof in
+  let signature = MetadataQuery.signature_of metasenv goal in
   let newmeta = CicMkImplicit.new_meta metasenv [] in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let eq_uri = 
-    match LibraryObjects.eq_URI() with
-      | None ->assert false
-      | Some eq_uri -> eq_uri in
   let ct = find_context_theorems context metasenv in
   let lt = 
     if use_library then 
-      find_library_theorems dbd metasenv [goal] 
+      find_library_theorems dbd metasenv goal 
     else [] in
    (* all equations are added to the cache *) 
-  prerr_endline ("ho trovato " ^ (string_of_int (List.length lt)));
-  let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in
-  let equations,others = partition_equalities (ct@lt) in
+  prerr_endline 
+    ("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
+  (* let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in *)
+  let cache = cache_add_list cache context (ct@lt) in  
+  let equations = retrieve_equations signature universe cache context in
+  prerr_endline 
+    ("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
+  let eqs_and_types =
+    HExtlib.filter_map 
+      (fun t -> 
+        let ty,_ =
+          CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
+           (* retrieve_equations could also return flexible terms *)
+          if is_an_equality ty then Some(t,ty) 
+          else
+            try
+               let ty' = unfold context ty in
+                if is_an_equality ty' then Some(t,ty') else None
+             with _ -> None) (* catturare l'eccezione giusta di unfold *)
+      equations in
   let bag = Equality.mk_equality_bag () in
   let units, other_equalities, newmeta = 
-    partition_unit_equalities context metasenv newmeta bag equations in
-  (* other equations are added to the cache; note that untis equalities
-     are not)*)
-  let env = (metasenv, context, CicUniv.empty_ugraph) in 
-  (* let equalities = 
+    partition_unit_equalities context metasenv newmeta bag eqs_and_types in
+  (* let env = (metasenv, context, CicUniv.empty_ugraph) in 
+    let equalities = 
+    let eq_uri = 
+    match LibraryObjects.eq_URI() with
+      | None ->assert false
+      | Some eq_uri -> eq_uri in
     Saturation.simplify_equalities bag eq_uri env units in *)
   let passive = Saturation.make_passive units in
   let no = List.length units in
-  prerr_endline ("No = " ^ (string_of_int no));
   let active = Saturation.make_active [] in
   let active,passive,newmeta = 
     Saturation.pump_actives context bag newmeta active passive (no+1) infinity
   in 
     (active,passive,bag),cache,newmeta
 
-let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast = 
+let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast = 
   let head, metasenv, args, newmeta =
     ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
   in
@@ -238,9 +247,10 @@ let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast =
       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
       [args,metasenv,newmetas,head,newmeta],cache,newmeta
     else
+      (*
       let proof = 
         None,metasenv,term,term (* term non e' significativo *)
-      in
+      in *)
       let flags = 
         if fast then
           {AutoTypes.default_flags() with 
@@ -253,7 +263,7 @@ let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast =
            maxwidth = 2;maxdepth = 4;
            use_paramod=true;use_only_paramod=false} 
       in
-      match auto newmeta tables cache context metasenv propositional_args flags with
+      match auto newmeta tables universe cache context metasenv propositional_args flags with
       | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
       | substs,cache,newmeta ->
           List.map 
@@ -272,14 +282,14 @@ let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast =
   in
   results,cache,newmeta
 
-let build_equalities auto context metasenv tables cache newmeta equations =
+let build_equalities auto context metasenv tables universe cache newmeta equations =
   List.fold_left 
     (fun (facts,cache,newmeta) (t,ty) ->
        (* in any case we add the equation to the cache *)
        let cache = AutoCache.cache_add_list cache context [(t,ty)] in
        try
          let saturated,cache,newmeta = 
-           fill_hypothesis context metasenv newmeta ty tables cache auto true
+           fill_hypothesis context metasenv newmeta ty tables universe cache auto true
          in
          let (active,passive,bag) = tables in
          let eqs,bag,newmeta = 
@@ -299,11 +309,12 @@ let build_equalities auto context metasenv tables cache newmeta equations =
       )
     ([],cache,newmeta) equations
 
-let close_more tables maxmeta context status auto cache =
+let close_more tables maxmeta context status auto universe cache =
   let (active,passive,bag) = tables in
   let proof, goalno = status in
-  let _, metasenv,_,_ = proof in
-  let equations = retrieve_equations cache in
+  let _, metasenv,_,_ = proof in  
+  let signature = MetadataQuery.signature_of metasenv goalno in
+  let equations = retrieve_equations signature universe cache context in
   let eqs_and_types =
     HExtlib.filter_map 
       (fun t -> 
@@ -313,7 +324,7 @@ let close_more tables maxmeta context status auto cache =
           if is_an_equality ty then Some(t,ty) else None)
       equations in
   let units, cache, maxm = 
-      build_equalities auto context metasenv tables cache maxmeta eqs_and_types in
+      build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
   prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
     string_of_int maxm);
   List.iter
@@ -329,9 +340,8 @@ let close_more tables maxmeta context status auto cache =
     (active,passive,bag),cache,newmeta
 
 let find_context_equalities 
-  maxmeta bag context proof cache 
+  maxmeta bag context proof (universe:Universe.universe) cache 
 =
-  prerr_endline "find_equalities";
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
@@ -353,7 +363,7 @@ let find_context_equalities
                 let term = S.lift index term in
                 let saturated,cache,newmeta = 
                   fill_hypothesis context metasenv newmeta term 
-                    empty_tables cache default_auto false
+                    empty_tables universe cache default_auto false
                 in
                 let eqs,newmeta = 
                   List.fold_left 
@@ -393,8 +403,8 @@ let find_context_equalities
 (***************** applyS *******************)
 
 let new_metasenv_and_unify_and_t 
- dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty
- goal_arity 
+ dbd flags universe proof goal ?tables newmeta' metasenv' 
context term' ty termty goal_arity 
 =
  let (consthead,newmetasenv,arguments,_) =
    ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
@@ -428,7 +438,7 @@ let new_metasenv_and_unify_and_t
  in
  match 
    let (active, passive,bag), cache, maxmeta =
-     init_cache_and_tables dbd true (proof'''',newmeta)
+     init_cache_and_tables dbd flags.use_library universe (proof'''',newmeta)
    in
      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive 
        max_int max_int flags.timeout
@@ -446,7 +456,7 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) =
+let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
@@ -492,7 +502,7 @@ let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) =
    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
    let goal_arity = count_prods context ty in
    let subst, proof, gl, active, passive =
-    new_metasenv_and_unify_and_t dbd flags proof goal ?tables
+    new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
      newmeta' metasenv' context term' ty termty goal_arity
    in
     subst, proof, gl, active, passive
@@ -673,18 +683,18 @@ let try_candidate
     let open_goals = order_new_goals metasenv subst open_goals ppterm in
     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
     Some (metasenv,subst,open_goals), tables , maxmeta
-  with ProofEngineTypes.Fail s -> 
+  with 
+    | ProofEngineTypes.Fail s -> 
     (*debug_print("   KO: "^Lazy.force s);*)None,tables, maxm
+    | CicUnification.Uncertain s ->  
+    (*debug_print("   BECCATO: "^Lazy.force s);*)None,tables, maxm
 ;;
 
 let applicative_case 
-  tables maxm depth subst fake_proof goalno goalty metasenv context cache
+  tables maxm depth subst fake_proof goalno goalty metasenv context universe
+  cache
 = 
-  let candidates = get_candidates cache goalty in
-  let debug_msg =
-    (lazy ("candidates for " ^ (CicPp.ppterm goalty) ^ " = " ^ 
-            (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
-  debug_print debug_msg;
+  let candidates = get_candidates universe cache goalty in
   let tables, elems, maxm = 
     List.fold_left 
       (fun (tables,elems,maxm) cand ->
@@ -729,7 +739,7 @@ let cache_add_success sort cache k v =
   cache k
 ;;
 
-let rec auto_main tables maxm context flags elems cache =
+let rec auto_main tables maxm context flags elems universe cache =
   let flags = calculate_timeout flags in
   let ppterm = ppterm context in
   let irl = mk_irl context in
@@ -757,7 +767,7 @@ let rec auto_main tables maxm context flags elems cache =
               (lazy (" FAILURE(not in prop)"));
             aux flags tables maxm cache tl (* FAILURE (not in prop) *))
           else
-          match aux_single flags tables maxm cache metasenv subst elem goalty cc with
+          match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
           | Fail s, tables, cache, maxm' -> 
               assert(maxm' >= maxm);let maxm = maxm' in
               debug_print
@@ -804,11 +814,10 @@ let rec auto_main tables maxm context flags elems cache =
            (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
           aux flags tables maxm cache ((metasenv,subst,gl)::tl)
 
-  and aux_single flags tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
+  and aux_single flags tables maxm universe 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) *)
-    prerr_endline ("DEPTH = +++++++= "^ (string_of_int depth));
     match cache_examine cache goalty with
     | Failed_in d when d >= depth -> 
         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
@@ -839,14 +848,14 @@ let rec auto_main tables maxm context flags elems cache =
              else
                applicative_case 
                  tables maxm depth subst fake_proof goalno 
-                 goalty metasenv context cache in
+                 goalty metasenv context universe cache in
              assert(maxm1 >= maxm);
              let maxm = maxm1 in
              elems@more_elems, tables, cache, maxm, flags            
           else
            let elems, tables, cache, maxm =
             applicative_case tables maxm depth subst fake_proof goalno 
-              goalty metasenv context cache in
+              goalty metasenv context universe cache in
            elems, tables, cache, maxm, flags  
         in
         aux flags tables maxm cache elems
@@ -855,13 +864,13 @@ let rec auto_main tables maxm context flags elems cache =
     aux flags tables maxm cache elems
 
 and
-  auto_all_solutions maxm tables cache context metasenv gl flags 
+  auto_all_solutions maxm tables universe cache context metasenv gl flags 
 =
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
   let elems = [metasenv,[],goals] in
   let rec aux tables maxm solutions cache elems flags =
-    match auto_main tables maxm context flags elems cache with
+    match auto_main tables maxm context flags elems universe cache with
     | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
     | Success (metasenv,subst,others),tables,cache,maxm -> 
         if Unix.gettimeofday () > flags.timeout then
@@ -887,19 +896,19 @@ and
 
 (* }}} ****************** AUTO ***************)
 
-let auto_all tables cache context metasenv gl flags =
+let auto_all tables universe cache context metasenv gl flags =
   let solutions, cache, _ = 
-    auto_all_solutions 0 tables cache context metasenv gl flags
+    auto_all_solutions 0 tables universe cache context metasenv gl flags
   in
   solutions, cache
 ;;
 
-let auto flags metasenv tables cache context metasenv gl =
+let auto flags metasenv tables universe cache context metasenv gl =
   let initial_time = Unix.gettimeofday() in
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
   let elems = [metasenv,[],goals] in
-  match auto_main tables 0 context flags elems cache with
+  match auto_main tables 0 context flags elems universe cache with
   | Success (metasenv,subst,_), tables,cache,_ -> 
       prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
       Some (subst,metasenv), cache
@@ -937,7 +946,8 @@ let flags_of_params params ?(for_applyS=false) () =
  let use_paramod = bool "use_paramod" true in
  let use_only_paramod =
   if for_applyS then true else bool "paramodulation" false in
- let use_library = bool "library" (not use_only_paramod) in
+ let use_library = bool "library"  
+   ((AutoTypes.default_flags()).AutoTypes.use_library) in
  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
  let timeout = int "timeout" 0 in
@@ -958,12 +968,12 @@ let flags_of_params params ?(for_applyS=false) () =
     AutoTypes.dont_cache_failures = false;
   }
 
-let applyS_tac ~dbd ~term ~params =
+let applyS_tac ~dbd ~term ~params ~universe =
  ProofEngineTypes.mk_tactic
   (fun status ->
     try 
       let _, proof, gl,_,_ =
-       apply_smart ~dbd ~term ~subst:[]
+       apply_smart ~dbd ~term ~subst:[] ~universe
         (flags_of_params params ~for_applyS:true ()) status
       in 
        proof, gl
@@ -1003,6 +1013,7 @@ let rec position_of i x = function
   | _ -> i
 ;;
 
+
 let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   Saturation.reset_refs();
   let proof,goalno = status in 
@@ -1013,7 +1024,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   let names = Utils.names_of_context context in
   let bag = Equality.mk_equality_bag () in
   let eq_index, equalities, maxm,cache  = 
-    find_context_equalities 0 bag context proof AutoCache.cache_empty 
+    find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty 
   in
   let eq_what = 
     let what = find_in_ctx 1 target context in
@@ -1093,8 +1104,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   proof,[goalno]
 ;;
 
-
-let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
+let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
   (* argument parsing *)
   let string = string params in
   let bool = bool params in
@@ -1117,16 +1127,16 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
       (* just for testing *)
       let use_library = flags.use_library in
       let tables,cache,newmeta =
-       init_cache_and_tables dbd use_library (proof, goal) in
+       init_cache_and_tables dbd use_library universe (proof, goal) in
       let tables,cache,newmeta =
         if flags.close_more then
          close_more 
-           tables newmeta context (proof, goal) auto_all_solutions cache 
+           tables newmeta context (proof, goal) auto_all_solutions universe cache 
        else tables,cache,newmeta in
       let initial_time = Unix.gettimeofday() in
       let (_,oldmetasenv,_,_) = proof in
       let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
-      match auto_main tables newmeta context flags [elem] cache with
+      match auto_main tables newmeta context flags [elem] universe cache with
        | Success (metasenv,subst,_), tables,cache,_ -> 
            prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
            let proof,metasenv = 
@@ -1142,7 +1152,8 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
            raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
 ;;
 
-let auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);;
+let auto_tac ~dbd ~params ~universe = 
+  ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
 
 let eq_of_goal = function
   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
@@ -1158,7 +1169,7 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
   let initgoal = [], [], ty in
   let eq_uri = eq_of_goal ty in
   let (active,passive,bag), cache, maxm =
-     init_cache_and_tables dbd true (proof,goal) in
+     init_cache_and_tables dbd true Universe.empty (proof,goal) in
   let equalities = (Saturation.list_of_passive passive) in
   (* we demodulate using both actives passives *)
   let table = 
index 6e64fb66eee33a638bb9339f43650f45cd850023..d749a26af175a8221d2d655794594ad0536873fd 100644 (file)
 
 (* stops at the first solution *)
 val auto_tac:
- dbd:HMysql.dbd -> params:(string * string) list -> ProofEngineTypes.tactic
+  dbd:HMysql.dbd -> 
+  params:(string * string) list -> 
+  universe:Universe.universe ->
+  ProofEngineTypes.tactic
 
 val applyS_tac:
- dbd:HMysql.dbd -> term: Cic.term -> params:(string * string) list ->
+  dbd:HMysql.dbd -> 
+  term: Cic.term -> 
+  params:(string * string) list ->
+  universe:Universe.universe ->
   ProofEngineTypes.tactic
 
 val demodulate_tac : dbd:HMysql.dbd -> ProofEngineTypes.tactic
index 0b42391fa63beb345d941aa34a773562cdf8fb97..57701310c445b3de47adc3e56aa3806708e397fc 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-module Codomain = struct 
-  type t = Cic.term 
-  let compare = Pervasives.compare 
-end
-module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
-type universe = TI.t
-(* (proof,ty) list *)
 type cache_key = Cic.term
 type cache_elem = 
   | Failed_in of int
   | Succeded of Cic.term
   | UnderInspection
   | Notfound
-type cache = (universe * ((cache_key * cache_elem) list));;
+type cache = (Universe.universe * ((cache_key * cache_elem) list));;
 
-let cache_empty = (TI.empty,[]);;
-let get_candidates (univ,_) ty = 
-  S.elements (TI.retrieve_unifiables univ ty)
-;;
-
-let rec unfold context = function
-  | Cic.Prod(name,s,t) -> 
-      let t' = unfold ((Some (name,Cic.Decl s))::context) t in
-       Cic.Prod(name,s,t')     
-  | t -> ProofEngineReduction.unfold context t
 
+let cache_empty = (Universe.empty,[]);;
 
-let rec collapse_head_metas = function 
-  | Cic.Appl(a::l) -> 
-      let a' = collapse_head_metas a in
-      (match a' with
-       | Cic.Meta(n,m) -> Cic.Meta(n,m)
-       | t ->  
-           let l' = List.map collapse_head_metas l in
-              Cic.Appl(t::l'))
-  | t -> t
-;;
-  
-let rec head t = 
-  let rec aux = function
-  | Cic.Prod(_,_,t) -> 
-      CicSubstitution.subst (Cic.Meta (-1,[])) (aux t)
-  | t -> t
-  in collapse_head_metas (aux t)
+let get_candidates (univ,_) ty = 
+  Universe.get_candidates univ ty
 ;;
 
-let index (univ,oldcache) key term =
-  prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
-  (TI.index univ key term,oldcache)
+let index (univ,cache) key term =
+  Universe.index univ key term,cache
 ;;
 
-let index_term_and_unfolded_term cache context t ty =
-  let key = head ty in
-  let cache = index cache key t in
-  try  
-    let key = head (unfold context ty) in
-    index cache key t
-  with ProofEngineTypes.Fail _ -> cache
+let index_term_and_unfolded_term (univ,cache) context t ty =
+  Universe.index_local_term univ context t ty, cache
 ;;
 
-let cache_add_list cache context terms_and_types =
-  List.fold_left  
-    (fun acc (term,ty) -> 
-       index_term_and_unfolded_term acc context term ty)
-    cache terms_and_types
+let cache_add_list (univ,cache) context terms_and_types =
+  let univ = 
+    List.fold_left
+      (fun univ (t,ty) -> 
+        Universe.index_local_term univ context t ty)
+      univ terms_and_types  
+  in
+  univ, cache
 
 let cache_examine (_,oldcache) cache_key = 
   try List.assoc cache_key oldcache with Not_found -> Notfound
@@ -112,7 +77,7 @@ let cache_add_failure cache cache_key depth =
       assert false (* if succed it can't fail *)
 ;;
 let cache_add_success ((univ,_) as cache) cache_key proof =
-  TI.index univ cache_key proof,snd
+  Universe.index univ cache_key proof,snd
   (match cache_examine cache cache_key with
   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
index 8e94bba86e4f072796f32d482f363d5df2e5ed24..e8d034a3298a9630fa0c8b1efe693579a1045ed2 100644 (file)
@@ -317,22 +317,22 @@ let int params name default =
         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 ;;  
 
-let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
+let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) =
   (* argument parsing *)
   let int = int params in
   let bool = bool params in
-  let newauto = bool "new" false in
+  let oldauto = bool "old" false in
   let use_only_paramod = bool "paramodulation" false in
-  let newauto = if use_only_paramod then true else newauto in
+  let oldauto = if use_only_paramod then false else oldauto in
   let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
   let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
-   if not newauto then 
+   if oldauto then 
     auto_tac_old ~depth ~width ~dbd () (proof,goal)
    else
-    ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params) (proof,goal)
+    ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params ~universe) (proof,goal)
 
-let auto_tac ~params ~dbd =
-      ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
+let auto_tac ~params ~dbd ~universe=
+      ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe)
 ;;
 
 let pp_proofterm = Equality.pp_proofterm;;
index 23f1b813fdf727b635906c26d335bfaeeb11c839..d96a826150f2922c9890e41d3988779b7b8b81de 100644 (file)
@@ -25,6 +25,9 @@
  *)
 
 val auto_tac:
- params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+ params:(string * string) list 
+  -> dbd:HMysql.dbd 
+  -> universe:Universe.universe
+  -> ProofEngineTypes.tactic
 
 val pp_proofterm: Cic.term -> string
index 9031a0338736fa152c1efd1add013abc95a66b5c..5a84c2c2ba73bab691fdd39cc606ebfa718346a9 100644 (file)
@@ -38,7 +38,7 @@ let default_flags _ =
   {maxwidth=3;
    maxdepth=3;
    timeout=Unix.gettimeofday() +.3.0;
-   use_library=true;
+   use_library=false;
    use_paramod=true;
    use_only_paramod=false;
    close_more=false; 
index 7561281a854ddd5871a32a577e7912a064517abd..fc8b175a273e04970d1af8dd2b32c97cb2ae5383 100644 (file)
@@ -48,7 +48,7 @@ let suppose t id ty =
 let by_term_we_proved ~dbd t ty id ty' =
  let just =
   match t with
-     None -> Tactics.auto ~dbd ~params:[]
+     None -> Tactics.auto ~dbd ~params:[] (* da sistemare *) ~universe:Universe.empty
    | Some t -> Tactics.apply t
  in
   match id with
@@ -80,7 +80,7 @@ let by_term_we_proved ~dbd t ty id ty' =
 let bydone ~dbd t =
  let just =
   match t with
-     None -> Tactics.auto ~dbd ~params:[]
+     None -> Tactics.auto ~dbd ~params:[] ~universe:Universe.empty
    | Some t -> Tactics.apply t
  in
   just
@@ -150,8 +150,8 @@ let rewritingstep ~dbd lhs rhs just conclude =
    match just with
       None ->
        Tactics.auto ~dbd
-        ~params:["paramodulation","1"; "timeout","3"; "library","1"]
-    | Some just -> Tactics.apply just
+        ~params:["paramodulation","1"; "timeout","3"] ~universe:Universe.empty
+    | Some just -> Tactics.apply just 
   in
    match lhs with
       None ->
index 9b4f565c801a5bad56419ec2bebedbc3f15b7cb8..443ae973fe2c7b0c86d288ab08015c482db471a9 100644 (file)
@@ -240,22 +240,47 @@ let only constants uri =
   Constr.UriManagerSet.subset consts constants 
 ;;
 
-let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals =
-  let add_uris_for acc goal =
-   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
-   let main, sig_constants = Constr.signature_of ty in
-   let set = signature_of_hypothesis context metasenv in
-   let set =
-    match main with
-       None -> set
-     | Some (main,l) ->
-        List.fold_right Constr.UriManagerSet.add (main::l) set in
-   let set = Constr.UriManagerSet.union set sig_constants in
-   let all_constants_closed = close_with_types set metasenv context in
-   Constr.UriManagerSet.union all_constants_closed acc
-  in
-  let all_constants_closed = 
-    List.fold_left add_uris_for Constr.UriManagerSet.empty goals in
+let rec types_of_equality = function
+  | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _] 
+    when (LibraryObjects.is_eq_URI uri) -> 
+      let uri_set = Constr.constants_of ty in
+      if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then
+       Constr.SetSet.empty
+      else Constr.SetSet.singleton uri_set
+  | Cic.Prod (_, s, t) -> 
+      Constr.SetSet.union (types_of_equality s) (types_of_equality t)
+  | _ -> Constr.SetSet.empty
+;;
+
+let types_for_equality metasenv goal =
+  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+  let all = types_of_equality ty in
+  let _, all = 
+    List.fold_left
+      (fun (i,acc) _ ->         
+        let ty, _ = 
+           CicTypeChecker.type_of_aux' 
+             metasenv context (Cic.Rel i) CicUniv.empty_ugraph in
+        let newty = types_of_equality ty in
+          (i+1,Constr.SetSet.union newty acc)) 
+      (1,all) context
+  in all
+;;
+          
+let signature_of metasenv goal = 
+  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+  let ty_set = Constr.constants_of ty in
+  let hyp_set = signature_of_hypothesis context metasenv in
+  let set = Constr.UriManagerSet.union ty_set hyp_set in
+    close_with_types set metasenv context
+
+
+let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
+  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+  let ty_set = Constr.constants_of ty in
+  let hyp_set = signature_of_hypothesis context metasenv in
+  let set = Constr.UriManagerSet.union ty_set hyp_set in
+  let all_constants_closed = close_with_types set metasenv context in
   (* we split predicates from the rest *)
   let predicates, rest = 
     Constr.UriManagerSet.partition is_predicate all_constants_closed
@@ -263,11 +288,34 @@ let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals =
   let uris =
     Constr.UriManagerSet.fold
       (fun u acc -> 
-        let uris =
-          sigmatch ~dbd ~facts:false ~where:`Statement 
-            (Some (u,[]),all_constants_closed)
-        in
-        acc @ uris)
+         prerr_endline ("processing "^(UriManager.string_of_uri u));
+         let set_for_sigmatch = 
+          Constr.UriManagerSet.remove u all_constants_closed in
+        if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
+          (* equality has a special treatment *)
+           (prerr_endline "special treatment";
+          let tfe =
+            Constr.SetSet.elements (types_for_equality metasenv goal) 
+          in
+            List.fold_left 
+              (fun acc l ->
+                 let tyl = Constr.UriManagerSet.elements l in
+                  prerr_endline ("tyl: "^(String.concat "\n" 
+                       (List.map UriManager.string_of_uri tyl)));
+                 let set_for_sigmatch =
+                   Constr.UriManagerSet.diff set_for_sigmatch l in
+                 let uris =
+                   sigmatch ~dbd ~facts:false ~where:`Statement 
+                     (Some (u,tyl),set_for_sigmatch) in
+                   acc @ uris) 
+              acc tfe)
+        else
+           (prerr_endline "normal treatment";
+           let uris =
+             sigmatch ~dbd ~facts:false ~where:`Statement 
+               (Some (u,[]),set_for_sigmatch)
+           in
+             acc @ uris))
       predicates []
   in
 (*
@@ -277,8 +325,9 @@ let universe_of_goals ~(dbd:HMysql.dbd) metasenv 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
+  if apply_only then 
+    List.filter (only all_constants_closed) uris 
+  else uris
 ;;
 
 let filter_out_predicate set ctx menv =
index aebe451986e64fdba499093a430fa33c173830cb..1bc9fa3630ead558cfd8c26134bd21d8735e7fe7 100644 (file)
@@ -33,8 +33,16 @@ val signature_of_goal:
   dbd:HMysql.dbd -> ProofEngineTypes.status ->
     UriManager.uri list
 
-val universe_of_goals:
-  dbd:HMysql.dbd -> Cic.metasenv -> ProofEngineTypes.goal list ->
+val signature_of:
+ Cic.metasenv -> 
+  ProofEngineTypes.goal ->
+  MetadataConstraints.UriManagerSet.t
+
+val universe_of_goal:
+  dbd:HMysql.dbd -> 
+  bool ->  (* apply only or not *)
+  Cic.metasenv -> 
+  ProofEngineTypes.goal ->
     UriManager.uri list
 
 val equations_for_goal:
index 7123c134a93a98056655f6cee83e55600b559945..10a64af19d09a15d762697512ba00de2270a964d 100644 (file)
@@ -372,7 +372,8 @@ let contextualize uri ty left right t =
    * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
    * ctx_ty is the type of ctx
    *)
-    let rec aux uri ty left right ctx_d ctx_ty = function
+    let rec aux uri ty left right ctx_d ctx_ty t =
+      match t with 
       | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
         when LibraryObjects.is_sym_eq_URI uri_sym  ->
           let ty,l,r,p = open_sym ens tl in
@@ -407,8 +408,8 @@ let contextualize uri ty left right t =
           let c_what = put_in_ctx ctx_c what in
           (* now put the proofs in the compound context *)
           let p1 = (* p1: dc_what = d_m *)
-            if is_not_fixed_lp then 
-              aux uri ty2 c_what m ctx_d ctx_ty p1 
+            if is_not_fixed_lp then
+              aux uri ty2 c_what m ctx_d ctx_ty p1
             else
               mk_sym uri_sym ctx_ty d_m dc_what
                 (aux uri ty2 m c_what ctx_d ctx_ty p1)
@@ -417,7 +418,7 @@ let contextualize uri ty left right t =
             if avoid_eq_ind then
               mk_sym uri_sym ctx_ty dc_what dc_other
                 (aux uri ty1 what other ctx_dc ctx_ty p2)
-            else
+             else
               aux uri ty1 other what ctx_dc ctx_ty p2
           in
           (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
@@ -496,7 +497,7 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
     p
 ;;
 
-let parametrize_proof p l r ty = 
+let parametrize_proof menv p l r ty = 
   let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
   let mot = CicUtil.metas_of_term_set in
   let parameters = uniq (mot p @ mot l @ mot r) in 
@@ -517,9 +518,21 @@ let parametrize_proof p l r ty =
       match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
     ~what ~with_what ~where:p
   in
+  let ty_of_m _ = Cic.Implicit (Some `Type)
+(*
+  let ty_of_m = function
+    | Cic.Meta (i,_) ->
+       (try
+         let _,_,ty = CicUtil.lookup_meta i menv in ty
+       with CicUtil.Meta_not_found _ -> 
+         prerr_endline "eccoci";assert false)
+    | _ -> assert false
+*)
+  (*
   let ty_of_m _ = ty (*function 
     | Cic.Meta (i,_) -> List.assoc i menv 
     | _ -> assert false *)
+  *)
   in
   let args, proof,_ = 
     List.fold_left 
@@ -729,7 +742,7 @@ let build_goal_proof bag eq l initial ty se context menv =
         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)
+          parametrize_proof menv cic l r (CicSubstitution.lift n mty)
         in
         let h = (id, instance)::lift_list h in
         acc@[id,real_cic],n+1,h) 
index 7bbc4d43ca7fb7548a6397f08ffc16f473d9c648..28c22a64e34b8fd7ccf99d34ba4903f7f526aa0f 100644 (file)
@@ -1003,8 +1003,11 @@ let build_newgoal bag context goal posu rule expansion =
       Utils.guarded_simpl context 
         (apply_subst subst (CicSubstitution.subst other t)) 
     in
-    let bo' = (*apply_subst subst*) t in 
-    let name = Cic.Name "x" in
+    let bo' = (*apply_subst subst*) t in
+    (* patch?? 
+    let bo' = t in
+    let ty = apply_subst subst ty in *)
+    let name = Cic.Name "x" in 
     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
     bo, (newgoalproofstep::goalproof)
   in
index 40d07e414b644090362d3da6dabf2daf7ab6f785..d9472601c958c96b62526c9af50c11e1ac5a6f9b 100644 (file)
@@ -1238,6 +1238,62 @@ let eq_and_ty_of_goal = function
   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
 ;;
 
+(* fix proof takes in input a term and try to build a metasenv for it *)
+
+let fix_proof metasenv context all_implicits p =
+  let rec aux metasenv n p =
+    match p with
+      | Cic.Meta (i,_) -> 
+          if all_implicits then 
+           metasenv,Cic.Implicit None
+         else
+         let irl = 
+           CicMkImplicit.identity_relocation_list_for_metavariable context 
+         in
+          let meta = CicSubstitution.lift n (Cic.Meta (i,irl)) in
+         let metasenv =
+           try 
+           let _ = CicUtil.lookup_meta i metasenv in metasenv
+           with CicUtil.Meta_not_found _ ->
+            prerr_endline ("not found: "^(string_of_int i));
+           let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
+             (i,context,Cic.Meta(j,irl))::metasenv
+         in
+           metasenv,meta
+      | Cic.Appl l ->
+         let metasenv,l=
+            List.fold_right 
+             (fun a (metasenv,l) -> 
+                let metasenv,a' = aux metasenv n a in
+                  metasenv,a'::l)
+             l (metasenv,[])
+         in metasenv,Cic.Appl l
+      | Cic.Lambda(name,s,t) ->
+         let metasenv,s = aux metasenv n s in
+         let metasenv,t = aux metasenv (n+1) t in
+           metasenv,Cic.Lambda(name,s,t)
+      | Cic.Prod(name,s,t) ->
+         let metasenv,s = aux metasenv n s in
+         let metasenv,t = aux metasenv (n+1) t in
+           metasenv,Cic.Prod(name,s,t)
+      | Cic.LetIn(name,s,t) ->
+         let metasenv,s = aux metasenv n s in
+         let metasenv,t = aux metasenv (n+1) t in
+           metasenv,Cic.LetIn(name,s,t)              
+      | t -> metasenv,t
+  in
+  aux metasenv 0 p 
+;;
+
+let fix_metasenv metasenv context =
+  List.fold_left 
+    (fun m (i,c,t) ->
+       let m,t = fix_proof m context false t in
+       let m = List.filter (fun (j,_,_) -> j<>i) m in
+        (i,c,t)::m)
+    metasenv metasenv
+;;
+
 (* status: input proof status
  * goalproof: forward steps on goal
  * newproof: backward steps
@@ -1246,38 +1302,95 @@ let eq_and_ty_of_goal = function
  * 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
 =
+  if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
+  else prerr_endline (CicMetaSubst.ppmetasenv [] 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 names = Utils.names_of_context context in
-      prerr_endline "Proof:";
-      prerr_endline 
-        (Equality.pp_proof bag names goalproof newproof subsumption_subst
-          subsumption_id type_of_goal);
-(*       prerr_endline "ENDOFPROOFS"; *)
+  let names = Utils.names_of_context context in
+  prerr_endline "Proof:";
+  prerr_endline 
+    (Equality.pp_proof bag names goalproof newproof subsumption_subst
+       subsumption_id type_of_goal);
 (*
       prerr_endline ("max weight: " ^ 
        (string_of_int (Equality.max_weight goalproof newproof)));
 *)
-      (* generation of the CIC proof *)
-      let side_effects = 
-        List.filter (fun i -> i <> goalno)
-          (ProofEngineHelpers.compare_metasenvs 
-            ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
-      in
-      let goal_proof, side_effects_t = 
-        let initial = Equality.add_subst subsumption_subst newproof in
-        Equality.build_goal_proof bag
-          eq_uri goalproof initial type_of_goal side_effects
-          context proof_menv
-      in
-      (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
-      let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+  (* generation of the CIC proof *) 
+  (* let metasenv' = List.filter (fun i,_,_ -> i<>goalno) metasenv in *)
+  let side_effects = 
+    List.filter (fun i -> i <> goalno)
+      (ProofEngineHelpers.compare_metasenvs 
+         ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in
+  let goal_proof, side_effects_t = 
+    let initial = (* Equality.add_subst subsumption_subst*) newproof in
+      Equality.build_goal_proof bag
+        eq_uri goalproof initial type_of_goal side_effects
+        context proof_menv  
+  in
+  let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+  let real_menv =  fix_metasenv (proof_menv@metasenv) context in
+  let real_menv,goal_proof = 
+    fix_proof real_menv context false goal_proof in
+(*
+  let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in
+    (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
+*)
+  let goal_proof,goal_ty,real_menv,_ = 
+    (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
+    try
+      CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
+    with 
+      | CicUtil.Meta_not_found _ 
+      | CicRefine.RefineFailure _ 
+      | CicRefine.Uncertain _ 
+      | CicRefine.AssertFailure _
+      | Invalid_argument "list_fold_left2" as exn ->
+          prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+          prerr_endline (CicPp.pp goal_proof names); 
+          prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+          raise exn
+  in     
+  let subst_side_effects,real_menv,_ = 
+    try
+      CicUnification.fo_unif_subst [] context real_menv
+        goal_ty type_of_goal CicUniv.empty_ugraph
+    with
+      | CicUnification.UnificationFailure s
+      | CicUnification.Uncertain s 
+      | CicUnification.AssertFailure s -> assert false
+         (*            fail "Maybe the local context of metas in the goal was not an IRL" s *)
+  in
+  prerr_endline "+++++++++++++ FINE UNIF";
+  let final_subst = 
+    (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
+  in
+(*
+      let metas_of_proof = Utils.metas_of_term goal_proof in
+*)
+  let proof, real_metasenv = 
+    ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+      proof goalno (CicMetaSubst.apply_subst final_subst) 
+      (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
+  in      
+  let open_goals = 
+    (ProofEngineHelpers.compare_metasenvs 
+       ~oldmetasenv:metasenv ~newmetasenv:real_metasenv) in
+(*
+  let open_goals =
+    List.map (fun i,_,_ -> i) real_metasenv in
+*)
+  final_subst, proof, open_goals
+
+
+(*
+
       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
       (* prerr_endline (CicPp.pp goal_proof names); *)
       let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
@@ -1287,23 +1400,26 @@ let build_proof
       (* replacing fake mets with real ones *)
       (* prerr_endline "replacing metas..."; *)
       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
-      let goal_proof_menv, what, with_what,free_meta = 
+      if proof_menv = [] then prerr_endline "VUOTA";
+      CicMetaSubst.ppmetasenv [] proof_menv;
+      let what, with_what = 
         List.fold_left 
-          (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> 
-             match uniq with
-               | Some m -> 
-(*                     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))) 
-          ([],[],[],None) 
+          (fun (acc1,acc2) i -> 
+            (Cic.Meta(i,[]))::acc1, (Cic.Implicit None)::acc2)
+          ([],[])
+         metas_still_open_in_proof
+(*
           (List.filter 
            (fun (i,_,_) -> 
              List.mem i metas_still_open_in_proof
              (*&& not(List.mem i metas_still_open_in_goal)*)) 
            proof_menv)
+*)
+      in
+      let goal_proof_menv =
+       List.filter 
+          (fun (i,_,_) -> List.mem i metas_still_open_in_proof)
+             proof_menv
       in
       let replace where = 
         (* we need this fake equality since the metas of the hypothesis may be
@@ -1332,54 +1448,58 @@ let build_proof
           ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false)
           ~where:type_of_goal
       in
+      let goal_proof,goal_ty,real_menv,_ = 
+        prerr_endline "parte la refine";
+        try
+          CicRefine.type_of_aux' metasenv context goal_proof
+            CicUniv.empty_ugraph
+        with 
+        | CicUtil.Meta_not_found _ 
+        | CicRefine.RefineFailure _ 
+        | CicRefine.Uncertain _ 
+        | CicRefine.AssertFailure _
+        | Invalid_argument "list_fold_left2" as exn ->
+            prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+            prerr_endline (CicPp.pp goal_proof names); 
+            prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+            raise exn
+      in      
+      prerr_endline "+++++++++++++ METASENV";
+      prerr_endline
+       (CicMetaSubst.ppmetasenv [] real_menv);
       let subst_side_effects,real_menv,_ = 
-        let fail t s = raise (ProofEngineTypes.Fail (lazy (t^Lazy.force s))) in
-        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
+          CicUnification.fo_unif_subst [] context real_menv
+           goal_ty type_of_goal CicUniv.empty_ugraph
         with
         | CicUnification.UnificationFailure s
         | CicUnification.Uncertain s 
-        | CicUnification.AssertFailure s -> 
-            fail "Maybe the local context of metas in the goal was not an IRL" s
+        | CicUnification.AssertFailure s -> assert false
+(*            fail "Maybe the local context of metas in the goal was not an IRL" s *)
       in
       let final_subst = 
         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
       in
-(* prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); *)
-      let _ = 
-        try
-          CicTypeChecker.type_of_aux' real_menv context goal_proof
-            CicUniv.empty_ugraph
-        with 
-        | CicUtil.Meta_not_found _ 
-        | CicTypeChecker.TypeCheckerFailure _ 
-        | CicTypeChecker.AssertFailure _ 
-        | Invalid_argument "list_fold_left2" as exn ->
-            prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-            prerr_endline (CicPp.pp goal_proof names); 
-            prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-            raise exn
-      in
-
+(*
       let metas_of_proof = Utils.metas_of_term goal_proof in
-
+*)
       let proof, real_metasenv = 
         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
-          proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
+          proof goalno (CicMetaSubst.apply_subst final_subst) 
+         (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
       in
-      let open_goals = 
+      let open_goals =
+       List.map (fun i,_,_ -> i) real_metasenv in
+
+(*
         HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof) 
-      in
+      in *)
 (*
         match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] 
       in
@@ -1393,7 +1513,7 @@ let build_proof
 *)
       final_subst, proof, open_goals
 ;;
-
+*)
 
 (* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
 
@@ -1411,20 +1531,19 @@ let pump_actives context bag maxm active passive saturation_steps max_time =
   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 eq_uri = 
-    match LibraryObjects.eq_URI () with
-      | None -> assert false
-      | Some uri -> uri
-  in 
-  let env = [],context,CicUniv.empty_ugraph in
-  match 
-    given_clause bag eq_uri env ([],[]) passive active 0 saturation_steps max_time
-  with
-  | ParamodulationFailure (_,a,p) ->
-      a, p, !maxmeta
-  | ParamodulationSuccess _ ->
-      assert false
+  assert (maxm > max ma mp);
+  match LibraryObjects.eq_URI () with
+    | None -> active, passive, !maxmeta
+    | Some eq_uri -> 
+       let env = [],context,CicUniv.empty_ugraph in
+         (match 
+            given_clause bag eq_uri env ([],[]) 
+              passive active 0 saturation_steps max_time
+          with
+            | ParamodulationFailure (_,a,p) ->
+                a, p, !maxmeta
+            | ParamodulationSuccess _ ->
+                assert false)
 ;;
 
 let all_subsumed bag maxm status active passive =
@@ -1481,7 +1600,8 @@ let given_clause
   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 metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
+  let goal = [], metasenv', cleaned_goal in
   let env = metasenv,context,CicUniv.empty_ugraph in
   prerr_endline ">>>>>> ACTIVES >>>>>>>>"; 
   List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
index 81c84af35acf54b90e15429d58e0ea34a616bdb8..00d745fd906fb1ec2ac0aa6fa88a11faa17b7515 100644 (file)
@@ -98,6 +98,12 @@ let metas_of_term term =
     | C.Meta _ as t -> TermSet.singleton t
     | C.Appl l ->
         List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l
+    | C.Lambda(n,s,t) ->
+       TermSet.union (aux s) (aux t)
+    | C.Prod(n,s,t) ->
+       TermSet.union (aux s) (aux t)
+    | C.LetIn(n,s,t) ->
+       TermSet.union (aux s) (aux t)
     | t -> TermSet.empty (* TODO: maybe add other cases? *)
   in
   aux term
index 16c0d1cd39630f3a93e06c06c237f44a4f606380..3379fbe77b14503420f1954e65515250695ff773 100644 (file)
@@ -1,12 +1,17 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Oct 23 23:15:05 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
   dbd:HMysql.dbd ->
-  term:Cic.term -> params:(string * string) list -> ProofEngineTypes.tactic
+  term:Cic.term -> 
+  params:(string * string) list -> 
+  universe:Universe.universe -> 
+  ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
 val auto :
-  params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+  params:(string * string) list -> 
+  dbd:HMysql.dbd ->
+  universe:Universe.universe -> 
+  ProofEngineTypes.tactic
 val change :
   pattern:ProofEngineTypes.lazy_pattern ->
   Cic.lazy_term -> ProofEngineTypes.tactic