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