From a14adba81c00c9dcb9996d7af39e4803214606f1 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 31 Mar 2010 09:07:11 +0000 Subject: [PATCH] Tracing mechanism for auto. Interface changed to solve an ambiguity between an ampty trace and a missing trace. From: asperti --- .../binaries/matitaprover/matitaprover.ml | 7 +- .../binaries/matitaprover/run_on_a_list.sh | 2 +- .../content_pres/cicNotationPres.ml | 3 + .../software/components/grafite/grafiteAst.ml | 2 +- .../components/grafite/grafiteAstPp.ml | 18 +-- .../grafite_engine/grafiteEngine.ml | 135 ++++++++++-------- .../grafite_parser/grafiteDisambiguate.ml | 19 +-- .../grafite_parser/grafiteParser.ml | 15 +- helm/software/components/ng_tactics/nAuto.ml | 3 + helm/software/components/ng_tactics/nAuto.mli | 2 +- helm/software/components/ng_tactics/nnAuto.ml | 127 +++++++++++++--- .../software/components/ng_tactics/nnAuto.mli | 8 +- helm/software/components/tactics/auto.ml | 120 ++++++++-------- helm/software/components/tactics/auto.mli | 2 +- .../components/tactics/declarative.ml | 2 +- .../components/tptp_grafite/tptp2grafite.ml | 8 +- 16 files changed, 294 insertions(+), 179 deletions(-) diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index 38553b305..f72a7ebc5 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -67,7 +67,10 @@ module MakeBlob(C:LeafComparer) : Terms.Blob (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 @@ -145,7 +148,7 @@ module Main(P : Paramod.Paramod with type t = leaf) = struct ~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 diff --git a/helm/software/components/binaries/matitaprover/run_on_a_list.sh b/helm/software/components/binaries/matitaprover/run_on_a_list.sh index 420b6b956..79c1b42eb 100755 --- a/helm/software/components/binaries/matitaprover/run_on_a_list.sh +++ b/helm/software/components/binaries/matitaprover/run_on_a_list.sh @@ -8,7 +8,7 @@ gcc TreeLimitedRun.c -o TreeLimitedRun > 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 diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 35f128a05..82a326c48 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -371,6 +371,9 @@ let render ~lookup_uri ?(prec=(-1)) = (* 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) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 1910e34ac..5b10a5465 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -43,7 +43,7 @@ type 'lazy_term reduction = 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 diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index e022c6f33..f489b15b5 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -77,10 +77,10 @@ let opt_string_pp = function 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 = @@ -96,10 +96,12 @@ let rec pp_ntactic ~map_unicode_to_tex = 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 diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 520289aa1..4d7b8ce4e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -530,69 +530,77 @@ let record_index_obj = 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 = @@ -776,9 +784,10 @@ let eval_ng_tac tac = ) 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 diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 28742e6c7..7ce0407e8 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -307,15 +307,18 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function ;; 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 = diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 74991bcb9..3d5c662ca 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -250,9 +250,10 @@ EXTEND 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 -> @@ -422,7 +423,7 @@ EXTEND | "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] ; @@ -498,13 +499,13 @@ EXTEND ] ]; 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 ] ]; diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 65252eaf9..6f49f7d36 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -24,6 +24,9 @@ module Ast = CicNotationPt (* =================================== 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 diff --git a/helm/software/components/ng_tactics/nAuto.mli b/helm/software/components/ng_tactics/nAuto.mli index 36b5bd153..2e7394d8c 100644 --- a/helm/software/components/ng_tactics/nAuto.mli +++ b/helm/software/components/ng_tactics/nAuto.mli @@ -12,7 +12,7 @@ (* $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: diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 11b58895e..baa38195a 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -643,6 +643,7 @@ let search_in_th gty th = 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; @@ -656,12 +657,17 @@ type cache = 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 @@ -800,6 +806,65 @@ let perforate_small subst metasenv context t = 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 @@ -810,8 +875,10 @@ let get_candidates ?(smart=true) status cache signature gty = 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))))); @@ -833,11 +900,12 @@ let get_candidates ?(smart=true) status cache signature gty = 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 @@ -850,9 +918,15 @@ let get_candidates ?(smart=true) status cache signature gty = (* 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 @@ -866,7 +940,8 @@ let applicative_case depth signature status flags gty (cache:cache) = 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 @@ -993,16 +1068,17 @@ let rec intros_facts ~depth status facts = | _ -> 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 ;; @@ -1182,6 +1258,7 @@ let rec auto_clusters ?(top=false) 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 @@ -1256,8 +1333,9 @@ let rec auto_clusters ?(top=false) 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); *) @@ -1326,9 +1404,9 @@ auto_main flags signature (cache:cache) depth status: unit = 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"); ()) @@ -1358,13 +1436,13 @@ let cleanup_trace s trace = | _ -> 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 -> @@ -1375,6 +1453,16 @@ let auto_tac ~params:(_univ,flags) status = (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 @@ -1383,6 +1471,7 @@ let auto_tac ~params:(_univ,flags) status = let signature = height_of_goals status in let flags = { last = true; + candidates = candidates; maxwidth = width; maxsize = size; maxdepth = depth; @@ -1411,9 +1500,7 @@ let auto_tac ~params:(_univ,flags) status = | 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 diff --git a/helm/software/components/ng_tactics/nnAuto.mli b/helm/software/components/ng_tactics/nnAuto.mli index 13a519d70..bc71db5c6 100644 --- a/helm/software/components/ng_tactics/nnAuto.mli +++ b/helm/software/components/ng_tactics/nnAuto.mli @@ -13,21 +13,21 @@ val is_a_fact_obj: #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 diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 973cc1d78..a89bbd4a1 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -141,7 +141,7 @@ let is_an_equational_goal = function | _ -> false ;; -type auto_params = Cic.term list * (string * string) list +type auto_params = Cic.term list option * (string * string) list let elems = ref [] ;; @@ -377,52 +377,53 @@ let init_cache_and_tables 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 = @@ -956,7 +957,7 @@ let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache = (***************** 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,_ = @@ -1673,7 +1674,7 @@ let try_smart_candidate dbd = let ppterm = ppterm context in try - let params = ([],[]) in + let params = (None,[]) in let automation_cache = { AutomationCache.tables = tables ; AutomationCache.univ = Universe.empty; } @@ -2129,17 +2130,20 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa 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 diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index c8a9224cb..557d78194 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -23,7 +23,7 @@ * 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 -> diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 139dcb1f8..02d7c6144 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -197,7 +197,7 @@ let rewritingstep ~dbd ~automation_cache lhs rhs just last_step = | `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 diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index c63fca741..2e1bb9bce 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -246,14 +246,14 @@ let ng_generate_tactics fv ueq_case context arities = 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; @@ -294,10 +294,10 @@ let generate_tactics fv ueq_case = 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; -- 2.39.2