X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcoercGraph.ml;h=355c8019a80401f055b559f99f5352e154ea4022;hb=2951babfd31047ac057714130157da2bc36e906e;hp=06d7a12d3ea3a5e250ae595dc747d906e75b0857;hpb=27b3610b7add7ee75eb25f8f01e0f1426c278f52;p=helm.git diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml index 06d7a12d3..355c8019a 100644 --- a/components/library/coercGraph.ml +++ b/components/library/coercGraph.ml @@ -28,7 +28,7 @@ open Printf;; type coercion_search_result = - | SomeCoercion of Cic.term + | SomeCoercion of Cic.term list | NoCoercion | NotMetaClosed | NotHandled of string Lazy.t @@ -37,7 +37,7 @@ let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () (* searches a coercion fron src to tgt in the !coercions list *) -let look_for_coercion src tgt = +let look_for_coercion' src tgt = let arity_of con = try let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in @@ -65,34 +65,37 @@ let look_for_coercion src tgt = (CoercDb.name_of_carr src) (CoercDb.name_of_carr tgt))); None - | [u] -> + | _::_ -> debug_print (lazy ( - sprintf ":-) TROVATA 1 coercion da %s a %s: %s" - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt) - (UriManager.name_of_uri u))); - Some u - | u::_ -> - debug_print (lazy ( - sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" + sprintf ":-) TROVATE %d coercion(s) da %s a %s" (List.length l) (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt) - (UriManager.name_of_uri u))); - Some u + (CoercDb.name_of_carr tgt))); + Some l in (match uri with None -> NoCoercion - | Some u -> - let c = CicUtil.term_of_uri u in - let arity = arity_of c in - let args = mk_implicits (arity - 1) in - let newt = - match args with - [] -> c - | _ -> Cic.Appl (c::args) + | Some ul -> + let cl = List.map CicUtil.term_of_uri ul in + let funclass_arityl = + let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in + List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl + in + let arityl = List.map arity_of cl in + let argsl = + List.map2 + (fun arity fn_arity -> + mk_implicits (arity - 1 - fn_arity)) arityl funclass_arityl in - SomeCoercion newt) + let newtl = + List.map2 + (fun args c -> + match args with + | [] -> c + | _ -> Cic.Appl (c::args)) + argsl cl + in + SomeCoercion newtl) with | CoercDb.EqCarrNotImplemented s -> NotHandled s | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed @@ -101,7 +104,7 @@ let look_for_coercion src tgt = let look_for_coercion src tgt = let src_uri = CoercDb.coerc_carr_of_term src in let tgt_uri = CoercDb.coerc_carr_of_term tgt in - look_for_coercion src_uri tgt_uri + look_for_coercion' src_uri tgt_uri let is_a_coercion t = try @@ -114,28 +117,105 @@ let source_of t = let uri = CicUtil.uri_of_term t in CoercDb.term_of_carr (fst (CoercDb.get_carr uri)) with Invalid_argument _ -> assert false (* t must be a coercion *) - -let target_of t = + +let is_a_coercion_to_funclass t = try let uri = CicUtil.uri_of_term t in - CoercDb.term_of_carr (snd (CoercDb.get_carr uri)) - with Invalid_argument _ -> assert false (* t must be a coercion *) - + match snd (CoercDb.get_carr uri) with + | CoercDb.Fun i -> Some i + | _ -> None + with Invalid_argument _ -> None + let generate_dot_file () = + let module Pp = GraphvizPp.Dot in + let buf = Buffer.create 10240 in + let fmt = Format.formatter_of_buffer buf in + Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] + ~edge_attrs:["fontsize", "10"] fmt; let l = CoercDb.to_list () in - let preamble = " - digraph pippo { - node [fontsize=9, width=.4, height=.4]; - edge [fontsize=10]; - \n" - in - let conclusion = " } \n" in - let data = List.fold_left - (fun acc (src,tgt,c) -> - acc ^ CoercDb.name_of_carr src ^ " -> " ^ - CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ - "\"];\n") "" l - in - preamble ^ data ^ conclusion - + let pp_description carr = + match CoercDb.uri_of_carr carr with + | None -> () + | Some uri -> + Pp.node (CoercDb.name_of_carr carr) + ~attrs:["href", UriManager.string_of_uri uri] fmt in + List.iter + (fun (src, tgt, cl) -> + let src_name = CoercDb.name_of_carr src in + let tgt_name = CoercDb.name_of_carr tgt in + pp_description src; + pp_description tgt; + List.iter + (fun c -> + Pp.edge src_name tgt_name + ~attrs:[ "label", UriManager.name_of_uri c; + "href", UriManager.string_of_uri c ] + fmt) + cl) + l; + Pp.trailer fmt; + Buffer.contents buf +;; + +let is_composite t = + try + let uri = + match t with + | Cic.Appl (he::_) -> CicUtil.uri_of_term he + | _ -> CicUtil.uri_of_term t + in + match CicEnvironment.get_obj CicUniv.empty_ugraph uri with + | Cic.Constant (_,_, _, _, attrs),_ -> + List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs + | _ -> false + with Invalid_argument _ -> false +;; + +let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);; + +let splat e l = List.map (fun x -> e, x) l;; + +let get_coercions_to carr = + let l = CoercDb.to_list () in + List.flatten + (HExtlib.filter_map + (fun (src,tgt,cl) -> + if CoercDb.eq_carr tgt carr then Some (splat src cl) else None) + l) +;; + +let get_coercions_from carr = + let l = CoercDb.to_list () in + List.flatten + (HExtlib.filter_map + (fun (src,tgt,cl) -> + if CoercDb.eq_carr src carr then Some (splat tgt cl) else None) + l) +;; + +let intersect l1 l2 = + let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in + uniq (List.filter is_in_l1 l2) +;; + +let grow s = + uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s) +;; + +let lb c = + let l = get_coercions_from c in + function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l +;; + +let rec min acc = function + | c::tl -> + if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl + | [] -> acc +;; + +let meets left right = + let u = UriManager.uri_of_string "cic:/foo.con" in + min [] (List.map fst (intersect (grow [left,u]) (grow [right,u]))) +;; + (* EOF *)