Missing check implemented: uniformity of left parameters in contravariant

position was missing from strictly_positive.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index f450dcd896a6dcaf10495e36cbe4053ccd1b77e0..fa24119b303babd1f406ee71558b81b5a8a7f27d 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -141,6 +141,27 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri n
 
 exception CicEnvironmentError;;
 
+let check_homogeneous_call context indparamsno n uri reduct tl =
+ let last =
+  List.fold_left
+   (fun k x ->
+     if k = 0 then 0
+     else
+      match CicReduction.whd context x with
+      | Cic.Rel m when m = n - (indparamsno - k) -> k - 1
+      | _ -> raise (TypeCheckerFailure (lazy 
+         ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+         string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+         "appl:\n"^ CicPp.ppterm reduct))))
+   indparamsno tl
+ in
+  if last <> 0 then
+   raise (TypeCheckerFailure
+    (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
+     UriManager.string_of_uri uri)))
+;;
+
+
 let rec type_of_constant ~logger uri orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
@@ -329,21 +350,18 @@ and does_not_occur ?(subst=[]) context n nn te =
             does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
           ) fl true
 
-(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
-(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
-(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
-(*CSC strictly_positive                                                  *)
-(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
-and weakly_positive context n nn uri te =
+(* Inductive types being checked for positivity have *)
+(* indexes x s.t. n < x <= nn.                       *)
+and weakly_positive context n nn uri indparamsno posuri te =
  let module C = Cic in
-(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
+  (*CSC: Not very nice. *)
   let leftno = 
     match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
     | Cic.InductiveDefinition (_,_,leftno,_), _ -> leftno
     | _ -> assert false
   in
   let dummy = Cic.Sort Cic.Prop in
-  (*CSC: mettere in cicSubstitution *)
+  (*CSC: to be moved in cicSubstitution? *)
   let rec subst_inductive_type_with_dummy =
    function
       C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
@@ -407,6 +425,10 @@ and weakly_positive context n nn uri te =
         C.MutConstruct (uri,typeno,consno,exp_named_subst')
     | t -> t
   in
+  (* this function has the same semantics of are_all_occurrences_positive
+     but the i-th context entry role is played by dummy and some checks
+     are skipped because we already know that are_all_occurrences_positive
+     of uri in te. *)
   let rec aux context n nn te = 
     match CicReduction.whd context te with
      | C.Appl (C.Sort C.Prop::tl) -> 
@@ -415,13 +437,13 @@ and weakly_positive context n nn uri te =
      | C.Prod (name,source,dest) when
         does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
          (* dummy abstraction, so we behave as in the anonimous case *)
-         strictly_positive context n nn source &&
-           weakly_positive ((Some (name,(C.Decl source)))::context)
-           (n + 1) (nn + 1) uri dest
+         strictly_positive context n nn indparamsno posuri source &&
+           aux ((Some (name,(C.Decl source)))::context)
+           (n + 1) (nn + 1) dest
      | C.Prod (name,source,dest) ->
          does_not_occur context n nn source &&
-           weakly_positive ((Some (name,(C.Decl source)))::context)
-           (n + 1) (nn + 1) uri dest
+           aux ((Some (name,(C.Decl source)))::context)
+           (n + 1) (nn + 1) dest
      | _ ->
        raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
  in 
@@ -439,19 +461,21 @@ and instantiate_parameters params c =
    | (C.Cast (te,_), _) -> instantiate_parameters params te
    | (t,l) -> raise (AssertFailure (lazy "1"))
 
-and strictly_positive context n nn te =
+and strictly_positive context n nn indparamsno posuri te =
  let module C = Cic in
  let module U = UriManager in
   match CicReduction.whd context te with
    | t when does_not_occur context n nn t -> true
-   | C.Rel _ -> true
+   | C.Rel _ when indparamsno = 0 -> true
    | C.Cast (te,ty) ->
       (*CSC: bisogna controllare ty????*)
-      strictly_positive context n nn te
+      strictly_positive context n nn indparamsno posuri te
    | C.Prod (name,so,ta) ->
       does_not_occur context n nn so &&
-       strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
-   | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
+       strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1)
+        indparamsno posuri ta
+   | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
+      check_homogeneous_call context indparamsno n posuri reduct tl;
       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_) 
    | (C.MutInd (uri,i,exp_named_subst)) as t -> 
@@ -485,8 +509,8 @@ and strictly_positive context n nn te =
           (fun x i ->
              i &&
                weakly_positive
-               ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
-               x
+                ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+                indparamsno posuri x
           ) cl' true
    | t -> false
        
@@ -494,30 +518,9 @@ and strictly_positive context n nn te =
 and are_all_occurrences_positive context uri indparamsno i n nn te =
  let module C = Cic in
   match CicReduction.whd context te with
-     C.Appl ((C.Rel m)::tl) when m = i ->
-      (*CSC: riscrivere fermandosi a 0 *)
-      (* let's check if the inductive type is applied at least to *)
-      (* indparamsno parameters                                   *)
-      let last =
-       List.fold_left
-        (fun k x ->
-          if k = 0 then 0
-          else
-           match CicReduction.whd context x with
-              C.Rel m when m = n - (indparamsno - k) -> k - 1
-            | _ ->
-              raise (TypeCheckerFailure
-               (lazy 
-               ("Non-positive occurence in mutual inductive definition(s) [1]" ^
-                UriManager.string_of_uri uri)))
-        ) indparamsno tl
-      in
-       if last = 0 then
-        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-       else
-        raise (TypeCheckerFailure
-         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
-          UriManager.string_of_uri uri)))
+     C.Appl ((C.Rel m)::tl) as reduct when m = i ->
+      check_homogeneous_call context indparamsno n uri reduct tl;
+      List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Rel m when m = i ->
       if indparamsno = 0 then
        true
@@ -528,7 +531,7 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
    | C.Prod (name,source,dest) when
       does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
       (* dummy abstraction, so we behave as in the anonimous case *)
-      strictly_positive context n nn source &&
+      strictly_positive context n nn indparamsno uri source &&
        are_all_occurrences_positive
         ((Some (name,(C.Decl source)))::context) uri indparamsno
         (i+1) (n + 1) (nn + 1) dest