check_is_really_smaller simplified to consider that it is called only on terms

(immediately put in normal form) that inhabit an inductive type. Moreover,
some duplicated code has been removed.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ffb53c236a3f4faefd8ce1ddb72d1f6c8f528e82..787a0cb3c02e6c8549deb29a4793420c3b591055 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -741,10 +741,7 @@ and eat_lambdas ~subst context n te =
    | (n, te) ->
        raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
 
-(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) 
 and check_is_really_smaller_arg ~subst context n nn kl x safes te =
- (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
- (*CSC: cfr guarded_by_destructors                             *)
  let module C = Cic in
  let module U = UriManager in
  (*CSC: we could perform beta-iota(-zeta?) immediately, and
@@ -752,90 +749,17 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
  match CicReduction.whd ~subst context te with
      C.Rel m when List.mem m safes -> true
    | C.Rel _ -> false
-   | C.Var _
-   | C.Meta _
-   | C.Sort _
-   | C.Implicit _
-   | C.Cast _
-(*   | C.Cast (te,ty) ->
-      check_is_really_smaller_arg ~subst n nn kl x safes te &&
-       check_is_really_smaller_arg ~subst n nn kl x safes ty*)
-(*   | C.Prod (_,so,ta) ->
-      check_is_really_smaller_arg ~subst n nn kl x safes so &&
-       check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
-        (List.map (fun x -> x + 1) safes) ta*)
-   | C.Prod _ -> raise (AssertFailure (lazy "10"))
-   | C.Lambda (name,so,ta) ->
-      check_is_really_smaller_arg ~subst context n nn kl x safes so &&
-       check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
-        (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
-   | C.LetIn (name,so,ty,ta) ->
-      check_is_really_smaller_arg ~subst context n nn kl x safes so &&
-       check_is_really_smaller_arg ~subst context n nn kl x safes ty &&
-        check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context)
-        (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl (he::_) ->
-      (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
-      (*CSC: solo perche' non abbiamo trovato controesempi            *)
       check_is_really_smaller_arg ~subst context n nn kl x safes he
-   | C.Appl [] -> raise (AssertFailure (lazy "11"))
+   | C.MutConstruct _
    | C.Const _
-   | C.MutInd _ -> raise (AssertFailure (lazy "12"))
-   | C.MutConstruct _ -> false
+   | C.Var _ -> false
+   | C.Lambda (name,ty,ta) ->
+      check_is_really_smaller_arg ~subst (Some (name,Cic.Decl ty)::context)
+       (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
-          C.Rel m when List.mem m safes || m = x ->
-           let (lefts_and_tys,len,isinductive,paramsno,cl) =
-           let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let tys =
-                 List.map
-                  (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
-                in
-                 let (_,isinductive,_,cl) = List.nth tl i in
-                  let cl' =
-                   List.map
-                    (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
-                  let lefts =
-                   match tl with
-                      [] -> assert false
-                    | (_,_,ty,_)::_ ->
-                       fst (split_prods ~subst [] paramsno ty)
-                  in
-                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
-           in
-            if not isinductive then
-              List.fold_right
-               (fun p i ->
-                 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
-               pl true
-            else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
-              List.fold_right
-               (fun (p,(_,c)) i ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args lefts_and_tys 0 len debrujinedte
-                 in
-                  let (e,safes',n',nn',x',context') =
-                   get_new_safes ~subst context p c rl' safes n nn x
-                  in
-                   i &&
-                   check_is_really_smaller_arg ~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 ->
+          C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
            let (lefts_and_tys,len,isinductive,paramsno,cl) =
             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
@@ -907,29 +831,13 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
          ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
-         (fun (_,_,ty,bo) i ->
-           i &&
-            check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
-             x_plus_len safes' bo
-         ) fl true
-   | C.CoFix (_, fl) ->
-      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,_ =
-        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 ->
+         (fun (_,_,_,bo) i ->
            i &&
             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true
+   | t ->
+      raise (AssertFailure (lazy ("An inhabitant of an inductive type in normal form cannot have this shape: " ^ CicPp.ppterm t)))
 
 and guarded_by_destructors ~subst context n nn kl x safes t =
  let module C = Cic in
@@ -1030,7 +938,7 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
              guarded_by_destructors ~subst context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
-               (fun (p,(_,c,brujinedc)) i ->
+               (fun (p,(name,c,brujinedc)) i ->
                    i &&
                  let rl' = recursive_args lefts_and_tys 0 len brujinedc in
                   let (e,safes',n',nn',x',context') =
@@ -2336,11 +2244,6 @@ let check_allowed_sort_elimination uri i s1 s2 =
 
 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 ->