(* $Id$ *)
-open Inference;;
-open Utils;;
-
(* set to false to disable paramodulation inside auto_tac *)
+
let connect_to_auto = true;;
| ParamodulationSuccess of new_proof
;;
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term;;
+(* type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; *)
type theorem = Cic.term * Cic.term * Cic.metasenv;;
let symbols_of_equality equality =
let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in
- let m1 = symbols_of_term left in
+ let m1 = Utils.symbols_of_term left in
let m =
- TermMap.fold
+ Utils.TermMap.fold
(fun k v res ->
try
- let c = TermMap.find k res in
- TermMap.add k (c+v) res
+ let c = Utils.TermMap.find k res in
+ Utils.TermMap.add k (c+v) res
with Not_found ->
- TermMap.add k v res)
- (symbols_of_term right) m1
+ Utils.TermMap.add k v res)
+ (Utils.symbols_of_term right) m1
in
m
;;
| _ when (!symbols_counter > 0) ->
(symbols_counter := !symbols_counter - 1;
let cardinality map =
- TermMap.fold (fun k v res -> res + v) map 0
+ Utils.TermMap.fold (fun k v res -> res + v) map 0
in
let symbols =
let _, _, term = goal in
- symbols_of_term term
+ Utils.symbols_of_term term
in
let card = cardinality symbols in
let foldfun k v (r1, r2) =
- if TermMap.mem k symbols then
- let c = TermMap.find k symbols in
+ if Utils.TermMap.mem k symbols then
+ let c = Utils.TermMap.find k symbols in
let c1 = abs (c - v) in
let c2 = v - c1 in
r1 + c2, r2 + c1
in
let f equality (i, e) =
let common, others =
- TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+ Utils.TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
in
let c = others + (abs (common - card)) in
if c < i then (c, equality)
let e1 = EqualitySet.min_elt pos_set in
let initial =
let common, others =
- TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
+ Utils.TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
in
(others + (abs (common - card))), e1
in
in
let in_weight = round (howmany *. ratio /. (ratio +. 1.))
and in_age = round (howmany /. (ratio +. 1.)) in
- debug_print
+ Utils.debug_print
(lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
let counter = ref !symbols_ratio in
let rec pickw w ps =
in
(* we could also demodulate using passive. Currently we don't *)
let new_pos =
- List.map (demodulate Positive active_table) new_pos
+ List.map (demodulate Utils.Positive active_table) new_pos
in
let new_pos_set =
List.fold_left
let ress = EqualitySet.remove equality ress in
resl, ress, e::newn
in
- let pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
+ let pl, ps, newp = List.fold_right (f Utils.Positive) pl ([], ps, []) in
let passive_table =
List.fold_left
(fun tbl e -> Indexing.index tbl e) Indexing.empty pl
let prova eq_uri env new' active =
let given = List.filter is_commutative_law (fst active) in
let _ =
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "symmetric:\n%s\n"
(String.concat "\n"
match passive with
| None -> [], None
| Some ((pn, _), (pp, _), pt) ->
- let pn = List.map (fun e -> (Negative, e)) pn
- and pp = List.map (fun e -> (Positive, e)) pp in
+ let pn = List.map (fun e -> (Utils.Negative, e)) pn
+ and pp = List.map (fun e -> (Utils.Positive, e)) pp in
pn @ pp, Some pt
in
let a_theorems, p_theorems = theorems in
(fun t e -> Indexing.index t e)
Indexing.empty active
in
- let res = forward_simplify eq_uri env (Positive,e) (active, tbl) in
+ let res = forward_simplify eq_uri env (Utils.Positive,e) (active, tbl) in
match others with
| hd::tl -> (
match res with
;;
let simplify_equalities eq_uri env equalities =
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "equalities:\n%s\n"
(String.concat "\n"
(List.map Equality.string_of_equality equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
match equalities with
| [] -> []
| hd::tl ->
let res =
List.rev (simpl eq_uri env hd tl [])
in
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "equalities AFTER:\n%s\n"
(String.concat "\n"
;;
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 = Utils.names_of_context ctx in
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
when LibraryObjects.is_eq_URI uri ->
(let goal_equation =
Equality.mk_equality
- (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv)
+ (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)
in
(* match Indexing.subsumption env table goal_equation with*)
match Indexing.unification env table goal_equation with
let given_clause
eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
=
- let names = names_of_context context in
+ let names = Utils.names_of_context context in
let initial_time = Unix.gettimeofday () in
let iterations_left iterno =
let now = Unix.gettimeofday () in
in
(* SIMPLIFICATION OF CURRENT *)
let res =
- forward_simplify eq_uri env (Positive, current) active
+ forward_simplify eq_uri env (Utils.Positive, current) active
in
match res with
| None -> step goals theorems passive active (iterno+1)
(active, passive)
else
let current, passive = select env ([goal],[]) passive in
- let res = forward_simplify eq_uri env (Positive, current) ~passive active in
+ let res = forward_simplify eq_uri env (Utils.Positive, current) ~passive active in
match res with
| None ->
saturate_equations eq_uri env goal accept_fun passive active
| Some current ->
- debug_print (lazy (Printf.sprintf "selected: %s"
+ Utils.debug_print (lazy (Printf.sprintf "selected: %s"
(Equality.string_of_equality ~env current)));
let new' = infer eq_uri env current active in
let active =
in
let active, passive, new' = simplify new' active passive in
let _ =
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "active:\n%s\n"
(String.concat "\n"
(fst active)))))
in
let _ =
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "new':\n%s\n"
(String.concat "\n"
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 = find_equalities context proof in
+ let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities dbd context (proof, goal') (maxm+2)
+ 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
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty)));
Cic.Meta (maxm+1, irl),
let t1 = Unix.gettimeofday () in
let theorems =
if full then
- let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in
- let context_hyp = find_context_hypotheses env eq_indexes in
+ 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 =
[(t, ty, [])], []
in
let t2 = Unix.gettimeofday () in
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
let _ =
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf
"Theorems:\n-------------------------------------\n%s\n"
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" (print_metasenv metasenv);
+ Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
Printf.printf "\nequalities:\n%s\n"
(String.concat "\n"
(List.map
(* 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
+ let names = Utils.names_of_context context in
prerr_endline "OLD PROOF";
print_endline (PP.pp proof names);
prerr_endline "NEW PROOF";
let uri, metasenv, meta_proof, term_to_prove = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
- let names = names_of_context context in
- let eq_indexes, equalities, maxm = find_equalities context proof in
+ let names = Utils.names_of_context context in
+ let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
let cleaned_goal = Utils.remove_local_context type_of_goal in
let res, time =
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
+ Inference.find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
in
let library_equalities = List.map snd library_equalities in
let t2 = Unix.gettimeofday () in
let equalities =
simplify_equalities eq_uri env (equalities@library_equalities)
in
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
let t1 = Unix.gettimeofday () in
let theorems =
if full then
- let thms = find_library_theorems dbd env (proof, goalno) lib_eq_uris in
- let context_hyp = find_context_hypotheses env eq_indexes in
+ let thms = Inference.find_library_theorems dbd env (proof, goalno) lib_eq_uris in
+ let context_hyp = Inference.find_context_hypotheses env eq_indexes in
context_hyp @ thms, []
else
let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
in
let t2 = Unix.gettimeofday () in
let _ =
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf
"Theorems:\n-------------------------------------\n%s\n"
"Term: %s, type: %s"
(CicPp.ppterm t) (CicPp.ppterm ty))
(fst theorems)))));
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
in
let uri, metasenv, meta_proof, term_to_prove = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
let eq_uri = eq_of_goal type_of_goal in
- let eq_indexes, equalities, maxm = find_equalities context proof in
+ let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities false dbd context (proof, goal') (maxm+2) in
+ Inference.find_library_equalities false dbd context (proof, goal') (maxm+2) in
let t2 = Unix.gettimeofday () in
maxmeta := maxm+2;
let equalities = (* equalities @ *) library_equalities in
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "\n\nequalities:\n%s\n"
(String.concat "\n"
(* (string_of_equality e) *)
)
equalities))));
- debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
+ Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
let rec simpl e others others_simpl =
let (u, e) = e in
- let active = List.map (fun (u, e) -> (Positive, e))
+ let active = List.map (fun (u, e) -> (Utils.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 eq_uri env (Positive, e) (active, tbl) in
+ let res = forward_simplify eq_uri env (Utils.Positive, e) (active, tbl) in
match others with
| hd::tl -> (
match res with
match equalities with
| [] -> []
| hd::tl ->
- let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
+ let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
let res =
List.rev (simpl (*(Positive,*) hd others [])
in
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "\nequalities AFTER:\n%s\n"
(String.concat "\n"
)
res))));
res in
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
;;
let _, metasenv, meta_proof, _ = proof in
let _, context, goal = CicUtil.lookup_meta goal' metasenv in
let eq_uri = eq_of_goal goal in
- let eq_indexes, equalities, maxm = find_equalities context proof in
+ let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities false dbd context (proof, goal') (maxm+2)
+ Inference.find_library_equalities false 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
- debug_print
+ Utils.debug_print
(lazy
(Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
(CicPp.ppterm ty)));
let active = make_active () in
let passive = make_passive equalities in
Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
- Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
+ Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
Printf.printf "\nequalities:\n%s\n"
(String.concat "\n"
(List.map
print_newline ();
(*
with e ->
- debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
+ Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
*)
;;
*
* lists are coded using _ (example: H_H1_H2)
*)
+
let superposition_tac ~target ~table ~subterms_only ~demod_table status =
reset_refs();
Indexing.init_index ();
let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
let eq_uri,tty = eq_and_ty_of_goal ty in
let env = (metasenv, context, CicUniv.empty_ugraph) in
- let names = names_of_context context in
- let eq_index, equalities, maxm = find_equalities context proof in
+ let names = Utils.names_of_context context in
+ let eq_index, equalities, maxm = Inference.find_equalities context proof in
let eq_what =
let what = find_in_ctx 1 target context in
List.nth equalities (position_of 0 what eq_index)
projects / helm.git / commitdiff