From 63bf7f1e50ca65c2a224e34aa7d232bff10ea934 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Apr 2008 20:50:58 +0000 Subject: [PATCH] fixed_args fixed to accept passing a partially applied fix to a fix that passes itself partially applied to anothere fix --- .../components/ng_kernel/nCicTypeChecker.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 99829c4a7..9b0de30f2 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -71,12 +71,16 @@ let string_of_recfuns ~subst ~metasenv ~context l = let fixed_args bos j n nn = let rec aux k acc = function | NCic.Appl (NCic.Rel i::args) when i+k > n && i+k <= nn -> - (try - let lefts, _ = HExtlib.split_nth j args in - List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) - (HExtlib.list_mapi (fun x i -> x,i) (List.combine acc lefts)) - with Failure "HExtlib.split_nth" -> assert false) - (* se sono meno di j, fino a j deduco, dopo false *) + let rec combine l1 l2 = + match l1,l2 with + [],[] -> [] + | he1::tl1, he2::tl2 -> (he1,he2)::combine tl1 tl2 + | he::tl, [] -> (false,NCic.Rel ~-1)::combine tl [] (* dummy term *) + | [],_::_ -> assert false + in + let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in + List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) + (HExtlib.list_mapi (fun x i -> x,i) (combine acc lefts)) | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t in List.fold_left (aux 0) @@ -606,7 +610,7 @@ exception NotGuarded of string Lazy.t;; let rec typeof ~subst ~metasenv context term = let rec typeof_aux context = - fun t -> (*prerr_endline (NCicPp.ppterm ~context t); *) + fun t -> (*prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);*) match t with | C.Rel n -> (try -- 2.39.2