eq
;;
+let mk_tmp_equality (weight,(ty,l,r,o),m) =
+ let id = -1 in
+ uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
+;;
+
+
let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
(weight,proof,(ty,l,r,o),m,id)
let rec aux acc id =
let p,_,_ = proof_of_id id in
match p with
- | Exact _ -> id :: acc
+ | Exact _ -> if (List.mem id acc) then acc else id :: acc
| Step (_,(_,id1, (_,id2), _)) ->
let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
Printf.sprintf "%d = %s: %s = %s" id
(CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
| Step (_,(step,id1, (_,id2), _) ) ->
- Printf.sprintf "%5d: %s %4d %4d %s = %s" id
+ Printf.sprintf "%6d: %s %6d %6d %s = %s" id
(if step = SuperpositionRight then "SupR" else "Demo")
id1 id2 (CicPp.pp l names) (CicPp.pp r names)
with
Not_found -> assert false
let pp_proof names goalproof =
- String.concat "\n" (List.map (string_of_id names) (wfo goalproof))
+ String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^
+ "\ngoal is demodulated with " ^
+ (String.concat " "
+ ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
+;;
let build_goal_proof l initial =
let proof =
(Cic.term * Cic.term * Cic.term * Utils.comparison) *
Cic.metasenv ->
equality
+
+val mk_tmp_equality :
+ int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv ->
+ equality
val open_equality :
equality ->
in
if sign = Utils.Positive then
(bo,
- (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'),
+ (Equality.Step (subst,(Equality.Demodulation,
+ id,(pos,id'),
(*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
Equality.ProofBlock (
subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality newmeta env table sign newtarget
+ demodulation_equality ?from newmeta env table sign newtarget
| None ->
let res = demodulation_aux metasenv' context ugraph table 0 right in
if Utils.debug_res then check_res res "demod result 1";
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality newmeta env table sign newtarget
+ demodulation_equality ?from newmeta env table sign newtarget
| None ->
newmeta, target
in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
(* qua *)
- let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
-(* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
+ let bo' =
+ Utils.guarded_simpl context (apply_subst s (S.subst other bo))
+ in
let name = C.Name "x" in
incr sup_r_counter;
let bo'' =
S.lift 1 eq_ty; l; r]
in
bo',
- ( Equality.Step (s,(Equality.SuperpositionRight,
- id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
- Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
+ (Equality.Step
+ (s,(Equality.SuperpositionRight,
+ id,(pos,id'),(Cic.Lambda(name,ty,bo'')))),
+ Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
in
let newmeta, newequality =
List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
;;
+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 deep l r =
+ let eqtmp =
+ Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
+ match Indexing.subsumption env active_table eqtmp with
+ | None -> false
+ | Some (s,eq') ->
+ prerr_endline
+ ("\n\n " ^ Equality.string_of_equality ~env eq ^
+ "\nis"^(if deep then " CONTEXTUALLY " else " ")^"subsumed by \n " ^
+ Equality.string_of_equality ~env eq' ^ "\n\n");
+ true
+ in
+ let rec aux b = function
+ | Cic.Rel n, Cic.Rel m -> if n = m then true else false
+ | ((Cic.Appl l) as left),((Cic.Appl l') as right) ->
+ check b left right ||
+ (try
+ List.for_all2 (fun t t' -> aux true (t,t')) (List.tl l) (List.tl l')
+ with Invalid_argument _ -> false)
+ | (Cic.Meta _),_
+ | _,(Cic.Meta _) -> false
+ | _ -> false
+ in
+ aux false (left,right)
+;;
+
+(*
+let check_for_deep env active_table eq =
+ match Indexing.subsumption env active_table eq with
+ | None -> false
+ | Some _ -> true
+;;
+*)
+
+let profiler = HExtlib.profile "check_for_deep";;
+
+let check_for_deep_subsumption env active_table eq =
+ profiler.HExtlib.profile (check_for_deep_subsumption env active_table) eq
+;;
+
(* buttare via sign *)
(** simplifies current using active and passive *)
match res with
| None -> None
| Some c ->
- (* immagino non funzioni piu'... *)
if Indexing.in_index active_table c then
None
else
match passive_table with
| None ->
+ if check_for_deep_subsumption env active_table c then
+ None
+ else
+ res
+(*
if Indexing.subsumption env active_table c = None then
res
else
None
+*)
| Some passive_table ->
if Indexing.in_index passive_table c then None
else
- if Indexing.subsumption env active_table c = None then
- if Indexing.subsumption env passive_table c = None then
- res
- else
- None
+ if check_for_deep_subsumption env active_table c then
+ None
+ else
+(* if Indexing.subsumption env active_table c = None then*)
+ (match Indexing.subsumption env passive_table c with
+ | None -> res
+ | Some (_,c') -> None (*Some c'*))
+(*
else
None
+*)
;;
type fs_time_info_t = {
| None -> demodulate active_table goal
| Some passive_table ->
let changed, goal = demodulate active_table goal in
- let changed', goal = demodulate passive_table goal in
- (changed || changed'), goal
+(* let changed', goal = demodulate passive_table goal in*)
+ (changed (*|| changed'*)), goal
in
changed,
if not changed then
| _ -> ((pl, ps), passive_table), Some (newp)
;;
+let build_table equations =
+ List.fold_left
+ (fun (l, t, w) e ->
+ let ew, _, _, _ , _ = Equality.open_equality e in
+ e::l, Indexing.index t e, min ew w)
+ ([], Indexing.empty, 1000000) equations
+;;
+
let backward_simplify env new' ?passive active =
- let new_pos, new_table, min_weight =
+ let new_pos, new_table, min_weight = build_table new' in
+(*
List.fold_left
(fun (l, t, w) e ->
let ew, _, _, _ , _ = Equality.open_equality e in
e::l, Indexing.index t e, min ew w)
([], Indexing.empty, 1000000) new'
in
+*)
let active, newa =
backward_simplify_active env new_pos new_table min_weight active in
match passive with
simplify (new' @ p @ rp) active passive
in
let active, _, new' = simplify new' active passive in
+ let goals =
+ let a,b,_ = build_table new' in
+ simplify_goals env goals ~passive (a,b)
+ in
+
(* pessima prova
let new1 = prova env new' active in
let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in
projects / helm.git / commitdiff