]> matita.cs.unibo.it Git - helm.git/commitdiff
guarded_by_constructor completely rewritten, fixed missing lift when generating the...
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 24 Apr 2008 13:01:26 +0000 (13:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 24 Apr 2008 13:01:26 +0000 (13:01 +0000)
helm/software/components/cic_proof_checking/cicTypeChecker.ml

index 44cf6d24ad1c03bda2f5a61605fb092b4537a3c9..a5e745af3592ac08dd47fb3f6dc59ebba80ceb1f 100644 (file)
@@ -746,7 +746,7 @@ and specialize_inductive_type ~logger ~subst ~metasenv context t =
                cl 
             in
             name, isind, arity, cl)
-          tl
+          tl, paramsno
       | _ -> assert false)
   | _ -> assert false
 
@@ -773,11 +773,15 @@ and check_is_really_smaller_arg
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
       | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
-         let tys = 
+         let tys,_ = 
            specialize_inductive_type ~logger ~subst ~metasenv context term 
          in
-         let tys_ctx = 
-           List.map (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+         let tys_ctx,_ = 
+           List.fold_left
+             (fun (types,len) (n,_,ty,_) ->
+               Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+               len+1) 
+             ([],0) tys
          in
          let _,isinductive,_,cl = List.nth tys i in
          if not isinductive then
@@ -887,12 +891,15 @@ and guarded_by_destructors
            List.for_all
              (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
              tl &&
-           let tys = 
+           let tys,_ = 
              specialize_inductive_type ~logger ~subst ~metasenv context t
            in
-           let tys_ctx = 
-             List.map 
-               (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+           let tys_ctx,_ = 
+             List.fold_left
+               (fun (types,len) (n,_,ty,_) ->
+                 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                 len+1) 
+               ([],0) tys
            in
            let _,isinductive,_,cl = List.nth tys i in
             if not isinductive then
@@ -992,224 +999,112 @@ and guarded_by_destructors
 (* 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.                            *)
-and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
+and guarded_by_constructors ~logger ~subst ~metasenv indURI =
  let module C = Cic in
-  (*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 *)
+ let rec aux context n nn h te =
   match CicReduction.whd ~subst context te with
-     C.Rel m when m > n && m <= nn -> h
-   | C.Rel _ -> true
-   | C.Meta _
+   | C.Rel m when m > n && m <= nn -> h
+   | C.Rel _ 
+   | C.Meta _ -> true
    | C.Sort _
    | C.Implicit _
    | C.Cast _
    | C.Prod _
-   | C.LetIn _ ->
-      (* the term has just been type-checked *)
-      raise (AssertFailure (lazy "17"))
+   | C.MutInd _ 
+   | C.LetIn _ -> raise (AssertFailure (lazy "17"))
    | C.Lambda (name,so,de) ->
       does_not_occur ~subst context n nn so &&
-       guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
-        (n + 1) (nn + 1) h de args coInductiveTypeURI
+      aux ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) h de
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      h &&
-       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
-   | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
-      let consty =
-       let obj,_ = 
-         try 
-           CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
-         with Not_found -> assert false
-       in
-       match obj with
-          C.InductiveDefinition (itl,_,_,_) ->
-           let (_,_,_,cl) = List.nth itl i in
-            let (_,cons) = List.nth cl (j - 1) in
-             CicSubstitution.subst_vars exp_named_subst cons
-        | _ ->
-            raise (TypeCheckerFailure
-             (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
+      h && List.for_all (does_not_occur ~subst context n nn) tl
+   | C.MutConstruct (_,_,_,exp_named_subst) ->
+      List.for_all 
+        (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst
+   | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) as t ->
+      List.for_all 
+        (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst &&
+      let consty, len_tys, tys_ctx, paramsno =
+       let tys, paramsno = 
+         specialize_inductive_type ~logger ~subst ~metasenv context t in
+       let _,_,_,cl = List.nth tys i in  
+       let _,ty = List.nth cl (j-1) in  
+         ty, List.length tys,
+         fst(List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+           Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1)
+          ([],0) tys), paramsno
       in
-       let rec analyse_branch context ty te =
-        match CicReduction.whd ~subst context ty with
-           C.Meta _ -> raise (AssertFailure (lazy "34"))
-         | C.Rel _
-         | C.Var _
-         | C.Sort _ ->
-            does_not_occur ~subst context n nn te
-         | C.Implicit _
-         | C.Cast _ ->
-            raise (AssertFailure (lazy "24"))(* due to type-checking *)
-         | C.Prod (name,so,de) ->
-            analyse_branch ((Some (name,(C.Decl so)))::context) de te
-         | C.Lambda _
-         | C.LetIn _ ->
-            raise (AssertFailure (lazy "25"))(* due to type-checking *)
-         | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> 
-             guarded_by_constructors ~subst context n nn true te []
-              coInductiveTypeURI
-         | C.Appl ((C.MutInd (uri,_,_))::_) -> 
-            guarded_by_constructors ~subst context n nn true te tl
-             coInductiveTypeURI
-         | C.Appl _ ->
-            does_not_occur ~subst context n nn te
-         | C.Const _ -> raise (AssertFailure (lazy "26"))
-         | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
-            guarded_by_constructors ~subst context n nn true te []
-             coInductiveTypeURI
-         | C.MutInd _ ->
-            does_not_occur ~subst context n nn te
-         | C.MutConstruct _ -> raise (AssertFailure (lazy "27"))
-         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
-         (*CSC: in head position.                                       *)
-         | C.MutCase _
-         | C.Fix _
-         | C.CoFix _ ->
-            raise (AssertFailure (lazy "28"))(* due to type-checking *)
+      let rec_params =
+       let c = 
+         debrujin_constructor ~check_exp_named_subst:false
+           indURI len_tys context consty 
        in
-       let rec analyse_instantiated_type context ty l =
-        match CicReduction.whd ~subst context ty with
-           C.Rel _
-         | C.Var _
-         | C.Meta _
-         | C.Sort _
-         | C.Implicit _
-         | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *)
-         | C.Prod (name,so,de) ->
-            begin
-             match l with
-                [] -> true
-              | he::tl ->
-                 analyse_branch context so he &&
-                  analyse_instantiated_type
-                   ((Some (name,(C.Decl so)))::context) de tl
-            end
-         | C.Lambda _
-         | C.LetIn _ ->
-            raise (AssertFailure (lazy "30"))(* due to type-checking *)
-         | C.Appl _ -> 
-            List.fold_left
-             (fun i x -> i && does_not_occur ~subst context n nn x) true l
-         | C.Const _ -> raise (AssertFailure (lazy "31"))
-         | C.MutInd _ ->
-            List.fold_left
-             (fun i x -> i && does_not_occur ~subst context n nn x) true l
-         | C.MutConstruct _ -> raise (AssertFailure (lazy "32"))
-         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
-         (*CSC: in head position.                                       *)
-         | C.MutCase _
-         | C.Fix _
-         | C.CoFix _ ->
-            raise (AssertFailure (lazy "33"))(* due to type-checking *)
-       in
-        let rec instantiate_type args consty =
-         function
-            [] -> true
-          | tlhe::tltl as l ->
-             let consty' = CicReduction.whd ~subst context 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 ~subst context 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 (AssertFailure (lazy "23"))
-                  end
-               | [] -> analyse_instantiated_type context 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 ~subst context n nn x) true tl &&
-       let len = List.length fl in
-        let n_plus_len = n + len
-        and nn_plus_len = nn + len
-        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-        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
-        in
-         List.fold_right
-          (fun (_,ty,bo) i ->
-            i && does_not_occur ~subst context n nn ty &&
-             guarded_by_constructors ~subst (tys@context) 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 ~subst context n nn x) true tl &&
-        does_not_occur ~subst context n nn out &&
-         does_not_occur ~subst context n nn te &&
-          List.fold_right
-           (fun x i ->
-             i &&
-             guarded_by_constructors ~subst context n nn h x args
-              coInductiveTypeURI
-           ) pl true
-   | C.Appl l ->
-      List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
-   | C.Var (_,exp_named_subst)
-   | C.Const (_,exp_named_subst) ->
-      List.fold_right
-       (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
-   | C.MutInd _ -> assert false
-   | C.MutConstruct (_,_,_,exp_named_subst) ->
-      List.fold_right
-       (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
-   | C.MutCase (_,_,out,te,pl) ->
+       let len_ctx = List.length context in
+       recursive_args (context@tys_ctx) len_ctx (len_ctx+len_tys) c
+      in
+      let rec analyse_instantiated_type rec_spec args =
+       match rec_spec, args with
+       | h::rec_spec, he::args -> 
+           aux context n nn h he &&
+           analyse_instantiated_type rec_spec args 
+       | _,[] -> true
+       | _ -> raise (AssertFailure (lazy 
+         ("Too many args for constructor: " ^ String.concat " "
+         (List.map (fun x-> CicPp.ppterm x) args))))
+      in
+      let left, args = HExtlib.split_nth paramsno tl in
+      List.for_all (does_not_occur ~subst context n nn) left &&
+      analyse_instantiated_type rec_params args
+   | C.Appl ((C.MutCase (_,_,out,te,pl))::_) 
+   | C.MutCase (_,_,out,te,pl) as t ->
+       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+       List.for_all (does_not_occur ~subst context n nn) tl &&
        does_not_occur ~subst context n nn out &&
-        does_not_occur ~subst context n nn te &&
-         List.fold_right
-          (fun x i ->
-            i &&
-             guarded_by_constructors ~subst context n nn h x args
-              coInductiveTypeURI
-          ) pl true
-   | C.Fix (_,fl) ->
+       does_not_occur ~subst context n nn te &&
+       List.for_all (aux context n nn h ) pl
+   | C.Fix (_,fl)
+   | C.Appl (C.Fix (_,fl)::_) as t ->
+       let tl = 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
-       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
        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
+          ) ([],0) fl
        in
-        List.fold_right
-         (fun (_,_,ty,bo) i ->
-           i && does_not_occur ~subst context n nn ty &&
-            does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo
-         ) fl true
-   | C.CoFix (_,fl) ->
-      let len = List.length fl in
+        List.for_all (does_not_occur ~subst context n nn) tl &&
+        List.for_all
+         (fun (_,_,ty,bo) ->
+           does_not_occur ~subst context n nn ty &&
+           aux (tys@context) n_plus_len nn_plus_len h bo)
+         fl
+   | C.Appl ((C.CoFix (_,fl))::_) 
+   | C.CoFix (_,fl) as t ->
+       let tl = 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
-       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
        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
+          List.fold_left
+            (fun (types,len) (n,ty,_) ->
+               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                len+1)
+            ) ([],0) fl
        in
-        List.fold_right
-         (fun (_,ty,bo) i ->
-           i && does_not_occur ~subst context n nn ty &&
-            guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
-             h bo
-             args coInductiveTypeURI
-         ) fl true
+       List.for_all (does_not_occur ~subst context n nn) tl &&
+       List.for_all 
+         (fun (_,ty,bo) ->
+            does_not_occur ~subst context n nn ty &&
+            aux (tys@context) n_plus_len nn_plus_len h bo) 
+         fl
+   | C.Var _
+   | C.Const _
+   | C.Appl _ as t -> does_not_occur ~subst context n nn t
+ in
+   aux 
 
 and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   need_dummy ind arity1 arity2 ugraph =
@@ -1852,8 +1747,8 @@ end;
                            let's control the guarded by constructors 
                            conditions C{f,M}
                          *)
-                         if not (guarded_by_constructors ~subst
-                              (types @ context) 0 len false bo [] uri) then
+                         if not (guarded_by_constructors ~logger ~subst ~metasenv uri
+                 (types @ context) 0 len false bo) then
                            raise
                              (TypeCheckerFailure 
                                (lazy "CoFix: not guarded by constructors"))