helm/software/components/tactics/automationCache.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 tables =
  27   Saturation.active_table * Saturation.passive_table * Equality.equality_bag
  28
  29 type cache = {
  30         univ : Universe.universe;
  31         tables : Saturation.active_table *
  32                  Saturation.passive_table *
  33                  Equality.equality_bag;
  34 }
  35
  36 let empty_tables () =
  37   Saturation.make_active [],
  38   Saturation.make_passive [],
  39   Equality.mk_equality_bag ()
  40 ;;
  41
  42 let empty () = {
  43         univ = Universe.empty;
  44         tables = empty_tables ();
  45 }
  46
  47 let pump cache steps =
  48   let active, passive, bag = cache.tables in
  49   let active, passive, bag =
  50     Saturation.pump_actives
  51       [] bag active passive steps infinity
  52   in
  53   let tables = active, passive, bag in
  54   { cache with tables = tables }
  55 ;;
  56
  57 let add_term_to_active cache metasenv subst context t ty_opt =
  58   let actives, passives, bag = cache.tables in
  59   let bag, metasenv, head, t, args, mes, ugraph =
  60     match ty_opt with
  61     | Some ty ->
  62         bag, metasenv, ty, t, [], (CicUtil.metas_of_term (Cic.Appl [t;ty])),
  63         CicUniv.oblivion_ugraph
  64     | None ->
  65         let ty, ugraph =
  66           CicTypeChecker.type_of_aux'
  67             ~subst metasenv context t CicUniv.oblivion_ugraph
  68         in
  69         let bag, head, metasenv, args =
  70           Equality.saturate_term bag metasenv subst context ty
  71         in
  72         let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in
  73         let t = if args = [] then t else Cic.Appl (t:: args) in
  74         bag, metasenv, head, t, args, mes, ugraph
  75   in
  76   if List.exists
  77       (function
  78       | Cic.Meta(i,_) ->
  79           (try
  80             let _,mc, mt = CicUtil.lookup_meta i metasenv in
  81             let sort, u =
  82                CicTypeChecker.type_of_aux' metasenv mc mt ugraph
  83             in
  84             fst (CicReduction.are_convertible mc sort (Cic.Sort Cic.Prop) u)
  85           with
  86           | CicUtil.Meta_not_found _ -> false)
  87       | _ -> assert false)
  88      args
  89   then
  90     cache
  91   else
  92     let env = metasenv, context, CicUniv.oblivion_ugraph in
  93     let newmetas =
  94       List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv
  95     in
  96     let tables =
  97       Saturation.add_to_active bag actives passives env head t newmetas
  98     in
  99     { cache with tables = tables }
 100 ;;
 101
 102 let pp_cache cache =
 103   prerr_endline "Automation cache";
 104   prerr_endline "----------------------------------------------";
 105   prerr_endline "universe:";
 106   Universe.iter cache.univ (fun _ ts ->
 107     prerr_endline (" "^
 108       String.concat "\n " (List.map CicPp.ppterm ts)));
 109   prerr_endline "tables/actives:";
 110   let active, passive, _ = cache.tables in
 111   List.iter
 112     (fun e -> prerr_endline (" " ^ Equality.string_of_equality e))
 113     (Saturation.list_of_active active);
 114   prerr_endline "tables/passives:";
 115   List.iter
 116     (fun e -> prerr_endline (" " ^ Equality.string_of_equality e))
 117     (Saturation.list_of_passive passive);
 118   prerr_endline "----------------------------------------------";
 119 ;;