From ef5e2e1726e24e4523ee28ead5d7796498192692 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Jun 2006 16:52:45 +0000 Subject: [PATCH] fixed equalities_for_goal --- components/tactics/metadataQuery.ml | 76 ++++++++++++++++++++++------ components/tactics/metadataQuery.mli | 4 +- 2 files changed, 63 insertions(+), 17 deletions(-) diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml index 8822c527c..a5c387971 100644 --- a/components/tactics/metadataQuery.ml +++ b/components/tactics/metadataQuery.ml @@ -38,15 +38,35 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) -let signature_of_hypothesis context = - List.fold_left - (fun set hyp -> - match hyp with - | None -> set - | Some (_, Cic.Decl t) - | Some (_, Cic.Def (t, _)) -> - Constr.UriManagerSet.union set (Constr.constants_of t)) - Constr.UriManagerSet.empty context +let signature_of_hypothesis context metasenv = + let set, _ = + List.fold_right + (fun hyp (set,current_ctx) -> + match hyp with + | None -> set, hyp::current_ctx + | Some (_, Cic.Decl t) -> + Constr.UriManagerSet.union set (Constr.constants_of t), + hyp::current_ctx + | Some (_, Cic.Def (t, _)) -> + try + let ty,_ = + CicTypeChecker.type_of_aux' + metasenv current_ctx t CicUniv.empty_ugraph + in + let sort,_ = + CicTypeChecker.type_of_aux' + metasenv current_ctx ty CicUniv.empty_ugraph + in + match sort with + | Cic.Sort Cic.Prop -> set, hyp::current_ctx + | _ -> Constr.UriManagerSet.union set (Constr.constants_of t), + hyp::current_ctx + with + | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx) + context (Constr.UriManagerSet.empty,[]) + in + set +;; let intersect uris siguris = let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in @@ -176,7 +196,7 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let main, sig_constants = Constr.signature_of ty in - let set = signature_of_hypothesis context in + let set = signature_of_hypothesis context metasenv in let set = match main with None -> set @@ -189,8 +209,26 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = let uris = List.filter nonvar (List.map snd uris) in let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in uris +;; + +let filter_predicate set ctx menv = + let is_predicate t = + let ty, _ = + try CicTypeChecker.type_of_aux' [] [] + (CicUtil.term_of_uri t) CicUniv.empty_ugraph + with CicTypeChecker.TypeCheckerFailure _ -> assert false + in + let rec check_last_pi = function + | Cic.Prod (_,_,tgt) -> check_last_pi tgt + | Cic.Sort Cic.Prop -> true + | _ -> false + in + not (check_last_pi ty) + in + Constr.UriManagerSet.filter is_predicate set +;; -let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = +let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = (* let to_string set = "{ " ^ (String.concat ", " @@ -200,7 +238,11 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = in *) let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in - let main, sig_constants = Constr.signature_of ty in + let main, sig_constants = + match signature with + | None -> Constr.signature_of ty + | Some s -> s + in (* Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *) (* match main with *) (* None -> raise Goal_is_not_an_equation *) @@ -216,15 +258,17 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = in match eq_URI,main with | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l - | _,_ -> [] + | _ -> [] in - Printf.printf "\nSome (m, l): %s, [%s]\n\n" + (*Printf.printf "\nSome (m, l): %s, [%s]\n\n" (UriManager.string_of_uri (List.hd l)) (String.concat "; " (List.map UriManager.string_of_uri (List.tl l))); + *) (* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *) - let set = signature_of_hypothesis context in + let set = signature_of_hypothesis context metasenv in (* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *) let set = Constr.UriManagerSet.union set sig_constants in + let set = filter_predicate set context metasenv in let set = close_with_types set metasenv context in (* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *) let set = close_with_constructors set metasenv context in @@ -261,7 +305,7 @@ let experimental_hint let all_constants = let hyp_and_sug = Constr.UriManagerSet.union - (signature_of_hypothesis context) + (signature_of_hypothesis context metasenv) sig_constants in let main = diff --git a/components/tactics/metadataQuery.mli b/components/tactics/metadataQuery.mli index b65a23fa9..0fa4a01df 100644 --- a/components/tactics/metadataQuery.mli +++ b/components/tactics/metadataQuery.mli @@ -32,7 +32,9 @@ val signature_of_goal: dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list val equations_for_goal: - dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list + dbd:HMysql.dbd -> + ?signature:MetadataConstraints.term_signature -> + ProofEngineTypes.status -> UriManager.uri list val experimental_hint: dbd:HMysql.dbd -> -- 2.39.2