X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.ml;h=6db568cb4ab9ad60516bc30f1a0d366e4e6a7b1f;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=246df0838ab36706b112b72659b7f0ea86d1e9bb;hpb=44b999cf4e56f792cf4db5b2b7fce588735f1e4e;p=helm.git diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml index 246df0838..6db568cb4 100644 --- a/helm/software/components/tactics/metadataQuery.ml +++ b/helm/software/components/tactics/metadataQuery.ml @@ -51,11 +51,11 @@ let signature_of_hypothesis context metasenv = try let ty,_ = CicTypeChecker.type_of_aux' - metasenv current_ctx t CicUniv.empty_ugraph + metasenv current_ctx t CicUniv.oblivion_ugraph in let sort,_ = CicTypeChecker.type_of_aux' - metasenv current_ctx ty CicUniv.empty_ugraph + metasenv current_ctx ty CicUniv.oblivion_ugraph in let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in match sort with @@ -109,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 @@ -129,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 @@ -150,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 @@ -162,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 @@ -171,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) @@ -194,8 +196,8 @@ let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch' (* used only by te old auto *) -let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = - let (_, metasenv, _, _) = proof in +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 metasenv in @@ -215,7 +217,7 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = let is_predicate u = let ty, _ = try CicTypeChecker.type_of_aux' [] [] - (CicUtil.term_of_uri u) CicUniv.empty_ugraph + (CicUtil.term_of_uri u) CicUniv.oblivion_ugraph with CicTypeChecker.TypeCheckerFailure _ -> assert false in let rec check_last_pi = function @@ -229,49 +231,98 @@ let is_predicate u = 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.empty_ugraph in + 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;*) +(* + 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 universe_of_goals ~(dbd:HMysql.dbd) proof goals = - let (_, metasenv, _, _) = proof in - let add_uris_for acc goal = - let (_, context, ty) = CicUtil.lookup_meta goal metasenv in - let main, sig_constants = Constr.signature_of ty in - let set = signature_of_hypothesis context metasenv in - let set = - match main with - None -> set - | Some (main,l) -> - List.fold_right Constr.UriManagerSet.add (main::l) set in - let set = Constr.UriManagerSet.union set sig_constants in - let all_constants_closed = close_with_types set metasenv context in - Constr.UriManagerSet.union all_constants_closed acc - in - let all_constants_closed = - List.fold_left add_uris_for Constr.UriManagerSet.empty goals in +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 - prerr_endline ("FOO!1"); let uris = Constr.UriManagerSet.fold (fun u acc -> - let uris = - sigmatch ~dbd ~facts:false ~where:`Statement - (Some (u,[]),all_constants_closed) - in - acc @ uris) + 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 - prerr_endline ("FOO!2"); (* let uris = sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) @@ -279,15 +330,16 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals = *) let uris = List.filter nonvar (List.map snd uris) in let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in - let uris = List.filter (only all_constants_closed) uris in - uris + 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:HMysql.dbd) ?signature ((proof, goal) as _status) = +let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) = (* let to_string set = "{\n" ^ @@ -297,7 +349,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = ^ "\n}" in *) - let (_, metasenv, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let main, sig_constants = match signature with @@ -346,8 +398,8 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = (* 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 @@ -377,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 @@ -428,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