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 module Codomain = struct
  27   type t = Cic.term
  28   let compare = Pervasives.compare
  29 end
  30 module S = Set.Make(Codomain)
  31 module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
  32 type universe = TI.t
  33 (* (proof,ty) list *)
  34 type cache_key = Cic.term
  35 type cache_elem =
  36   | Failed_in of int
  37   | Succeded of Cic.term
  38   | UnderInspection
  39   | Notfound
  40 type cache = (universe * ((cache_key * cache_elem) list));;
  41
  42 let cache_empty = (TI.empty,[]);;
  43 let get_candidates (univ,_) ty =
  44   S.elements (TI.retrieve_unifiables univ ty)
  45 ;;
  46
  47 let rec unfold context = function
  48   | Cic.Prod(name,s,t) ->
  49       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
  50         Cic.Prod(name,s,t')
  51   | t -> ProofEngineReduction.unfold context t
  52
  53
  54 let rec collapse_head_metas = function
  55   | Cic.Appl(a::l) ->
  56       let a' = collapse_head_metas a in
  57       (match a' with
  58         | Cic.Meta(n,m) -> Cic.Meta(n,m)
  59         | t ->
  60             let l' = List.map collapse_head_metas l in
  61                Cic.Appl(t::l'))
  62   | t -> t
  63 ;;
  64
  65 let rec head t =
  66   let rec aux = function
  67   | Cic.Prod(_,_,t) ->
  68       CicSubstitution.subst (Cic.Meta (-1,[])) (aux t)
  69   | t -> t
  70   in collapse_head_metas (aux t)
  71 ;;
  72
  73 let index (univ,oldcache) key term =
  74   prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
  75   (TI.index univ key term,oldcache)
  76 ;;
  77
  78 let index_term_and_unfolded_term cache context t ty =
  79   let key = head ty in
  80   let cache = index cache key t in
  81   try
  82     let key = head (unfold context ty) in
  83     index cache key t
  84   with ProofEngineTypes.Fail _ -> cache
  85 ;;
  86
  87 let cache_add_list cache context terms_and_types =
  88   List.fold_left
  89     (fun acc (term,ty) ->
  90        index_term_and_unfolded_term acc context term ty)
  91     cache terms_and_types
  92
  93 let cache_examine (_,oldcache) cache_key =
  94   try List.assoc cache_key oldcache with Not_found -> Notfound
  95 ;;
  96 let cache_replace (univ,oldcache) key v =
  97   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
  98   univ, (key,v)::oldcache
  99 ;;
 100 let cache_remove (univ,oldcache) key =
 101   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
 102   univ,oldcache
 103 ;;
 104 let cache_add_failure cache cache_key depth =
 105   match cache_examine cache cache_key with
 106   | Failed_in i when i > depth -> cache
 107   | Notfound
 108   | Failed_in _
 109   | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
 110   | Succeded t ->
 111       prerr_endline (CicPp.ppterm t);
 112       assert false (* if succed it can't fail *)
 113 ;;
 114 let cache_add_success ((univ,_) as cache) cache_key proof =
 115   TI.index univ cache_key proof,snd
 116   (match cache_examine cache cache_key with
 117   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
 118   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
 119   | Succeded t -> (* we may decide to keep the smallest proof *) cache
 120   | Notfound -> cache_replace cache cache_key (Succeded proof))
 121 ;;
 122 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
 123   match cache_examine cache cache_key with
 124   | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
 125   | Notfound -> univ,(cache_key,UnderInspection)::oldcache
 126   | Failed_in _
 127   | UnderInspection
 128   | Succeded _ -> assert false (* it must be a new goal *)
 129 ;;
 130 let cache_print context (_,oldcache) =
 131   let names = List.map (function None -> None | Some (x,_) -> Some x) context in
 132   String.concat "\n"
 133     (HExtlib.filter_map
 134       (function
 135         | (k,Succeded _) -> Some (CicPp.pp k names)
 136         | _ -> None)
 137       oldcache)
 138 ;;
 139 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
 140   match cache_examine cache cache_key with
 141   | Notfound
 142   | UnderInspection ->  cache_remove cache cache_key
 143   | Failed_in _ -> assert false
 144   | Succeded _ -> 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 ;;