1 (* Copyright (C) 2002, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
27 module Codomain = struct
29 let compare = Pervasives.compare
31 module S = Set.Make(Codomain)
32 module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
35 let empty_universe = TI.empty
36 let get_candidates universe ty =
37 S.elements (TI.retrieve_unifiables universe ty)
39 let rec head = function
40 | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
43 let index acc key term =
47 prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
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
56 let key = head (tyof term) in
60 let universe_of_context ctx metasenv universe =
61 let tail = function [] -> [] | h::tl -> tl in
64 (fun (acc,i,ctx) ctxentry ->
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)) ->
77 CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph
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)
89 type cache_key = Cic.term
92 | Succeded of Cic.term
95 type cache = (cache_key * cache_elem) list
96 let cache_examine cache cache_key =
97 try List.assoc cache_key cache with Not_found -> Notfound
99 let cache_replace cache key v =
100 let cache = List.filter (fun (i,_) -> i <> key) cache in
103 let cache_add_failure cache cache_key depth =
104 match cache_examine cache cache_key with
105 | Failed_in i when i > depth -> cache
108 | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
110 prerr_endline (CicPp.ppterm t);
111 assert false (* if succed it can't fail *)
113 let cache_add_success cache cache_key proof =
114 match cache_examine cache cache_key with
115 | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
116 | UnderInspection -> cache_replace cache cache_key (Succeded proof)
117 | Succeded t -> (* we may decide to keep the smallest proof *) cache
118 | Notfound -> cache_replace cache cache_key (Succeded proof)
120 let cache_add_underinspection cache cache_key depth =
121 match cache_examine cache cache_key with
122 | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
123 | Notfound -> (cache_key,UnderInspection)::cache
126 | Succeded _ -> assert false (* it must be a new goal *)
136 let default_flags = {
142 (* (metasenv, subst, (metano,depth)list *)
144 type and_elem = Cic.metasenv * Cic.substitution * (int * int * sort) list
147 | Success of Cic.metasenv * Cic.substitution * and_elem list