X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=63366b4b9997f5897027117458c17a98a7627f05;hb=a9268f8d853c99b4ae22dd7ff998f2ad9a89129b;hp=144740013542feb05afab69005d919f29e8e6cfa;hpb=e001f955d04398adca19bbc30dc5a162183f439f;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 144740013..63366b4b9 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -777,14 +777,17 @@ and guarded_by_destructors n nn kl x safes =
              bo
          ) fl true
 
-(*CSC h = 0 significa non ancora protetto *)
-and guarded_by_constructors n nn h te =
+(* 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.                            *)
+(*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
+and guarded_by_constructors n nn h te args coInductiveTypeURI =
  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 *)
   match CicReduction.whd te with
-     C.Rel m when m > n && m <= nn -> h = 1
+     C.Rel m when m > n && m <= nn -> h
    | C.Rel _
    | C.Var _  -> true
    | C.Meta _
@@ -796,43 +799,107 @@ and guarded_by_constructors n nn h te =
       raise (Impossible 17) (* the term has just been type-checked *)
    | C.Lambda (_,so,de) ->
       does_not_occur n nn so &&
-       guarded_by_constructors (n + 1) (nn + 1) h de
+       guarded_by_constructors (n + 1) (nn + 1) h de args coInductiveTypeURI
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      h = 1 &&
+      h &&
        List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
    | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
-      (* Invariant: we are sure that the constructor is a constructor *)
-      (* of the output inductive type of the whole co-fixpoint.       *)
-      let rl =
+      let consty =
        match CicEnvironment.get_cooked_obj uri cookingsno with
           C.InductiveDefinition (itl,_,_) ->
-           let (_,is_inductive,_,cl) = List.nth itl i in
-            let (_,cons,rrec_args) = List.nth cl (j - 1) in
-             (match !rrec_args with
-                 None -> raise (Impossible 18)
-               | Some rec_args -> assert (not is_inductive) ; rec_args
-             )
+           let (_,_,_,cl) = List.nth itl i in
+            let (_,cons,_) = List.nth cl (j - 1) in cons
         | _ ->
          raise (WrongUriToMutualInductiveDefinitions
           (UriManager.string_of_uri uri))
       in
-       List.fold_right
-        (fun (x,r) i ->
-          i &&
-           if r then
-begin
-let res =
-            guarded_by_constructors n nn 1 x
-in
- if not res then
-  begin
-   prerr_endline ("BECCATO: " ^ CicPp.ppterm x) ; flush stderr ; assert false
-  end ;
- res
-end
-           else
-            does_not_occur n nn x
-        ) (List.combine tl rl) true
+       let rec analyse_branch ty te =
+        match CicReduction.whd ty with
+           C.Meta _ -> raise (Impossible 34)
+         | C.Rel _
+         | C.Var _
+         | C.Sort _ ->
+            does_not_occur n nn te
+         | C.Implicit
+         | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
+         | C.Prod (_,_,de) ->
+            analyse_branch de te
+         | C.Lambda _
+         | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
+         | C.Appl ((C.MutInd (uri,_,_))::tl) as ty
+            when uri == coInductiveTypeURI -> 
+             guarded_by_constructors n nn true te [] coInductiveTypeURI
+         | C.Appl ((C.MutInd (uri,_,_))::tl) as ty -> 
+            guarded_by_constructors n nn true te tl coInductiveTypeURI
+         | C.Appl _ ->
+            does_not_occur n nn te
+         | C.Const _
+         | C.Abst _ -> raise (Impossible 26)
+         | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
+            guarded_by_constructors n nn true te [] coInductiveTypeURI
+         | C.MutInd _ ->
+            does_not_occur n nn te
+         | C.MutConstruct _ -> raise (Impossible 27)
+         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
+         (*CSC: in head position.                                       *)
+         | C.MutCase _
+         | C.Fix _
+         | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
+       in
+       let rec analyse_instantiated_type ty l =
+        match CicReduction.whd ty with
+           C.Rel _
+         | C.Var _
+         | C.Meta _
+         | C.Sort _
+         | C.Implicit
+         | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
+         | C.Prod (_,so,de) ->
+            begin
+             match l with
+                [] -> true
+              | he::tl ->
+                 analyse_branch so he &&
+                  analyse_instantiated_type de tl
+            end
+         | C.Lambda _
+         | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
+         | C.Appl _ -> 
+            List.fold_left (fun i x -> i && does_not_occur n nn x) true l
+         | C.Const _
+         | C.Abst _ -> raise (Impossible 31)
+         | C.MutInd _ ->
+            List.fold_left (fun i x -> i && does_not_occur n nn x) true l
+         | C.MutConstruct _ -> raise (Impossible 32)
+         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
+         (*CSC: in head position.                                       *)
+         | C.MutCase _
+         | C.Fix _
+         | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
+       in
+        let rec instantiate_type args consty =
+         function
+            [] -> true
+          | tlhe::tltl as l ->
+             let consty' = CicReduction.whd 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 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 (Impossible 23)
+                  end
+               | [] -> analyse_instantiated_type consty' l
+                  (* These are all the other cases *)
+       in
+        instantiate_type args consty tl
    | C.Appl ((C.CoFix (_,fl))::tl) ->
       List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
        let len = List.length fl in
