X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Flibrary%2FcoercDb.ml;fp=components%2Flibrary%2FcoercDb.ml;h=80222ad341f9d0ae8be79861a64735e03c46cbdc;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml new file mode 100644 index 000000000..80222ad34 --- /dev/null +++ b/components/library/coercDb.ml @@ -0,0 +1,196 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +type coerc_carr = + | Uri of UriManager.uri + | Sort of Cic.sort + | Term of Cic.term + | Fun of int +;; + +exception EqCarrNotImplemented of string Lazy.t +exception EqCarrOnNonMetaClosed + +let db = ref [] + +let coerc_carr_of_term t = + try + match t with + | Cic.Sort s -> Sort s + | Cic.Prod _ -> Fun 0 + (* BUG: this should be the real arity. The computation + requires menv, context etc.., but since carrs are compared discharging Fun + arity... it works *) + | Cic.Appl (t::_) + | t -> Uri (CicUtil.uri_of_term t) + with Invalid_argument _ -> + Term t +;; + +let uri_of_carr = function + | Uri u -> Some u + | _ -> None + +let rec name_of_carr = function + | Uri u -> UriManager.name_of_uri u + | Sort s -> CicPp.ppsort s + | Term (Cic.Appl ((Cic.Const (uri, _))::_)) + | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_)) + | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) -> + UriManager.name_of_uri uri + | Term (Cic.Prod (_,_,t)) -> name_of_carr (Term t) + | Term t -> + prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t); + "FixTheNameMangler" + | Fun i -> "FunClass_" ^ string_of_int i +;; + +let eq_carr ?(exact=false) src tgt = + match src, tgt with + | Uri src, Uri tgt -> + let coarse_eq = UriManager.eq src tgt in + let t = CicUtil.term_of_uri src in + let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in + (match ty, exact with + | Cic.Prod _, true -> false + | Cic.Prod _, false -> coarse_eq + | _ -> coarse_eq) + | Sort (Cic.Type _), Sort (Cic.Type _) -> true + | Sort src, Sort tgt when src = tgt -> true + | Term t1, Term t2 -> + if t1 = t2 then true + else + if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then + raise + (EqCarrNotImplemented + (lazy ("Unsupported carr for coercions: " ^ + CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2))) + else raise EqCarrOnNonMetaClosed + | Fun _,Fun _ -> true (* only one Funclass? *) +(* | Fun i,Fun j when i=j -> true *) + | Term t, _ + | _, Term t when not (CicUtil.is_meta_closed t) -> raise EqCarrOnNonMetaClosed + | _, _ -> false +;; + +let to_list () = + List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db +;; + +let rec myfilter p = function + | [] -> [] + | (s,t,l)::tl -> + let l = + HExtlib.filter_map + (fun (u,n,saturations) -> + if p (s,t,u,saturations) then + if n = 1 then + None + else + Some (u,n-1,saturations) + else + Some (u,n,saturations)) + l + in + if l = [] then myfilter p tl else (s,t,l)::myfilter p tl +;; + +let remove_coercion p = db := myfilter p !db;; + +let find_coercion f = + List.map + (fun uri,_,saturations -> uri,saturations) + (List.flatten + (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db)) +;; + +let get_carr uri = + try + let src, tgt, _ = + List.find + (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq uri x) xl) + !db + in + src, tgt + with Not_found -> assert false (* uri must be a coercion *) +;; + +let is_a_coercion u = + List.exists + (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq u x) xl) + !db +;; + +let is_a_coercion' t = + try + let uri = CicUtil.uri_of_term t in + is_a_coercion uri + with Invalid_argument _ -> false +;; + +let is_a_coercion_to_funclass t = + try + let uri = CicUtil.uri_of_term t in + match snd (get_carr uri) with + | Fun i -> Some i + | _ -> None + with Invalid_argument _ -> None + + +let term_of_carr = function + | Uri u -> CicUtil.term_of_uri u + | Sort s -> Cic.Sort s + | Fun _ -> assert false + | Term _ -> assert false +;; + +let add_coercion (src,tgt,u,saturations) = + let f s t = eq_carr s src && eq_carr t tgt in + let where = List.filter (fun (s,t,_) -> f s t) !db in + let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in + match where with + | [] -> db := (src,tgt,[u,1,saturations]) :: !db + | (src,tgt,l)::tl -> + assert (tl = []); (* not sure, this may be a feature *) + if List.exists (fun (x,_,_) -> UriManager.eq u x) l then + let l' = List.map + (fun (x,n,saturations') -> + if UriManager.eq u x then + (x,n+1,saturations) + else + (x,n,saturations)) + l + in + db := (src,tgt,l')::tl @ rest + else + db := (src,tgt,(u,1,saturations)::l)::tl @ rest + +;; + +type coerc_db = (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list +let dump () = !db +let restore coerc_db = db := coerc_db