(*
+(* NO INDEXING *)
+let empty_table () = []
+
+let index table equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> (Utils.Left, equality)::table
+ | Utils.Lt -> (Utils.Right, equality)::table
+ | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
+;;
+
+let remove_index table equality =
+ List.filter (fun (p, e) -> e != equality) table
+;;
+
+let in_index table equality =
+ List.exists (fun (p, e) -> e == equality) table
+;;
+
+let get_candidates mode table term = table
+*)
+
+
+(*
+(* PATH INDEXING *)
let empty_table () =
Path_indexing.PSTrie.empty
;;
*)
+(* DISCRIMINATION TREES *)
let empty_table () =
Discrimination_tree.DiscriminationTree.empty
;;
let match_unif_time_no = ref 0.;;
-let rec find_matches metasenv context ugraph lift_amount term =
+let rec find_matches metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let cmp = !Utils.compare_terms in
- let names = Utils.names_of_context context in
- let termty, ugraph =
- CicTypeChecker.type_of_aux' metasenv context term ugraph
- in
+(* let names = Utils.names_of_context context in *)
+(* let termty, ugraph = *)
+(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+(* in *)
function
| [] -> None
| candidate::tl ->
let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
- if not (fst (CicReduction.are_convertible
- ~metasenv context termty ty ugraph)) then (
- debug_print (
- Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found"
- (CicPp.pp termty names) (CicPp.pp ty names));
- find_matches metasenv context ugraph lift_amount term tl
- ) else
+(* if not (fst (CicReduction.are_convertible *)
+(* ~metasenv context termty ty ugraph)) then ( *)
+(* (\* debug_print ( *\) *)
+(* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
+(* (\* (CicPp.pp termty names) (CicPp.pp ty names)); *\) *)
+(* find_matches metasenv context ugraph lift_amount term termty tl *)
+(* ) else *)
let do_match c other eq_URI =
let subst', metasenv', ugraph' =
let t1 = Unix.gettimeofday () in
try
do_match c other eq_URI
with Inference.MatchingFailure ->
- find_matches metasenv context ugraph lift_amount term tl
+ find_matches metasenv context ugraph lift_amount term termty tl
else
let res =
try do_match c other eq_URI
if order = U.Gt then
res
else
- find_matches metasenv context ugraph lift_amount term tl
+ find_matches
+ metasenv context ugraph lift_amount term termty tl
| None ->
- find_matches metasenv context ugraph lift_amount term tl
+ find_matches metasenv context ugraph lift_amount term termty tl
;;
let rec find_all_matches ?(unif_fun=Inference.unification)
- metasenv context ugraph lift_amount term =
+ metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let cmp = !Utils.compare_terms in
- let names = Utils.names_of_context context in
- let termty, ugraph =
- CicTypeChecker.type_of_aux' metasenv context term ugraph
- in
+(* let names = Utils.names_of_context context in *)
+(* let termty, ugraph = *)
+(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+(* in *)
function
| [] -> []
| candidate::tl ->
let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
- if not (fst (CicReduction.are_convertible
- ~metasenv context termty ty ugraph)) then (
- debug_print (
- Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found"
- (CicPp.pp termty names) (CicPp.pp ty names));
- find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl
- ) else
+(* if not (fst (CicReduction.are_convertible *)
+(* ~metasenv context termty ty ugraph)) then ( *)
+(* (\* debug_print ( *\) *)
+(* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
+(* (\* (CicPp.pp termty names) (CicPp.pp ty names)); *\) *)
+(* find_all_matches ~unif_fun metasenv context ugraph *)
+(* lift_amount term termty tl *)
+(* ) else *)
let do_match c other eq_URI =
let subst', metasenv', ugraph' =
let t1 = Unix.gettimeofday () in
try
let res = do_match c other eq_URI in
res::(find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl)
+ lift_amount term termty tl)
with
| Inference.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl
+ lift_amount term termty tl
else
try
let res = do_match c other eq_URI in
let names = U.names_of_context context in
if order <> U.Lt && order <> U.Le then
res::(find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl)
+ lift_amount term termty tl)
else
find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl
+ lift_amount term termty tl
with
| Inference.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl
+ lift_amount term termty tl
;;
| _ ->
let leftc = get_candidates Matching table left in
find_all_matches ~unif_fun:Inference.matching
- metasenv context ugraph 0 left leftc
+ metasenv context ugraph 0 left ty leftc
in
let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) =
try
| _ ->
let rightc = get_candidates Matching table right in
find_all_matches ~unif_fun:Inference.matching
- metasenv context ugraph 0 right rightc
+ metasenv context ugraph 0 right ty rightc
in
List.exists (ok left) rightr
;;
match term with
| C.Meta _ -> None
| term ->
+ let termty, ugraph =
+ C.Implicit None, ugraph
+(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+ in
let res =
- find_matches metasenv context ugraph lift_amount term candidates
+ find_matches metasenv context ugraph lift_amount term termty candidates
in
if res <> None then
res
match term with
| C.Meta _ -> res, lifted_term
| term ->
+ let termty, ugraph =
+ C.Implicit None, ugraph
+(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+ in
let r =
- find_all_matches metasenv context ugraph lift_amount term candidates
+ find_all_matches
+ metasenv context ugraph lift_amount term termty candidates
in
r @ res, lifted_term
;;
| Cic.Meta (i, l) -> check_irl 1 l
| Cic.Rel _ -> true
| Cic.Const _ -> true
+ | Cic.MutInd (_, _, []) -> true
+ | Cic.MutConstruct (_, _, _, []) -> true
| _ -> false
;;
let unification metasenv context t1 t2 ugraph =
(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
let subst, menv, ug =
- if not (is_simple_term t1) || not (is_simple_term t2) then
+ if not (is_simple_term t1) || not (is_simple_term t2) then (
+ debug_print (
+ Printf.sprintf "NOT SIMPLE TERMS: %s %s"
+ (CicPp.ppterm t1) (CicPp.ppterm t2));
CicUnification.fo_unif metasenv context t1 t2 ugraph
- else
+ ) else
unification_simple metasenv context t1 t2 ugraph
in
let rec fix_term = function
| None ->
aux newmeta tl
in
- aux maxmeta candidates
+ let found, maxm = aux maxmeta candidates in
+ (List.fold_left
+ (fun l e ->
+ if List.exists (meta_convertibility_eq e) l then (
+ debug_print (
+ Printf.sprintf "NO!! %s already there!" (string_of_equality e));
+ l
+ )
+ else e::l)
+ [] found), maxm
;;
let set_ratio v = S.weight_age_ratio := (v+1); S.weight_age_counter := (v+1)
and set_sel v = S.symbols_ratio := v; S.symbols_counter := v;
and set_conf f = configuration_file := f
- and set_lpo () = Utils.compare_terms := Utils.lpo
- and set_kbo () = Utils.compare_terms := Utils.nonrec_kbo
+ and set_ordering o =
+ match o with
+ | "lpo" -> Utils.compare_terms := Utils.lpo
+ | "kbo" -> Utils.compare_terms := Utils.kbo
+ | "nr-kbo" -> Utils.compare_terms := Utils.nonrec_kbo
+ | o -> raise (Arg.Bad ("Unknown term ordering: " ^ o))
and set_fullred b = S.use_fullred := b
and set_time_limit v = S.time_limit := float_of_int v
in
"-f", Arg.Bool set_fullred,
"Enable/disable full-reduction strategy (default: enabled)";
- "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 3)";
+ "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 4)";
"-s", Arg.Int set_sel,
- "symbols-based selection ratio (relative to the weight ratio, default: 2)";
+ "symbols-based selection ratio (relative to the weight ratio, default: 0)";
"-c", Arg.String set_conf, "Configuration file (for the db connection)";
- "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
+ "-o", Arg.String set_ordering,
+ "Term ordering. Possible values are:\n" ^
+ "\tkbo: Knuth-Bendix ordering (default)\n" ^
+ "\tnr-kbo: Non-recursive variant of kbo\n" ^
+ "\tlpo: Lexicographic path ordering";
- "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
-
- "-l", Arg.Int set_time_limit, "Time limit (in seconds)";
+ "-l", Arg.Int set_time_limit, "Time limit in seconds (default: no limit)";
] (fun a -> ()) "Usage:"
in
Helm_registry.load_from !configuration_file;
(* equality-selection related globals *)
let use_fullred = ref true;;
-let weight_age_ratio = ref 3;; (* settable by the user from the command line *)
+let weight_age_ratio = ref (* 5 *) 3;; (* settable by the user *)
let weight_age_counter = ref !weight_age_ratio;;
-let symbols_ratio = ref 2;;
+let symbols_ratio = ref (* 0 *) 2;;
let symbols_counter = ref 0;;
+(* non-recursive Knuth-Bendix term ordering by default *)
+Utils.compare_terms := Utils.nonrec_kbo;;
+
(* statistics... *)
let derived_clauses = ref 0;;
let kept_clauses = ref 0;;
;;
-let backward_simplify_active env new_pos new_table active =
+let backward_simplify_active env new_pos new_table min_weight active =
let active_list, active_table = active in
let active_list, newa =
List.fold_right
(fun (s, equality) (res, newn) ->
- match forward_simplify env (s, equality) (new_pos, new_table) with
- | None -> res, newn
- | Some (s, e) ->
- if equality = e then
- (s, e)::res, newn
- else
- res, (s, e)::newn)
+ let ew, _, _, _, _ = equality in
+ if ew < min_weight then
+ (s, equality)::res, newn
+ else
+ match forward_simplify env (s, equality) (new_pos, new_table) with
+ | None -> res, newn
+ | Some (s, e) ->
+ if equality = e then
+ (s, e)::res, newn
+ else
+ res, (s, e)::newn)
active_list ([], [])
in
let find eq1 where =
;;
-let backward_simplify_passive env new_pos new_table passive =
+let backward_simplify_passive env new_pos new_table min_weight passive =
let (nl, ns), (pl, ps), passive_table = passive in
let f sign equality (resl, ress, newn) =
- match forward_simplify env (sign, equality) (new_pos, new_table) with
- | None -> resl, EqualitySet.remove equality ress, newn
- | Some (s, e) ->
- if equality = e then
- equality::resl, ress, newn
- else
- let ress = EqualitySet.remove equality ress in
- resl, ress, e::newn
+ let ew, _, _, _, _ = equality in
+ if ew < min_weight then
+(* let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *)
+ equality::resl, ress, newn
+ else
+ match forward_simplify env (sign, equality) (new_pos, new_table) with
+ | None -> resl, EqualitySet.remove equality ress, newn
+ | Some (s, e) ->
+ if equality = e then
+ equality::resl, ress, newn
+ else
+ let ress = EqualitySet.remove equality ress in
+ resl, ress, e::newn
in
let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
let backward_simplify env new' ?passive active =
- let new_pos, new_table =
+ let new_pos, new_table, min_weight =
List.fold_left
- (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
- ([], Indexing.empty_table ()) (snd new')
- in
- let active, newa = backward_simplify_active env new_pos new_table active in
+ (fun (l, t, w) e ->
+ let ew, _, _, _, _ = e in
+ (Positive, e)::l, Indexing.index t e, min ew w)
+ ([], Indexing.empty_table (), 1000000) (snd new')
+ in
+ let active, newa =
+ backward_simplify_active env new_pos new_table min_weight active in
match passive with
| None ->
active, (make_passive [] []), newa, None
| Some passive ->
let passive, newp =
- backward_simplify_passive env new_pos new_table passive in
+ backward_simplify_passive env new_pos new_table min_weight passive in
active, passive, newa, newp
;;
in
()
else
- let active = make_active () in
- let passive =
- make_passive [term_equality] (equalities @ library_equalities)
+ let equalities =
+ let equalities = equalities @ library_equalities in
+ debug_print (
+ Printf.sprintf "equalities:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality equalities)));
+ debug_print "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_table ()) 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 (
+ Printf.sprintf "equalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality res)));
+ res
in
+ let active = make_active () in
+ let passive = make_passive [term_equality] equalities in
Printf.printf "\ncurrent goal: %s\n"
(string_of_equality ~env term_equality);
Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
(String.concat "\n"
(List.map
(string_of_equality ~env)
- equalities));
+ (equalities @ library_equalities)));
print_endline "--------------------------------------------------";
let start = Unix.gettimeofday () in
print_endline "GO!";
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
()
let env = (metasenv, context, ugraph) in
(* try *)
let term_equality = equality_of_term new_meta_goal goal in
- let res =
+ let res, time =
if is_identity env term_equality then
let w, _, (eq_ty, left, right, o), m, a = term_equality in
let proof =
(HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
eq_ty; left]
in
- ParamodulationSuccess
- (Some (0, Inference.BasicProof proof,
- (eq_ty, left, right, o), m, a), env)
+ (ParamodulationSuccess
+ (Some (0, Inference.BasicProof proof,
+ (eq_ty, left, right, o), m, a), env), 0.)
else
let library_equalities, maxm =
find_library_equalities ~dbd context (proof, goal') (maxm+2)
in
maxmeta := maxm+2;
-
+ let equalities =
+ let equalities = equalities @ library_equalities in
+ debug_print (
+ Printf.sprintf "equalities:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality equalities)));
+ debug_print "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_table ()) 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 (
+ Printf.sprintf "equalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality res)));
+ res
+ in
let active = make_active () in
- let passive =
- make_passive [term_equality] (equalities @ library_equalities)
- in
+ let passive = make_passive [term_equality] equalities in
+ let start = Unix.gettimeofday () in
let res = given_clause_fullred env passive active in
- res
+ let finish = Unix.gettimeofday () in
+ (res, finish -. start)
in
match res with
| ParamodulationSuccess (Some goal, env) ->
raise (ProofEngineTypes.Fail
"Found a proof, but it doesn't typecheck")
in
+ debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time);
newstatus
| _ ->
raise (ProofEngineTypes.Fail "NO proof found")
;;
+module OrderedInt = struct
+ type t = int
+
+ let compare = Pervasives.compare
+end
+
+module IntSet = Set.Make(OrderedInt)
+
let compute_equality_weight ty left right =
+(* let metasw = ref IntSet.empty in *)
let metasw = ref 0 in
let weight_of t =
let w, m = (weight_of_term ~consider_metas:true(* false *) t) in
(* let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *)
(* metasw := !metasw + mw; *)
metasw := !metasw + (2 * (List.length m));
+(* metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *)
w
in
- (weight_of ty) + (weight_of left) + (weight_of right) + !metasw
+ (weight_of ty) + (weight_of left) + (weight_of right) +
+ !metasw
+(* (4 * IntSet.cardinal !metasw) *)
;;
;;
-let rec aux_ordering t1 t2 =
+let rec aux_ordering ?(recursion=true) t1 t2 =
let module C = Cic in
let compare_uris u1 u2 =
let res =
| C.MutConstruct _, _ -> Lt
| _, C.MutConstruct _ -> Gt
- | C.Appl l1, C.Appl l2 ->
+ | C.Appl l1, C.Appl l2 when recursion ->
let rec cmp t1 t2 =
match t1, t2 with
| [], [] -> Eq
else o
in
cmp l1 l2
+ | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion ->
+ aux_ordering h1 h2
| t1, t2 ->
- Printf.printf "These two terms are not comparable:\n%s\n%s\n\n"
- (CicPp.ppterm t1) (CicPp.ppterm t2);
+ debug_print (
+ Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
+ (CicPp.ppterm t1) (CicPp.ppterm t2));
Incomparable
;;
;;
+let rec kbo t1 t2 =
+(* debug_print ( *)
+(* Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
+(* if t1 = t2 then *)
+(* Eq *)
+(* else *)
+ let aux = aux_ordering ~recursion:false in
+ let w1 = weight_of_term t1
+ and w2 = weight_of_term t2 in
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> Eq
+ | _, [] -> Gt
+ | [], _ -> Lt
+ | hd1::tl1, hd2::tl2 ->
+ let o =
+(* debug_print ( *)
+(* Printf.sprintf "recursion kbo on %s %s" *)
+(* (CicPp.ppterm hd1) (CicPp.ppterm hd2)); *)
+ kbo hd1 hd2
+ in
+ if o = Eq then cmp tl1 tl2
+ else o
+ in
+ let comparison = compare_weights ~normalize:true w1 w2 in
+(* debug_print ( *)
+(* Printf.sprintf "Weights are: %s %s: %s" *)
+(* (string_of_weight w1) (string_of_weight w2) *)
+(* (string_of_comparison comparison)); *)
+ match comparison with
+ | Le ->
+ let r = aux t1 t2 in
+(* debug_print ("HERE! " ^ (string_of_comparison r)); *)
+ if r = Lt then Lt
+ else if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ if cmp tl1 tl2 = Lt then Lt else Incomparable
+ | _, _ -> Incomparable
+ ) else Incomparable
+ | Ge ->
+ let r = aux t1 t2 in
+ if r = Gt then Gt
+ else if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ if cmp tl1 tl2 = Gt then Gt else Incomparable
+ | _, _ -> Incomparable
+ ) else Incomparable
+ | Eq ->
+ let r = aux t1 t2 in
+ if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+(* if cmp tl1 tl2 = Gt then Gt else Incomparable *)
+ cmp tl1 tl2
+ | _, _ -> Incomparable
+ ) else r
+ | res -> res
+;;
+
+
let names_of_context context =
List.map
(function
val lpo: Cic.term -> Cic.term -> comparison
+val kbo: Cic.term -> Cic.term -> comparison
+
(** term-ordering function settable by the user *)
val compare_terms: (Cic.term -> Cic.term -> comparison) ref
projects / helm.git / commitdiff