(fun x _ m -> embed m x) m args
in
m, Terms.Node (Terms.Leaf (hash name):: args)
- ;;
+ let is_eq = function
+ | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
+ Some (ty,l,r)
+ | _ -> None
let saturate bo ty =
let vars, ty = embed [] ty in
let _, bo = embed vars bo in
~max_steps:max_int bag ~g_passives:[g_passives] ~passives
with
| P.Error s -> report_error s; 3
- | P.Unsatisfiable ((bag,_,l)::_) ->
+ | P.Unsatisfiable ((bag,_,_,l)::_) ->
success_msg bag l pp_unit_clause name; 0
| P.Unsatisfiable ([]) ->
report_error "Unsatisfiable but no solution output"; 3
> log
for PROBLEM in `cat $2`; do
echo running on $PROBLEM
- ./TreeLimitedRun -q0 $1 $(($1*2)) ./matitaprover.native --tptppath ~/TPTP-v3.7.0/ $PROBLEM \
+ ./TreeLimitedRun -q0 $1 $(($1*2)) ./matitaprover.native --tptppath ~/TPTP-v3.1.1/ $PROBLEM \
>> log 2>&1
echo So far `grep 'SZS status Unsatisfiable' log|wc -l` solved
done
(* use the one below to reset precedence and associativity *)
let invoke_reinit t = aux [] mathonly xref ~-1 t in
match l with
+ | A.Sup (A.Layout (A.Sub (t1,t2)), t3)
+ | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
+ -> Mpres.Msubsup (attrs, invoke' t1, invoke_reinit t2, invoke_reinit t3)
| A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2)
| A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2)
| A.Below (t1, t2) -> Mpres.Munder (attrs, invoke' t1, invoke_reinit t2)
type 'ident intros_spec = int option * 'ident option list
-type 'term auto_params = 'term list * (string*string) list
+type 'term auto_params = 'term list option * (string*string) list
type 'term just =
[ `Term of 'term
let pp_auto_params ~term_pp (univ, params) =
String.concat " "
(List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^
- if univ <> [] then
- (if params <> [] then " " else "") ^ "by " ^
- String.concat " " (List.map term_pp univ)
- else ""
+ match univ with
+ | None -> ""
+ | Some l -> (if params <> [] then " " else "") ^ "by " ^
+ String.concat " " (List.map term_pp l)
;;
let pp_just ~term_pp =
pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
- | NAuto (_,(l,flgs)) ->
- "nauto" ^
- (if l <> [] then (" by " ^
- (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
+ | NAuto (_,(None,flgs)) ->
+ "nauto" ^
+ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
+ | NAuto (_,(Some l,flgs)) ->
+ "nauto" ^ " by " ^
+ (String.concat "," (List.map CicNotationPp.pp_term l)) ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
end
;;
+let compute_keys uri height kind =
+ let mk_item orig_ty spec =
+ let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
+ let keys =
+ match ty with
+ | NCic.Const (NReference.Ref (_,NReference.Def h))
+ | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_)
+ when h > 0 ->
+ let ty',_,_=
+ NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in
+ [ty;ty']
+ | _ -> [ty]
+ in
+ keys,NCic.Const(NReference.reference_of_spec uri spec)
+ in
+ let data =
+ match kind with
+ | NCic.Fixpoint (ind,ifl,_) ->
+ HExtlib.list_mapi
+ (fun (_,_,rno,ty,_) i ->
+ if ind then mk_item ty (NReference.Fix (i,rno,height))
+ else mk_item ty (NReference.CoFix height)) ifl
+ | NCic.Inductive (b,lno,itl,_) ->
+ HExtlib.list_mapi
+ (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl
+ @
+ List.map
+ (fun ((_,_,ty),i,j) ->
+ mk_item ty (NReference.Con (i,j+1,lno)))
+ (List.flatten
+ (HExtlib.list_mapi
+ (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
+ itl))
+ | NCic.Constant (_,_,Some _, ty, _) ->
+ [ mk_item ty (NReference.Def height) ]
+ | NCic.Constant (_,_,None, ty, _) ->
+ [ mk_item ty NReference.Decl ]
+ in
+ let data = HExtlib.filter_map
+ (fun (keys, t) ->
+ let keys = List.filter
+ (function
+ | (NCic.Meta _)
+ | (NCic.Appl (NCic.Meta _::_)) -> false
+ | _ -> true)
+ keys
+ in
+ if keys <> [] then
+ begin
+ HLog.debug ("Indexing:" ^
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
+ Some (keys,t)
+ end
+ else
+ begin
+ HLog.debug ("Not indexing:" ^
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ None
+ end)
+ data
+ in data
+;;
+
let index_obj_for_auto status (uri, height, _, _, kind) =
(*prerr_endline (string_of_int height);*)
- let mk_item orig_ty spec =
- let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
- let keys =
- match ty with
- | NCic.Const (NReference.Ref (_,NReference.Def h))
- | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_)
- when h > 0 ->
- let ty',_,_= NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in
- [ty;ty']
- | _ -> [ty]
- in
- keys,NCic.Const(NReference.reference_of_spec uri spec)
- in
- let data =
- match kind with
- | NCic.Fixpoint (ind,ifl,_) ->
- HExtlib.list_mapi
- (fun (_,_,rno,ty,_) i ->
- if ind then mk_item ty (NReference.Fix (i,rno,height))
- else mk_item ty (NReference.CoFix height)) ifl
- | NCic.Inductive (b,lno,itl,_) ->
- HExtlib.list_mapi
- (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl
- @
- List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno)))
- (List.flatten (HExtlib.list_mapi
- (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
- itl))
- | NCic.Constant (_,_,Some _, ty, _) ->
- [ mk_item ty (NReference.Def height) ]
- | NCic.Constant (_,_,None, ty, _) ->
- [ mk_item ty NReference.Decl ]
- in
- let data = HExtlib.filter_map
- (fun (keys, t) ->
- let keys = List.filter
- (function
- | (NCic.Meta _)
- | (NCic.Appl (NCic.Meta _::_)) -> false
- | _ -> true)
- keys
- in
- if keys <> [] then
- begin
- HLog.debug ("Indexing:" ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
- HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
- Some (keys,t)
- end
- else
- begin
- HLog.debug ("Not indexing:" ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
- None
- end)
- data
- in
- let status = basic_index_obj data status in
- let dump = record_index_obj data :: status#dump in
- status#set_dump dump
+ let data = compute_keys uri height kind in
+ let status = basic_index_obj data status in
+ let dump = record_index_obj data :: status#dump in
+ status#set_dump dump
;;
let index_eq uri status =
) hyps,
(text,prefix_len,concl))
) seqs)
- | GrafiteAst.NAuto (_loc, (l,a)) ->
+ | GrafiteAst.NAuto (_loc, (None,a)) -> NAuto.auto_tac ~params:(None,a)
+ | GrafiteAst.NAuto (_loc, (Some l,a)) ->
NAuto.auto_tac
- ~params:(List.map (fun x -> "",0,x) l,a)
+ ~params:(Some List.map (fun x -> "",0,x) l,a)
| GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
| GrafiteAst.NCases (_loc, what, where) ->
NTactics.cases_tac
;;
let disambiguate_auto_params
- disambiguate_term metasenv context (terms, params)
+ disambiguate_term metasenv context (oterms, params)
=
- let metasenv, terms =
- List.fold_right
- (fun t (metasenv, terms) ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv,t::terms) terms (metasenv, [])
- in
- metasenv, (terms, params)
+ match oterms with
+ | None -> metasenv, (None, params)
+ | Some terms ->
+ let metasenv, terms =
+ List.fold_right
+ (fun t (metasenv, terms) ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,t::terms) terms (metasenv, [])
+ in
+ metasenv, (Some terms, params)
;;
let disambiguate_just disambiguate_term context metasenv =
concl = tactic_term -> (List.rev hyps,concl) ] ->
G.NAssert (loc, seqs)
| IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
- | SYMBOL "/"; num = OPT NUMBER ; SYMBOL "/" ->
- let depth = match num with Some n -> n | None -> "1" in
- G.NAuto (loc, ([],["slir","";"depth",depth]))
+ | SYMBOL "/"; num = OPT NUMBER ; SYMBOL "/" ;
+ (univ,params) = auto_params ->
+ let depth = match num with Some n -> n | None -> "1" in
+ G.NAuto (loc, (univ,["slir","";"depth",depth]@params))
| IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
G.NCases (loc, what, where)
| IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
| "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
id2 = IDENT ; RPAREN ->
- G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
+ G.ExistsElim (loc, `Auto (None,[]), id1, t1, id2, t2)
| just =
[ IDENT "using"; t=tactic_term -> `Term t
| params = auto_params -> `Auto params] ;
]
];
auto_params: [
- [ params =
+ [ params =
LIST0 [
i = auto_fixed_param -> i,""
| i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
string_of_int v | v = IDENT -> v ] -> i,v ];
- tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
- (match tl with Some l -> l | None -> []),
+ tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl,
+ (* (match tl with Some l -> l | None -> []), *)
params
]
];
(* =================================== paramod =========================== *)
let auto_paramod ~params:(l,_) status goal =
+ let l = match l with
+ | None -> raise (Error (lazy "no proof found",None))
+ | Some l -> l in
let gty = get_goalty status goal in
let n,h,metasenv,subst,o = status#obj in
let status,t = term_of_cic_term status gty (ctx_of gty) in
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
val auto_tac:
- params:(NTacStatus.tactic_term list * (string * string) list) ->
+ params:(NTacStatus.tactic_term list option * (string * string) list) ->
's NTacStatus.tactic
val group_by_tac:
type flags = {
do_types : bool; (* solve goals in Type *)
last : bool; (* last goal: take first solution only *)
+ candidates: Ast.term list option;
maxwidth : int;
maxsize : int;
maxdepth : int;
trace: Ast.term list
}
-let add_to_trace cache t =
+let add_to_trace ~depth cache t =
match t with
- | Ast.NRef _ -> {cache with trace = t::cache.trace}
+ | Ast.NRef _ ->
+ debug_print ~depth (lazy ("Adding to trace: " ^ CicNotationPp.pp_term t));
+ {cache with trace = t::cache.trace}
| Ast.NCic _ (* local candidate *)
| _ -> (*not an application *) cache
+let pptrace tr =
+ (lazy ("Proof Trace: " ^ (String.concat ";"
+ (List.map CicNotationPp.pp_term tr))))
(* not used
let remove_from_trace cache t =
match t with
aux t
;;
+let get_cands retrieve_for diff empty gty weak_gty =
+ let cands = retrieve_for gty in
+ match weak_gty with
+ | None -> cands, empty
+ | Some weak_gty ->
+ let more_cands = retrieve_for weak_gty in
+ cands, diff more_cands cands
+;;
+
+let get_candidates ?(smart=true) depth flags status cache signature gty =
+ let maxd = ((depth + 1) = flags.maxdepth) in
+ let universe = status#auto_cache in
+ let _,_,metasenv,subst,_ = status#obj in
+ let context = ctx_of gty in
+ let _, raw_gty = term_of_cic_term status gty context in
+ let raw_weak_gty, weak_gty =
+ if smart then
+ match raw_gty with
+ | NCic.Appl _
+ | NCic.Const _
+ | NCic.Rel _ ->
+ let weak = perforate_small subst metasenv context raw_gty in
+ Some weak, Some (mk_cic_term context weak)
+ | _ -> None,None
+ else None,None
+ in
+ let global_cands, smart_global_cands =
+ match flags.candidates with
+ | Some l when (not maxd) -> l,[]
+ | Some _
+ | None ->
+ let mapf s =
+ let to_ast = function
+ | NCic.Const r -> Ast.NRef r | _ -> assert false in
+ List.map to_ast (NDiscriminationTree.TermSet.elements s) in
+ let g,l =
+ get_cands
+ (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe)
+ NDiscriminationTree.TermSet.diff
+ NDiscriminationTree.TermSet.empty
+ raw_gty raw_weak_gty in
+ mapf g, mapf l in
+ let local_cands,smart_local_cands =
+ let mapf s =
+ let to_ast t =
+ let _status, t = term_of_cic_term status t context
+ in Ast.NCic t in
+ List.map to_ast (Ncic_termSet.elements s) in
+ let g,l =
+ get_cands
+ (fun ty -> search_in_th ty cache)
+ Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
+ mapf g, mapf l in
+ sort_candidates status context (global_cands@local_cands),
+ sort_candidates status context (smart_global_cands@smart_local_cands)
+;;
+
+(* old version
let get_candidates ?(smart=true) status cache signature gty =
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let c_ast = function
| NCic.Const r -> Ast.NRef r | _ -> assert false in
let _, raw_gty = term_of_cic_term status gty context in
- let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe raw_gty in
+ let cands =
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe raw_gty
+ in
let local_cands = search_in_th gty cache in
debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
(List.length tl)) in *)
let more_cands =
- NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe weak_gty in
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe weak_gty
+ in
let smart_cands =
NDiscriminationTree.TermSet.diff more_cands cands in
- let cic_weak_gty = mk_cic_term context weak_gty in
+ let cic_weak_gty = mk_cic_term context weak_gty in
let more_local_cands = search_in_th cic_weak_gty cache in
let smart_local_cands =
Ncic_termSet.diff more_local_cands local_cands in
(* if smart then smart_candidates, []
else candidates, [] *)
candidates, smart_candidates
-;;
+;;
+
+let get_candidates ?(smart=true) flags status cache signature gty =
+ match flags.candidates with
+ | None -> get_candidates ~smart status cache signature gty
+ | Some l -> l,[]
+;; *)
-let applicative_case depth signature status flags gty (cache:cache) =
+let applicative_case depth signature status flags gty cache =
app_counter:= !app_counter+1;
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
in
debug_print(lazy (string_of_bool is_eq));
let candidates, smart_candidates =
- get_candidates ~smart:(not is_eq) status tcache signature gty in
+ get_candidates ~smart:(not is_eq) depth
+ flags status tcache signature gty in
debug_print ~depth
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
debug_print ~depth
| _ -> status, facts
;;
-let rec intros ~depth status (cache:cache) =
+let rec intros ~depth status cache =
match is_prod status with
| Some _ ->
+ let trace = cache.trace in
let status,facts =
intros_facts ~depth status cache.facts
in
(* we reindex the equation from scratch *)
let unit_eq =
index_local_equations status#eq_cache status in
- status, init_cache ~facts ~unit_eq ()
+ status, init_cache ~facts ~unit_eq () ~trace
| _ -> status, cache
;;
flags signature cache depth status : unit =
debug_print ~depth (lazy ("entering auto clusters at depth " ^
(string_of_int depth)));
+ debug_print ~depth (pptrace cache.trace);
(* ignore(Unix.select [] [] [] 0.01); *)
let status = clean_up_tac status in
let goals = head_goals status#stack in
and
(* BRAND NEW VERSION *)
-auto_main flags signature (cache:cache) depth status: unit =
+auto_main flags signature cache depth status: unit =
debug_print ~depth (lazy "entering auto main");
+ debug_print ~depth (pptrace cache.trace);
debug_print ~depth (lazy ("stack length = " ^
(string_of_int (List.length status#stack))));
(* ignore(Unix.select [] [] [] 0.01); *)
let depth,cache =
if t=Ast.Ident("__whd",None) then depth, cache
else depth+1,loop_cache in
- let cache = add_to_trace cache t in
+ let cache = add_to_trace ~depth cache t in
try
- auto_clusters flags signature (cache:cache) depth status
+ auto_clusters flags signature cache depth status
with Gaveup _ ->
debug_print ~depth (lazy "Failed");
())
| _ -> false) trace
;;
-let auto_tac ~params:(_univ,flags) status =
+let auto_tac ~params:(univ,flags) status =
let oldstatus = status in
let status = (status:> NTacStatus.tac_status) in
let goals = head_goals status#stack in
let status, facts = mk_th_cache status goals in
let unit_eq = index_local_equations status#eq_cache status in
- let cache = init_cache ~facts ~unit_eq () in
+ let cache = init_cache ~facts ~unit_eq () in
(* pp_th status facts; *)
(*
NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
(NDiscriminationTree.TermSet.elements t))
)));
*)
+ let candidates =
+ match univ with
+ | None -> None
+ | Some l ->
+ let to_Ast t =
+ let status, res = disambiguate status [] t None in
+ let _,res = term_of_cic_term status res (ctx_of res)
+ in Ast.NCic res
+ in Some (List.map to_Ast l)
+ in
let depth = int "depth" flags 3 in
let size = int "size" flags 10 in
let width = int "width" flags 4 (* (3+List.length goals)*) in
let signature = height_of_goals status in
let flags = {
last = true;
+ candidates = candidates;
maxwidth = width;
maxsize = size;
maxdepth = depth;
| Proved (s,trace) ->
debug_print (lazy ("proved at depth " ^ string_of_int x));
let trace = cleanup_trace s trace in
- let _ = print (lazy
- ("Proof Trace: " ^ (String.concat ";"
- (List.map CicNotationPp.pp_term trace)))) in
+ let _ = print (pptrace trace) in
let stack =
match s#stack with
| (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
#NTacStatus.pstatus -> NUri.uri -> bool
val fast_eq_check_tac:
- params:(NTacStatus.tactic_term list * (string * string) list) ->
+ params:(NTacStatus.tactic_term list option * (string * string) list) ->
's NTacStatus.tactic
val paramod_tac:
- params:(NTacStatus.tactic_term list * (string * string) list) ->
+ params:(NTacStatus.tactic_term list option * (string * string) list) ->
's NTacStatus.tactic
val demod_tac:
- params:(NTacStatus.tactic_term list * (string * string) list) ->
+ params:(NTacStatus.tactic_term list option* (string * string) list) ->
's NTacStatus.tactic
val smart_apply_tac:
NTacStatus.tactic_term -> 's NTacStatus.tactic
val auto_tac:
- params:(NTacStatus.tactic_term list * (string * string) list) ->
+ params:(NTacStatus.tactic_term list option * (string * string) list) ->
's NTacStatus.tactic
| _ -> false
;;
-type auto_params = Cic.term list * (string * string) list
+type auto_params = Cic.term list option * (string * string) list
let elems = ref [] ;;
metasenv subst context t None)
automation_cache ct
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 automation_cache =
- add_list_to_tables metasenv subst 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
- else
- 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
+ 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
+ automation_cache.AutomationCache.univ,
+ automation_cache.AutomationCache.tables,
+ cache_empty
;;
let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast =
(***************** applyS *******************)
let apply_smart_aux
- dbd automation_cache params proof goal newmeta' metasenv' subst
+ dbd automation_cache (params:auto_params) proof goal newmeta' metasenv' subst
context term' ty termty goal_arity
=
let consthead,newmetasenv,arguments,_ =
=
let ppterm = ppterm context in
try
- let params = ([],[]) in
+ let params = (None,[]) in
let automation_cache = {
AutomationCache.tables = tables ;
AutomationCache.univ = Universe.empty; }
let _,metasenv,subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let signature = MetadataQuery.signature_of metasenv goal in
- let signature =
- 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 univ
+ 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
* http://cs.unibo.it/helm/.
*)
-type auto_params = Cic.term list * (string * string) list
+type auto_params = Cic.term list option * (string * string) list
val auto_tac:
dbd:HSql.dbd ->
| `Term just -> Tactics.apply just
| `SolveWith term ->
Tactics.demodulate ~automation_cache ~dbd
- ~params:([term],
+ ~params:(Some [term],
["all","1";"steps","1"; "use_context","false"])
| `Proof ->
Tacticals.id_tac
else [])@
[GA.Executable(floc,GA.NTactic(floc, [
if (*ueq_case*) true then
- GA.NAuto (floc,(
+ GA.NAuto (floc,(Some
HExtlib.list_mapi
(fun _ i ->
mk_ident ("H" ^ string_of_int i))
context
,[]))
else
- GA.NAuto (floc,([],[
+ GA.NAuto (floc,(None,[
"depth",string_of_int 5;
"width",string_of_int 5;
"size",string_of_int 20;
else [])@
[GA.Executable(floc,GA.Tactic(floc, Some (
if true (*ueq_case*) then
- GA.AutoBatch (floc,([],["paramodulation","";
+ GA.AutoBatch (floc,(None,["paramodulation","";
"timeout",string_of_int !paramod_timeout]))
else
- GA.AutoBatch (floc,([],[
+ GA.AutoBatch (floc,(None,[
"depth",string_of_int 5;
"width",string_of_int 5;
"size",string_of_int 20;
projects / helm.git / commitdiff