open AutoTypes;;
open AutoCache;;
-let debug_print s = prerr_endline (Lazy.force s);;
+let debug = false;;
+let debug_print s =
+ if debug then () else prerr_endline (Lazy.force s);;
(* functions for retrieving theorems *)
;;
let get_candidates universe cache t =
- let candidates =
+ let candidates=
(Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
in
let debug_msg =
candidates
;;
-let only singature context t =
+let only signature context t =
try
let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
let consts = MetadataConstraints.constants_of ty in
- MetadataConstraints.UriManagerSet.subset consts singature
+ let b = MetadataConstraints.UriManagerSet.subset consts signature in
+ if b then b
+ else
+ try
+ let ty' = unfold context ty in
+ let consts' = MetadataConstraints.constants_of ty' in
+ MetadataConstraints.UriManagerSet.subset consts' signature
+ with _-> false
with _ -> false
;;
+let not_default_eq_term t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ not (LibraryObjects.in_eq_URIs uri)
+ with Invalid_argument _ -> true
+
let retrieve_equations signature universe cache context=
match LibraryObjects.eq_URI() with
| None -> []
let fake= Cic.Meta(-1,[]) in
let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
let candidates = get_candidates universe cache fake_eq in
- List.filter (only signature context) candidates
+ (* defaults eq uris are built-in in auto *)
+ let candidates = List.filter not_default_eq_term candidates in
+ let candidates = List.filter (only signature context) candidates in
+ List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates;
+ candidates
let build_equality bag head args proof newmetas maxmeta =
match head with
Saturation.make_passive [],
Equality.mk_equality_bag)
-let init_cache_and_tables dbd use_library universe (proof, goal) =
+let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
(* the local cache in initially empty *)
let cache = AutoCache.cache_empty in
let _, metasenv, _, _ = proof in
let newmeta = CicMkImplicit.new_meta metasenv [] in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let ct = find_context_theorems context metasenv in
+ prerr_endline
+ ("ho trovato nel contesto " ^ (string_of_int (List.length ct)));
let lt =
if use_library then
- find_library_theorems dbd metasenv goal
+ find_library_theorems dbd metasenv goal
else [] in
- (* all equations are added to the cache *)
prerr_endline
("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
- (* let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in *)
let cache = cache_add_list cache context (ct@lt) in
- let equations = retrieve_equations signature universe cache context in
+ let equations =
+ retrieve_equations signature universe cache context in
prerr_endline
("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
let eqs_and_types =
let no = List.length units in
let active = Saturation.make_active [] in
let active,passive,newmeta =
- Saturation.pump_actives context bag newmeta active passive (no+1) infinity
+ if paramod then active,passive,newmeta
+ else
+ Saturation.pump_actives
+ context bag newmeta active passive (no+1) infinity
in
(active,passive,bag),cache,newmeta
in
match
let (active, passive,bag), cache, maxmeta =
- init_cache_and_tables dbd flags.use_library universe (proof'''',newmeta)
+ init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta)
in
Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
max_int max_int flags.timeout
let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
;;
+
let assert_proof_is_valid proof metasenv context goalty =
- let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
- let b,_ = CicReduction.are_convertible context ty goalty u in
- if not b then
+ if debug then
begin
- let names =
- List.map (function None -> None | Some (x,_) -> Some x) context
- in
- prerr_endline ("PROOF:" ^ CicPp.pp proof names);
- prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
- prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
- prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
- end;
- assert b
+ let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
+ let b,_ = CicReduction.are_convertible context ty goalty u in
+ if not b then
+ begin
+ let names =
+ List.map (function None -> None | Some (x,_) -> Some x) context
+ in
+ prerr_endline ("PROOF:" ^ CicPp.pp proof names);
+ prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
+ prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
+ prerr_endline ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
+ end;
+ assert b
+ end
+ else ()
;;
+
let assert_subst_are_disjoint subst subst' =
- assert(List.for_all
- (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
- subst)
+ if debug then
+ assert(List.for_all
+ (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
+ subst)
+ else ()
;;
+
let sort_new_elems =
List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
;;
in
debug_print (lazy (" OK: " ^ ppterm cand));
let metasenv = CicRefine.pack_coercion_metasenv metasenv in
- assert (maxmeta >= maxm);
- (*FIXME:sicuro che posso @?*)
assert_subst_are_disjoint subst subst';
let subst = subst@subst' in
let open_goals = order_new_goals metasenv subst open_goals ppterm in
else
match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
| Fail s, tables, cache, maxm' ->
- assert(maxm' >= maxm);let maxm = maxm' in
+ let maxm = maxm' in
debug_print
(lazy
(" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
in
aux flags tables maxm cache tl
| Success (metasenv,subst,others), tables, cache, maxm' ->
- assert(maxm' >= maxm);let maxm = maxm' in
+ let maxm = maxm' in
(* others are alternatives in OR *)
try
let goal = Cic.Meta(goalno,irl) in
Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
tables,cache,maxm(*FAILURE(depth)*)
| Succeded t ->
- assert(List.for_all (fun (i,_) -> i <> goalno) subst);
let entry = goalno, (cc, t,goalty) in
assert_subst_are_disjoint subst [entry];
let subst = entry :: subst in
let elems,tables,cache,maxm1, flags =
equational_case tables maxm cache
depth fake_proof goalno goalty subst context flags in
- assert(maxm1 >= maxm);
let maxm = maxm1 in
let more_elems, tables, cache, maxm1 =
if flags.use_only_paramod then
applicative_case
tables maxm depth subst fake_proof goalno
goalty metasenv context universe cache in
- assert(maxm1 >= maxm);
let maxm = maxm1 in
elems@more_elems, tables, cache, maxm, flags
else
(* just for testing *)
let use_library = flags.use_library in
let tables,cache,newmeta =
- init_cache_and_tables dbd use_library universe (proof, goal) in
+ init_cache_and_tables dbd use_library flags.use_only_paramod
+ universe (proof, goal) in
let tables,cache,newmeta =
if flags.close_more then
close_more
let initgoal = [], [], ty in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
- init_cache_and_tables dbd true Universe.empty (proof,goal) in
+ init_cache_and_tables dbd true true Universe.empty (proof,goal) in
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let table =
projects / helm.git / commitdiff