PARTIAL COMMIT:

 The whole logic of the guarded_by_constructors is being changed.
 The new idea is this one:
  1) The guarded_by_constructors is applied to a term t which must always
     generate an inhabitant of an inductive data type or of a co-inductive
     data type.
  2) When it find a constructor in head position, then the constructor
     must construct the inductive or co-inductive data type of 1).
  3) The type of the formal parameter of a constructor determines what
     condition is checked on the actual parameters of the constructors:
     a) Not recursive: the function must not occur in the actual parameter
     b) Simply recursive (to be defined): the function must occur in the
        actual parameter only guarded by constructors (where the constructor
        has already been found).
     c) Imbricated (i.e. it is another inductive type applied to the one
        that is going to be recursively defined): in this case the guarded
        by constructors (where the constructor has already been found) must
        be called, but:
         I) the expected inductive data type is no more the old one, but
            the one of the inductive data type that is in head position in
            the type.
        II) Once (if) one constructor of I) will be found, its type must
            be considered only after the substitution of the left (?)
            parameters and considering recursion IN THE CO-INDUCTIVE TYPE
            THAT IS THE OUTPUT TYPE OF THE WHOLE COFIX.

What is still wrong with this commit is that we don't have the notion of
imbricated argument yet. So, as soon as an imbricated argument is found,
the invariant 1-3 are broken and sooner or later an exception is raised
or false is returned.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 6529fede1789e1e62ac821a10bd62e481ff506b4..144740013542feb05afab69005d919f29e8e6cfa 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -778,94 +778,88 @@ and guarded_by_destructors n nn kl x safes =
          ) fl true
 
 (*CSC h = 0 significa non ancora protetto *)
-and guarded_by_constructors n nn h =
+and guarded_by_constructors n nn h te =
  let module C = Cic in
-  function
+  (*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 _
-   | 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
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       h = 1 &&
        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) =
+      (* Invariant: we are sure that the constructor is a constructor *)
+      (* of the output inductive type of the whole co-fixpoint.       *)
+      let rl =
        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)
+               | Some rec_args -> assert (not is_inductive) ; rec_args
              )
         | _ ->
          raise (WrongUriToMutualInductiveDefinitions
           (UriManager.string_of_uri uri))
       in
-       is_coinductive &&
        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
+   | 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
+          ) 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
    | 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
    | C.Fix (_,fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
@@ -882,7 +876,7 @@ 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
          ) fl true
 
 and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
@@ -1165,7 +1159,9 @@ and type_of_aux' env t =
             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")
+              raise (NotWellTyped "CoFix: not guarded by constructors") ;
+             if not (returns_a_coinductive ty) then
+              raise (NotWellTyped "CoFix: does not return a coinductive type")
             end
            else
             raise (NotWellTyped "CoFix: ill-typed bodies")
@@ -1210,6 +1206,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,_,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))
+        )
+    | 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))
+        )
+    | C.Prod (_,_,de) -> returns_a_coinductive de
+    | _ -> assert false
+
  in
   type_of_aux env t