X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=7ff0dfd2cc6560dd0b7cfefbb8d088122875283c;hb=433d9c9612c1557e03a549e004c796c1137d4b4a;hp=0c98946802bb3cf19dd95c5b8ba0f510af664dd4;hpb=7cb22a7f8107a6cde0b77b7879e04f586a347102;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 0c9894680..7ff0dfd2c 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -145,7 +145,7 @@ let not_unit_eq ctx eq = List.exists (fun (_,_,ty) -> try - let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph + let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph in s = Cic.Sort(Cic.Prop) with _ -> prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas @@ -313,7 +313,8 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = Founif.matching metasenv metas context term (S.lift lift_amount c) ugraph in - check_metasenv "founif :" metasenv'; + if Utils.debug_metas then + check_metasenv "founif :" metasenv'; Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) in let c, other = @@ -360,7 +361,7 @@ let find_matches metasenv context ugraph lift_amount term termty = can be either Founif.matching or Inference.unification *) (* XXX termty unused *) -let rec find_all_matches ?(unif_fun=Founif.unification) +let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false) metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in @@ -368,7 +369,16 @@ let rec find_all_matches ?(unif_fun=Founif.unification) let module M = CicMetaSubst in let module HL = HelmLibraryObjects in (* prerr_endline ("matching " ^ CicPp.ppterm term); *) - let cmp = !Utils.compare_terms in + let cmp x y = + let r = !Utils.compare_terms x y in +(* + prerr_endline ( + CicPp.ppterm x ^ " " ^ + Utils.string_of_comparison r ^ " " ^ + CicPp.ppterm y ); +*) + r + in let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> [] @@ -409,12 +419,14 @@ let rec find_all_matches ?(unif_fun=Founif.unification) let c' = apply_subst s c and other' = apply_subst s other in let order = cmp c' other' in - if order <> U.Lt && order <> U.Le then + if (demod && order = U.Gt) || + (not demod && (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 + lift_amount term termty tl with | Founif.MatchingFailure | CicUnification.UnificationFailure _ @@ -424,10 +436,10 @@ let rec find_all_matches ?(unif_fun=Founif.unification) ;; let find_all_matches - ?unif_fun metasenv context ugraph lift_amount term termty l + ?unif_fun ?demod metasenv context ugraph lift_amount term termty l = find_all_matches - ?unif_fun metasenv context ugraph lift_amount term termty l + ?unif_fun ?demod metasenv context ugraph lift_amount term termty l (*prerr_endline "CANDIDATES:"; List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l; prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int @@ -506,7 +518,8 @@ let subsumption_aux_all use_unification env table target = let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in let _, context, ugraph = env in let metasenv = tmetas in - check_for_duplicates metasenv "subsumption_aux_all"; + if Utils.debug_metas then + check_for_duplicates metasenv "subsumption_aux_all"; let predicate, unif_fun = if use_unification then Unification, Founif.unification @@ -556,7 +569,7 @@ let subsumption_all x y z = ;; let unification_all x y z = - prerr_endline "unification_all"; subsumption_aux_all true x y z + subsumption_aux_all true x y z ;; let rec demodulation_aux bag ?from ?(typecheck=false) @@ -565,12 +578,13 @@ let rec demodulation_aux bag ?from ?(typecheck=false) let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - check_for_duplicates metasenv "in input a demodulation aux"; + if Utils.debug_metas then + check_for_duplicates metasenv "in input a demodulation aux"; let candidates = get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term - in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates - in + in +(* let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *) let res = match term with | C.Meta _ -> None @@ -709,10 +723,11 @@ let rec demodulation_equality bag ?from eq_uri env table target = let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id') = Equality.open_equality equality in + (* let ty = - try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) - with CicUtil.Meta_not_found _ -> ty - in + try fst (CicTypeChecker.type_of_aux' menv' context what ugraph) + with CicUtil.Meta_not_found _ -> ty + in *) let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = @@ -888,8 +903,8 @@ let rec betaexpand_term | C.Meta (i, l) -> res, lifted_term | term -> let termty, ugraph = -(* C.Implicit None, ugraph *) - CicTypeChecker.type_of_aux' metasenv context term ugraph + C.Implicit None, ugraph +(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) in let candidates = get_candidates Unification table term in (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *) @@ -1080,9 +1095,9 @@ let build_newg bag context goal rule expansion = ;; let rec demod bag env table goal = - let goalproof,menv,t = goal in + let _,menv,t = goal in let _, context, ugraph = env in - let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in + let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in match res with | Some newt -> let newg = @@ -1232,12 +1247,10 @@ let rec demodulation_goal bag env table goal = | None -> do_right () ;; -type next = L | R -type solved = Yes of Equality.goal | No of Equality.goal list - (* returns all the 1 step demodulations *) module C = Cic;; module S = CicSubstitution;; + let rec demodulation_all_aux metasenv context ugraph table lift_amount term = @@ -1250,100 +1263,178 @@ let rec demodulation_all_aux let termty, ugraph = C.Implicit None, ugraph in let res = find_all_matches - metasenv context ugraph lift_amount term termty candidates + ~unif_fun:Founif.matching ~demod:true + metasenv context ugraph lift_amount term termty candidates in match term with | C.Appl l -> - let res, _, _ = + let res, _, _, _ = List.fold_left - (fun (res,l,r) t -> - res @ - List.map - (fun (rel, s, m, ug, c) -> - (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c)) - (demodulation_all_aux - metasenv context ugraph table lift_amount t), - l@[List.hd r], List.tl r) - (res, [], List.map (S.lift 1) l) l + (fun (res,b,l,r) t -> + if not b then res,b,l,r + else + let demods_for_t = + demodulation_all_aux + metasenv context ugraph table lift_amount t + in + let b = demods_for_t = [] in + res @ + List.map + (fun (rel, s, m, ug, c) -> + (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c)) + demods_for_t, b, l@[List.hd r], List.tl r) + (res, true, [], List.map (S.lift 1) l) l in res - | C.Prod (nn, s, t) - | C.Lambda (nn, s, t) -> - let context = (Some (nn, C.Decl s))::context in - let mk s t = - match term with - | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t) - in - res @ - List.map - (fun (rel, subst, m, ug, c) -> - mk (S.lift 1 s) rel, subst, m, ug, c) - (demodulation_all_aux - metasenv context ugraph table (lift_amount+1) t) - (* we could demodulate also in s, but then t may be badly - * typed... *) | t -> res ;; -let solve_demodulating bag env table initgoal steps = +let demod_all steps bag env table goal = let _, context, ugraph = env in - let solved goal res side = - let newg = build_newgoal bag context goal side Equality.Demodulation res in - match newg with - | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right]) - when LibraryObjects.is_eq_URI uri -> - (try - let _ = - Founif.unification m m context left right CicUniv.empty_ugraph - in - Yes newg - with CicUnification.UnificationFailure _ -> No [newg]) - | _ -> No [newg] + let is_visited l (_,_,t) = + List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l in - let solved goal res_list side = - let newg = List.map (fun x -> solved goal x side) res_list in - try - List.find (function Yes _ -> true | _ -> false) newg - with Not_found -> - No (List.flatten (List.map (function No s -> s | _-> assert false) newg)) + let rec aux steps visited nf bag = function + | _ when steps = 0 -> visited, bag, nf + | [] -> visited, bag, nf + | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest + | goal :: rest -> + let visited = goal :: visited in + let _,menv,t = goal in + let res = demodulation_all_aux menv context ugraph table 0 t in + let steps = if res = [] then steps-1 else steps in + let new_goals = + List.map (build_newg bag context goal Equality.Demodulation) res + in + let nf = if new_goals = [] then goal :: nf else nf in + aux steps visited nf bag (new_goals @ rest) in - let rec first f l = - match l with - | [] -> None - | x::tl -> - match f x with - | None -> first f tl - | Some x as ok -> ok + aux steps [] [] bag [goal] +;; + +let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) = + let proof,m,eq,ty,left,right = open_goal goal in + let pl = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pl + in + let pr = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pr in - let rec aux steps next goal = - if steps = 0 then None else - let goalproof,menv,_,_,left,right = open_goal goal in - let do_step t = - demodulation_all_aux menv context ugraph table 0 t + (pr@pl@proof, m, Cic.Appl [eq;ty;l;r]) +;; + +let demodulation_all_goal bag env table goal maxnf = + let proof,menv,eq,ty,left,right = open_goal goal in + let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in + let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in + let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in + let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in + List.fold_left + (fun acc (_,_,l as ld) -> + List.fold_left + (fun acc (_,_,r as rd) -> + combine_demodulation_proofs bag env goal ld rd :: acc) + acc r_demod) + [] l_demod +;; + +let solve_demodulating bag env table initgoal steps = + let proof,menv,eq,ty,left,right = open_goal initgoal in + let uri = + match eq with + | Cic.MutInd (u,_,_) -> u + | _ -> assert false + in + let _, context, ugraph = env in + let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in + let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in + let is_solved left right ml mr = + let m = ml @ (List.filter + (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr) in - match next with - | L -> - (match do_step left with - | _::_ as res -> - (match solved goal res Utils.Right with - | No newgoals -> - (match first (aux (steps - 1) L) newgoals with - | Some g as success -> success - | None -> aux steps R goal) - | Yes newgoal -> Some newgoal) - | [] -> aux steps R goal) - | R -> - (match do_step right with - | _::_ as res -> - (match solved goal res Utils.Left with - | No newgoals -> - (match first (aux (steps - 1) L) newgoals with - | Some g as success -> success - | None -> None) - | Yes newgoal -> Some newgoal) - | [] -> None) + try + let s,_,_ = + Founif.unification [] m context left right CicUniv.empty_ugraph in + Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left)) + with CicUnification.UnificationFailure _ -> + let solutions = + unification_all env table (Equality.mk_tmp_equality + (0,(Cic.Implicit None,left,right,Utils.Incomparable),m)) + in + if solutions = [] then None + else + let s, e, swapped = List.hd solutions in + let _,p,(ty,l,r,_),me,id = Equality.open_equality e in + let bag, p = + if swapped then Equality.symmetric bag ty l id uri me else bag, p + in + Some (bag, m,s, p) in - aux steps L initgoal + let newgoal = + HExtlib.list_findopt + (fun (pr,mr,r) _ -> + try + let pl,ml,l,bag,m,s,p = + match + HExtlib.list_findopt (fun (pl,ml,l) _ -> + match is_solved l r ml mr with + | None -> None + | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p) + ) l_demod + with Some x -> x | _ -> raise Not_found + in + let pl = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pl + in + let pr = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pr + in + Some (bag,pr@pl@proof,m,s,p) + with Not_found -> None) + r_demod + in + newgoal ;; -let get_stats () = "" ;; + +