X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=62308896fd02b6b89bb420bd9c2c501c99273e54;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=5eb89650b706dfba2fa9198087b990d2e66989b1;hpb=03cff55eef08d25984bc92080e4cac93889f3ba7;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 5eb89650b..62308896f 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1,19 +1,139 @@ open Utils;; +type equality = + int * (* weight *) + proof * + (Cic.term * (* type *) + Cic.term * (* left side *) + Cic.term * (* right side *) + Utils.comparison) * (* ordering *) + Cic.metasenv * (* environment for metas *) + Cic.term list (* arguments *) + +and proof = + | BasicProof of Cic.term + | ProofBlock of + Cic.substitution * UriManager.uri * + (* name, ty, eq_ty, left, right *) + (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * + (Utils.pos * equality) * equality + | NoProof +;; + + +let string_of_equality ?env = + match env with + | None -> ( + function + | w, _, (ty, left, right, o), _, _ -> + Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty) + (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right) + ) + | Some (_, context, _) -> ( + let names = names_of_context context in + function + | w, _, (ty, left, right, o), _, _ -> + Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names) + (CicPp.pp left names) (string_of_comparison o) + (CicPp.pp right names) + ) +;; + + +let rec build_term_proof equality = +(* Printf.printf "build_term_proof %s" (string_of_equality equality); *) +(* print_newline (); *) + let _, proof, _, _, _ = equality 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') -> + let name, ty, eq_ty, left, right = t' in + let bo = + Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + eq_ty; left; right] + in + let t' = Cic.Lambda (name, ty, CicSubstitution.lift 1 bo) in +(* 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) + | Cic.Const (_, ens) + | Cic.MutInd (_, _, ens) + | Cic.MutConstruct (_, _, _, ens) -> + List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) + | Cic.Cast (s, t) + | Cic.Prod (_, s, t) + | Cic.Lambda (_, s, t) + | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) + | Cic.Appl l -> List.flatten (List.map metas_of_term l) + | Cic.MutCase (uri, i, s, t, l) -> + (metas_of_term s) @ (metas_of_term t) @ + (List.flatten (List.map metas_of_term l)) + | Cic.Fix (i, il) -> + List.flatten + (List.map (fun (s, i, t1, t2) -> + (metas_of_term t1) @ (metas_of_term t2)) il) + | Cic.CoFix (i, il) -> + List.flatten + (List.map (fun (s, t1, t2) -> + (metas_of_term t1) @ (metas_of_term t2)) il) + | _ -> [] +;; + + exception NotMetaConvertible;; let meta_convertibility_aux table t1 t2 = let module C = Cic in - let rec aux table t1 t2 = + let print_table t = + String.concat ", " + (List.map + (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t) + in + let rec aux ((table_l, table_r) as table) t1 t2 = +(* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *) +(* (CicPp.ppterm t1) (CicPp.ppterm t2) *) +(* (print_table table_l) (print_table table_r); *) match t1, t2 with - | t1, t2 when t1 = t2 -> table | C.Meta (m1, tl1), C.Meta (m2, tl2) -> - let m1_binding, table = - try List.assoc m1 table, table - with Not_found -> m2, (m1, m2)::table + let m1_binding, table_l = + try List.assoc m1 table_l, table_l + with Not_found -> m2, (m1, m2)::table_l + and m2_binding, table_r = + try List.assoc m2 table_r, table_r + with Not_found -> m1, (m2, m1)::table_r in - if m1_binding <> m2 then +(* let m1_binding, m2_binding, table = *) +(* let m1b, table = *) +(* try List.assoc m1 table, table *) +(* with Not_found -> m2, (m1, m2)::table *) +(* in *) +(* let m2b, table = *) +(* try List.assoc m2 table, table *) +(* with Not_found -> m1, (m2, m1)::table *) +(* in *) +(* m1b, m2b, table *) +(* in *) +(* Printf.printf "table_l: %s\ntable_r: %s\n\n" *) +(* (print_table table_l) (print_table table_r); *) + if (m1_binding <> m2) || (m2_binding <> m1) then raise NotMetaConvertible else ( try @@ -23,7 +143,7 @@ let meta_convertibility_aux table t1 t2 = | None, Some _ | Some _, None -> raise NotMetaConvertible | None, None -> res | Some t1, Some t2 -> (aux res t1 t2)) - table tl1 tl2 + (table_l, table_r) tl1 tl2 with Invalid_argument _ -> raise NotMetaConvertible ) @@ -70,6 +190,7 @@ let meta_convertibility_aux table t1 t2 = table il1 il2 with Invalid_argument _ -> raise NotMetaConvertible ) + | t1, t2 when t1 = t2 -> table | _, _ -> raise NotMetaConvertible and aux_ens table ens1 ens2 = @@ -91,45 +212,433 @@ 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 + true + else if (left = right') && (right = left') then + true else - let print_table t w = - Printf.printf "table %s is:\n" w; - List.iter - (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v) - t; - print_newline (); - in try - let table = meta_convertibility_aux [] left left' in -(* print_table table "before"; *) - let table = meta_convertibility_aux table right right' in -(* print_table table "after"; *) + let table = meta_convertibility_aux ([], []) left left' in + let _ = meta_convertibility_aux table right right' in true with NotMetaConvertible -> -(* Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *) -(* (CicPp.ppterm left) (CicPp.ppterm right) *) -(* (CicPp.ppterm left') (CicPp.ppterm right'); *) - false + try + let table = meta_convertibility_aux ([], []) left right' in + let _ = meta_convertibility_aux table right left' in + true + with NotMetaConvertible -> + false ;; let meta_convertibility t1 t2 = - try - let _ = meta_convertibility_aux [] t1 t2 in + let f t = + String.concat ", " + (List.map + (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t) + in + if t1 = t2 then true - with NotMetaConvertible -> - false + else + try + let l, r = meta_convertibility_aux ([], []) t1 t2 in + (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *) + true + with NotMetaConvertible -> + false +;; + + +let replace_metas (* context *) term = + let module C = Cic in + let rec aux = function + | C.Meta (i, c) -> +(* let irl = *) +(* CicMkImplicit.identity_relocation_list_for_metavariable context *) +(* in *) +(* if c = irl then *) +(* C.Implicit (Some (`MetaIndex i)) *) +(* else ( *) +(* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *) +(* (String.concat "\n" *) +(* (List.map *) +(* (function None -> "" | Some t -> CicPp.ppterm t) c)); *) +(* C.Meta (i, c) *) +(* ) *) + C.Implicit (Some (`MetaInfo (i, c))) + | C.Var (u, ens) -> C.Var (u, aux_ens ens) + | C.Const (u, ens) -> C.Const (u, aux_ens ens) + | C.Cast (s, t) -> C.Cast (aux s, aux t) + | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t) + | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t) + | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t) + | C.Appl l -> C.Appl (List.map aux l) + | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens) + | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens) + | C.MutCase (uri, i, s, t, l) -> + C.MutCase (uri, i, aux s, aux t, List.map aux l) + | C.Fix (i, il) -> + let il' = + List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in + C.Fix (i, il') + | C.CoFix (i, il) -> + let il' = + List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in + C.CoFix (i, il') + | t -> t + and aux_ens ens = + List.map (fun (u, t) -> (u, aux t)) ens + in + aux term +;; + + +let restore_metas (* context *) term = + let module C = Cic in + let rec aux = function + | C.Implicit (Some (`MetaInfo (i, c))) -> +(* let c = *) +(* CicMkImplicit.identity_relocation_list_for_metavariable context *) +(* in *) +(* C.Meta (i, c) *) +(* let local_context:(C.term option) list = *) +(* Marshal.from_string mc 0 *) +(* in *) +(* C.Meta (i, local_context) *) + C.Meta (i, c) + | C.Var (u, ens) -> C.Var (u, aux_ens ens) + | C.Const (u, ens) -> C.Const (u, aux_ens ens) + | C.Cast (s, t) -> C.Cast (aux s, aux t) + | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t) + | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t) + | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t) + | C.Appl l -> C.Appl (List.map aux l) + | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens) + | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens) + | C.MutCase (uri, i, s, t, l) -> + C.MutCase (uri, i, aux s, aux t, List.map aux l) + | C.Fix (i, il) -> + let il' = + List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in + C.Fix (i, il') + | C.CoFix (i, il) -> + let il' = + List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in + C.CoFix (i, il') + | t -> t + and aux_ens ens = + List.map (fun (u, t) -> (u, aux t)) ens + in + aux term +;; + + +let rec restore_subst (* context *) subst = + List.map + (fun (i, (c, t, ty)) -> + i, (c, restore_metas (* context *) t, ty)) + subst +;; + + +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 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 + (* 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 + 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 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 = let module S = CicSubstitution in let module C = Cic in + + let print_info = false in + +(* let _ = *) +(* let names = names_of_context context in *) +(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *) +(* (CicPp.pp what names) (CicPp.ppterm what) *) +(* (CicPp.pp where names) (CicPp.ppterm where); *) +(* print_newline (); *) +(* in *) (* return value: ((list of all possible beta expansions, subst, metasenv, ugraph), @@ -374,32 +883,47 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) | C.Meta _ when (not metas_ok) -> res, lifted_term | _ -> +(* let term' = *) +(* if match_only then replace_metas context term *) +(* else term *) +(* in *) try let subst', metasenv', ugraph' = - CicUnification.fo_unif metasenv context - (S.lift lift_amount what) term ugraph +(* 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 + else + CicUnification.fo_unif metasenv context + (S.lift lift_amount what) term ugraph in - (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *) - (* (CicPp.ppterm (S.lift lift_amount what)); *) - (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *) - (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *) +(* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *) +(* (CicPp.ppterm (S.lift lift_amount what)); *) +(* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *) +(* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *) (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *) - let term' = CicMetaSubst.apply_subst subst' term in ( - if match_only && not (meta_convertibility term term') then ( -(* Printf.printf "term e term' sono diversi!:\n%s\n%s\n\n" *) -(* (CicPp.ppterm term) (CicPp.ppterm term'); *) - res, lifted_term - ) - else -(* let _ = *) -(* if match_only then *) -(* Printf.printf "OK, trovato match con %s\n" *) -(* (CicPp.ppterm term) *) +(* if match_only then *) +(* let t' = CicMetaSubst.apply_subst subst' term in *) +(* if not (meta_convertibility term t') then ( *) +(* res, lifted_term *) +(* ) else ( *) +(* let metas = metas_of_term term in *) +(* let fix_subst = function *) +(* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *) +(* (j, (c, C.Meta (i, lc), ty)) *) +(* | s -> s *) (* in *) - ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, - lifted_term) - ) - with _ -> +(* let subst' = List.map fix_subst subst' in *) +(* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *) +(* lifted_term) *) +(* ) *) +(* else *) + ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, + lifted_term) + with e -> + if print_info then ( + print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e)); + ); res, lifted_term in (* Printf.printf "exit aux\n"; *) @@ -433,24 +957,30 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) ) exp_named_subst ([], []) in - let expansions, _ = aux 0 where context metasenv [] ugraph in - List.map - (fun (term, subst, metasenv, ugraph) -> - let term' = C.Lambda (C.Anonymous, type_of_what, term) in -(* Printf.printf "term is: %s\nsubst is:\n%s\n\n" *) -(* (CicPp.ppterm term') (print_subst subst); *) - (term', subst, metasenv, ugraph)) - expansions -;; - - -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 expansions, _ = +(* let where = *) +(* if match_only then replace_metas (\* context *\) where *) +(* else where *) +(* in *) + if print_info then ( + Printf.printf "searching %s inside %s\n" + (CicPp.ppterm what) (CicPp.ppterm where); + ); + aux 0 where context metasenv [] ugraph + in + let mapfun = +(* if match_only then *) +(* (fun (term, subst, metasenv, ugraph) -> *) +(* let term' = *) +(* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *) +(* and subst = restore_subst subst in *) +(* (term', subst, metasenv, ugraph)) *) +(* else *) + (fun (term, subst, metasenv, ugraph) -> + let term' = C.Lambda (C.Anonymous, type_of_what, term) in + (term', subst, metasenv, ugraph)) + in + List.map mapfun expansions ;; @@ -466,18 +996,10 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match term with | C.Prod (name, s, t) -> (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *) - let (head, newmetas, args, _) = - PrimitiveTactics.new_metasenv_for_apply newmeta proof + let (head, newmetas, args, newmeta) = + ProofEngineHelpers.saturate_term newmeta [] context (S.lift index term) in - let newmeta = - List.fold_left - (fun maxm arg -> - match arg with - | C.Meta (i, _) -> (max maxm i) - | _ -> assert false) - newmeta args - in let p = if List.length args = 0 then C.Rel index @@ -487,12 +1009,20 @@ 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 proof = BasicProof p in + let e = (w, proof, (ty, t1, t2, o), newmetas, args) in + 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, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in + Some e, (newmeta+1) | _ -> None, newmeta in ( match do_find context term with @@ -509,12 +1039,15 @@ 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 ((w, p, (ty, left, right, o), menv, args) as equality) = + let table = Hashtbl.create (List.length args) in let newargs, _ = List.fold_right (fun t (newargs, index) -> match t with - | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1) + | Cic.Meta (i, l) -> + Hashtbl.add table i index; + ((Cic.Meta (index, l))::newargs, index+1) | _ -> assert false) args ([], newmeta) in @@ -522,14 +1055,27 @@ let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) = ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs ~where in - let menv', _ = + let menv' = List.fold_right - (fun (i, context, term) (menv, index) -> - ((index, context, term)::menv, index+1)) - menv ([], newmeta) + (fun (i, context, term) menv -> + try + let index = Hashtbl.find table i in + (index, context, term)::menv + with Not_found -> + (i, context, term)::menv) + menv [] + in + let ty = repl ty + and left = repl left + and right = repl right in + let metas = (metas_of_term left) @ (metas_of_term right) in + let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' + and newargs = + List.filter + (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs in (newmeta + (List.length newargs) + 1, - (repl proof, (repl ty, repl left, repl right), menv', newargs)) + (w, p, (ty, left, right, o), menv', newargs)) ;; @@ -537,7 +1083,11 @@ 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, BasicProof proof, (ty, t1, t2, o), [], []) in + e +(* (proof, (ty, t1, t2, o), [], []) *) | _ -> raise TermIsNotAnEquality ;; @@ -546,6 +1096,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 @@ -554,66 +1105,77 @@ 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 - (* ALB: TODO check that ty and eq_ty are indeed equal... *) - assert (eq_ty = ty); - - let where, is_left = - match nonrec_kbo left right with - | Lt -> right, false - | Gt -> left, true - | _ -> ( - Printf.printf "????????? %s = %s" (CicPp.ppterm left) - (CicPp.ppterm right); - print_newline (); - assert false (* again, for ground terms this shouldn't happen... *) - ) - in - let metasenv' = newmetas @ metasenv in - let res1 = - List.filter - (fun (t, s, m, ug) -> - nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt) - (beta_expand t1 ty where context metasenv' ugraph) - and res2 = - List.filter - (fun (t, s, m, ug) -> - nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt) - (beta_expand t2 ty where context metasenv' ugraph) - in -(* let what, other = *) -(* if is_left then left, right *) -(* else right, left *) -(* in *) - let build_new what other eq_URI (t, s, m, ug) = - let newgoal, newgoalproof = - match t with - | C.Lambda (nn, ty, bo) -> - let bo' = S.subst (M.apply_subst s other) bo in - let bo'' = - C.Appl ( - [C.MutInd (HL.Logic.eq_URI, 0, []); - S.lift 1 eq_ty] @ - if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo']) + let compare_terms = !Utils.compare_terms in + + if eq_ty <> ty then + [] + else + let where, is_left = + match t_order (* compare_terms left right *) with + | Lt -> right, false + | Gt -> left, true + | _ -> ( + Printf.printf "????????? %s = %s" (CicPp.ppterm left) + (CicPp.ppterm right); + print_newline (); + assert false (* again, for ground terms this shouldn't happen... *) + ) + in + let metasenv' = newmetas @ metasenv 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), [] + | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph) + | _ -> + let res1 = + List.filter + (fun (t, s, m, ug) -> + compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt) + (beta_expand t1 ty where context metasenv' ugraph) + and res2 = + List.filter + (fun (t, s, m, ug) -> + compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt) + (beta_expand t2 ty where context metasenv' ugraph) in - let t' = C.Lambda (nn, ty, bo'') in - S.subst (M.apply_subst s other) bo, - M.apply_subst s - (C.Appl [C.Const (eq_URI, []); ty; what; t'; - proof; other; eqproof]) - | _ -> assert false + res1, res2 in - let equation = - if is_left then (eq_ty, newgoal, right) - else (eq_ty, left, newgoal) + (* let what, other = *) + (* if is_left then left, right *) + (* else right, left *) + (* in *) + let build_new what other eq_URI (t, s, m, ug) = + let newgoal, newgoalproof = + match t with + | C.Lambda (nn, ty, bo) -> + let bo' = S.subst (M.apply_subst s other) bo in + let bo'' = + C.Appl ( + [C.MutInd (HL.Logic.eq_URI, 0, []); + S.lift 1 eq_ty] @ + if is_left then [bo'; S.lift 1 right] + else [S.lift 1 left; bo']) + in + let t' = C.Lambda (nn, ty, bo'') in + S.subst (M.apply_subst s other) bo, + M.apply_subst s + (C.Appl [C.Const (eq_URI, []); ty; what; t'; + proof; other; eqproof]) + | _ -> assert false + in + let equation = + if is_left then (eq_ty, newgoal, right, compare_terms newgoal right) + else (eq_ty, left, newgoal, compare_terms left newgoal) + in + (newgoalproof (* eqproof *), equation, [], []) in - (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 - new1 @ new2 + 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 + new1 @ new2 ;; @@ -623,92 +1185,130 @@ 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 - (* TODO check if ty and ty' are equal... *) - assert (eq_ty = ty'); - -(* let ok term subst other other_eq_side ugraph = *) -(* match term with *) -(* | C.Lambda (nn, ty, bo) -> *) -(* let bo' = S.subst (M.apply_subst subst other) bo in *) -(* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *) -(* not res *) -(* | _ -> assert false *) -(* in *) - let condition left right what other (t, s, m, ug) = - let subst = M.apply_subst s in - let cmp1 = nonrec_kbo (subst what) (subst other) in - let cmp2 = nonrec_kbo (subst left) (subst right) in -(* cmp1 = Gt && cmp2 = Gt *) - cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le -(* && (ok t s other right ug) *) - in - let metasenv' = metasenv @ newmetas @ newm' in - let beta_expand = beta_expand ~metas_ok:false in - let res1 = - List.filter - (condition left right t1 t2) - (beta_expand t1 eq_ty left context metasenv' ugraph) - and res2 = - List.filter - (condition left right t2 t1) - (beta_expand t2 eq_ty left context metasenv' ugraph) - and res3 = - List.filter - (condition right left t1 t2) - (beta_expand t1 eq_ty right context metasenv' ugraph) - and res4 = - List.filter - (condition right left t2 t1) - (beta_expand t2 eq_ty right context metasenv' ugraph) - in - let newmetas = newmetas @ newm' in - let newargs = args @ args' in - let build_new what other is_left eq_URI (t, s, m, ug) = -(* let what, other = *) -(* if is_left then left, right *) -(* else right, left *) -(* in *) - let newterm, neweqproof = - match t with - | C.Lambda (nn, ty, bo) -> - let bo' = M.apply_subst s (S.subst other bo) in - let bo'' = - C.Appl ( - [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ - if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo']) - in - let t' = C.Lambda (nn, ty, bo'') in - bo', - M.apply_subst s - (C.Appl [C.Const (eq_URI, []); ty; what; t'; eqproof; other; eqp']) - | _ -> assert false + let compare_terms = !Utils.compare_terms in + + if eq_ty <> ty' then + newmeta, [] + else + (* let ok term subst other other_eq_side ugraph = *) + (* match term with *) + (* | C.Lambda (nn, ty, bo) -> *) + (* let bo' = S.subst (M.apply_subst subst other) bo in *) + (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *) + (* not res *) + (* | _ -> assert false *) + (* in *) + let condition left right what other (t, s, m, ug) = + let subst = M.apply_subst s in + let cmp1 = compare_terms (subst what) (subst other) in + let cmp2 = compare_terms (subst left) (subst right) in + (* cmp1 = Gt && cmp2 = Gt *) + cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le + (* && (ok t s other right ug) *) in - let newmeta, newequality = - let left, right = - if is_left then (newterm, M.apply_subst s right) - else (M.apply_subst s left, newterm) in - fix_metas !maxmeta - (neweqproof, (eq_ty, left, right), newmetas, newargs) + let metasenv' = metasenv @ newmetas @ newm' in + let beta_expand = beta_expand ~metas_ok:false 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 + (condition l r s t) + (beta_expand s eq_ty l context metasenv' ugraph) + in + match cmp1, cmp2 with + | Gt, Gt -> + (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], [] + | Gt, Lt -> + [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], [] + | Lt, Gt -> + [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), [] + | Lt, Lt -> + [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph) + | Gt, _ -> + let res1 = res left right t1 t2 + and res2 = res left right t2 t1 in + res1, res2, [], [] + | Lt, _ -> + let res3 = res right left t1 t2 + and res4 = res right left t2 t1 in + [], [], res3, res4 + | _, Gt -> + let res1 = res left right t1 t2 + and res3 = res right left t1 t2 in + res1, [], res3, [] + | _, Lt -> + let res2 = res left right t2 t1 + and res4 = res right left t2 t1 in + [], res2, [], res4 + | _, _ -> + let res1 = res left right t1 t2 + and res2 = res left right t2 t1 + and res3 = res right left t1 t2 + and res4 = res right left t2 t1 in + res1, res2, res3, res4 in - maxmeta := newmeta; - newequality - in - let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1 - and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2 - 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), _, _ -> - not (fst (CR.are_convertible context left right ugraph)) - in - !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4)) + let newmetas = newmetas @ newm' in + let newargs = args @ args' in + let build_new what other is_left eq_URI (t, s, m, ug) = + (* let what, other = *) + (* if is_left then left, right *) + (* else right, left *) + (* in *) + let newterm, neweqproof = + match t with + | C.Lambda (nn, ty, bo) -> + let bo' = M.apply_subst s (S.subst other bo) in + let bo'' = + C.Appl ( + [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ + if is_left then [bo'; S.lift 1 right] + else [S.lift 1 left; bo']) + in + let t' = C.Lambda (nn, ty, bo'') in + bo', + M.apply_subst s + (C.Appl [C.Const (eq_URI, []); ty; what; t'; + eqproof; other; eqp']) + | _ -> assert false + in + let newmeta, newequality = + 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, neworder), newmetas, newargs) + in + maxmeta := newmeta; + newequality + in + let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1 + and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2 + 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, _), _, _ -> + not (fst (CR.are_convertible context left right ugraph)) + in + (!maxmeta, + (List.filter ok (new1 @ new2 @ new3 @ new4))) +;; +*) + + +let is_identity ((_, context, ugraph) as env) = function + | ((_, _, (ty, left, right, _), _, _) as equality) -> + (left = right || + (fst (CicReduction.are_convertible context left right ugraph))) ;; +(* let demodulation newmeta (metasenv, context, ugraph) target source = let module C = Cic in let module S = CicSubstitution in @@ -716,35 +1316,73 @@ 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 + if eq_ty <> ty then newmeta, target else - let get_params step = - match step with - | 3 -> true, t1, t2, HL.Logic.eq_ind_URI - | 2 -> false, t1, t2, HL.Logic.eq_ind_URI - | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI - | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI - | _ -> assert false + let first_step, get_params = + 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 + | _ -> assert false) + | Lt -> 1, (function + | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI + | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI + | _ -> assert false) + | _ -> + let first_step = 3 in + let get_params step = + match step with + | 3 -> true, t1, t2, HL.Logic.eq_ind_URI + | 2 -> false, t1, t2, HL.Logic.eq_ind_URI + | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI + | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI + | _ -> assert false + in + 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 + let names = names_of_context context in (* Printf.printf *) -(* "demodulate\ntarget: %s = %s\nwhat: %s\nother: %s\nis_left: %s\n" *) -(* (CicPp.ppterm left) (CicPp.ppterm right) (CicPp.ppterm what) *) -(* (CicPp.ppterm other) (string_of_bool is_left); *) -(* Printf.printf "step: %d\n" step; *) +(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *) +(* (string_of_equality ~env target) (CicPp.pp what names) *) +(* (CicPp.pp other names) (string_of_bool is_left); *) +(* Printf.printf "step: %d" step; *) (* print_newline (); *) + let ok (t, s, m, ug) = - nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt + compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt in let res = - List.filter ok - (beta_expand ~metas_ok:false ~match_only:true - what ty left context (metasenv @ metas) ugraph) + let r = (beta_expand ~metas_ok:false ~match_only:true + what ty (if is_left then left else right) + context (metasenv @ metas) ugraph) + in +(* let m' = metas_of_term what *) +(* and m'' = metas_of_term (if is_left then left else right) in *) +(* if (List.mem 527 m'') && (List.mem 6 m') then ( *) +(* Printf.printf *) +(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *) +(* (string_of_equality ~env target) (CicPp.pp what names) *) +(* (CicPp.pp other names) (string_of_bool is_left); *) +(* Printf.printf "step: %d" step; *) +(* print_newline (); *) +(* print_endline "res:"; *) +(* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *) +(* print_newline (); *) +(* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *) +(* print_newline (); *) +(* ); *) + List.filter ok r in match res with | [] -> @@ -754,7 +1392,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source = let newterm, newproof = match t with | C.Lambda (nn, ty, bo) -> - let bo' = M.apply_subst s (S.subst other bo) in +(* let bo' = M.apply_subst s (S.subst other bo) in *) + let bo' = S.subst (M.apply_subst s other) bo in let bo'' = C.Appl ( [C.MutInd (HL.Logic.eq_URI, 0, []); @@ -763,7 +1402,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source = else [S.lift 1 left; bo']) in let t' = C.Lambda (nn, ty, bo'') in - M.apply_subst s (S.subst other bo), +(* M.apply_subst s (S.subst other bo), *) + bo', M.apply_subst s (C.Appl [C.Const (eq_URI, []); ty; what; t'; proof; other; proof']) @@ -771,23 +1411,41 @@ let demodulation newmeta (metasenv, context, ugraph) target source = in let newmeta, newtarget = let left, right = - if is_left then (newterm, M.apply_subst s right) - else (M.apply_subst s left, newterm) in - let newmetasenv = metasenv @ metas in - let newargs = args @ args' in - fix_metas newmeta - (newproof, (eq_ty, left, right), newmetasenv, newargs) +(* if is_left then (newterm, M.apply_subst s right) *) +(* else (M.apply_subst s left, newterm) in *) + 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 *) +(* (newproof, (eq_ty, left, right), newmetasenv, newargs) *) + let m = (metas_of_term left) @ (metas_of_term right) in + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas + and newargs = + List.filter + (function C.Meta (i, _) -> List.mem i m | _ -> assert false) + args + in + newmeta, + (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs) in - let _, (_, left, right), _, _ = newtarget - and _, (_, oldleft, oldright), _, _ = target in (* Printf.printf *) -(* "demodulate, newtarget: %s = %s\ntarget was: %s = %s\n" *) -(* (CicPp.ppterm left) (CicPp.ppterm right) *) -(* (CicPp.ppterm oldleft) (CicPp.ppterm oldright); *) +(* "demodulate, newtarget: %s\ntarget was: %s\n" *) +(* (string_of_equality ~env newtarget) *) +(* (string_of_equality ~env target); *) +(* (\* let _, _, newm, newa = newtarget in *\) *) +(* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *) +(* (\* (print_metasenv newm) *\) *) +(* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *) (* print_newline (); *) - demodulate newmeta step metasenv newtarget + if is_identity env newtarget then + newmeta, newtarget + else + demodulate newmeta first_step metasenv newtarget in - demodulate newmeta 3 (metasenv @ metas') target + demodulate newmeta first_step (metasenv @ metas') target ;; @@ -798,3 +1456,76 @@ let demodulation newmeta env target source = *) +let subsumption env target source = + let _, (ty, tl, tr, _), tmetas, _ = target + and _, (ty', sl, sr, _), smetas, _ = source in + if ty <> ty' then + false + else + let metasenv, context, ugraph = env in + let metasenv = metasenv @ tmetas @ smetas in + let names = names_of_context context in + let samesubst subst subst' = +(* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *) +(* (print_subst subst) (print_subst subst'); *) +(* print_newline (); *) + let tbl = Hashtbl.create (List.length subst) in + List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst; + List.for_all + (fun (m, (c, t1, t2)) -> + try + let c', t1', t2' = Hashtbl.find tbl m in + if (c = c') && (t1 = t1') && (t2 = t2') then true + else false + with Not_found -> + true) + subst' + in + let subsaux left right left' right' = + try + let subst, menv, ug = matching metasenv context left left' ugraph + and subst', menv', ug' = matching metasenv context right right' ugraph + in +(* Printf.printf "left = right: %s = %s\n" *) +(* (CicPp.pp left names) (CicPp.pp right names); *) +(* Printf.printf "left' = right': %s = %s\n" *) +(* (CicPp.pp left' names) (CicPp.pp right' names); *) + samesubst subst subst' + with e -> +(* print_endline (Printexc.to_string e); *) + false + in + let res = + if subsaux tl tr sl sr then true + else subsaux tl tr sr sl + in + if res then ( + Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n" + (string_of_equality ~env target) (string_of_equality ~env source); + print_newline (); + ); + 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 +;;