From 1997c9713a0f75ec65803cc8132223142df98204 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 23 Nov 2006 14:09:08 +0000 Subject: [PATCH] Universe is a discrimination-tree structure. --- components/tactics/universe.ml | 148 ++++++++++++++++++++++++++++++++ components/tactics/universe.mli | 44 ++++++++++ 2 files changed, 192 insertions(+) create mode 100644 components/tactics/universe.ml create mode 100644 components/tactics/universe.mli diff --git a/components/tactics/universe.ml b/components/tactics/universe.ml new file mode 100644 index 000000000..40c3c1abd --- /dev/null +++ b/components/tactics/universe.ml @@ -0,0 +1,148 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module Codomain = struct + type t = Cic.term + let compare = Pervasives.compare +end +module S = Set.Make(Codomain) +module TI = Discrimination_tree.DiscriminationTreeIndexing(S) +type universe = TI.t + +let empty = TI.empty +;; + +let get_candidates univ ty = + S.elements (TI.retrieve_unifiables univ ty) +;; + +let rec unfold context = function + | Cic.Prod(name,s,t) -> + let t' = unfold ((Some (name,Cic.Decl s))::context) t in + Cic.Prod(name,s,t') + | t -> ProofEngineReduction.unfold context t + +let rec collapse_head_metas = function + | Cic.Appl(a::l) -> + let a' = collapse_head_metas a in + (match a' with + | Cic.Meta(n,m) -> Cic.Meta(n,m) + | t -> + let l' = List.map collapse_head_metas l in + Cic.Appl(t::l')) + | t -> t +;; + +let rec dummies_of_coercions = + function + | Cic.Appl (c::l) when CoercGraph.is_a_coercion c -> + Cic.Meta (-1,[]) + | Cic.Appl l -> + let l' = List.map dummies_of_coercions l in Cic.Appl l' + | Cic.Lambda(n,s,t) -> + let s' = dummies_of_coercions s in + let t' = dummies_of_coercions t in + Cic.Lambda (n,s',t') + | Cic.Prod(n,s,t) -> + let s' = dummies_of_coercions s in + let t' = dummies_of_coercions t in + Cic.Prod (n,s',t') + | Cic.LetIn(n,s,t) -> + let s' = dummies_of_coercions s in + let t' = dummies_of_coercions t in + Cic.LetIn (n,s',t') + | Cic.MutCase _ -> prerr_endline "mutcase";Cic.Meta (-1,[]) + | t -> t +;; + +let rec head remove_coercions t = + let clean_up t = + if remove_coercions then dummies_of_coercions t + else t in + let rec aux = function + | Cic.Prod(_,_,t) -> + CicSubstitution.subst (Cic.Meta (-1,[])) (aux t) + | t -> t + in collapse_head_metas (clean_up (aux t)) +;; + + +let index univ key term = + (* flexible terms are not indexed *) + if key = Cic.Meta(-1,[]) then univ + else + (prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term); + TI.index univ key term) +;; + +let keys context ty = + try + [head true ty; head true (unfold context ty)] + with ProofEngineTypes.Fail _ -> [head true ty] + +let index_term_and_unfolded_term univ context t ty = + let key = head true ty in + let univ = index univ key t in + try + let key = head true (unfold context ty) in + index univ key t + with ProofEngineTypes.Fail _ -> univ +;; + +let index_local_term univ context t ty = + let key = head true ty in + let univ = index univ key t in + let key1 = head false ty in + let univ = + if key<>key1 then index univ key1 t else univ in + try + let key = head true (unfold context ty) in + index univ key t + with ProofEngineTypes.Fail _ -> univ +;; + + +let index_list univ context terms_and_types = + List.fold_left + (fun acc (term,ty) -> + index_term_and_unfolded_term acc context term ty) + univ terms_and_types + +;; + +let remove univ context term ty = + let key = head true ty in + let univ = TI.remove_index univ key term in + try + let key = head true (unfold context ty) in + TI.remove_index univ key term + with ProofEngineTypes.Fail _ -> univ + +let remove_uri univ uri = + let term = CicUtil.term_of_uri uri in + let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in + remove univ [] term ty + + diff --git a/components/tactics/universe.mli b/components/tactics/universe.mli new file mode 100644 index 000000000..4ae0ff961 --- /dev/null +++ b/components/tactics/universe.mli @@ -0,0 +1,44 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type universe +val empty : universe +val get_candidates: universe -> Cic.term -> Cic.term list +val index: + universe -> + Cic.term -> (* key *) + Cic.term -> (* value *) + universe +val keys: Cic.context -> Cic.term -> Cic.term list +val index_term_and_unfolded_term: + universe -> Cic.context -> Cic.term -> Cic.term -> universe +val index_local_term: + universe -> Cic.context -> Cic.term -> Cic.term -> universe +val index_list: + universe -> Cic.context -> (Cic.term*Cic.term) list -> universe +val remove: + universe -> Cic.context -> Cic.term -> Cic.term -> universe +val remove_uri: + universe -> UriManager.uri -> universe -- 2.39.2