added slim version of does_not_occur

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index ecc63445ca364d4f97117e86d13c0ea60fd0359a..fd7e756ce9a0552f6ce0ccaa8b85aecc8f970ffc 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -89,90 +89,6 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
 
 exception CicEnvironmentError;;
 
-and does_not_occur ?(subst=[]) context n nn te =
- let module C = Cic in
-   match te with
-      C.Rel m when m > n && m <= nn -> false
-    | C.Rel m ->
-       (try
-         (match List.nth context (m-1) with
-             Some (_,C.Def (bo,_)) ->
-              does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
-           | _ -> true)
-        with
-         Failure _ -> assert false)
-    | C.Sort _
-    | C.Implicit _ -> true
-    | C.Meta (_,l) ->
-       List.fold_right
-        (fun x i ->
-          match x with
-             None -> i
-           | Some x -> i && does_not_occur ~subst context n nn x) l true &&
-       (try
-         let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
-          does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
-        with
-         CicUtil.Subst_not_found _ -> true)
-    | C.Cast (te,ty) ->
-       does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
-    | C.Prod (name,so,dest) ->
-       does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
-         (nn + 1) dest
-    | C.Lambda (name,so,dest) ->
-       does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
-         dest
-    | C.LetIn (name,so,ty,dest) ->
-       does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst context n nn ty &&
-         does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
-          (n + 1) (nn + 1) dest
-    | C.Appl l ->
-       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
-    | C.Var (_,exp_named_subst)
-    | C.Const (_,exp_named_subst)
-    | C.MutInd (_,_,exp_named_subst)
-    | C.MutConstruct (_,_,_,exp_named_subst) ->
-       List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
-        exp_named_subst true
-    | C.MutCase (_,_,out,te,pl) ->
-       does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
-        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
-    | C.Fix (_,fl) ->
-       let len = List.length fl in
-        let n_plus_len = n + len in
-        let nn_plus_len = nn + len in
-        let tys,_ =
-         List.fold_left
-          (fun (types,len) (n,_,ty,_) ->
-             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-              len+1)
-          ) ([],0) fl
-        in
-         List.fold_right
-          (fun (_,_,ty,bo) i ->
-            i && does_not_occur ~subst context n nn ty &&
-            does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
-          ) fl true
-    | C.CoFix (_,fl) ->
-       let len = List.length fl in
-        let n_plus_len = n + len in
-        let nn_plus_len = nn + len in
-        let tys,_ =
-         List.fold_left
-          (fun (types,len) (n,ty,_) ->
-             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-              len+1)
-          ) ([],0) fl
-        in
-         List.fold_right
-          (fun (_,ty,bo) i ->
-            i && does_not_occur ~subst context n nn ty &&
-            does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
-          ) fl true
-
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
@@ -1293,6 +1209,30 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
     aux ty_he args_with_ty
 ;;
 
+exception DoesOccur;;
+
+let does_not_occur ~subst context n nn t = 
+  let rec aux (context,n,nn as k) _ = function
+    | C.Rel m when m > n && m <= nn -> raise DoesOccur
+    | C.Rel m ->
+        (try (match List.nth context (m-1) with
+          | _,C.Def (bo,_) -> aux k () (S.lift m bo)
+          | _ -> ())
+         with Failure _ -> assert false)
+    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
+    | C.Meta (mno,(s,l)) ->
+         (try
+           let _,_,term,_ = U.lookup_subst mno subst in
+           aux (context,n+s,nn+s) () (S.subst_meta (0,l) term)
+          with CicUtil.Subst_not_found _ -> match l with
+          | C.Irl len -> if not (n >= s+len || s > nn) then raise DoesOccur
+          | C.Ctx lc -> List.iter (aux (context,n+s,nn+s) ()) lc)
+    | t -> U.fold (fun e (ctx,n,nn) -> (e::ctx,n+1,nn+1)) k aux () t
+  in
+   try aux (context,n,nn) () t; true
+   with DoesOccur -> false
+;;
+
 let rec typeof ~subst ~metasenv context term =
   let rec typeof_aux context = function
     | C.Rel n ->
@@ -1307,10 +1247,10 @@ let rec typeof ~subst ~metasenv context term =
     | C.Meta (n,l) as t -> 
        let canonical_context,ty =
         try
-         let _,c,_,ty = NCicUtils.lookup_subst n subst in c,ty
-        with NCicUtils.Subst_not_found _ -> try
-         let _,_,c,ty = NCicUtils.lookup_meta n metasenv in c,ty
-        with NCicUtils.Meta_not_found _ ->
+         let _,c,_,ty = U.lookup_subst n subst in c,ty
+        with U.Subst_not_found _ -> try
+         let _,_,c,ty = U.lookup_meta n metasenv in c,ty
+        with U.Meta_not_found _ ->
          raise (AssertFailure (lazy (Printf.sprintf
           "%s not found" (NCicPp.ppterm t))))
        in
@@ -1475,7 +1415,7 @@ let rec typeof ~subst ~metasenv context term =
                           S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
          in
           lift_metas 1 canonical_context in
-       let l = NCicUtils.expand_local_context lc_kind in
+       let l = U.expand_local_context lc_kind in
        try
         List.iter2 
         (fun t ct -> 
@@ -1643,8 +1583,7 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) =
       in
         List.iter (fun (_,name,x,ty,bo) ->
          let ty_bo = typeof ~subst ~metasenv types bo in
-         if not (R.are_convertible ~subst ~metasenv types ty_bo
-            (S.lift len ty))
+         if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty))
          then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
          else
           if inductive then begin