let debug_print = Utils.debug_print;;
+(*
+for debugging
+let check_equation env equation msg =
+ let w, proof, (eq_ty, left, right, order), metas, args = equation in
+ let metasenv, context, ugraph = env in
+ let metasenv' = metasenv @ metas in
+ try
+ CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+ CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+ ()
+ with
+ CicUtil.Meta_not_found _ as exn ->
+ begin
+ prerr_endline msg;
+ prerr_endline (CicPp.ppterm left);
+ prerr_endline (CicPp.ppterm right);
+ raise exn
+ end
+*)
type retrieval_mode = Matching | Unification;;
Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
in
let left, right = if is_left then newterm, right else left, newterm in
- let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
+ let m =
+ (Inference.metas_of_term left)
+ @ (Inference.metas_of_term right)
+ @ (Inference.metas_of_term eq_ty) in
(* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *)
let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv')
and newargs = args
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
+ let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
let expansions, _ =
let term = if ordering = U.Gt then left else right in
betaexpand_term metasenv context ugraph table 0 term
let res =
let w = Utils.compute_equality_weight eq_ty left right in
- (w, newproof, (eq_ty, left, right, neworder), [], [])
+ (w, newproof, (eq_ty, left, right, neworder), menv @ menv', [])
in
res
in
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
'a * Inference.proof *
- (Index.key * Index.key * Index.key * Utils.comparison) * 'b * 'c ->
+ (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv * 'c ->
int *
(int * Inference.proof *
- (Index.key * Index.key * Index.key * Utils.comparison) * 'd list *
+ (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv *
'e list)
list
val superposition_right :
match do_find context term with
| Some p, newmeta ->
let tl, newmeta' = (aux (index+1) newmeta tl) in
- (index, p)::tl, max newmeta newmeta'
+ if newmeta' < newmeta then
+ prerr_endline "big trouble";
+ (index, p)::tl, newmeta' (* max???? *)
| None, _ ->
aux (index+1) newmeta tl
)
match res with
| Some e ->
let tl, newmeta' = aux newmeta tl in
- (uri, e)::tl, max newmeta newmeta'
+ if newmeta' < newmeta then
+ prerr_endline "big trouble";
+ (uri, e)::tl, newmeta' (* max???? *)
| None ->
aux newmeta tl
in
;;
-let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
let table = Hashtbl.create (List.length args) in
+
let newargs, newmeta =
List.fold_right
(fun t (newargs, index) ->
| _ -> assert false)
args ([], newmeta+1)
in
+
let repl where =
ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
~where
let ty = repl ty
and left = repl left
and right = repl right in
- let metas = (metas_of_term left) @ (metas_of_term right) in
+ let metas = (metas_of_term left) @ (metas_of_term right) @ (metas_of_term ty) in
let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
let newargs =
List.filter
| p -> assert false
in
let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
- (newmeta + 1, neweq)
+ (newmeta +1, neweq)
;;
+let relocate newmeta menv =
+ let subst, metasenv, newmeta =
+ List.fold_right
+ (fun (i, context, ty) (subst, menv, maxmeta) ->
+ let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
+ let newmeta = maxmeta, context, ty in
+ newsubst::subst, newmeta::menv, maxmeta+1)
+ menv ([], [], newmeta+1)
+ in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let subst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let term = CicMetaSubst.apply_subst subst term in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ (i, (context, term, ty))) subst in
+ subst, metasenv, newmeta
+
+
+let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+ (* debug
+ let _ , eq =
+ fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
+ prerr_endline (string_of_equality eq); *)
+ let subst, metasenv, newmeta = relocate newmeta menv in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ let left = CicMetaSubst.apply_subst subst left in
+ let right = CicMetaSubst.apply_subst subst right in
+ let args = List.map (CicMetaSubst.apply_subst subst) args in
+ let rec fix_proof = function
+ | NoProof -> NoProof
+ | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
+ | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
+ ProofBlock (subst' @ subst, eq_URI, namety, bo, (pos, eq), p)
+ | p -> assert false
+ in
+ let metas = (metas_of_term left)@(metas_of_term right)@(metas_of_term ty) in
+ let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
+ let eq = (w, fix_proof p, (ty, left, right, o), metasenv, args) in
+ (* debug prerr_endline (string_of_equality eq); *)
+ newmeta, eq
+
let term_is_equality term =
let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
match term with
open Inference;;
open Utils;;
+(*
+for debugging
+let check_equation env equation msg =
+ let w, proof, (eq_ty, left, right, order), metas, args = equation in
+ let metasenv, context, ugraph = env in
+ let metasenv' = metasenv @ metas in
+ try
+ CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+ CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+ ()
+ with
+ CicUtil.Meta_not_found _ as exn ->
+ begin
+ prerr_endline msg;
+ prerr_endline (CicPp.ppterm left);
+ prerr_endline (CicPp.ppterm right);
+ raise exn
+ end
+*)
(* set to false to disable paramodulation inside auto_tac *)
let connect_to_auto = true;;
let demodulate table current =
let newmeta, newcurrent =
- let _ =
- let w, proof, (eq_ty, left, right, order), metas, args = current in
- let metasenv, context, ugraph = env in
- let metasenv' = metasenv @ metas in
- try
- CicTypeChecker.type_of_aux' metasenv' context left ugraph;
- CicTypeChecker.type_of_aux' metasenv' context right ugraph;
- with
- CicUtil.Meta_not_found _ as exn ->
- begin
- prerr_endline "siamo in forward_simplify";
- prerr_endline (CicPp.ppterm left);
- prerr_endline (CicPp.ppterm right);
- raise exn
- end
- in
Indexing.demodulation_equality !maxmeta env table sign current in
maxmeta := newmeta;
if is_identity env newcurrent then
let demodulate sign table target =
let newmeta, newtarget =
- let _ =
- let w, proof, (eq_ty, left, right, order), metas, args = target in
- let metasenv, context, ugraph = env in
- let metasenv' = metasenv @ metas in
- try
- CicTypeChecker.type_of_aux' metasenv' context left ugraph;
- CicTypeChecker.type_of_aux' metasenv' context right ugraph;
- with
- CicUtil.Meta_not_found _ as exn ->
- begin
- prerr_endline "siamo in forward_simplify_new";
- prerr_endline (CicPp.ppterm left);
- prerr_endline (CicPp.ppterm right);
- raise exn
- end
- in
Indexing.demodulation_equality !maxmeta env table sign target in
maxmeta := newmeta;
newtarget
let new_neg, new_pos =
let new_neg = List.map (demodulate Negative active_table) new_neg
and new_pos = List.map (demodulate Positive active_table) new_pos in
+ new_neg,new_pos
+
+(* PROVA
match passive_table with
| None -> new_neg, new_pos
| Some passive_table ->
List.map (demodulate Negative passive_table) new_neg,
- List.map (demodulate Positive passive_table) new_pos
+ List.map (demodulate Positive passive_table) new_pos *)
in
let t2 = Unix.gettimeofday () in
let _, context, goal = CicUtil.lookup_meta goal' metasenv in
let eq_indexes, equalities, maxm = find_equalities context proof in
let lib_eq_uris, library_equalities, maxm =
+
find_library_equalities dbd context (proof, goal') (maxm+2)
in
let library_equalities = List.map snd library_equalities in
raise (ProofEngineTypes.Fail
(lazy "Found a proof, but it doesn't typecheck"))
in
+ let tall = fs_time_info.build_all in
+ let tdemodulate = fs_time_info.demodulate in
+ let tsubsumption = fs_time_info.subsumption in
debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
+ debug_print (lazy (Printf.sprintf "\ntall: %.9f" tall));
+ debug_print (lazy (Printf.sprintf "\ntdemod: %.9f" tdemodulate));
+ debug_print (lazy (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption));
+ debug_print (lazy (Printf.sprintf "\ninfer_time: %.9f" !infer_time));
+ debug_print (lazy (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time));
+ debug_print (lazy (Printf.sprintf "\nforward_simpl_new_times: %.9f" !forward_simpl_new_time));
+ debug_print (lazy (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time));
+ debug_print (lazy (Printf.sprintf "\npassive_maintainance_time: %.9f" !passive_maintainance_time));
newstatus
| _ ->
raise (ProofEngineTypes.Fail (lazy "NO proof found"))
(* $Id$ *)
-let debug = false;;
+let debug = true;;
let debug_print s = if debug then prerr_endline (Lazy.force s);;
(* settable by the user... *)
-(* let compare_terms = ref nonrec_kbo;; *)
+let compare_terms = ref nonrec_kbo;;
(* let compare_terms = ref ao;; *)
-let compare_terms = ref rpo;;
+(* let compare_terms = ref rpo;; *)
let guarded_simpl ?(debug=false) context t =
- let t' = ProofEngineReduction.simpl context t in
- if t = t' then t else
- begin
- let simpl_order = !compare_terms t t' in
- if debug then
- prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t'));
- if simpl_order = Gt then (if debug then prerr_endline "GT";t')
- else (if debug then prerr_endline "NO_GT";t)
- end
+ if !compare_terms == nonrec_kbo then t
+ else
+ let t' = ProofEngineReduction.simpl context t in
+ if t = t' then t else
+ begin
+ let simpl_order = !compare_terms t t' in
+ if debug then
+ prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t'));
+ if simpl_order = Gt then (if debug then prerr_endline "GT";t')
+ else (if debug then prerr_endline "NO_GT";t)
+ end
;;
type equality_sign = Negative | Positive;;
projects / helm.git / commitdiff