X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=969d412cef43a28151e995250fdf10d2adc172c4;hb=9e3eb63a93acaca0b4ad59c213e9ea430524d3ae;hp=e79d78e846cac9677d6280cba0f78cf3a6e45b07;hpb=bdc855b1b6c9552a49a01769cb906a438ca60cc4;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index e79d78e84..969d412ce 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1,25 +1,153 @@ 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 = + | NoProof + | 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) * proof + | ProofGoalBlock of proof * equality + | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof +;; + + let string_of_equality ?env = match env with | None -> ( function - | _, (ty, left, right, o), _, _ -> - Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty) + | 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 - | _, (ty, left, right, o), _, _ -> - Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names) + | 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 build_proof_term equality = +(* Printf.printf "build_term_proof %s" (string_of_equality equality); *) +(* print_newline (); *) + + let indent = ref 0 in + + let rec do_build_proof proof = + match proof with + | NoProof -> + Printf.fprintf stderr "WARNING: no proof!\n"; +(* (string_of_equality equality); *) + Cic.Implicit None + | BasicProof term -> term + | ProofGoalBlock (proofbit, equality) -> + print_endline "found ProofGoalBlock, going up..."; + let _, proof, _, _, _ = equality in + do_build_goal_proof proofbit proof + | ProofSymBlock (ens, proof) -> + let proof = do_build_proof proof in + Cic.Appl [ + Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *) + proof + ] + | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) -> +(* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *) +(* print_newline (); *) + + 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 s = String.make !indent ' ' in *) +(* incr indent; *) + +(* print_endline (s ^ "build proof'------------"); *) + + let proof' = + let _, proof', _, _, _ = eq in + do_build_proof proof' + in +(* print_endline (s ^ "END proof'"); *) + +(* print_endline (s ^ "build eqproof-----------"); *) + + let eqproof = do_build_proof eqproof in + +(* print_endline (s ^ "END eqproof"); *) +(* decr indent; *) + + + 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']) + + and do_build_goal_proof proofbit proof = +(* match proofbit with *) +(* | BasicProof _ -> do_build_proof proof *) +(* | proofbit -> *) + match proof with + | ProofGoalBlock (pb, eq) -> + do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq)) +(* let _, proof, _, _, _ = eq in *) +(* let newproof = replace_proof proofbit proof in *) +(* do_build_proof newproof *) + +(* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *) +(* let eqproof' = replace_proof proofbit eqproof in *) +(* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *) + | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *) + + and replace_proof newproof = function + | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> + let uri = eq_URI in +(* if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *) +(* HelmLibraryObjects.Logic.eq_ind_r_URI *) +(* else *) +(* HelmLibraryObjects.Logic.eq_ind_URI *) +(* in *) + let eqproof' = replace_proof newproof eqproof in + ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof') +(* ProofBlock (subst, eq_URI, t', poseq, newproof) *) + | ProofGoalBlock (pb, equality) -> + let pb' = replace_proof newproof pb in + ProofGoalBlock (pb', equality) +(* let w, proof, t, menv, args = equality in *) +(* let proof' = replace_proof newproof proof in *) +(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *) + | BasicProof _ -> newproof + | p -> p + in + let _, proof, _, _, _ = equality in + do_build_proof proof +;; + + let rec metas_of_term = function | Cic.Meta (i, c) -> [i] | Cic.Var (_, ens) @@ -161,8 +289,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 @@ -202,6 +330,7 @@ let meta_convertibility t1 t2 = ;; +(* let replace_metas (* context *) term = let module C = Cic in let rec aux = function @@ -244,8 +373,10 @@ let replace_metas (* context *) term = in aux term ;; +*) +(* let restore_metas (* context *) term = let module C = Cic in let rec aux = function @@ -284,47 +415,281 @@ let restore_metas (* context *) term = 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 + | Cic.Const _ -> true + | Cic.MutInd (_, _, []) -> true + | Cic.MutConstruct (_, _, _, []) -> 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 = + 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 = + let s = match s with C.Meta _ -> lookup s subst | _ -> s + and t = match t with C.Meta _ -> lookup t subst | _ -> t + in + 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), t -> ( + try + 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 = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *) + subst, menv + with CicUtil.Meta_not_found m -> + let names = names_of_context context in + debug_print ( + Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m + (CicPp.pp t1 names) (CicPp.pp t2 names) + (print_metasenv menv) (print_metasenv metasenv)); + assert false + ) + | _, 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 Invalid_argument _ -> + raise (U.UnificationFailure "Inference.unification.unif") + ) + | _, _ -> raise (U.UnificationFailure "Inference.unification.unif") + in + let subst, menv = unif [] metasenv t1 t2 in + let menv = + List.filter + (fun (m, _, _) -> + try let _ = List.find (fun (i, _) -> m = i) subst in false + with Not_found -> true) + menv + in + 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 ( + debug_print ( + Printf.sprintf "NOT SIMPLE TERMS: %s %s" + (CicPp.ppterm t1) (CicPp.ppterm t2)); + 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 Invalid_argument _ -> +(* 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 = - try - let subst, metasenv, ugraph = - CicUnification.fo_unif 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 +(* 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 *) +(* Printf.printf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2); *) +(* print_newline (); *) + 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 + | CicUnification.UnificationFailure _ + | CicUnification.Uncertain _ -> +(* Printf.printf "failed to match %s %s\n" *) +(* (CicPp.ppterm t1) (CicPp.ppterm t2); *) +(* print_endline (Printexc.to_string e); *) + 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" *) @@ -613,11 +978,11 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) (* 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 + with + | MatchingFailure + | CicUnification.UnificationFailure _ + | CicUnification.Uncertain _ -> + res, lifted_term in (* Printf.printf "exit aux\n"; *) retval @@ -655,10 +1020,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) (* 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 = @@ -677,22 +1038,14 @@ 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 *) - Utils.comparison) * (* ordering *) - 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 let module T = CicTypeChecker in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in + let ok_types ty menv = + List.for_all (fun (_, _, mt) -> mt = ty) menv + in let rec aux index newmeta = function | [] -> [], newmeta | (Some (_, C.Decl (term)))::tl -> @@ -700,17 +1053,9 @@ 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 - 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 + let (head, newmetas, args, newmeta) = + ProofEngineHelpers.saturate_term newmeta [] + context (S.lift index term) 0 in let p = if List.length args = 0 then @@ -719,17 +1064,31 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = C.Appl ((C.Rel index)::args) in ( match head with - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> - Printf.printf "OK: %s\n" (CicPp.ppterm term); + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) -> + debug_print ( + Printf.sprintf "OK: %s" (CicPp.ppterm term)); +(* debug_print ( *) +(* Printf.sprintf "args: %s\n" *) +(* (String.concat ", " (List.map CicPp.ppterm args))); *) +(* debug_print ( *) +(* Printf.sprintf "newmetas:\n%s\n" *) +(* (print_metasenv newmetas)); *) let o = !Utils.compare_terms t1 t2 in - Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1) + 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 -> + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when UriManager.eq uri eq_uri -> 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) + 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 @@ -746,17 +1105,128 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; -let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) = +let equations_blacklist = + List.fold_left + (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s) + UriManager.UriSet.empty [ + "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; + "cic:/Coq/Init/Logic/trans_eq.con"; + "cic:/Coq/Init/Logic/f_equal.con"; + "cic:/Coq/Init/Logic/f_equal2.con"; + "cic:/Coq/Init/Logic/f_equal3.con"; + "cic:/Coq/Init/Logic/sym_eq.con"; +(* "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *) +(* "cic:/Coq/Init/Peano/mult_n_Sm.con"; *) + + (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`... + perche' questo cacchio di teorema rompe le scatole :'( *) + "cic:/Rocq/SUBST/comparith/mult_n_2.con"; + ] +;; + +let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = + let module C = Cic in + let module S = CicSubstitution in + let module T = CicTypeChecker in + let candidates = + List.fold_left + (fun l uri -> + let suri = UriManager.string_of_uri uri in + if UriManager.UriSet.mem uri equations_blacklist then + l + else + let t = CicUtil.term_of_uri uri in + let ty, _ = + CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph + in + (t, ty)::l) + [] + (MetadataQuery.equations_for_goal ~dbd status) + in + let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI + and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in + let iseq uri = + (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2) + in + let ok_types ty menv = + List.for_all (fun (_, _, mt) -> mt = ty) menv + in + let rec aux newmeta = function + | [] -> [], newmeta + | (term, termty)::tl -> + debug_print ( + Printf.sprintf "Examining: %s (%s)" + (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)); + let res, newmeta = + match termty with + | C.Prod (name, s, t) -> + let head, newmetas, args, newmeta = + ProofEngineHelpers.saturate_term newmeta [] context termty 0 + in + let p = + if List.length args = 0 then + term + else + C.Appl (term::args) + in ( + match head with + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when (iseq uri) && (ok_types ty newmetas) -> + debug_print ( + Printf.sprintf "OK: %s" (CicPp.ppterm term)); + 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 iseq uri -> + let o = !Utils.compare_terms t1 t2 in + let w = compute_equality_weight ty t1 t2 in + let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in + Some e, (newmeta+1) + | _ -> None, newmeta + in + match res with + | Some e -> + let tl, newmeta' = aux newmeta tl in + e::tl, max newmeta newmeta' + | None -> + aux newmeta tl + in + let found, maxm = aux maxmeta candidates in + (List.fold_left + (fun l e -> + if List.exists (meta_convertibility_eq e) l then ( + debug_print ( + Printf.sprintf "NO!! %s already there!" (string_of_equality e)); + l + ) + else e::l) + [] found), maxm +;; + + +let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = +(* print_endline ("fix_metas " ^ (string_of_int newmeta)); *) let table = Hashtbl.create (List.length args) in - let newargs, _ = + let is_this_case = ref false in + let newargs, newmeta = List.fold_right (fun t (newargs, index) -> match t with | Cic.Meta (i, l) -> Hashtbl.add table i index; +(* if index = 5469 then ( *) +(* Printf.printf "?5469 COMES FROM (%d): %s\n" *) +(* i (string_of_equality equality); *) +(* print_newline (); *) +(* is_this_case := true *) +(* ); *) ((Cic.Meta (index, l))::newargs, index+1) | _ -> assert false) - args ([], newmeta) + args ([], newmeta+1) in let repl where = ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs @@ -781,17 +1251,82 @@ let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) = List.filter (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs in - (newmeta + (List.length newargs) + 1, - (repl proof, (ty, left, right, o), menv', newargs)) + let rec fix_proof = function + | NoProof -> NoProof + | BasicProof term -> BasicProof (repl term) + | ProofBlock (subst, eq_URI, t', (pos, eq), p) -> + +(* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *) +(* (string_of_equality equality) (print_subst subst); *) + + let subst' = + List.fold_left + (fun s arg -> + match arg with + | Cic.Meta (i, l) -> ( + try + let j = Hashtbl.find table i in + if List.mem_assoc i subst then + s + else +(* let _, context, ty = CicUtil.lookup_meta j menv' in *) +(* (i, (context, Cic.Meta (j, l), ty))::s *) + let _, context, ty = CicUtil.lookup_meta i menv in + (i, (context, Cic.Meta (j, l), ty))::s + with Not_found -> s + ) + | _ -> assert false) + [] args + in +(* let subst'' = *) +(* List.map *) +(* (fun (i, e) -> *) +(* try let j = Hashtbl.find table i in (j, e) *) +(* with _ -> (i, e)) subst *) +(* in *) + +(* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *) +(* print_newline (); *) + + ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p) +(* | ProofSymBlock (ens, p) -> *) +(* let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *) +(* ProofSymBlock (ens', fix_proof p) *) + | p -> assert false + in +(* (newmeta + (List.length newargs) + 2, *) + let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in +(* if !is_this_case then ( *) +(* print_endline "\nTHIS IS THE TROUBLE!!!"; *) +(* let pt = build_proof_term neweq in *) +(* Printf.printf "equality: %s\nproof: %s\n" *) +(* (string_of_equality neweq) (CicPp.ppterm pt); *) +(* print_endline (String.make 79 '-'); *) +(* ); *) + (newmeta + 1, neweq) +(* (w, fix_proof p, (ty, left, right, o), menv', newargs)) *) +;; + + +let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term = + let iseq uri = UriManager.eq uri eq_uri in + match term with + | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true + | _ -> false ;; 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 -> +let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term = + let iseq uri = UriManager.eq uri eq_uri in + match term with + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> let o = !Utils.compare_terms t1 t2 in - (proof, (ty, t1, t2, o), [], []) + 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 ;; @@ -800,6 +1335,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 @@ -1001,22 +1537,17 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = (!maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))) ;; +*) let is_identity ((_, context, ugraph) as env) = function - | ((_, (ty, left, right, _), _, _) as equality) -> - let res = - (left = right || - (fst (CicReduction.are_convertible context left right ugraph))) - in -(* if res then ( *) -(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *) -(* print_newline (); *) -(* ); *) - res + | ((_, _, (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 @@ -1214,6 +1745,7 @@ let subsumption env target source = ); res ;; +*) let extract_differing_subterms t1 t2 = @@ -1236,3 +1768,5 @@ let extract_differing_subterms t1 t2 = | hd::[] -> Some hd | _ -> None ;; + +