X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=f5233d03dbab9e907e5c02711729023019b32afa;hb=2daf59a983cae8151e513196577ae77b1d12e157;hp=4d56d30e963d9f0dcf5b8a55aac923fe21a4a6c6;hpb=c76c8c83852508d69e7765dc9e929cdcf34af57d;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 4d56d30e9..f5233d03d 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1,24 +1,84 @@ open Utils;; +type equality = + int * (* weight *) + (Cic.term * (* type *) + Cic.term * (* left side *) + Cic.term * (* right side *) + Utils.comparison) * (* ordering *) + Cic.metasenv * (* environment for metas *) + Cic.term list (* arguments *) +;; + + +type proof = + | BasicProof of Cic.term + | ProofBlock of + Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) * + equality + | NoProof +;; + + 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) ) ;; +let prooftable = Hashtbl.create 2001;; + +let store_proof equality proof = + if not (Hashtbl.mem prooftable equality) then + Hashtbl.add prooftable equality proof +;; + + +let delete_proof equality = +(* Printf.printf "| Removing proof of %s" (string_of_equality equality); *) +(* print_newline (); *) + Hashtbl.remove prooftable equality +;; + + +let rec build_term_proof equality = +(* Printf.printf "build_term_proof %s" (string_of_equality equality); *) +(* print_newline (); *) + let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in + match proof with + | NoProof -> + Printf.fprintf stderr "WARNING: no proof for %s\n" + (string_of_equality equality); + Cic.Implicit None + | BasicProof term -> term + | ProofBlock (subst, eq_URI, t', (pos, eq), eq') -> +(* Printf.printf " ProofBlock: eq = %s, eq' = %s" *) +(* (string_of_equality eq) (string_of_equality eq'); *) +(* print_newline (); *) + let proof' = build_term_proof eq in + let eqproof = build_term_proof eq' in + let _, (ty, what, other, _), menv', args' = eq in + let what, other = if pos = Utils.Left then what, other else other, what in + CicMetaSubst.apply_subst subst + (Cic.Appl [Cic.Const (eq_URI, []); ty; + what; t'; eqproof; other; proof']) +;; + + let rec metas_of_term = function | Cic.Meta (i, c) -> [i] | Cic.Var (_, ens) @@ -160,8 +220,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 @@ -293,29 +353,285 @@ let rec restore_subst (* context *) subst = ;; -exception MatchingFailure;; +let rec check_irl start = function + | [] -> true + | None::tl -> check_irl (start+1) tl + | (Some (Cic.Rel x))::tl -> + if x = start then check_irl (start+1) tl else false + | _ -> false +;; -let matching metasenv context t1 t2 ugraph = - try - let subst, metasenv, ugraph = - CicUnification.fo_unif metasenv context t1 t2 ugraph +let rec is_simple_term = function + | Cic.Appl ((Cic.Meta _)::_) -> false + | Cic.Appl l -> List.for_all is_simple_term l + | Cic.Meta (i, l) -> check_irl 1 l + | Cic.Rel _ -> true + | _ -> false +;; + + +let lookup_subst meta subst = + match meta with + | Cic.Meta (i, _) -> ( + try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t + with Not_found -> meta + ) + | _ -> assert false +;; + + +let unification_simple metasenv context t1 t2 ugraph = + let module C = Cic in + let module M = CicMetaSubst in + let module U = CicUnification in + let lookup = lookup_subst in + let rec occurs_check subst what where = + (* Printf.printf "occurs_check %s %s" *) + (* (CicPp.ppterm what) (CicPp.ppterm where); *) + (* print_newline (); *) + match where with + | t when what = t -> true + | C.Appl l -> List.exists (occurs_check subst what) l + | C.Meta _ -> + let t = lookup where subst in + if t <> where then occurs_check subst what t else false + | _ -> false + in + let rec unif subst menv s t = +(* Printf.printf "unif %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 + and t = match t with C.Meta _ -> lookup t subst | _ -> t in - let t' = CicMetaSubst.apply_subst subst t1 in - if not (meta_convertibility t1 t') then - raise MatchingFailure + (* 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 -> + unif subst menv t s + | C.Meta _, t when occurs_check subst s t -> + raise (U.UnificationFailure "Inference.unification.unif") +(* | C.Meta (i, l), C.Meta (j, l') -> *) +(* let _, _, ty = CicUtil.lookup_meta i menv in *) +(* let _, _, ty' = CicUtil.lookup_meta j menv in *) +(* let binding1 = lookup s subst in *) +(* let binding2 = lookup t subst in *) +(* let subst, menv = *) +(* if binding1 != s then *) +(* if binding2 != t then *) +(* unif subst menv binding1 binding2 *) +(* else *) +(* if binding1 = t then *) +(* subst, menv *) +(* else *) +(* ((j, (context, binding1, ty'))::subst, *) +(* List.filter (fun (m, _, _) -> j <> m) menv) *) +(* else *) +(* if binding2 != t then *) +(* if s = binding2 then *) +(* subst, menv *) +(* else *) +(* ((i, (context, binding2, ty))::subst, *) +(* List.filter (fun (m, _, _) -> i <> m) menv) *) +(* else *) +(* ((i, (context, t, ty))::subst, *) +(* List.filter (fun (m, _, _) -> i <> m) menv) *) +(* in *) +(* subst, menv *) + + | C.Meta (i, l), t -> + let _, _, ty = CicUtil.lookup_meta i menv in + let 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 _ -> unif subst menv t s + | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> + raise (U.UnificationFailure "Inference.unification.unif") + | C.Appl (hds::tls), C.Appl (hdt::tlt) -> ( + try + List.fold_left2 + (fun (subst', menv) s t -> unif subst' menv s t) + (subst, menv) tls tlt + with e -> + raise (U.UnificationFailure "Inference.unification.unif") + ) + | _, _ -> raise (U.UnificationFailure "Inference.unification.unif") + in + let subst, menv = unif [] metasenv t1 t2 in + (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *) + (* print_newline (); *) +(* let rec fix_term = function *) +(* | (C.Meta (i, l) as t) -> *) +(* lookup t subst *) +(* | C.Appl l -> C.Appl (List.map fix_term l) *) +(* | t -> t *) +(* in *) +(* let rec fix_subst = function *) +(* | [] -> [] *) +(* | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *) +(* in *) +(* List.rev (fix_subst subst), menv, ugraph *) + List.rev subst, menv, ugraph +;; + + +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 + CicUnification.fo_unif metasenv context t1 t2 ugraph else - let metas = metas_of_term t1 in - let fix_subst = function - | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas -> - (j, (c, Cic.Meta (i, lc), ty)) - | s -> s + unification_simple metasenv context t1 t2 ugraph + in + let rec fix_term = function + | (Cic.Meta (i, l) as t) -> + let t' = lookup_subst t subst in + if t <> t' then fix_term t' else t + | Cic.Appl l -> Cic.Appl (List.map fix_term l) + | t -> t + in + let rec fix_subst = function + | [] -> [] + | (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 +;; + +(* let unification = CicUnification.fo_unif;; *) + +exception MatchingFailure;; + + +let matching_simple metasenv context t1 t2 ugraph = + let module C = Cic in + let module M = CicMetaSubst in + let module U = CicUnification in + let lookup meta subst = + match meta with + | C.Meta (i, _) -> ( + try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t + with Not_found -> meta + ) + | _ -> 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 + in + 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 when value <> s -> + raise MatchingFailure + | 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 e -> +(* 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 *) + try + let subst, metasenv, ugraph = + (* CicUnification.fo_unif metasenv context t1 t2 ugraph *) + unification metasenv context t1 t2 ugraph in - let subst = List.map fix_subst subst in - subst, metasenv, ugraph - with e -> - raise MatchingFailure + let t' = CicMetaSubst.apply_subst subst t1 in + if not (meta_convertibility t1 t') then + raise MatchingFailure + else + let metas = metas_of_term t1 in + let fix_subst = function + | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas -> + (j, (c, Cic.Meta (i, lc), ty)) + | 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 e -> +(* Printf.printf "failed to match %s %s\n" *) +(* (CicPp.ppterm t1) (CicPp.ppterm t2); *) + 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 = @@ -584,7 +900,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 @@ -676,16 +992,6 @@ 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 *) -;; - - let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = let module C = Cic in let module S = CicSubstitution in @@ -719,12 +1025,21 @@ 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 + let w = compute_equality_weight ty t1 t2 in + let e = (w, (ty, t1, t2, o), newmetas, args) in + store_proof e (BasicProof p); + Some e, (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 + let w = compute_equality_weight ty t1 t2 in + let e = (w, (ty, t1, t2, o), [], []) in + store_proof e (BasicProof (C.Rel index)); + Some e, (newmeta+1) | _ -> None, newmeta in ( match do_find context term with @@ -741,7 +1056,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 ((weight, (ty, left, right, o), menv, args) as equality) = let table = Hashtbl.create (List.length args) in let newargs, _ = List.fold_right @@ -777,7 +1092,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)) + (weight, (ty, left, right, o), menv', newargs)) ;; @@ -785,7 +1100,12 @@ 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 + let w = compute_equality_weight ty t1 t2 in + let e = (w, (ty, t1, t2, o), [], []) in + store_proof e (BasicProof proof); + e +(* (proof, (ty, t1, t2, o), [], []) *) | _ -> raise TermIsNotAnEquality ;; @@ -794,6 +1114,7 @@ let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function 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 @@ -802,8 +1123,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 +1132,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 +1143,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 +1186,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 +1203,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 +1230,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 +1298,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 +1310,17 @@ 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))) @@ -1009,6 +1333,7 @@ let is_identity ((_, context, ugraph) as env) = function ;; +(* let demodulation newmeta (metasenv, context, ugraph) target source = let module C = Cic in let module S = CicSubstitution in @@ -1016,8 +1341,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 +1350,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 +1372,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 +1441,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 +1453,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 +1482,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 +1531,26 @@ 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 +;;