Major code semplification in check_allowed_sort_elimination: the

need_dummy and not need_dummy cases are now unified.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2f7075dacf34fca1004e1a1aeb7d7bcf50c1d851..168f6d6aeb091f9e19ac9c1a6ef837efd90b9380 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1278,7 +1278,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   need_dummy ind arity1 arity2 ugraph =
  let module C = Cic in
  let module U = UriManager in
-  match (CicReduction.whd ~subst context arity1, CicReduction.whd ~subst context arity2) with
+  let arity1 = CicReduction.whd ~subst context arity1 in
+  let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
+   match arity1, CicReduction.whd ~subst context arity2 with
      (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
        let b,ugraph1 =
         CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
@@ -1288,6 +1290,14 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
           ugraph1
        else
         false,ugraph1
+   | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy ->
+       let b,ugraph1 =
+        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
+       if not b then
+        false,ugraph1
+       else
+        check_allowed_sort_elimination_aux ugraph1
+         ((Some (name,C.Decl so))::context) ta true
    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
    | (C.Sort C.Prop, C.Sort C.Set)
    | (C.Sort C.Prop, C.Sort C.CProp)
@@ -1335,67 +1345,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
        )
    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
      (* TASSI: da verificare *)
-   | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
-       let b,ugraph1 =
-        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
-       if not b then
-        false,ugraph1
-       else
-         (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
-              C.Sort C.Prop -> true,ugraph1
-           | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
-               (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-                 match o with
-                    C.InductiveDefinition (itl,_,_,_) ->
-                     let (_,_,_,cl) = List.nth itl i in
-                     (* is a singleton definition or the empty proposition? *)
-                     (List.length cl = 1 || List.length cl = 0),ugraph1
-                  | _ ->
-                   raise (TypeCheckerFailure
-                    (lazy
-                      ("Unknown mutual inductive definition:" ^
-                       UriManager.string_of_uri uri))))
-           | _ -> false,ugraph1)
-   | ((C.Sort C.Set, C.Prod (name,so,ta)) 
-   | (C.Sort C.CProp, C.Prod (name,so,ta)))
-     when not need_dummy ->
-       let b,ugraph1 =
-        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
-       if not b then
-        false,ugraph1
-       else
-         (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
-           C.Sort C.Prop
-         | C.Sort C.Set  -> true,ugraph1
-         | C.Sort C.CProp -> true,ugraph1
-         | C.Sort (C.Type _) ->
-             (* TASSI: da verificare *)
-             (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-              match o with
-               C.InductiveDefinition (itl,_,paramsno,_) ->
-                 let (_,_,_,cl) = List.nth itl i in
-                 let tys =
-                   List.map
-                     (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
-                 in
-                 (List.fold_right
-                   (fun (_,x) (i,ugraph) -> 
-                     if i then 
-                       is_small ~logger tys paramsno x ugraph
-                     else
-                       false,ugraph
-                  ) cl (true,ugraph1))
-             | _ ->
-                 raise (TypeCheckerFailure (lazy
-                         ("Unknown mutual inductive definition:" ^
-                          UriManager.string_of_uri uri)))
-             )
-         | _ -> raise (AssertFailure (lazy "19"))
-         )
-   | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
-       (* TASSI: da verificare *)
-       CicReduction.are_convertible ~subst ~metasenv context so ind ugraph
    | (_,_) -> false,ugraph
+ in
+  check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
         
 and type_of_branch ~subst context argsno need_dummy outtype term constype =
  let module C = Cic in