Missing check implemented: the sort of each constructors should be constrained

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index a5e745af3592ac08dd47fb3f6dc59ebba80ceb1f..6cbb44f8044432db90ae2cd361d2831cb132be8d 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -557,25 +557,35 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
   (* constructors using Prods                                *)
   let len = List.length itl in
   let tys =
-    List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
+    List.rev_map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
   let _,ugraph2 =
     List.fold_right
-      (fun (_,_,_,cl) (i,ugraph) ->
+      (fun (_,_,ty,cl) (i,ugraph) ->
+        let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in
        let ugraph'' = 
           List.fold_left
             (fun ugraph (name,te) -> 
-              let debrujinedte = debrujin_constructor uri len [] te in
-              let augmented_term =
-               List.fold_right
-                 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
-                 itl debrujinedte
-              in
-              let _,ugraph' = type_of ~logger augmented_term ugraph in
+              let te = debrujin_constructor uri len [] te in
+              let context,te = split_prods ~subst:[] tys indparamsno te in
+              let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in
+              let ugraph =
+               match
+                CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
+               with
+                  Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) ->
+                   CicUniv.add_ge u2 u1 ugraph
+                | Cic.Sort _, Cic.Sort Cic.Prop
+                | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp
+                | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
+                | _, _ ->
+                   raise
+                    (TypeCheckerFailure
+                      (lazy ("Wrong constructor or inductive arity shape"))) in
               (* let's check also the positivity conditions *)
               if
                not
-                 (are_all_occurrences_positive tys uri indparamsno i 0 len
-                     debrujinedte)
+                 (are_all_occurrences_positive context uri indparamsno
+                    (i+indparamsno) indparamsno (len+indparamsno) te)
               then
                 begin
                 prerr_endline (UriManager.string_of_uri uri);
@@ -584,7 +594,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
                  (TypeCheckerFailure
                     (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
               else
-               ugraph'
+               ugraph
             ) ugraph cl in
        (i + 1),ugraph''
       ) itl (1,ugrap1)
@@ -708,7 +718,8 @@ and split_prods ~subst context n te =
  let module R = CicReduction in
   match (n, R.whd ~subst context te) with
      (0, _) -> context,te
-   | (n, C.Prod (name,so,ta)) when n > 0 ->
+   | (n, C.Sort _) when n <= 0 -> context,te
+   | (n, C.Prod (name,so,ta)) ->
        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
    | (_, _) -> raise (AssertFailure (lazy "8"))
 
@@ -838,7 +849,9 @@ and guarded_by_destructors
 =
  let module C = Cic in
  let module U = UriManager in
-  match CicReduction.whd ~subst context t with
+  let t = CicReduction.whd ~delta:false ~subst context t in
+  let res =
+   match t with
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
       (match List.nth context (m-1) with
@@ -995,6 +1008,14 @@ and guarded_by_destructors
       List.fold_right
        (fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
        tl true
+  in
+   if res then res
+   else
+    let t' = CicReduction.whd ~subst context t in
+     if t = t' then
+      false
+     else
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t'
 
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
@@ -1318,7 +1339,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
     | C.Var (uri,exp_named_subst) ->
       incr fdebug ;
        let ugraph1 = 
-         check_exp_named_subst ~logger ~subst context exp_named_subst ugraph 
+         check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph 
        in 
        let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
        let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
@@ -1431,7 +1452,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.Const (uri,exp_named_subst) ->
        incr fdebug ;
        let ugraph1 = 
-        check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph 
+        check_exp_named_subst uri ~logger ~subst  context exp_named_subst ugraph 
        in
        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
        let cty1 =
@@ -1442,11 +1463,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.MutInd (uri,i,exp_named_subst) ->
       incr fdebug ;
        let ugraph1 = 
-        check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph 
+        check_exp_named_subst uri ~logger  ~subst context exp_named_subst ugraph 
        in
-        (* TASSI: da me c'era anche questa, ma in CVS no *)
        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
-        (* fine parte dubbia *)
        let cty =
         CicSubstitution.subst_vars exp_named_subst mty
        in
@@ -1454,9 +1473,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
         cty,ugraph2
    | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let ugraph1 = 
-        check_exp_named_subst ~logger ~subst context exp_named_subst ugraph 
+        check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
        in
-        (* TASSI: idem come sopra *)
        let mty,ugraph2 = 
         type_of_mutual_inductive_constr ~logger uri i j ugraph1 
        in
@@ -1763,7 +1781,24 @@ end;
        let (_,ty,_) = List.nth fl i in
         ty,ugraph2
 
- and check_exp_named_subst ~logger ~subst context =
+ and check_exp_named_subst uri ~logger ~subst context ens ugraph =
+   let params =
+    let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    (match obj with
+        Cic.Constant (_,_,_,params,_) -> params
+      | Cic.Variable (_,_,_,params,_) -> params
+      | Cic.CurrentProof (_,_,_,_,params,_) -> params
+      | Cic.InductiveDefinition (_,params,_,_) -> params
+    ) in
+   let rec check_same_order params ens =
+    match params,ens with
+     | _,[] -> ()
+     | [],_::_ ->
+        raise (TypeCheckerFailure (lazy "Bad explicit named substitution"))
+     | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' ->
+        check_same_order tl tl'
+     | _::tl,l -> check_same_order tl l
+   in
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
         [] -> ugraph
@@ -1789,7 +1824,8 @@ end;
                 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
-     check_exp_named_subst_aux ~logger []
+    check_same_order params ens ;
+    check_exp_named_subst_aux ~logger [] ens ugraph
        
  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in