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
  35 let cache_empty = (Universe.empty,[]);;
  36
  37 let get_candidates (univ,_) ty =
  38   if Universe.key ty = ty then
  39     Universe.get_candidates univ ty
  40   else
  41     []
  42 ;;
  43
  44 let index (univ,cache) key term =
  45   Universe.index univ key term,cache
  46 ;;
  47
  48 let index_term_and_unfolded_term (univ,cache) context t ty =
  49   Universe.index_local_term univ context t ty, cache
  50 ;;
  51
  52 let cache_add_list (univ,cache) context terms_and_types =
  53   let univ =
  54     List.fold_left
  55       (fun univ (t,ty) ->
  56          Universe.index_local_term univ context t ty)
  57       univ terms_and_types
  58   in
  59   univ, cache
  60
  61 let cache_examine (_,oldcache) cache_key =
  62   try List.assoc cache_key oldcache with Not_found -> Notfound
  63 ;;
  64 let cache_replace (univ,oldcache) key v =
  65   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
  66   univ, (key,v)::oldcache
  67 ;;
  68 let cache_remove (univ,oldcache) key =
  69   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
  70   univ,oldcache
  71 ;;
  72 let cache_add_failure cache cache_key depth =
  73   match cache_examine cache cache_key with
  74   | Failed_in i when i > depth -> cache
  75   | Notfound
  76   | Failed_in _
  77   | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
  78   | Succeded t ->
  79       prerr_endline (CicPp.ppterm t);
  80       assert false (* if succed it can't fail *)
  81 ;;
  82 let cache_add_success ((univ,_) as cache) cache_key proof =
  83   (if Universe.key cache_key = cache_key then
  84     Universe.index univ cache_key proof
  85   else
  86     univ),snd
  87   (match cache_examine cache cache_key with
  88   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
  89   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
  90   | Succeded t -> (* we may decide to keep the smallest proof *) cache
  91   | Notfound -> cache_replace cache cache_key (Succeded proof))
  92 ;;
  93 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
  94   match cache_examine cache cache_key with
  95   | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
  96   | Notfound -> univ,(cache_key,UnderInspection)::oldcache
  97   | Failed_in _
  98   | UnderInspection
  99   | Succeded _ -> assert false (* it must be a new goal *)
 100 ;;
 101 let cache_print context (_,oldcache) =
 102   let names = List.map (function None -> None | Some (x,_) -> Some x) context in
 103   String.concat "\n"
 104     (HExtlib.filter_map
 105       (function
 106         | (k,Succeded _) -> Some (CicPp.pp k names)
 107         | _ -> None)
 108       oldcache)
 109 ;;
 110 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
 111   match cache_examine cache cache_key with
 112   | Notfound
 113   | UnderInspection ->  cache_remove cache cache_key
 114   | Failed_in _ -> assert false
 115   | Succeded _ -> assert false (* it must be a new goal *)
 116 ;;
 117 let cache_size (_,oldcache) =
 118   List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
 119 ;;
 120 let cache_clean (univ,oldcache) =
 121   univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache
 122 ;;