X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=a62238cfbc7aade664f85422222cfde19365b4dd;hb=738ff6e752f9e5facba4e92bdb64453062f52c7d;hp=25042b4cdf8b1d6aee7f82145cee50ac4d29a9ca;hpb=9ae6d985833cf9e6855f41c942dc3c3d24af10e0;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 25042b4cd..a62238cfb 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-(* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *)
+(* $Id$ *)
 
 module C = NCic 
 module R = NCicReduction
@@ -107,11 +107,11 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context =
   let res =
    match t with
     | C.Meta (i,(s,C.Ctx l)) ->
-       let l1 = U.sharing_map (aux (k-s)) l in
+       let l1 = HExtlib.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.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
        C.Rel (k + number_of_types - no)
     | t -> U.map (fun _ k -> k+1) k aux t
   in
@@ -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" 
@@ -151,7 +151,7 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
           prerr_endline (PP.ppterm ~subst ~metasenv ~context
              (S.subst ~avoid_beta_redexes:true arg t));
 *)
-          if R.are_convertible ~subst ~metasenv context ty_arg s then
+          if R.are_convertible ~subst context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
           else
             raise 
@@ -190,8 +190,8 @@ let rec instantiate_parameters params c =
 
 let specialize_inductive_type_constrs ~subst context ty_term =
   match R.whd ~subst context ty_term with
-  | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref)  
-  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) :: _ ) as ty ->
+  | C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref)  
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref) :: _ ) as ty ->
       let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
       let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
       let left_args,_ = HExtlib.split_nth leftno args in
@@ -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 <= k || 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
 ;;
 
@@ -249,8 +252,8 @@ let rec weakly_positive ~subst context n nn uri te =
   let dummy = C.Sort (C.Type ~-1) in
   (*CSC: mettere in cicSubstitution *)
   let rec subst_inductive_type_with_dummy _ = function
-    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
-    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) 
+    | C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))))::tl) 
         when NUri.eq uri' uri -> dummy
     | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
   in
@@ -282,7 +285,7 @@ and strictly_positive ~subst context n nn te =
        strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       List.for_all (does_not_occur ~subst context n nn) tl
-   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as r)::tl) -> 
+   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as r)::tl) -> 
       let _,paramsno,tyl,_,i = E.get_checked_indtys r in
       let _,name,ity,cl = List.nth tyl i in
       let ok = List.length tyl = 1 in
@@ -365,7 +368,7 @@ let rec typeof ~subst ~metasenv context term =
         try
          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
+         let _,c,ty = U.lookup_meta n metasenv in c,ty
         with U.Meta_not_found _ ->
          raise (AssertFailure (lazy (Printf.sprintf
           "%s not found" (PP.ppterm ~subst ~metasenv ~context t))))
@@ -393,7 +396,7 @@ let rec typeof ~subst ~metasenv context term =
     | C.LetIn (n,ty,t,bo) ->
        let ty_t = typeof_aux context t in
        let _ = typeof_aux context ty in