@@ -841,14 +908,18 @@ end
          List.fold_right
           (fun (_,ty,bo) i ->
             i && does_not_occur n_plus_len nn_plus_len ty &&
-             guarded_by_constructors n_plus_len nn_plus_len h bo
+             guarded_by_constructors 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 n nn x) true tl &&
         does_not_occur n nn out &&
          does_not_occur n nn te &&
           List.fold_right
-           (fun x i -> i && guarded_by_constructors n nn h x) pl true
+           (fun x i ->
+             i &&
+             guarded_by_constructors n nn h x args coInductiveTypeURI
+           ) pl true
    | C.Appl l ->
       List.fold_right (fun x i -> i && does_not_occur n nn x) l true
    | C.Const _ -> true
@@ -859,7 +930,10 @@ end
        does_not_occur n nn out &&
         does_not_occur n nn te &&
          List.fold_right
-          (fun x i -> i && guarded_by_constructors n nn h x) pl true
+          (fun x i ->
+            i &&
+             guarded_by_constructors n nn h x args coInductiveTypeURI
+          ) pl true
    | C.Fix (_,fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
@@ -876,7 +950,8 @@ end
         List.fold_right
          (fun (_,ty,bo) i ->
            i && does_not_occur n_plus_len nn_plus_len ty &&
-            guarded_by_constructors n_plus_len nn_plus_len h bo
+            guarded_by_constructors n_plus_len nn_plus_len h bo args
+             coInductiveTypeURI
          ) fl true
 
 and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
@@ -1157,11 +1232,14 @@ and type_of_aux' env t =
             (CicSubstitution.lift len ty))
            then
             begin
-             (* let's control the guarded by constructors conditions C{f,M} *)
-             if not (guarded_by_constructors 0 len 0 bo) then
-              raise (NotWellTyped "CoFix: not guarded by constructors") ;
-             if not (returns_a_coinductive ty) then
-              raise (NotWellTyped "CoFix: does not return a coinductive type")
+             (* let's control that the returned type is coinductive *)
+             match returns_a_coinductive ty with
+                None ->
+                 raise(NotWellTyped "CoFix: does not return a coinductive type")
+              | Some uri ->
+                 (*let's control the guarded by constructors conditions C{f,M}*)
+                 if not (guarded_by_constructors 0 len false bo [] uri) then
+                  raise (NotWellTyped "CoFix: not guarded by constructors")
             end
            else
             raise (NotWellTyped "CoFix: ill-typed bodies")
@@ -1210,12 +1288,12 @@ and type_of_aux' env t =
  and returns_a_coinductive ty =
   let module C = Cic in
    match CicReduction.whd ty with
-      C.MutInd (uri,_,i) ->
+      C.MutInd (uri,cookingsno,i) ->
        (*CSC: definire una funzioncina per questo codice sempre replicato *)
-       (match CicEnvironment.get_obj uri with
+       (match CicEnvironment.get_cooked_obj uri cookingsno with
            C.InductiveDefinition (itl,_,_) ->
-            let (_,is_inductive,_,_) = List.nth itl i in
-             not is_inductive
+            let (_,is_inductive,_,cl) = List.nth itl i in
+             if is_inductive then None else (Some uri)
          | _ ->
            raise (WrongUriToMutualInductiveDefinitions
             (UriManager.string_of_uri uri))
@@ -1224,13 +1302,13 @@ and type_of_aux' env t =
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (itl,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
-             not is_inductive
+             if is_inductive then None else (Some uri)
          | _ ->
            raise (WrongUriToMutualInductiveDefinitions
             (UriManager.string_of_uri uri))
         )
     | C.Prod (_,_,de) -> returns_a_coinductive de
-    | _ -> assert false
+    | _ -> None
 
  in
   type_of_aux env t