X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.ml;h=b7e3902296fc986edbffe93a7f5a161542c33e62;hb=433d9c9612c1557e03a549e004c796c1137d4b4a;hp=e0dc18d05f7146e9bf0125265eb9ef4aaa41e660;hpb=5da42f6120f3075c3da8ab3082ead39ea57955fa;p=helm.git diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml index e0dc18d05..b7e390229 100644 --- a/helm/software/components/library/coercDb.ml +++ b/helm/software/components/library/coercDb.ml @@ -25,81 +25,68 @@ (* $Id$ *) +let debug = false +let debug_print = + if debug then fun x -> prerr_endline (Lazy.force x) + else ignore +;; + type coerc_carr = | Uri of UriManager.uri | Sort of Cic.sort - | Term of Cic.term | Fun of int + | Dead ;; -exception EqCarrNotImplemented of string Lazy.t -exception EqCarrOnNonMetaClosed +type saturations = int +type coerced_pos = int +type coercion_entry = + coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos + +type coerc_db = (* coercion_entry grouped by carrier with molteplicity *) + (coerc_carr * coerc_carr * + (UriManager.uri * int * saturations * coerced_pos) list) list -let db = ref [] +let db = ref ([] : coerc_db) +let dump () = !db +let restore coerc_db = db := coerc_db +let empty_coerc_db = [] -let coerc_carr_of_term t = +let rec coerc_carr_of_term t a = try - match t with - | Cic.Sort s -> Sort s - | Cic.Prod _ -> assert false - | Cic.Appl (t::_) - | t -> Uri (CicUtil.uri_of_term t) - with Invalid_argument _ -> - Term t + match t, a with + | Cic.Sort s, 0 -> Sort s + | Cic.Appl (t::_), 0 -> coerc_carr_of_term t a + | t, 0 -> Uri (CicUtil.uri_of_term t) + | _, n -> Fun n + with Invalid_argument _ -> Dead ;; -let uri_of_carr = function - | Uri u -> Some u - | _ -> None - -let rec name_of_carr = function +let string_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 + | Dead -> "UnsupportedCarrier" ;; let eq_carr ?(exact=false) src tgt = match src, tgt with | Uri src, Uri tgt -> let coarse_eq = UriManager.eq src tgt in - let src_noxpointer = UriManager.strip_xpointer src in - if exact && coarse_eq && UriManager.uri_is_ind src_noxpointer then - match - fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph src_noxpointer) - with - | Cic.InductiveDefinition (_,[],m,_) when m = 0 -> true - | Cic.Constant _ -> true - | _ -> false - else - 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 + 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 _, Sort _ -> true + | Fun _,Fun _ when not exact -> true (* only one Funclass *) + | Fun i,Fun j when i = j -> true (* only one Funclass *) | _, _ -> false ;; -let to_list () = - List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db +let to_list db = + List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db ;; let rec myfilter p = function @@ -107,14 +94,11 @@ 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)) + (fun (u,n,saturations,cpos) as e -> + if p (s,t,u,saturations,cpos) then + if n = 1 then None + else Some (u,n-1,saturations,cpos) + else Some e) l in if l = [] then myfilter p tl else (s,t,l)::myfilter p tl @@ -123,72 +107,69 @@ let rec myfilter p = function let remove_coercion p = db := myfilter p !db;; let find_coercion f = - List.map - (fun uri,_,saturations -> uri,saturations) - (List.flatten + 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 = +let is_a_coercion t = try - let uri = CicUtil.uri_of_term t in - is_a_coercion uri - with Invalid_argument _ -> false + let uri = CicUtil.uri_of_term t in + match + HExtlib.filter_map + (fun (src,tgt,xl) -> + let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in + if xl = [] then None else Some (src,tgt,xl)) + !db + with + | [] -> None + | (_,_,[])::_ -> assert false + | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p) + | (src,tgt,(u,_,s,p)::_)::_ -> + debug_print + (lazy "coercion has multiple entries, returning the first one"); + Some (src,tgt,u,s,p) + with Invalid_argument _ -> + debug_print (lazy "this term is not a constant"); + None ;; -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 add_coercion (src,tgt,u,saturations,cpos) = 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 + | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !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') -> - assert (saturations=saturations'); + if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then + let l = + let l = + (* this code reorders the list so that adding an already declared + * coercion moves it to the begging of the list *) + let item = List.find (fun (x,_,_,_) -> UriManager.eq u x) l in + let rest=List.filter (fun (x,_,_,_) -> not (UriManager.eq u x)) l in + item :: rest + in + List.map + (fun (x,n,x_saturations,x_cpos) as e -> if UriManager.eq u x then - (x,n+1,saturations) - else - (x,n,saturations)) + (* not sure, this may be a feature *) + (assert (x_saturations = saturations && x_cpos = cpos); + (x,n+1,saturations,cpos)) + else e) l in - db := (src,tgt,l')::tl @ rest + db := (src,tgt,l)::tl @ rest else - db := (src,tgt,(u,1,saturations)::l)::tl @ rest - + db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest +;; + +let prefer u = + let prefer (s,t,l) = + let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in + s,t,lb@la + in + db := List.map prefer !db; ;;