X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fauto.ml;h=aca89bd4a609a8b427aaa71fc4f8200786fc81b5;hb=78f2fb8fcf0bbd2521b67e4366b734ad88ebdc68;hp=65087f8cbd14571035e856d22ecf389254098714;hpb=3f586b01da59fe16b3d7f37da28bdd71f2225131;p=helm.git diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 65087f8cb..aca89bd4a 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -28,7 +28,7 @@ open AutoCache;; let debug = false;; let debug_print s = - if debug then () else prerr_endline (Lazy.force s);; + if debug then prerr_endline (Lazy.force s);; (* functions for retrieving theorems *) @@ -192,7 +192,7 @@ let empty_tables = let init_cache_and_tables dbd use_library paramod universe (proof, goal) = (* the local cache in initially empty *) let cache = AutoCache.cache_empty in - let _, metasenv, _, _ = proof in + let _, metasenv, _, _, _ = proof in let signature = MetadataQuery.signature_of metasenv goal in let newmeta = CicMkImplicit.new_meta metasenv [] in let _,context,_ = CicUtil.lookup_meta goal metasenv in @@ -335,7 +335,7 @@ let build_equalities auto context metasenv tables universe cache newmeta equatio let close_more tables maxmeta context status auto universe cache = let (active,passive,bag) = tables in let proof, goalno = status in - let _, metasenv,_,_ = proof in + let _, metasenv,_,_, _ = proof in let signature = MetadataQuery.signature_of metasenv goalno in let equations = retrieve_equations signature universe cache context in let eqs_and_types = @@ -368,7 +368,7 @@ let find_context_equalities let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let _,metasenv,_,_ = proof in + let _,metasenv,_,_, _ = proof in let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in (* if use_auto is true, we try to close the hypothesis of equational statements using auto; a naif, and probably wrong approach *) @@ -435,8 +435,8 @@ let new_metasenv_and_unify_and_t match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in let proof',oldmetasenv = - let (puri,metasenv,pbo,pty) = proof in - (puri,newmetasenv,pbo,pty),metasenv + let (puri,metasenv,pbo,pty, attrs) = proof in + (puri,newmetasenv,pbo,pty, attrs),metasenv in let goal_for_paramod = match LibraryObjects.eq_URI () with @@ -446,7 +446,7 @@ let new_metasenv_and_unify_and_t 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 = proof' in uri,metasenv_for_paramod,p,ty in + let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let proof''',goals = ProofEngineTypes.apply_tactic @@ -471,7 +471,7 @@ let new_metasenv_and_unify_and_t | Some (_,proof''''',_), active,passive,_ -> subst,proof''''', ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive + ~newmetasenv:(let _,m,_,_, _ = proof''''' in m), active, passive ;; let rec count_prods context ty = @@ -483,7 +483,7 @@ let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in - let (_,metasenv,_,_) = proof in + let (_,metasenv,_,_, _) = 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' = @@ -653,7 +653,7 @@ let equational_case with | None, active, passive, maxmeta -> [], (active,passive,bag), cache, maxmeta, flags - | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta -> + | Some(subst',(_,metasenv,proof,_, _),open_goals),active,passive,maxmeta -> assert_subst_are_disjoint subst subst'; let subst = subst@subst' in let open_goals = order_new_goals metasenv subst open_goals ppterm in @@ -668,7 +668,7 @@ let equational_case assert (maxmeta >= maxm); let res' = List.map - (fun subst',(_,metasenv,proof,_),open_goals -> + (fun subst',(_,metasenv,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 @@ -702,7 +702,7 @@ let try_candidate = let ppterm = ppterm context in try - let subst', ((_,metasenv,_,_), open_goals), maxmeta = + let subst', ((_,metasenv,_,_, _), open_goals), maxmeta = PrimitiveTactics.apply_with_subst ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) in @@ -863,7 +863,7 @@ let rec auto_main tables maxm context flags elems universe cache = | Notfound | Failed_in _ when depth > 0 -> (* we have more depth now *) let cache = cache_add_underinspection cache goalty depth in - let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in + let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *) let elems, tables, cache, maxm, flags = if is_equational_case goalty flags then let elems,tables,cache,maxm1, flags = @@ -1044,7 +1044,7 @@ let rec position_of i x = function let superposition_tac ~target ~table ~subterms_only ~demod_table status = Saturation.reset_refs(); let proof,goalno = status in - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goalno metasenv in let eq_uri,tty = eq_and_ty_of_goal ty in let env = (metasenv, context, CicUniv.empty_ugraph) in @@ -1148,7 +1148,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) = ~target ~table ~subterms_only ~demod_table (proof,goal) | false -> (* this is the real auto *) - let _,metasenv,_,_ = proof in + let _,metasenv,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let flags = flags_of_params params () in (* just for testing *) @@ -1162,7 +1162,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) = tables newmeta context (proof, goal) auto_all_solutions universe cache else tables,cache,newmeta in let initial_time = Unix.gettimeofday() in - let (_,oldmetasenv,_,_) = proof in + let (_,oldmetasenv,_,_, _) = proof in let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in match auto_main tables newmeta context flags [elem] universe cache with | Success (metasenv,subst,_), tables,cache,_ -> @@ -1191,7 +1191,7 @@ let eq_of_goal = function (* DEMODULATE *) let demodulate_tac ~dbd ~universe (proof,goal)= - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,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 = [], [], ty in @@ -1218,7 +1218,7 @@ let demodulate_tac ~dbd ~universe (proof,goal)= in let extended_metasenv = (maxm,context,newty)::metasenv in let extended_status = - (curi,extended_metasenv,pbo,pty),goal in + (curi,extended_metasenv,pbo,pty, attrs),goal in let (status,newgoals) = ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac ~term:proofterm)