fixed metadataquery so that only are calculated without the DB (but are calculated)
removed is_meta_convertible left right in is_weak_identity
added extra dependencies between gcd < relevant_equations < ord to make
paramodulation happy. In the past this used to be the order used by make.
added an hack in applys.ma, since it used to work due to convertibility.
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 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 predicates, rest =
Constr.UriManagerSet.partition is_predicate all_constants_closed
in
+ prerr_endline ("FOO!1");
let uris =
Constr.UriManagerSet.fold
(fun u acc ->
acc @ uris)
predicates []
in
+ prerr_endline ("FOO!2");
(*
let uris =
sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed)
;;
let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
-(* let to_string set =
- "{ " ^
- (String.concat ", "
+ let to_string set =
+ "{\n" ^
+ (String.concat "\n"
(Constr.UriManagerSet.fold
- (fun u l -> (UriManager.string_of_uri u)::l) set []))
- ^ " }"
- in *)
+ (fun u l -> (" "^UriManager.string_of_uri u)::l) set []))
+ ^ "\n}"
+ in
let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants =
(* 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 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 is_identity (_, context, ugraph) eq =
let _,_,(ty,left,right,_),menv,_ = open_equality eq in
(* doing metaconv here is meaningless *)
- fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+ left = right
+(* fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+ * *)
;;
let module T = CicTypeChecker in
let _,metasenv,_,_ = proof in
let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
- let use_auto, auto =
+ let auto =
match auto with
- | None -> false, default_auto
- | Some auto -> true, auto in
+ | None -> default_auto
+ | Some auto -> auto in
(* if use_auto is true, we try to close the hypothesis of equational
statements using auto; a naif, and probably wrong approach *)
let rec aux cache index newmeta = function
(Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
let do_find context term =
match term with
- | C.Prod (name, s, t) when (is_an_equality t && use_auto) ->
+ | C.Prod (name, s, t) when is_an_equality t ->
(try
let term = S.lift index term in
let saturated,cache,newmeta =
let candidates = List.map utty_of_u eqs in
let candidates = List.filter is_monomorphic_eq candidates in
let candidates = List.filter is_var_free candidates in
- let use_auto, auto =
+ let auto =
match auto with
- | None -> false, default_auto
- | Some auto -> true, auto in
+ | None -> default_auto
+ | Some auto -> auto in
(* if use_auto is true, we try to close the hypothesis of equational
statements using auto; a naif, and probably wrong approach *)
let rec aux cache newmeta = function
(CicPp.ppterm term) (CicPp.ppterm termty)));
let res, newmeta, cache =
match termty with
- | C.Prod (name, s, t) when use_auto ->
+ | C.Prod (name, s, t) ->
(try
let saturated,cache,newmeta =
close_hypothesis_of_term context metasenv newmeta termty
eqs, newmeta , cache
with AutoFailure (cache,newmeta) ->
[], newmeta , cache)
- | C.Prod _ -> [], newmeta, cache
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
[e], newmeta+1, cache
include "datatypes/constructors.ma".
include "nat/exp.ma".
include "nat/gcd.ma".
+include "nat/relevant_equations.ma". (* required by auto paramod *)
(* this definition of log is based on pairs, with a remainder *)
include "nat/times.ma".
include "nat/minus.ma".
+include "nat/gcd.ma".
+(* if gcd is compiled before this, the applys will take too much *)
theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p.
intros.
theorem prova2 :
\forall n. S n \divides (S n)!.
intros.
-(* o fare una List.rev quando si fa la make_passives... la tira su,
- ma tardi....
+(* se non trova subito sym_times poi si perde! *)
+(* alternativamente si puo' abilitare la are_convertible nella
+ is_identity, ma poi va peggio nel resto (conv lunghe) *)
letin www \def sym_times.
clearbody www.
-*)
applyS (witness ? ? ? (refl_eq ? ?)).
qed.
projects / helm.git / commitdiff