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