From: Enrico Tassi Date: Thu, 3 Apr 2008 16:55:10 +0000 (+0000) Subject: debujin implemented with the map recursor X-Git-Tag: make_still_working~5461 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4e923b3538c36c7f7cdd98246fc29a1ed6379b48;p=helm.git debujin implemented with the map recursor --- diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 80d4dea0e..f4c6cd4ab 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -257,7 +257,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = let ugraph'' = List.fold_left (fun ugraph (name,te) -> - let debruijnedte = debruijn_constructor uri len te in + let debruijnedte = debruijn uri len te in let augmented_term = List.fold_right (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) @@ -619,75 +619,22 @@ let rec split_prods ~subst context n te = | (_, _) -> raise (AssertFailure (lazy "split_prods")) ;; -let debruijn_constructor ?(cb=fun _ _ -> ()) uri number_of_types t = assert false -(* +let debruijn ?(cb=fun _ _ -> ()) uri number_of_types = let rec aux k t = - let module C = Cic in let res = match t with - C.Rel n as t when n <= k -> t - | C.Rel _ -> - raise (TypeCheckerFailure (lazy "unbound variable found in constructor type")) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i,l) -> - let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in - C.Meta (i,l') - | C.Sort _ - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) - | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t) - | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t) - | C.Appl l -> C.Appl (List.map (aux k) l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' -> - if exp_named_subst != [] then - raise (TypeCheckerFailure - (lazy ("non-empty explicit named substitution is applied to "^ - "a mutual inductive type which is being defined"))) ; - C.Rel (k + number_of_types - tyno) ; - | C.MutInd (uri',tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst - in - C.MutInd (uri',tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst - in - C.MutConstruct (uri,tyno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, i, aux k outty, aux k t, - List.map (aux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) + | C.Meta (i,(s,C.Ctx l)) -> + let l1 = NCicUtils.sharing_map (aux (k-s)) l in + if l1 == l then t else C.Meta (i,(s,C.Ctx l1)) + | C.Meta _ -> t + | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) + | C.Const (Ref.Ref (_,uri1,Ref.Ind no)) when NUri.eq uri uri1 -> + C.Rel (k + number_of_types - no) + | t -> NCicUtils.map (fun _ k -> k+1) k aux t in - cb t res; - res + cb t res; res in - aux 0*) + aux 0 ;; @@ -731,14 +678,14 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = aux ty_he args_with_ty ;; -let fix_lefts_in_constrs ~subst paramsno tyl i = +let fix_lefts_in_constrs ~subst uri paramsno tyl i = let len = List.length tyl in let _,_,arity,cl = List.nth tyl i in let tys = List.map (fun (_,n,ty,_) -> n,C.Decl ty) tyl in let cl' = List.map (fun (_,id,ty) -> - let debruijnedty = debruijn_constructor ref len ty in + let debruijnedty = debruijn uri len ty in id, snd (split_prods ~subst tys paramsno ty), snd (split_prods ~subst tys paramsno debruijnedty)) cl @@ -1072,19 +1019,19 @@ and guarded_by_destructors ~subst context recfuns t = let rec_arg = List.nth tl rec_no in aux k rec_arg; List.iter (aux k) tl - | C.Match (ref,outtype,term,pl) as t -> + | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t -> (match R.whd ~subst context term with | C.Rel m | C.Appl (C.Rel m :: _ ) as t when List.mem m safes || m = x -> let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in if not isinductive then recursor aux k t else - let lefts_and_tys,len,cl = fix_lefts_in_constrs ~subst paramsno tl i in + let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in let args = match t with C.Appl (_::tl) -> tl | _ -> [] in aux k outtype; List.iter (aux k) args; List.iter2 (fun p (_,_,bruijnedc) -> - let rl = recursive_args ~subst lefts_and_tys 0 len bruijnedc in + let rl = recursive_args ~subst c_ctx 0 len bruijnedc in let p, k = get_new_safes ~subst k p rl in aux k p) pl cl @@ -1246,7 +1193,7 @@ assert false (* List.fold_right (fun (p,(_,c)) i -> let rl' = - let debruijnedte = debruijn_constructor uri len c in + let debruijnedte = debruijn uri len c in recursive_args lefts_and_tys 0 len debruijnedte in let (e,safes',n',nn',x',context') = @@ -1299,7 +1246,7 @@ assert false (* List.fold_right (fun (p,(_,c)) i -> let rl' = - let debruijnedte = debruijn_constructor uri len c in + let debruijnedte = debruijn uri len c in recursive_args lefts_and_tys 0 len debruijnedte in let (e,safes',n',nn',x',context') =