X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=6cbb44f8044432db90ae2cd361d2831cb132be8d;hb=d025518bc5930796c748704b069a2719b34b00d3;hp=bcdb340bd1d137af0393fbd1cf2cfe6fc028fc17;hpb=e8f4be1c4c7d4162035dd45ac4ea38b9ed168098;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index bcdb340bd..6cbb44f80 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -141,12 +141,12 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri n
 
 exception CicEnvironmentError;;
 
-let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
+let rec type_of_constant ~logger uri orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let cobj,ugraph =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+   match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
     | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
        logger#log (`Start_type_checking uri) ;
@@ -154,7 +154,7 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
        let inferred_ugraph = 
          match uobj with
            C.Constant (_,Some te,ty,_,_) ->
-           let _,ugraph = type_of ~logger ty ugraph in
+           let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
            let type_of_te,ugraph = type_of ~logger te ugraph in
               let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
               if not b then
@@ -166,17 +166,17 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
                 ugraph
          | C.Constant (_,None,ty,_,_) ->
            (* only to check that ty is well-typed *)
-           let _,ugraph = type_of ~logger ty ugraph in 
+           let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in 
            ugraph
          | C.CurrentProof (_,conjs,te,ty,_,_) ->
              let _,ugraph =
               List.fold_left
                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
                  let _,ugraph = 
-		   type_of_aux' ~logger metasenv context ty ugraph 
+		  type_of_aux' ~logger metasenv context ty ugraph 
 		 in
                  (metasenv @ [conj],ugraph)
-               ) ([],ugraph) conjs
+               ) ([],CicUniv.empty_ugraph) conjs
              in
              let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
              let type_of_te,ugraph = type_of_aux' ~logger conjs [] te ugraph in
@@ -205,17 +205,19 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
     | _ ->
         raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
 
-and type_of_variable ~logger uri (ugraph as orig_ugraph) =
+and type_of_variable ~logger uri orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   (* 0 because a variable is never cooked => no partial cooking at one level *)
-  match CicEnvironment.is_type_checked ~trust:true ugraph uri with
-     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
-   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph) ->
+  match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
+  | CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
+  | CicEnvironment.UncheckedObj 
+     (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph) 
+    ->
       logger#log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
-      let _,ugraph = type_of ~logger ty ugraph in
+      let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
       let inferred_ugraph = 
        match bo with
            None -> ugraph
@@ -228,7 +230,9 @@ and type_of_variable ~logger uri (ugraph as orig_ugraph) =
 	     else
 	       ugraph 
       in
-       let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+       let ugraph, ul, obj = 
+         check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj 
+       in
        CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
        logger#log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
@@ -236,7 +240,8 @@ and type_of_variable ~logger uri (ugraph as orig_ugraph) =
          | CicEnvironment.CheckedObj _ 
          | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError)
    |  _ ->
-	raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
+	raise (TypeCheckerFailure (lazy 
+          ("Unknown variable:" ^ U.string_of_uri uri)))
 
 and does_not_occur ?(subst=[]) context n nn te =
  let module C = Cic in
@@ -264,14 +269,15 @@ and does_not_occur ?(subst=[]) context n nn te =
         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
+       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)
+        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 &&
@@ -279,16 +285,17 @@ and does_not_occur ?(subst=[]) context n nn te =
          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
+       List.for_all (does_not_occur ~subst context n nn) l
     | 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
+       List.for_all (fun (_,x) -> does_not_occur ~subst context n nn x)
+        exp_named_subst
     | 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
+       does_not_occur ~subst context n nn out && 
+       does_not_occur ~subst context n nn te &&
+       List.for_all (does_not_occur ~subst context n nn) pl
     | C.Fix (_,fl) ->
        let len = List.length fl in
         let n_plus_len = n + len in
@@ -550,25 +557,35 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
   (* constructors using Prods                                *)
   let len = List.length itl in
   let tys =
-    List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
+    List.rev_map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
   let _,ugraph2 =
     List.fold_right
