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
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
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
(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
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
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)
*)
let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
let cmatch' = Constr.cmatch'
-
+
+(* 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 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
+ 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
+ uris
+
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
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)
*)
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" ^
(String.concat "\n"
(fun u l -> (" "^UriManager.string_of_uri u)::l) set []))
^ "\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
(* 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
| 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
(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
projects / helm.git / blobdiff