helm/software/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 let rec head = function
  47   | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
  48   | t -> t
  49 ;;
  50 let index ((univ,oldcache) as cache) key term =
  51   match key with
  52   | Cic.Meta _ -> cache
  53   | _ ->
  54       prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
  55       (TI.index univ key term,oldcache)
  56 ;;
  57 let cache_add_library dbd proof gl cache =
  58   let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
  59   let terms = List.map CicUtil.term_of_uri univ in
  60   let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in
  61   List.fold_left
  62     (fun acc term ->
  63       let key = head (tyof term) in
  64       index acc key term)
  65     cache terms
  66 ;;
  67 let cache_add_context ctx metasenv cache =
  68   let tail = function [] -> [] | h::tl -> tl in
  69   let rc,_,_ =
  70     List.fold_left
  71     (fun (acc,i,ctx) ctxentry ->
  72       match ctxentry with
  73       | Some (_,Cic.Decl t) ->
  74           let key = CicSubstitution.lift i (head t) in
  75           let elem = Cic.Rel i in
  76           index acc key elem, i+1, tail ctx
  77       | Some (_,Cic.Def (_,Some t)) ->
  78           let key = CicSubstitution.lift i (head t) in
  79           let elem = Cic.Rel i in
  80           index acc key elem, i+1, tail ctx
  81       | Some (_,Cic.Def (t,None)) ->
  82           let ctx = tail ctx in
  83           let key,_ =
  84             CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph
  85           in
  86           let elem = Cic.Rel i in
  87           let key = CicSubstitution.lift i (head key) in
  88           index acc key elem, i+1, ctx
  89       |  _ -> acc,i+1,tail ctx)
  90     (cache,1,ctx) ctx
  91   in
  92   rc
  93 ;;
  94
  95 let cache_examine (_,oldcache) cache_key =
  96   try List.assoc cache_key oldcache with Not_found -> Notfound
  97 ;;
  98 let cache_replace (univ,oldcache) key v =
  99   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
 100   univ, (key,v)::oldcache
 101 ;;
 102 let cache_remove (univ,oldcache) key =
 103   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
 104   univ,oldcache
 105 ;;
 106 let cache_add_failure cache cache_key depth =
 107   match cache_examine cache cache_key with
 108   | Failed_in i when i > depth -> cache
 109   | Notfound
 110   | Failed_in _
 111   | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
 112   | Succeded t ->
 113       prerr_endline (CicPp.ppterm t);
 114       assert false (* if succed it can't fail *)
 115 ;;
 116 let cache_add_success ((univ,_) as cache) cache_key proof =
 117   TI.index univ cache_key proof,snd
 118   (match cache_examine cache cache_key with
 119   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
 120   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
 121   | Succeded t -> (* we may decide to keep the smallest proof *) cache
 122   | Notfound -> cache_replace cache cache_key (Succeded proof))
 123 ;;
 124 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
 125   match cache_examine cache cache_key with
 126   | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
 127   | Notfound -> univ,(cache_key,UnderInspection)::oldcache
 128   | Failed_in _
 129   | UnderInspection
 130   | Succeded _ -> assert false (* it must be a new goal *)
 131 ;;
 132 let cache_print context (_,oldcache) =
 133   let names = List.map (function None -> None | Some (x,_) -> Some x) context in
 134   String.concat "\n"
 135     (HExtlib.filter_map
 136       (function
 137         | (k,Succeded _) -> Some (CicPp.pp k names)
 138         | _ -> None)
 139       oldcache)
 140 ;;
 141 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
 142   match cache_examine cache cache_key with
 143   | Notfound
 144   | UnderInspection ->  cache_remove cache cache_key
 145   | Failed_in _ -> assert false
 146   | Succeded _ -> assert false (* it must be a new goal *)
 147 ;;
 148 let cache_size (_,oldcache) =
 149   List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
 150 ;;
 151 let cache_clean (univ,oldcache) =
 152   univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache
 153 ;;