-      (fun (_,_,_,cl) (i,ugraph) ->
+      (fun (_,_,ty,cl) (i,ugraph) ->
+        let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in
 	let ugraph'' = 
           List.fold_left
             (fun ugraph (name,te) -> 
-              let debrujinedte = debrujin_constructor uri len [] te in
-              let augmented_term =
-		List.fold_right
-		  (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
-		  itl debrujinedte
-              in
-              let _,ugraph' = type_of ~logger augmented_term ugraph in
+              let te = debrujin_constructor uri len [] te in
+              let context,te = split_prods ~subst:[] tys indparamsno te in
+              let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in
+              let ugraph =
+               match
+                CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
+               with
+                  Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) ->
+                   CicUniv.add_ge u2 u1 ugraph
+                | Cic.Sort _, Cic.Sort Cic.Prop
+                | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp
+                | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
+                | _, _ ->
+                   raise
+                    (TypeCheckerFailure
+                      (lazy ("Wrong constructor or inductive arity shape"))) in
               (* let's check also the positivity conditions *)
               if
 		not
-		  (are_all_occurrences_positive tys uri indparamsno i 0 len
-                     debrujinedte)
+		  (are_all_occurrences_positive context uri indparamsno
+                    (i+indparamsno) indparamsno (len+indparamsno) te)
               then
                 begin
                 prerr_endline (UriManager.string_of_uri uri);
@@ -577,7 +594,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 		  (TypeCheckerFailure
                     (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
               else
-		ugraph'
+		ugraph
             ) ugraph cl in
 	(i + 1),ugraph''
       ) itl (1,ugrap1)
@@ -595,16 +612,18 @@ and check_mutual_inductive_defs uri obj ugraph =
 		lazy ("Unknown mutual inductive definition:" ^
 		 UriManager.string_of_uri uri)))
 
-and type_of_mutual_inductive_defs ~logger uri i (ugraph as orig_ugraph) =
+and type_of_mutual_inductive_defs ~logger uri i orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj,ugraph1 =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+   match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
      | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
 	 logger#log (`Start_type_checking uri) ;
-	 let inferred_ugraph = check_mutual_inductive_defs ~logger uri uobj ugraph in
+	 let inferred_ugraph = 
+           check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph 
+         in
          let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
 	 CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
 	 logger#log (`Type_checking_completed uri) ;
@@ -613,25 +632,25 @@ and type_of_mutual_inductive_defs ~logger uri i (ugraph as orig_ugraph) =
 	    | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 	 )
   in
-    match cobj with
-	C.InductiveDefinition (dl,_,_,_) ->
-	  let (_,_,arity,_) = List.nth dl i in
-	    arity,ugraph1
-      | _ ->
-	  raise (TypeCheckerFailure
-           (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
+  match cobj with
+  | C.InductiveDefinition (dl,_,_,_) ->
+      let (_,_,arity,_) = List.nth dl i in
+        arity,ugraph1
+  | _ ->
+     raise (TypeCheckerFailure
+      (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
 	    
-and type_of_mutual_inductive_constr ~logger uri i j (ugraph as orig_ugraph) =
+and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj,ugraph1 =
-    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+    match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
 	CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
       | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
 	  logger#log (`Start_type_checking uri) ;
 	  let inferred_ugraph = 
-	    check_mutual_inductive_defs ~logger uri uobj ugraph 
+	    check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph 
 	  in
           let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
 	  CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
@@ -699,7 +718,8 @@ and split_prods ~subst context n te =
  let module R = CicReduction in
   match (n, R.whd ~subst context te) with
      (0, _) -> context,te
-   | (n, C.Prod (name,so,ta)) when n > 0 ->
+   | (n, C.Sort _) when n <= 0 -> context,te
+   | (n, C.Prod (name,so,ta)) ->
        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
    | (_, _) -> raise (AssertFailure (lazy "8"))
 
@@ -737,7 +757,7 @@ and specialize_inductive_type ~logger ~subst ~metasenv context t =
                cl 
             in
             name, isind, arity, cl)
-          tl
+          tl, paramsno
       | _ -> assert false)
   | _ -> assert false
 
@@ -764,11 +784,15 @@ and check_is_really_smaller_arg
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
       | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
-         let tys = 
+         let tys,_ = 
            specialize_inductive_type ~logger ~subst ~metasenv context term 
          in
-         let tys_ctx = 
-           List.map (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+         let tys_ctx,_ = 
+           List.fold_left
+             (fun (types,len) (n,_,ty,_) ->
+               Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+               len+1) 
+             ([],0) tys
          in
          let _,isinductive,_,cl = List.nth tys i in
          if not isinductive then
@@ -825,7 +849,9 @@ and guarded_by_destructors
 =
  let module C = Cic in
  let module U = UriManager in
-  match CicReduction.whd ~subst context t with
+  let t = CicReduction.whd ~delta:false ~subst context t in
+  let res =
+   match t with
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
       (match List.nth context (m-1) with
@@ -878,12 +904,15 @@ and guarded_by_destructors
            List.for_all
              (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
              tl &&
-           let tys = 
+           let tys,_ = 
              specialize_inductive_type ~logger ~subst ~metasenv context t
            in
-           let tys_ctx = 
-             List.map 
-               (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+           let tys_ctx,_ = 
+             List.fold_left
+               (fun (types,len) (n,_,ty,_) ->
+                 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                 len+1) 
+               ([],0) tys
            in
            let _,isinductive,_,cl = List.nth tys i in
             if not isinductive then
@@ -979,228 +1008,124 @@ and guarded_by_destructors
       List.fold_right
        (fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
        tl true
+  in
+   if res then res
+   else
+    let t' = CicReduction.whd ~subst context t in
+     if t = t' then
+      false
+     else
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t'
 
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
 (* found in head position must be applied to.                            *)
-and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
+and guarded_by_constructors ~logger ~subst ~metasenv indURI =
  let module C = Cic in
-  (*CSC: There is a lot of code replication between the cases X and    *)
-  (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
-  (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
+ let rec aux context n nn h te =
   match CicReduction.whd ~subst context te with
-     C.Rel m when m > n && m <= nn -> h
-   | C.Rel _ -> true
-   | C.Meta _
+   | C.Rel m when m > n && m <= nn -> h
+   | C.Rel _ 
+   | C.Meta _ -> true
    | C.Sort _
    | C.Implicit _
    | C.Cast _
    | C.Prod _
-   | C.LetIn _ ->
-      (* the term has just been type-checked *)
-      raise (AssertFailure (lazy "17"))
+   | C.MutInd _ 
+   | C.LetIn _ -> raise (AssertFailure (lazy "17"))
    | C.Lambda (name,so,de) ->
       does_not_occur ~subst context n nn so &&
-       guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
-        (n + 1) (nn + 1) h de args coInductiveTypeURI
+      aux ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) h de
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      h &&
-       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
-   | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
-      let consty =
-	let obj,_ = 
-	  try 
-	    CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
-	  with Not_found -> assert false
-	in
-       match obj with
-          C.InductiveDefinition (itl,_,_,_) ->
-           let (_,_,_,cl) = List.nth itl i in
-            let (_,cons) = List.nth cl (j - 1) in
-             CicSubstitution.subst_vars exp_named_subst cons
-        | _ ->
-            raise (TypeCheckerFailure
-             (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
+      h && List.for_all (does_not_occur ~subst context n nn) tl
+   | C.MutConstruct (_,_,_,exp_named_subst) ->
+      List.for_all 
+        (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst
+   | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) as t ->
+      List.for_all 
+        (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst &&
+      let consty, len_tys, tys_ctx, paramsno =
+       let tys, paramsno = 
+         specialize_inductive_type ~logger ~subst ~metasenv context t in
+       let _,_,_,cl = List.nth tys i in  
+       let _,ty = List.nth cl (j-1) in  
+         ty, List.length tys,
+         fst(List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+           Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1)
+          ([],0) tys), paramsno
       in
-       let rec analyse_branch context ty te =
-        match CicReduction.whd ~subst context ty with
-           C.Meta _ -> raise (AssertFailure (lazy "34"))
-         | C.Rel _
-         | C.Var _
-         | C.Sort _ ->
-            does_not_occur ~subst context n nn te
-         | C.Implicit _
-         | C.Cast _ ->
-            raise (AssertFailure (lazy "24"))(* due to type-checking *)
-         | C.Prod (name,so,de) ->
-            analyse_branch ((Some (name,(C.Decl so)))::context) de te
-         | C.Lambda _
-         | C.LetIn _ ->
-            raise (AssertFailure (lazy "25"))(* due to type-checking *)
-         | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> 
-             guarded_by_constructors ~subst context n nn true te []
-              coInductiveTypeURI
-         | C.Appl ((C.MutInd (uri,_,_))::_) -> 
-            guarded_by_constructors ~subst context n nn true te tl
-             coInductiveTypeURI
-         | C.Appl _ ->
-            does_not_occur ~subst context n nn te
-         | C.Const _ -> raise (AssertFailure (lazy "26"))
-         | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
-            guarded_by_constructors ~subst context n nn true te []
-             coInductiveTypeURI
-         | C.MutInd _ ->
-            does_not_occur ~subst context n nn te
-         | C.MutConstruct _ -> raise (AssertFailure (lazy "27"))
-         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
-         (*CSC: in head position.                                       *)
-         | C.MutCase _
-         | C.Fix _
-         | C.CoFix _ ->
-            raise (AssertFailure (lazy "28"))(* due to type-checking *)
-       in
-       let rec analyse_instantiated_type context ty l =
-        match CicReduction.whd ~subst context ty with
-           C.Rel _
-         | C.Var _
-         | C.Meta _
-         | C.Sort _
-         | C.Implicit _
-         | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *)
-         | C.Prod (name,so,de) ->
-            begin
-             match l with
-                [] -> true
-              | he::tl ->
-                 analyse_branch context so he &&
-                  analyse_instantiated_type
-                   ((Some (name,(C.Decl so)))::context) de tl
-            end
-         | C.Lambda _
-         | C.LetIn _ ->
-            raise (AssertFailure (lazy "30"))(* due to type-checking *)
-         | C.Appl _ -> 
-            List.fold_left
-             (fun i x -> i && does_not_occur ~subst context n nn x) true l
-         | C.Const _ -> raise (AssertFailure (lazy "31"))
-         | C.MutInd _ ->
-            List.fold_left
-             (fun i x -> i && does_not_occur ~subst context n nn x) true l
-         | C.MutConstruct _ -> raise (AssertFailure (lazy "32"))
-         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
-         (*CSC: in head position.                                       *)
-         | C.MutCase _
-         | C.Fix _
-         | C.CoFix _ ->
-            raise (AssertFailure (lazy "33"))(* due to type-checking *)
-       in
-        let rec instantiate_type args consty =
-         function
-            [] -> true
-          | tlhe::tltl as l ->
-             let consty' = CicReduction.whd ~subst context consty in
-              match args with 
-                 he::tl ->
-                  begin
-                   match consty' with
-                      C.Prod (_,_,de) ->
-                       let instantiated_de = CicSubstitution.subst he de in
-                        (*CSC: siamo sicuri che non sia troppo forte? *)
-                        does_not_occur ~subst context n nn tlhe &
-                         instantiate_type tl instantiated_de tltl
-                    | _ ->
-                      (*CSC:We do not consider backbones with a MutCase, a    *)
-                      (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
-                      raise (AssertFailure (lazy "23"))
-                  end
-               | [] -> analyse_instantiated_type context consty' l
-                  (* These are all the other cases *)
+      let rec_params =
+       let c = 
+         debrujin_constructor ~check_exp_named_subst:false
+           indURI len_tys context consty 
        in
-        instantiate_type args consty tl
-   | C.Appl ((C.CoFix (_,fl))::tl) ->
-      List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
-       let len = List.length fl in
-        let n_plus_len = n + len
-        and nn_plus_len = nn + len
-        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-        and 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 &&
-             guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
-              h bo args coInductiveTypeURI
-          ) fl true
-   | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
-       List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
-        does_not_occur ~subst context n nn out &&
-         does_not_occur ~subst context n nn te &&
-          List.fold_right
-           (fun x i ->
-             i &&
-             guarded_by_constructors ~subst context n nn h x args
-              coInductiveTypeURI
-           ) pl true
-   | 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) ->
-      List.fold_right
-       (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
-   | C.MutInd _ -> assert false
-   | 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) ->
+       let len_ctx = List.length context in
+       recursive_args (context@tys_ctx) len_ctx (len_ctx+len_tys) c
+      in
+      let rec analyse_instantiated_type rec_spec args =
+       match rec_spec, args with
+       | h::rec_spec, he::args -> 
+           aux context n nn h he &&
+           analyse_instantiated_type rec_spec args 
+       | _,[] -> true
+       | _ -> raise (AssertFailure (lazy 
+         ("Too many args for constructor: " ^ String.concat " "
+         (List.map (fun x-> CicPp.ppterm x) args))))
+      in
+      let left, args = HExtlib.split_nth paramsno tl in
+      List.for_all (does_not_occur ~subst context n nn) left &&
+      analyse_instantiated_type rec_params args
+   | C.Appl ((C.MutCase (_,_,out,te,pl))::_) 
+   | C.MutCase (_,_,out,te,pl) as t ->
+       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+       List.for_all (does_not_occur ~subst context n nn) tl &&
        does_not_occur ~subst context n nn out &&
-        does_not_occur ~subst context n nn te &&
-         List.fold_right
-          (fun x i ->
-            i &&
-             guarded_by_constructors ~subst context n nn h x args
-              coInductiveTypeURI
-          ) pl true
-   | C.Fix (_,fl) ->
+       does_not_occur ~subst context n nn te &&
+       List.for_all (aux context n nn h ) pl
+   | C.Fix (_,fl)
+   | C.Appl (C.Fix (_,fl)::_) as t ->
+       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
       let len = List.length fl in
        let n_plus_len = n + len
        and nn_plus_len = nn + len
-       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
        and tys,_ =
         List.fold_left
           (fun (types,len) (n,_,ty,_) ->
              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
               len+1)
-	  ) ([],0) fl
+          ) ([],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
+        List.for_all (does_not_occur ~subst context n nn) tl &&
+        List.for_all
+         (fun (_,_,ty,bo) ->
+           does_not_occur ~subst context n nn ty &&
+           aux (tys@context) n_plus_len nn_plus_len h bo)
+         fl
+   | C.Appl ((C.CoFix (_,fl))::_) 
+   | C.CoFix (_,fl) as t ->
+       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+       let len = List.length fl in
        let n_plus_len = n + len
        and nn_plus_len = nn + len
-       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
        and tys,_ =
-        List.fold_left
-          (fun (types,len) (n,ty,_) ->
-             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-              len+1)
-	  ) ([],0) fl
+          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 &&
-            guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
-             h bo
-             args coInductiveTypeURI
-         ) fl true
+       List.for_all (does_not_occur ~subst context n nn) tl &&
+       List.for_all 
+         (fun (_,ty,bo) ->
+            does_not_occur ~subst context n nn ty &&
+            aux (tys@context) n_plus_len nn_plus_len h bo) 
+         fl
+   | C.Var _
+   | C.Const _
+   | C.Appl _ as t -> does_not_occur ~subst context n nn t
+ in
+   aux 
 
 and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   need_dummy ind arity1 arity2 ugraph =
@@ -1414,7 +1339,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
     | C.Var (uri,exp_named_subst) ->
       incr fdebug ;
 	let ugraph1 = 
-	  check_exp_named_subst ~logger ~subst context exp_named_subst ugraph 
+	  check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph 
 	in 
 	let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
 	let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
@@ -1527,7 +1452,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.Const (uri,exp_named_subst) ->
        incr fdebug ;
        let ugraph1 = 
-	 check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph 
+	 check_exp_named_subst uri ~logger ~subst  context exp_named_subst ugraph 
        in
        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
        let cty1 =
@@ -1538,11 +1463,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.MutInd (uri,i,exp_named_subst) ->
       incr fdebug ;
        let ugraph1 = 
-	 check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph 
+	 check_exp_named_subst uri ~logger  ~subst context exp_named_subst ugraph 
        in
-	 (* TASSI: da me c'era anche questa, ma in CVS no *)
        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
-	 (* fine parte dubbia *)
        let cty =
 	 CicSubstitution.subst_vars exp_named_subst mty
        in
@@ -1550,9 +1473,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 cty,ugraph2
    | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let ugraph1 = 
-	 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph 
+	 check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
        in
-	 (* TASSI: idem come sopra *)
        let mty,ugraph2 = 
 	 type_of_mutual_inductive_constr ~logger uri i j ugraph1 
        in
@@ -1843,8 +1765,8 @@ end;
 			    let's control the guarded by constructors 
 			    conditions C{f,M}
 			  *)
-			  if not (guarded_by_constructors ~subst
-                              (types @ context) 0 len false bo [] uri) then
+			  if not (guarded_by_constructors ~logger ~subst ~metasenv uri
+                 (types @ context) 0 len false bo) then
 			    raise
 			      (TypeCheckerFailure 
 				(lazy "CoFix: not guarded by constructors"))
@@ -1859,7 +1781,24 @@ end;
        let (_,ty,_) = List.nth fl i in
 	 ty,ugraph2
 
- and check_exp_named_subst ~logger ~subst context =
+ and check_exp_named_subst uri ~logger ~subst context ens ugraph =
+   let params =
+    let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    (match obj with
+        Cic.Constant (_,_,_,params,_) -> params
+      | Cic.Variable (_,_,_,params,_) -> params
+      | Cic.CurrentProof (_,_,_,_,params,_) -> params
+      | Cic.InductiveDefinition (_,params,_,_) -> params
+    ) in
+   let rec check_same_order params ens =
+    match params,ens with
+     | _,[] -> ()
+     | [],_::_ ->
+        raise (TypeCheckerFailure (lazy "Bad explicit named substitution"))
+     | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' ->
+        check_same_order tl tl'
+     | _::tl,l -> check_same_order tl l
+   in
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
 	 [] -> ugraph
@@ -1885,7 +1824,8 @@ end;
 		 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
-     check_exp_named_subst_aux ~logger []
+    check_same_order params ens ;
+    check_exp_named_subst_aux ~logger [] ens ugraph
        
  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in