components/tactics/autoTypes.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
  27 module Codomain = struct
  28   type t = Cic.term
  29   let compare = Pervasives.compare
  30 end
  31 module S = Set.Make(Codomain)
  32 module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
  33 type universe = TI.t
  34
  35 let empty_universe = TI.empty
  36 let get_candidates universe ty =
  37   S.elements (TI.retrieve_unifiables universe ty)
  38 ;;
  39 let rec head = function
  40   | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
  41   | t -> t
  42 ;;
  43 let index acc key term =
  44   match key with
  45   | Cic.Meta _ -> acc
  46   | _ ->
  47       prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
  48       TI.index acc key term
  49 ;;
  50 let universe_of_goals dbd proof gl universe =
  51   let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
  52   let terms = List.map CicUtil.term_of_uri univ in
  53   let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in
  54   List.fold_left
  55     (fun acc term ->
  56       let key = head (tyof term) in
  57       index acc key term)
  58     universe terms
  59 ;;
  60 let universe_of_context ctx metasenv universe =
  61   let tail = function [] -> [] | h::tl -> tl in
  62   let rc,_,_ =
  63     List.fold_left
  64     (fun (acc,i,ctx) ctxentry ->
  65       match ctxentry with
  66       | Some (_,Cic.Decl t) ->
  67           let key = CicSubstitution.lift i (head t) in
  68           let elem = Cic.Rel i in
  69           index acc key elem, i+1, tail ctx
  70       | Some (_,Cic.Def (_,Some t)) ->
  71           let key = CicSubstitution.lift i (head t) in
  72           let elem = Cic.Rel i in
  73           index acc key elem, i+1, tail ctx
  74       | Some (_,Cic.Def (t,None)) ->
  75           let ctx = tail ctx in
  76           let key,_ =
  77             CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph
  78           in
  79           let elem = Cic.Rel i in
  80           let key = CicSubstitution.lift i (head key) in
  81           index acc key elem, i+1, ctx
  82       |  _ -> universe,i+1,tail ctx)
  83     (universe,1,ctx) ctx
  84   in
  85   rc
  86 ;;
  87 let add_to_universe key proof universe =
  88   index universe key proof
  89 ;;
  90
  91 (* (proof,ty) list *)
  92 type cache_key = Cic.term
  93 type cache_elem =
  94   | Failed_in of int
  95   | Succeded of Cic.term
  96   | UnderInspection
  97   | Notfound
  98 type cache = (cache_key * cache_elem) list
  99 let cache_examine cache cache_key =
 100   try List.assoc cache_key cache with Not_found -> Notfound
 101 ;;
 102 let cache_replace cache key v =
 103   let cache = List.filter (fun (i,_) -> i <> key) cache in
 104   (key,v)::cache
 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 cache cache_key proof =
 117   match cache_examine cache cache_key with
 118   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
 119   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
 120   | Succeded t -> (* we may decide to keep the smallest proof *) cache
 121   | Notfound -> cache_replace cache cache_key (Succeded proof)
 122 ;;
 123 let cache_add_underinspection cache cache_key depth =
 124   match cache_examine cache cache_key with
 125   | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
 126   | Notfound -> (cache_key,UnderInspection)::cache
 127   | Failed_in _
 128   | UnderInspection
 129   | Succeded _ -> assert false (* it must be a new goal *)
 130 ;;
 131 let cache_empty = []
 132 let cache_print context cache =
 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       cache)
 140 ;;
 141 let cache_size cache =
 142   List.length (List.filter (function (_,Succeded _) -> true | _ -> false) cache)
 143 ;;
 144 let cache_clean cache =
 145   List.filter (function (_,Succeded _) -> true | _ -> false) cache
 146 ;;
 147
 148 type flags = {
 149   maxwidth: int;
 150   maxdepth: int;
 151   timeout: float;
 152   use_paramod: bool;
 153   use_only_paramod : bool;
 154 }
 155
 156 let default_flags _ =
 157   {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. 3.0;use_paramod=true;use_only_paramod=false}
 158 ;;
 159
 160 (* (metasenv, subst, (metano,depth)list *)
 161 type sort = P | T;;
 162 type and_elem =  Cic.metasenv * Cic.substitution * (int * int * sort) list
 163 type auto_result =
 164   | Fail of string
 165   | Success of Cic.metasenv * Cic.substitution * and_elem list
 166