+ debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
+ (* debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names)); *)
+ debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
+ debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
+ false
+ end
+ else true
+;;
+
+let assert_proof_is_valid proof metasenv context goalty =
+ assert (check_proof_is_valid proof metasenv context goalty)
+;;
+
+let assert_subst_are_disjoint subst subst' =
+ if debug then
+ assert(List.for_all
+ (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
+ subst)
+ else ()
+;;
+
+let split_goals_in_prop metasenv subst gl =
+ List.partition
+ (fun g ->
+ let _,context,ty = CicUtil.lookup_meta g metasenv in
+ try
+ let sort,u = typeof ~subst metasenv context ty ugraph in
+ is_propositional context sort
+ with
+ | CicTypeChecker.AssertFailure s
+ | CicTypeChecker.TypeCheckerFailure s ->
+ debug_print
+ (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
+ debug_print s;
+ false)
+ (* FIXME... they should type! *)
+ gl
+;;
+
+let split_goals_with_metas metasenv subst gl =
+ List.partition
+ (fun g ->
+ let _,context,ty = CicUtil.lookup_meta g metasenv in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ CicUtil.is_meta_closed ty)
+ gl
+;;
+
+let order_new_goals metasenv subst open_goals ppterm =
+ let prop,rest = split_goals_in_prop metasenv subst open_goals in
+ let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
+ let closed_type, open_type = split_goals_with_metas metasenv subst rest in
+ let open_goals =
+ (List.map (fun x -> x,P) (open_prop @ closed_prop))
+ @
+ (List.map (fun x -> x,T) (open_type @ closed_type))
+ in
+ let tys =
+ List.map
+ (fun (i,sort) ->
+ let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
+ in
+ debug_print (lazy (" OPEN: "^
+ String.concat "\n"
+ (List.map
+ (function
+ | (i,t,P) -> string_of_int i ^ ":"^ppterm t^ "Prop"
+ | (i,t,T) -> string_of_int i ^ ":"^ppterm t^ "Type")
+ tys)));
+ open_goals
+;;
+
+let is_an_equational_goal = function
+ | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
+ | _ -> false
+;;
+
+type auto_params = Cic.term list * (string * string) list
+
+let elems = ref [] ;;
+
+(* closing a term w.r.t. its metavariables
+ very naif version: it does not take dependencies properly into account *)
+
+let naif_closure ?(prefix_name="xxx_") t metasenv context =
+ let in_term t (i,_,_) =
+ List.exists (fun (j,_) -> j=i) (CicUtil.metas_of_term t)
+ in
+ let metasenv = List.filter (in_term t) metasenv in
+ let metasenv = ProofEngineHelpers.sort_metasenv metasenv in
+ let n = List.length metasenv in
+ let what = List.map (fun (i,cc,ty) -> Cic.Meta(i,[])) metasenv in
+ let _,with_what =
+ List.fold_left
+ (fun (i,acc) (_,cc,ty) -> (i-1,Cic.Rel i::acc))
+ (n,[]) metasenv
+ in
+ let t = CicSubstitution.lift n t in
+ let body =
+ ProofEngineReduction.replace_lifting
+ ~equality:(fun c t1 t2 ->
+ match t1,t2 with
+ | Cic.Meta(i,_),Cic.Meta(j,_) -> i = j
+ | _ -> false)
+ ~context ~what ~with_what ~where:t
+ in
+ let _, t =
+ List.fold_left
+ (fun (n,t) (_,cc,ty) ->
+ n-1, Cic.Lambda(Cic.Name (prefix_name^string_of_int n),
+ CicSubstitution.lift n ty,t))
+ (n-1,body) metasenv
+ in
+ t, List.length metasenv
+;;
+
+let lambda_close ?prefix_name t menv ctx =
+ let t, num_lambdas = naif_closure ?prefix_name t menv ctx in
+ List.fold_left
+ (fun (t,i) -> function
+ | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
+ | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
+ | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1)
+ (t,num_lambdas) ctx
+;;
+
+(* functions for retrieving theorems *)
+
+
+exception FillingFailure of AutoCache.cache * AutomationCache.tables
+
+let rec unfold context = function
+ | Cic.Prod(name,s,t) ->
+ let t' = unfold ((Some (name,Cic.Decl s))::context) t in
+ Cic.Prod(name,s,t')
+ | t -> ProofEngineReduction.unfold context t
+
+let find_library_theorems dbd proof goal =
+ let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
+ let terms = List.map CicUtil.term_of_uri univ in
+ List.map
+ (fun t ->
+ (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph)))
+ terms
+
+let find_context_theorems context metasenv =
+ let l,_ =
+ List.fold_left
+ (fun (res,i) ctxentry ->
+ match ctxentry with
+ | Some (_,Cic.Decl t) ->
+ (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
+ | Some (_,Cic.Def (_,t)) ->
+ (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
+ | None -> res,i+1)
+ ([],1) context
+ in l
+
+let rec is_an_equality = function
+ | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
+ when (LibraryObjects.is_eq_URI uri) -> true
+ | Cic.Prod (_, _, t) -> is_an_equality t
+ | _ -> false
+;;
+
+let partition_equalities =
+ List.partition (fun (_,ty) -> is_an_equality ty)
+
+
+let default_auto tables _ cache _ _ _ _ = [],cache,tables ;;
+
+(* giusto per provare che succede
+let is_unit_equation context metasenv oldnewmeta term =
+ let head, metasenv, args, newmeta =
+ TermUtil.saturate_term oldnewmeta metasenv context term 0
+ in
+ let newmetas =
+ List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
+ in
+ Some (args,metasenv,newmetas,head,newmeta) *)
+
+let is_unit_equation context metasenv oldnewmeta term =
+ let head, metasenv, args, newmeta =
+ TermUtil.saturate_term oldnewmeta metasenv context term 0
+ in
+ let propositional_args =
+ HExtlib.filter_map
+ (function
+ | Cic.Meta(i,_) ->
+ let _,_,mt = CicUtil.lookup_meta i metasenv in
+ let sort,u =
+ CicTypeChecker.type_of_aux' metasenv context mt
+ CicUniv.oblivion_ugraph
+ in
+ if is_propositional context sort then Some i else None
+ | _ -> assert false)
+ args
+ in
+ if propositional_args = [] then
+ let newmetas =
+ List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
+ in
+ Some (args,metasenv,newmetas,head,newmeta)
+ else None
+;;
+
+let get_candidates skip_trie_filtering universe cache t =
+ let t = if skip_trie_filtering then Cic.Meta(0,[]) else t in
+ let candidates=
+ (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
+ in
+ let debug_msg =
+ (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
+ (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
+ debug_print debug_msg;
+ candidates
+;;
+
+let only signature context metasenv t =
+ try
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
+ in
+ let consts = MetadataConstraints.constants_of ty in
+ let b = MetadataConstraints.UriManagerSet.subset consts signature in
+(* if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b) *)
+ if b then b
+ else
+ let ty' = unfold context ty in
+ let consts' = MetadataConstraints.constants_of ty' in
+ let b = MetadataConstraints.UriManagerSet.subset consts' signature in
+(*
+ if not b then prerr_endline ("filtering " ^ (CicPp.ppterm t))
+ else prerr_endline ("keeping " ^ (CicPp.ppterm t));
+*)
+ b
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> assert false
+ | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
+;;
+
+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 dont_filter signature universe cache context metasenv =
+ match LibraryObjects.eq_URI() with
+ | None -> []
+ | Some eq_uri ->
+ let eq_uri = UriManager.strip_xpointer eq_uri in
+ let fake= Cic.Meta(-1,[]) in
+ let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
+ let candidates = get_candidates false universe cache fake_eq in
+ if dont_filter then candidates
+ else let eq_uri = UriManager.uri_of_uriref eq_uri 0 None in
+ (* let candidates = List.filter not_default_eq_term candidates in *)
+ List.filter
+ (only (MetadataConstraints.UriManagerSet.add eq_uri signature)
+ context metasenv) candidates
+
+let build_equality bag head args proof newmetas =
+ match head with
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
+ let p =
+ if args = [] then proof else Cic.Appl (proof::args)
+ in
+ let o = !Utils.compare_terms t1 t2 in
+ let stat = (ty,t1,t2,o) in
+ (* let w = compute_equality_weight stat in *)
+ let w = 0 in
+ let proof = Equality.Exact p in
+ let bag, e = Equality.mk_equality bag (w, proof, stat, newmetas) in
+ (* to clean the local context of metas *)
+ Equality.fix_metas bag e
+ | _ -> assert false
+;;
+
+let partition_unit_equalities context metasenv newmeta bag equations =
+ List.fold_left
+ (fun (bag,units,other,maxmeta)(t,ty) ->
+ if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
+ let _ =
+ HLog.warn
+ ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
+ ^ " since it is not meta closed")
+ in
+ bag, units,(t,ty)::other,maxmeta
+ else
+ match is_unit_equation context metasenv maxmeta ty with
+ | Some (args,metasenv,newmetas,head,newmeta') ->
+ let bag, equality =
+ build_equality bag head args t newmetas in
+ bag, equality::units,other,maxmeta
+ | None ->
+ bag, units,(t,ty)::other,maxmeta)
+ (bag,[],[],newmeta) equations
+;;
+
+let init_cache_and_tables
+ ?dbd ~use_library ~use_context
+ automation_cache restricted_univ (proof, goal)
+=
+ let _, metasenv, _, _, _, _ = proof in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ if restricted_univ = [] then
+ let ct =
+ if use_context then find_context_theorems context metasenv else []
+ in
+ let lt =
+ match use_library, dbd with
+ | true, Some dbd -> find_library_theorems dbd metasenv goal
+ | _ -> []
+ in
+ let cache = AutoCache.cache_empty in
+ let cache = cache_add_list cache context (ct@lt) in
+ let tables =
+ let env = metasenv, context, CicUniv.oblivion_ugraph in
+ List.fold_left
+ (fun (a,p,b) (t,ty) ->
+ let mes = CicUtil.metas_of_term ty in
+ Saturation.add_to_active b a p env ty t
+ (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv))
+ automation_cache.AutomationCache.tables ct
+ in
+(* AutomationCache.pp_cache { automation_cache with AutomationCache.tables =
+ * tables }; *)
+ automation_cache.AutomationCache.univ, tables, cache
+ else
+ let metasenv, t_ty, s_t_ty, _ =
+ List.fold_left
+ (fun (metasenv,acc, sacc, maxmeta) t ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux'
+ metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+ in
+ let head, metasenv, args, maxmeta =
+ TermUtil.saturate_term maxmeta metasenv context ty 0
+ in
+ let st = if args = [] then t else Cic.Appl (t::args) in
+ metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
+ (metasenv, [],[], CicMkImplicit.new_meta metasenv []) restricted_univ
+ in
+ let automation_cache = AutomationCache.empty () in
+ let automation_cache =
+ let universe = automation_cache.AutomationCache.univ in
+ let universe =
+ Universe.index_list universe context t_ty
+ in
+ { automation_cache with AutomationCache.univ = universe }
+ in
+ let automation_cache =
+ List.fold_left
+ (fun c (t,ty) ->
+ AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
+ automation_cache s_t_ty
+ in
+(* AutomationCache.pp_cache automation_cache; *)
+ automation_cache.AutomationCache.univ,
+ automation_cache.AutomationCache.tables,
+ cache_add_list cache_empty context t_ty
+;;
+ (*
+(* let signature = MetadataQuery.signature_of metasenv goal in *)
+(* let newmeta = CicMkImplicit.new_meta metasenv [] in *)
+ let equations =
+ retrieve_equations dont_filter (* true *) signature universe cache context metasenv
+ in
+ debug_print
+ (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
+ let eqs_and_types =
+ HExtlib.filter_map
+ (fun t ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux'
+ metasenv context t CicUniv.oblivion_ugraph
+ in
+ (* retrieve_equations could also return flexible terms *)
+ if is_an_equality ty then Some(t,ty)
+ else
+ try
+ let ty' = unfold context ty in
+ if is_an_equality ty' then Some(t,ty') else None
+ with ProofEngineTypes.Fail _ -> None)
+ equations
+ in
+ let bag = Equality.mk_equality_bag () in
+ let units, other_equalities, newmeta =
+ partition_unit_equalities context metasenv newmeta bag eqs_and_types