-let main dbd full term metasenv ugraph = ()
-(*
-let main dbd full term metasenv ugraph =
- let module C = Cic in
- let module T = CicTypeChecker in
- let module PET = ProofEngineTypes in
- let module PP = CicPp in
- let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
- let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
- let proof, goals = status in
- let goal' = List.nth goals 0 in
- let _, metasenv, meta_proof, _ = proof in
- let _, context, goal = CicUtil.lookup_meta goal' metasenv in
- let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
- let lib_eq_uris, library_equalities, maxm =
-
- Inference.find_library_equalities dbd context (proof, goal') (maxm+2)
- in
- let library_equalities = List.map snd library_equalities in
- maxmeta := maxm+2; (* TODO ugly!! *)
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let new_meta_goal, metasenv, type_of_goal =
- let _, context, ty = CicUtil.lookup_meta goal' metasenv in
- Utils.debug_print
- (lazy
- (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty)));
- Cic.Meta (maxm+1, irl),
- (maxm+1, context, ty)::metasenv,
- ty
- in
- let env = (metasenv, context, ugraph) in
- let t1 = Unix.gettimeofday () in
- let theorems =
- if full then
- let theorems = Inference.find_library_theorems dbd env (proof, goal') lib_eq_uris in
- let context_hyp = Inference.find_context_hypotheses env eq_indexes in
- context_hyp @ theorems, []
- else
- let refl_equal =
- let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
- UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
- in
- let t = CicUtil.term_of_uri refl_equal in
- let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
- [(t, ty, [])], []
- in
- let t2 = Unix.gettimeofday () in
- Utils.debug_print
- (lazy
- (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
- let _ =
- Utils.debug_print
- (lazy
- (Printf.sprintf
- "Theorems:\n-------------------------------------\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (t, ty, _) ->
- Printf.sprintf
- "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty))
- (fst theorems)))))
- in
- (*try*)
- 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
- Printf.printf "\ncurrent goal: %s\n"
- (let _, _, g = goal in CicPp.ppterm g);
- Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
- Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
- Printf.printf "\nequalities:\n%s\n"
- (String.concat "\n"
- (List.map
- (Equality.string_of_equality ~env) equalities));
-(* (equalities @ library_equalities))); *)
- print_endline "--------------------------------------------------";
- let start = Unix.gettimeofday () in
- print_endline "GO!";
- start_time := Unix.gettimeofday ();
- let res =
- let goals = make_goals goal in
- (if !use_fullred then given_clause_fullred else given_clause_fullred)
- dbd env goals theorems passive active
- in
- let finish = Unix.gettimeofday () in
- let _ =
- match res with
- | ParamodulationFailure ->
- Printf.printf "NO proof found! :-(\n\n"
- | 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 = Utils.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 eq ->
- let (_, _, _, menv,_) = Equality.open_equality eq in
- m @ menv)
- metasenv equalities
- in
- let _ =
- (*try*)
- let ty, ug =
- CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
- in
- print_endline (string_of_float (finish -. start));
- Printf.printf
- "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
- (CicPp.pp type_of_goal names) (CicPp.pp ty names)
- (string_of_bool
- (fst (CicReduction.are_convertible
- context type_of_goal ty ug)));
- (*with e ->
- Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
- Printf.printf "MAXMETA USED: %d\n" !maxmeta;
- print_endline (string_of_float (finish -. start));*)
- in
- ()
-
- | ParamodulationSuccess None ->
- Printf.printf "Success, but no proof?!?\n\n"
- in
- if Utils.time then
- begin
- prerr_endline
- ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
- "forward_simpl_new_time: %.9f\n" ^^
- "backward_simpl_time: %.9f\n")
- !infer_time !forward_simpl_time !forward_simpl_new_time
- !backward_simpl_time) ^
- (Printf.sprintf "passive_maintainance_time: %.9f\n"
- !passive_maintainance_time) ^
- (Printf.sprintf " successful unification/matching time: %.9f\n"
- !Indexing.match_unif_time_ok) ^
- (Printf.sprintf " failed unification/matching time: %.9f\n"
- !Indexing.match_unif_time_no) ^
- (Printf.sprintf " indexing retrieval time: %.9f\n"
- !Indexing.indexing_retrieval_time) ^
- (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n"
- !Indexing.build_newtarget_time) ^
- (Printf.sprintf "derived %d clauses, kept %d clauses.\n"
- !derived_clauses !kept_clauses))
- end
-(*
- with exc ->
- print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
- raise exc
-*)
-;;
-*)
-