From: Claudio Sacerdoti Coen Date: Sun, 17 May 2009 19:12:15 +0000 (+0000) Subject: alpha_eq defined and exported X-Git-Tag: make_still_working~3971 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8f9cc4af6bcd524a8e6c0ab012661ff2a66dc381;p=helm.git alpha_eq defined and exported --- diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 1815ceedf..2e13a5304 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -190,127 +190,134 @@ let get_relevance = ref (fun ~metasenv:_ ~subst:_ _ _ -> assert false);; let set_get_relevance f = get_relevance := f;; +let alpha_eq ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 = + if t1 === t2 then + true + else + match (t1,t2) with + | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> + NCicEnvironment.universe_leq a b + | (C.Sort (C.Type a), C.Sort (C.Type b)) -> + NCicEnvironment.universe_eq a b + | (C.Sort C.Prop,C.Sort (C.Type _)) -> (not test_eq_only) + | (C.Sort C.Prop, C.Sort C.Prop) -> true + + | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> + aux true context s1 s2 && + aux test_eq_only ((name1, C.Decl s1)::context) t1 t2 + | (C.Lambda (name1,s1,t1), C.Lambda(_,_,t2)) -> + if test_lambda_source then + aux test_eq_only context t1 t2 + else + (* thanks to inversion of well typedness, the source + * of these lambdas must be already convertible *) + aux test_eq_only ((name1, C.Decl s1)::context) t1 t2 + | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> + aux test_eq_only context ty1 ty2 && + aux test_eq_only context s1 s2 && + aux test_eq_only ((name1, C.Def (s1,ty1))::context) t1 t2 + + | (C.Meta (n1,(s1, C.Irl _)), C.Meta (n2,(s2, C.Irl _))) + when n1 = n2 && s1 = s2 -> true + | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 && + let l1 = NCicUtils.expand_local_context l1 in + let l2 = NCicUtils.expand_local_context l2 in + (try List.for_all2 + (fun t1 t2 -> aux test_eq_only context + (NCicSubstitution.lift s1 t1) + (NCicSubstitution.lift s2 t2)) + l1 l2 + with Invalid_argument "List.for_all2" -> + prerr_endline ("Meta " ^ string_of_int n1 ^ + " occurrs with local contexts of different lenght\n"^ + NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2); + assert false) -> true + + | C.Meta (n1,l1), _ -> + (try + let _,_,term,_ = NCicUtils.lookup_subst n1 subst in + let term = NCicSubstitution.subst_meta l1 term in + aux test_eq_only context term t2 + with NCicUtils.Subst_not_found _ -> false) + | _, C.Meta (n2,l2) -> + (try + let _,_,term,_ = NCicUtils.lookup_subst n2 subst in + let term = NCicSubstitution.subst_meta l2 term in + 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)) + when (Ref.eq r1 r2 && + List.length (E.get_relevance r1) >= List.length tl1) -> + let relevance = E.get_relevance r1 in + let relevance = match r1 with + | Ref.Ref (_,Ref.Con (_,_,lno)) -> + let _,relevance = HExtlib.split_nth lno relevance in + HExtlib.mk_list false lno @ relevance + | _ -> relevance + in + (try + HExtlib.list_forall_default3_var + (fun t1 t2 b -> not b || aux true context t1 t2 ) + tl1 tl2 true relevance + with Invalid_argument _ -> false + | HExtlib.FailureAt fail -> + let relevance = + !get_relevance ~metasenv ~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 true 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 ~metasenv ~subst context hd1 tl1 in + (try + HExtlib.list_forall_default3 + (fun t1 t2 b -> not b || aux true context t1 t2) + tl1 tl2 true relevance + with Invalid_argument _ -> false) + + | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1), + C.Match (ref2,outtype2,term2,pl2)) -> + let _,_,itl,_,_ = E.get_checked_indtys ref1 in + let _,_,ty,_ = List.nth itl tyno in + let rec remove_prods ~subst context ty = + let ty = whd ~subst context ty in + match ty with + | C.Sort _ -> ty + | C.Prod (name,so,ta) -> remove_prods ~subst ((name,(C.Decl so))::context) ta + | _ -> assert false + in + let is_prop = + match remove_prods ~subst [] ty with + | C.Sort C.Prop -> true + | _ -> false + in + Ref.eq ref1 ref2 && + aux test_eq_only context outtype1 outtype2 && + (is_prop || aux test_eq_only context term1 term2) && + (try List.for_all2 (aux test_eq_only context) pl1 pl2 + with Invalid_argument _ -> false) + | (C.Implicit _, _) | (_, C.Implicit _) -> assert false + | (_,_) -> false +;; + (* t1, t2 must be well-typed *) let are_convertible ~metasenv ~subst = let rec aux test_eq_only context t1 t2 = - let alpha_eq test_eq_only t1 t2 = - if t1 === t2 then - true - else - match (t1,t2) with - | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> - NCicEnvironment.universe_leq a b - | (C.Sort (C.Type a), C.Sort (C.Type b)) -> - NCicEnvironment.universe_eq a b - | (C.Sort C.Prop,C.Sort (C.Type _)) -> (not test_eq_only) - | (C.Sort C.Prop, C.Sort C.Prop) -> true - - | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - aux true context s1 s2 && - aux test_eq_only ((name1, C.Decl s1)::context) t1 t2 - | (C.Lambda (name1,s1,t1), C.Lambda(_,_,t2)) -> - (* thanks to inversion of well typedness, the source - * of these lambdas must be already convertible *) - aux test_eq_only ((name1, C.Decl s1)::context) t1 t2 - | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> - aux test_eq_only context ty1 ty2 && - aux test_eq_only context s1 s2 && - aux test_eq_only ((name1, C.Def (s1,ty1))::context) t1 t2 - - | (C.Meta (n1,(s1, C.Irl _)), C.Meta (n2,(s2, C.Irl _))) - when n1 = n2 && s1 = s2 -> true - | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 && - let l1 = NCicUtils.expand_local_context l1 in - let l2 = NCicUtils.expand_local_context l2 in - (try List.for_all2 - (fun t1 t2 -> aux test_eq_only context - (NCicSubstitution.lift s1 t1) - (NCicSubstitution.lift s2 t2)) - l1 l2 - with Invalid_argument "List.for_all2" -> - prerr_endline ("Meta " ^ string_of_int n1 ^ - " occurrs with local contexts of different lenght\n"^ - NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2); - assert false) -> true - - | C.Meta (n1,l1), _ -> - (try - let _,_,term,_ = NCicUtils.lookup_subst n1 subst in - let term = NCicSubstitution.subst_meta l1 term in - aux test_eq_only context term t2 - with NCicUtils.Subst_not_found _ -> false) - | _, C.Meta (n2,l2) -> - (try - let _,_,term,_ = NCicUtils.lookup_subst n2 subst in - let term = NCicSubstitution.subst_meta l2 term in - 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)) - when (Ref.eq r1 r2 && - List.length (E.get_relevance r1) >= List.length tl1) -> - let relevance = E.get_relevance r1 in - let relevance = match r1 with - | Ref.Ref (_,Ref.Con (_,_,lno)) -> - let _,relevance = HExtlib.split_nth lno relevance in - HExtlib.mk_list false lno @ relevance - | _ -> relevance - in - (try - HExtlib.list_forall_default3_var - (fun t1 t2 b -> not b || aux true context t1 t2 ) - tl1 tl2 true relevance - with Invalid_argument _ -> false - | HExtlib.FailureAt fail -> - let relevance = - !get_relevance ~metasenv ~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 true 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 ~metasenv ~subst context hd1 tl1 in - (try - HExtlib.list_forall_default3 - (fun t1 t2 b -> not b || aux true context t1 t2) - tl1 tl2 true relevance - with Invalid_argument _ -> false) - - | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1), - C.Match (ref2,outtype2,term2,pl2)) -> - let _,_,itl,_,_ = E.get_checked_indtys ref1 in - let _,_,ty,_ = List.nth itl tyno in - let rec remove_prods ~subst context ty = - let ty = whd ~subst context ty in - match ty with - | C.Sort _ -> ty - | C.Prod (name,so,ta) -> remove_prods ~subst ((name,(C.Decl so))::context) ta - | _ -> assert false - in - let is_prop = - match remove_prods ~subst [] ty with - | C.Sort C.Prop -> true - | _ -> false - in - Ref.eq ref1 ref2 && - aux test_eq_only context outtype1 outtype2 && - (is_prop || aux test_eq_only context term1 term2) && - (try List.for_all2 (aux test_eq_only context) pl1 pl2 - with Invalid_argument _ -> false) - | (C.Implicit _, _) | (_, C.Implicit _) -> assert false - | (_,_) -> false + let alpha_eq test_eq_only = + alpha_eq ~test_lambda_source:false aux test_eq_only metasenv subst context in if alpha_eq test_eq_only t1 t2 then true @@ -365,6 +372,13 @@ let are_convertible ~metasenv ~subst = aux false ;; +let alpha_eq metasenv subst = + let rec aux test_lambda_source context t1 t2 = + alpha_eq ~test_lambda_source aux true metasenv subst context t1 t2 + in + aux true +;; + let rec head_beta_reduce ~delta ~upto ~subst t l = match upto, t, l with | 0, C.Appl l1, _ -> C.Appl (l1 @ l)