X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=a0cf2bb2180674e1ce5c03856189c88ce643567c;hb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;hp=09a0234575e2dc918d116500ea80ba4f981b403e;hpb=758dbd74dccfb2491b59e4267600caf1d485e77a;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 09a023457..a0cf2bb21 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -373,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 @@ -413,8 +415,9 @@ let restore_metas (* context *) term = in aux term ;; +*) - +(* let rec restore_subst (* context *) subst = List.map (fun (i, (c, t, ty)) -> @@ -438,6 +441,8 @@ let rec is_simple_term = function | Cic.Meta (i, l) -> check_irl 1 l | Cic.Rel _ -> true | Cic.Const _ -> true + | Cic.MutInd (_, _, []) -> true + | Cic.MutConstruct (_, _, _, []) -> true | _ -> false ;; @@ -475,7 +480,7 @@ let unification_simple metasenv context t1 t2 ugraph = | 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") + raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in @@ -487,24 +492,24 @@ let unification_simple metasenv context t1 t2 ugraph = subst, menv with CicUtil.Meta_not_found m -> let names = names_of_context context in - debug_print ( + debug_print (lazy ( 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)); + (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") + raise (U.UnificationFailure (U.failure_msg_of_string "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 (U.failure_msg_of_string "Inference.unification.unif")) ) - | _, _ -> raise (U.UnificationFailure "Inference.unification.unif") + | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) in let subst, menv = unif [] metasenv t1 t2 in let menv = @@ -521,9 +526,12 @@ let unification_simple metasenv context t1 t2 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 + if not (is_simple_term t1) || not (is_simple_term t2) then ( + debug_print (lazy ( + Printf.sprintf "NOT SIMPLE TERMS: %s %s" + (CicPp.ppterm t1) (CicPp.ppterm t2))); CicUnification.fo_unif metasenv context t1 t2 ugraph - else + ) else unification_simple metasenv context t1 t2 ugraph in let rec fix_term = function @@ -1047,7 +1055,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *) let (head, newmetas, args, newmeta) = ProofEngineHelpers.saturate_term newmeta [] - context (S.lift index term) + context (S.lift index term) 0 in let p = if List.length args = 0 then @@ -1058,14 +1066,14 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match head with | 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 ( *) + debug_print (lazy ( + Printf.sprintf "OK: %s" (CicPp.ppterm term))); +(* debug_print (lazy ( *) (* Printf.sprintf "args: %s\n" *) -(* (String.concat ", " (List.map CicPp.ppterm args))); *) -(* debug_print ( *) +(* (String.concat ", " (List.map CicPp.ppterm args)))); *) +(* debug_print (lazy ( *) (* Printf.sprintf "newmetas:\n%s\n" *) -(* (print_metasenv newmetas)); *) +(* (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 @@ -1109,6 +1117,10 @@ let equations_blacklist = "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"; ] ;; @@ -1119,6 +1131,7 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = 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 @@ -1141,14 +1154,14 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = let rec aux newmeta = function | [] -> [], newmeta | (term, termty)::tl -> - debug_print ( + debug_print (lazy ( Printf.sprintf "Examining: %s (%s)" - (CicPp.ppterm term) (CicPp.ppterm termty)); + (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 + ProofEngineHelpers.saturate_term newmeta [] context termty 0 in let p = if List.length args = 0 then @@ -1159,8 +1172,8 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = 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)); + debug_print (lazy ( + 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 @@ -1182,7 +1195,16 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = | None -> aux newmeta tl in - aux maxmeta candidates + let found, maxm = aux maxmeta candidates in + (List.fold_left + (fun l e -> + if List.exists (meta_convertibility_eq e) l then ( + debug_print (lazy ( + Printf.sprintf "NO!! %s already there!" (string_of_equality e))); + l + ) + else e::l) + [] found), maxm ;;