X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.ml;h=9f953ccf8f07b370cce20ab074a5f255c93fd8a9;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=ac7441a4cdad4ee5f40fda81d3c0cf213cf7fb3e;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index ac7441a4c..9f953ccf8 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -34,22 +34,26 @@ type coercion_search_result = | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list | NoCoercion - | NotMetaClosed - | NotHandled of string Lazy.t + | NotHandled let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () let saturate_coercion ul metasenv subst context = let cl = - List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in - let funclass_arityl = - let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in - List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl + List.map + (fun u,saturations -> + let t = CicUtil.term_of_uri u in + let arity = + match CoercDb.is_a_coercion t with + | Some (_,CoercDb.Fun i,_,_,_) -> i + | _ -> 0 + in + arity,t,saturations) ul in let freshmeta = CicMkImplicit.new_meta metasenv subst in - List.map2 - (fun arity (c,saturations) -> + List.map + (fun (arity,c,saturations) -> let ty,_ = CicTypeChecker.type_of_aux' ~subst metasenv context c CicUniv.oblivion_ugraph in @@ -62,30 +66,38 @@ let saturate_coercion ul metasenv subst context = match args with [] -> c | _ -> Cic.Appl (c::args) - ) funclass_arityl cl + ) cl ;; (* searches a coercion fron src to tgt in the !coercions list *) -let look_for_coercion' metasenv subst context src tgt = +let look_for_coercion_carr metasenv subst context src tgt = + let is_dead = function CoercDb.Dead -> true | _ -> false in let pp_l s l = match l with | [] -> debug_print (lazy (sprintf ":-( coercion non trovata[%s] da %s a %s" s - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); + (CoercDb.string_of_carr src) + (CoercDb.string_of_carr tgt))); | _::_ -> debug_print (lazy ( sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s (List.length l) - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); + (CoercDb.string_of_carr src) + (CoercDb.string_of_carr tgt))); in - try + if is_dead src || is_dead tgt then NotHandled + else 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 && + match t, tgt with + | CoercDb.Sort Cic.Prop, CoercDb.Sort Cic.Prop + | CoercDb.Sort Cic.Set, CoercDb.Sort Cic.Set + | CoercDb.Sort _, CoercDb.Sort (Cic.Type _|Cic.CProp _) -> true + | _ -> CoercDb.eq_carr t tgt) in pp_l "precise" l; (match l with @@ -97,96 +109,130 @@ let look_for_coercion' metasenv subst context src tgt = pp_l "approx" l; (match l with | [] -> NoCoercion - | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context)) + | ul -> + SomeCoercionToTgt (saturate_coercion ul metasenv subst context)) | ul -> SomeCoercion (saturate_coercion ul metasenv subst context)) - with - | CoercDb.EqCarrNotImplemented s -> NotHandled s - | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed +;; + +let rec count_pi c s t = + match CicReduction.whd ~delta:false ~subst:s c t with + | Cic.Prod (_,_,t) -> 1 + count_pi c s t + | _ -> 0 ;; let look_for_coercion metasenv subst context 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' metasenv subst context src_uri tgt_uri + let src_arity = count_pi context subst src in + let tgt_arity = count_pi context subst tgt in + let src_carr = CoercDb.coerc_carr_of_term src src_arity in + let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in + look_for_coercion_carr metasenv subst context src_carr tgt_carr let source_of t = - try - 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 *) + match CoercDb.is_a_coercion t with + | None -> assert false + | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s + | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u + | Some _ -> assert false (* t must be a coercion not to funclass *) +;; -let generate_dot_file () = +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; - 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 + 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" + (" + + + "^ + String.concat "" + (List.map + (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 ^ + (match CicEnvironment.get_obj CicUniv.empty_ugraph u with + | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _ + when List.exists ((=) (`Flavour `Variant)) attrs -> "*" + | _ -> "") + ) ul + in + "") + (List.sort (fun (x,y,_) (x1,y1,_) -> + let rc = compare x x1 in + if rc = 0 then compare y y1 else rc) l)) + ^ "
SourceTargetArrows
" ^ src_name ^ "" ^ tgt_name ^ "" ^ + String.concat ", " names ^ "
") + (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.name_of_carr src in - let tgt_name = CoercDb.name_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 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.oblivion_ugraph uri with - | Cic.Constant (_,_, _, _, attrs),_ -> - List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs - | _ -> false - with Invalid_argument _ -> false -;; - let coerced_arg l = match l with - | [] | [_] -> assert false - | c::_ when not (CoercDb.is_a_coercion' c) -> assert false + | [] | [_] -> None | c::tl -> - let arity = - match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a - in - (* decide a decent structure for coercion carriers so that all this stuff is - * useless *) - let pi = - (* this calculation is not complete, since we have strange carriers *) - let rec count_pi = function - | Cic.Prod(_,_,t) -> 1+ (count_pi t) - | _ -> 0 - in - let uri = CicUtil.uri_of_term c in - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - | Cic.Constant (_, _, ty, _, _) -> count_pi ty - | _ -> assert false - in - try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None + match CoercDb.is_a_coercion c with + | None -> None + | Some (_,_,_,_,cpos) -> + if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None ;; (************************* meet calculation stuff ********************) @@ -207,11 +253,11 @@ let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;; let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;; -let splat e l = List.map (fun x -> e, Some x) l;; +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 @@ -221,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 @@ -252,13 +298,19 @@ 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 left right = +let meets metasenv subst context (grow_left,left) (grow_right,right) = let saturate metasenv uo = match uo with | None -> metasenv, None @@ -272,7 +324,9 @@ let meets metasenv subst context left right = 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 *)