X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcoercGraph.ml;h=37ded8ee0675de18ca3600be2cba6ac57ec1e75d;hb=387c6f39b2e55c887e8947039e5d7f56bce7f7a8;hp=70e90af52f2c4fb0333441b872873c6e5fbfec0e;hpb=6bb370c6e1a036e82315765d6dceb1939c30ed23;p=helm.git diff --git a/components/cic_unification/coercGraph.ml b/components/cic_unification/coercGraph.ml index 70e90af52..37ded8ee0 100644 --- a/components/cic_unification/coercGraph.ml +++ b/components/cic_unification/coercGraph.ml @@ -39,6 +39,30 @@ type coercion_search_result = 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 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 freshmeta = CicMkImplicit.new_meta metasenv subst in + List.map2 + (fun arity c -> + let ty,_ = + CicTypeChecker.type_of_aux' ~subst metasenv context c + CicUniv.empty_ugraph in + let _,metasenv,args,lastmeta = + TermUtil.saturate_term freshmeta metasenv context ty arity in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + metasenv, Cic.Meta (lastmeta-1,irl), + match args with + [] -> c + | _ -> Cic.Appl (c::args) + ) funclass_arityl cl +;; + (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion' metasenv subst context src tgt = try @@ -64,31 +88,7 @@ let look_for_coercion' metasenv subst context src tgt = in (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 freshmeta = CicMkImplicit.new_meta metasenv subst in - let newtl = - List.map2 - (fun arity c -> - let ty,_ = - CicTypeChecker.type_of_aux' ~subst metasenv context c - CicUniv.empty_ugraph in - let _,metasenv,args,lastmeta = - TermUtil.saturate_term freshmeta metasenv context ty arity in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - metasenv, Cic.Meta (lastmeta-1,irl), - match args with - [] -> c - | _ -> Cic.Appl (c::args) - ) funclass_arityl cl - in - SomeCoercion newtl) + | Some ul -> SomeCoercion (saturate_coercion ul metasenv subst context)) with | CoercDb.EqCarrNotImplemented s -> NotHandled s | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed @@ -150,51 +150,114 @@ let is_composite t = with Invalid_argument _ -> false ;; -let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);; +let coerced_arg l = + match l with + | [] | [_] -> assert false + | c::_ when not (CoercDb.is_a_coercion' c) -> assert false + | 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.empty_ugraph uri) with + | Cic.Constant (_, _, ty, _, _) -> count_pi ty + | _ -> assert false + in + try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None +;; + +(************************* meet calculation stuff ********************) +let eq_uri_opt u1 u2 = + match u1,u2 with + | Some u1, Some u2 -> UriManager.eq u1 u2 + | None,Some _ | Some _, None -> false + | None, None -> true +;; + +let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;; + +let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) = + CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22 +;; + +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, x) l;; +let splat e l = List.map (fun x -> e, Some x) l;; +(* : carr -> (carr * uri option) where the option is always Some *) 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 splat_coercion_to carr (src,tgt,cl) = + if CoercDb.eq_carr tgt carr then Some (splat src cl) else None + in + let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in + l ;; +(* : carr -> (carr * uri option) where the option is always Some *) 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 splat_coercion_from carr (src,tgt,cl) = + if CoercDb.eq_carr src carr then Some (splat tgt cl) else None + in + List.flatten (HExtlib.filter_map (splat_coercion_from carr) l) ;; +(* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 } + * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *) 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 is_in_l1 (x,u2) = + HExtlib.filter_map + (fun (src,u1) -> + if CoercDb.eq_carr x src then Some (src,u1,u2) else None) + l1 + in + uniq2 (List.flatten (List.map is_in_l1 l2)) ;; -let grow s = - uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s) +(* grow tgt gives all the (src,u) such that u:tgt->src *) +let grow tgt = + uniq ((tgt,None)::(get_coercions_to tgt)) ;; -let lb c = +let lb (c,_,_) = let l = get_coercions_from c in - function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l + fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l ;; +(* 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 | 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]))) +let meets metasenv subst context left right = + let saturate metasenv uo = + match uo with + | None -> metasenv, None + | Some u -> + match saturate_coercion [u] metasenv subst context with + | [metasenv, sat, last] -> metasenv, Some (sat, last) + | _ -> assert false + in + List.map + (fun (c,uo1,uo2) -> + let metasenv, uo1 = saturate metasenv uo1 in + let metasenv, uo2 = saturate metasenv uo2 in + c,metasenv, uo1, uo2) + (min [] (intersect (grow left) (grow right))) ;; (* EOF *)