]> matita.cs.unibo.it Git - helm.git/commitdiff
existential variables in goal supported
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 18 May 2006 11:06:40 +0000 (11:06 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 18 May 2006 11:06:40 +0000 (11:06 +0000)
components/tactics/paramodulation/equality.ml
components/tactics/paramodulation/equality.mli
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/saturation.ml
components/tactics/paramodulation/subst.ml
components/tactics/paramodulation/subst.mli
components/tactics/paramodulation/utils.ml

index b6c3dc66a6625ec2e2ba92043e5108d6375f501d..34b69718f50413569c247ce90d7d443a44240017 100644 (file)
@@ -465,18 +465,19 @@ let pp_proof names goalproof proof =
       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
 ;;
 
-let build_goal_proof l initial ty =
-  let proof = 
+let build_goal_proof l initial ty se =
+  let se = List.map (fun i -> Cic.Meta (i,[])) se in 
+  let proof,se = 
    List.fold_left 
-   (fun  current_proof (pos,id,subst,pred) -> 
+   (fun (current_proof,se) (pos,id,subst,pred) -> 
       let p,l,r = proof_of_id id in
       let p = build_proof_term p in
       let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
-        build_proof_step subst current_proof p pos l r pred)
-   initial l
+        build_proof_step subst current_proof p pos l r pred,
+        List.map (fun x -> Subst.apply_subst subst x) se)
+   (initial,se) l
   in
-  proof 
-  (*canonical (contextualize_rewrites proof ty)*)
+  canonical (contextualize_rewrites proof ty), se
 ;;
 
 let refl_proof ty term = 
@@ -486,8 +487,9 @@ let refl_proof ty term =
        ty; term]
 ;;
 
-let metas_of_proof p = 
-  Utils.metas_of_term (build_proof_term p)
+let metas_of_proof p =
+  let p = build_proof_term p in
+  Utils.metas_of_term p
 ;;
 
 let relocate newmeta menv =
@@ -520,7 +522,7 @@ let fix_metas newmeta eq =
   let fix_proof = function
     | Exact p -> Exact (Subst.apply_subst subst p)
     | Step (s,(r,id1,(pos,id2),pred)) -> 
-        Step (Subst.concat_substs s subst,(r,id1,(pos,id2), pred))
+        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
index d2c58041d680089c804b6ef90a29c03ecbb9bbf9..c86cbdeaccb0114af41db35d3389121a7043902a 100644 (file)
@@ -57,10 +57,14 @@ val compare : equality -> equality -> int
 val string_of_equality : ?env:Utils.environment -> equality -> string
 val string_of_proof : 
   ?names:(Cic.name option)list -> proof -> goal_proof -> string
-val build_proof_term: proof -> Cic.term 
+val build_proof_term: 
+  proof -> Cic.term
+(* 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 [goal_proof] [initial_proof] [ty] 
  *  [ty] is the type of the goal *)
-val build_goal_proof: goal_proof -> Cic.term -> Cic.term-> Cic.term
+val build_goal_proof: 
+  goal_proof -> Cic.term -> Cic.term-> int list -> Cic.term * Cic.term list
 val refl_proof: Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality
index fd3caa345963398b86ef482ef920e57164f39e12..2c560cb55b7e7cf5a975d1a0fdb0e6b3337907d1 100644 (file)
@@ -437,20 +437,9 @@ let subsumption_aux use_unification env table target =
         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
         try
           let other = if pos = Utils.Left then r else l in
+          let what' = Subst.apply_subst subst what in
           let subst', menv', ug' =
-            let t1 = Unix.gettimeofday () in
-            try
-              let other = Subst.apply_subst subst other in
-              let r = unif_fun metasenv m context what other ugraph in 
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
-              r
-            with 
-              | Inference.MatchingFailure 
-              | CicUnification.UnificationFailure _ as e ->
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
-              raise e
+            unif_fun metasenv m context what' other ugraph
           in
           (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok what tl
index 351bc11bd0b88f67def8add7000da426cb418c4a..b93f6b09195885db698ba6e053b40b1f1ea8695c 100644 (file)
@@ -142,10 +142,10 @@ let age_factor = 0.01;;
    of weight, age and goal-similarity
 *)
 
