X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.ml;h=6db568cb4ab9ad60516bc30f1a0d366e4e6a7b1f;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=b9c0536538e4295726347b7ad82071e1c89ed160;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml index b9c053653..6db568cb4 100644 --- a/helm/software/components/tactics/metadataQuery.ml +++ b/helm/software/components/tactics/metadataQuery.ml @@ -38,15 +38,36 @@ 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.oblivion_ugraph + in + let sort,_ = + CicTypeChecker.type_of_aux' + metasenv current_ctx ty CicUniv.oblivion_ugraph + in + let set = Constr.UriManagerSet.union set(Constr.constants_of ty)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 @@ -88,19 +109,19 @@ let filter_uris_backward ~dbd ~facts signature uris = intersect uris siguris let compare_goal_list proof goal1 goal2 = - let _,metasenv,_,_ = proof in + let _,metasenv, _subst, _,_, _ = proof in let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in let ty_sort1,_ = - CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph in let ty_sort2,_ = - CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.oblivion_ugraph in let prop1 = let b,_ = CicReduction.are_convertible - ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph + ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.oblivion_ugraph in if b then 0 else 1 @@ -108,7 +129,7 @@ let compare_goal_list proof goal1 goal2 = let prop2 = let b,_ = CicReduction.are_convertible - ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph + ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.oblivion_ugraph in if b then 0 else 1 @@ -129,7 +150,7 @@ let close_with_types s metasenv context = (fun e bag -> let t = CicUtil.term_of_uri e in let ty, _ = - CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph in Constr.UriManagerSet.union bag (Constr.constants_of ty)) s s @@ -141,7 +162,7 @@ let close_with_constructors s metasenv context = match t with Cic.MutInd (uri,_,_) | Cic.MutConstruct (uri,_,_,_) -> - (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with Cic.InductiveDefinition(tl,_,_,_) -> snd (List.fold_left @@ -150,6 +171,8 @@ let close_with_constructors s metasenv context = List.fold_left (fun (j,s) _ -> let curi = UriManager.uri_of_uriref uri i (Some j) in +(* prerr_endline ("adding " ^ + * (UriManager.string_of_uri curi)); *) j+1,Constr.UriManagerSet.add curi s) (1,s) cl in (i+1,s)) (0,bag) tl) | _ -> assert false) @@ -172,11 +195,12 @@ let cmatch' = let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch' -let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = - let (_, metasenv, _, _) = proof in +(* used only by te old auto *) +let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) = + let (_, metasenv, _subst, _, _, _) = 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 @@ -190,54 +214,192 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in uris -let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = -(* let to_string set = - "{ " ^ - (String.concat ", " +let is_predicate u = + let ty, _ = + try CicTypeChecker.type_of_aux' [] [] + (CicUtil.term_of_uri u) CicUniv.oblivion_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 + check_last_pi ty +;; + +let only constants uri = + prerr_endline (UriManager.string_of_uri uri); + let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *) + let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in + let consts = Constr.constants_of ty in +(* + prerr_endline ("XXX " ^ UriManager.string_of_uri uri); + Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^ + UriManager.string_of_uri u)) consts; + Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^ + UriManager.string_of_uri u)) constants;*) + Constr.UriManagerSet.subset consts constants +;; + +let rec types_of_equality = function + | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _] + when (LibraryObjects.is_eq_URI uri) -> + let uri_set = Constr.constants_of ty in + if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then + Constr.SetSet.empty + else Constr.SetSet.singleton uri_set + | Cic.Prod (_, s, t) -> + Constr.SetSet.union (types_of_equality s) (types_of_equality t) + | _ -> Constr.SetSet.empty +;; + +let types_for_equality metasenv goal = + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let all = types_of_equality ty in + let _, all = + List.fold_left + (fun (i,acc) _ -> + let ty, _ = + CicTypeChecker.type_of_aux' + metasenv context (Cic.Rel i) CicUniv.oblivion_ugraph in + let newty = types_of_equality ty in + (i+1,Constr.SetSet.union newty acc)) + (1,all) context + in all +;; + +let signature_of metasenv goal = + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let ty_set = Constr.constants_of ty in + let hyp_set = signature_of_hypothesis context metasenv in + let set = Constr.UriManagerSet.union ty_set hyp_set in + close_with_types + (close_with_constructors (close_with_types set metasenv context) + metasenv context) + metasenv context + + +let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal = + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let ty_set = Constr.constants_of ty in + let hyp_set = signature_of_hypothesis context metasenv in + let set = Constr.UriManagerSet.union ty_set hyp_set in + let all_constants_closed = close_with_types set metasenv context in + (* we split predicates from the rest *) + let predicates, rest = + Constr.UriManagerSet.partition is_predicate all_constants_closed + in + let uris = + Constr.UriManagerSet.fold + (fun u acc -> + debug_print (lazy ("processing "^(UriManager.string_of_uri u))); + let set_for_sigmatch = + Constr.UriManagerSet.remove u all_constants_closed in + if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then + (* equality has a special treatment *) + (debug_print (lazy "special treatment"); + let tfe = + Constr.SetSet.elements (types_for_equality metasenv goal) + in + List.fold_left + (fun acc l -> + let tyl = Constr.UriManagerSet.elements l in + debug_print (lazy ("tyl: "^(String.concat "\n" + (List.map UriManager.string_of_uri tyl)))); + let set_for_sigmatch = + Constr.UriManagerSet.diff set_for_sigmatch l in + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement + (Some (u,tyl),set_for_sigmatch) in + acc @ uris) + acc tfe) + else + (debug_print (lazy "normal treatment"); + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement + (Some (u,[]),set_for_sigmatch) + in + acc @ uris)) + predicates [] + in +(* + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) + in +*) + let uris = List.filter nonvar (List.map snd uris) in + let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in + if apply_only then + List.filter (only all_constants_closed) uris + else uris +;; + +let filter_out_predicate set ctx menv = + Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set +;; + +let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) = +(* + let to_string set = + "{\n" ^ + (String.concat "\n" (Constr.UriManagerSet.fold - (fun u l -> (UriManager.string_of_uri u)::l) set [])) - ^ " }" - in *) - let (_, metasenv, _, _) = proof in + (fun u l -> (" "^UriManager.string_of_uri u)::l) set [])) + ^ "\n}" + in +*) + let (_, metasenv, _subst, _, _, _) = 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 *) (* | Some (m,l) -> *) - let m, l = + let l = let eq_URI = - let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in - UriManager.uri_of_string (us ^ "#xpointer(1/1)") + match LibraryObjects.eq_URI () with + None -> None + | Some s -> + Some + (UriManager.uri_of_string + (UriManager.string_of_uri s ^ "#xpointer(1/1)")) in - match main with - | None -> eq_URI, [] - | Some (m, l) when UriManager.eq m eq_URI -> m, l - | Some (m, l) -> eq_URI, [] + 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" - (UriManager.string_of_uri m) - (String.concat "; " (List.map UriManager.string_of_uri l)); + (*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_out_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 (* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *) - let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in + let set_for_sigmatch = List.fold_right Constr.UriManagerSet.remove l set in let uris = - sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in + sigmatch ~dbd ~facts:false ~where:`Statement (main,set_for_sigmatch) in let uris = List.filter nonvar (List.map snd uris) in let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in + let set = List.fold_right Constr.UriManagerSet.add l set in + let uris = List.filter (only set) uris in uris (* ) *) (* else raise Goal_is_not_an_equation *) let experimental_hint - ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = - let (_, metasenv, _, _) = proof in + ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let (uris, (main, sig_constants)) = match signature with @@ -258,7 +420,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 = @@ -267,7 +429,8 @@ let experimental_hint | Some (main,_) -> let ty, _ = CicTypeChecker.type_of_aux' - metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph + metasenv context (CicUtil.term_of_uri main) + CicUniv.oblivion_ugraph in Constr.constants_of ty in @@ -318,10 +481,10 @@ let experimental_hint (aux uris) let new_experimental_hint - ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe + ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe ((proof, goal) as status) = - let (_, metasenv, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let (uris, (main, sig_constants)) = match signature with