X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=63366b4b9997f5897027117458c17a98a7627f05;hb=09aa799947c84148221af82e94e911adea8fd1e6;hp=5363c5e64f3294a7c06c43277826c33065207d8e;hpb=1f911ae5768c21f0f30c74cbc9bedf537477e5f5;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5363c5e64..63366b4b9 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -285,12 +285,6 @@ and strictly_positive n nn te =
             i &&
              weakly_positive (n+1) (nn+1) uri x
           ) cl' true
-   | C.MutInd (uri,_,i) ->
-      (match CicEnvironment.get_obj uri with
-          C.InductiveDefinition (tl,_,_) ->
-           List.length tl = 1
-        | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
-      )
    | t -> does_not_occur n nn t
 
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
@@ -783,95 +777,163 @@ 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 =
+(* 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
-  function
-     C.Rel m when m > n && m <= nn -> h = 1
+  (*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
    | C.Rel _
-   | C.Var _ 
+   | C.Var _  -> true
    | C.Meta _
    | C.Sort _
-   | C.Implicit -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
-   | C.Cast (te,ty) ->
-      guarded_by_constructors n nn h te &&
-       guarded_by_constructors n nn h ty
-   | C.Prod (_,so,de) ->
+   | C.Implicit
+   | C.Cast _
+   | C.Prod _
+   | C.LetIn _ ->
       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
-   | C.LetIn (_,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) ->
-      let (is_coinductive, 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 -> (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
-       is_coinductive &&
-       List.fold_right
-        (fun (x,r) i ->
-          i &&
-           if r then
-            guarded_by_constructors n nn 1 x
-           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
+        let n_plus_len = n + len
+        and nn_plus_len = nn + len in
+         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 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 args coInductiveTypeURI
+           ) pl true
    | C.Appl l ->
       List.fold_right (fun x i -> i && does_not_occur n nn x) l true
-   | C.Const _
+   | C.Const _ -> true
    | C.Abst _
-   | C.MutInd _ 
-   | C.MutConstruct _ -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
+   | C.MutInd _ -> assert false
+   | C.MutConstruct _ -> true
    | C.MutCase (_,_,_,out,te,pl) ->
-      let rec returns_a_coinductive =
-       function
-          (*CSC: per le regole di tipaggio, la chiamata ricorsiva verra' *)
-          (*CSC: effettata solo una volta, per mangiarsi l'astrazione    *)
-          (*CSC: non dummy                                               *)
-          C.Lambda (_,_,de) -> returns_a_coinductive de
-        | C.MutInd (uri,_,i) ->
-           (*CSC: definire una funzioncina per questo codice sempre replicato *)
-           (match CicEnvironment.get_obj uri with
-               C.InductiveDefinition (itl,_,_) ->
-                let (_,is_inductive,_,_) = List.nth itl i in
-                 not is_inductive
-             | _ ->
-               raise (WrongUriToMutualInductiveDefinitions
-                (UriManager.string_of_uri uri))
-            )
-        (*CSC: bug nella prossima riga (manca la whd) *)
-        | C.Appl ((C.MutInd (uri,_,i))::_) ->
-           (match CicEnvironment.get_obj uri with
-               C.InductiveDefinition (itl,_,_) ->
-                let (_,is_inductive,_,_) = List.nth itl i in
-                 not is_inductive
-             | _ ->
-               raise (WrongUriToMutualInductiveDefinitions
-                (UriManager.string_of_uri uri))
-            )
-        | _ -> false
-      in
        does_not_occur n nn out &&
         does_not_occur n nn te &&
-        if returns_a_coinductive out then
          List.fold_right
-          (fun x i -> i && guarded_by_constructors n nn h x) pl true
-        else
-         List.fold_right (fun x i -> i && does_not_occur n nn 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
@@ -888,7 +950,8 @@ and guarded_by_constructors n nn h =
         List.fold_right
          (fun (_,ty,bo) i ->
            i && does_not_occur n_plus_len nn_plus_len ty &&
-            does_not_occur n_plus_len nn_plus_len 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 =
@@ -1024,9 +1087,8 @@ and type_of_aux' env t =
          let _ = sort_of_prod (sort1,sort2) in
           C.Prod (n,s,type2)
    | C.LetIn (n,s,t) ->
-       let type1 = type_of_aux env s in
-       let type2 = type_of_aux (type1::env) t in
-        type2
+       let t' = CicSubstitution.subst s t in
+        type_of_aux env t'
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux env he
       and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
@@ -1170,9 +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")
+             (* 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")
@@ -1217,6 +1284,32 @@ and type_of_aux' env t =
           end
       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
     )
+
+ and returns_a_coinductive ty =
+  let module C = Cic in
+   match CicReduction.whd ty with
+      C.MutInd (uri,cookingsno,i) ->
+       (*CSC: definire una funzioncina per questo codice sempre replicato *)
+       (match CicEnvironment.get_cooked_obj uri cookingsno with
+           C.InductiveDefinition (itl,_,_) ->
+            let (_,is_inductive,_,cl) = List.nth itl i in
+             if is_inductive then None else (Some uri)
+         | _ ->
+           raise (WrongUriToMutualInductiveDefinitions
+            (UriManager.string_of_uri uri))
+        )
+    | C.Appl ((C.MutInd (uri,_,i))::_) ->
+       (match CicEnvironment.get_obj uri with
+           C.InductiveDefinition (itl,_,_) ->
+            let (_,is_inductive,_,_) = List.nth itl i in
+             if is_inductive then None else (Some uri)
+         | _ ->
+           raise (WrongUriToMutualInductiveDefinitions
+            (UriManager.string_of_uri uri))
+        )
+    | C.Prod (_,_,de) -> returns_a_coinductive de
+    | _ -> None
+
  in
   type_of_aux env t