From 1df8405217896500edba22b61653e03b5289747c Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 13 Jun 2008 12:59:14 +0000 Subject: [PATCH] final relevance check --- .../components/ng_kernel/nCicReduction.ml | 47 +++++++++++- .../components/ng_kernel/nCicTypeChecker.ml | 71 +++++++++---------- 2 files changed, 79 insertions(+), 39 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 61bb201b7..61591e4f8 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -171,8 +171,19 @@ 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 rec aux test_eq_only context t1 t2 = let rec alpha_eq test_eq_only t1 t2 = if t1 === t2 then @@ -222,7 +233,41 @@ let are_convertible ?(subst=[]) get_relevance = 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 + 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) + 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)) -> aux test_eq_only context hd1 hd2 && let relevance = get_relevance ~subst context hd1 tl1 in diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 56d06a71b..464186f2e 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -1053,44 +1053,39 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) = ty | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference")) -and get_relevance ~subst context te args = - match te with - | C.Const r when List.length (E.get_relevance r) >= List.length args -> - let relevance = E.get_relevance r in - (match r with - | Ref.Ref (_,Ref.Con (_,_,lno)) -> - let _,relevance = HExtlib.split_nth lno relevance in - HExtlib.mk_list false lno @ relevance - | _ -> relevance) - | t -> - let ty = typeof ~subst ~metasenv:[] context t in - let rec aux context ty = function - | [] -> [] - | arg::tl -> match R.whd ~subst context ty with - | C.Prod (name,so,de) -> - let sort = typeof ~subst ~metasenv:[] context so in - let new_ty = S.subst ~avoid_beta_redexes:true arg de in - (match R.whd ~subst context sort with - | C.Sort C.Prop -> - false::(aux ((name,(C.Decl so))::context) new_ty tl) - | C.Sort _ - | C.Meta _ -> true::(aux ((name,(C.Decl so))::context) de tl) - | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf - "Prod: the type %s of the source of %s is not a sort" - (PP.ppterm ~subst ~metasenv:[] ~context sort) - (PP.ppterm ~subst ~metasenv:[] ~context so))))) - | _ -> - raise - (TypeCheckerFailure - (lazy (Printf.sprintf - "Appl: %s is not a function, it cannot be applied" - (PP.ppterm ~subst ~metasenv:[] ~context - (let res = List.length tl in - let eaten = List.length args - res in - (C.Appl - (t::fst - (HExtlib.split_nth eaten args)))))))) - in aux context ty args +and get_relevance ~subst context t args = + let ty = typeof ~subst ~metasenv:[] context t in + let rec aux context ty = function + | [] -> [] + | arg::tl -> match R.whd ~subst context ty with + | C.Prod (name,so,de) -> + let sort = typeof ~subst ~metasenv:[] context so in + let new_ty = S.subst ~avoid_beta_redexes:true arg de in + (*prerr_endline ("so: " ^ PP.ppterm ~subst ~metasenv:[] + ~context so); + prerr_endline ("sort: " ^ PP.ppterm ~subst ~metasenv:[] + ~context sort);*) + (match R.whd ~subst context sort with + | C.Sort C.Prop -> + false::(aux context new_ty tl) + | C.Sort _ + | C.Meta _ -> true::(aux context new_ty tl) + | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf + "Prod: the type %s of the source of %s is not a sort" + (PP.ppterm ~subst ~metasenv:[] ~context sort) + (PP.ppterm ~subst ~metasenv:[] ~context so))))) + | _ -> + raise + (TypeCheckerFailure + (lazy (Printf.sprintf + "Appl: %s is not a function, it cannot be applied" + (PP.ppterm ~subst ~metasenv:[] ~context + (let res = List.length tl in + let eaten = List.length args - res in + (C.Appl + (t::fst + (HExtlib.split_nth eaten args)))))))) + in aux context ty args ;; let typecheck_context ~metasenv ~subst context = -- 2.39.2