X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.ml;h=4beaab5c1e3d668a6ca10460dd9027fa8b8e3a9c;hb=4d0ef1046012225b44ee5a1768265c52e534109f;hp=6b87de349ce7f2225b54835e968b6cb54c7d6463;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml index 6b87de349..4beaab5c1 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 @@ -113,15 +113,15 @@ let compare_goal_list proof goal1 goal2 = 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,7 @@ 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,7 +195,7 @@ 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 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 @@ -215,7 +216,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,7 +230,7 @@ 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); @@ -260,7 +261,7 @@ let types_for_equality metasenv goal = (fun (i,acc) _ -> let ty, _ = CicTypeChecker.type_of_aux' - metasenv context (Cic.Rel i) CicUniv.empty_ugraph in + 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 @@ -272,10 +273,11 @@ let signature_of metasenv goal = 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 set metasenv context + close_with_constructors (close_with_types set metasenv context) + metasenv context -let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal = +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 @@ -288,20 +290,20 @@ let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal = let uris = Constr.UriManagerSet.fold (fun u acc -> - prerr_endline ("processing "^(UriManager.string_of_uri u)); + 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 *) - (prerr_endline "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 - prerr_endline ("tyl: "^(String.concat "\n" - (List.map UriManager.string_of_uri tyl))); + 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 = @@ -310,7 +312,7 @@ let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal = acc @ uris) acc tfe) else - (prerr_endline "normal treatment"; + (debug_print (lazy "normal treatment"); let uris = sigmatch ~dbd ~facts:false ~where:`Statement (Some (u,[]),set_for_sigmatch) @@ -334,7 +336,7 @@ 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" ^ @@ -393,7 +395,7 @@ 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) = + ~(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)) = @@ -424,7 +426,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 @@ -475,7 +478,7 @@ 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, _subst, _, _, _) = proof in