+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
type path_string_elem = Cic.term;;
type path_string = path_string_elem list;;
let head_of_term = function
| Cic.Appl (hd::tl) -> hd
-(* | Cic.Meta _ -> Cic.Implicit None *)
| term -> term
;;
let indexing_retrieval_time = ref 0.;;
-(* let my_apply_subst subst term = *)
-(* let module C = Cic in *)
-(* let lookup lift_amount meta = *)
-(* match meta with *)
-(* | C.Meta (i, _) -> ( *)
-(* try *)
-(* let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in *)
-(* (\* CicSubstitution.lift lift_amount *\)t *)
-(* with Not_found -> meta *)
-(* ) *)
-(* | _ -> assert false *)
-(* in *)
-(* let rec apply_aux lift_amount = function *)
-(* | C.Meta (i, l) as t -> lookup lift_amount t *)
-(* | C.Appl l -> C.Appl (List.map (apply_aux lift_amount) l) *)
-(* | C.Prod (nn, s, t) -> *)
-(* C.Prod (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
-(* | C.Lambda (nn, s, t) -> *)
-(* C.Lambda (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
-(* | t -> t *)
-(* in *)
-(* apply_aux 0 term *)
-(* ;; *)
-
-
-(* let apply_subst subst term = *)
-(* Printf.printf "| apply_subst:\n| subst: %s\n| term: %s\n" *)
-(* (Utils.print_subst ~prefix:" ; " subst) (CicPp.ppterm term); *)
-(* let res = my_apply_subst subst term in *)
-(* (\* let res = CicMetaSubst.apply_subst subst term in *\) *)
-(* Printf.printf "| res: %s\n" (CicPp.ppterm res); *)
-(* print_endline "|"; *)
-(* res *)
-(* ;; *)
-
-(* let apply_subst = my_apply_subst *)
let apply_subst = CicMetaSubst.apply_subst
-(* let apply_subst = *)
-(* let profile = CicUtil.profile "apply_subst" in *)
-(* (fun s a -> profile (apply_subst s) a) *)
-(* ;; *)
-
(*
(* NO INDEXING *)
+let init_index () = ()
+
let empty_table () = []
let index table equality =
(*
(* PATH INDEXING *)
+let init_index () = ()
+
let empty_table () =
Path_indexing.PSTrie.empty
;;
;;
-(* let get_candidates = *)
-(* let profile = CicUtil.profile "Indexing.get_candidates" in *)
-(* (fun mode tree term -> profile.profile (get_candidates mode tree) term) *)
-(* ;; *)
-
-
let match_unif_time_ok = ref 0.;;
let match_unif_time_no = ref 0.;;
+(*
+ finds the first equality in the index that matches "term", of type "termty"
+ termty can be Implicit if it is not needed. The result (one of the sides of
+ the equality, actually) should be not greater (wrt the term ordering) than
+ term
+*)
let rec find_matches metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils 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 check = match termty with C.Implicit None -> false | _ -> true in
function
| [] -> None
let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
-(* debug_print (lazy ( *)
-(* 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 do_match c eq_URI =
let subst', metasenv', ugraph' =
let t1 = Unix.gettimeofday () in
try
in
if o <> U.Incomparable then
try
- do_match c (* other *) eq_URI
+ do_match c eq_URI
with Inference.MatchingFailure ->
find_matches metasenv context ugraph lift_amount term termty tl
else
let res =
- try do_match c (* other *) eq_URI
+ try do_match c eq_URI
with Inference.MatchingFailure -> None
in
match res with
| Some (_, s, _, _, _) ->
- let c' = (* M. *)apply_subst s c
- and other' = (* M. *)apply_subst s other in
+ let c' = apply_subst s c
+ and other' = apply_subst s other in
let order = cmp c' other' in
let names = U.names_of_context context in
-(* let _ = *)
-(* debug_print *)
-(* (Printf.sprintf "OK matching: %s and %s, order: %s" *)
-(* (CicPp.ppterm c') *)
-(* (CicPp.ppterm other') *)
-(* (Utils.string_of_comparison order)); *)
-(* debug_print *)
-(* (Printf.sprintf "subst:\n%s\n" (Utils.print_subst s)) *)
-(* in *)
if order = U.Gt then
res
else
;;
+(*
+ as above, but finds all the matching equalities, and the matching condition
+ can be either Inference.matching or Inference.unification
+*)
let rec find_all_matches ?(unif_fun=Inference.unification)
metasenv context ugraph lift_amount term termty =
let module C = Cic 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 _ = *)
-(* match term with *)
-(* | C.Meta _ -> assert false *)
-(* | _ -> () *)
-(* 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 (lazy ( *\) *)
-(* (\* 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 r =
- unif_fun (metasenv @ metas) context
- term (S.lift lift_amount c) ugraph in
- let t2 = Unix.gettimeofday () in
- match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
- r
- with
- | Inference.MatchingFailure
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ as e ->
- let t2 = Unix.gettimeofday () in
- match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
- in
- (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
- (candidate, eq_URI))
- in
- let c, other, eq_URI =
- if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
- else right, left, Utils.eq_ind_r_URI ()
- in
- if o <> U.Incomparable then
+ let do_match c 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 termty tl)
+ let r =
+ unif_fun (metasenv @ metas) context
+ term (S.lift lift_amount c) ugraph in
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+ r
with
| Inference.MatchingFailure
| CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
+ | CicUnification.Uncertain _ as e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
+ in
+ (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+ (candidate, eq_URI))
+ in
+ let c, other, eq_URI =
+ if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+ else right, left, Utils.eq_ind_r_URI ()
+ in
+ if o <> U.Incomparable then
+ try
+ let res = do_match c eq_URI in
+ res::(find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl)
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl
+ else
+ try
+ let res = do_match c eq_URI in
+ match res with
+ | _, s, _, _, _ ->
+ let c' = apply_subst s c
+ and other' = apply_subst s other in
+ let order = cmp c' other' 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 termty tl)
+ else
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl
- else
- try
- let res = do_match c (* other *) eq_URI in
- match res with
- | _, s, _, _, _ ->
- let c' = (* M. *)apply_subst s c
- and other' = (* M. *)apply_subst s other in
- let order = cmp c' other' 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 termty tl)
- else
- find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term termty tl
- with
- | Inference.MatchingFailure
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
- find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term termty tl
;;
+(*
+ returns true if target is subsumed by some equality in table
+*)
let subsumption env table target =
let _, (ty, left, right, _), tmetas, _ = target in
let metasenv, context, ugraph = env in
let demod_counter = ref 1;;
+(** demodulation, when target is an equality *)
let rec demodulation_equality newmeta env table sign target =
let module C = Cic in
let module S = CicSubstitution in
in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
- let bo = (* M. *)apply_subst subst (S.subst other t) in
-(* let t' = *)
-(* let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *)
-(* incr demod_counter; *)
-(* let l, r = *)
-(* if is_left then t, S.lift 1 right else S.lift 1 left, t in *)
-(* (name, ty, S.lift 1 eq_ty, l, r) *)
-(* in *)
+ let bo = apply_subst subst (S.subst other t) in
let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
incr demod_counter;
let bo' =
incr maxmeta;
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
- Printf.printf "\nADDING META: %d\n" !maxmeta;
+ debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
print_newline ();
C.Meta (!maxmeta, irl)
in
-(* let target' = *)
let eq_found =
let proof' =
-(* let ens = *)
-(* if pos = Utils.Left then *)
-(* build_ens_for_sym_eq ty what other *)
-(* else *)
-(* build_ens_for_sym_eq ty other what *)
let termlist =
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
let target_proof =
let pb =
- Inference.ProofBlock (subst, eq_URI, (name, ty), bo'(* t' *),
+ Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
eq_found, Inference.BasicProof metaproof)
in
match proof with
| Inference.BasicProof _ ->
print_endline "replacing a BasicProof";
pb
- | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) ->
+ | Inference.ProofGoalBlock (_, parent_proof) ->
print_endline "replacing another ProofGoalBlock";
- Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *))
+ Inference.ProofGoalBlock (pb, parent_proof)
| _ -> assert false
in
-(* (0, target_proof, (eq_ty, left, right, order), metas, args) *)
-(* in *)
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
(LibraryObjects.eq_URI (), 0, 1, []);
eq_ty; if is_left then right else left]
in
(bo,
- Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *)))
+ 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 newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
and newargs = args
-(* let a = *)
-(* List.filter *)
-(* (function C.Meta (i, _) -> List.mem i m | _ -> assert false) args in *)
-(* let delta = (List.length args) - (List.length a) in *)
-(* if delta > 0 then *)
-(* let first = List.hd a in *)
-(* let rec aux l = function *)
-(* | 0 -> l *)
-(* | d -> let l = aux l (d-1) in l @ [first] *)
-(* in *)
-(* aux a delta *)
-(* else *)
-(* a *)
in
let ordering = !Utils.compare_terms left right in
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
-(* if subsumption env table newtarget then *)
-(* newmeta, build_identity newtarget *)
-(* else *)
demodulation_equality newmeta env table sign newtarget
| None ->
let res = demodulation_aux metasenv' context ugraph table 0 right in
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
-(* if subsumption env table newtarget then *)
-(* newmeta, build_identity newtarget *)
-(* else *)
demodulation_equality newmeta env table sign newtarget
| None ->
newmeta, target
;;
+(**
+ Performs the beta expansion of the term "term" w.r.t. "table",
+ i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
+ in table.
+*)
let rec betaexpand_term metasenv context ugraph table lift_amount term =
let module C = Cic in
let module S = CicSubstitution in
let sup_l_counter = ref 1;;
+(**
+ superposition_left
+ returns a list of new clauses inferred with a left superposition step
+ the negative equation "target" and one of the positive equations in "table"
+*)
let superposition_left newmeta (metasenv, context, ugraph) table target =
let module C = Cic in
let module S = CicSubstitution in
let maxmeta = ref newmeta in
let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
- print_endline "\nSUPERPOSITION LEFT\n";
-
+ debug_print (lazy "\nSUPERPOSITION LEFT\n");
+
let time1 = Unix.gettimeofday () in
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
- let bo' = (* M. *)apply_subst s (S.subst other bo) in
-(* let t' = *)
-(* let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *)
-(* incr sup_l_counter; *)
-(* let l, r = *)
-(* if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in *)
-(* (name, ty, S.lift 1 eq_ty, l, r) *)
-(* in *)
+ let bo' = apply_subst s (S.subst other bo) in
let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
incr sup_l_counter;
let bo'' =
CicMkImplicit.identity_relocation_list_for_metavariable context in
C.Meta (!maxmeta, irl)
in
-(* let target' = *)
- let eq_found =
- let proof' =
-(* let ens = *)
-(* if pos = Utils.Left then *)
-(* build_ens_for_sym_eq ty what other *)
-(* else *)
-(* build_ens_for_sym_eq ty other what *)
-(* in *)
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Inference.ProofSymBlock (termlist, proof')
- in
- let what, other =
- if pos = Utils.Left then what, other else other, what
+ let eq_found =
+ let proof' =
+ let termlist =
+ if pos = Utils.Left then [ty; what; other]
+ else [ty; other; what]
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+ Inference.ProofSymBlock (termlist, proof')
in
- let target_proof =
- let pb =
- Inference.ProofBlock (s, eq_URI, (name, ty), bo''(* t' *), eq_found,
- Inference.BasicProof metaproof)
- in
- match proof with
- | Inference.BasicProof _ ->
- print_endline "replacing a BasicProof";
- pb
- | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) ->
- print_endline "replacing another ProofGoalBlock";
- Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *))
- | _ -> assert false
+ let what, other =
+ if pos = Utils.Left then what, other else other, what
in
-(* (weight, target_proof, (eq_ty, left, right, ordering), [], []) *)
-(* in *)
+ pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+ in
+ let target_proof =
+ let pb =
+ Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
+ Inference.BasicProof metaproof)
+ in
+ match proof with
+ | Inference.BasicProof _ ->
+ debug_print (lazy "replacing a BasicProof");
+ pb
+ | Inference.ProofGoalBlock (_, parent_proof) ->
+ debug_print (lazy "replacing another ProofGoalBlock");
+ Inference.ProofGoalBlock (pb, parent_proof)
+ | _ -> assert false
+ in
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
(LibraryObjects.eq_URI (), 0, 1, []);
eq_ty; if ordering = U.Gt then right else left]
in
(bo',
- Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *)))
+ Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
in
let left, right =
if ordering = U.Gt then newgoal, right else left, newgoal in
let sup_r_counter = ref 1;;
+(**
+ superposition_right
+ returns a list of new clauses inferred with a right superposition step
+ between the positive equation "target" and one in the "table" "newmeta" is
+ the first free meta index, i.e. the first number above the highest meta
+ index: its updated value is also returned
+*)
let superposition_right newmeta (metasenv, context, ugraph) table target =
let module C = Cic in
let module S = CicSubstitution in
let res l r =
List.filter
(fun (_, subst, _, _, _) ->
- let subst = (* M. *)apply_subst subst in
+ let subst = apply_subst subst in
let o = !Utils.compare_terms (subst l) (subst r) in
o <> U.Lt && o <> U.Le)
(fst (betaexpand_term metasenv' context ugraph table 0 l))
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
- let bo' = (* M. *)apply_subst s (S.subst other bo) in
+ let bo' = apply_subst s (S.subst other bo) in
let t' =
let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
incr sup_r_counter;
S.lift 1 eq_ty; l; r]
in
bo',
- Inference.ProofBlock (
- s, eq_URI, (name, ty), bo''(* t' *), eq_found, eqproof)
+ Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
in
let newmeta, newequality =
let left, right =
- if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
- else (* M. *)apply_subst s left, newgoal in
+ if ordering = U.Gt then newgoal, apply_subst s right
+ else apply_subst s left, newgoal in
let neworder = !Utils.compare_terms left right
and newmenv = newmetas @ menv'
and newargs = args @ args' in
-(* let m = *)
-(* (Inference.metas_of_term left) @ (Inference.metas_of_term right) in *)
-(* let a = *)
-(* List.filter *)
-(* (function C.Meta (i, _) -> List.mem i m | _ -> assert false) *)
-(* (args @ args') *)
-(* in *)
-(* let delta = (List.length args) - (List.length a) in *)
-(* if delta > 0 then *)
-(* let first = List.hd a in *)
-(* let rec aux l = function *)
-(* | 0 -> l *)
-(* | d -> let l = aux l (d-1) in l @ [first] *)
-(* in *)
-(* aux a delta *)
-(* else *)
-(* a *)
-(* in *)
let eq' =
let w = Utils.compute_equality_weight eq_ty left right in
(w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
in
let new1 = List.map (build_new U.Gt) res1
and new2 = List.map (build_new U.Lt) res2 in
-(* let ok = function *)
-(* | _, _, (_, left, right, _), _, _ -> *)
-(* not (fst (CR.are_convertible context left right ugraph)) *)
-(* in *)
let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
;;
+(** demodulation, when the target is a goal *)
let rec demodulation_goal newmeta env table goal =
let module C = Cic in
let module S = CicSubstitution in
with CicUtil.Meta_not_found _ -> ty
in
let newterm, newproof =
- let bo = (* M. *)apply_subst subst (S.subst other t) in
+ let bo = apply_subst subst (S.subst other t) in
let bo' = apply_subst subst t in
let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
incr demod_counter;
incr maxmeta;
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
- Printf.printf "\nADDING META: %d\n" !maxmeta;
- print_newline ();
+ debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
C.Meta (!maxmeta, irl)
in
let eq_found =
let proof' =
-(* let ens = *)
-(* if pos = Utils.Left then build_ens_for_sym_eq ty what other *)
-(* else build_ens_for_sym_eq ty other what *)
-(* in *)
let termlist =
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
;;
+(** demodulation, when the target is a theorem *)
let rec demodulation_theorem newmeta env table theorem =
let module C = Cic in
let module S = CicSubstitution in
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
open Utils;;
| BasicProof of Cic.term
| ProofBlock of
Cic.substitution * UriManager.uri *
- (Cic.name * Cic.term) * Cic.term *
- (* name, ty, eq_ty, left, right *)
-(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *)
- (Utils.pos * equality) * proof
- | ProofGoalBlock of proof * proof (* equality *)
-(* | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *)
+ (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
+ | ProofGoalBlock of proof * proof
| ProofSymBlock of Cic.term list * proof
| SubProof of Cic.term * int * proof
;;
;;
+let rec string_of_proof = function
+ | NoProof -> "NoProof"
+ | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
+ | SubProof (t, i, p) ->
+ Printf.sprintf "SubProof(%s, %s, %s)"
+ (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
+ | ProofSymBlock _ -> "ProofSymBlock"
+ | ProofBlock _ -> "ProofBlock"
+ | ProofGoalBlock (p1, p2) ->
+ Printf.sprintf "ProofGoalBlock(%s, %s)"
+ (string_of_proof p1) (string_of_proof p2)
+;;
+
+
+(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
let build_ens_for_sym_eq sym_eq_URI termlist =
let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
match obj with
in
aux (uris, termlist)
| _ -> assert false
-(* [(UriManager.uri_of_string *)
-(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); *)
-(* (UriManager.uri_of_string *)
-(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); *)
-(* (UriManager.uri_of_string *)
-(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] *)
;;
| ProofGoalBlock (proofbit, proof) ->
print_endline "found ProofGoalBlock, going up...";
do_build_goal_proof proofbit proof
-(* | ProofSymBlock (ens, proof) -> *)
-(* let proof = do_build_proof proof in *)
-(* Cic.Appl [ *)
-(* Cic.Const (Utils.sym_eq_URI (), ens); (\* symmetry *\) *)
-(* proof *)
-(* ] *)
| ProofSymBlock (termlist, proof) ->
let proof = do_build_proof proof in
let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
- | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
+ | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
let t' = Cic.Lambda (name, ty, bo) in
let proof' =
let _, proof', _, _, _ = eq in
~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
and do_build_goal_proof proofbit proof =
-(* match proofbit with *)
-(* | BasicProof _ -> do_build_proof proof *)
-(* | proofbit -> *)
- match proof with
- | ProofGoalBlock (pb, p(* eq *)) ->
- do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *)))
-(* let _, proof, _, _, _ = eq in *)
-(* let newproof = replace_proof proofbit proof in *)
-(* do_build_proof newproof *)
-
-(* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
-(* let eqproof' = replace_proof proofbit eqproof in *)
-(* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
- | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
+ match proof with
+ | ProofGoalBlock (pb, p) ->
+ do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
+ | _ -> do_build_proof (replace_proof proofbit proof)
and replace_proof newproof = function
- | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) ->
+ | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
let eqproof' = replace_proof newproof eqproof in
- ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof')
- | ProofGoalBlock (pb, p(* equality *)) ->
+ ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
+ | ProofGoalBlock (pb, p) ->
let pb' = replace_proof newproof pb in
- ProofGoalBlock (pb', p(* equality *))
-(* let w, proof, t, menv, args = equality in *)
-(* let proof' = replace_proof newproof proof in *)
-(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
+ ProofGoalBlock (pb', p)
| BasicProof _ -> newproof
| SubProof (term, meta_index, p) ->
SubProof (term, meta_index, replace_proof newproof p)
| p -> p
in
-(* let _, proof, _, _, _ = equality in *)
do_build_proof proof
;;
(fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
in
let rec aux ((table_l, table_r) as table) t1 t2 =
-(* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
-(* (CicPp.ppterm t1) (CicPp.ppterm t2) *)
-(* (print_table table_l) (print_table table_r); *)
match t1, t2 with
| C.Meta (m1, tl1), C.Meta (m2, tl2) ->
let m1_binding, table_l =
try List.assoc m2 table_r, table_r
with Not_found -> m1, (m2, m1)::table_r
in
-(* let m1_binding, m2_binding, table = *)
-(* let m1b, table = *)
-(* try List.assoc m1 table, table *)
-(* with Not_found -> m2, (m1, m2)::table *)
-(* in *)
-(* let m2b, table = *)
-(* try List.assoc m2 table, table *)
-(* with Not_found -> m1, (m2, m1)::table *)
-(* in *)
-(* m1b, m2b, table *)
-(* in *)
-(* Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
-(* (print_table table_l) (print_table table_r); *)
if (m1_binding <> m2) || (m2_binding <> m1) then
raise NotMetaConvertible
else (
else
try
let l, r = meta_convertibility_aux ([], []) t1 t2 in
- (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
true
with NotMetaConvertible ->
false
;;
-(*
-let replace_metas (* context *) term =
- let module C = Cic in
- let rec aux = function
- | C.Meta (i, c) ->
-(* let irl = *)
-(* CicMkImplicit.identity_relocation_list_for_metavariable context *)
-(* in *)
-(* if c = irl then *)
-(* C.Implicit (Some (`MetaIndex i)) *)
-(* else ( *)
-(* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
-(* (String.concat "\n" *)
-(* (List.map *)
-(* (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
-(* C.Meta (i, c) *)
-(* ) *)
- C.Implicit (Some (`MetaInfo (i, c)))
- | C.Var (u, ens) -> C.Var (u, aux_ens ens)
- | C.Const (u, ens) -> C.Const (u, aux_ens ens)
- | C.Cast (s, t) -> C.Cast (aux s, aux t)
- | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
- | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
- | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
- | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
- | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
- | C.MutCase (uri, i, s, t, l) ->
- C.MutCase (uri, i, aux s, aux t, List.map aux l)
- | C.Fix (i, il) ->
- let il' =
- List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
- C.Fix (i, il')
- | C.CoFix (i, il) ->
- let il' =
- List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
- C.CoFix (i, il')
- | t -> t
- and aux_ens ens =
- List.map (fun (u, t) -> (u, aux t)) ens
- in
- aux term
-;;
-*)
-
-
-(*
-let restore_metas (* context *) term =
- let module C = Cic in
- let rec aux = function
- | C.Implicit (Some (`MetaInfo (i, c))) ->
-(* let c = *)
-(* CicMkImplicit.identity_relocation_list_for_metavariable context *)
-(* in *)
-(* C.Meta (i, c) *)
-(* let local_context:(C.term option) list = *)
-(* Marshal.from_string mc 0 *)
-(* in *)
-(* C.Meta (i, local_context) *)
- C.Meta (i, c)
- | C.Var (u, ens) -> C.Var (u, aux_ens ens)
- | C.Const (u, ens) -> C.Const (u, aux_ens ens)
- | C.Cast (s, t) -> C.Cast (aux s, aux t)
- | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
- | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
- | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
- | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
- | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
- | C.MutCase (uri, i, s, t, l) ->
- C.MutCase (uri, i, aux s, aux t, List.map aux l)
- | C.Fix (i, il) ->
- let il' =
- List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
- C.Fix (i, il')
- | C.CoFix (i, il) ->
- let il' =
- List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
- C.CoFix (i, il')
- | t -> t
- and aux_ens ens =
- List.map (fun (u, t) -> (u, aux t)) ens
- in
- aux term
-;;
-*)
-
-(*
-let rec restore_subst (* context *) subst =
- List.map
- (fun (i, (c, t, ty)) ->
- i, (c, restore_metas (* context *) t, ty))
- subst
-;;
-*)
-
-
let rec check_irl start = function
| [] -> true
| None::tl -> check_irl (start+1) tl
| _ -> false
;;
+
let rec is_simple_term = function
| Cic.Appl ((Cic.Meta _)::_) -> false
| Cic.Appl l -> List.for_all is_simple_term l
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 (
debug_print
| [] -> []
| (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
in
-(* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
-(* print_endline "|"; *)
fix_subst subst, menv, ug
;;
exception MatchingFailure;;
+(*
let matching_simple metasenv context t1 t2 ugraph =
let module C = Cic in
let module M = CicMetaSubst in
| _ -> assert false
in
let rec do_match subst menv s t =
-(* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
-(* (print_subst subst); *)
-(* print_newline (); *)
-(* let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
-(* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *)
- (* Printf.printf "after apply_subst: %s %s\n%s" *)
- (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
- (* print_newline (); *)
match s, t with
| s, t when s = t -> subst, menv
-(* | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
-(* do_match subst menv t s *)
-(* | C.Meta _, t when occurs_check subst s t -> *)
-(* raise MatchingFailure *)
-(* | s, C.Meta _ when occurs_check subst t s -> *)
-(* raise MatchingFailure *)
| s, C.Meta (i, l) ->
let filter_menv i menv =
List.filter (fun (m, _, _) -> i <> m) menv
let subst, menv =
let value = lookup t subst in
match value with
-(* | C.Meta (i', l') when Hashtbl.mem table i' -> *)
-(* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
| value when value = t ->
let _, _, ty = CicUtil.lookup_meta i menv in
(i, (context, s, ty))::subst, filter_menv i menv
| value -> do_match subst menv s value
in
subst, menv
-(* else if value <> s then *)
-(* raise MatchingFailure *)
-(* else subst *)
-(* if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
-(* else subst *)
-(* in *)
-(* let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
-(* subst, menv *)
-(* | _, C.Meta _ -> do_match subst menv t s *)
-(* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
-(* raise MatchingFailure *)
| C.Appl ls, C.Appl lt -> (
try
List.fold_left2
(fun (subst, menv) s t -> do_match subst menv s t)
(subst, menv) ls lt
with Invalid_argument _ ->
-(* print_endline (Printexc.to_string e); *)
-(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
-(* print_newline (); *)
raise MatchingFailure
)
| _, _ ->
-(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
-(* print_newline (); *)
raise MatchingFailure
in
let subst, menv = do_match [] metasenv t1 t2 in
- (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
- (* print_newline (); *)
subst, menv, ugraph
;;
+*)
let matching metasenv context t1 t2 ugraph =
-(* if (is_simple_term t1) && (is_simple_term t2) then *)
-(* let subst, menv, ug = *)
-(* matching_simple metasenv context t1 t2 ugraph in *)
-(* (\* Printf.printf "matching %s %s:\n%s\n" *\) *)
-(* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
-(* (\* print_newline (); *\) *)
-(* subst, menv, ug *)
-(* else *)
-(* debug_print *)
-(* (Printf.sprintf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
-(* print_newline (); *)
try
let subst, metasenv, ugraph =
- (* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
unification metasenv context t1 t2 ugraph
in
let t' = CicMetaSubst.apply_subst subst t1 in
| s -> s
in
let subst = List.map fix_subst subst in
-
-(* Printf.printf "matching %s %s:\n%s\n" *)
-(* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
-(* print_newline (); *)
-
subst, metasenv, ugraph
with
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
-(* Printf.printf "failed to match %s %s\n" *)
-(* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
-(* print_endline (Printexc.to_string e); *)
raise MatchingFailure
;;
-(* let matching = *)
-(* let profile = CicUtil.profile "Inference.matching" in *)
-(* (fun metasenv context t1 t2 ugraph -> *)
-(* profile (matching metasenv context t1 t2) ugraph) *)
-(* ;; *)
-
-
-let beta_expand ?(metas_ok=true) ?(match_only=false)
- what type_of_what where context metasenv ugraph =
- let module S = CicSubstitution in
- let module C = Cic in
-
-(* let _ = *)
-(* let names = names_of_context context in *)
-(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
-(* (CicPp.pp what names) (CicPp.ppterm what) *)
-(* (CicPp.pp where names) (CicPp.ppterm where); *)
-(* print_newline (); *)
-(* in *)
- (*
- return value:
- ((list of all possible beta expansions, subst, metasenv, ugraph),
- lifted term)
- *)
- let rec aux lift_amount term context metasenv subst ugraph =
-(* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
- let res, lifted_term =
- match term with
- | C.Rel m ->
- [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
-
- | C.Var (uri, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.Var (uri, e), s, m, ug)) ens'
- in
- expansions, C.Var (uri, lifted_ens)
-
- | C.Meta (i, l) ->
- let l', lifted_l =
- List.fold_right
- (fun arg (res, lifted_tl) ->
- match arg with
- | Some arg ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
- arg_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
- res),
- (Some lifted_arg)::lifted_tl)
- | None ->
- (List.map
- (fun (r, s, m, ug) -> None::r, s, m, ug)
- res,
- None::lifted_tl)
- ) l ([], [])
- in
- let e =
- List.map
- (fun (l, s, m, ug) ->
- (C.Meta (i, l), s, m, ug)) l'
- in
- e, C.Meta (i, lifted_l)
-
- | C.Sort _
- | C.Implicit _ as t -> [], t
-
- | C.Cast (s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux lift_amount t context metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Cast (t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Cast (lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Cast (lifted_s, lifted_t)
-
- | C.Prod (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Prod (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Prod (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Prod (nn, lifted_s, lifted_t)
-
- | C.Lambda (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
-
- | C.LetIn (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
-
- | C.Appl l ->
- let l', lifted_l =
- aux_list lift_amount l context metasenv subst ugraph
- in
- (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
- C.Appl lifted_l)
-
- | C.Const (uri, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.Const (uri, e), s, m, ug)) ens'
- in
- (expansions, C.Const (uri, lifted_ens))
-
- | C.MutInd (uri, i ,exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.MutInd (uri, i, e), s, m, ug)) ens'
- in
- (expansions, C.MutInd (uri, i, lifted_ens))
-
- | C.MutConstruct (uri, i, j, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
- in
- (expansions, C.MutConstruct (uri, i, j, lifted_ens))
-
- | C.MutCase (sp, i, outt, t, pl) ->
- let pl_res, lifted_pl =
- aux_list lift_amount pl context metasenv subst ugraph
- in
- let l1, lifted_outt =
- aux lift_amount outt context metasenv subst ugraph in
- let l2, lifted_t =
- aux lift_amount t context metasenv subst ugraph in
-
- let l1' =
- List.map
- (fun (outt, s, m, ug) ->
- C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
- let l3' =
- List.map
- (fun (pl, s, m, ug) ->
- C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
- in
- (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
-
- | C.Fix (i, fl) ->
- let len = List.length fl in
- let fl', lifted_fl =
- List.fold_right
- (fun (nm, idx, ty, bo) (res, lifted_tl) ->
- let lifted_ty = S.lift lift_amount ty in
- let bo_res, lifted_bo =
- aux (lift_amount+len) bo context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) ->
- (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
- bo_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) ->
- (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
- (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
- ) fl ([], [])
- in
- (List.map
- (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
- C.Fix (i, lifted_fl))
-
- | C.CoFix (i, fl) ->
- let len = List.length fl in
- let fl', lifted_fl =
- List.fold_right
- (fun (nm, ty, bo) (res, lifted_tl) ->
- let lifted_ty = S.lift lift_amount ty in
- let bo_res, lifted_bo =
- aux (lift_amount+len) bo context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) ->
- (nm, lifted_ty, a)::lifted_tl, s, m, ug)
- bo_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) ->
- (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
- (nm, lifted_ty, lifted_bo)::lifted_tl)
- ) fl ([], [])
- in
- (List.map
- (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
- C.CoFix (i, lifted_fl))
- in
- let retval =
- match term with
- | C.Meta _ when (not metas_ok) ->
- res, lifted_term
- | _ ->
-(* let term' = *)
-(* if match_only then replace_metas context term *)
-(* else term *)
-(* in *)
- try
- let subst', metasenv', ugraph' =
-(* Printf.printf "provo a unificare %s e %s\n" *)
-(* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
- if match_only then
- matching metasenv context term (S.lift lift_amount what) ugraph
- else
- CicUnification.fo_unif metasenv context
- (S.lift lift_amount what) term ugraph
- in
-(* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
-(* (CicPp.ppterm (S.lift lift_amount what)); *)
-(* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
-(* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
- (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
-(* if match_only then *)
-(* let t' = CicMetaSubst.apply_subst subst' term in *)
-(* if not (meta_convertibility term t') then ( *)
-(* res, lifted_term *)
-(* ) else ( *)
-(* let metas = metas_of_term term in *)
-(* let fix_subst = function *)
-(* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
-(* (j, (c, C.Meta (i, lc), ty)) *)
-(* | s -> s *)
-(* in *)
-(* let subst' = List.map fix_subst subst' in *)
-(* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
-(* lifted_term) *)
-(* ) *)
-(* else *)
- ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
- lifted_term)
- with
- | MatchingFailure
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
- res, lifted_term
- in
-(* Printf.printf "exit aux\n"; *)
- retval
-
- and aux_list lift_amount l context metasenv subst ugraph =
- List.fold_right
- (fun arg (res, lifted_tl) ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 = List.map
- (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
- in
- (l1 @ (List.map
- (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
- lifted_arg::lifted_tl)
- ) l ([], [])
-
- and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
- List.fold_right
- (fun (u, arg) (res, lifted_tl) ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
- in
- (l1 @ (List.map (fun (r, s, m, ug) ->
- (u, lifted_arg)::r, s, m, ug) res),
- (u, lifted_arg)::lifted_tl)
- ) exp_named_subst ([], [])
-
- in
- let expansions, _ =
-(* let where = *)
-(* if match_only then replace_metas (\* context *\) where *)
-(* else where *)
-(* in *)
- aux 0 where context metasenv [] ugraph
- in
- let mapfun =
-(* if match_only then *)
-(* (fun (term, subst, metasenv, ugraph) -> *)
-(* let term' = *)
-(* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
-(* and subst = restore_subst subst in *)
-(* (term', subst, metasenv, ugraph)) *)
-(* else *)
- (fun (term, subst, metasenv, ugraph) ->
- let term' = C.Lambda (C.Anonymous, type_of_what, term) in
- (term', subst, metasenv, ugraph))
- in
- List.map mapfun expansions
-;;
-
let find_equalities context proof =
let module C = Cic in
let do_find context term =
match term with
| C.Prod (name, s, t) ->
-(* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
let (head, newmetas, args, newmeta) =
ProofEngineHelpers.saturate_term newmeta []
context (S.lift index term) 0
debug_print
(lazy
(Printf.sprintf "OK: %s" (CicPp.ppterm term)));
-(* debug_print ( *)
-(* Printf.sprintf "args: %s\n" *)
-(* (String.concat ", " (List.map CicPp.ppterm args)))); *)
-(* debug_print (lazy ( *)
-(* Printf.sprintf "newmetas:\n%s\n" *)
-(* (print_metasenv newmetas))); *)
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in
"cic:/Coq/ZArith/Zcompare/rename.con";
(* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
perche' questo cacchio di teorema rompe le scatole :'( *)
- "cic:/Rocq/SUBST/comparith/mult_n_2.con";
+ "cic:/Rocq/SUBST/comparith/mult_n_2.con";
+
+ "cic:/matita/logic/equality/eq_f.con";
+ "cic:/matita/logic/equality/eq_f2.con";
+ "cic:/matita/logic/equality/eq_rec.con";
+ "cic:/matita/logic/equality/eq_rect.con";
]
- ;;
+;;
let find_library_equalities dbd context status maxmeta =
let module C = Cic in
in
(uri, t, ty)::l)
[]
- (MetadataQuery.equations_for_goal ~dbd status)
+ (let t1 = Unix.gettimeofday () in
+ let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
+ let t2 = Unix.gettimeofday () in
+ (debug_print
+ (lazy
+ (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
+ (t2 -. t1))));
+ eqs)
in
- let eq_uri1 = eq_XURI () (* UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI *)
- and eq_uri2 = LibraryObjects.eq_URI () in (* HelmLibraryObjects.Logic.eq_URI in *)
+ let eq_uri1 = eq_XURI ()
+ and eq_uri2 = LibraryObjects.eq_URI () in
let iseq uri =
(UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
in
else
let t = CicUtil.term_of_uri uri in
let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
- (uri, t, ty, [])::l)
+ (t, ty, [])::l)
[] (MetadataQuery.signature_of_goal ~dbd status)
in
let refl_equal =
let u = eq_XURI () in
let t = CicUtil.term_of_uri u in
let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
- (u, t, ty, [])
+ (t, ty, [])
in
refl_equal::candidates
;;
let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
-(* print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
let table = Hashtbl.create (List.length args) in
- let is_this_case = ref false in
let newargs, newmeta =
List.fold_right
(fun t (newargs, index) ->
let _ =
if List.length metas > 0 then
let first = List.hd metas in
+ (* this new equality might have less variables than its parents: here
+ we fill the gap with a dummy arg. Example:
+ with (f X Y) = X we can simplify
+ (g X) = (f X Y) in
+ (g X) = X.
+ So the new equation has only one variable, but it still has type like
+ \lambda X,Y:..., so we need to pass a dummy arg for Y
+ (I hope this makes some sense...)
+ *)
Hashtbl.iter
(fun k v ->
if not (List.exists
let rec fix_proof = function
| NoProof -> NoProof
| BasicProof term -> BasicProof (repl term)
- | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) ->
-
-(* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
-(* (string_of_equality equality) (print_subst subst); *)
-
-(* debug_print "table is:"; *)
-(* Hashtbl.iter *)
-(* (fun k v -> debug_print (Printf.sprintf "%d: %d" k v)) *)
-(* table; *)
+ | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
let subst' =
List.fold_left
(fun s arg ->
let _, context, ty = CicUtil.lookup_meta i menv in
(i, (context, Cic.Meta (j, l), ty))::s
with Not_found | CicUtil.Meta_not_found _ ->
-(* debug_print ("Not_found meta ?" ^ (string_of_int i)); *)
s
)
| _ -> assert false)
[] args
in
-
-(* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
-(* print_newline (); *)
-
ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
| p -> assert false
in
let w = compute_equality_weight ty t1 t2 in
let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
e
-(* (proof, (ty, t1, t2, o), [], []) *)
| _ ->
raise TermIsNotAnEquality
;;
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-(*
-let superposition_left (metasenv, context, ugraph) target source =
- let module C = Cic in
- let module S = CicSubstitution in
- let module M = CicMetaSubst in
- let module HL = HelmLibraryObjects in
- let module CR = CicReduction in
- (* we assume that target is ground (does not contain metavariables): this
- * should always be the case (I hope, at least) *)
- let proof, (eq_ty, left, right, t_order), _, _ = target in
- let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty then
- []
- else
- let where, is_left =
- match t_order (* compare_terms left right *) with
- | Lt -> right, false
- | Gt -> left, true
- | _ -> (
- Printf.printf "????????? %s = %s" (CicPp.ppterm left)
- (CicPp.ppterm right);
- print_newline ();
- assert false (* again, for ground terms this shouldn't happen... *)
- )
- in
- let metasenv' = newmetas @ metasenv in
- let result = s_order (* compare_terms t1 t2 *) in
- let res1, res2 =
- match result with
- | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
- | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
- | _ ->
- let res1 =
- List.filter
- (fun (t, s, m, ug) ->
- compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
- (beta_expand t1 ty where context metasenv' ugraph)
- and res2 =
- List.filter
- (fun (t, s, m, ug) ->
- compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
- (beta_expand t2 ty where context metasenv' ugraph)
- in
- res1, res2
- in
- (* let what, other = *)
- (* if is_left then left, right *)
- (* else right, left *)
- (* in *)
- let build_new what other eq_URI (t, s, m, ug) =
- let newgoal, newgoalproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
- let bo' = S.subst (M.apply_subst s other) bo in
- let bo'' =
- C.Appl (
- [C.MutInd (HL.Logic.eq_URI, 0, []);
- S.lift 1 eq_ty] @
- if is_left then [bo'; S.lift 1 right]
- else [S.lift 1 left; bo'])
- in
- let t' = C.Lambda (nn, ty, bo'') in
- S.subst (M.apply_subst s other) bo,
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- proof; other; eqproof])
- | _ -> assert false
- in
- let equation =
- if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
- else (eq_ty, left, newgoal, compare_terms left newgoal)
- in
- (newgoalproof (* eqproof *), equation, [], [])
- in
- let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
- and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
- new1 @ new2
-;;
-
-
-let superposition_right newmeta (metasenv, context, ugraph) target source =
- let module C = Cic in
- let module S = CicSubstitution in
- let module M = CicMetaSubst in
- let module HL = HelmLibraryObjects in
- let module CR = CicReduction in
- let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
- let eqp', (ty', t1, t2, s_order), newm', args' = source in
- let maxmeta = ref newmeta in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty' then
- newmeta, []
- else
- (* let ok term subst other other_eq_side ugraph = *)
- (* match term with *)
- (* | C.Lambda (nn, ty, bo) -> *)
- (* let bo' = S.subst (M.apply_subst subst other) bo in *)
- (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
- (* not res *)
- (* | _ -> assert false *)
- (* in *)
- let condition left right what other (t, s, m, ug) =
- let subst = M.apply_subst s in
- let cmp1 = compare_terms (subst what) (subst other) in
- let cmp2 = compare_terms (subst left) (subst right) in
- (* cmp1 = Gt && cmp2 = Gt *)
- cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
- (* && (ok t s other right ug) *)
- in
- let metasenv' = metasenv @ newmetas @ newm' in
- let beta_expand = beta_expand ~metas_ok:false in
- let cmp1 = t_order (* compare_terms left right *)
- and cmp2 = s_order (* compare_terms t1 t2 *) in
- let res1, res2, res3, res4 =
- let res l r s t =
- List.filter
- (condition l r s t)
- (beta_expand s eq_ty l context metasenv' ugraph)
- in
- match cmp1, cmp2 with
- | Gt, Gt ->
- (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
- | Gt, Lt ->
- [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
- | Lt, Gt ->
- [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
- | Lt, Lt ->
- [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
- | Gt, _ ->
- let res1 = res left right t1 t2
- and res2 = res left right t2 t1 in
- res1, res2, [], []
- | Lt, _ ->
- let res3 = res right left t1 t2
- and res4 = res right left t2 t1 in
- [], [], res3, res4
- | _, Gt ->
- let res1 = res left right t1 t2
- and res3 = res right left t1 t2 in
- res1, [], res3, []
- | _, Lt ->
- let res2 = res left right t2 t1
- and res4 = res right left t2 t1 in
- [], res2, [], res4
- | _, _ ->
- let res1 = res left right t1 t2
- and res2 = res left right t2 t1
- and res3 = res right left t1 t2
- and res4 = res right left t2 t1 in
- res1, res2, res3, res4
- in
- let newmetas = newmetas @ newm' in
- let newargs = args @ args' in
- let build_new what other is_left eq_URI (t, s, m, ug) =
- (* let what, other = *)
- (* if is_left then left, right *)
- (* else right, left *)
- (* in *)
- let newterm, neweqproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
- let bo' = M.apply_subst s (S.subst other bo) in
- let bo'' =
- C.Appl (
- [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
- if is_left then [bo'; S.lift 1 right]
- else [S.lift 1 left; bo'])
- in
- let t' = C.Lambda (nn, ty, bo'') in
- bo',
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- eqproof; other; eqp'])
- | _ -> assert false
- in
- let newmeta, newequality =
- let left, right =
- if is_left then (newterm, M.apply_subst s right)
- else (M.apply_subst s left, newterm) in
- let neworder = compare_terms left right in
- fix_metas !maxmeta
- (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
- in
- maxmeta := newmeta;
- newequality
- in
- let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
- and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
- and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
- and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
- let ok = function
- | _, (_, left, right, _), _, _ ->
- not (fst (CR.are_convertible context left right ugraph))
- in
- (!maxmeta,
- (List.filter ok (new1 @ new2 @ new3 @ new4)))
-;;
-*)
-
-
let is_identity ((_, context, ugraph) as env) = function
| ((_, _, (ty, left, right, _), _, _) as equality) ->
(left = right ||
(meta_convertibility left right) ||
(fst (CicReduction.are_convertible context left right ugraph)))
;;
-
-
-(*
-let demodulation newmeta (metasenv, context, ugraph) target source =
- let module C = Cic in
- let module S = CicSubstitution in
- let module M = CicMetaSubst in
- let module HL = HelmLibraryObjects in
- let module CR = CicReduction in
-
- let proof, (eq_ty, left, right, t_order), metas, args = target
- and proof', (ty, t1, t2, s_order), metas', args' = source in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty then
- newmeta, target
- else
- let first_step, get_params =
- match s_order (* compare_terms t1 t2 *) with
- | Gt -> 1, (function
- | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
- | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
- | _ -> assert false)
- | Lt -> 1, (function
- | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
- | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
- | _ -> assert false)
- | _ ->
- let first_step = 3 in
- let get_params step =
- match step with
- | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
- | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
- | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
- | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
- | _ -> assert false
- in
- first_step, get_params
- in
- let rec demodulate newmeta step metasenv target =
- let proof, (eq_ty, left, right, t_order), metas, args = target in
- let is_left, what, other, eq_URI = get_params step in
-
- let env = metasenv, context, ugraph in
- let names = names_of_context context in
-(* Printf.printf *)
-(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(* (string_of_equality ~env target) (CicPp.pp what names) *)
-(* (CicPp.pp other names) (string_of_bool is_left); *)
-(* Printf.printf "step: %d" step; *)
-(* print_newline (); *)
-
- let ok (t, s, m, ug) =
- compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
- in
- let res =
- let r = (beta_expand ~metas_ok:false ~match_only:true
- what ty (if is_left then left else right)
- context (metasenv @ metas) ugraph)
- in
-(* let m' = metas_of_term what *)
-(* and m'' = metas_of_term (if is_left then left else right) in *)
-(* if (List.mem 527 m'') && (List.mem 6 m') then ( *)
-(* Printf.printf *)
-(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(* (string_of_equality ~env target) (CicPp.pp what names) *)
-(* (CicPp.pp other names) (string_of_bool is_left); *)
-(* Printf.printf "step: %d" step; *)
-(* print_newline (); *)
-(* print_endline "res:"; *)
-(* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
-(* print_newline (); *)
-(* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
-(* print_newline (); *)
-(* ); *)
- List.filter ok r
- in
- match res with
- | [] ->
- if step = 0 then newmeta, target
- else demodulate newmeta (step-1) metasenv target
- | (t, s, m, ug)::_ ->
- let newterm, newproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
-(* let bo' = M.apply_subst s (S.subst other bo) in *)
- let bo' = S.subst (M.apply_subst s other) bo in
- let bo'' =
- C.Appl (
- [C.MutInd (HL.Logic.eq_URI, 0, []);
- S.lift 1 eq_ty] @
- if is_left then [bo'; S.lift 1 right]
- else [S.lift 1 left; bo'])
- in
- let t' = C.Lambda (nn, ty, bo'') in
-(* M.apply_subst s (S.subst other bo), *)
- bo',
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- proof; other; proof'])
- | _ -> assert false
- in
- let newmeta, newtarget =
- let left, right =
-(* if is_left then (newterm, M.apply_subst s right) *)
-(* else (M.apply_subst s left, newterm) in *)
- if is_left then newterm, right
- else left, newterm
- in
- let neworder = compare_terms left right in
-(* let newmetasenv = metasenv @ metas in *)
-(* let newargs = args @ args' in *)
-(* fix_metas newmeta *)
-(* (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
- let m = (metas_of_term left) @ (metas_of_term right) in
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
- and newargs =
- List.filter
- (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
- args
- in
- newmeta,
- (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
- in
-(* Printf.printf *)
-(* "demodulate, newtarget: %s\ntarget was: %s\n" *)
-(* (string_of_equality ~env newtarget) *)
-(* (string_of_equality ~env target); *)
-(* (\* let _, _, newm, newa = newtarget in *\) *)
-(* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
-(* (\* (print_metasenv newm) *\) *)
-(* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
-(* print_newline (); *)
- if is_identity env newtarget then
- newmeta, newtarget
- else
- demodulate newmeta first_step metasenv newtarget
- in
- demodulate newmeta first_step (metasenv @ metas') target
-;;
-
-
-(*
-let demodulation newmeta env target source =
- newmeta, target
-;;
-*)
-
-
-let subsumption env target source =
- let _, (ty, tl, tr, _), tmetas, _ = target
- and _, (ty', sl, sr, _), smetas, _ = source in
- if ty <> ty' then
- false
- else
- let metasenv, context, ugraph = env in
- let metasenv = metasenv @ tmetas @ smetas in
- let names = names_of_context context in
- let samesubst subst subst' =
-(* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
-(* (print_subst subst) (print_subst subst'); *)
-(* print_newline (); *)
- let tbl = Hashtbl.create (List.length subst) in
- List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
- List.for_all
- (fun (m, (c, t1, t2)) ->
- try
- let c', t1', t2' = Hashtbl.find tbl m in
- if (c = c') && (t1 = t1') && (t2 = t2') then true
- else false
- with Not_found ->
- true)
- subst'
- in
- let subsaux left right left' right' =
- try
- let subst, menv, ug = matching metasenv context left left' ugraph
- and subst', menv', ug' = matching metasenv context right right' ugraph
- in
-(* Printf.printf "left = right: %s = %s\n" *)
-(* (CicPp.pp left names) (CicPp.pp right names); *)
-(* Printf.printf "left' = right': %s = %s\n" *)
-(* (CicPp.pp left' names) (CicPp.pp right' names); *)
- samesubst subst subst'
- with e ->
-(* print_endline (Printexc.to_string e); *)
- false
- in
- let res =
- if subsaux tl tr sl sr then true
- else subsaux tl tr sr sl
- in
- if res then (
- Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
- (string_of_equality ~env target) (string_of_equality ~env source);
- print_newline ();
- );
- res
-;;
-*)
-
-
-let extract_differing_subterms t1 t2 =
- let module C = Cic in
- let rec aux t1 t2 =
- match t1, t2 with
- | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
- [(t1, t2)]
- | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
- let res = List.concat (List.map2 aux tl1 tl2) in
- if h1 <> h2 then
- if res = [] then [(h1, h2)] else [(t1, t2)]
- else
- if List.length res > 1 then [(t1, t2)] else res
- | t1, t2 ->
- if t1 <> t2 then [(t1, t2)] else []
- in
- let res = aux t1 t2 in
- match res with
- | hd::[] -> Some hd
- | _ -> None
-;;
-
-
-let rec string_of_proof = function
- | NoProof -> "NoProof"
- | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
- | SubProof (t, i, p) ->
- Printf.sprintf "SubProof(%s, %s, %s)"
- (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
- | ProofSymBlock _ -> "ProofSymBlock"
- | ProofBlock _ -> "ProofBlock"
- | ProofGoalBlock (p1, p2) ->
- Printf.sprintf "ProofGoalBlock(%s, %s)"
- (string_of_proof p1) (string_of_proof p2)
-;;
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
type equality =
int * (* weight *)
- proof *
+ proof * (* proof *)
(Cic.term * (* type *)
Cic.term * (* left side *)
Cic.term * (* right side *)
and proof =
| NoProof
- | BasicProof of Cic.term
- | ProofBlock of
- Cic.substitution * UriManager.uri *
- (Cic.name * Cic.term) * Cic.term *
- (* name, ty, eq_ty, left, right *)
-(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *)
- (Utils.pos * equality) * proof
- | ProofGoalBlock of proof * proof (* equality *)
-(* | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *)
- | ProofSymBlock of Cic.term list * proof
+ | BasicProof of Cic.term (* already a proof of a goal *)
+ | ProofBlock of (* proof of a rewrite step *)
+ Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
+ (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
+ | ProofGoalBlock of proof * proof
+ (* proof of the new meta, proof of the goal from which this comes *)
+ | ProofSymBlock of Cic.term list * proof (* expl.named subst, proof *)
| SubProof of Cic.term * int * proof
+ (* parent proof, subgoal, proof of the subgoal *)
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+(** builds the Cic.term encoded by proof *)
+val build_proof_term: proof -> Cic.term
+
+val string_of_proof: proof -> string
exception MatchingFailure
+(** matching between two terms. Can raise MatchingFailure *)
val matching:
Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
CicUniv.universe_graph ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+(**
+ special unification that checks if the two terms are "simple", and in
+ such case should be significantly faster than CicUnification.fo_unif
+*)
val unification:
Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
CicUniv.universe_graph ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph
-(**
- Performs the beta expansion of the term "where" w.r.t. "what",
- i.e. returns the list of all the terms t s.t. "(t what) = where".
-*)
-val beta_expand:
- ?metas_ok:bool -> ?match_only:bool -> Cic.term -> Cic.term -> Cic.term ->
- Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
- (Cic.term * Cic.substitution * Cic.metasenv * CicUniv.universe_graph) list
-
-
(**
scans the context to find all Declarations "left = right"; returns a
list of tuples (proof, (type, left, right), newmetas). Uses
val find_equalities:
Cic.context -> ProofEngineTypes.proof -> int list * equality list * int
-
-exception TermIsNotAnEquality;;
-
(**
- raises TermIsNotAnEquality if term is not an equation.
- The first Cic.term is a proof of the equation
+ searches the library for equalities that can be applied to the current goal
*)
-val equality_of_term: Cic.term -> Cic.term -> equality
+val find_library_equalities:
+ HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
+ UriManager.UriSet.t * equality list * int
-val term_is_equality: Cic.term -> bool
+(**
+ searches the library for theorems that are not equalities (returned by the
+ function above)
+*)
+val find_library_theorems:
+ HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t ->
+ (Cic.term * Cic.term * Cic.metasenv) list
(**
- superposition_left env target source
- returns a list of new clauses inferred with a left superposition step
- the negative equation "target" and the positive equation "source"
+ searches the context for hypotheses that are not equalities
*)
-(* val superposition_left: environment -> equality -> equality -> equality list *)
+val find_context_hypotheses:
+ environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
+
+
+exception TermIsNotAnEquality;;
(**
- superposition_right newmeta env target source
- returns a list of new clauses inferred with a right superposition step
- the positive equations "target" and "source"
- "newmeta" is the first free meta index, i.e. the first number above the
- highest meta index: its updated value is also returned
+ raises TermIsNotAnEquality if term is not an equation.
+ The first Cic.term is a proof of the equation
*)
-(* val superposition_right: *)
-(* int -> environment -> equality -> equality -> int * equality list *)
+val equality_of_term: Cic.term -> Cic.term -> equality
-(* val demodulation: int -> environment -> equality -> equality -> int * equality *)
+val term_is_equality: Cic.term -> bool
+(** tests a sort of alpha-convertibility between the two terms, but on the
+ metavariables *)
val meta_convertibility: Cic.term -> Cic.term -> bool
-
+
+(** meta convertibility between two equations *)
val meta_convertibility_eq: equality -> equality -> bool
val is_identity: environment -> equality -> bool
val string_of_equality: ?env:environment -> equality -> string
-(* val subsumption: environment -> equality -> equality -> bool *)
-
val metas_of_term: Cic.term -> int list
+(** ensures that metavariables in equality are unique *)
val fix_metas: int -> equality -> int * equality
-
-val extract_differing_subterms:
- Cic.term -> Cic.term -> (Cic.term * Cic.term) option
-
-val build_proof_term: proof (* equality *) -> Cic.term
-
-val find_library_equalities:
- HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
- UriManager.UriSet.t * equality list * int
-
-val find_library_theorems:
- HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t ->
- (UriManager.uri * Cic.term * Cic.term * Cic.metasenv) list
-
-val find_context_hypotheses:
- environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
-
-val string_of_proof: proof -> string
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
(* path indexing implementation *)
(* position of the subterm, subterm (Appl are not stored...) *)
module PSTrie = Trie.Make(PSMap);;
-(*
-(*
- * Trie: maps over lists.
- * Copyright (C) 2000 Jean-Christophe FILLIATRE
- *)
-module PSTrie = struct
- type key = path_string
- type t = Node of PosEqSet.t option * (t PSMap.t)
-
- let empty = Node (None, PSMap.empty)
-
- let rec find l t =
- match (l, t) with
- | [], Node (None, _) -> raise Not_found
- | [], Node (Some v, _) -> v
- | x::r, Node (_, m) -> find r (PSMap.find x m)
-
- let rec mem l t =
- match (l, t) with
- | [], Node (None, _) -> false
- | [], Node (Some _, _) -> true
- | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false
-
- let add l v t =
- let rec ins = function
- | [], Node (_, m) -> Node (Some v, m)
- | x::r, Node (v, m) ->
- let t' = try PSMap.find x m with Not_found -> empty in
- let t'' = ins (r, t') in
- Node (v, PSMap.add x t'' m)
- in
- ins (l, t)
-
- let rec remove l t =
- match (l, t) with
- | [], Node (_, m) -> Node (None, m)
- | x::r, Node (v, m) ->
- try
- let t' = remove r (PSMap.find x m) in
- Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m)
- with Not_found ->
- t
-
- let rec fold f t acc =
- let rec traverse revp t acc = match t with
- | Node (None, m) ->
- PSMap.fold (fun x -> traverse (x::revp)) m acc
- | Node (Some v, m) ->
- f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc)
- in
- traverse [] t acc
-
-end
-*)
-
let index trie equality =
let _, _, (_, l, r, ordering), _, _ = equality in
let index pos trie ps =
let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in
let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in
-(* if PosEqSet.mem (pos, equality) (PSTrie.find ps trie) then *)
-(* Printf.printf "OK: %s, %s indexed\n" (Utils.string_of_pos pos) *)
-(* (Inference.string_of_equality equality); *)
trie
in
match ordering with
else
PSTrie.add ps ps_set trie
with Not_found ->
-(* Printf.printf "NOT_FOUND: %s, %s\n" (Utils.string_of_pos pos) *)
-(* (Inference.string_of_equality equality); *)
trie
-(* raise Not_found *)
in
match ordering with
| Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl
List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
| _ -> PosEqSet.empty
with Not_found ->
-(* Printf.printf "Not_found: %s, term was: %s\n" *)
-(* (CicPp.ppterm hd_term) (CicPp.ppterm term); *)
-(* Printf.printf "map is:\n %s\n\n" *)
-(* (String.concat "\n" *)
-(* (PSMap.fold *)
-(* (fun k v l -> *)
-(* match k with *)
-(* | Index i -> ("Index " ^ (string_of_int i))::l *)
-(* | Term t -> ("Term " ^ (CicPp.ppterm t))::l) *)
-(* map [])); *)
PosEqSet.empty
in
try
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
let configuration_file = ref "../../matita/matita.conf.xml";;
let core_notation_script = "../../matita/core_notation.moo";;
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
open Inference;;
open Utils;;
type theorem = Cic.term * Cic.term * Cic.metasenv;;
-(*
-let symbols_of_equality (_, (_, left, right), _, _) =
- TermSet.union (symbols_of_term left) (symbols_of_term right)
-;;
-*)
-
let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
let m1 = symbols_of_term left in
let m =
TermMap.add k v res)
(symbols_of_term right) m1
in
-(* Printf.printf "symbols_of_equality %s:\n" *)
-(* (string_of_equality equality); *)
-(* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
-(* print_newline (); *)
m
;;
| false ->
let w1, _, (ty, left, right, _), _, a = eq1
and w2, _, (ty', left', right', _), _, a' = eq2 in
-(* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
-(* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
-(* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
match Pervasives.compare w1 w2 with
| 0 ->
let res = (List.length a) - (List.length a') in
let res = Pervasives.compare (List.hd a) (List.hd a') in
if res <> 0 then res else Pervasives.compare eq1 eq2
with Failure "hd" -> Pervasives.compare eq1 eq2
-(* match a, a' with *)
-(* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
-(* let res = Pervasives.compare i j in *)
-(* if res <> 0 then res else Pervasives.compare eq1 eq2 *)
-(* | _, _ -> Pervasives.compare eq1 eq2 *)
)
| res -> res
end
module EqualitySet = Set.Make(OrderedEquality);;
+(**
+ selects one equality from passive. The selection strategy is a combination
+ of weight, age and goal-similarity
+*)
let select env goals passive (active, _) =
processed_clauses := !processed_clauses + 1;
-
let goal =
match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
in
-
let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
let remove eq l =
List.filter (fun e -> e <> eq) l
| [], hd::tl ->
let passive_table =
Indexing.remove_index passive_table hd
-(* if !use_fullred then Indexing.remove_index passive_table hd *)
-(* else passive_table *)
in
(Positive, hd),
(([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
let cardinality map =
TermMap.fold (fun k v res -> res + v) map 0
in
-(* match active with *)
-(* | (Negative, e)::_ -> *)
-(* let symbols = symbols_of_equality e in *)
let symbols =
let _, _, term = goal in
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
- let c1 = abs (c - v) in
- let c2 = v - c1 in
- r1 + c2, r2 + c1
- else
- r1, r2 + v
- in
- let f equality (i, e) =
- let common, others =
- TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
- in
- let c = others + (abs (common - card)) in
- if c < i then (c, equality)
-(* else if c = i then *)
-(* match OrderedEquality.compare equality e with *)
-(* | -1 -> (c, equality) *)
-(* | res -> (i, e) *)
- else (i, e)
- in
- let e1 = EqualitySet.min_elt pos_set in
- let initial =
- let common, others =
- TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
- in
- (others + (abs (common - card))), e1
- in
- let _, current = EqualitySet.fold f pos_set initial in
-(* Printf.printf "\nsymbols-based selection: %s\n\n" *)
-(* (string_of_equality ~env current); *)
- let passive_table =
- Indexing.remove_index passive_table current
-(* if !use_fullred then Indexing.remove_index passive_table current *)
-(* else passive_table *)
- in
- (Positive, current),
- (([], neg_set),
- (remove current pos_list, EqualitySet.remove current pos_set),
- passive_table)
-(* | _ -> *)
-(* let current = EqualitySet.min_elt pos_set in *)
-(* let passive_table = *)
-(* Indexing.remove_index passive_table current *)
-(* (\* if !use_fullred then Indexing.remove_index passive_table current *\) *)
-(* (\* else passive_table *\) *)
-(* in *)
-(* let passive = *)
-(* (neg_list, neg_set), *)
-(* (remove current pos_list, EqualitySet.remove current pos_set), *)
-(* passive_table *)
-(* in *)
-(* (Positive, current), passive *)
+ let card = cardinality symbols in
+ let foldfun k v (r1, r2) =
+ if TermMap.mem k symbols then
+ let c = TermMap.find k symbols in
+ let c1 = abs (c - v) in
+ let c2 = v - c1 in
+ r1 + c2, r2 + c1
+ else
+ r1, r2 + v
+ in
+ let f equality (i, e) =
+ let common, others =
+ TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+ in
+ let c = others + (abs (common - card)) in
+ if c < i then (c, equality)
+ else (i, e)
+ in
+ let e1 = EqualitySet.min_elt pos_set in
+ let initial =
+ let common, others =
+ TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
+ in
+ (others + (abs (common - card))), e1
+ in
+ let _, current = EqualitySet.fold f pos_set initial in
+ let passive_table =
+ Indexing.remove_index passive_table current
+ in
+ (Positive, current),
+ (([], neg_set),
+ (remove current pos_list, EqualitySet.remove current pos_set),
+ passive_table)
)
| _ ->
symbols_counter := !symbols_ratio;
(neg_list, neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
Indexing.remove_index passive_table current
-(* if !use_fullred then Indexing.remove_index passive_table current *)
-(* else passive_table *)
in
(Positive, current), passive
else
;;
+(* initializes the passive set of equalities *)
let make_passive neg pos =
let set_of equalities =
List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
let table =
List.fold_left (fun tbl e -> Indexing.index tbl e)
(Indexing.empty_table ()) pos
-(* if !use_fullred then *)
-(* List.fold_left (fun tbl e -> Indexing.index tbl e) *)
-(* (Indexing.empty_table ()) pos *)
-(* else *)
-(* Indexing.empty_table () *)
in
(neg, set_of neg),
(pos, set_of pos),
;;
+(* adds to passive a list of equalities: new_neg is a list of negative
+ equalities, new_pos a list of positive equalities *)
let add_to_passive passive (new_neg, new_pos) =
let (neg_list, neg_set), (pos_list, pos_set), table = passive in
let ok set equality = not (EqualitySet.mem equality set) in
let neg = List.filter (ok neg_set) new_neg
and pos = List.filter (ok pos_set) new_pos in
let table =
- List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
-(* if !use_fullred then *)
-(* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
-(* else *)
-(* table *)
+ List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
in
let add set equalities =
List.fold_left (fun s e -> EqualitySet.add e s) set equalities
;;
+(* removes from passive equalities that are estimated impossible to activate
+ within the current time limit *)
let prune_passive howmany (active, _) passive =
let (nl, ns), (pl, ps), tbl = passive in
let howmany = float_of_int howmany
else
EqualitySet.empty, EqualitySet.empty
in
-(* let in_weight, ns = pickw in_weight ns in *)
-(* let _, ps = pickw in_weight ps in *)
let ns, ps = pickw in_weight ns ps in
let rec picka w s l =
if w > 0 then
let in_age, ns, nl = picka in_age ns nl in
let _, ps, pl = picka in_age ps pl in
if not (EqualitySet.is_empty ps) then
-(* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
maximal_retained_equality := Some (EqualitySet.max_elt ps);
let tbl =
EqualitySet.fold
(fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
-(* if !use_fullred then *)
-(* EqualitySet.fold *)
-(* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
-(* else *)
-(* tbl *)
in
(nl, ns), (pl, ps), tbl
;;
+(** inference of new equalities between current and some in active *)
let infer env sign current (active_list, active_table) =
let new_neg, new_pos =
match sign with
;;
+(** simplifies current using active and passive *)
let forward_simplify env (sign, current) ?passive (active_list, active_table) =
let pl, passive_table =
match passive with
pn @ pp, Some pt
in
let all = if pl = [] then active_list else active_list @ pl in
-
- (* let rec find_duplicate sign current = function *)
-(* | [] -> false *)
-(* | (s, eq)::tl when s = sign -> *)
-(* if meta_convertibility_eq current eq then true *)
-(* else find_duplicate sign current tl *)
-(* | _::tl -> find_duplicate sign current tl *)
-(* in *)
-
-(* let res = *)
-(* if sign = Positive then *)
-(* Indexing.subsumption env active_table current *)
-(* else *)
-(* false *)
-(* in *)
-(* if res then *)
-(* None *)
-(* else *)
let demodulate table current =
let newmeta, newcurrent =
| Some passive_table ->
if Indexing.in_index passive_table c then None
else res
-
-(* | Some (s, c) -> if find_duplicate s c all then None else res *)
-
-(* if s = Utils.Negative then *)
-(* res *)
-(* else *)
-(* if Indexing.subsumption env active_table c then *)
-(* None *)
-(* else ( *)
-(* match passive_table with *)
-(* | None -> res *)
-(* | Some passive_table -> *)
-(* if Indexing.subsumption env passive_table c then *)
-(* None *)
-(* else *)
-(* res *)
-(* ) *)
-
-(* let pred (sign, eq) = *)
-(* if sign <> s then false *)
-(* else subsumption env c eq *)
-(* in *)
-(* if List.exists pred all then None *)
-(* else res *)
;;
type fs_time_info_t = {
let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
+(** simplifies new using active and passive *)
let forward_simplify_new env (new_neg, new_pos) ?passive active =
let t1 = Unix.gettimeofday () in
maxmeta := newmeta;
newtarget
in
-(* let f sign' target (sign, eq) = *)
-(* if sign <> sign' then false *)
-(* else subsumption env target eq *)
-(* in *)
-
let t1 = Unix.gettimeofday () in
let new_neg, new_pos =
(fun e -> not ((fst (Indexing.subsumption env active_table e)) ||
(fst (Indexing.subsumption env passive_table e))))
in
-
- let t1 = Unix.gettimeofday () in
-
-(* let new_neg, new_pos = *)
-(* List.filter subs new_neg, *)
-(* List.filter subs new_pos *)
-(* in *)
-
-(* let new_neg, new_pos = *)
-(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
-(* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
-(* in *)
-
- let t2 = Unix.gettimeofday () in
- fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
-
+(* let t1 = Unix.gettimeofday () in *)
+(* let t2 = Unix.gettimeofday () in *)
+(* fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); *)
let is_duplicate =
match passive_table with
| None ->
(Indexing.in_index passive_table e)))
in
new_neg, List.filter is_duplicate new_pos
-
-(* new_neg, new_pos *)
-
-(* let res = *)
-(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
-(* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
-(* in *)
-(* res *)
;;
+(** simplifies active usign new *)
let backward_simplify_active env new_pos new_table min_weight active =
let active_list, active_table = active in
let active_list, newa =
res, tbl
else if (is_identity env eq) || (find eq res) then (
res, tbl
- ) (* else if (find eq res) then *)
-(* res, tbl *)
+ )
else
(s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
active_list ([], Indexing.empty_table ()),
;;
+(** simplifies passive using new *)
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) =
let ew, _, _, _, _ = equality in
if ew < min_weight then
-(* let _ = debug_print (lazy (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
;;
+(* returns an estimation of how many equalities in passive can be activated
+ within the current time limit *)
let get_selection_estimate () =
elapsed_time := (Unix.gettimeofday ()) -. !start_time;
-(* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
+ (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
int_of_float (
ceil ((float_of_int !processed_clauses) *.
((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
;;
+(** initializes the set of goals *)
let make_goals goal =
let active = []
and passive = [0, [goal]] in
;;
+(** initializes the set of theorems *)
let make_theorems theorems =
theorems, []
-(* let active = [] *)
-(* and passive = theorems in *)
-(* active, passive *)
;;
| [] -> false, (active, passive)
;;
-
+
+(** simplifies a goal with equalities in active and passive *)
let simplify_goal env goal ?passive (active_list, active_table) =
let pl, passive_table =
match passive with
let changed', goal = demodulate passive_table goal in
(changed || changed'), goal
in
- let _ =
- let p, _, t = goal in
- debug_print
- (lazy
- (Printf.sprintf "Goal after demodulation: %s, %s"
- (string_of_proof p) (CicPp.ppterm t)))
- in
changed, goal
;;
| None ->
let p_theorems = List.map (mapfun active_table) p_theorems in
List.fold_left (foldfun active_table) ([], p_theorems) a_theorems
-(* List.map (demodulate active_table) theorems *)
| Some passive_table ->
let p_theorems = List.map (mapfun active_table) p_theorems in
let p_theorems, a_theorems =
List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in
let p_theorems = List.map (mapfun passive_table) p_theorems in
List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
-(* let theorems = List.map (demodulate active_table) theorems in *)
-(* List.map (demodulate passive_table) theorems *)
;;
+(* 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 module HL = HelmLibraryObjects in
;;
-(*
-let apply_to_goal env theorems active (depth, goals) =
- let _ =
- debug_print ("apply_to_goal: " ^ (string_of_int (List.length goals)))
- in
- let metasenv, context, ugraph = env in
- let goal = List.hd goals in
- let proof, metas, term = goal in
-(* debug_print *)
-(* (Printf.sprintf "apply_to_goal with goal: %s" (CicPp.ppterm term)); *)
- let newmeta = CicMkImplicit.new_meta metasenv [] in
- let metasenv = (newmeta, context, term)::metasenv @ metas in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let status =
- ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta)
- in
- let rec aux = function
- | [] -> false, [] (* goals *) (* None *)
- | (theorem, thmty, _)::tl ->
- try
- let subst_in, (newproof, newgoals) =
- PrimitiveTactics.apply_tac_verbose ~term:theorem status
- in
- if newgoals = [] then
- let _, _, p, _ = newproof in
- let newp =
- let rec repl = function
- | Inference.ProofGoalBlock (_, gp) ->
- Inference.ProofGoalBlock (Inference.BasicProof p, gp)
- | Inference.NoProof -> Inference.BasicProof p
- | Inference.BasicProof _ -> Inference.BasicProof p
- | Inference.SubProof (t, i, p2) ->
- Inference.SubProof (t, i, repl p2)
- | _ -> assert false
- in
- repl proof
- in
- true, [[newp, metas, term]] (* Some newp *)
- else if List.length newgoals = 1 then
- let _, menv, p, _ = newproof in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- let goals =
- List.map
- (fun i ->
- let _, _, ty = CicUtil.lookup_meta i menv in
- let proof =
- Inference.SubProof
- (p, i, Inference.BasicProof (Cic.Meta (i, irl)))
- in (proof, menv, ty))
- newgoals
- in
- let res, others = aux tl in
- if res then (true, others) else (false, goals::others)
- else
- aux tl
- with ProofEngineTypes.Fail msg ->
- (* debug_print ("FAIL!!:" ^ msg); *)
- aux tl
- in
- let r, l =
- if Inference.term_is_equality term then
- let rec appleq = function
- | [] -> false, []
- | (Positive, equality)::tl ->
- let ok, _, newproof = apply_equality_to_goal env equality goal in
- if ok then true, [(depth, [newproof, metas, term])] else appleq tl
- | _::tl -> appleq tl
- in
- let al, _ = active in
- appleq al
- else
- false, []
- in
- if r = true then r, l else
- let r, l = aux theorems in
- if r = true then
- r, List.map (fun l -> (depth+1, l)) l
- else
- r, (depth, goals)::(List.map (fun l -> (depth+1, l)) l)
-;;
-*)
-
-let new_meta () =
- incr maxmeta; !maxmeta
+let new_meta metasenv =
+ let m = CicMkImplicit.new_meta metasenv [] in
+ incr maxmeta;
+ while !maxmeta <= m do incr maxmeta done;
+ !maxmeta
;;
+(* applies a theorem or an equality to goal, returning a list of subgoals or
+ an indication of failure *)
let apply_to_goal env theorems ?passive active goal =
let metasenv, context, ugraph = env in
let proof, metas, term = goal in
- debug_print
- (lazy
- (Printf.sprintf "apply_to_goal with goal: %s"
- (* (string_of_proof proof) *)(CicPp.ppterm term)));
+ (* debug_print *)
+ (* (lazy *)
+ (* (Printf.sprintf "apply_to_goal with goal: %s" *)
+ (* (\* (string_of_proof proof) *\)(CicPp.ppterm term))); *)
let status =
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
let proof', newmeta =
let rec get_meta = function
- | SubProof (t, i, _) -> t, i
+ | SubProof (t, i, p) ->
+ let t', i' = get_meta p in
+ if i' = -1 then t, i else t', i'
| ProofGoalBlock (_, p) -> get_meta p
- | _ ->
- let n = new_meta () in (* CicMkImplicit.new_meta metasenv [] in *)
- Cic.Meta (n, irl), n
+ | _ -> Cic.Implicit None, -1
in
- get_meta proof
+ let p, m = get_meta proof in
+ if m = -1 then
+ let n = new_meta (metasenv @ metas) in
+ Cic.Meta (n, irl), n
+ else
+ p, m
in
-(* let newmeta = CicMkImplicit.new_meta metasenv [] in *)
let metasenv = (newmeta, context, term)::metasenv @ metas in
- ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta)
-(* ((None, metasenv, proof', term), newmeta) *)
+ let bit = new_meta metasenv, context, term in
+ let metasenv' = bit::metasenv in
+ ((None, metasenv', Cic.Meta (newmeta, irl), term), newmeta)
in
let rec aux = function
- | [] -> `No (* , [], [] *)
+ | [] -> `No
| (theorem, thmty, _)::tl ->
try
let subst, (newproof, newgoals) =
in
let _, m = status in
let subst = List.filter (fun (i, _) -> i = m) subst in
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "m = %d\nsubst = %s\n" *)
-(* m (print_subst subst))); *)
`Ok (subst, [newp, metas, term])
else
let _, menv, p, _ = newproof in
| SubProof (t, i, p) ->
SubProof (t, i, gp p)
| ProofGoalBlock (sp1, sp2) ->
-(* SubProof (p, i, sp) *)
ProofGoalBlock (sp1, gp sp2)
-(* gp sp *)
| BasicProof _
| NoProof ->
SubProof (p, i, BasicProof (Cic.Meta (i, irl)))
ProofSymBlock (s, gp sp)
| ProofBlock (s, u, nt, t, pe, sp) ->
ProofBlock (s, u, nt, t, pe, gp sp)
-(* | _ -> assert false *)
in gp proof
in
- debug_print
- (lazy
- (Printf.sprintf "new sub goal: %s"
- (* (string_of_proof p') *)(CicPp.ppterm ty)));
(p', menv, ty))
newgoals
in
Pervasives.compare (weight t1) (weight t2))
goals
in
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "\nGoOn with subst: %s" (print_subst subst))); *)
let best = aux tl in
match best with
| `Ok (_, _) -> best
| `No -> `GoOn ([subst, goals])
- | `GoOn sl(* , subst', goals' *) ->
-(* if (List.length goals') < (List.length goals) then best *)
-(* else `GoOn, subst, goals *)
- `GoOn ((subst, goals)::sl)
+ | `GoOn sl -> `GoOn ((subst, goals)::sl)
with ProofEngineTypes.Fail msg ->
aux tl
in
let r, s, l =
if Inference.term_is_equality term then
-(* let _ = debug_print (lazy "OK, is equality!!") in *)
let rec appleq_a = function
| [] -> false, [], []
| (Positive, equality)::tl ->
;;
-let apply_to_goal_conj env theorems ?passive active (depth, goals) =
- let rec aux = function
- | goal::tl ->
- let propagate_subst subst (proof, metas, term) =
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n" *)
-(* (print_subst subst) (string_of_proof proof) *)
-(* (CicPp.ppterm term))); *)
- let rec repl = function
- | NoProof -> NoProof
- | BasicProof t ->
- BasicProof (CicMetaSubst.apply_subst subst t)
- | ProofGoalBlock (p, pb) ->
-(* debug_print (lazy "HERE"); *)
- let pb' = repl pb in
- ProofGoalBlock (p, pb')
- | SubProof (t, i, p) ->
- let t' = CicMetaSubst.apply_subst subst t in
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf *)
-(* "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n" *)
-(* i (CicPp.ppterm t) (print_subst subst) *)
-(* (CicPp.ppterm t'))); *)
- let p = repl p in
- SubProof (t', i, p)
- | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
- | ProofBlock (s, u, nty, t, pe, p) ->
- ProofBlock (subst @ s, u, nty, t, pe, p)
- in (repl proof, metas, term)
- in
- let r = apply_to_goal env theorems ?passive active goal in (
- match r with
- | `No -> `No (depth, goals)
- | `GoOn sl (* (subst, gl) *) ->
-(* let tl = List.map (propagate_subst subst) tl in *)
-(* debug_print (lazy "GO ON!!!"); *)
- let l =
- List.map
- (fun (s, gl) ->
- (depth+1, gl @ (List.map (propagate_subst s) tl))) sl
+(* sorts a conjunction of goals in order to detect earlier if it is
+ unsatisfiable. Non-predicate goals are placed at the end of the list *)
+let sort_goal_conj (metasenv, context, ugraph) (depth, gl) =
+ let gl =
+ List.stable_sort
+ (fun (_, e1, g1) (_, e2, g2) ->
+ let ty1, _ =
+ CicTypeChecker.type_of_aux' (e1 @ metasenv) context g1 ugraph
+ and ty2, _ =
+ CicTypeChecker.type_of_aux' (e2 @ metasenv) context g2 ugraph
+ in
+ let prop1 =
+ let b, _ =
+ CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty1 ugraph
+ in
+ if b then 0 else 1
+ and prop2 =
+ let b, _ =
+ CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty2 ugraph
+ in
+ if b then 0 else 1
+ in
+ if prop1 = 0 && prop2 = 0 then
+ let e1 = if Inference.term_is_equality g1 then 0 else 1
+ and e2 = if Inference.term_is_equality g2 then 0 else 1 in
+ e1 - e2
+ else
+ prop1 - prop2)
+ gl
+ in
+ (depth, gl)
+;;
+
+
+let is_meta_closed goals =
+ List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals
+;;
+
+
+(* applies a series of theorems/equalities to a conjunction of goals *)
+let rec apply_to_goal_conj env theorems ?passive active (depth, goals) =
+ let aux (goal, r) tl =
+ let propagate_subst subst (proof, metas, term) =
+ let rec repl = function
+ | NoProof -> NoProof
+ | BasicProof t ->
+ BasicProof (CicMetaSubst.apply_subst subst t)
+ | ProofGoalBlock (p, pb) ->
+ let pb' = repl pb in
+ ProofGoalBlock (p, pb')
+ | SubProof (t, i, p) ->
+ let t' = CicMetaSubst.apply_subst subst t in
+ let p = repl p in
+ SubProof (t', i, p)
+ | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
+ | ProofBlock (s, u, nty, t, pe, p) ->
+ ProofBlock (subst @ s, u, nty, t, pe, p)
+ in (repl proof, metas, term)
+ in
+ (* let r = apply_to_goal env theorems ?passive active goal in *) (
+ match r with
+ | `No -> `No (depth, goals)
+ | `GoOn sl ->
+ let l =
+ List.map
+ (fun (s, gl) ->
+ let tl = List.map (propagate_subst s) tl in
+ sort_goal_conj env (depth+1, gl @ tl)) sl
+ in
+ `GoOn l
+ | `Ok (subst, gl) ->
+ if tl = [] then
+ `Ok (depth, gl)
+ else
+ let p, _, _ = List.hd gl in
+ let subproof =
+ let rec repl = function
+ | SubProof (_, _, p) -> repl p
+ | ProofGoalBlock (p1, p2) ->
+ ProofGoalBlock (repl p1, repl p2)
+ | p -> p
in
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "%s\n" *)
-(* (String.concat "; " *)
-(* (List.map *)
-(* (fun (s, gl) -> *)
-(* (Printf.sprintf "[%s]" *)
-(* (String.concat "; " *)
-(* (List.map *)
-(* (fun (p, _, g) -> *)
-(* (Printf.sprintf "<%s, %s>" *)
-(* (string_of_proof p) *)
-(* (CicPp.ppterm g))) gl)))) l)))); *)
- `GoOn l (* (depth+1, gl @ tl) *)
- | `Ok (subst, gl) ->
- if tl = [] then
-(* let _ = *)
-(* let p, _, t = List.hd gl in *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "OK: %s, %s\n" *)
-(* (string_of_proof p) (CicPp.ppterm t))) *)
-(* in *)
- `Ok (depth, gl)
- else
- let p, _, _ = List.hd gl in
- let subproof =
- let rec repl = function
- | SubProof (_, _, p) -> repl p
- | ProofGoalBlock (p1, p2) ->
- ProofGoalBlock (repl p1, repl p2)
- | p -> p
- in
- build_proof_term (repl p)
- in
- let i =
- let rec get_meta = function
- | SubProof (_, i, p) -> max i (get_meta p)
- | ProofGoalBlock (_, p) -> get_meta p
- | _ -> -1 (* assert false *)
- in
- get_meta p
- in
- let subst =
- let _, (context, _, _) = List.hd subst in
- [i, (context, subproof, Cic.Implicit None)]
- in
- let tl = List.map (propagate_subst subst) tl in
- `GoOn ([depth+1, tl])
- )
- | _ -> assert false
+ build_proof_term (repl p)
+ in
+ let i =
+ let rec get_meta = function
+ | SubProof (_, i, p) ->
+ let i' = get_meta p in
+ if i' = -1 then i else i'
+(* max i (get_meta p) *)
+ | ProofGoalBlock (_, p) -> get_meta p
+ | _ -> -1
+ in
+ get_meta p
+ in
+ let subst =
+ let _, (context, _, _) = List.hd subst in
+ [i, (context, subproof, Cic.Implicit None)]
+ in
+ let tl = List.map (propagate_subst subst) tl in
+ let conj = sort_goal_conj env (depth(* +1 *), tl) in
+ `GoOn ([conj])
+ )
in
- debug_print
- (lazy
- (Printf.sprintf "apply_to_goal_conj (%d, [%s])"
- depth
- (String.concat "; "
- (List.map (fun (_, _, t) -> CicPp.ppterm t) goals))));
- if depth > !maxdepth || (List.length goals) > !maxwidth then (
- debug_print
- (lazy (Printf.sprintf "Pruning because depth = %d, width = %d"
- depth (List.length goals)));
+ if depth > !maxdepth || (List.length goals) > !maxwidth then
`No (depth, goals)
- ) else
- aux goals
+ else
+ let rec search_best res = function
+ | [] -> res
+ | goal::tl ->
+ let r = apply_to_goal env theorems ?passive active goal in
+ match r with
+ | `Ok _ -> (goal, r)
+ | `No -> search_best res tl
+ | `GoOn l ->
+ let newres =
+ match res with
+ | _, `Ok _ -> assert false
+ | _, `No -> goal, r
+ | _, `GoOn l2 ->
+ if (List.length l) < (List.length l2) then goal, r else res
+ in
+ search_best newres tl
+ in
+ let hd = List.hd goals in
+ let res = hd, (apply_to_goal env theorems ?passive active hd) in
+ let best =
+ match res with
+ | _, `Ok _ -> res
+ | _, _ -> search_best res (List.tl goals)
+ in
+ let res = aux best (List.filter (fun g -> g != (fst best)) goals) in
+ match res with
+ | `GoOn ([conj]) when is_meta_closed (snd conj) &&
+ (List.length (snd conj)) < (List.length goals)->
+ apply_to_goal_conj env theorems ?passive active conj
+ | _ -> res
;;
+(*
module OrderedGoals = struct
type t = int * (Inference.proof * Cic.metasenv * Cic.term) list
) else
false) l1 l2
in !res
-(* let res = Pervasives.compare g1 g2 in *)
-(* let _ = *)
-(* let print_goals (d, gl) = *)
-(* let gl' = List.map (fun (_, _, t) -> CicPp.ppterm t) gl in *)
-(* Printf.sprintf "%d, [%s]" d (String.concat "; " gl') *)
-(* in *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "comparing g1:%s and g2:%s, res: %d\n" *)
-(* (print_goals g1) (print_goals g2) res)) *)
-(* in *)
-(* res *)
end
module GoalsSet = Set.Make(OrderedGoals);;
exception SearchSpaceOver;;
+*)
+(*
let apply_to_goals env is_passive_empty theorems active goals =
debug_print (lazy "\n\n\tapply_to_goals\n\n");
let add_to set goals =
in
true, GoalsSet.singleton newgoals
| `GoOn newgoals ->
-(* let print_set set msg = *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "%s:\n%s" msg *)
-(* (String.concat "\n" *)
-(* (GoalsSet.fold *)
-(* (fun (d, gl) l -> *)
-(* let gl' = *)
-(* List.map (fun (_, _, t) -> CicPp.ppterm t) gl *)
-(* in *)
-(* let s = *)
-(* Printf.sprintf "%d, [%s]" d *)
-(* (String.concat "; " gl') *)
-(* in *)
-(* s::l) set [])))) *)
-(* in *)
-
-(* let r, s = *)
-(* try aux set tl with SearchSpaceOver -> false, GoalsSet.empty *)
-(* in *)
-(* if r then *)
-(* r, s *)
-(* else *)
-
let set' = add_to set (goals::tl) in
-(* print_set set "SET BEFORE"; *)
-(* let n = GoalsSet.cardinal set in *)
let set' = add_to set' newgoals in
-(* print_set set "SET AFTER"; *)
-(* let m = GoalsSet.cardinal set in *)
-(* if n < m then *)
false, set'
-(* else *)
-(* let _ = print_set set "SET didn't change" in *)
-(* aux set tl *)
| `No newgoals ->
aux set tl
-(* let set = add_to set (newgoals::goals::tl) in *)
-(* let res, set = aux set tl in *)
-(* res, set *)
in
let n = List.length goals in
let res, goals = aux (add_to GoalsSet.empty goals) goals in
else
res, goals
;;
+*)
+
+
+(* sorts the list of passive goals to minimize the search for a proof (doesn't
+ work that well yet...) *)
+let sort_passive_goals goals =
+ List.stable_sort
+ (fun (d1, l1) (d2, l2) ->
+ let r1 = d2 - d1
+ and r2 = (List.length l1) - (List.length l2) in
+ let foldfun ht (_, _, t) =
+ let _ = List.map (fun i -> Hashtbl.replace ht i 1) (metas_of_term t)
+ in ht
+ in
+ let m1 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l1)
+ and m2 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l2)
+ in let r3 = m1 - m2 in
+ if r3 <> 0 then r3
+ else if r2 <> 0 then r2
+ else r1)
+ (* let _, _, g1 = List.hd l1 *)
+(* and _, _, g2 = List.hd l2 in *)
+(* let e1 = if Inference.term_is_equality g1 then 0 else 1 *)
+(* and e2 = if Inference.term_is_equality g2 then 0 else 1 *)
+(* in let r4 = e1 - e2 in *)
+(* if r4 <> 0 then r3 else r1) *)
+ goals
+;;
+
+
+let print_goals goals =
+ (String.concat "\n"
+ (List.map
+ (fun (d, gl) ->
+ let gl' =
+ List.map
+ (fun (p, _, t) ->
+ (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
+ in
+ Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
+;;
+(* tries to prove the first conjunction in goals with applications of
+ theorems/equalities, returning new sub-goals or an indication of success *)
let apply_goal_to_theorems dbd env theorems ?passive active goals =
-(* let theorems, _ = theorems in *)
- let context_hyp, library_thms = theorems in
- let thm_uris =
- List.fold_left
- (fun s (u, _, _, _) -> UriManager.UriSet.add u s)
- UriManager.UriSet.empty library_thms
- in
+ let theorems, _ = theorems in
let a_goals, p_goals = goals in
let goal = List.hd a_goals in
- let rec aux = function
- | [] -> false, (a_goals, p_goals)
- | theorem::tl ->
- let res = apply_to_goal_conj env [theorem] ?passive active goal in
- match res with
- | `Ok newgoals ->
- true, ([newgoals], [])
- | `No _ ->
- aux tl
-(* false, (a_goals, p_goals) *)
- | `GoOn newgoals ->
- let res, (ag, pg) = aux tl in
- if res then
- res, (ag, pg)
+ let not_in_active gl =
+ not
+ (List.exists
+ (fun (_, gl') ->
+ if (List.length gl) = (List.length gl') then
+ List.for_all2 (fun (_, _, g1) (_, _, g2) -> g1 = g2) gl gl'
else
- let newgoals =
- List.filter
- (fun (d, gl) ->
- (d <= !maxdepth) && (List.length gl) <= !maxwidth)
- newgoals in
- let p_goals = newgoals @ pg in
- let p_goals =
- List.stable_sort
- (fun (d1, l1) (d2, l2) -> (List.length l1) - (List.length l2))
- p_goals
- in
- res, (ag, p_goals)
+ false)
+ a_goals)
in
- let theorems =
-(* let ty = *)
-(* match goal with *)
-(* | (_, (_, _, t)::_) -> t *)
-(* | _ -> assert false *)
-(* in *)
-(* if CicUtil.is_meta_closed ty then *)
-(* let _ = *)
-(* debug_print (lazy (Printf.sprintf "META CLOSED: %s" (CicPp.ppterm ty))) *)
-(* in *)
-(* let metasenv, context, ugraph = env in *)
-(* let uris = *)
-(* MetadataConstraints.sigmatch ~dbd (MetadataConstraints.signature_of ty) *)
-(* in *)
-(* let uris = List.sort (fun (i, _) (j, _) -> Pervasives.compare i j) uris in *)
-(* let uris = *)
-(* List.filter *)
-(* (fun u -> UriManager.UriSet.mem u thm_uris) (List.map snd uris) *)
-(* in *)
-(* List.map *)
-(* (fun u -> *)
-(* let t = CicUtil.term_of_uri u in *)
-(* let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in *)
-(* (t, ty, [])) *)
-(* uris *)
-(* else *)
- List.map (fun (_, t, ty, m) -> (t, ty, m)) library_thms
+ let aux theorems =
+ let res = apply_to_goal_conj env theorems ?passive active goal in
+ match res with
+ | `Ok newgoals ->
+ true, ([newgoals], [])
+ | `No _ ->
+ false, (a_goals, p_goals)
+ | `GoOn newgoals ->
+ let newgoals =
+ List.filter
+ (fun (d, gl) ->
+ (d <= !maxdepth) && (List.length gl) <= !maxwidth &&
+ not_in_active gl)
+ newgoals in
+ let p_goals = newgoals @ p_goals in
+ let p_goals = sort_passive_goals p_goals in
+ false, (a_goals, p_goals)
in
- aux (context_hyp @ theorems)
+ aux theorems
;;
;;
+(* given-clause algorithm with lazy reduction strategy *)
let rec given_clause dbd env goals theorems passive active =
let goals = simplify_goals env goals active in
let ok, goals = activate_goal goals in
-(* let theorems = simplify_theorems env theorems active in *)
+ (* let theorems = simplify_theorems env theorems active in *)
if ok then
let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
if ok then
passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
kept_clauses := (size_of_passive passive) + (size_of_active active);
-
-(* (\* let goals = simplify_goals env goals active in *\) *)
-(* (\* let theorems = simplify_theorems env theorems active in *\) *)
-(* let is_passive_empty = passive_is_empty passive in *)
-(* try *)
-(* let ok, goals = false, [] in (\* apply_to_goals env is_passive_empty theorems active goals in *\) *)
-(* if ok then *)
-(* let proof = *)
-(* match goals with *)
-(* | (_, [proof, _, _])::_ -> Some proof *)
-(* | _ -> assert false *)
-(* in *)
-(* ParamodulationSuccess (proof, env) *)
-(* else *)
match passive_is_empty passive with
| true -> (* ParamodulationFailure *)
given_clause dbd env goals theorems passive active
(lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current)));
let _, proof, _, _, _ = current in
- ParamodulationSuccess (Some proof (* current *), env)
+ ParamodulationSuccess (Some proof, env)
) else (
debug_print
(lazy "\n================================================");
| Some goal -> let _, proof, _, _, _ = goal in Some proof
| None -> None
in
- ParamodulationSuccess (proof (* goal *), env)
+ ParamodulationSuccess (proof, env)
else
let t1 = Unix.gettimeofday () in
let new' = forward_simplify_new env new' active in
in
nn @ al @ pp, tbl
in
-(* let _ = *)
-(* Printf.printf "active:\n%s\n" *)
-(* (String.concat "\n" *)
-(* ((List.map *)
-(* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
-(* (string_of_equality ~env e)) (fst active)))); *)
-(* print_newline (); *)
-(* in *)
-(* let _ = *)
-(* match new' with *)
-(* | neg, pos -> *)
-(* Printf.printf "new':\n%s\n" *)
-(* (String.concat "\n" *)
-(* ((List.map *)
-(* (fun e -> "Negative " ^ *)
-(* (string_of_equality ~env e)) neg) @ *)
-(* (List.map *)
-(* (fun e -> "Positive " ^ *)
-(* (string_of_equality ~env e)) pos))); *)
-(* print_newline (); *)
-(* in *)
match contains_empty env new' with
| false, _ ->
let active =
in
let passive = add_to_passive passive new' in
let (_, ns), (_, ps), _ = passive in
-(* Printf.printf "passive:\n%s\n" *)
-(* (String.concat "\n" *)
-(* ((List.map (fun e -> "Negative " ^ *)
-(* (string_of_equality ~env e)) *)
-(* (EqualitySet.elements ns)) @ *)
-(* (List.map (fun e -> "Positive " ^ *)
-(* (string_of_equality ~env e)) *)
-(* (EqualitySet.elements ps)))); *)
-(* print_newline (); *)
given_clause dbd env goals theorems passive active
| true, goal ->
let proof =
let _, proof, _, _, _ = goal in Some proof
| None -> None
in
- ParamodulationSuccess (proof (* goal *), env)
+ ParamodulationSuccess (proof, env)
)
-(* with SearchSpaceOver -> *)
-(* ParamodulationFailure *)
;;
+(** given-clause algorithm with full reduction strategy *)
let rec given_clause_fullred dbd env goals theorems passive active =
let goals = simplify_goals env goals ~passive active in
let ok, goals = activate_goal goals in
(* let theorems = simplify_theorems env theorems ~passive active in *)
if ok then
- let _ =
- let print_goals goals =
- (String.concat "\n"
- (List.map
- (fun (d, gl) ->
- let gl' =
- List.map
- (fun (p, _, t) ->
- (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
- in
- Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
- in
- debug_print
- (lazy
- (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n"
- (print_goals (fst goals)) (print_goals (snd goals))))
- in
+(* let _ = *)
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" *)
+(* (print_goals (fst goals)) (print_goals (snd goals)))); *)
+(* let current = List.hd (fst goals) in *)
+(* let p, _, t = List.hd (snd current) in *)
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "goal activated:\n%s\n%s\n" *)
+(* (CicPp.ppterm t) (string_of_proof p))); *)
+(* in *)
let ok, goals =
apply_goal_to_theorems dbd env theorems ~passive active goals
in
let time2 = Unix.gettimeofday () in
passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
-
+
kept_clauses := (size_of_passive passive) + (size_of_active active);
-
-(* try *)
-(* let ok, goals = apply_to_goals env is_passive_empty theorems active goals in *)
-(* if ok then *)
-(* let proof = *)
-(* match goals with *)
-(* | (_, [proof, _, _])::_ -> Some proof *)
-(* | _ -> assert false *)
-(* in *)
-(* ParamodulationSuccess (proof, env) *)
-(* else *)
-(* let _ = *)
-(* debug_print *)
-(* (lazy ("new_goals: " ^ (string_of_int (List.length goals)))); *)
-(* debug_print *)
-(* (lazy *)
-(* (String.concat "\n" *)
-(* (List.map *)
-(* (fun (d, gl) -> *)
-(* let gl' = *)
-(* List.map *)
-(* (fun (p, _, t) -> *)
-(* (\* (string_of_proof p) ^ ", " ^ *\) (CicPp.ppterm t)) gl *)
-(* in *)
-(* Printf.sprintf "%d: %s" d (String.concat "; " gl')) *)
-(* goals))); *)
-(* in *)
match passive_is_empty passive with
| true -> (* ParamodulationFailure *)
given_clause_fullred dbd env goals theorems passive active
(lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current)));
let _, proof, _, _, _ = current in
- ParamodulationSuccess (Some proof (* current *), env)
+ ParamodulationSuccess (Some proof, env)
) else (
debug_print
(lazy "\n================================================");
match contains_empty env new' with
| false, _ ->
let passive = add_to_passive passive new' in
-(* let (_, ns), (_, ps), _ = passive in *)
-(* Printf.printf "passive:\n%s\n" *)
-(* (String.concat "\n" *)
-(* ((List.map (fun e -> "Negative " ^ *)
-(* (string_of_equality ~env e)) *)
-(* (EqualitySet.elements ns)) @ *)
-(* (List.map (fun e -> "Positive " ^ *)
-(* (string_of_equality ~env e)) *)
-(* (EqualitySet.elements ps)))); *)
-(* print_newline (); *)
given_clause_fullred dbd env goals theorems passive active
| true, goal ->
let proof =
| Some goal -> let _, proof, _, _, _ = goal in Some proof
| None -> None
in
- ParamodulationSuccess (proof (* goal *), env)
+ ParamodulationSuccess (proof, env)
)
-(* with SearchSpaceOver -> *)
-(* ParamodulationFailure *)
;;
-(* let given_clause_ref = ref given_clause;; *)
let main dbd full term metasenv ugraph =
let module C = Cic in
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
- Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
- print_newline ();
+ 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 new_meta_goal = Cic.Meta (goal', irl) in *)
let env = (metasenv, context, ugraph) in
+ 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
- context_hyp, theorems
+ context_hyp @ theorems, []
else
let refl_equal =
let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
in
let t = CicUtil.term_of_uri refl_equal in
let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
- [], [(refl_equal, t, ty, [])]
+ [(t, ty, [])], []
in
+ let t2 = Unix.gettimeofday () in
+ debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
let _ =
debug_print
(lazy
"Theorems:\n-------------------------------------\n%s\n"
(String.concat "\n"
(List.map
- (fun (_, t, ty, _) ->
+ (fun (t, ty, _) ->
Printf.sprintf
"Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty))
- (snd theorems)))))
+ (fst theorems)))))
in
try
let goal = Inference.BasicProof new_meta_goal, [], goal in
-(* let term_equality = equality_of_term new_meta_goal goal in *)
-(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *)
-(* if is_identity env term_equality then *)
-(* let proof = *)
-(* Cic.Appl [Cic.MutConstruct (\* reflexivity *\) *)
-(* (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); *)
-(* eq_ty; left] *)
-(* in *)
-(* let _ = *)
-(* Printf.printf "OK, found a proof!\n"; *)
-(* let names = names_of_context context in *)
-(* print_endline (PP.pp proof names) *)
-(* in *)
-(* () *)
-(* else *)
- 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_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
- )
+ 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_table ()) active
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
+ 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
- let active = make_active () in
- let passive = make_passive [] (* [term_equality] *) equalities in
- Printf.printf "\ncurrent goal: %s\n"
- (let _, _, g = goal in CicPp.ppterm g);
-(* (string_of_equality ~env term_equality); *)
- Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
- Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
- Printf.printf "\nequalities:\n%s\n"
- (String.concat "\n"
- (List.map
- (string_of_equality ~env)
- (equalities @ library_equalities)));
+ 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 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" (print_metasenv metasenv);
+ Printf.printf "\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (string_of_equality ~env)
+ (equalities @ library_equalities)));
print_endline "--------------------------------------------------";
let start = Unix.gettimeofday () in
print_endline "GO!";
start_time := Unix.gettimeofday ();
-(* let res = *)
-(* (if !use_fullred then given_clause_fullred else given_clause) *)
-(* env [0, [goal]] theorems passive active *)
-(* in *)
let res =
let goals = make_goals goal in
-(* and theorems = make_theorems theorems in *)
(if !use_fullred then given_clause_fullred else given_clause)
dbd env goals theorems passive active
in
match res with
| ParamodulationFailure ->
Printf.printf "NO proof found! :-(\n\n"
- | ParamodulationSuccess (Some proof (* goal *), env) ->
-(* let proof = Inference.build_proof_term goal in *)
+ | ParamodulationSuccess (Some proof, env) ->
let proof = Inference.build_proof_term proof in
Printf.printf "OK, found a proof!\n";
(* REMEMBER: we have to instantiate meta_proof, we should use
(fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
in
let _ =
-(* Printf.printf "OK, found a proof!\n"; *)
-(* (\* 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 *)
-(* print_endline (PP.pp proof names); *)
try
let ty, ug =
CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
in
-(* Printf.printf "OK, found a proof!\n"; *)
-(* (\* 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 *)
-(* print_endline (PP.pp proof names); *)
- (* print_endline (PP.ppterm proof); *)
-
print_endline (string_of_float (finish -. start));
Printf.printf
"\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
let goal = Inference.BasicProof new_meta_goal, [], goal in
- let res, time =
+ let res, time =
+ let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
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
(List.map string_of_equality res))));
res
in
+ debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
+ let t1 = Unix.gettimeofday () in
let theorems =
if full then
-(* let refl_eq = *)
-(* let u = eq_XURI () in *)
-(* let t = CicUtil.term_of_uri u in *)
-(* let ty, _ = *)
-(* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *)
-(* (t, ty, []) *)
-(* in *)
-(* let le_S = *)
-(* let u = UriManager.uri_of_string *)
-(* "cic:/matita/nat/orders/le.ind#xpointer(1/1/2)" in *)
-(* let t = CicUtil.term_of_uri u in *)
-(* let ty, _ = *)
-(* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *)
-(* (t, ty, []) *)
-(* in *)
-(* let thms = refl_eq::le_S::[] in *)
- let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in
+ let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in
let context_hyp = find_context_hypotheses env eq_indexes in
-(* context_hyp @ thms *)
- (context_hyp, thms)
+ context_hyp @ thms, []
else
let refl_equal =
let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
in
let t = CicUtil.term_of_uri refl_equal in
let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
- [], [(refl_equal, t, ty, [])]
+ [(t, ty, [])], []
in
+ let t2 = Unix.gettimeofday () in
let _ =
debug_print
(lazy
"Theorems:\n-------------------------------------\n%s\n"
(String.concat "\n"
(List.map
- (fun (_, t, ty, _) ->
+ (fun (t, ty, _) ->
Printf.sprintf
"Term: %s, type: %s"
(CicPp.ppterm t) (CicPp.ppterm ty))
- (snd theorems)))))
+ (fst theorems)))));
+ debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
in
let active = make_active () in
- let passive = make_passive [(* term_equality *)] equalities in
+ let passive = make_passive [] equalities in
let start = Unix.gettimeofday () in
-(* let res = given_clause_fullred env [0, [goal]] theorems passive active in *)
let res =
let goals = make_goals goal in
-(* and theorems = make_theorems theorems in *)
- given_clause_fullred dbd env goals theorems passive active
+ given_clause_fullred dbd env goals theorems passive active
in
let finish = Unix.gettimeofday () in
(res, finish -. start)
in
match res with
- | ParamodulationSuccess (Some proof (* goal *), env) ->
+ | ParamodulationSuccess (Some proof, env) ->
debug_print (lazy "OK, found a proof!");
-(* let proof = Inference.build_proof_term goal in *)
let proof = Inference.build_proof_term proof in
let names = names_of_context context in
let newmetasenv =
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
let debug = true;;
let debug_print s = if debug then prerr_endline (Lazy.force s);;
let weight_of_term ?(consider_metas=true) term =
- (* ALB: what to consider as a variable? I think "variables" in our case are
- Metas and maybe Rels... *)
let module C = Cic in
let vars_dict = Hashtbl.create 5 in
let rec aux = function
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; *)
+ let w, m = (weight_of_term ~consider_metas:true t) in
metasw := !metasw + (2 * (List.length m));
-(* metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *)
w
in
(* Warning: the following let cannot be expanded since it forces the
right evaluation order!!!! *)
let w = (weight_of ty) + (weight_of left) + (weight_of right) in
w + !metasw
-(* (4 * IntSet.cardinal !metasw) *)
;;
* normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
* (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
let normalize_weight maxmeta (cw, wl) =
-(* Printf.printf "normalize_weight: %d, %s\n" maxmeta *)
-(* (string_of_weight (cw, wl)); *)
let rec aux = function
| 0 -> []
| m -> (m, 0)::(aux (m-1))
((h1, w1) as weight1) ((h2, w2) as weight2)=
let (h1, w1), (h2, w2) =
if normalize then
-(* let maxmeta = *)
-(* let maxmeta l = *)
-(* try *)
-(* match List.hd l with *)
-(* | (m, _) -> m *)
-(* with Failure _ -> 0 *)
-(* in *)
-(* max (maxmeta w1) (maxmeta w2) *)
-(* in *)
-(* (normalize_weight maxmeta (h1, w1)), (normalize_weight maxmeta (h2, w2)) *)
normalize_weights weight1 weight2
else
(h1, w1), (h2, w2)
else if r = 0 then (lt, eq+1, gt), diffs
else (lt, eq, gt+1), diffs
| (meta1, w1), (meta2, w2) ->
- Printf.printf "HMMM!!!! %s, %s\n"
- (string_of_weight weight1) (string_of_weight weight2);
+ debug_print
+ (lazy
+ (Printf.sprintf "HMMM!!!! %s, %s\n"
+ (string_of_weight weight1) (string_of_weight weight2)));
assert false)
((0, 0, 0), 0) w1 w2
with Invalid_argument _ ->
- Printf.printf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n"
- (string_of_weight (h1, w1)) (string_of_weight weight1)
- (string_of_weight (h2, w2)) (string_of_weight weight2)
- (string_of_bool normalize);
+ debug_print
+ (lazy
+ (Printf.sprintf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n"
+ (string_of_weight (h1, w1)) (string_of_weight weight1)
+ (string_of_weight (h2, w2)) (string_of_weight weight2)
+ (string_of_bool normalize)));
assert false
in
let hdiff = h1 - h2 in
let rec kbo t1 t2 =
-(* debug_print (lazy ( *)
-(* 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 (lazy ( *)
-(* 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 (lazy ( *)
-(* 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 (lazy ("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 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 =
+ kbo hd1 hd2
+ in
+ if o = Eq then cmp tl1 tl2
+ else o
+ in
+ let comparison = compare_weights ~normalize:true w1 w2 in
+ match comparison with
+ | Le ->
+ let r = aux t1 t2 in
+ 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 ->
+ cmp tl1 tl2
+ | _, _ -> Incomparable
+ ) else r
+ | res -> res
;;
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
(* (weight of constants, [(meta, weight_of_meta)]) *)
type weight = int * (int * int) list;;
projects / helm.git / commitdiff