components/tactics/autoCache.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 type cache_key = Cic.term
  27 type cache_elem =
  28   | Failed_in of int
  29   | Succeded of Cic.term
  30   | UnderInspection
  31   | Notfound
  32 type cache = (Universe.universe * ((cache_key * cache_elem) list));;
  33
  34 let debug = false;;
  35 let prerr_endline s =
  36   if debug then prerr_endline s else ()
  37 ;;
  38
  39 let cache_empty = (Universe.empty,[]);;
  40
  41 let get_candidates (univ,_) ty =
  42 (*   if Universe.key ty = ty then *)
  43     Universe.get_candidates univ ty
  44 (*
  45   else
  46     (prerr_endline ("skip: " ^ CicPp.ppterm (Universe.key ty)); [])
  47  *)
  48 ;;
  49
  50 let index (univ,cache) key term =
  51   Universe.index univ key term,cache
  52 ;;
  53
  54 let index_term_and_unfolded_term (univ,cache) context t ty =
  55   Universe.index_local_term univ context t ty, cache
  56 ;;
  57
  58 let cache_add_list (univ,cache) context terms_and_types =
  59   let univ =
  60     List.fold_left
  61       (fun univ (t,ty) ->
  62          prerr_endline ("indexing: " ^ CicPp.ppterm ty);
  63          Universe.index_local_term univ context t ty)
  64       univ terms_and_types
  65   in
  66   univ, cache
  67
  68 let cache_examine (_,oldcache) cache_key =
  69   prerr_endline ("examine : " ^ CicPp.ppterm cache_key);
  70   try snd (List.find (fun (x,_) -> CicUtil.alpha_equivalence x cache_key)
  71         oldcache) with Not_found ->
  72     prerr_endline "notfound";
  73     Notfound
  74 ;;
  75 let cache_replace (univ,oldcache) key v =
  76   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
  77   univ, (key,v)::oldcache
  78 ;;
  79 let cache_remove (univ,oldcache) key =
  80   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
  81   univ,oldcache
  82 ;;
  83 let cache_add_failure cache cache_key depth =
  84   prerr_endline
  85     ("CACHE: ADD FAIL " ^ CicPp.ppterm cache_key ^
  86       " depth: " ^ string_of_int depth);
  87   match cache_examine cache cache_key with
  88   | Failed_in i when i > depth -> cache
  89   | Notfound
  90   | Failed_in _
  91   | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
  92   | Succeded t -> cache
  93                   (*
  94       prerr_endline (CicPp.ppterm t);
  95       assert false (* if succed it can't fail *) *)
  96 ;;
  97 let cache_add_success ((univ,_) as cache) cache_key proof =
  98   let u_key = Universe.key cache_key in
  99   if u_key <> cache_key then
 100     Universe.index univ u_key proof, snd cache
 101   else
 102     univ,
 103     snd
 104     (match cache_examine cache cache_key with
 105     | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
 106     | UnderInspection -> cache_replace cache cache_key (Succeded proof)
 107     | Succeded t -> (* we may decide to keep the smallest proof *) cache
 108     | Notfound -> cache_replace cache cache_key (Succeded proof))
 109 (*
 110   (if Universe.key cache_key = cache_key then
 111     Universe.index univ cache_key proof
 112   else
 113     univ),snd
 114   (prerr_endline ("CACHE: ADD SUCCESS" ^ CicPp.ppterm cache_key);
 115   match cache_examine cache cache_key with
 116   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
 117   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
 118   | Succeded t -> (* we may decide to keep the smallest proof *) cache
 119   | Notfound -> cache_replace cache cache_key (Succeded proof))
 120 ;;
 121 *)
 122 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
 123   prerr_endline ("CACHE: ADD INSPECTING" ^ CicPp.ppterm cache_key);
 124   match cache_examine cache cache_key with
 125   | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
 126   | Notfound -> univ,(cache_key,UnderInspection)::oldcache
 127   | Failed_in _
 128   | UnderInspection
 129   | Succeded _ -> assert false (* it must be a new goal *)
 130 ;;
 131 let cache_print context (_,oldcache) =
 132   let names = List.map (function None -> None | Some (x,_) -> Some x) context in
 133   String.concat "\n"
 134     (HExtlib.filter_map
 135       (function
 136         | (k,Succeded _) -> Some ("CACHE SUCCESS: " ^ CicPp.pp k names)
 137         | _ -> None)
 138       oldcache)
 139 ;;
 140 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
 141   prerr_endline ("CACHE: REMOVE INSPECTING" ^ CicPp.ppterm cache_key);
 142   match cache_examine cache cache_key with
 143   | Notfound
 144   | Failed_in _ (* -> assert false  *)
 145   | UnderInspection ->  cache_remove cache cache_key
 146   | Succeded _ -> cache (*
 147       prerr_endline (CicPp.ppterm cache_key);
 148       assert false (* it must be a new goal *) *)
 149 ;;
 150 let cache_size (_,oldcache) =
 151   List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
 152 ;;
 153 let cache_clean (univ,oldcache) =
 154   univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache
 155 ;;