From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 May 2008 16:53:33 +0000 (+0000)
Subject: - is_closed removed from the kernel (it used to make a loose test, replaced
X-Git-Tag: make_still_working~5224
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d66222777ea069f6cde311548dc327f5be09ec59;p=helm.git

- is_closed removed from the kernel (it used to make a loose test, replaced
  with a tighter one)
- does_not_occur no longer calls lift (performance improvement)
- does_not_occur: bug fixed in management of Metas
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index ef1442d4e..8282f1402 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -128,10 +128,10 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
    | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2)) 
    | C.Sort _,C.Sort (C.Type _) -> t2
    | C.Sort (C.Type _) , C.Sort C.CProp -> t1
-   | C.Sort _, C.Sort C.CProp -> t2
-   | C.Meta _, C.Sort _
-   | C.Meta _, C.Meta _
-   | C.Sort _, C.Meta _ when U.is_closed t2 -> t2
+   | C.Sort _, C.Sort C.CProp
+   | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _
+   | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (_,(_,(C.Irl 0 | C.Ctx [])))
+   | C.Sort _, C.Meta  (_,(_,(C.Irl 0 | C.Ctx []))) -> t2
    | _ -> 
       raise (TypeCheckerFailure (lazy (Printf.sprintf
         "Prod: expected two sorts, found = %s, %s" 
@@ -218,24 +218,27 @@ let specialize_and_abstract_constrs ~subst r_uri r_len context ty_term =
 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
+  let rec aux k _ = function
+    | C.Rel m when m > n+k && m <= nn+k -> raise DoesOccur
+    | C.Rel m when m > nn+k -> ()
     | C.Rel m ->
-        (try (match List.nth context (m-1) with
-          | _,C.Def (bo,_) -> aux k () (S.lift m bo)
-          | _ -> ())
+        (try match List.nth context (m-1-k) with
+          | _,C.Def (bo,_) -> aux (n-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
+            (* possible optimization here: try does_not_occur on l and
+               perform substitution only if DoesOccur is raised *)
+            let _,_,term,_ = U.lookup_subst mno subst in
+            aux (k-s) () (S.subst_meta (0,l) term)
+          with U.Subst_not_found _ -> match l with
+          | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
+          | C.Ctx lc -> List.iter (aux (k-s) ()) lc)
+    | t -> U.fold (fun _ k -> k + 1) k aux () t
   in
-   try aux (context,n,nn) () t; true
+   try aux 0 () t; true
    with DoesOccur -> false
 ;;
 
diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml
index 213c0457a..5b5045a66 100644
--- a/helm/software/components/ng_kernel/nCicUtils.ml
+++ b/helm/software/components/ng_kernel/nCicUtils.ml
@@ -89,18 +89,3 @@ let map g k f = function
      if oty1 == oty && t1 == t && pl1 == pl then orig 
      else NCic.Match(r,oty1,t1,pl1)
 ;;
-
-exception NotClosed
-
-let is_closed t = 
-  try
-    let rec aux k _ = function
-      | NCic.Rel n when n > k -> raise NotClosed
-      | NCic.Meta (_, (s, NCic.Irl n)) when not (n+s <= k) -> raise NotClosed
-      | NCic.Meta (_, (s, NCic.Ctx l)) -> List.iter (aux (k+s) ()) l 
-      | _ -> fold (fun _ k -> k + 1) k aux () t
-    in 
-      aux 0 () t; true
-  with NotClosed -> false
-;;
-
diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli
index b032a2218..e010f5d19 100644
--- a/helm/software/components/ng_kernel/nCicUtils.mli
+++ b/helm/software/components/ng_kernel/nCicUtils.mli
@@ -29,5 +29,3 @@ val fold:
 val map:
  (NCic.hypothesis -> 'k -> 'k) -> 'k ->
  ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term
-
-val is_closed: NCic.term -> bool