remove_refl p1
| _ -> Cic.Appl (List.map remove_refl args))
| Cic.Appl l -> Cic.Appl (List.map remove_refl l)
+ | Cic.LetIn (name,bo,rest) ->
+ Cic.LetIn (name,remove_refl bo,remove_refl rest)
| _ -> t
in
let rec canonical t =
match t with
+ | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
| Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
when LibraryObjects.is_sym_eq_URI uri_sym ->
(match p_of_sym ens tl with
* ctx is a term with an open (Rel 1). (Rel 1) is the empty context
*)
let rec aux uri ty left right ctx_d = function
+ | Cic.LetIn (name,body,rest) ->
+ (* we should go in body *)
+ Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
| Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
when LibraryObjects.is_eq_ind_URI uri_ind ||
LibraryObjects.is_eq_ind_r_URI uri_ind ->
contextualize eq ty l r t
;;
-let build_proof_step subst p1 p2 pos l r pred =
- let p1 = Subst.apply_subst subst p1 in
- let p2 = Subst.apply_subst subst p2 in
- let l = Subst.apply_subst subst l in
- let r = Subst.apply_subst subst r in
- let pred = Subst.apply_subst subst pred in
+let build_proof_step lift subst p1 p2 pos l r pred =
+ let p1 = Subst.apply_subst_lift lift subst p1 in
+ let p2 = Subst.apply_subst_lift lift subst p2 in
+ let l = CicSubstitution.lift lift l in
+ let l = Subst.apply_subst_lift lift subst l in
+ let r = CicSubstitution.lift lift r in
+ let r = Subst.apply_subst_lift lift subst r in
+ let pred = CicSubstitution.lift lift pred in
+ let pred = Subst.apply_subst_lift lift subst pred in
let ty,body =
match pred with
| Cic.Lambda (_,ty,body) -> ty,body
mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
;;
-let build_proof_term proof =
- let rec aux = function
- | Exact term -> term
- | Step (subst,(_, id1, (pos,id2), pred)) ->
- let p,_,_ = proof_of_id id1 in
- let p1 = aux p in
- let p,l,r = proof_of_id id2 in
- let p2 = aux p in
- build_proof_step subst p1 p2 pos l r pred
+let parametrize_proof p ty =
+ let parameters = CicUtil.metas_of_term p in (* ?if they are under a lambda? *)
+ let parameters =
+ HExtlib.list_uniq (List.sort Pervasives.compare parameters)
in
- aux proof
+ let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in
+ let with_what, lift_no =
+ List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1)
+ in
+ let p = CicSubstitution.lift (lift_no-1) p in
+ let p =
+ ProofEngineReduction.replace_lifting
+ ~equality:(=) ~what ~with_what ~where:p
+ in
+ let ty_of_m _ = ty (*function
+ | Cic.Meta (i,_) -> List.assoc i menv
+ | _ -> assert false *)
+ in
+ let args, proof,_ =
+ List.fold_left
+ (fun (instance,p,n) m ->
+ (instance@[m],
+ Cic.Lambda
+ (Cic.Name ("x"^string_of_int n),
+ CicSubstitution.lift (lift_no - n - 1) (ty_of_m m),
+ p),
+ n+1))
+ ([Cic.Rel 1],p,1)
+ what
+ in
+ let instance = match args with | [x] -> x | _ -> Cic.Appl args in
+ proof, instance
;;
let wfo goalproof proof =
((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
;;
+(* returns the list of ids that should be factorized *)
+let get_duplicate_step_in_wfo l p =
+ let ol = List.rev l in
+ let h = Hashtbl.create 13 in
+ let add i n =
+ let p,_,_ = proof_of_id i in
+ match p with
+ | Exact _ -> ()
+ | _ ->
+ try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1)
+ with Not_found -> Hashtbl.add h i (n,1)
+ in
+ let rec aux n = function
+ | Exact _ -> n
+ | Step (_,(_,i1,(_,i2),_)) ->
+ add i1 n;add i2 n;
+ max (aux (n+1) (let p,_,_ = proof_of_id i1 in p))
+ (aux (n+1) (let p,_,_ = proof_of_id i2 in p))
+ in
+ let i = aux 0 p in
+ let _ =
+ List.fold_left
+ (fun acc (_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p))
+ i ol
+ in
+ (* now h is complete *)
+ let proofs = Hashtbl.fold (fun k (pos,count) acc->(k,pos,count)::acc) h [] in
+ let proofs = List.filter (fun (_,_,c) -> c > 1) proofs in
+ let proofs =
+ List.sort (fun (_,c1,_) (_,c2,_) -> Pervasives.compare c2 c1) proofs
+ in
+ List.map (fun (i,_,_) -> i) proofs
+;;
+
+let build_proof_term h lift proof =
+ let proof_of_id aux id =
+ let p,l,r = proof_of_id id in
+ try List.assoc id h,l,r with Not_found -> aux p, l, r
+ in
+ let rec aux = function
+ | Exact term -> CicSubstitution.lift lift term
+ | Step (subst,(_, id1, (pos,id2), pred)) ->
+ if Subst.is_in_subst 9 subst then
+ prerr_endline (Printf.sprintf "ID %d-%d has: %s\n" id1 id2 (Subst.ppsubst
+ subst));
+ let p1,_,_ = proof_of_id aux id1 in
+ let p2,l,r = proof_of_id aux id2 in
+ build_proof_step lift subst p1 p2 pos l r pred
+ in
+ aux proof
+;;
+
let build_goal_proof l initial ty se =
let se = List.map (fun i -> Cic.Meta (i,[])) se in
+ let lets = get_duplicate_step_in_wfo l initial in
+ let letsno = List.length lets in
+ let _,mty,_,_ = open_eq ty in
+ let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l
+ in
+ let lets,_,h =
+ List.fold_left
+ (fun (acc,n,h) id ->
+ let p,_,_ = proof_of_id id in
+ let cic = build_proof_term h n p in
+ let real_cic,instance =
+ parametrize_proof cic (CicSubstitution.lift n mty)
+ in
+ let h = (id, instance)::lift_list h in
+ acc@[id,real_cic],n+1,h)
+ ([],0,[]) lets
+ in
let proof,se =
let rec aux se current_proof = function
| [] -> current_proof,se
| (pos,id,subst,pred)::tl ->
let p,l,r = proof_of_id id in
- let p = build_proof_term p in
+ let p = build_proof_term h letsno p in
let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
- let proof = build_proof_step subst current_proof p pos l r pred in
+ let proof =
+ build_proof_step letsno subst current_proof p pos l r pred
+ in
let proof,se = aux se proof tl in
- Subst.apply_subst subst proof,
- List.map (fun x -> Subst.apply_subst subst x) se
+ Subst.apply_subst_lift letsno subst proof,
+ List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
in
- aux se initial l
+ aux se (build_proof_term h letsno initial) l
+ in
+ let n,proof =
+ let initial = proof in
+ List.fold_right
+ (fun (id,cic) (n,p) ->
+ n-1,
+ Cic.LetIn (
+ Cic.Name ("H"^string_of_int id),
+ cic, p))
+ lets (letsno-1,initial)
in
- canonical (contextualize_rewrites proof ty), se
+ canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se
;;
let refl_proof ty term =
;;
let metas_of_proof p =
- let p = build_proof_term p in
+ let p = build_proof_term [] 0 p in
Utils.metas_of_term p
;;
let fix_metas newmeta eq =
let w, p, (ty, left, right, o), menv,_ = open_equality eq in
- (* debug
- let _ , eq =
- fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
- prerr_endline (string_of_equality eq); *)
let subst, metasenv, newmeta = relocate newmeta menv in
let ty = Subst.apply_subst subst ty in
let left = Subst.apply_subst subst left in
in
let p = fix_proof p in
let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in
- (* debug prerr_endline (string_of_equality eq); *)
newmeta+1, eq
exception NotMetaConvertible;;
* http://cs.unibo.it/helm/.
*)
+let _profiler = <:profiler<_profiler>>;;
+
(* $Id$ *)
type goal = Equality.goal_proof * Cic.metasenv * Cic.term
module Index = Equality_indexing.DT (* path tree based indexing *)
*)
-let beta_expand_time = ref 0.;;
-
let debug_print = Utils.debug_print;;
(*
;;
-let indexing_retrieval_time = ref 0.;;
-
-
let apply_subst = Subst.apply_subst
let index = Index.index
*)
let get_candidates ?env mode tree term =
- let t1 = Unix.gettimeofday () in
- let res =
- let s =
- match mode with
- | Matching -> Index.retrieve_generalizations tree term
- | Unification -> Index.retrieve_unifiables tree term
- in
- Index.PosEqSet.elements s
+ let s =
+ match mode with
+ | Matching -> Index.retrieve_generalizations tree term
+ | Unification -> Index.retrieve_unifiables tree term
in
-(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
-(* print_newline (); *)
- let t2 = Unix.gettimeofday () in
- indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
- (* make fresh instances *)
- res
+ Index.PosEqSet.elements s
;;
-let profiler = HExtlib.profile "P/Indexing.get_candidates"
-
-let get_candidates ?env mode tree term =
- profiler.HExtlib.profile (get_candidates ?env 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
let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
+(*
let p="proof = "^
(CicPp.ppterm(Equality.build_proof_term proof))^"\n"
in
+*)
check_for_duplicates metas "gia nella metas";
- check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
+ check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
) else
let do_match c eq_URI =
let subst', metasenv', ugraph' =
- let t1 = Unix.gettimeofday () in
- try
- let r =
- ( Inference.matching 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 as e ->
- let t2 = Unix.gettimeofday () in
- match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
- | CicUtil.Meta_not_found _ as exn -> raise exn
+ Inference.matching
+ metasenv metas context term (S.lift lift_amount c) ugraph
in
Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
(candidate, eq_URI))
find_matches metasenv context ugraph lift_amount term termty tl
;;
+let find_matches metasenv context ugraph lift_amount term termty =
+ find_matches metasenv context ugraph lift_amount term termty
+;;
+
(*
as above, but finds all the matching equalities, and the matching condition
can be either Inference.matching or Inference.unification
let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
let do_match c eq_URI =
let subst', metasenv', ugraph' =
- let t1 = Unix.gettimeofday () in
- try
- let term =
- match c,term with
- | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r]
- when LibraryObjects.is_eq_URI u -> l
-(*
- if Utils.compare_weights (Utils.weight_of_term l)
- (Utils.weight_of_term r) = Utils.Gt
- then l else r
-*)
- | _ -> term
- in
-
- 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
+ unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
in
- (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
- (candidate, eq_URI))
+ (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 ()
let find_all_matches
?unif_fun metasenv context ugraph lift_amount term termty l
=
- let rc =
find_all_matches
?unif_fun metasenv context ugraph lift_amount term termty l
- in
(*prerr_endline "CANDIDATES:";
List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
(List.length rc));*)
- rc
-
+;;
(*
returns true if target is subsumed by some equality in table
*)
+let print_res l =
+ prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+ ((pos,equation),_)) -> Equality.string_of_equality equation)l))
+;;
+
let subsumption_aux use_unification env table target =
-(* let print_res l =*)
-(* prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*)
-(* ((pos,equation),_)) -> Equality.string_of_equality equation)l))*)
-(* in*)
let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
let metasenv, context, ugraph = env in
let metasenv = tmetas in
find_all_matches ~unif_fun
metasenv context ugraph 0 left ty leftc
in
-(* print_res leftr;*)
let rec ok what = function
| [] -> None
| (_, subst, menv, ug, ((pos,equation),_))::tl ->
find_all_matches ~unif_fun
metasenv context ugraph 0 right ty rightc
in
-(* print_res rightr;*)
ok left rightr
-(* (if r then *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
-(* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
;;
-let subsumption = subsumption_aux false;;
-let unification = subsumption_aux true;;
+let subsumption x y z =
+ subsumption_aux false x y z
+;;
+
+let unification x y z =
+ subsumption_aux true x y z
+;;
let rec demodulation_aux ?from ?(typecheck=false)
metasenv context ugraph table lift_amount term =
res
;;
-
-let build_newtarget_time = ref 0.;;
-
-
-let demod_counter = ref 1;;
-
exception Foo
-let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
-
(** demodulation, when target is an equality *)
let rec demodulation_equality ?from newmeta env table sign target =
let module C = Cic in
let maxmeta = ref newmeta in
let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
- let time1 = Unix.gettimeofday () in
if Utils.debug_metas then
begin
Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
(* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
let name = C.Name "x" in
- incr demod_counter;
let bo' =
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
*)
in
let newmenv = (* Inference.filter subst *) menv in
+(*
let _ =
if Utils.debug_metas then
try ignore(CicTypeChecker.type_of_aux'
raise exc;
else ()
in
+*)
let left, right = if is_left then newterm, right else left, newterm in
let ordering = !Utils.compare_terms left right in
let stat = (eq_ty, left, right, ordering) in
- let time2 = Unix.gettimeofday () in
- build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
let res =
let w = Utils.compute_equality_weight stat in
- Equality.mk_equality (w, newproof, stat,newmenv)
+ (Equality.mk_equality (w, newproof, stat,newmenv))
in
if Utils.debug_metas then
ignore(check_target context res "buildnew_target output");
!maxmeta, res
in
- let build_newtarget is_left x =
- profiler.HExtlib.profile (build_newtarget is_left) x
- in
let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
if Utils.debug_res then check_res res "demod result";
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 rec betaexpand_term
+ ?(subterms_only=false) metasenv context ugraph table lift_amount term
+=
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- let candidates = get_candidates Unification table term in
let res, lifted_term =
match term with
C.Implicit None, ugraph
(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
in
+ let candidates = get_candidates Unification table term in
let r =
- find_all_matches
- metasenv context ugraph lift_amount term termty candidates
+ if subterms_only then
+ []
+ else
+ find_all_matches
+ metasenv context ugraph lift_amount term termty candidates
in
r @ res, lifted_term
;;
-let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
-
-let betaexpand_term metasenv context ugraph table lift_amount term =
- profiler.HExtlib.profile
- (betaexpand_term metasenv context ugraph table lift_amount) term
-
-
-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 fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) =
- let unchanged = CicSubstitution.lift 1 unchanged in
- let ty = CicSubstitution.lift 1 ty in
- let pred =
- match posu with
- | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
- | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
- in
- (pred, subst, menv, ug, eq_f)
-;;
-
-let build_newgoal context goalproof goal_info expansion =
- let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info expansion in
- let pos, equality = eq_found in
- let (_, proof', (ty, what, other, _), menv',id) =
- Equality.open_equality equality in
- let what, other = if pos = Utils.Left then what, other else other, what in
- let newterm, newgoalproof =
- let bo =
- Utils.guarded_simpl context
- (apply_subst subst (CicSubstitution.subst other t))
- in
- let bo' = (*apply_subst subst*) t in
- let name = Cic.Name "x" in
- let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
- bo, (newgoalproofstep::goalproof)
- in
- let newmetasenv = (* Inference.filter subst *) menv in
- (newgoalproof, newmetasenv, newterm)
-;;
-
-let superposition_left
- (metasenv, context, ugraph) table (proof,menv,ty)
-=
- 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 module U = Utils in
- let big,small,pos,eq,ty =
- match ty with
- | Cic.Appl [eq;ty;l;r] ->
- let c =
- Utils.compare_weights ~normalize:true
- (Utils.weight_of_term l) (Utils.weight_of_term r)
- in
- (match c with
- | Utils.Gt -> l,r,Utils.Right,eq,ty
- | _ -> r,l,Utils.Left,eq,ty)
- | _ ->
- let names = Utils.names_of_context context in
- prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names);
- assert false
- in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map (build_newgoal context proof (eq,ty,small,pos)) expansions
-;;
-
-let sup_r_counter = ref 1;;
-
(**
superposition_right
returns a list of new clauses inferred with a right superposition step
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 superposition_right
+ ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
+=
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let metasenv' = newmetas in
let maxmeta = ref newmeta in
let res1, res2 =
- let betaexpand_term metasenv context ugraph table d term =
- let t1 = Unix.gettimeofday () in
- let res = betaexpand_term metasenv context ugraph table d term in
- let t2 = Unix.gettimeofday () in
- beta_expand_time := !beta_expand_time +. (t2 -. t1);
- res
- in
match ordering with
| U.Gt ->
- fst (betaexpand_term metasenv' context ugraph table 0 left), []
+ fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
| U.Lt ->
- [], fst (betaexpand_term metasenv' context ugraph table 0 right)
+ [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
| _ ->
let res l r =
List.filter
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))
+ (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
in
(res left right), (res right left)
in
let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
if Utils.debug_metas then
ignore (check_target context (snd eq_found) "buildnew1" );
- let time1 = Unix.gettimeofday () in
let pos, equality = eq_found in
let (_, proof', (ty, what, other, _), menv',id') =
Utils.guarded_simpl context (apply_subst s (S.subst other bo))
in
let name = C.Name "x" in
- incr sup_r_counter;
let bo'' =
let l, r =
if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
newm, eq'
in
maxmeta := newmeta;
- let time2 = Unix.gettimeofday () in
- build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
if Utils.debug_metas then
ignore(check_target context newequality "buildnew2");
newequality
(List.filter ok (new1 @ new2)))
;;
-(** demodulation, when the target is a goal *)
-let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) =
- Equality.meta_convertibility g1 g2
-;;
-
-let rec demodulation_goal env table goal =
- let metasenv, context, ugraph = env in
- let goalproof, metas, term = goal in
- let term = Utils.guarded_simpl (~debug:true) context term in
- let goal = goalproof, metas, term in
- let metasenv' = metas in
-
- let left,right,eq,ty =
- match term with
- | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty
- | _ -> assert false
- in
- let do_right () =
- let resright = demodulation_aux metasenv' context ugraph table 0 right in
- match resright with
- | Some t ->
- let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in
- if goal_metaconvertibility_eq goal newg then
- false, goal
- else
- true, snd (demodulation_goal env table newg)
- | None -> false, goal
- in
- let resleft =
- demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left
- in
- match resleft with
- | Some t ->
- let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in
- if goal_metaconvertibility_eq goal newg then
- do_right ()
- else
- true, snd (demodulation_goal env table newg)
- | None -> do_right ()
-;;
-
(** demodulation, when the target is a theorem *)
let rec demodulation_theorem newmeta env table theorem =
let module C = Cic in
let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
(* let bo' = apply_subst subst t in *)
(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
- incr demod_counter;
(*
let newproofold =
Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
newmeta, theorem
;;
+(*****************************************************************************)
+(** OPERATIONS ON GOALS **)
+(** **)
+(** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
+(*****************************************************************************)
+
+let open_goal g =
+ match g with
+ | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
+ assert (LibraryObjects.is_eq_URI uri);
+ proof,menv,eq,ty,l,r
+ | _ -> assert false
+;;
+
+let ty_of_goal (_,_,ty) = ty ;;
+
+(* checks if two goals are metaconvertible *)
+let goal_metaconvertibility_eq g1 g2 =
+ Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
+;;
+
+(* when the betaexpand_term function is called on the left/right side of the
+ * goal, the predicate has to be fixed
+ * C[x] ---> (eq ty unchanged C[x])
+ * [posu] is the side of the [unchanged] term in the original goal
+ *)
+let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
+ let _,_,eq,ty,l,r = open_goal goal in
+ let unchanged = if posu = Utils.Left then l else r in
+ let unchanged = CicSubstitution.lift 1 unchanged in
+ let ty = CicSubstitution.lift 1 ty in
+ let pred =
+ match posu with
+ | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
+ | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
+ in
+ (pred, subst, menv, ug, eq_f)
+;;
+
+(* ginve the old [goal], the side that has not changed [posu] and the
+ * expansion builds a new goal *)
+let build_newgoal context goal posu expansion =
+ let goalproof,_,_,_,_,_ = open_goal goal in
+ let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newgoalproof =
+ let bo =
+ Utils.guarded_simpl context
+ (apply_subst subst (CicSubstitution.subst other t))
+ in
+ let bo' = (*apply_subst subst*) t in
+ let name = Cic.Name "x" in
+ let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
+ in
+ let newmetasenv = (* Inference.filter subst *) menv in
+ (newgoalproof, newmetasenv, newterm)
+;;
+
+(**
+ 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 (metasenv, context, ugraph) table goal =
+ let proof,menv,eq,ty,l,r = open_goal goal in
+ let c =
+ Utils.compare_weights ~normalize:true
+ (Utils.weight_of_term l) (Utils.weight_of_term r)
+ in
+ let big,small,possmall =
+ match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+ in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map (build_newgoal context goal possmall) expansions
+;;
+
+(** demodulation, when the target is a goal *)
+let rec demodulation_goal env table goal =
+ let goalproof,menv,_,_,left,right = open_goal goal in
+ let metasenv, context, ugraph = env in
+(* let term = Utils.guarded_simpl (~debug:true) context term in*)
+ let do_right () =
+ let resright = demodulation_aux menv context ugraph table 0 right in
+ match resright with
+ | Some t ->
+ let newg = build_newgoal context goal Utils.Left t in
+ if goal_metaconvertibility_eq goal newg then
+ false, goal
+ else
+ true, snd (demodulation_goal env table newg)
+ | None -> false, goal
+ in
+ let resleft = demodulation_aux menv context ugraph table 0 left in
+ match resleft with
+ | Some t ->
+ let newg = build_newgoal context goal Utils.Right t in
+ if goal_metaconvertibility_eq goal newg then
+ do_right ()
+ else
+ true, snd (demodulation_goal env table newg)
+ | None -> do_right ()
+;;
+
+let get_stats () = <:show<Indexing.>> ;;
* http://cs.unibo.it/helm/.
*)
-(* $Id$ *)
+let _profiler = <:profiler<_profiler>>;;
-(* <:profiler<"saturation">> *)
+(* $Id$ *)
open Inference;;
open Utils;;
let compare eq1 eq2 =
match Equality.meta_convertibility_eq eq1 eq2 with
| true -> 0
- | false ->
+ | false ->
let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in
let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality eq2 in
match Pervasives.compare w1 w2 with
(ignore(Indexing.check_target c current "infer1");
ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list));
let new_pos =
- let maxm, res =
- Indexing.superposition_right !maxmeta env active_table current in
+ let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
+ maxmeta := maxm;
+ let active_table = Indexing.index active_table copy_of_current in
+ let _ = <:start<current contro active>> in
+ let maxm, res =
+ Indexing.superposition_right !maxmeta env active_table current
+ in
+ let _ = <:stop<current contro active>> in
if Utils.debug_metas then
ignore(List.map
(function current ->
| [] -> []
| equality::tl ->
let maxm, res =
- Indexing.superposition_right !maxmeta env table equality in
+ Indexing.superposition_right ~subterms_only:true !maxmeta env table equality
+ in
maxmeta := maxm;
if Utils.debug_metas then
ignore
let pos = infer_positive table tl in
res @ pos
in
+(*
let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
maxmeta := maxm;
+*)
let curr_table = Indexing.index Indexing.empty current in
- let pos = infer_positive curr_table (copy_of_current::active_list)
- in
+ let _ = <:start<active contro current>> in
+ let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in
+ let _ = <:stop<active contro current>> in
if Utils.debug_metas then
ignore(List.map
(function current ->
Indexing.check_target c current "sup3") pos);
- res @ pos
+ res @ pos
in
derived_clauses := !derived_clauses + (List.length new_pos);
match !maximal_retained_equality with
let check_for_deep_subsumption env active_table eq =
let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in
- if id = 14242 then assert false;
-
let check_subsumed deep l r =
let eqtmp =
Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
(fun current -> Indexing.check_target c current "forward new pos")
new_pos;)
end;
- let t1 = Unix.gettimeofday () in
-
let active_list, active_table = active in
let passive_table =
match passive with
| None -> None
| Some ((_, _), pt) -> Some pt
in
- let t2 = Unix.gettimeofday () in
- fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
-
let demodulate sign table target =
let newmeta, newtarget =
Indexing.demodulation_equality !maxmeta env table sign target in
maxmeta := newmeta;
newtarget
in
- let t1 = Unix.gettimeofday () in
(* we could also demodulate using passive. Currently we don't *)
let new_pos =
List.map (demodulate Positive active_table) new_pos
in
- let t2 = Unix.gettimeofday () in
- fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
-
let new_pos_set =
List.fold_left
(fun s e ->
if not (Equality.is_identity env e) then
- if EqualitySet.mem e s then s
- else EqualitySet.add e s
+(* if EqualitySet.mem e s then s *)
+ (*else*) EqualitySet.add e s
else s)
EqualitySet.empty new_pos
in
not ((Indexing.in_index active_table e) ||
(Indexing.in_index passive_table e)))
in
- List.filter subs (List.filter is_duplicate new_pos)
+ List.filter subs (List.filter is_duplicate new_pos)
;;
let selected = hd in
let passive_goals = tl in
let new' = Indexing.superposition_left env (snd active) selected in
- let metasenv, context, ugraph = env in
- let names = names_of_context context in
selected::active_goals, passive_goals @ new'
| _::tl -> aux tl
in
else if Unix.gettimeofday () > max_time then
(ParamodulationFailure "No more time to spend")
else
+ let _ = prerr_endline "simpl goal with active" in
let goals = simplify_goal_set env goals passive active in
match check_if_goals_set_is_solved env active goals with
| Some p ->
- Printf.eprintf "Found a proof in: %f\n"
- (Unix.gettimeofday() -. initial_time);
+ prerr_endline
+ (Printf.sprintf "Found a proof in: %f\n"
+ (Unix.gettimeofday() -. initial_time));
+(* assert false;*)
ParamodulationSuccess p
| None ->
prerr_endline
kept_clauses := (size_of_passive passive) + (size_of_active active);
(* SELECTION *)
if passive_is_empty passive then
- ParamodulationFailure "No more passive" (* maybe this is a success! *)
+ ParamodulationFailure "No more passive"(*maybe this is a success! *)
else
begin
let goals = infer_goal_set env active goals in
let current, passive = select env goals passive in
- Printf.eprintf "Selected = %s\n"
- (Equality.string_of_equality ~env current);
+ prerr_endline (Printf.sprintf "Selected = %s\n"
+ (Equality.string_of_equality ~env current));
(* SIMPLIFICATION OF CURRENT *)
let res =
forward_simplify env (Positive, current) ~passive active
| None -> step goals theorems passive active (iterno+1)
| Some current ->
(* GENERATION OF NEW EQUATIONS *)
+ prerr_endline "infer";
let new' = infer env current active in
+ prerr_endline "infer goal";
let goals = infer_goal_set_with_current env current goals in
let active =
- if Equality.is_identity env current then
- assert false
- (* nonsense code, check to se if it can be removed *)
- else
let al, tbl = active in
al @ [current], Indexing.index tbl current
in
(* FORWARD AND BACKWARD SIMPLIFICATION *)
+ prerr_endline "fwd/back simpl";
let rec simplify new' active passive =
let new' = forward_simplify_new env new' ~passive active in
let active, passive, newa, retained, pruned =
backward_simplify env new' ~passive active
in
- let passive = List.fold_left filter_dependent passive pruned in
+ let passive =
+ List.fold_left filter_dependent passive pruned
+ in
match newa, retained with
| None, None -> active, passive, new'
| Some p, None
| Some p, Some rp -> simplify (new' @ p @ rp) active passive
in
let active, passive, new' = simplify new' active passive in
+ prerr_endline "simpl goal with new";
let goals =
let a,b,_ = build_table new' in
simplify_goal_set env goals passive (a,b)
*)
let goals = make_goal_set goal in
let max_iterations = 1000 in
- let max_time = Unix.gettimeofday () +. 600. (* minutes *) in
+ let max_time = Unix.gettimeofday () +. 120. (* minutes *) in
given_clause env goals theorems passive active max_iterations max_time
in
let finish = Unix.gettimeofday () in
~newmetasenv:metasenv ~oldmetasenv:proof_menv)
in
let goal_proof, side_effects_t =
- let initial = Equality.build_proof_term newproof in
+ let initial = newproof in
Equality.build_goal_proof goalproof initial type_of_goal side_effects
in
let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
in
if changed then
begin
- let opengoal = Cic.Meta(maxm,irl) in
+ let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
let proofterm,_ =
Equality.build_goal_proof newproof opengoal ty [] in
let extended_metasenv = (maxm,context,newty)::metasenv in
let demodulate_tac ~dbd ~pattern =
ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
;;
+
+let get_stats () =
+ <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats ();;
+
projects / helm.git / commitdiff