X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=e79d78e846cac9677d6280cba0f78cf3a6e45b07;hb=bdc855b1b6c9552a49a01769cb906a438ca60cc4;hp=4d56d30e963d9f0dcf5b8a55aac923fe21a4a6c6;hpb=c76c8c83852508d69e7765dc9e929cdcf34af57d;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 4d56d30e9..e79d78e84 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -5,16 +5,17 @@ let string_of_equality ?env = match env with | None -> ( function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty) - (CicPp.ppterm left) (CicPp.ppterm right) + | _, (ty, left, right, o), _, _ -> + Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty) + (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right) ) | Some (_, context, _) -> ( let names = names_of_context context in function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names) - (CicPp.pp left names) (CicPp.pp right names) + | _, (ty, left, right, o), _, _ -> + Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names) + (CicPp.pp left names) (string_of_comparison o) + (CicPp.pp right names) ) ;; @@ -160,8 +161,8 @@ let meta_convertibility_aux table t1 t2 = let meta_convertibility_eq eq1 eq2 = - let _, (ty, left, right), _, _ = eq1 - and _, (ty', left', right'), _, _ = eq2 in + let _, (ty, left, right, _), _, _ = eq1 + and _, (ty', left', right', _), _, _ = eq2 in if ty <> ty' then false else if (left = left') && (right = right') then @@ -584,7 +585,7 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) (* 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 + matching metasenv context term (S.lift lift_amount what) ugraph else CicUnification.fo_unif metasenv context (S.lift lift_amount what) term ugraph @@ -677,12 +678,13 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) type equality = - Cic.term * (* proof *) - (Cic.term * (* type *) - Cic.term * (* left side *) - Cic.term) * (* right side *) - Cic.metasenv * (* environment for metas *) - Cic.term list (* arguments *) + Cic.term * (* proof *) + (Cic.term * (* type *) + Cic.term * (* left side *) + Cic.term * (* right side *) + Utils.comparison) * (* ordering *) + Cic.metasenv * (* environment for metas *) + Cic.term list (* arguments *) ;; @@ -719,12 +721,15 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match head with | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> Printf.printf "OK: %s\n" (CicPp.ppterm term); - Some (p, (ty, t1, t2), newmetas, args), (newmeta+1) + let o = !Utils.compare_terms t1 t2 in + Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1) | _ -> None, newmeta ) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> - Some (C.Rel index, - (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1) + let t1 = S.lift index t1 + and t2 = S.lift index t2 in + let o = !Utils.compare_terms t1 t2 in + Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1) | _ -> None, newmeta in ( match do_find context term with @@ -741,7 +746,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; -let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) = +let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) = let table = Hashtbl.create (List.length args) in let newargs, _ = List.fold_right @@ -777,7 +782,7 @@ let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) = (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs in (newmeta + (List.length newargs) + 1, - (repl proof, (ty, left, right), menv', newargs)) + (repl proof, (ty, left, right, o), menv', newargs)) ;; @@ -785,7 +790,8 @@ exception TermIsNotAnEquality;; let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> - (proof, (ty, t1, t2), [], []) + let o = !Utils.compare_terms t1 t2 in + (proof, (ty, t1, t2, o), [], []) | _ -> raise TermIsNotAnEquality ;; @@ -802,8 +808,8 @@ let superposition_left (metasenv, context, ugraph) target source = 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), _, _ = target in - let eqproof, (ty, t1, t2), newmetas, args = source in + 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 @@ -811,7 +817,7 @@ let superposition_left (metasenv, context, ugraph) target source = [] else let where, is_left = - match compare_terms left right with + match t_order (* compare_terms left right *) with | Lt -> right, false | Gt -> left, true | _ -> ( @@ -822,7 +828,7 @@ let superposition_left (metasenv, context, ugraph) target source = ) in let metasenv' = newmetas @ metasenv in - let result = compare_terms t1 t2 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), [] @@ -865,10 +871,10 @@ let superposition_left (metasenv, context, ugraph) target source = | _ -> assert false in let equation = - if is_left then (eq_ty, newgoal, right) - else (eq_ty, left, newgoal) + if is_left then (eq_ty, newgoal, right, compare_terms newgoal right) + else (eq_ty, left, newgoal, compare_terms left newgoal) in - (eqproof, equation, [], []) + (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 @@ -882,8 +888,8 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let module CR = CicReduction in - let eqproof, (eq_ty, left, right), newmetas, args = target in - let eqp', (ty', t1, t2), newm', args' = source 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 @@ -909,8 +915,8 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = in let metasenv' = metasenv @ newmetas @ newm' in let beta_expand = beta_expand ~metas_ok:false in - let cmp1 = compare_terms left right - and cmp2 = compare_terms t1 t2 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 @@ -977,8 +983,9 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = 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), newmetas, newargs) + (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs) in maxmeta := newmeta; newequality @@ -988,15 +995,16 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = 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), _, _ -> + | _, (_, left, right, _), _, _ -> not (fst (CR.are_convertible context left right ugraph)) in - !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4)) + (!maxmeta, + (List.filter ok (new1 @ new2 @ new3 @ new4))) ;; let is_identity ((_, context, ugraph) as env) = function - | ((_, (ty, left, right), _, _) as equality) -> + | ((_, (ty, left, right, _), _, _) as equality) -> let res = (left = right || (fst (CicReduction.are_convertible context left right ugraph))) @@ -1016,8 +1024,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source = let module HL = HelmLibraryObjects in let module CR = CicReduction in - let proof, (eq_ty, left, right), metas, args = target - and proof', (ty, t1, t2), metas', args' = source 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 @@ -1025,7 +1033,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source = newmeta, target else let first_step, get_params = - match compare_terms t1 t2 with + 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 @@ -1047,7 +1055,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source = first_step, get_params in let rec demodulate newmeta step metasenv target = - let proof, (eq_ty, left, right), metas, args = target in + 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 @@ -1116,6 +1124,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source = 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 *) @@ -1127,7 +1136,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source = (function C.Meta (i, _) -> List.mem i m | _ -> assert false) args in - newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs) + newmeta, + (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs) in (* Printf.printf *) (* "demodulate, newtarget: %s\ntarget was: %s\n" *) @@ -1155,8 +1165,8 @@ let demodulation newmeta env target source = let subsumption env target source = - let _, (ty, tl, tr), tmetas, _ = target - and _, (ty', sl, sr), smetas, _ = source in + let _, (ty, tl, tr, _), tmetas, _ = target + and _, (ty', sl, sr, _), smetas, _ = source in if ty <> ty' then false else @@ -1204,3 +1214,25 @@ let subsumption env target source = ); 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 +;;