X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=fbb384d5e66eb63909ae88aafaebb3a75f3c7c4e;hb=6beda5aa100b617b75d88a5a519b5022c99208a0;hp=8f36b9e1780e1d562c99939f7b791d181b615aec;hpb=37018b8195f0f376d9eb04a98cbda5550f7ac8ef;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 8f36b9e17..fbb384d5e 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -292,8 +292,12 @@ and does_not_occur ?(subst=[]) context n nn te =
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
-        let tys =
-         List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+        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 ->
@@ -304,8 +308,12 @@ and does_not_occur ?(subst=[]) context n nn te =
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
-        let tys =
-         List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+        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 ->
@@ -886,7 +894,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       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
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
@@ -899,7 +912,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       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
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
@@ -1091,7 +1109,12 @@ and guarded_by_destructors ~subst context n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       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
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
@@ -1104,7 +1127,12 @@ and guarded_by_destructors ~subst context n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       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
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
@@ -1257,7 +1285,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
         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.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+        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 &&
@@ -1298,7 +1332,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
        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.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
+       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 &&
@@ -1309,7 +1349,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
        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.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+       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 &&
@@ -1458,8 +1504,25 @@ and check_metasenv_consistency ~logger ~subst metasenv context
        match (t,ct) with
        | _,None -> ugraph
        | Some t,Some (_,C.Def (ct,_)) ->
+          (*CSC: the following optimization is to avoid a possibly expensive
+                 reduction that can be easily avoided and that is quite
+                 frequent. However, this is better handled using levels to
+                 control reduction *)
+          let optimized_t =
+           match t with
+              Cic.Rel n ->
+               (try
+                 match List.nth context (n - 1) with
+                    Some (_,C.Def (te,_)) -> S.lift n te
+                  | _ -> t
+                with
+                 Failure _ -> t)
+            | _ -> t
+          in
+(*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!"
+else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*)
 	   let b,ugraph1 = 
-	     R.are_convertible ~subst ~metasenv context t ct ugraph 
+	     R.are_convertible ~subst ~metasenv context optimized_t ct ugraph 
 	   in
 	   if not b then
 	     raise 
@@ -1608,7 +1671,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 List.fold_right (
 	   fun x (l,ugraph) -> 
 	     let ty,ugraph1 = type_of_aux ~logger context x ugraph in
-	     let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in
+	     (*let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in*)
 	       ((x,ty)::l,ugraph1)) 
 	   tl ([],ugraph1) 
        in
@@ -1768,21 +1831,28 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       in
 	if not b then
         raise
-          (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed")));
+          (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed")));
         (* let's check if the type of branches are right *)
-      let parsno =
+      let parsno,constructorsno =
         let obj,_ =
           try
             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
           with Not_found -> assert false
         in
         match obj with
-            C.InductiveDefinition (_,_,parsno,_) -> parsno
+            C.InductiveDefinition (il,_,parsno,_) ->
+             let _,_,_,cl =
+              try List.nth il i with Failure _ -> assert false
+             in
+              parsno, List.length cl
           | _ ->
               raise (TypeCheckerFailure
                 (lazy ("Unknown mutual inductive definition:" ^
                   UriManager.string_of_uri uri)))
-	in
+      in
+      if List.length pl <> constructorsno then
+       raise (TypeCheckerFailure
+        (lazy ("Wrong number of cases in case analysis"))) ;
       let (_,branches_ok,ugraph5) =
         List.fold_left
           (fun (j,b,ugraph) p ->
@@ -1834,16 +1904,14 @@ end;
           in
            outtype,ugraph5
    | C.Fix (i,fl) ->
-      let types_times_kl,ugraph1 =
-	(* WAS: list rev list map *)
+      let types,kl,ugraph1,len =
         List.fold_left
-          (fun (l,ugraph) (n,k,ty,_) ->
+          (fun (types,kl,ugraph,len) (n,k,ty,_) ->
             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
-            ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
-	  ) ([],ugraph) fl
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              k::kl,ugraph1,len+1)
+	  ) ([],[],ugraph,0) fl
       in
-      let (types,kl) = List.split types_times_kl in
-      let len = List.length types in
       let ugraph2 = 
 	List.fold_left
           (fun ugraph (name,x,ty,bo) ->
@@ -1877,15 +1945,15 @@ end;
       let (_,_,ty,_) = List.nth fl i in
 	ty,ugraph2
    | C.CoFix (i,fl) ->
-       let types,ugraph1 =
+       let types,ugraph1,len =
 	 List.fold_left
-	   (fun (l,ugraph) (n,ty,_) -> 
+	   (fun (l,ugraph,len) (n,ty,_) -> 
               let _,ugraph1 = 
 		type_of_aux ~logger context ty ugraph in 
-		(Some (C.Name n,(C.Decl ty))::l,ugraph1)
-	   ) ([],ugraph) fl
+		(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
+                 ugraph1,len+1)
+	   ) ([],ugraph,0) fl
        in
-       let len = List.length types in
        let ugraph2 = 
 	 List.fold_left
            (fun ugraph (_,ty,bo) ->
@@ -1991,6 +2059,8 @@ end;
 	 (match (CicReduction.whd ~subst context hetype) with 
               Cic.Prod (n,s,t) ->
 		let b,ugraph1 = 
+(*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then(
+prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*)
 		  CicReduction.are_convertible 
 		    ~subst ~metasenv context hety s ugraph 
 		in