-let rec select env goals passive =
+let rec select env (goals,_) passive =
   processed_clauses := !processed_clauses + 1;
   let goal =
-    match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
+    match (List.rev goals) with goal::_ -> goal | _ -> assert false
   in
   let (pos_list, pos_set), passive_table = passive in
   let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
@@ -654,25 +654,15 @@ let simplify_goals env goals ?passive active =
   let a_goals, p_goals = goals in
   let p_goals = 
     List.map
-      (fun (d, gl) ->
-         let gl =
-           List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
-         d, gl)
+      (fun g -> snd (simplify_goal env g ?passive active))
       p_goals
   in
-  let goals =
-    List.fold_left
-      (fun (a, p) (d, gl) ->
-         let changed = ref false in
-         let gl =
-           List.map
-             (fun g ->
-                let c, g = simplify_goal env g ?passive active in
-                changed := !changed || c; g) gl in
-         if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
-      ([], p_goals) a_goals
+  let a_goals = 
+    List.map
+      (fun g -> snd (simplify_goal env g ?passive active))
+      a_goals
   in
-  goals
+  a_goals, p_goals
 ;;
 
 
@@ -718,8 +708,6 @@ let backward_simplify_active env new_pos new_table min_weight active =
          else eq::p)
       newa []
   in
-  if List.length active1 <> List.length (fst active) then
-    prerr_endline "\n\n\nMANCAVANO DELLE PRUNED!!!!\n\n\n";
   match newa with
   | [] -> (active1,tbl), None, pruned 
   | _ -> (active1,tbl), Some newa, pruned
@@ -843,6 +831,9 @@ let make_goals goal =
   active, passive
 ;;
 
+let make_goal_set goal = 
+  ([],[goal]) 
+;;
 
 (** initializes the set of theorems *)
 let make_theorems theorems =
@@ -957,8 +948,8 @@ let print_goals goals =
 ;;
 
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-  let names = names_of_context ctx in
-  Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
+(*  let names = names_of_context ctx in*)
+(*  Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);*)
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
@@ -966,8 +957,8 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
          Equality.mk_equality
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) 
       in
-      match Indexing.subsumption env table goal_equation with
-(*       match Indexing.unification env table goal_equation with *)
+(*      match Indexing.subsumption env table goal_equation with*)
+       match Indexing.unification env table goal_equation with 
         | Some (subst, equality ) ->
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
@@ -982,11 +973,18 @@ let counter = ref 0
 let rec given_clause_fullred dbd env goals theorems ~passive active =
   let goals = simplify_goals env goals ~passive active in 
   let _,context,_ = env in
-  let ok, goals = activate_goal goals in
+  let ok, (goals:
+    (Equality.goal_proof * Cic.metasenv * Cic.term) list * 
+    (Equality.goal_proof * Cic.metasenv * Cic.term) list) = activate_goal 
+    
+    (goals: 
+  (Equality.goal_proof * Cic.metasenv * Cic.term) list * 
+    (Equality.goal_proof * Cic.metasenv * Cic.term) list)
+  in
 (*   let theorems = simplify_theorems env theorems ~passive active in *)
   if ok then
     let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in 
-    let _, _, t = List.hd (snd (List.hd (fst goals))) in
+    let _, _, t = List.hd (fst goals) in
     let _ = prerr_endline ("goal activated = " ^ (CicPp.pp t names)) in
 (*     let _ = *)
 (*       debug_print *)
