From: Wilmer Ricciotti Date: Fri, 3 Oct 2008 09:13:53 +0000 (+0000) Subject: Final implementation of proof irrelevant conversion, which hadn't X-Git-Tag: make_still_working~4706 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88381f8e48371c86d29eaeee8354ebfd651ab9e8;p=helm.git Final implementation of proof irrelevant conversion, which hadn't been committed (!) --- diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 6af86f9cd..e2063e451 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -164,6 +164,23 @@ let rec list_forall_default3 f l1 l2 def l3 = | a::ta, b::tb, [] -> f a b def && list_forall_default3 f ta tb def [] ;; +exception FailureAt of int;; + +let list_forall_default3_var f l1 l2 def l3 = + let rec aux f l1 l2 def l3 i = + match l1,l2,l3 with + | [], [], _ -> true + | [], _, _ + | _, [], _ -> raise (Invalid_argument "list_forall_default3") + | a::ta, b::tb, c::tc -> + if f a b c then aux f ta tb def tc (i+1) + else raise (FailureAt i) + | a::ta, b::tb, [] -> + if f a b def then aux f ta tb def [] (i+1) + else raise (FailureAt i) + in aux f l1 l2 def l3 0 +;; + let sharing_map f l = let unchanged = ref true in let rec aux b = function diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli index c80d2e4f8..dae914477 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -100,7 +100,9 @@ val list_iter_default2: ('a -> 'b -> unit) -> 'a list -> 'b -> 'b list -> unit length (otherwise it raises Invalid_argument). It stops when the first two lists are empty. The third one can be shorter and is padded with a default value. *) val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool +val list_forall_default3_var: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool +exception FailureAt of int (** split_nth n l * @returns two list, the first contains at least n elements, the second the diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 316b39dab..4de73408f 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -171,21 +171,8 @@ let whd = R.whd let (===) x y = Pervasives.compare x y = 0 ;; -exception Dance;; - -let prof = HExtlib.profiling_enabled := true;HExtlib.profile "cache failures";; -let prof2 = HExtlib.profiling_enabled := true;HExtlib.profile "dancing sorts";; (* t1, t2 must be well-typed *) -let are_convertible ?(subst=[]) get_relevance = -(* - let get_relevance_p ~subst context t args = - (match prof with {HExtlib.profile = p} -> p) - (fun (a,b,c,d) -> get_relevance ~subst:a b c d) - (subst,context,t,args) - in - let dance () = (match prof2 with {HExtlib.profile = p} -> p) (fun () -> ()) () - in -*) +let are_convertible ?(subst=[]) get_exact_relev = let rec aux test_eq_only context t1 t2 = let alpha_eq test_eq_only t1 t2 = if t1 === t2 then @@ -236,7 +223,7 @@ let are_convertible ?(subst=[]) get_relevance = aux test_eq_only context t1 term with NCicUtils.Subst_not_found _ -> false) - | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) + | (C.Appl ((C.Const r1) as hd1::tl1), C.Appl (C.Const r2::tl2)) when (Ref.eq r1 r2 && List.length (E.get_relevance r1) >= List.length tl1) -> let relevance = E.get_relevance r1 in @@ -246,34 +233,31 @@ let are_convertible ?(subst=[]) get_relevance = HExtlib.mk_list false lno @ relevance | _ -> relevance in - let fail = ref ~-1 in - let res = (try - HExtlib.list_forall_default3 - (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2) + (try + HExtlib.list_forall_default3_var + (fun t1 t2 b -> not b || aux test_eq_only context t1 t2 ) tl1 tl2 true relevance - with Invalid_argument _ -> false) - in res - (* if res then true - else - let relevance = get_relevance_p ~subst context _hd1 tl1 in - let _,relevance = HExtlib.split_nth !fail relevance in - let b,relevance = (match relevance with - | [] -> assert false - | b::tl -> b,tl) in - let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in - let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in - if (not b) then - (dance (); - try - HExtlib.list_forall_default3 - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) - tl1 tl2 true relevance - with Invalid_argument _ -> false) - else false *) - | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> + with Invalid_argument _ -> false + | HExtlib.FailureAt fail -> + let relevance = get_exact_relev ~subst context hd1 tl1 in + let _,relevance = HExtlib.split_nth fail relevance in + let b,relevance = (match relevance with + | [] -> assert false + | b::tl -> b,tl) in + if (not b) then + let _,tl1 = HExtlib.split_nth (fail+1) tl1 in + let _,tl2 = HExtlib.split_nth (fail+1) tl2 in + try + HExtlib.list_forall_default3 + (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) + tl1 tl2 true relevance + with Invalid_argument _ -> false + else false) + + | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> aux test_eq_only context hd1 hd2 && - let relevance = get_relevance ~subst context hd1 tl1 in - (try + let relevance = get_exact_relev ~subst context hd1 tl1 in + (try HExtlib.list_forall_default3 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) tl1 tl2 true relevance