1. bug fixed: the context must be type-checked before using it in type_of_aux'.

   Otherwise get_cooked_obj raises Not_found in Deannotate
2. big improvement in guarded_by_destructors: when a fix applied to a safe
   argument is found in the body of another fix, the body of the inner fix
   is check adding the recusrive formal parameter as an additional safe
   argument.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 2855367002ef063677589e455b143d5727453ffa..ffb53c236a3f4faefd8ce1ddb72d1f6c8f528e82 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -347,6 +347,10 @@ and weakly_positive context n nn uri te =
     | C.Lambda (name,so,ta) ->
        C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
         subst_inductive_type_with_dummy_mutind ta)
+    | C.LetIn (name,so,ty,ta) ->
+       C.LetIn (name, subst_inductive_type_with_dummy_mutind so,
+        subst_inductive_type_with_dummy_mutind ty,
+        subst_inductive_type_with_dummy_mutind ta)
     | C.Appl tl ->
        C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
     | C.MutCase (uri,i,outtype,term,pl) ->
@@ -369,6 +373,13 @@ and weakly_positive context n nn uri te =
          exp_named_subst
        in
         C.Const (uri,exp_named_subst')
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map
+         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+         exp_named_subst
+       in
+        C.Var (uri,exp_named_subst')
     | C.MutInd (uri,typeno,exp_named_subst) ->
        let exp_named_subst' =
         List.map
@@ -460,7 +471,6 @@ and strictly_positive context n nn te =
           List.fold_right
           (fun x i -> i && does_not_occur context n nn x)
           arguments true &&
-         (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
           List.fold_right
           (fun x i ->
              i &&
@@ -737,6 +747,8 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
  (*CSC: cfr guarded_by_destructors                             *)
  let module C = Cic in
  let module U = UriManager in
+ (*CSC: we could perform beta-iota(-zeta?) immediately, and
+   delta only on-demand when it fails without *)
  match CicReduction.whd ~subst context te with
      C.Rel m when List.mem m safes -> true
    | C.Rel _ -> false
@@ -919,10 +931,10 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
              x_plus_len safes' bo
          ) fl true
 
-and guarded_by_destructors ~subst context n nn kl x safes =
+and guarded_by_destructors ~subst context n nn kl x safes t =
  let module C = Cic in
  let module U = UriManager in
-  function
+  match CicReduction.whd ~subst context t with
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
       (match List.nth context (m-1) with
@@ -960,10 +972,6 @@ and guarded_by_destructors ~subst context n nn kl x safes =
            i && guarded_by_destructors ~subst context n nn kl x safes param
          ) tl true &&
          check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
-   | C.Appl tl ->
-      List.fold_right
-       (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
-       tl true
    | C.Var (_,exp_named_subst)
    | C.Const (_,exp_named_subst)
    | C.MutInd (_,_,exp_named_subst)
@@ -1023,11 +1031,11 @@ and guarded_by_destructors ~subst context n nn kl x safes =
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
                (fun (p,(_,c,brujinedc)) i ->
+                   i &&
                  let rl' = recursive_args lefts_and_tys 0 len brujinedc in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
                   in
-                   i &&
                    guarded_by_destructors ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
@@ -1098,24 +1106,45 @@ and guarded_by_destructors ~subst context n nn kl x safes =
             (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
             pl true
       )
-   | C.Fix (_, fl) ->
+   | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t->
+      let l = 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
-       and x_plus_len = x + len
-       and tys,_ =
+      let n_plus_len = n + len in
+      let nn_plus_len = nn + len in
+      let x_plus_len = x + len in
+      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
-       and safes' = List.map (fun x -> x + len) safes in
-        List.fold_right
-         (fun (_,_,ty,bo) i ->
-           i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
-            guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
-             x_plus_len safes' bo
-         ) fl true
+         ) ([],0) fl in
+       let safes' = List.map (fun x -> x + len) safes in
+        List.for_all
+         (guarded_by_destructors ~subst context n nn kl x safes) l &&
+        snd (List.fold_left
+         (fun (fixno',i) (_,recno,ty,bo) ->
+           fixno'+1,
+           i &&
+           guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
+           if
+            fixno' = fixno &&
+            List.length l > recno &&
+            (*case where the recursive argument is already really_smaller *)
+            check_is_really_smaller_arg ~subst context n nn kl x safes
+             (List.nth l recno)
+           then
+            let bo_without_lambdas,_,context =
+             eat_lambdas ~subst (tys@context) (recno+1) bo
+            in
+             (* we assume the formal argument to be safe *)
+             guarded_by_destructors ~subst context (n_plus_len+recno+1)
+              (nn_plus_len+recno+1) kl (x_plus_len+recno+1)
+              (1::List.map (fun x -> x+recno+1) safes')
+              bo_without_lambdas
+           else
+            guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len
+             kl x_plus_len safes' bo
+         ) (0,true) fl)
    | C.CoFix (_, fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
@@ -1135,6 +1164,10 @@ and guarded_by_destructors ~subst context n nn kl x safes =
             guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true
+   | C.Appl tl ->
+      List.fold_right
+       (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
+       tl true
 
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
@@ -1935,7 +1968,7 @@ end;
                               (len + eaten) kl 1 [] m) then
                       raise
                         (TypeCheckerFailure 
-                          (lazy ("Fix: not guarded by destructors")))
+                          (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t)))
                     else
                       ugraph2
                 end
@@ -2301,4 +2334,23 @@ let check_allowed_sort_elimination uri i s1 s2 =
   CicUniv.empty_ugraph)
 ;;
 
-Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
+Deannotate.type_of_aux' :=
+ fun context t ->
+  (*CSC: we need to type-check the context to avoid Not_found in
+    get_cooked_obj in CicReduction. However, this implementation may
+    be very inefficient, since we may type-check the same context
+    O(n^2) times. On the other hand, type-checking the context in Deannotate
+    would be a cost to pay not only for Coq objects. *)
+  ignore (
+  List.fold_right
+   (fun el context ->
+      (match el with
+          None -> ()
+        | Some (_,Cic.Decl ty) ->
+           ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph)
+        | Some (_,Cic.Def (bo,ty)) ->
+           ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph);
+           ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph));
+      el::context
+   ) context []);
+  fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;