X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=746a2faead0fcfc567e2d8c6a1dd45231c8be509;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=1252c6069cd3664a492c52b0c6a358127a99f3be;hpb=b24260fd5c00791ad04042405e3942f288f54ab2;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 1252c6069..746a2faea 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -330,6 +330,7 @@ let meta_convertibility t1 t2 = ;; +(* let replace_metas (* context *) term = let module C = Cic in let rec aux = function @@ -420,6 +421,7 @@ let rec restore_subst (* context *) subst = i, (c, restore_metas (* context *) t, ty)) subst ;; +*) let rec check_irl start = function @@ -435,6 +437,7 @@ let rec is_simple_term = function | Cic.Appl l -> List.for_all is_simple_term l | Cic.Meta (i, l) -> check_irl 1 l | Cic.Rel _ -> true + | Cic.Const _ -> true | _ -> false ;; @@ -455,9 +458,6 @@ let unification_simple metasenv context t1 t2 ugraph = 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 @@ -467,57 +467,32 @@ let unification_simple metasenv context t1 t2 ugraph = | _ -> 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 (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") @@ -526,25 +501,19 @@ let unification_simple metasenv context t1 t2 ugraph = List.fold_left2 (fun (subst', menv) s t -> unif subst' menv s t) (subst, menv) tls tlt - with e -> + with Invalid_argument _ -> 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 *) + 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 ;; @@ -641,7 +610,7 @@ let matching_simple metasenv context t1 t2 ugraph = List.fold_left2 (fun (subst, menv) s t -> do_match subst menv s t) (subst, menv) ls lt - with e -> + with Invalid_argument _ -> (* print_endline (Printexc.to_string e); *) (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *) (* print_newline (); *) @@ -668,6 +637,8 @@ let matching metasenv context t1 t2 ugraph = (* (\* 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 *) @@ -690,9 +661,12 @@ let matching metasenv context t1 t2 ugraph = (* print_newline (); *) subst, metasenv, ugraph - with e -> + 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 ;; @@ -708,8 +682,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) 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" *) @@ -998,11 +970,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 @@ -1040,10 +1012,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 = @@ -1067,6 +1035,9 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = 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 -> @@ -1085,8 +1056,16 @@ 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 let w = compute_equality_weight ty t1 t2 in let proof = BasicProof p in @@ -1094,7 +1073,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = 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 @@ -1117,22 +1097,46 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; -let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta = +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"; *) + ] +;; + +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.map - (fun uri -> - let t = CicUtil.term_of_uri uri in - let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - t, ty) + List.fold_left + (fun l uri -> + 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 = - uri == eq_uri1 || uri == eq_uri2 + (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 @@ -1141,7 +1145,7 @@ let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta = match termty with | C.Prod (name, s, t) -> let head, newmetas, args, newmeta = - ProofEngineHelpers.saturate_term newmeta [] [] termty + ProofEngineHelpers.saturate_term newmeta [] context termty in let p = if List.length args = 0 then @@ -1150,8 +1154,10 @@ let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta = C.Appl (term::args) in ( match head with - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> - Printf.printf "OK: %s\n" (CicPp.ppterm term); + | 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 @@ -1242,7 +1248,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = (* (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 _ -> s + with Not_found -> s ) | _ -> assert false) [] args @@ -1277,10 +1283,20 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = ;; +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 let w = compute_equality_weight ty t1 t2 in let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in