-       if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
+       if not (R.are_convertible ~subst context ty ty_t) then
          raise 
           (TypeCheckerFailure 
             (lazy (Printf.sprintf
@@ -416,7 +419,7 @@ let rec typeof ~subst ~metasenv context term =
 *)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
-   | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
+   | C.Match (Ref.Ref (_,_,Ref.Ind (_,tyno)) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
       let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
       let constructorsno =
@@ -471,7 +474,7 @@ let rec typeof ~subst ~metasenv context term =
               let ty_branch = 
                 type_of_branch ~subst context leftno outtype cons ty_cons 0 
               in
-              j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch,
+              j+1, R.are_convertible ~subst context ty_p ty_branch,
               ty_p, ty_branch
             else
               j,false,old_p_ty,old_exp_p_ty
@@ -533,7 +536,7 @@ let rec typeof ~subst ~metasenv context term =
                 (_,C.Decl t1), (_,C.Decl t2)
               | (_,C.Def (t1,_)), (_,C.Def (t2,_))
               | (_,C.Def (_,t1)), (_,C.Decl t2) ->
-                 if not (R.are_convertible ~subst ~metasenv tl t1 t2) then
+                 if not (R.are_convertible ~subst tl t1 t2) then
                   raise 
                       (TypeCheckerFailure 
                         (lazy (Printf.sprintf 
@@ -584,7 +587,7 @@ let rec typeof ~subst ~metasenv context term =
                     with Failure _ -> t)
               | _ -> t
              in
-             if not (R.are_convertible ~subst ~metasenv context optimized_t ct)
+             if not (R.are_convertible ~subst context optimized_t ct)
              then
                raise 
                  (TypeCheckerFailure 
@@ -595,7 +598,7 @@ let rec typeof ~subst ~metasenv context term =
                      (PP.ppterm ~subst ~metasenv ~context t))))
           | t, (_,C.Decl ct) ->
               let type_t = typeof_aux context t in
-              if not (R.are_convertible ~subst ~metasenv context type_t ct) then
+              if not (R.are_convertible ~subst context type_t ct) then
                 raise (TypeCheckerFailure 
                  (lazy (Printf.sprintf 
                   ("Not well typed metavariable local context: "^^
@@ -630,7 +633,7 @@ let rec typeof ~subst ~metasenv context term =
     let arity2 = R.whd ~subst context arity2 in
       match arity1,arity2 with
        | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
-          if not (R.are_convertible ~subst ~metasenv context so1 so2) then
+          if not (R.are_convertible ~subst context so1 so2) then
            raise (TypeCheckerFailure (lazy (Printf.sprintf
             "In outtype: expected %s, found %s"
             (PP.ppterm ~subst ~metasenv ~context so1)
@@ -639,7 +642,7 @@ let rec typeof ~subst ~metasenv context term =
           aux ((name, C.Decl so1)::context)
            (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
        | C.Sort _, C.Prod (name,so,ta) ->
-          if not (R.are_convertible ~subst ~metasenv context so ind) then
+          if not (R.are_convertible ~subst context so ind) then
            raise (TypeCheckerFailure (lazy (Printf.sprintf
             "In outtype: expected %s, found %s"
             (PP.ppterm ~subst ~metasenv ~context ind)
@@ -805,13 +808,9 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
          ) bos
       in
        List.iter (fun (bo,k) -> aux k bo) bos_and_ks
-  | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
+  | C.Match (Ref.Ref (_,uri,Ref.Ind (true,_)),outtype,term,pl) as t ->
      (match R.whd ~subst context term with
      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
-        (* TODO: add CoInd to references so that this call is useless *)
-        let isinductive, _, _, _, _ = E.get_checked_indtys ref in
-        if not isinductive then recursor aux k t
-        else
          let ty = typeof ~subst ~metasenv context term in
          let dc_ctx, dcl, start, stop = 
            specialize_and_abstract_constrs ~subst r_uri r_len context ty in
@@ -953,17 +952,17 @@ and is_really_smaller
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with
-  | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) 
-  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) ->
-     let isinductive, _, itl, _, _ = E.get_checked_indtys ref in
-     if isinductive then None else (Some (uri,List.length itl))
+  | C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref) 
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref)::_) ->
+     let _, _, itl, _, _ = E.get_checked_indtys ref in
+     Some (uri,List.length itl)
   | C.Prod (n,so,de) ->
      returns_a_coinductive ~subst ((n,C.Decl so)::context) de
   | _ -> None
 
 and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = 
   match E.get_checked_obj uri, ref with
-  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i)  ->
+  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind (_,i))  ->
       let _,_,arity,_ = List.nth tl i in arity
   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j))  ->
       let _,_,_,cl = List.nth tl i in 
@@ -983,7 +982,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
    | C.Constant (_,_,Some te,ty,_) ->
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
-      if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then
+      if not (R.are_convertible ~subst [] ty_te ty) then
        raise (TypeCheckerFailure (lazy (Printf.sprintf (
         "the type of the body is not convertible with the declared one.\n"^^
         "inferred type:\n%s\nexpected type:\n%s")
@@ -1010,7 +1009,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
       in
       List.iter2 (fun (_,name,x,ty,_) bo ->
        let ty_bo = typeof ~subst ~metasenv types bo in
-       if not (R.are_convertible ~subst ~metasenv types ty_bo ty)
+       if not (R.are_convertible ~subst types ty_bo ty)
        then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
        else
         if inductive then begin