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 80d4dea0ec3bae7c8648a6d5043a4a6f39faa6a8..f4c6cd4ab154d98a79979af46ce163c82e1feaa2 100644 (file)
--- 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') =