X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.ml;h=9f953ccf8f07b370cce20ab074a5f255c93fd8a9;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=0b0db09d9b26153f7905909a26766955bc0404f6;hpb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;p=helm.git diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index 0b0db09d9..9f953ccf8 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -135,14 +135,10 @@ let source_of t = | Some _ -> assert false (* t must be a coercion not to funclass *) ;; -let generate_dot_file () = - let l = CoercDb.to_list () in +let generate_dot_file fmt = + let l = CoercDb.to_list (CoercDb.dump ()) in 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; - if l <> [] then + if List.exists (fun (_,t,_) -> CoercDb.string_of_carr t = "Type") l then Format.fprintf fmt "subgraph cluster_rest { style=\"filled\"; color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n" (" @@ -154,47 +150,79 @@ let generate_dot_file () = (fun (src,tgt,ul) -> let src_name = CoercDb.string_of_carr src in let tgt_name = CoercDb.string_of_carr tgt in - let names = List.map (fun (u,_,_) -> UriManager.name_of_uri u) ul in + let names = + List.map (fun (u,_,_) -> + UriManager.name_of_uri u ^ + (match CicEnvironment.get_obj CicUniv.empty_ugraph u with + | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _ + when List.exists ((=) (`Flavour `Variant)) attrs -> "*" + | _ -> "") + ) ul + in "") + String.concat ", " names ^ "") (List.sort (fun (x,y,_) (x1,y1,_) -> let rc = compare x x1 in if rc = 0 then compare y y1 else rc) l)) ^ "
" ^ src_name ^ "" ^ tgt_name ^ "" ^ - String.concat "," names ^ "
") - (String.concat ";" - (List.flatten (List.map (fun (s,t,_) -> - let src_name = CoercDb.string_of_carr s in - let tgt_name = CoercDb.string_of_carr t in - [ "\""^src_name^"\""; "\""^tgt_name^"\"" ] - ) l))); - let pp_description carr = - match carr with - | CoercDb.Uri uri -> - Pp.node (CoercDb.string_of_carr carr) - ~attrs:["href", UriManager.string_of_uri uri] fmt - | _ -> () + (String.concat ";" ["Type"]); + let type_uri u = + let ty, _ = + CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u) + CicUniv.oblivion_ugraph + in + ty + in + let deref_coercion u = + match CicEnvironment.get_obj CicUniv.empty_ugraph u with + | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _ + when List.exists ((=) (`Flavour `Variant)) attrs -> + UriManager.name_of_uri u' + | Cic.Constant (_,Some t,_,_,_), _ when + let rec is_id = function + | Cic.Lambda (_,_,t) -> is_id t + | Cic.Rel _ -> true + | _ -> false + in is_id t -> "ID" + | _ -> UriManager.name_of_uri u in List.iter (fun (src, tgt, ul) -> - let src_name = CoercDb.string_of_carr src in - let tgt_name = CoercDb.string_of_carr tgt in - pp_description src; - pp_description tgt; List.iter - (fun (u,saturations,_) -> + (fun (u,saturations,cpos) -> + let ty = type_uri u in + let src_name, tgt_name = + let rec aux ctx cpos t = + match cpos, t with + | 0,Cic.Prod (_,src,tgt) -> + CicPp.pp src ctx, tgt, (Some (Cic.Name "_")::ctx) + | 0,t -> CicPp.pp t ctx, Cic.Implicit None, [] + | n,Cic.Prod (_,_,tgt) -> aux (Some (Cic.Name "_")::ctx) (n-1) tgt + | _ -> assert false + in + let ssrc, rest, ctx = aux [] cpos ty in + let stgt, rest, _ = aux ctx saturations rest in + let stgt = + if rest <> Cic.Implicit None then + match tgt with + | CoercDb.Fun _ -> CoercDb.string_of_carr tgt + | _ -> assert false + else + stgt + in + ssrc, stgt + in + Pp.node src_name fmt; + Pp.node tgt_name fmt; Pp.edge src_name tgt_name ~attrs:[ "label", - (UriManager.name_of_uri u ^ - if saturations = 0 then - "" - else - "(" ^ string_of_int saturations ^ ")"); + (deref_coercion u ^ + if saturations = 0 then "" + else "(" ^ string_of_int saturations ^ ")"); "href", UriManager.string_of_uri u ] fmt) ul) l; - Pp.trailer fmt; - Buffer.contents buf ;; let coerced_arg l = @@ -229,7 +257,7 @@ let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;; (* : carr -> (carr * uri option) where the option is always Some *) let get_coercions_to carr = - let l = CoercDb.to_list () in + let l = CoercDb.to_list (CoercDb.dump ()) in let splat_coercion_to carr (src,tgt,cl) = if CoercDb.eq_carr tgt carr then Some (splat src cl) else None in @@ -239,7 +267,7 @@ let get_coercions_to carr = (* : carr -> (carr * uri option) where the option is always Some *) let get_coercions_from carr = - let l = CoercDb.to_list () in + let l = CoercDb.to_list (CoercDb.dump ()) in let splat_coercion_from carr (src,tgt,cl) = if CoercDb.eq_carr src carr then Some (splat tgt cl) else None in @@ -270,10 +298,16 @@ let lb (c,_,_) = (* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *) -let rec min acc = function +let rec min acc skipped = function | c::tl -> - if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl - | [] -> acc + if List.exists (lb c) (tl@acc) + then min acc (c::skipped) tl else min (c::acc) skipped tl + | [] -> acc, skipped +;; + + +let sort l = + let low, high = min [] [] l in low @ high ;; let meets metasenv subst context (grow_left,left) (grow_right,right) = @@ -287,12 +321,12 @@ let meets metasenv subst context (grow_left,left) (grow_right,right) = in List.map (fun (c,uo1,uo2) -> - let metasenv, uo1 = - if grow_left then saturate metasenv uo1 else metasenv, None in - let metasenv, uo2 = - if grow_right then saturate metasenv uo2 else metasenv, None in + let metasenv, uo1 = saturate metasenv uo1 in + let metasenv, uo2 = saturate metasenv uo2 in c,metasenv, uo1, uo2) - (min [] (intersect (grow left) (grow right))) + (sort (intersect + (if grow_left then grow left else [left,None]) + (if grow_right then grow right else [right,None]))) ;; (* EOF *)