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 symbols_counter = ref 0;;
(* non-recursive Knuth-Bendix term ordering by default *)
-Utils.compare_terms := Utils.rpo;;
+(* Utils.compare_terms := Utils.rpo;; *)
(* Utils.compare_terms := Utils.nonrec_kbo;; *)
(* Utils.compare_terms := Utils.ao;; *)
type theorem = Cic.term * Cic.term * Cic.metasenv;;
-
-let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
+let symbols_of_equality (_, _, (_, left, right, _), _, _) =
let m1 = symbols_of_term left in
let m =
TermMap.fold
m
;;
-
module OrderedEquality = struct
type t = Inference.equality
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = active_list @ pl in
let t2 = Unix.gettimeofday () in
fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
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
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = if pl = [] then active_list else active_list @ pl in
let demodulate table goal =
let newmeta, newgoal =
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = if pl = [] then active_list else active_list @ pl in
let a_theorems, p_theorems = theorems in
let demodulate table theorem =
let newmeta, newthm =
;;
+let rec simpl env e others others_simpl =
+ let active = others @ others_simpl in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ Indexing.empty active
+ in
+ let res = forward_simplify env e (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl env hd tl others_simpl
+ | Some e -> simpl env hd tl (e::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> e::others_simpl
+ )
+;;
+
+let simplify_equalities env equalities =
+ debug_print
+ (lazy
+ (Printf.sprintf "equalities:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality equalities))));
+ debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = List.map (fun e -> (Positive, e)) tl in
+ let res =
+ List.rev (List.map snd (simpl env (Positive, hd) others []))
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "equalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality res))));
+ res
+;;
+
(* applies equality to goal to see if the goal can be closed *)
let apply_equality_to_goal env equality goal =
let module C = Cic in
let aux (goal, r) tl =
let propagate_subst subst (proof, metas, term) =
let rec repl = function
- | NoProof -> NoProof
+ | NoProof -> NoProof
| BasicProof t ->
BasicProof (CicMetaSubst.apply_subst subst t)
| ProofGoalBlock (p, pb) ->
al @ [(sign, current)], Indexing.index tbl current
in
let passive = add_to_passive passive new' in
- let (_, ns), (_, ps), _ = passive in
given_clause dbd env goals theorems passive active
| true, goal ->
let proof =
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
in
(*try*)
let goal = Inference.BasicProof new_meta_goal, [], goal in
- let equalities =
- let equalities = equalities @ library_equalities in
- debug_print
- (lazy
- (Printf.sprintf "equalities:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let active = others @ others_simpl in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify env e (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl (e::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> e::others_simpl
- )
- in
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = List.map (fun e -> (Positive, e)) tl in
- let res =
- List.rev (List.map snd (simpl (Positive, hd) others []))
- in
- debug_print
- (lazy
- (Printf.sprintf "equalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality res))));
- res
- 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 library_equalities = List.map snd library_equalities in
let t2 = Unix.gettimeofday () in
maxmeta := maxm+2;
- let equalities =
- let equalities = equalities @ library_equalities in
- debug_print
- (lazy
- (Printf.sprintf "equalities:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let active = others @ others_simpl in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify env e (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl (e::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> e::others_simpl
- )
- in
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = List.map (fun e -> (Positive, e)) tl in
- let res =
- List.rev (List.map snd (simpl (Positive, hd) others []))
- in
- debug_print
- (lazy
- (Printf.sprintf "equalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality res))));
- res
- in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
debug_print
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
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"))
let init () = ();;
-(* UGLY SIDE EFFECT...
-if connect_to_auto then (
- AutoTactic.paramodulation_tactic := saturate;
- AutoTactic.term_is_equality := Inference.term_is_equality;
-);;
-*)
-
let retrieve_and_print dbd term metasenv ugraph =
let module C = Cic in
let module T = CicTypeChecker in
in
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
- let goal = Inference.BasicProof new_meta_goal, [], goal in
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities dbd context (proof, goal') (maxm+2)
- in
+ find_library_equalities dbd context (proof, goal') (maxm+2) in
let t2 = Unix.gettimeofday () in
- maxmeta := maxm+2;
- let equalities =
- let equalities = (* equalities @ *) library_equalities in
- debug_print
- (lazy
- (Printf.sprintf "\n\nequalities:\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (u, e) ->
-(* Printf.sprintf "%s: %s" *)
- (UriManager.string_of_uri u)
-(* (string_of_equality e) *)
- )
- equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let (u, e) = e in
- let active = List.map (fun (u, e) -> (Positive, e))
- (others @ others_simpl) in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify env (Positive, e) (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> (u, (snd e))::others_simpl
- )
- in
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
- let res =
- List.rev (simpl (*(Positive,*) hd others [])
- in
- debug_print
- (lazy
- (Printf.sprintf "\nequalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (u, e) ->
- Printf.sprintf "%s: %s"
- (UriManager.string_of_uri u)
- (string_of_equality e)
- )
- res))));
- res
+ maxmeta := maxm+2;
+ let equalities = (* equalities @ *) library_equalities in
+ debug_print
+ (lazy
+ (Printf.sprintf "\n\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+(* Printf.sprintf "%s: %s" *)
+ (UriManager.string_of_uri u)
+(* (string_of_equality e) *)
+ )
+ equalities))));
+ debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ let rec simpl e others others_simpl =
+ let (u, e) = e in
+ let active = List.map (fun (u, e) -> (Positive, e))
+ (others @ others_simpl) in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ Indexing.empty active
in
- debug_print
- (lazy
- (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+ let res = forward_simplify env (Positive, e) (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> (u, (snd e))::others_simpl
+ )
+ in
+ let _equalities =
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
+ let res =
+ List.rev (simpl (*(Positive,*) hd others [])
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "\nequalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+ Printf.sprintf "%s: %s"
+ (UriManager.string_of_uri u)
+ (string_of_equality e)
+ )
+ res))));
+ res in
+ debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
;;
ty
in
let env = (metasenv, context, ugraph) in
- let t1 = Unix.gettimeofday () in
(*try*)
let goal = Inference.BasicProof new_meta_goal, [], goal in
- let equalities =
- let equalities = equalities @ library_equalities in
- debug_print
- (lazy
- (Printf.sprintf "equalities:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let active = others @ others_simpl in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify env e (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl (e::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> e::others_simpl
- )
- in
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = List.map (fun e -> (Positive, e)) tl in
- let res =
- List.rev (List.map snd (simpl (Positive, hd) others []))
- in
- debug_print
- (lazy
- (Printf.sprintf "equalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality res))));
- res
- in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
let active = make_active () in
let passive = make_passive [] equalities in
Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
(List.map
(string_of_equality ~env) equalities));
print_endline "--------------------------------------------------";
- let start = Unix.gettimeofday () in
print_endline "GO!";
start_time := Unix.gettimeofday ();
if !time_limit < 1. then time_limit := 60.;
let ra, rp =
saturate_equations env goal (fun e -> true) passive active
in
- let finish = Unix.gettimeofday () in
let initial =
List.fold_left (fun s e -> EqualitySet.add e s)
EqualitySet.empty equalities
in
- let addfun s e = EqualitySet.add e s
- (*
+ let addfun s e =
if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
- *)
in
let passive =
debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
*)
;;
+
+let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
+ let module I = Inference in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let eq_indexes, equalities, maxm = I.find_equalities context proof in
+ let lib_eq_uris, library_equalities, maxm =
+ I.find_library_equalities dbd context (proof, goal) (maxm+2) in
+ if library_equalities = [] then prerr_endline "VUOTA!!!";
+ 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 env = (metasenv, context, CicUniv.empty_ugraph) in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
+ let table =
+ List.fold_left
+ (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
+ in
+ if newmeta != maxm then
+ begin
+ let opengoal = Cic.Meta(maxm,irl) in
+ let proofterm =
+ Inference.build_proof_term ~noproof:opengoal newproof in
+ let extended_metasenv = (maxm,context,newty)::metasenv in
+ let extended_status =
+ (curi,extended_metasenv,pbo,pty),goal in
+ let (status,newgoals) =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm)
+ extended_status in
+ (status,maxm::newgoals)
+ end
+ else if newty = ty then
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+ else ProofEngineTypes.apply_tactic
+ (ReductionTactics.simpl_tac ~pattern)
+ initialstatus
+;;
+
+let demodulate_tac ~dbd ~pattern =
+ ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
+;;
projects / helm.git / blobdiff