@@ -1003,12 +1001,12 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
     let ok, proof =
       (* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
       let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
-      match (fst goals) with
-        | (_,[goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_ 
+      match fst goals with
+        | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_ 
             when left = right && iseq uri -> 
             let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
             true, Some (goalproof, reflproof, Subst.empty_subst,m)
-        | (_, [goal])::_ ->
+        | goal::_ ->
             (match check_if_goal_is_subsumed env (snd active) goal with
             | None -> false,None
             | Some p ->
@@ -1122,7 +1120,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
   | true -> ParamodulationFailure ""
       (* given_clause_fullred dbd env goals theorems passive active  *)     
   | false ->
-      let current, passive = select env (fst goals) passive in
+      let current, passive = select env goals passive in
       prerr_endline 
         ("Selected = " ^ Equality.string_of_equality ~env current);
 (* ^ 
@@ -1270,27 +1268,25 @@ let rec check goal = function
 ;;
   
 let simplify_goal_set env goals passive active = 
-  (*
-  let supl_goals = 
-     (List.flatten 
-       (List.map (Indexing.superposition_left env (snd active)) 
-         goals))
-  in
-  *)
+  let active_goals, passive_goals = goals in 
   let simplified =
     HExtlib.filter_map 
       (fun g -> 
         match simplify_goal env g ~passive active with 
         | true, g -> Some g
         | false, g -> Some g)
-      goals
+      active_goals
   in
+  (simplified,passive_goals)
+        (*
   HExtlib.list_uniq ~eq:(fun (_,_,t1) (_,_,t2) -> t1 = t2)
     (List.sort (fun (_,_,t1) (_,_,t2) -> compare t1 t1)
       ((*goals @*) simplified))
+      *)
 ;;
 
 let check_if_goals_set_is_solved env active goals =
+  let active_goals, passive_goals = goals in 
   List.fold_left 
     (fun proof goal ->
       match proof with
@@ -1299,14 +1295,39 @@ let check_if_goals_set_is_solved env active goals =
           check goal [
             check_if_goal_is_identity env;
             check_if_goal_is_subsumed env (snd active)])
-    None goals
+    None active_goals
 ;;
 
-let size_of_goal_set = List.length;;
+let infer_goal_set env active goals = 
+  let active_goals, passive_goals = goals in
+  match passive_goals with
+  | [] -> goals
+  | hd::tl -> 
+      let selected = hd in
+      let passive_goals = tl in
+      let new' = Indexing.superposition_left env (snd active) selected in
+      selected::active_goals, passive_goals @ new'
+;;
+
+let infer_goal_set_with_current env current goals = 
+  let active_goals, passive_goals = goals in
+  let _,table,_ = build_table [current] in
+  active_goals,
+  List.fold_left 
+    (fun acc g ->
+      let new' = Indexing.superposition_left env table g in
+      acc @ new')
+    passive_goals active_goals
+;;
+
+
+
+let size_of_goal_set_a (l,_) = List.length l;;
+let size_of_goal_set_p (_,l) = List.length l;;
 
 (** given-clause algorithm with full reduction strategy: NEW implementation *)
 (* here goals is a set of goals in OR *)
-let given_clause
+let given_clause 
   ((_,context,_) as env) goals theorems passive active max_iterations max_time
 = 
   let initial_time = Unix.gettimeofday () in
@@ -1334,9 +1355,9 @@ let given_clause
           ParamodulationSuccess p
       | None -> 
           prerr_endline 
-            (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d\n"
+            (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n"
             iterno (size_of_active active) (size_of_passive passive)
-            (size_of_goal_set goals));
+            (size_of_goal_set_a goals) (size_of_goal_set_p goals));
           (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)  
           let passive =
             let selection_estimate = iterations_left iterno in
@@ -1355,7 +1376,8 @@ let given_clause
             ParamodulationFailure "No more passive" (* maybe this is a success! *)
           else
             begin
-              let current, passive = select env [1,goals] passive in
+              let goals = infer_goal_set env active goals in
+              let current, passive = select env goals passive in
               Printf.eprintf  "Selected = %s\n"
                 (Equality.string_of_equality ~env current);
               (* SIMPLIFICATION OF CURRENT *)
@@ -1367,6 +1389,7 @@ let given_clause
               | Some current ->
                   (* GENERATION OF NEW EQUATIONS *)
                   let new' = infer env current active in
+                  let goals = infer_goal_set_with_current env current goals in
                   let active = 
                     if Equality.is_identity env current then 
                       assert false 
@@ -1405,7 +1428,7 @@ let rec saturate_equations env goal accept_fun passive active =
   if !elapsed_time > !time_limit then
     (active, passive)
   else
-    let current, passive = select env [1, [goal]] passive in
+    let current, passive = select env ([goal],[]) passive in
     let res = forward_simplify env (Positive, current) ~passive active in
     match res with
     | None ->
@@ -1652,31 +1675,18 @@ let saturate
   maxdepth := depth;
   maxwidth := width;
 (*  CicUnification.unif_ty := false;*)
-  let proof, goal = status in
-  let goal' = goal in
+  let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove = proof in
-  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let names = names_of_context context in
   let eq_indexes, equalities, maxm = find_equalities context proof in
-  let new_meta_goal, metasenv, type_of_goal =
-    let irl =
-      CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
-    debug_print
-      (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
-    Cic.Meta (maxm+1, irl),
-    (maxm+1, context, ty)::metasenv,
-    ty
-  in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
-  prerr_endline 
-    ("METASENV DEL GOAL: " ^ CicMetaSubst.ppmetasenv [] metasenv );
-  let goal = [], metasenv, goal in
+  let goal = [], metasenv, type_of_goal in
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
-      find_library_equalities dbd context (proof, goal') (maxm+2)
+      find_library_equalities dbd context (proof, goalno) (maxm+2)
     in
     let library_equalities = List.map snd library_equalities in
     let t2 = Unix.gettimeofday () in
@@ -1688,7 +1698,7 @@ let saturate
     let t1 = Unix.gettimeofday () in
     let theorems =
       if full then
-        let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in
+        let thms = find_library_theorems dbd env (proof, goalno) lib_eq_uris in
         let context_hyp = find_context_hypotheses env eq_indexes in
         context_hyp @ thms, []
       else
@@ -1725,12 +1735,9 @@ let saturate
       let goals = make_goals goal in
       given_clause_fullred dbd env goals theorems passive active
 *)
-      let goals = [goal] in
+      let goals = make_goal_set goal in
       let max_iterations = 1000 in
-      let max_time = 
-        Unix.gettimeofday () +. 
-        600. (* minutes *)
-      in
+      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
       given_clause env goals theorems passive active max_iterations max_time 
     in
     let finish = Unix.gettimeofday () in
@@ -1742,153 +1749,88 @@ let saturate
   | ParamodulationSuccess 
     (goalproof,newproof,subsumption_subst, proof_menv) ->
       prerr_endline "OK, found a proof!";
-
-      prerr_endline "NEWPROOF";
-     (* prerr_endline (Equality.string_of_proof_new ~names newproof
-      * goalproof);*)
       prerr_endline (Equality.pp_proof names goalproof newproof);
-
-(*       assert false; *)
-      
-      (* generation of the proof *)
-      let cic_proof_new = 
-        Equality.build_goal_proof 
-          goalproof (Equality.build_proof_term newproof) type_of_goal
+      prerr_endline "ENDOFPROOFS";
+      (* generation of the CIC proof *)
+      let side_effects = 
+        List.filter (fun i -> i <> goalno)
+          (ProofEngineHelpers.compare_metasenvs 
+            ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
       in
-      let cic_proof_new = 
-        Subst.apply_subst subsumption_subst cic_proof_new 
+      let free_metas = 
+        List.filter (fun i -> i <> goalno)
+          (ProofEngineHelpers.compare_metasenvs 
+            ~oldmetasenv:metasenv ~newmetasenv:proof_menv)
       in
-      
-      (* replacing fake mets with real ones *)
-      let equality_for_replace i t1 =
-        match t1 with
-        | C.Meta (n, _) -> n = i
-        | _ -> false
+      let goal_proof, side_effects_t = 
+        let initial = Equality.build_proof_term newproof in
+        Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
-      let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in
-      prerr_endline "replacing metas (new)";
-      let newproof_menv, what, with_what,_ = 
-        let irl = mkirl context in
+      let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+      let side_effects_t = 
+        List.map (Subst.apply_subst subsumption_subst) side_effects_t
+      in
+      (* 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 = 
         List.fold_left 
           (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
                | None ->
-                   [i,context,ty], 
-                   (Cic.Meta(i,[]))::acc2, 
+                   [i,context,ty], (Cic.Meta(i,[]))::acc2, 
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
           ([],[],[],None) proof_menv 
       in
-      let cic_proof_new = ProofEngineReduction.replace_lifting
-              ~equality:(=)
-              ~what ~with_what
-              ~where:cic_proof_new
-      in
-
-      (* pp new/old proof *)
-(*      prerr_endline "NEWPROOFCIC";*)
-(*      prerr_endline (CicPp.pp cic_proof_new names); *)
-
-      (* generation of proof metasenv *)
-      let newmetasenv_new = metasenv@newproof_menv in
-      let newmetasenv_new =
-        let i1 =
-          match new_meta_goal with
-          | C.Meta (i, _) -> i | _ -> assert false
-        in
-        List.filter (fun (i, _, _) -> i <> i1 && i <> goal') newmetasenv_new
+      let replace where = 
+        ProofEngineReduction.replace_lifting 
+          ~equality:(=) ~what ~with_what ~where
       in
+      let goal_proof = replace goal_proof in
+        (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? 
+         * what mi pare buono, sostituisce solo le meta farlocche *)
+      let side_effects_t = List.map replace side_effects_t in
       (* check/refine/... build the new proof *)
-      let newstatus =
-        let cic_proof,newmetasenv,proof_menv,ty, ug =
-          let cic_proof_new,new_ty,newmetasenv_new,newug = 
-            try
-              (*
-               prerr_endline "refining ... (new) ";
-               CicRefine.type_of_aux' 
-                newmetasenv_new context cic_proof_new ugraph
-              *)
-              let ty,ug = 
-                prerr_endline "typechecking ... (new) ";
-                CicTypeChecker.type_of_aux' 
-                  newmetasenv_new context cic_proof_new ugraph
-              in
-              cic_proof_new, ty, newmetasenv_new, ug
-            with
-            | CicTypeChecker.TypeCheckerFailure s ->
-                prerr_endline "THE PROOF DOESN'T TYPECHECK!!!";
-                prerr_endline (Lazy.force s);
-                assert false
-            | CicRefine.RefineFailure s 
-            | CicRefine.Uncertain s 
-            | CicRefine.AssertFailure s -> 
-                prerr_endline "FAILURE IN REFINE";
-                prerr_endline (Lazy.force s);
-                assert false
-          in
-          if List.length newmetasenv_new <> 0 then
-            prerr_endline 
-              ("Some METAS are still open: "(* ^ CicMetaSubst.ppmetasenv
-               [] newmetasenv_new*));
-          cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug
-          (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *)
-        in
-        prerr_endline "FINAL PROOF";
-        prerr_endline (CicPp.pp cic_proof names);
-        prerr_endline "ENDOFPROOFS";
-        (*  
-        debug_print
-          (lazy
-             (Printf.sprintf
-                "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
-                (CicPp.pp type_of_goal names) (CicPp.pp ty names)
-                (string_of_bool
-                   (fst (CicReduction.are_convertible
-                           context type_of_goal ty ug)))));
-        *)
-        let real_proof =
-          ProofEngineReduction.replace
-            ~equality:equality_for_replace
-            ~what:[goal'] ~with_what:[cic_proof]
-            ~where:meta_proof
+      let replaced_goal = 
+        ProofEngineReduction.replace
+          ~what:side_effects ~with_what:side_effects_t
+          ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false)
+          ~where:type_of_goal
+      in
+      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
-        (*
-        debug_print
-          (lazy
-             (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
-                (match uri with Some uri -> UriManager.string_of_uri uri
-                 | None -> "")
-                (print_metasenv newmetasenv)
-                (CicPp.pp real_proof [](* names *))
-                (CicPp.pp term_to_prove names)));
-        *)
-        let open_goals = List.map (fun (i,_,_) -> i) proof_menv in
-        (uri, newmetasenv, real_proof, term_to_prove), open_goals
+        try
+          CicUnification.fo_unif_subst [] context (metasenv @ free_metas_menv)
+           replaced_goal 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
+      in
+      
+      let final_subst = 
+        (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
+      in
+      let proof, real_metasenv = 
+        ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+          proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
       in
-      if Utils.time then
-        begin
-          let tall = fs_time_info.build_all in
-          let tdemodulate = fs_time_info.demodulate in
-          let tsubsumption = fs_time_info.subsumption in
-          prerr_endline (
-            (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
-              (Printf.sprintf "\ntall: %.9f" tall) ^
-              (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
-              (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
-              (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
-              (Printf.sprintf "\nforward_simpl_times: %.9f" 
-                !forward_simpl_time) ^
-              (Printf.sprintf "\nforward_simpl_new_times: %.9f" 
-                !forward_simpl_new_time) ^
-              (Printf.sprintf "\nbackward_simpl_times: %.9f" 
-                !backward_simpl_time) ^
-              (Printf.sprintf "\npassive_maintainance_time: %.9f" 
-                 !passive_maintainance_time))
-        end;
-      newstatus 
+      let open_goals = 
+        match free_meta with Some (Cic.Meta (m,_)) -> [m] | _ -> [] 
+      in
+      Printf.eprintf 
+        "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" 
+          (String.concat ", " (List.map string_of_int open_goals))
+          (CicMetaSubst.ppmetasenv [] metasenv)
+          (CicMetaSubst.ppmetasenv [] real_metasenv);
+      prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
+      proof, open_goals
 ;;
 
 let retrieve_and_print dbd term metasenv ugraph = 
@@ -1901,18 +1843,8 @@ let retrieve_and_print dbd term metasenv ugraph =
   let proof, goals = status in
   let goal' = List.nth goals 0 in
   let uri, metasenv, meta_proof, term_to_prove = proof in
-  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+  let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
   let eq_indexes, equalities, maxm = find_equalities context proof in
-  let new_meta_goal, metasenv, type_of_goal =
-    let irl =
-      CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
-    debug_print
-      (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
-    Cic.Meta (maxm+1, irl),
-    (maxm+1, context, ty)::metasenv,
-    ty
-  in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in
   let t1 = Unix.gettimeofday () in
@@ -2086,8 +2018,8 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
   if newmeta != maxm then
     begin
       let opengoal = Cic.Meta(maxm,irl) in
-      let proofterm = 
-        Equality.build_goal_proof newproof opengoal ty in
+      let proofterm,_ = 
+        Equality.build_goal_proof newproof opengoal ty [] in
         let extended_metasenv = (maxm,context,newty)::metasenv in
         let extended_status = 
           (curi,extended_metasenv,pbo,pty),goal in
index f738d2f63354a343c82b0416d5cd6cb69f7e3ded..819472a15485c0314da6228a3374f300d67d7e94 100644 (file)
@@ -211,5 +211,6 @@ let merge_subst_if_possible = naif_merge_subst_if_possible;;
 
 let empty_subst = [];;
 
-let concat_substs x y = x @ y;;
+let concat x y = x @ y;;
+
 
index 3bbf7d00cb2f322b680d250f84f4e4fba6d18106..9c124d9633502900162b760365add3ee62a02f2f 100644 (file)
@@ -39,5 +39,4 @@ val is_in_subst : int -> substitution -> bool
 val merge_subst_if_possible: 
   substitution -> substitution -> 
     substitution option
-val concat_substs: substitution -> substitution -> substitution
-
+val concat: substitution -> substitution -> substitution
index 18ccd5f79b52c0fe471de74101b57698323868f5..6a32e25953f5afff5df75c0ce55058c246303a0c 100644 (file)
@@ -429,7 +429,6 @@ let compare_weights ?(normalize=false)
   | (m, _, n) when m > 0 && n > 0 ->
       Incomparable
   | _ -> assert false 
-
 ;;