-(* Copyright (C) 2002, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-open AutoTypes;;
-open AutoCache;;
-
-let debug = false;;
-let debug_print s =
- if debug then prerr_endline (Lazy.force s);;
-
-
-let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
-let ugraph = CicUniv.oblivion_ugraph;;
-let typeof = CicTypeChecker.type_of_aux';;
-let ppterm ctx t =
- let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
- CicPp.pp t names
-;;
-
-let is_propositional context sort =
- match CicReduction.whd context sort with
- | Cic.Sort Cic.Prop
- | Cic.Sort (Cic.CProp _) -> true
- | _-> false
-;;
-
-let is_in_prop context subst metasenv ty =
- let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
- is_propositional context sort
-;;
-
-exception NotConvertible;;
-
-let check_proof_is_valid proof metasenv context goalty =
- if debug then
- begin
- try
- let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in
- let b,_ = CicReduction.are_convertible context ty goalty u in
- if not b then raise NotConvertible else b
- with _ ->
- let names =
- List.map (function None -> None | Some (x,_) -> Some x) context
- in
- 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 option * (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, subst, _, _, _ = proof in
- let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let add_list_to_tables metasenv subst automation_cache ct =
- List.fold_left
- (fun automation_cache (t,_) ->
- AutomationCache.add_term_to_active automation_cache
- metasenv subst context t None)
- automation_cache ct
- in
- match restricted_univ with
- | None ->
- 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 automation_cache =
- add_list_to_tables metasenv subst automation_cache ct
- in
-(* AutomationCache.pp_cache automation_cache; *)
- automation_cache.AutomationCache.univ,
- automation_cache.AutomationCache.tables,
- cache
- | Some restricted_univ ->
- let t_ty =
- List.map
- (fun t ->
- let ty, _ = CicTypeChecker.type_of_aux'
- metasenv ~subst:[] context t CicUniv.oblivion_ugraph
- in
- t, ty)
- restricted_univ
- in
- (* let automation_cache = AutomationCache.empty () in *)
- let automation_cache =
- let universe = Universe.empty in
- let universe =
- Universe.index_list universe context t_ty
- in
- { automation_cache with AutomationCache.univ = universe }
- in
- let ct =
- if use_context then find_context_theorems context metasenv else t_ty
- in
- let automation_cache =
- add_list_to_tables metasenv subst automation_cache ct
- in
- (* AutomationCache.pp_cache automation_cache; *)
- automation_cache.AutomationCache.univ,
- automation_cache.AutomationCache.tables,
- cache_empty
-;;
-
-let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast =
- let actives, passives, bag = tables in
- let bag, head, metasenv, args =
- Equality.saturate_term bag metasenv subst context term
- in
- let tables = actives, passives, bag 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
- let results,cache,tables =
- if propositional_args = [] then
- let _,_,bag = tables in
- let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in
- [args,metasenv,newmetas,head],cache,tables
- else
- (*
- let proof =
- None,metasenv,term,term (* term non e' significativo *)
- in *)
- let flags =
- if fast then
- {AutoTypes.default_flags() with
- AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
- maxwidth = 2;maxdepth = 2;
- use_paramod=true;use_only_paramod=false}
- else
- {AutoTypes.default_flags() with
- AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
- maxwidth = 2;maxdepth = 4;
- use_paramod=true;use_only_paramod=false}
- in
- match auto tables universe cache context metasenv propositional_args flags with
- | [],cache,tables -> raise (FillingFailure (cache,tables))
- | substs,cache,tables ->
- let actives, passaives, bag = tables in
- let bag, res =
- List.fold_right
- (fun subst (bag,acc) ->
- let metasenv =
- CicMetaSubst.apply_subst_metasenv subst metasenv
- in
- let head = CicMetaSubst.apply_subst subst head in
- let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in
- let args = List.map (CicMetaSubst.apply_subst subst) args in
- let newm = CicMkImplicit.new_meta metasenv subst in
- let bag = Equality.push_maxmeta bag newm in
- bag, ((args,metasenv,newmetas,head) :: acc))
- substs (bag,[])
- in
- let tables = actives, passives, bag in
- res, cache, tables
- in
- results,cache,tables
-;;
-
-let build_equalities auto context metasenv subst tables universe cache equations =
- List.fold_left
- (fun (tables,facts,cache) (t,ty) ->
- (* in any case we add the equation to the cache *)
- let cache = AutoCache.cache_add_list cache context [(t,ty)] in
- try
- let saturated, cache, tables =
- fill_hypothesis context metasenv subst ty tables universe cache auto true
- in
- let eqs, tables =
- List.fold_left
- (fun (acc, tables) (args,metasenv,newmetas,head) ->
- let actives, passives, bag = tables in
- let bag, equality =
- build_equality bag head args t newmetas
- in
- let tables = actives, passives, bag in
- equality::acc,tables)
- ([],tables) saturated
- in
- (tables, eqs@facts, cache)
- with FillingFailure (cache,tables) ->
- (* if filling hypothesis fails we add the equation to
- the cache *)
- (tables,facts,cache)
- )
- (tables,[],cache) equations
-
-let close_more tables context status auto signature universe cache =
- let proof, goalno = status in
- let _, metasenv,subst,_,_, _ = proof in
- let equations =
- retrieve_equations false signature universe cache context metasenv
- in
- 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 None)
- equations in
- let tables, units, cache =
- build_equalities auto context metasenv subst tables universe cache eqs_and_types
- in
- let active,passive,bag = tables in
- let passive = Saturation.add_to_passive units passive in
- let no = List.length units in
- let active, passive, bag =
- Saturation.pump_actives context bag active passive (no+1) infinity
- in
- (active,passive,bag), cache
-;;
-
-let find_context_equalities dbd tables context proof (universe:Universe.universe) cache
-=
- let module C = Cic in
- let module S = CicSubstitution in
- let module T = CicTypeChecker in
- let _,metasenv,subst,_,_, _ = proof 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 tables cache index = function
- | [] -> tables, [], cache
- | (Some (_, C.Decl (term)))::tl ->
- debug_print
- (lazy
- (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
- let do_find tables context term =
- match term with
- | C.Prod (name, s, t) when is_an_equality t ->
- (try
- let term = S.lift index term in
- let saturated, cache, tables =
- fill_hypothesis context metasenv subst term
- tables universe cache default_auto false
- in
- let actives, passives, bag = tables in
- let bag,eqs =
- List.fold_left
- (fun (bag,acc) (args,metasenv,newmetas,head) ->
- let bag, equality =
- build_equality bag head args (Cic.Rel index) newmetas
- in
- bag, equality::acc)
- (bag,[]) saturated
- in
- let tables = actives, passives, bag in
- tables, eqs, cache
- with FillingFailure (cache,tables) ->
- tables, [], cache)
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
- when LibraryObjects.is_eq_URI uri ->
- let term = S.lift index term in
- let actives, passives, bag = tables in
- let bag, e =
- build_equality bag term [] (Cic.Rel index) []
- in
- let tables = actives, passives, bag in
- tables, [e], cache
- | _ -> tables, [], cache
- in
- let tables, eqs, cache = do_find tables context term in
- let tables, rest, cache = aux tables cache (index+1) tl in
- tables, List.map (fun x -> index,x) eqs @ rest, cache
- | _::tl ->
- aux tables cache (index+1) tl
- in
- let tables, il, cache = aux tables cache 1 context in
- let indexes, equalities = List.split il in
- tables, indexes, equalities, cache
-;;
-
-(********** PARAMETERS PASSING ***************)
-
-let bool params name default =
- try
- let s = List.assoc name params in
- if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
- else if s = "0" || s = "false" || s = "no" || s= "off" then false
- else
- let msg = "Unrecognized value for parameter "^name^"\n" in
- let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
- raise (ProofEngineTypes.Fail (lazy msg))
- with Not_found -> default
-;;
-
-let string params name default =
- try List.assoc name params with
- | Not_found -> default
-;;
-
-let int params name default =
- try int_of_string (List.assoc name params) with
- | Not_found -> default
- | Failure _ ->
- raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
-;;
-
-let flags_of_params params ?(for_applyS=false) () =
- let int = int params in
- let bool = bool params in
- let close_more = bool "close_more" false in
- let use_paramod = bool "use_paramod" true in
- let skip_trie_filtering = bool "skip_trie_filtering" false in
- let skip_context = bool "skip_context" false in
- let use_only_paramod =
- if for_applyS then true else bool "paramodulation" false in
- let use_library = bool "library"
- ((AutoTypes.default_flags()).AutoTypes.use_library) in
- let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
- let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
- let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
- let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
- let do_type = bool "type" false in
- let timeout = int "timeout" 0 in
- { AutoTypes.maxdepth =
- if use_only_paramod then 2 else depth;
- AutoTypes.maxwidth = width;
- AutoTypes.maxsize = size;
- AutoTypes.timeout =
- if timeout = 0 then
- if for_applyS then Unix.gettimeofday () +. 30.0
- else
- infinity
- else
- Unix.gettimeofday() +. (float_of_int timeout);
- AutoTypes.use_library = use_library;
- AutoTypes.use_paramod = use_paramod;
- AutoTypes.use_only_paramod = use_only_paramod;
- AutoTypes.close_more = close_more;
- AutoTypes.dont_cache_failures = false;
- AutoTypes.maxgoalsizefactor = gsize;
- AutoTypes.do_types = do_type;
- AutoTypes.skip_trie_filtering = skip_trie_filtering;
- AutoTypes.skip_context = skip_context;
- }
-
-
-let eq_of_goal = function
- | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
- uri
- | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
-;;
-
-(* performs steps of rewrite with the universe, obtaining if possible
- * a trivial goal *)
-let solve_rewrite ~automation_cache ~params:(univ,params) (proof,goal)=
- let steps = int_of_string (string params "steps" "4") in
- let use_context = bool params "use_context" true in
- let universe, tables, cache =
- init_cache_and_tables ~use_library:false ~use_context
- automation_cache univ (proof,goal)
- in
- let actives, passives, bag = tables in
- let pa,metasenv,subst,pb,pc,pd = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- let context = CicMetaSubst.apply_subst_context subst context in
- let ty = CicMetaSubst.apply_subst subst ty in
- let eq_uri = eq_of_goal ty in
- let initgoal = [], metasenv, ty in
- let table =
- let equalities = (Saturation.list_of_passive passives) in
- List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities
- in
- let env = metasenv,context,CicUniv.oblivion_ugraph in
- debug_print (lazy ("demod to solve: " ^ CicPp.ppterm ty));
- match Indexing.solve_demodulating bag env table initgoal steps with
- | Some (bag, gproof, metasenv, sub_subst, proof) ->
- let subst_candidates,extra_infos =
- List.split
- (HExtlib.filter_map
- (fun (i,c,_) ->
- if i <> goal && c = context then Some (i,(c,ty)) else None)
- metasenv)
- in
- let proofterm,proto_subst =
- let proof = Equality.add_subst sub_subst proof in
- Equality.build_goal_proof
- bag eq_uri gproof proof ty subst_candidates context metasenv
- in
- let proofterm = Subst.apply_subst sub_subst proofterm in
- let extrasubst =
- HExtlib.filter_map
- (fun (i,((c,ty),t)) ->
- match t with
- | Cic.Meta (j,_) when i=j -> None
- | _ -> Some (i,(c,t,ty)))
- (List.combine subst_candidates
- (List.combine extra_infos proto_subst))
- in
- let subst = subst @ extrasubst in
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- let proofterm, _, metasenv,subst, _ =
- CicRefine.type_of metasenv subst context proofterm
- CicUniv.oblivion_ugraph
- in
- let status = (pa,metasenv,subst,pb,pc,pd), goal in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm) status
- | None ->
- raise
- (ProofEngineTypes.Fail (lazy
- ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
-;;
-
-(* Demodulate thorem *)
-let open_type ty bo =
- let rec open_type_aux context ty k args =
- match ty with
- | Cic.Prod (n,s,t) ->
- let n' =
- FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in
- let entry = match n' with
- | Cic.Name _ -> Some (n',(Cic.Decl s))
- | Cic.Anonymous -> None
- in
- open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args)
- | Cic.LetIn (n,s,sty,t) ->
- let entry = Some (n,(Cic.Def (s,sty)))
- in
- open_type_aux (entry::context) t (k+1) args
- | _ -> context, ty, args
- in
- let context, ty, args = open_type_aux [] ty 1 [] in
- match args with
- | [] -> context, ty, bo
- | _ -> context, ty, Cic.Appl (bo::args)
-;;
-
-let rec close_type bo ty context =
- match context with
- | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty)
- | Some (n,(Cic.Decl s))::tl ->
- close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl
- | Some (n,(Cic.Def (s,sty)))::tl ->
- close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl
- | _ -> assert false
-;;
-
-let is_subsumed univ context ty =
- let candidates = Universe.get_candidates univ ty in
- List.fold_left
- (fun res cand ->
- match res with
- | Some found -> Some found
- | None ->
- try
- let mk_irl =
- CicMkImplicit.identity_relocation_list_for_metavariable in
- let metasenv = [(0,context,ty)] in
- let fake_proof =
- None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[]
- in
- let (_,metasenv,subst,_,_,_), open_goals =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:cand)
- (fake_proof,0)
- in
- let prop_goals, other =
- split_goals_in_prop metasenv subst open_goals
- in
- if prop_goals = [] then Some cand else None
- with
- | ProofEngineTypes.Fail s -> None
- | CicUnification.Uncertain s -> None
- ) None candidates
-;;
-
-let demodulate_theorem ~automation_cache uri =
- let eq_uri =
- match LibraryObjects.eq_URI () with
- | Some (uri) -> uri
- | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
- let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- let context,ty,bo =
- match obj with
- | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[]))
- | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem"))
- in
- if CicUtil.is_closed ty then
- raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction")));
- let initgoal = [], [], ty in
- (* compute the signature *)
- let signature =
- let ty_set = MetadataConstraints.constants_of ty in
- let hyp_set = MetadataQuery.signature_of_hypothesis context [] in
- let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in
- MetadataQuery.close_with_types set [] context
- in
- (* retrieve equations from the universe universe *)
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let equations =
- retrieve_equations true signature universe AutoCache.cache_empty context []
- 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' [] 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 bag, units, _, newmeta =
- partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
- in
- let table =
- List.fold_left
- (fun tbl eq -> Indexing.index tbl eq)
- Indexing.empty units
- in
- let changed,(newproof,newmetasenv, newty) =
- Indexing.demod bag
- ([],context,CicUniv.oblivion_ugraph) table initgoal in
- if changed then
- begin
- let oldproof = Equality.Exact bo in
- let proofterm,_ =
- Equality.build_goal_proof (~contextualize:false) (~forward:true) bag
- eq_uri newproof oldproof ty [] context newmetasenv
- in
- if newmetasenv <> [] then
- raise (ProofEngineTypes.Fail (lazy ("metasenv not empty")))
- else
- begin
- assert_proof_is_valid proofterm newmetasenv context newty;
- match is_subsumed universe context newty with
- | Some t -> raise
- (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t)))
- | None -> close_type proofterm newty context
- end
- end
- else (* if newty = ty then *)
- raise (ProofEngineTypes.Fail (lazy "no progress"))
- (*else ProofEngineTypes.apply_tactic
- (ReductionTactics.simpl_tac
- ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
-;;
-
-
-(* NEW DEMODULATE *)
-let demodulate ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
- let universe, tables, cache =
- init_cache_and_tables
- ~dbd ~use_library:false ~use_context:true
- automation_cache univ (proof,goal)
- in
- let eq_uri =
- match LibraryObjects.eq_URI () with
- | Some (uri) -> uri
- | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
- let active, passive, bag = tables in
- let curi,metasenv,subst,pbo,pty, attrs = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let initgoal = [], metasenv, ty in
- let equalities = (Saturation.list_of_passive passive) in
- (* we demodulate using both actives passives *)
- let env = metasenv,context,CicUniv.empty_ugraph in
- debug_print (lazy ("PASSIVES:" ^ string_of_int(List.length equalities)));
- List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
- equalities;
- let table =
- List.fold_left
- (fun tbl eq -> Indexing.index tbl eq)
- (snd active) equalities
- in
- let changed,(newproof,newmetasenv, newty) =
- (* Indexing.demodulation_goal bag *)
- Indexing.demod bag
- (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
- in
- if changed then
- begin
- let maxm = CicMkImplicit.new_meta metasenv subst in
- let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
- let subst_candidates = List.map (fun (i,_,_) -> i) metasenv in
- let subst_candidates = List.filter (fun x-> x <> goal) subst_candidates in
- let proofterm, proto_subst =
- Equality.build_goal_proof (~contextualize:false) bag
- eq_uri newproof opengoal ty subst_candidates context metasenv
- in
- (* XXX understan what to do with proto subst *)
- let metasenv = (maxm,context,newty)::metasenv in
- let proofterm, _, metasenv, subst, _ =
- CicRefine.type_of metasenv subst context proofterm
- CicUniv.oblivion_ugraph
- in
- let extended_status = (curi,metasenv,subst,pbo,pty, attrs),goal in
- let proof,gl =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm) extended_status
- in
- proof,maxm::gl
- end
- else
- raise (ProofEngineTypes.Fail (lazy "no progress"))
-;;
-
-let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache =
- ProofEngineTypes.mk_tactic
- (fun status ->
- let all = bool flags "all" false in
- if all then
- solve_rewrite ~params ~automation_cache status
- else
- demodulate ~dbd ~params ~automation_cache status)
-;;
-(***************** applyS *******************)
-
-let apply_smart_aux
- dbd automation_cache (params:auto_params) proof goal newmeta' metasenv' subst
- context term' ty termty goal_arity
-=
- let consthead,newmetasenv,arguments,_ =
- TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
- let term'' =
- match arguments with
- | [] -> term'
- | _ -> Cic.Appl (term'::arguments)
- in
- let consthead =
- let rec aux t = function
- | [] ->
- let t = CicReduction.normalize ~delta:false context t in
- (match t, ty with
- | Cic.Appl (hd1::_), Cic.Appl (hd2::_) when hd1 <> hd2 ->
- let t = ProofEngineReduction.unfold context t in
- (match t with
- | Cic.Appl (hd1'::_) when hd1' = hd2 -> t
- | _ -> raise (ProofEngineTypes.Fail (lazy "incompatible head")))
- | _ -> t)
- | arg :: tl ->
- match CicReduction.whd context t with
- | Cic.Prod (_,_,tgt) ->
- aux (CicSubstitution.subst arg tgt) tl
- | _ -> assert false
- in
- aux termty arguments
- in
- let goal_for_paramod =
- match LibraryObjects.eq_URI () with
- | Some uri ->
- Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Implicit (Some `Type); consthead; ty]
- | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
- in
- try
- let goal_for_paramod, _, newmetasenv, subst, _ =
- CicRefine.type_of newmetasenv subst context goal_for_paramod
- CicUniv.oblivion_ugraph
- in
- let newmeta = CicMkImplicit.new_meta newmetasenv subst in
- let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
- let proof'' =
- let uri,_,_,p,ty, attrs = proof in
- uri,metasenv_for_paramod,subst,p,ty, attrs
- in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-(*
- prerr_endline ("------ prima di rewrite su ------ " ^ string_of_int goal);
- prerr_endline ("menv:\n"^CicMetaSubst.ppmetasenv [] metasenv_for_paramod);
- prerr_endline ("subst:\n"^CicMetaSubst.ppsubst
- ~metasenv:(metasenv_for_paramod)
- subst);
-*)
-
- let (proof''',goals) =
- ProofEngineTypes.apply_tactic
- (EqualityTactics.rewrite_tac ~direction:`RightToLeft
- ~pattern:(ProofEngineTypes.conclusion_pattern None)
- (Cic.Meta(newmeta,irl)) []) (proof'',goal)
- in
- let goal = match goals with [g] -> g | _ -> assert false in
- let proof'''', _ =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac term'')
- (proof''',goal)
- in
-
-
- let (_,m,_,_,_,_ as p) =
- let pu,metasenv,subst,proof,px,py = proof'''' in
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- let proof'''' = pu,metasenv,subst,proof,px,py in
- let univ, params = params in
- let use_context = bool params "use_context" true in
- let universe, (active,passive,bag), cache =
- init_cache_and_tables ~use_library:false ~use_context
- automation_cache univ (proof'''',newmeta)
- in
- match
- Saturation.solve_narrowing bag (proof'''',newmeta) active passive
- 2 (*0 infinity*)
- with
- | None, active, passive, bag ->
- raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
- | Some(subst',(pu,metasenv,_,proof,px, py),open_goals),active,
- passive,bag ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- pu,metasenv,subst,proof,px,py
- in
-
-(*
- let (_,m,_,_,_,_ as p),_ =
- solve_rewrite ~params ~automation_cache (proof'''',newmeta)
- in
-*)
-
- let open_goals =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv' ~newmetasenv:m
- in
- p, open_goals
- with
- CicRefine.RefineFailure msg ->
- raise (ProofEngineTypes.Fail msg)
-;;
-
-let apply_smart
- ~dbd ~term ~automation_cache ~params (proof, goal)
-=
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let module C = Cic in
- let (_,metasenv,subst,_,_, _) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = CicMkImplicit.new_meta metasenv subst in
- let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
- match term with
- C.Var (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Var (uri,exp_named_subst')
- | C.Const (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Const (uri,exp_named_subst')
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutInd (uri,tyno,exp_named_subst')
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutConstruct (uri,tyno,consno,exp_named_subst')
- | _ -> [],newmeta,[],term
- in
- let metasenv' = metasenv@newmetasenvfragment in
- let termty,_ =
- CicTypeChecker.type_of_aux'
- metasenv' ~subst context term' CicUniv.oblivion_ugraph
- in
- let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
- let goal_arity =
- let rec count_prods context ty =
- match CicReduction.whd ~subst context ty with
- | Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
- | _ -> 0
- in
- count_prods context ty
- in
- apply_smart_aux dbd automation_cache params proof goal
- newmeta' metasenv' subst context term' ty termty goal_arity
-;;
-
-let applyS_tac ~dbd ~term ~params ~automation_cache =
- ProofEngineTypes.mk_tactic
- (fun status ->
- try
- apply_smart ~dbd ~term ~params ~automation_cache status
- with
- | CicUnification.UnificationFailure msg
- | CicTypeChecker.TypeCheckerFailure msg ->
- raise (ProofEngineTypes.Fail msg))
-;;
-
-
-(****************** AUTO ********************)
-
-let calculate_timeout flags =
- if flags.timeout = 0. then
- (debug_print (lazy "AUTO WITH NO TIMEOUT");
- {flags with timeout = infinity})
- else
- flags
-;;
-let is_equational_case goalty flags =
- let ensure_equational t =
- if is_an_equational_goal t then true
- else false
- in
- (flags.use_paramod && is_an_equational_goal goalty) ||
- (flags.use_only_paramod && ensure_equational goalty)
-;;
-
-type menv = Cic.metasenv
-type subst = Cic.substitution
-type goal = ProofEngineTypes.goal * int * AutoTypes.sort
-let candidate_no = ref 0;;
-type candidate = int * Cic.term Lazy.t
-type cache = AutoCache.cache
-
-type fail =
- (* the goal (mainly for depth) and key of the goal *)
- goal * AutoCache.cache_key
-type op =
- (* goal has to be proved *)
- | D of goal
- (* goal has to be cached as a success obtained using candidate as the first
- * step *)
- | S of goal * AutoCache.cache_key * candidate * int
-type elem =
- (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
- menv * subst * int * op list * op list * fail list
-type status =
- (* list of computations that may lead to the solution: all op list will
- * end with the same (S(g,_)) *)
- elem list
-type auto_result =
- (* menv, subst, alternatives, tables, cache *)
- | Proved of menv * subst * elem list * AutomationCache.tables * cache
- | Gaveup of AutomationCache.tables * cache
-
-
-(* the status exported to the external observer *)
-type auto_status =
- (* context, (goal,candidate) list, and_list, history *)
- Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
- (int * Cic.term * int) list * Cic.term Lazy.t list
-
-let d_prefix l =
- let rec aux acc = function
- | (D g)::tl -> aux (acc@[g]) tl
- | _ -> acc
- in
- aux [] l
-;;
-let prop_only l =
- List.filter (function (_,_,P) -> true | _ -> false) l
-;;
-
-let d_goals l =
- let rec aux acc = function
- | (D g)::tl -> aux (acc@[g]) tl
- | (S _)::tl -> aux acc tl
- | [] -> acc
- in
- aux [] l
-;;
-
-let calculate_goal_ty (goalno,_,_) s m =
- try
- let _,cc,goalty = CicUtil.lookup_meta goalno m in
- (* XXX applicare la subst al contesto? *)
- Some (cc, CicMetaSubst.apply_subst s goalty)
- with CicUtil.Meta_not_found i when i = goalno -> None
-;;
-
-let calculate_closed_goal_ty (goalno,_,_) s =
- try
- let cc,_,goalty = List.assoc goalno s in
- (* XXX applicare la subst al contesto? *)
- Some (cc, CicMetaSubst.apply_subst s goalty)
- with Not_found ->
- None
-;;
-
-let pp_status ctx status =
- if debug then
- let names = Utils.names_of_context ctx in
- let pp x =
- let x =
- ProofEngineReduction.replace
- ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
- ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
- in
- CicPp.pp x names
- in
- let string_of_do m s (gi,_,_ as g) d =
- match calculate_goal_ty g s m with
- | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
- | None -> Printf.sprintf "D(%d, _, %d)" gi d
- in
- let string_of_s m su k (ci,ct) gi =
- Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
- in
- let string_of_ol m su l =
- String.concat " | "
- (List.map
- (function
- | D (g,d,s) -> string_of_do m su (g,d,s) d
- | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
- l)
- in
- let string_of_fl m s fl =
- String.concat " | "
- (List.map (fun ((i,_,_),ty) ->
- Printf.sprintf "(%d, %s)" i (pp ty)) fl)
- in
- let rec aux = function
- | [] -> ()
- | (m,s,_,_,ol,fl)::tl ->
- Printf.eprintf "< [%s] ;;; [%s]>\n"
- (string_of_ol m s ol) (string_of_fl m s fl);
- aux tl
- in
- Printf.eprintf "-------------------------- status -------------------\n";
- aux status;
- Printf.eprintf "-----------------------------------------------------\n";
-;;
-
-let auto_status = ref [] ;;
-let auto_context = ref [];;
-let in_pause = ref false;;
-let pause b = in_pause := b;;
-let cond = Condition.create ();;
-let mutex = Mutex.create ();;
-let hint = ref None;;
-let prune_hint = ref [];;
-
-let step _ = Condition.signal cond;;
-let give_hint n = hint := Some n;;
-let give_prune_hint hint =
- prune_hint := hint :: !prune_hint
-;;
-
-let check_pause _ =
- if !in_pause then
- begin
- Mutex.lock mutex;
- Condition.wait cond mutex;
- Mutex.unlock mutex
- end
-;;
-
-let get_auto_status _ =
- let status = !auto_status in
- let and_list,elems,last =
- match status with
- | [] -> [],[],[]
- | (m,s,_,don,gl,fail)::tl ->
- let and_list =
- HExtlib.filter_map
- (fun (id,d,_ as g) ->
- match calculate_goal_ty g s m with
- | Some (_,x) -> Some (id,x,d) | None -> None)
- (d_goals gl)
- in
- let rows =
- (* these are the S goalsin the or list *)
- let orlist =
- List.map
- (fun (m,s,_,don,gl,fail) ->
- HExtlib.filter_map
- (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
- (List.rev don @ gl))
- status
- in
- (* this function eats id from a list l::[id,x] returning x, l *)
- let eat_tail_if_eq id l =
- let rec aux (s, l) = function
- | [] -> s, l
- | ((id1,_,_),k1,c)::tl when id = id1 ->
- (match s with
- | None -> aux (Some c,l) tl
- | Some _ -> assert false)
- | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
- in
- let c, l = aux (None, []) l in
- c, List.rev l
- in
- let eat_in_parallel id l =
- let rec aux (b,eaten, new_l as acc) l =
- match l with
- | [] -> acc
- | l::tl ->
- match eat_tail_if_eq id l with
- | None, l -> aux (b@[false], eaten, new_l@[l]) tl
- | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
- in
- aux ([],[],[]) l
- in
- let rec eat_all rows l =
- match l with
- | [] -> rows
- | elem::or_list ->
- match List.rev elem with
- | ((to_eat,depth,_),k,_)::next_lunch ->
- let b, eaten, l = eat_in_parallel to_eat l in
- let eaten = HExtlib.list_uniq eaten in
- let eaten = List.rev eaten in
- let b = true (* List.hd (List.rev b) *) in
- let rows = rows @ [to_eat,k,b,depth,eaten] in
- eat_all rows l
- | [] -> eat_all rows or_list
- in
- eat_all [] (List.rev orlist)
- in
- let history =
- HExtlib.filter_map
- (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
- gl
- in
-(* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
- and_list, rows, history
- in
- !auto_context, elems, and_list, last
-;;
-
-(* Works if there is no dependency over proofs *)
-let is_a_green_cut goalty =
- CicUtil.is_meta_closed goalty
-;;
-let rec first_s = function
- | (D _)::tl -> first_s tl
- | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
- | [] -> None
-;;
-let list_union l1 l2 =
- (* TODO ottimizzare compare *)
- HExtlib.list_uniq (List.sort compare (l1 @ l1))
-;;
-let rec eq_todo l1 l2 =
- match l1,l2 with
- | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
- | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
- when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
- if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
- | [],[] -> true
- | _ -> false
-;;
-let eat_head todo id fl orlist =
- let rec aux acc = function
- | [] -> [], acc
- | (m, s, _, _, todo1, fl1)::tl as orlist ->
- let rec aux1 todo1 =
- match first_s todo1 with
- | None -> orlist, acc
- | Some (((gno,_,_),_,_,_), todo11) ->
- (* TODO confronto tra todo da ottimizzare *)
- if gno = id && eq_todo todo11 todo then
- aux (list_union fl1 acc) tl
- else
- aux1 todo11
- in
- aux1 todo1
- in
- aux fl orlist
-;;
-let close_proof p ty menv context =
- let metas =
- List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
- in
- let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
- naif_closure p menv context
-;;
-(* XXX capire bene quando aggiungere alla cache *)
-let add_to_cache_and_del_from_orlist_if_green_cut
- g s m cache key todo orlist fl ctx size minsize
-=
- let cache = cache_remove_underinspection cache key in
- (* prima per fare la irl usavamo il contesto vero e proprio e non quello
- * canonico! XXX *)
- match calculate_closed_goal_ty g s with
- | None -> assert false
- | Some (canonical_ctx , gty) ->
- let goalno,depth,sort = g in
- let irl = mk_irl canonical_ctx in
- let goal = Cic.Meta(goalno, irl) in
- let proof = CicMetaSubst.apply_subst s goal in
- let green_proof, closed_proof =
- let b = is_a_green_cut proof in
- if not b then
- b, (* close_proof proof gty m ctx *) proof
- else
- b, proof
- in
- debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
- if is_a_green_cut key then
- (* if the initia goal was closed, we cut alternatives *)
- let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
- let orlist, fl = eat_head todo goalno fl orlist in
- let cache =
- if size < minsize then
- (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
- else
- (* if the proof is closed we cache it *)
- if green_proof then cache_add_success cache key proof
- else (* cache_add_success cache key closed_proof *)
- (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
- in
- cache, orlist, fl, true
- else
- let cache =
- debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
- if size < minsize then
- (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
- (* if the substituted goal and the proof are closed we cache it *)
- if is_a_green_cut gty then
- if green_proof then cache_add_success cache gty proof
- else (* cache_add_success cache gty closed_proof *)
- (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
- else (*
- try
- let ty, _ =
- CicTypeChecker.type_of_aux' ~subst:s
- m ctx closed_proof CicUniv.oblivion_ugraph
- in
- if is_a_green_cut ty then
- cache_add_success cache ty closed_proof
- else cache
- with
- | CicTypeChecker.TypeCheckerFailure _ ->*)
- (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
- in
- cache, orlist, fl, false
-;;
-let close_failures (fl : fail list) (cache : cache) =
- List.fold_left
- (fun cache ((gno,depth,_),gty) ->
- if CicUtil.is_meta_closed gty then
- ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
- cache_add_failure cache gty depth)
- else
- cache)
- cache fl
-;;
-let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
- let entry = goalno, (canonical_ctx, t,ty) in
- assert_subst_are_disjoint subst [entry];
- let subst = entry :: subst in
-
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-
- subst, metasenv
-;;
-
-let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
- None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
-;;
-
-let equational_case
- tables cache depth fake_proof goalno goalty subst context
- flags
-=
- let active,passive,bag = tables in
- let ppterm = ppterm context in
- let status = (fake_proof,goalno) in
- if flags.use_only_paramod then
- begin
- debug_print (lazy ("PARAMODULATION SU: " ^
- string_of_int goalno ^ " " ^ ppterm goalty ));
- let goal_steps, saturation_steps, timeout =
- max_int,max_int,flags.timeout
- in
- match
- Saturation.given_clause bag status active passive
- goal_steps saturation_steps timeout
- with
- | None, active, passive, bag ->
- [], (active,passive,bag), cache, flags
- | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
- passive,bag ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- let open_goals =
- order_new_goals metasenv subst open_goals ppterm
- in
- let open_goals =
- List.map (fun (x,sort) -> x,depth-1,sort) open_goals
- in
- incr candidate_no;
- [(!candidate_no,proof),metasenv,subst,open_goals],
- (active,passive,bag), cache, flags
- end
- else
- begin
- debug_print (lazy ("NARROWING DEL GOAL: " ^
- string_of_int goalno ^ " " ^ ppterm goalty ));
- let goal_steps, saturation_steps, timeout =
- 1,0,flags.timeout
- in
- match
- Saturation.solve_narrowing bag status active passive goal_steps
- with
- | None, active, passive, bag ->
- [], (active,passive,bag), cache, flags
- | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
- passive,bag ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- let open_goals =
- order_new_goals metasenv subst open_goals ppterm
- in
- let open_goals =
- List.map (fun (x,sort) -> x,depth-1,sort) open_goals
- in
- incr candidate_no;
- [(!candidate_no,proof),metasenv,subst,open_goals],
- (active,passive,bag), cache, flags
- end
-(*
- begin
- let params = ([],["use_context","false"]) in
- let automation_cache = {
- AutomationCache.tables = tables ;
- AutomationCache.univ = Universe.empty; }
- in
- try
- let ((_,metasenv,subst,_,_,_),open_goals) =
-
- solve_rewrite ~params ~automation_cache
- (fake_proof, goalno)
- in
- let proof = lazy (Cic.Meta (-1,[])) in
- [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
- with ProofEngineTypes.Fail _ -> [], tables, cache, flags
-(*
- let res = Saturation.all_subsumed bag status active passive in
- let res' =
- List.map
- (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- let open_goals =
- order_new_goals metasenv subst open_goals ppterm
- in
- let open_goals =
- List.map (fun (x,sort) -> x,depth-1,sort) open_goals
- in
- incr candidate_no;
- (!candidate_no,proof),metasenv,subst,open_goals)
- res
- in
- res', (active,passive,bag), cache, flags
-*)
- end
-*)
-;;
-
-let sort_new_elems =
- List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
- let p1 = List.length (prop_only l1) in
- let p2 = List.length (prop_only l2) in
- if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
-;;
-
-
-let try_candidate dbd
- goalty tables subst fake_proof goalno depth context cand
-=
- let ppterm = ppterm context in
- try
- let actives, passives, bag = tables in
- let (_,metasenv,subst,_,_,_), open_goals =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:cand)
- (fake_proof,goalno)
- in
- let tables = actives, passives,
- Equality.push_maxmeta bag
- (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
- in
- debug_print (lazy (" OK: " ^ ppterm cand));
- let metasenv = CicRefine.pack_coercion_metasenv metasenv in
- let open_goals = order_new_goals metasenv subst open_goals ppterm in
- let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
- incr candidate_no;
- Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
- with
- | ProofEngineTypes.Fail s -> None,tables
- | CicUnification.Uncertain s -> None,tables
-;;
-
-let applicative_case dbd
- tables depth subst fake_proof goalno goalty metasenv context
- signature universe cache flags
-=
- (* let goalty_aux =
- match goalty with
- | Cic.Appl (hd::tl) ->
- Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
- | _ -> goalty
- in *)
- let goalty_aux = goalty in
- let candidates =
- get_candidates flags.skip_trie_filtering universe cache goalty_aux
- in
- (* if the goal is an equality we skip the congruence theorems
- let candidates =
- if is_equational_case goalty flags
- then List.filter not_default_eq_term candidates
- else candidates
- in *)
- let candidates = List.filter (only signature context metasenv) candidates
- in
- let tables, elems =
- List.fold_left
- (fun (tables,elems) cand ->
- match
- try_candidate dbd goalty
- tables subst fake_proof goalno depth context cand
- with
- | None, tables -> tables, elems
- | Some x, tables -> tables, x::elems)
- (tables,[]) candidates
- in
- let elems = sort_new_elems elems in
- elems, tables, cache
-;;
-
-let try_smart_candidate dbd
- goalty tables subst fake_proof goalno depth context cand
-=
- let ppterm = ppterm context in
- try
- let params = (None,[]) in
- let automation_cache = {
- AutomationCache.tables = tables ;
- AutomationCache.univ = Universe.empty; }
- in
- debug_print (lazy ("candidato per " ^ string_of_int goalno
- ^ ": " ^ CicPp.ppterm cand));
-(*
- let (_,metasenv,subst,_,_,_) = fake_proof in
- prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
- prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
-*)
- let ((_,metasenv,subst,_,_,_),open_goals) =
- apply_smart ~dbd ~term:cand ~params ~automation_cache
- (fake_proof, goalno)
- in
- let metasenv = CicRefine.pack_coercion_metasenv metasenv in
- let open_goals = order_new_goals metasenv subst open_goals ppterm in
- let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
- incr candidate_no;
- Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
- with
- | ProofEngineTypes.Fail s -> None,tables
- | CicUnification.Uncertain s -> None,tables
-;;
-
-let smart_applicative_case dbd
- tables depth subst fake_proof goalno goalty metasenv context signature
- universe cache flags
-=
- let goalty_aux =
- match goalty with
- | Cic.Appl (hd::tl) ->
- Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
- | _ -> goalty
- in
- let smart_candidates =
- get_candidates flags.skip_trie_filtering universe cache goalty_aux
- in
- let candidates =
- get_candidates flags.skip_trie_filtering universe cache goalty
- in
- let smart_candidates =
- List.filter
- (fun x -> not(List.mem x candidates)) smart_candidates
- in
- let debug_msg =
- (lazy ("smart_candidates" ^ " = " ^
- (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
- debug_print debug_msg;
- let candidates = List.filter (only signature context metasenv) candidates in
- let smart_candidates =
- List.filter (only signature context metasenv) smart_candidates
- in
-(*
- let penalty cand depth =
- if only signature context metasenv cand then depth else ((prerr_endline (
- "penalizzo " ^ CicPp.ppterm cand));depth -1)
- in
-*)
- let tables, elems =
- List.fold_left
- (fun (tables,elems) cand ->
- match
- try_candidate dbd goalty
- tables subst fake_proof goalno depth context cand
- with
- | None, tables ->
- (* if normal application fails we try to be smart *)
- (match try_smart_candidate dbd goalty
- tables subst fake_proof goalno depth context cand
- with
- | None, tables -> tables, elems
- | Some x, tables -> tables, x::elems)
- | Some x, tables -> tables, x::elems)
- (tables,[]) candidates
- in
- let tables, smart_elems =
- List.fold_left
- (fun (tables,elems) cand ->
- match
- try_smart_candidate dbd goalty
- tables subst fake_proof goalno depth context cand
- with
- | None, tables -> tables, elems
- | Some x, tables -> tables, x::elems)
- (tables,[]) smart_candidates
- in
- let elems = sort_new_elems (elems @ smart_elems) in
- elems, tables, cache
-;;
-
-let equational_and_applicative_case dbd
- signature universe flags m s g gty tables cache context
-=
- let goalno, depth, sort = g in
- let fake_proof = mk_fake_proof m s g gty context in
- if is_equational_case gty flags then
- let elems,tables,cache, flags =
- equational_case tables cache
- depth fake_proof goalno gty s context flags
- in
- let more_elems, tables, cache =
- if flags.use_only_paramod then
- [],tables, cache
- else
- applicative_case dbd
- tables depth s fake_proof goalno
- gty m context signature universe cache flags
- in
- elems@more_elems, tables, cache, flags
- else
- let elems, tables, cache =
- match LibraryObjects.eq_URI () with
- | Some _ ->
- smart_applicative_case dbd tables depth s fake_proof goalno
- gty m context signature universe cache flags
- | None ->
- applicative_case dbd tables depth s fake_proof goalno
- gty m context signature universe cache flags
- in
- elems, tables, cache, flags
-;;
-let rec condition_for_hint i = function
- | [] -> false
- | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
- | _::tl -> condition_for_hint i tl
-;;
-let remove_s_from_fl (id,_,_) (fl : fail list) =
- let rec aux = function
- | [] -> []
- | ((id1,_,_),_)::tl when id = id1 -> tl
- | hd::tl -> hd :: aux tl
- in
- aux fl
-;;
-
-let prunable_for_size flags s m todo =
- let rec aux b = function
- | (S _)::tl -> aux b tl
- | (D (_,_,T))::tl -> aux b tl
- | (D g)::tl ->
- (match calculate_goal_ty g s m with
- | None -> aux b tl
- | Some (canonical_ctx, gty) ->
- let gsize, _ =
- Utils.weight_of_term
- ~consider_metas:false ~count_metas_occurrences:true gty in
- let newb = b || gsize > flags.maxgoalsizefactor in
- aux newb tl)
- | [] -> b
- in
- aux false todo
-
-(*
-let prunable ty todo =
- let rec aux b = function
- | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
- | (D (_,_,T))::tl -> aux b tl
- | D _::_ -> false
- | [] -> b
- in
- aux false todo
-;;
-*)
-
-let prunable menv subst ty todo =
- let rec aux = function
- | (S(_,k,_,_))::tl ->
- (match Equality.meta_convertibility_subst k ty menv with
- | None -> aux tl
- | Some variant ->
- no_progress variant tl (* || aux tl*))
- | (D (_,_,T))::tl -> aux tl
- | _ -> false
- and no_progress variant = function
- | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
- | D ((n,_,P) as g)::tl ->
- (match calculate_goal_ty g subst menv with
- | None -> no_progress variant tl
- | Some (_, gty) ->
- (match calculate_goal_ty g variant menv with
- | None -> assert false
- | Some (_, gty') ->
- if gty = gty' then no_progress variant tl
-(*
-(prerr_endline (string_of_int n);
- prerr_endline (CicPp.ppterm gty);
- prerr_endline (CicPp.ppterm gty');
- prerr_endline "---------- subst";
- prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
- prerr_endline "---------- variant";
- prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
- prerr_endline "---------- menv";
- prerr_endline (CicMetaSubst.ppmetasenv [] menv);
- no_progress variant tl) *)
- else false))
- | _::tl -> no_progress variant tl
- in
- aux todo
-
-;;
-let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
- let s =
- HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
- in
- List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
-;;
-let filter_prune_hint c l =
- let prune = !prune_hint in
- prune_hint := []; (* possible race... *)
- if prune = [] then c,l
- else
- cache_reset_underinspection c,
- List.filter (condition_for_prune_hint prune) l
-;;
-
-let auto_main dbd tables context flags signature universe cache elems =
- auto_context := context;
- let rec aux tables flags cache (elems : status) =
- pp_status context elems;
-(* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
- auto_status := elems;
- check_pause ();
-*)
- let cache, elems = filter_prune_hint cache elems in
- match elems with
- | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
- debug_print (lazy "skip");
- (match !hint with
- | Some i when condition_for_hint i todo ->
- aux tables flags cache orlist
- | _ ->
- hint := None;
- aux tables flags cache elems)
- | [] ->
- (* complete failure *)
- debug_print (lazy "give up");
- Gaveup (tables, cache)
- | (m, s, _, _, [],_)::orlist ->
- (* complete success *)
- debug_print (lazy "success");
- Proved (m, s, orlist, tables, cache)
- | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
- when not flags.AutoTypes.do_types ->
- (* skip since not Prop, don't even check if closed by side-effect *)
- debug_print (lazy "skip existential goal");
- aux tables flags cache ((m, s, size, don, todo, fl)::orlist)
- | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
- (* partial success, cache g and go on *)
- let cache, orlist, fl, sibling_pruned =
- add_to_cache_and_del_from_orlist_if_green_cut
- g s m cache key todo orlist fl context size minsize
- in
- debug_print (lazy (AutoCache.cache_print context cache));
- let fl = remove_s_from_fl g fl in
- let don = if sibling_pruned then don else op::don in
- aux tables flags cache ((m, s, size, don, todo, fl)::orlist)
- | (m, s, size, don, todo, fl)::orlist
- when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
- debug_print (lazy ("FAIL: WIDTH"));
- (* too many goals in and generated by last th *)
- let cache = close_failures fl cache in
- aux tables flags cache orlist
- | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
- debug_print
- (lazy ("FAIL: SIZE: "^string_of_int size ^
- " > " ^ string_of_int flags.maxsize ));
- (* we already have a too large proof term *)
- let cache = close_failures fl cache in
- aux tables flags cache orlist
- | _ when Unix.gettimeofday () > flags.timeout ->
- (* timeout *)
- debug_print (lazy ("FAIL: TIMEOUT"));
- Gaveup (tables, cache)
- | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
- (* attack g *)
- debug_print (lazy "attack goal");
- match calculate_goal_ty g s m with
- | None ->
- (* closed by side effect *)
- debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
- aux tables flags cache ((m,s,size,don,todo, fl)::orlist)
- | Some (canonical_ctx, gty) ->
- let gsize, _ =
- Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
- in
- if gsize > flags.maxgoalsizefactor then
- (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
- aux tables flags cache orlist)
- else if prunable_for_size flags s m todo then
- (debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
- aux tables flags cache orlist)
- else
- (* still to be proved *)
- (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
- match cache_examine cache gty with
- | Failed_in d when d >= depth ->
- (* fail depth *)
- debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
- let cache = close_failures fl cache in
- aux tables flags cache orlist
- | UnderInspection ->
- (* fail loop *)
- debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
- let cache = close_failures fl cache in
- aux tables flags cache orlist
- | Succeded t ->
- debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
- let s, m = put_in_subst s m g canonical_ctx t gty in
- aux tables flags cache ((m, s, size, don,todo, fl)::orlist)
- | Notfound
- | Failed_in _ when depth > 0 ->
- ( (* more depth or is the first time we see the goal *)
- if prunable m s gty todo then
- (debug_print (lazy(
- "FAIL: LOOP: one father is equal"));
- aux tables flags cache orlist)
- else
- let cache = cache_add_underinspection cache gty depth in
- auto_status := status;
- check_pause ();
- debug_print
- (lazy ("INSPECTING: " ^
- string_of_int gno ^ "("^ string_of_int size ^ "): "^
- CicPp.ppterm gty));
- (* elems are possible computations for proving gty *)
- let elems, tables, cache, flags =
- equational_and_applicative_case dbd
- signature universe flags m s g gty tables cache context
- in
- if elems = [] then
- (* this goal has failed *)
- let cache = close_failures ((g,gty)::fl) cache in
- aux tables flags cache orlist
- else
- (* elems = (cand,m,s,gl) *)
- let size_gl l = List.length
- (List.filter (function (_,_,P) -> true | _ -> false) l)
- in
- let elems =
- let inj_gl gl = List.map (fun g -> D g) gl in
- let rec map = function
- | [] -> assert false
- | (cand,m,s,gl)::[] ->
- (* in the last one we add the failure *)
- let todo =
- inj_gl gl @ (S(g,gty,cand,size+1))::todo
- in
- (* we are the last in OR, we fail on g and
- * also on all failures implied by g *)
- (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
- :: orlist
- | (cand,m,s,gl)::tl ->
- (* we add the S step after gl and before todo *)
- let todo =
- inj_gl gl @ (S(g,gty,cand,size+1))::todo
- in
- (* since we are not the last in OR, we do not
- * imply failures *)
- (m,s, size + size_gl gl, don, todo, []) :: map tl
- in
- map elems
- in
- aux tables flags cache elems)
- | _ ->
- (* no more depth *)
- debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
- let cache = close_failures fl cache in
- aux tables flags cache orlist)
- in
- (aux tables flags cache elems : auto_result)
-;;
-
-
-let
- auto_all_solutions dbd tables universe cache context metasenv gl flags
-=
- let signature =
- List.fold_left
- (fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
- )
- MetadataConstraints.UriManagerSet.empty gl
- in
- let goals = order_new_goals metasenv [] gl CicPp.ppterm in
- let goals =
- List.map
- (fun (x,s) -> D (x,flags.maxdepth,s)) goals
- in
- let elems = [metasenv,[],1,[],goals,[]] in
- let rec aux tables solutions cache elems flags =
- match auto_main dbd tables context flags signature universe cache elems with
- | Gaveup (tables,cache) ->
- solutions,cache, tables
- | Proved (metasenv,subst,others,tables,cache) ->
- if Unix.gettimeofday () > flags.timeout then
- ((subst,metasenv)::solutions), cache, tables
- else
- aux tables ((subst,metasenv)::solutions) cache others flags
- in
- let rc = aux tables [] cache elems flags in
- match rc with
- | [],cache,tables -> [],cache,tables
- | solutions, cache,tables ->
- let solutions =
- HExtlib.filter_map
- (fun (subst,newmetasenv) ->
- let opened =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
- in
- if opened = [] then Some subst else None)
- solutions
- in
- solutions,cache,tables
-;;
-
-(******************* AUTO ***************)
-
-
-let auto dbd flags metasenv tables universe cache context metasenv gl =
- let initial_time = Unix.gettimeofday() in
- let signature =
- List.fold_left
- (fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
- )
- MetadataConstraints.UriManagerSet.empty gl
- in
- let goals = order_new_goals metasenv [] gl CicPp.ppterm in
- let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
- let elems = [metasenv,[],1,[],goals,[]] in
- match auto_main dbd tables context flags signature universe cache elems with
- | Proved (metasenv,subst,_, tables,cache) ->
- debug_print(lazy
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- Some (subst,metasenv), cache
- | Gaveup (tables,cache) ->
- debug_print(lazy
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- None,cache
-;;
-
-let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
- let flags = flags_of_params params () in
- let use_library = flags.use_library in
- let universe, tables, cache =
- init_cache_and_tables
- ~dbd ~use_library ~use_context:(not flags.skip_context)
- automation_cache univ (proof, goal)
- in
- let _,metasenv,subst,_,_, _ = proof in
- let _,context,goalty = CicUtil.lookup_meta goal metasenv in
- let signature = MetadataQuery.signature_of metasenv goal in
- let signature =
- match univ with
- | None -> signature
- | Some l ->
- List.fold_left
- (fun set t ->
- let ty, _ =
- CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.oblivion_ugraph
- in
- MetadataConstraints.UriManagerSet.union set
- (MetadataConstraints.constants_of ty)
- )
- signature l
- in
- let tables,cache =
- if flags.close_more then
- close_more
- tables context (proof, goal)
- (auto_all_solutions dbd) signature universe cache
- else tables,cache in
- let initial_time = Unix.gettimeofday() in
- let (_,oldmetasenv,_,_,_, _) = proof in
- hint := None;
- let elem =
- metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
- in
- match auto_main dbd tables context flags signature universe cache [elem] with
- | Proved (metasenv,subst,_, tables,cache) ->
- debug_print (lazy
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- let proof,metasenv =
- ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goal subst metasenv
- in
- let opened =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:metasenv
- in
- proof,opened
- | Gaveup (tables,cache) ->
- debug_print
- (lazy ("TIME:"^
- string_of_float(Unix.gettimeofday()-.initial_time)));
- raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
-;;
-
-let auto_tac ~dbd ~params ~automation_cache =
- ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~automation_cache);;
-
-let pp_proofterm = Equality.pp_proofterm;;
-
-let revision = "$Revision$";;
-let size_and_depth context metasenv t = 100, 100