components/tactics/auto.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 open AutoTypes;;
  27
  28 let debug_print s = ();;(*prerr_endline s;;*)
  29
  30 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
  31 let ugraph = CicUniv.empty_ugraph;;
  32 let typeof = CicTypeChecker.type_of_aux';;
  33 let ppterm ctx t =
  34   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
  35   CicPp.pp t names
  36 ;;
  37 let is_in_prop context subst metasenv ty =
  38   let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
  39   fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
  40 ;;
  41 let assert_proof_is_valid proof metasenv context goalty =
  42   let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
  43   let b,_ = CicReduction.are_convertible context ty goalty u in
  44   if not b then
  45     begin
  46       prerr_endline (CicPp.ppterm proof);
  47       prerr_endline (CicPp.ppterm ty);
  48       prerr_endline (CicPp.ppterm goalty);
  49     end;
  50   assert b
  51 ;;
  52 let assert_subst_are_disjoint subst subst' =
  53   assert(List.for_all
  54     (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
  55     subst)
  56 ;;
  57 let sort_new_elems =
  58   List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
  59 ;;
  60
  61 let split_goals_in_prop metasenv subst gl =
  62   List.partition
  63     (fun g ->
  64       let _,context,ty = CicUtil.lookup_meta g metasenv in
  65       try
  66         let sort,u = typeof ~subst metasenv context ty ugraph in
  67         fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
  68       with
  69       | CicTypeChecker.AssertFailure s
  70       | CicTypeChecker.TypeCheckerFailure s ->
  71           debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
  72           debug_print (Lazy.force s);
  73           false)
  74     (* FIXME... they should type! *)
  75     gl
  76 ;;
  77
  78 let split_goals_with_metas metasenv subst gl =
  79   List.partition
  80     (fun g ->
  81       let _,context,ty = CicUtil.lookup_meta g metasenv in
  82       let ty = CicMetaSubst.apply_subst subst ty in
  83       CicUtil.is_meta_closed ty)
  84     gl
  85 ;;
  86
  87 let order_new_goals metasenv subst open_goals ppterm =
  88   let prop,rest = split_goals_in_prop metasenv subst open_goals in
  89   let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
  90   let open_goals =
  91     (List.map (fun x -> x,P) (closed_prop @ open_prop))
  92     @
  93     (List.map (fun x -> x,T) rest)
  94   in
  95   let tys =
  96     List.map
  97       (fun (i,_) ->
  98         let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals
  99   in
 100   debug_print ("   OPEN: "^
 101     String.concat " "
 102       (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
 103   open_goals
 104 ;;
 105
 106 let try_candidate subst fake_proof goalno depth context cand =
 107   let ppterm = ppterm context in
 108   try
 109     debug_print ("   PROVO: " ^ ppterm cand);
 110     let subst', ((_,metasenv,_,_), open_goals) =
 111       PrimitiveTactics.apply_with_subst ~term:cand ~subst (fake_proof,goalno)
 112     in
 113     debug_print ("   OK: " ^ ppterm cand);
 114     (*FIXME:sicuro che posso @?*)
 115     assert_subst_are_disjoint subst subst';
 116     let subst = subst@subst' in
 117     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 118     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 119     Some (metasenv,subst,open_goals)
 120   with ProofEngineTypes.Fail s -> (*debug_print("   KO: "^Lazy.force s);*)None
 121 ;;
 122
 123 (* Works if there is no dependency over proofs *)
 124 let is_a_green_cut goalty =
 125   CicUtil.is_meta_closed goalty
 126 ;;
 127 let prop = function (_,_,P) -> true | _ -> false;;
 128
 129 let auto_main context flags elems cache universe =
 130   let timeout =
 131     if flags.timeout = 0. then
 132       infinity
 133     else
 134       Unix.gettimeofday () +. flags.timeout
 135   in
 136   let ppterm = ppterm context in
 137   let irl = mk_irl context in
 138   let rec aux cache = function (* elems in OR *)
 139     | [] -> Fail "no more steps can be done", cache (* COMPLETE FAILURE *)
 140     | (metasenv,subst,[])::tl ->
 141         Success (metasenv,subst,tl), cache (* solution::cont *)
 142     | (metasenv,subst,goals)::tl when
 143       List.length (List.filter prop goals) > flags.maxwidth ->
 144         debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
 145         aux cache tl (* FAILURE (width) *)
 146     | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
 147         if Unix.gettimeofday() > timeout then Fail "timeout",cache
 148         else
 149         try
 150           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
 151           debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
 152           if sort = T then
 153             (debug_print (" FAILURE(not in prop)");
 154             aux cache tl (* FAILURE (not in prop) *))
 155           else
 156           match aux_single cache metasenv subst elem goalty cc with
 157           | Fail _, cache ->
 158               debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
 159               let cache = cache_add_failure cache goalty depth in
 160               aux cache tl
 161           | Success (metasenv,subst,others), cache ->
 162               (* others are alternatives in OR *)
 163               try
 164                 let goal = Cic.Meta(goalno,irl) in
 165                 let proof = CicMetaSubst.apply_subst subst goal in
 166                 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
 167                 if is_a_green_cut goalty then
 168                   (assert_proof_is_valid proof metasenv context goalty;
 169                   let cache = cache_add_success cache goalty proof in
 170                   aux cache ((metasenv,subst,gl)::tl))
 171                 else
 172                   (let goalty = CicMetaSubst.apply_subst subst goalty in
 173                   assert_proof_is_valid proof metasenv context goalty;
 174                   let cache =
 175                     if is_a_green_cut goalty then
 176                       cache_add_success cache goalty proof
 177                     else
 178                       cache
 179                   in
 180                   let others =
 181                     List.map
 182                       (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
 183                     others
 184                   in
 185                   aux cache ((metasenv,subst,gl)::others@tl))
 186               with CicUtil.Meta_not_found i when i = goalno ->
 187                 assert false
 188         with CicUtil.Meta_not_found i when i = goalno ->
 189           (* goalno was closed by sideeffect *)
 190           aux cache ((metasenv,subst,gl)::tl)
 191   and aux_single cache metasenv subst (goalno, depth, _) goalty cc =
 192     let goalty = CicMetaSubst.apply_subst subst goalty in
 193 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
 194       (* FAILURE (euristic cut) *)
 195     match cache_examine cache goalty with
 196     | Failed_in d when d >= depth -> Fail "depth",cache(*FAILURE(depth)*)
 197     | Succeded t ->
 198         assert(List.for_all (fun (i,_) -> i <> goalno) subst);
 199         let entry = goalno, (cc, t,goalty) in
 200         assert_subst_are_disjoint subst [entry];
 201         let subst = entry :: subst in
 202         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 203         debug_print ("  CACHE HIT!");
 204         Success (metasenv, subst, []),cache
 205     | UnderInspection -> Fail "looping",cache
 206     | Notfound
 207     | Failed_in _ when depth > 0 -> (* we have more depth now *)
 208         let cache = cache_add_underinspection cache goalty depth in
 209         let candidates = get_candidates universe goalty in
 210         let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
 211         let elems =
 212           HExtlib.filter_map
 213             (try_candidate subst fake_proof goalno depth context)
 214             candidates
 215         in
 216         let elems = sort_new_elems elems in
 217         aux cache elems
 218     | _ -> Fail "??",cache
 219   in
 220     aux cache elems
 221 ;;
 222
 223 let auto universe cache context metasenv gl flags =
 224   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 225   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 226   let elems = [metasenv,[],goals] in
 227   match auto_main context flags elems cache universe with
 228   | Fail s,cache -> prerr_endline s;None,cache
 229   | Success (metasenv,subst,_), cache -> Some (subst,metasenv), cache
 230 ;;
 231
 232 let auto_all_solutions universe cache context metasenv gl flags =
 233   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 234   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 235   let elems = [metasenv,[],goals] in
 236   let bigbang = Unix.gettimeofday () in
 237   let rec aux solutions cache elems flags =
 238     match auto_main context flags elems cache universe with
 239     | Fail s,cache ->prerr_endline s; solutions,cache
 240     | Success (metasenv,subst,others), cache ->
 241         let elapsed = Unix.gettimeofday () -. bigbang in
 242         if elapsed > flags.timeout then
 243           ((subst,metasenv)::solutions), cache
 244         else
 245           aux ((subst,metasenv)::solutions) cache others
 246             {flags with timeout = flags.timeout -. elapsed}
 247   in
 248   aux [] cache elems flags
 249 ;;