X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercGraph.ml;h=355c8019a80401f055b559f99f5352e154ea4022;hb=a5cb4c29b556fdfe343b8fcc574fac57974bfe4e;hp=cd958a8f62074aa5ba4ac76fb023043b2478587e;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/library/coercGraph.ml b/helm/software/components/library/coercGraph.ml index cd958a8f6..355c8019a 100644 --- a/helm/software/components/library/coercGraph.ml +++ b/helm/software/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,35 +37,65 @@ 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 + let rec count_pi = function + | Cic.Prod (_,_,t) -> 1 + count_pi t + | _ -> 0 + in + count_pi ty + with Invalid_argument _ -> assert false (* all coercions have an uri *) + in + let rec mk_implicits = function + | 0 -> [] + | n -> Cic.Implicit None :: mk_implicits (n-1) + in try let l = CoercDb.find_coercion - (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) + (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in + let uri = + match l with + | [] -> + debug_print + (lazy + (sprintf ":-( coercion non trovata da %s a %s" + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt))); + None + | _::_ -> + debug_print (lazy ( + sprintf ":-) TROVATE %d coercion(s) da %s a %s" + (List.length l) + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt))); + Some l in - match l with - | [] -> - debug_print - (lazy - (sprintf ":-( coercion non trovata da %s a %s" - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); - NoCoercion - | [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))); - SomeCoercion (CicUtil.term_of_uri u) - | u::_ -> - debug_print (lazy ( - sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" - (List.length l) - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt) - (UriManager.name_of_uri u))); - SomeCoercion (CicUtil.term_of_uri u) + (match uri with + None -> NoCoercion + | 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 + 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 @@ -74,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 @@ -87,11 +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 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 *)