X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=59b06ef2986e711d900a81d1588773b1df868d96;hb=a060ed37101ce0e97bc26af8d49ce2491471c60c;hp=5b5121e8677ea61a45642b6fd236302e9e4d6540;hpb=5bd00cfdff937c2bb6c257f9c28b00ca027103e0;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 5b5121e86..59b06ef29 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -70,16 +70,20 @@ let maxmeta = ref 0;; let maxdepth = ref 3;; let maxwidth = ref 3;; +type new_proof = + Equality.goal_proof * Equality.new_proof * Equality.substitution * Cic.metasenv +type old_proof = Equality.old_proof * Cic.metasenv type result = | ParamodulationFailure - | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option + | ParamodulationSuccess of (new_proof * old_proof) option ;; -type goal = proof * Cic.metasenv * Cic.term;; +type goal = (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Cic.term;; type theorem = Cic.term * Cic.term * Cic.metasenv;; -let symbols_of_equality (_, _, (_, left, right, _), _) = +let symbols_of_equality equality = + let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in let m1 = symbols_of_term left in let m = TermMap.fold @@ -96,14 +100,14 @@ let symbols_of_equality (_, _, (_, left, right, _), _) = (* griggio *) module OrderedEquality = struct - type t = Inference.equality + type t = Equality.equality let compare eq1 eq2 = - match meta_convertibility_eq eq1 eq2 with + match Equality.meta_convertibility_eq eq1 eq2 with | true -> 0 | false -> - let w1, _, (ty, left, right, _), m1 = eq1 - and w2, _, (ty', left', right', _), m2 = eq2 in + let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in + let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality eq2 in match Pervasives.compare w1 w2 with | 0 -> let res = (List.length m1) - (List.length m2) in @@ -142,7 +146,7 @@ let rec select env goals passive = 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 -> e <> eq) l in + let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in if !weight_age_ratio > 0 then weight_age_counter := !weight_age_counter - 1; match !weight_age_counter with @@ -192,7 +196,7 @@ let rec select env goals passive = let passive_table = Indexing.remove_index passive_table current in - current, + current, ((remove current pos_list, EqualitySet.remove current pos_set), passive_table)) | _ -> @@ -255,8 +259,6 @@ let prune_passive howmany (active, _) passive = and in_age = round (howmany /. (ratio +. 1.)) in debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); - let symbols, card = None, 0 - in let counter = ref !symbols_ratio in let rec pickw w ps = if w > 0 then @@ -264,7 +266,7 @@ let prune_passive howmany (active, _) passive = let _ = counter := !counter - 1; if !counter = 0 then counter := !symbols_ratio in - let e = EqualitySet.min_elt ps in + let e = EqualitySet.min_elt ps in let ps' = pickw (w-1) (EqualitySet.remove e ps) in EqualitySet.add e ps' else @@ -300,7 +302,7 @@ let prune_passive howmany (active, _) passive = (** inference of new equalities between current and some in active *) -let infer env current ((active_list:Inference.equality list), active_table) = +let infer env current (active_list, active_table) = let (_,c,_) = env in if Utils.debug_metas then (ignore(Indexing.check_target c current "infer1"); @@ -325,9 +327,9 @@ let infer env current ((active_list:Inference.equality list), active_table) = (function current -> Indexing.check_target c current "sup2") res); let pos = infer_positive table tl in - res @ pos + res @ pos in - let maxm, copy_of_current = Inference.fix_metas !maxmeta current in + let maxm, copy_of_current = Equality.fix_metas !maxmeta current in maxmeta := maxm; let curr_table = Indexing.index Indexing.empty current in let pos = infer_positive curr_table (copy_of_current::active_list) @@ -336,7 +338,7 @@ let infer env current ((active_list:Inference.equality list), active_table) = ignore(List.map (function current -> Indexing.check_target c current "sup3") pos); - res @ pos + res @ pos in derived_clauses := !derived_clauses + (List.length new_pos); match !maximal_retained_equality with @@ -365,7 +367,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) = let newmeta, newcurrent = Indexing.demodulation_equality !maxmeta env table sign current in maxmeta := newmeta; - if is_identity env newcurrent then + if Equality.is_identity env newcurrent then (* debug_print *) (* (lazy *) (* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) @@ -396,7 +398,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) = match demodulate passive_table newcurrent with | None -> None | Some newnewcurrent -> - if newcurrent <> newnewcurrent then + if Equality.compare newcurrent newnewcurrent <> 0 then demod newnewcurrent else Some newnewcurrent in @@ -404,6 +406,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) = match res with | None -> None | Some c -> + (* immagino non funzioni piu'... *) if Indexing.in_index active_table c then None else @@ -471,7 +474,7 @@ let forward_simplify_new env new_pos ?passive active = let new_pos_set = List.fold_left (fun s e -> - if not (Inference.is_identity env e) then + if not (Equality.is_identity env e) then if EqualitySet.mem e s then s else EqualitySet.add e s else s) @@ -510,12 +513,11 @@ let rec simplify_goal env goal ?passive (active_list, active_table) = | None -> None | Some ((_, _), pt) -> Some pt in - let demodulate table goal = - let newmeta, newgoal = + let changed, newmeta, newgoal = Indexing.demodulation_goal !maxmeta env table goal in maxmeta := newmeta; - goal <> newgoal, newgoal + changed, newgoal in let changed, goal = match passive_table with @@ -565,28 +567,28 @@ let backward_simplify_active env new_pos new_table min_weight active = let active_list, newa = List.fold_right (fun equality (res, newn) -> - let ew, _, _, _ = equality in + let ew, _, _, _,_ = Equality.open_equality equality in if ew < min_weight then equality::res, newn else match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with | None -> res, newn | Some e -> - if equality = e then + if Equality.compare equality e = 0 then e::res, newn else res, e::newn) active_list ([], []) in let find eq1 where = - List.exists (meta_convertibility_eq eq1) where + List.exists (Equality.meta_convertibility_eq eq1) where in let active, newa = List.fold_right (fun eq (res, tbl) -> if List.mem eq res then res, tbl - else if (is_identity env eq) || (find eq res) then ( + else if (Equality.is_identity env eq) || (find eq res) then ( res, tbl ) else @@ -594,8 +596,8 @@ let backward_simplify_active env new_pos new_table min_weight active = active_list ([], Indexing.empty), List.fold_right (fun eq p -> - if (is_identity env eq) then p - else eq::p) + if (Equality.is_identity env eq) then p + else eq::p) newa [] in match newa with @@ -608,7 +610,7 @@ let backward_simplify_active env new_pos new_table min_weight active = let backward_simplify_passive env new_pos new_table min_weight passive = let (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = - let ew, _, _, _ = equality in + let ew, _, _, _ , _ = Equality.open_equality equality in if ew < min_weight then equality::resl, ress, newn else @@ -636,7 +638,7 @@ let backward_simplify env new' ?passive active = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> - let ew, _, _, _ = e in + let ew, _, _, _ , _ = Equality.open_equality e in e::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) new' in @@ -658,7 +660,7 @@ let close env new' given = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> - let ew, _, _, _ = e in + let ew, _, _, _ , _ = Equality.open_equality e in e::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) (snd new') in @@ -670,7 +672,9 @@ let close env new' given = ;; let is_commutative_law eq = - let w, proof, (eq_ty, left, right, order), metas = eq in + let w, proof, (eq_ty, left, right, order), metas , _ = + Equality.open_equality eq + in match left,right with Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> @@ -686,7 +690,7 @@ let prova env new' active = (Printf.sprintf "symmetric:\n%s\n" (String.concat "\n" (List.map - (fun e -> string_of_equality ~env e) + (fun e -> Equality.string_of_equality ~env e) given)))) in close env new' given ;; @@ -794,7 +798,7 @@ let simplify_equalities env equalities = (lazy (Printf.sprintf "equalities:\n%s\n" (String.concat "\n" - (List.map string_of_equality equalities)))); + (List.map Equality.string_of_equality equalities)))); debug_print (lazy "SIMPLYFYING EQUALITIES..."); match equalities with | [] -> [] @@ -806,7 +810,7 @@ let simplify_equalities env equalities = (lazy (Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" - (List.map string_of_equality res)))); + (List.map Equality.string_of_equality res)))); res ;; @@ -822,28 +826,42 @@ let print_goals goals = Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals)) ;; -let check_if_goal_is_subsumed env (proof,menv,ty) table = +let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table = match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when UriManager.eq uri (LibraryObjects.eq_URI ()) -> - (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in - match Indexing.subsumption env table goal_equation with - | Some (subst, (_,p,_,m)) -> - let p = Inference.apply_subst subst (Inference.build_proof_term p) in - let newp = - let rec repl = function - | Inference.ProofGoalBlock (_, gp) -> - Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp) - | Inference.NoProof -> Inference.BasicProof ([],p) - | Inference.BasicProof _ -> Inference.BasicProof ([],p) - | Inference.SubProof (t, i, p2) -> - Inference.SubProof (t, i, repl p2) - | _ -> assert false - in - repl proof - in - Some (newp,Inference.apply_subst_metasenv subst m @ menv) - | None -> None) + (let goal_equation = + Equality.mk_equality + (0,(Equality.Exact (Cic.Rel (-1)),proof),(eq_ty,left,right,Eq),menv) + in + match Indexing.subsumption env table goal_equation with + | Some (subst, equality ) -> + let (_,(np,p),(ty,l,r,_),m,id) = + Equality.open_equality equality in + let p = Equality.apply_subst subst + (Equality.build_proof_term_old p) in + let newp = + let rec repl = function + | Equality.ProofGoalBlock (_, gp) -> + Equality.ProofGoalBlock + (Equality.BasicProof (Equality.empty_subst,p), gp) + | Equality.NoProof -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.BasicProof _ -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.SubProof (t, i, p2) -> + Equality.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + let newcicp,np,subst,cicmenv = + cicproof,np, subst, (m @ menv) + in + Some + ((newcicp,np,subst,cicmenv), + (newp, Equality.apply_subst_metasenv subst m @ menv )) + | None -> None) | _ -> None ;; @@ -883,22 +901,31 @@ let rec given_clause_fullred dbd env goals theorems ~passive active = in let newp = let rec repl = function - | Inference.ProofGoalBlock (_, gp) -> - Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp) - | Inference.NoProof -> Inference.BasicProof ([],p) - | Inference.BasicProof _ -> Inference.BasicProof ([],p) - | Inference.SubProof (t, i, p2) -> - Inference.SubProof (t, i, repl p2) + | Equality.ProofGoalBlock (_, gp) -> + Equality.ProofGoalBlock + (Equality.BasicProof (Equality.empty_subst,p), gp) + | Equality.NoProof -> + + Equality.BasicProof (Equality.empty_subst,p) + | Equality.BasicProof _ -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.SubProof (t, i, p2) -> + Equality.SubProof (t, i, repl p2) | _ -> assert false in - repl proof - in true, Some (newp,m) + repl (snd proof) + in + let reflproof = Equality.refl_proof eq_ty left in + true, + Some ((fst proof,Equality.Exact reflproof, + Equality.empty_subst,m), + (newp,m)) | (_, [proof,m,ty])::_ -> (match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with | None -> false,None - | Some (newproof,m) -> + | Some p -> prerr_endline "Proof found by subsumption!"; - true, Some (newproof,m)) + true, Some p) | _ -> false, None in if ok then @@ -940,7 +967,6 @@ let rec given_clause_fullred dbd env goals theorems ~passive active = and given_clause_fullred_aux dbd env goals theorems passive active = prerr_endline (string_of_int !counter ^ " MAXMETA: " ^ string_of_int !maxmeta ^ - " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ " #ACTIVES: " ^ string_of_int (size_of_active active) ^ " #PASSIVES: " ^ string_of_int (size_of_passive passive)); incr counter; @@ -1008,7 +1034,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | false -> let current, passive = select env (fst goals) passive in prerr_endline - ("Selected = " ^ string_of_equality ~env current); + ("Selected = " ^ Equality.string_of_equality ~env current); (* ^ (let w,p,(t,l,r,o),m = current in " size w: " ^ string_of_int (HExtlib.estimate_size w)^ @@ -1029,8 +1055,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (* weight_age_counter := !weight_age_counter + 1; *) given_clause_fullred dbd env goals theorems passive active | Some current -> - debug_print (lazy (Printf.sprintf "selected: %s" - (string_of_equality ~env current))); + prerr_endline (Printf.sprintf "selected sipl: %s" + (Equality.string_of_equality ~env current)); let t1 = Unix.gettimeofday () in let new' = infer env current active in let _ = @@ -1040,12 +1066,12 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (String.concat "\n" (List.map (fun e -> "Positive " ^ - (string_of_equality ~env e)) new')))) + (Equality.string_of_equality ~env e)) new')))) in let t2 = Unix.gettimeofday () in infer_time := !infer_time +. (t2 -. t1); let active = - if is_identity env current then active + if Equality.is_identity env current then active else let al, tbl = active in al @ [current], Indexing.index tbl current @@ -1065,14 +1091,13 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | None, None -> active, passive, new' | Some p, None | None, Some p -> - let np = new' in - if Utils.debug_metas then - begin - List.iter - (fun x->Indexing.check_target context x "simplify1") - p; - end; - simplify (new' @ p) active passive + if Utils.debug_metas then + begin + List.iter + (fun x->Indexing.check_target context x "simplify1") + p; + end; + simplify (new' @ p) active passive | Some p, Some rp -> simplify (new' @ p @ rp) active passive in @@ -1105,7 +1130,7 @@ end prova *) (Printf.sprintf "active:\n%s\n" (String.concat "\n" ((List.map - (fun e -> (string_of_equality ~env e)) + (fun e -> (Equality.string_of_equality ~env e)) (fst active)))))) in let _ = @@ -1115,7 +1140,7 @@ end prova *) (String.concat "\n" ((List.map (fun e -> "Negative " ^ - (string_of_equality ~env e)) new'))))) + (Equality.string_of_equality ~env e)) new'))))) in let passive = add_to_passive passive new' in given_clause_fullred dbd env goals theorems passive active @@ -1142,10 +1167,10 @@ let rec saturate_equations env goal accept_fun passive active = saturate_equations env goal accept_fun passive active | Some current -> debug_print (lazy (Printf.sprintf "selected: %s" - (string_of_equality ~env current))); + (Equality.string_of_equality ~env current))); let new' = infer env current active in let active = - if is_identity env current then active + if Equality.is_identity env current then active else let al, tbl = active in al @ [current], Indexing.index tbl current @@ -1167,24 +1192,25 @@ let rec saturate_equations env goal accept_fun passive active = (Printf.sprintf "active:\n%s\n" (String.concat "\n" (List.map - (fun e -> string_of_equality ~env e) + (fun e -> Equality.string_of_equality ~env e) (fst active))))) in - let _ = + let _ = debug_print (lazy (Printf.sprintf "new':\n%s\n" (String.concat "\n" (List.map (fun e -> "Negative " ^ - (string_of_equality ~env e)) new')))) + (Equality.string_of_equality ~env e)) new')))) in let new' = List.filter accept_fun new' in let passive = add_to_passive passive new' in saturate_equations env goal accept_fun passive active ;; - +let main dbd full term metasenv ugraph = () +(* let main dbd full term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in @@ -1246,7 +1272,9 @@ let main dbd full term metasenv ugraph = (fst theorems))))) in (*try*) - let goal = Inference.BasicProof ([],new_meta_goal), [], goal in + let goal = + ([],Equality.BasicProof (Equality.empty_subst ,new_meta_goal)), [], goal + in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in @@ -1258,7 +1286,7 @@ let main dbd full term metasenv ugraph = Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map - (string_of_equality ~env) equalities)); + (Equality.string_of_equality ~env) equalities)); (* (equalities @ library_equalities))); *) print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in @@ -1274,17 +1302,27 @@ let main dbd full term metasenv ugraph = match res with | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" - | ParamodulationSuccess (Some (proof, env)) -> - let proof = Inference.build_proof_term proof in + | ParamodulationSuccess (Some ((cicproof,cicmenv),(proof, env))) -> Printf.printf "OK, found a proof!\n"; + let oldproof = Equation.build_proof_term proof in + let newproof,_,newenv,_ = + CicRefine.type_of_aux' + cicmenv context cicproof CicUniv.empty_ugraph + in (* REMEMBER: we have to instantiate meta_proof, we should use apply the "apply" tactic to proof and status *) let names = names_of_context context in + prerr_endline "OLD PROOF"; print_endline (PP.pp proof names); + prerr_endline "NEW PROOF"; + print_endline (PP.pp newproof names); let newmetasenv = List.fold_left - (fun m (_, _, _, menv) -> m @ menv) metasenv equalities + (fun m eq -> + let (_, _, _, menv,_) = Equality.open_equality eq in + m @ menv) + metasenv equalities in let _ = (*try*) @@ -1316,8 +1354,6 @@ let main dbd full term metasenv ugraph = "backward_simpl_time: %.9f\n") !infer_time !forward_simpl_time !forward_simpl_new_time !backward_simpl_time) ^ - (Printf.sprintf "beta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ (Printf.sprintf "passive_maintainance_time: %.9f\n" !passive_maintainance_time) ^ (Printf.sprintf " successful unification/matching time: %.9f\n" @@ -1337,14 +1373,13 @@ let main dbd full term metasenv ugraph = raise exc *) ;; - +*) let default_depth = !maxdepth and default_width = !maxwidth;; let reset_refs () = maxmeta := 0; - Indexing.local_max := 100; symbols_counter := 0; weight_age_counter := !weight_age_ratio; processed_clauses := 0; @@ -1358,10 +1393,50 @@ let reset_refs () = passive_maintainance_time := 0.; derived_clauses := 0; kept_clauses := 0; - Indexing.beta_expand_time := 0.; - Inference.metas_of_proof_time := 0.; + Equality.reset (); +;; + +let interactive_comparison context t1 t2 = + let rc = ref [] in + let module P = Printf in + let rec aux n context t1 t2 = +(* let names = names_of_context context in*) + let pp t1 t2 = () (* + P.eprintf "%s%s === %s\n" (String.make n ' ') + (CicPp.pp t1 names) (CicPp.pp t2 names) *) + in + match t1,t2 with + | _, Cic.Appl [Cic.Const(uri,_);t2] when + UriManager.eq uri (UriManager.uri_of_string + "cic:/Coq/Init/Logic/sym_eq.con")-> aux n context t1 t2 + | Cic.Implicit _, _ -> pp t1 t2 + | Cic.Meta (n,_), _ -> + rc := (n,t2,context) :: !rc; + pp (Cic.Meta(n,[])) t2 + | Cic.Rel n1, Cic.Rel n2 when n1 = n2 -> pp t1 t2 + | Cic.Appl l1,Cic.Appl l2 -> + if List.length l1 <> List.length l2 then + begin + prerr_endline "ERROR: application with diff num of args"; + pp t1 t2 + end + else + List.iter2 (aux (n+1) context) l1 l2 + | Cic.Lambda (name,s,t1),Cic.Lambda(_,_,t2) -> + let context = (Some (name,(Cic.Decl s)))::context in + aux (n+1) context t1 t2 + | Cic.Const (u1,_), Cic.Const (u2,_) when UriManager.eq u1 u2 -> + pp t1 t2 + | _,_ -> pp t1 t2 + in + aux 0 context t1 t2; + List.iter (fun (n,t,ctx) -> + let names = names_of_context ctx in + Printf.eprintf "%d := %s\n" n (CicPp.pp t names)) + (HExtlib.list_uniq (List.sort (fun (x,_,_) (y,_,_) -> x-y) !rc)) ;; + let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in @@ -1375,7 +1450,6 @@ let saturate let goal' = goal in let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in - prerr_endline ("CTX: " ^ string_of_int (HExtlib.estimate_size context)); let eq_indexes, equalities, maxm = find_equalities context proof in let new_meta_goal, metasenv, type_of_goal = let irl = @@ -1389,7 +1463,9 @@ let saturate in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in - let goal = Inference.BasicProof ([],new_meta_goal), [], goal in + let goal = + ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal + in let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = @@ -1445,20 +1521,31 @@ let saturate (res, finish -. start) in match res with - | ParamodulationSuccess (Some (proof, proof_menv)) -> + | ParamodulationSuccess + (Some ((goalproof,newproof,subsumption_subst, newproof_menv),(proof, proof_menv))) -> prerr_endline "OK, found a proof!"; - debug_print (lazy "OK, found a proof!"); - let proof = Inference.build_proof_term proof in + prerr_endline (Equality.string_of_proof_old proof); + + let cic_proof = Equality.build_proof_term_old proof in + + let cic_proof_new,cic_proof_new_menv = + Equality.build_goal_proof goalproof (Equality.build_proof_term_new newproof) + in + let newproof_menv = + Equality.apply_subst_metasenv subsumption_subst + (newproof_menv @ cic_proof_new_menv) + in + let cic_proof_new = Equality.apply_subst subsumption_subst cic_proof_new in + let equality_for_replace i t1 = match t1 with | C.Meta (n, _) -> n = i | _ -> false in - prerr_endline "replacing metas"; + let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in + prerr_endline "replacing metas (old)"; let proof_menv, what, with_what = - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in + let irl = mkirl context in List.fold_left (fun (acc1,acc2,acc3) (i,_,ty) -> (i,context,ty)::acc1, @@ -1466,13 +1553,35 @@ let saturate (Cic.Meta(i,irl)) ::acc3) ([],[],[]) proof_menv in - let proof = ProofEngineReduction.replace_lifting + let cic_proof = ProofEngineReduction.replace_lifting + ~equality:(=) + ~what ~with_what + ~where:cic_proof + in + prerr_endline "replacing metas (new)"; + let newproof_menv, what, with_what = + let irl = mkirl context in + List.fold_left + (fun (acc1,acc2,acc3) (i,_,ty) -> + (i,context,ty)::acc1, + (Cic.Meta(i,[]))::acc2, + (Cic.Meta(i,irl)) ::acc3) + ([],[],[]) newproof_menv + in + let cic_proof_new = ProofEngineReduction.replace_lifting ~equality:(=) ~what ~with_what - ~where:proof + ~where:cic_proof_new in - (* prerr_endline (CicPp.ppterm proof); *) let names = names_of_context context in + prerr_endline "OLDPROOF"; + prerr_endline (Equality.string_of_proof_old proof); + prerr_endline "OLDPROOFCIC"; + prerr_endline (CicPp.pp cic_proof names); + prerr_endline "NEWPROOF"; + prerr_endline (Equality.string_of_proof_new ~names newproof goalproof); + prerr_endline "NEWPROOFCIC"; + prerr_endline (CicPp.pp cic_proof_new names); let newmetasenv = let i1 = match new_meta_goal with @@ -1481,13 +1590,70 @@ let saturate List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv in let newmetasenv = newmetasenv@proof_menv in + let newmetasenv_new = newmetasenv@newproof_menv in let newstatus = try - let ty, ug = - prerr_endline "type checking ... "; - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph + let cic_proof,newmetasenv,proof_menv,ty, ug = + prerr_endline "type checking ... (old) "; +(* let old_ty, oldug = *) +(* CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph *) +(* in*) + 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 "FAILURE IN TYPECHECKING"; + 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); + interactive_comparison context cic_proof_new cic_proof; + assert false + in +(* + prerr_endline "check unif ... (old vs new) "; + (try + ignore(CicUnification.fo_unif + newmetasenv_new context cic_proof_new cic_proof CicUniv.empty_ugraph) + with CicUnification.UnificationFailure _ -> + prerr_endline "WARNING, new and old proofs are not unifiable"); + prerr_endline "unif ... (new) "; + let subst, newmetasenv_new, newug = + CicUnification.fo_unif + newmetasenv_new context new_ty type_of_goal newug + in + if subst <> [] then + prerr_endline "UNIF SERVE ################################"; +*) + let subst = [] in + if List.length newmetasenv_new <> 0 then + prerr_endline + ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv + [] newmetasenv_new); + (CicMetaSubst.apply_subst subst cic_proof_new), + newmetasenv_new, + (CicMetaSubst.apply_subst_metasenv subst newmetasenv_new), + (CicMetaSubst.apply_subst subst new_ty), + newug +(* cic_proof,newmetasenv,proof_menv,oldty,oldug*) in - prerr_endline (CicPp.pp proof [](* names *)); + prerr_endline "FINAL PROOF"; + prerr_endline (CicPp.pp cic_proof names); + prerr_endline "ENDOFPROOFS"; + debug_print (lazy (Printf.sprintf @@ -1499,7 +1665,7 @@ let saturate let real_proof = ProofEngineReduction.replace ~equality:equality_for_replace - ~what:[goal'] ~with_what:[proof] + ~what:[goal'] ~with_what:[cic_proof] ~where:meta_proof in debug_print @@ -1514,7 +1680,7 @@ let saturate List.map (fun (i,_,_) -> i) proof_menv) with CicTypeChecker.TypeCheckerFailure _ -> debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!"); - debug_print (lazy (CicPp.pp proof names)); + debug_print (lazy (CicPp.pp cic_proof names)); raise (ProofEngineTypes.Fail (lazy "Found a proof, but it doesn't typecheck")) in @@ -1529,10 +1695,6 @@ let saturate (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ - (Printf.sprintf "\nbeta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ - (Printf.sprintf "\nmetas_of_proof: %.9f\n" - !Inference.metas_of_proof_time) ^ (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ (Printf.sprintf "\nforward_simpl_new_times: %.9f" !forward_simpl_new_time) ^ @@ -1629,7 +1791,7 @@ let retrieve_and_print dbd term metasenv ugraph = (fun (u, e) -> Printf.sprintf "%s: %s" (UriManager.string_of_uri u) - (string_of_equality e) + (Equality.string_of_equality e) ) res)))); res in @@ -1669,7 +1831,9 @@ let main_demod_equalities dbd term metasenv ugraph = in let env = (metasenv, context, ugraph) in (*try*) - let goal = Inference.BasicProof ([],new_meta_goal), [], goal in + let goal = + ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal + in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in let passive = make_passive equalities in @@ -1678,7 +1842,7 @@ let main_demod_equalities dbd term metasenv ugraph = Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map - (string_of_equality ~env) equalities)); + (Equality.string_of_equality ~env) equalities)); print_endline "--------------------------------------------------"; print_endline "GO!"; start_time := Unix.gettimeofday (); @@ -1705,12 +1869,12 @@ let main_demod_equalities dbd term metasenv ugraph = EqualitySet.elements (List.fold_left addfun EqualitySet.empty l) in Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n" - (String.concat "\n" (List.map (string_of_equality ~env) active)) + (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 (term_of_equality e)) passive)); + (List.map (fun e -> CicPp.ppterm (Equality.term_of_equality e)) passive)); print_newline (); (* with e -> @@ -1729,7 +1893,9 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in let goalterm = Cic.Meta (metano,irl) in - let initgoal = Inference.BasicProof ([],goalterm), [], ty in + let initgoal = + ([],Equality.BasicProof (Equality.empty_subst,goalterm)), [], ty + in let env = (metasenv, context, CicUniv.empty_ugraph) in let equalities = simplify_equalities env (equalities@library_equalities) in let table = @@ -1737,14 +1903,15 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = (fun tbl eq -> Indexing.index tbl eq) Indexing.empty equalities in - let newmeta,(newproof,newmetasenv, newty) = Indexing.demodulation_goal - maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal + let _, newmeta,(newproof,newmetasenv, newty) = + Indexing.demodulation_goal + maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal in if newmeta != maxm then begin let opengoal = Cic.Meta(maxm,irl) in let proofterm = - Inference.build_proof_term ~noproof:opengoal newproof in + Equality.build_proof_term_old ~noproof:opengoal (snd newproof) in let extended_metasenv = (maxm,context,newty)::metasenv in let extended_status = (curi,extended_metasenv,pbo,pty),goal in