X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=973cc1d782433a91e3296b9022dc808b433eb1c7;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=81d5c6f4c1f80aa9a03c80070c3239663c170259;hpb=92c870913842926076d44bb822ec47f9e0843bc4;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 81d5c6f4c..973cc1d78 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -38,12 +38,14 @@ 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 @@ -516,10 +518,9 @@ let build_equalities auto context metasenv subst tables universe cache equations ) (tables,[],cache) equations -let close_more tables context status auto universe cache = +let close_more tables context status auto signature universe cache = let proof, goalno = status in let _, metasenv,subst,_,_, _ = proof in - let signature = MetadataQuery.signature_of metasenv goalno in let equations = retrieve_equations false signature universe cache context metasenv in @@ -1036,7 +1037,7 @@ let apply_smart_aux in match Saturation.solve_narrowing bag (proof'''',newmeta) active passive - 1 (*0 infinity*) + 2 (*0 infinity*) with | None, active, passive, bag -> raise (ProofEngineTypes.Fail (lazy ("paramod fails"))) @@ -1631,18 +1632,27 @@ let try_candidate dbd ;; let applicative_case dbd - tables depth subst fake_proof goalno goalty metasenv context universe - cache flags + tables depth subst fake_proof goalno goalty metasenv context + signature universe cache flags = - let goalty_aux = + (* let goalty_aux = match goalty with | Cic.Appl (hd::tl) -> Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl)) | _ -> goalty - in + 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 -> @@ -1690,10 +1700,9 @@ let try_smart_candidate dbd ;; let smart_applicative_case dbd - tables depth subst fake_proof goalno goalty metasenv context universe - cache flags + tables depth subst fake_proof goalno goalty metasenv context signature + universe cache flags = - let signature = MetadataQuery.signature_of metasenv goalno in let goalty_aux = match goalty with | Cic.Appl (hd::tl) -> @@ -1714,9 +1723,7 @@ let smart_applicative_case dbd (lazy ("smart_candidates" ^ " = " ^ (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in debug_print debug_msg; -(* we only filter the smart candidates since they could be too many let candidates = List.filter (only signature context metasenv) candidates in -*) let smart_candidates = List.filter (only signature context metasenv) smart_candidates in @@ -1759,7 +1766,7 @@ let smart_applicative_case dbd ;; let equational_and_applicative_case dbd - universe flags m s g gty tables cache context + 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 @@ -1774,7 +1781,7 @@ let equational_and_applicative_case dbd else applicative_case dbd tables depth s fake_proof goalno - gty m context universe cache flags + gty m context signature universe cache flags in elems@more_elems, tables, cache, flags else @@ -1782,10 +1789,10 @@ let equational_and_applicative_case dbd match LibraryObjects.eq_URI () with | Some _ -> smart_applicative_case dbd tables depth s fake_proof goalno - gty m context universe cache flags + gty m context signature universe cache flags | None -> applicative_case dbd tables depth s fake_proof goalno - gty m context universe cache flags + gty m context signature universe cache flags in elems, tables, cache, flags ;; @@ -1882,7 +1889,8 @@ let filter_prune_hint c l = cache_reset_underinspection c, List.filter (condition_for_prune_hint prune) l ;; -let auto_main dbd tables context flags universe cache elems = + +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; @@ -1994,7 +2002,7 @@ let auto_main dbd tables context flags universe cache elems = (* elems are possible computations for proving gty *) let elems, tables, cache, flags = equational_and_applicative_case dbd - universe flags m s g gty tables cache context + signature universe flags m s g gty tables cache context in if elems = [] then (* this goal has failed *) @@ -2043,6 +2051,14 @@ let auto_main dbd tables context flags universe cache elems = 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 @@ -2050,7 +2066,7 @@ let in let elems = [metasenv,[],1,[],goals,[]] in let rec aux tables solutions cache elems flags = - match auto_main dbd tables context flags universe cache elems with + match auto_main dbd tables context flags signature universe cache elems with | Gaveup (tables,cache) -> solutions,cache, tables | Proved (metasenv,subst,others,tables,cache) -> @@ -2077,12 +2093,21 @@ let (******************* AUTO ***************) + let auto dbd flags metasenv tables universe cache context metasenv gl = - let initial_time = Unix.gettimeofday() in + 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 universe cache elems with + 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))); @@ -2103,19 +2128,32 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa 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 = + 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 + in let tables,cache = if flags.close_more then close_more tables context (proof, goal) - (auto_all_solutions dbd) universe cache + (auto_all_solutions dbd) signature universe cache else tables,cache in let initial_time = Unix.gettimeofday() in let (_,oldmetasenv,_,_,_, _) = proof in - hint := None; + hint := None; let elem = metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[] in - match auto_main dbd tables context flags universe cache [elem] with + 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)));